OAI/Computability/DirectedFeedback/Games/PoweringReach.lean

GitHub source file

127 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Foundations.PCP.PoweringReach.ReachLE line 12
2. theorem OAI.DFVSGames.Foundations.PCP.PoweringReach.reach_refl line 15
3. theorem OAI.DFVSGames.Foundations.PCP.PoweringReach.reach_mono line 18
4. theorem OAI.DFVSGames.Foundations.PCP.PoweringReach.reach_prepend line 23
5. def OAI.DFVSGames.Foundations.PCP.PoweringReach.reversePorts line 30
6. theorem OAI.DFVSGames.Foundations.PCP.PoweringReach.reversePorts_length line 34
7. theorem OAI.DFVSGames.Foundations.PCP.PoweringReach.walkEnd_reversePorts line 40
8. theorem OAI.DFVSGames.Foundations.PCP.PoweringReach.wordEnd_eq_walkEnd_ofFn line 51
9. theorem OAI.DFVSGames.Foundations.PCP.PoweringReach.reach_reverse line 61
10. theorem OAI.DFVSGames.Foundations.PCP.PoweringReach.tail_reach line 73
11. theorem OAI.DFVSGames.Foundations.PCP.PoweringReach.head_reach_endpoint line 87
12. def OAI.DFVSGames.Foundations.PCP.PoweringReach.tailFromStart line 101
13. def OAI.DFVSGames.Foundations.PCP.PoweringReach.headFromEnd line 105
14. theorem OAI.DFVSGames.Foundations.PCP.PoweringReach.tailFromStart_val line 109
15. theorem OAI.DFVSGames.Foundations.PCP.PoweringReach.headFromEnd_val line 113
16. def OAI.DFVSGames.Foundations.PCP.PoweringTest.baseGraph line 125
17. def OAI.DFVSGames.Foundations.PCP.PoweringTest.pathAccepts line 134
18. theorem OAI.DFVSGames.Foundations.PCP.PoweringTest.pathAccepts_eq_true_iff line 142
19. abbrev OAI.DFVSGames.Foundations.PCP.PoweringTest.Dart line 153
20. def OAI.DFVSGames.Foundations.PCP.PoweringTest.reverseDart line 155
21. theorem OAI.DFVSGames.Foundations.PCP.PoweringTest.reverseDart_involutive line 165
22. def OAI.DFVSGames.Foundations.PCP.PoweringTest.poweredGraph line 170
23. theorem OAI.DFVSGames.Foundations.PCP.PoweringTest.poweredGraph_tail_false line 182
24. theorem OAI.DFVSGames.Foundations.PCP.PoweringTest.poweredGraph_tail_true line 187
25. theorem OAI.DFVSGames.Foundations.PCP.PoweringTest.poweredGraph_edgeSatisfied line 192
26. theorem OAI.DFVSGames.Foundations.PCP.PoweringTest.rejection_mean_eq_path_mean line 201
27. theorem OAI.DFVSGames.Foundations.PCP.PoweringTest.pathAccepts_honest line 212
28. theorem OAI.DFVSGames.Foundations.PCP.PoweringTest.perfect_completeness line 226
29. theorem OAI.DFVSGames.Foundations.PCP.PoweringTest.preserves_satisfiability line 237
30. def OAI.DFVSGames.Foundations.PCP.PoweringTest.decodedBad line 249
31. theorem OAI.DFVSGames.Foundations.PCP.PoweringTest.decodedBad_eq_true_iff line 253
32. theorem OAI.DFVSGames.Foundations.PCP.PoweringTest.decodedBad_rot line 259
33. def OAI.DFVSGames.Foundations.PCP.PoweringTest.witness line 268
34. theorem OAI.DFVSGames.Foundations.PCP.PoweringTest.witness_bad line 280
35. theorem OAI.DFVSGames.Foundations.PCP.PoweringTest.witness_implies_path_rejection line 288
36. theorem OAI.DFVSGames.Foundations.PCP.PoweringTest.witness_implies_rejection line 315
37. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.match_in_tail_inline_PoweringOpinionTables line 335
38. def OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.firstIndex line 342
39. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.get_firstIndex line 349
40. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.firstIndex_matches line 362
41. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.firstIndex_is_first line 367
42. abbrev OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.AddressIndex line 383
43. def OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.addressIndex line 387
44. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.addressIndex_get line 394
45. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.addressIndex_matches line 403
46. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.addressIndex_is_first line 409
47. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.addressIndex_lt line 415
48. abbrev OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.LabelTable line 421
49. def OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.labelTable line 423
50. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.labelTable_get line 426
51. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.labelTable_addressIndex line 431
52. structure OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.WalkOpinionRow line 438
53. abbrev OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.WalkRows line 443
54. def OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.walkRows line 445
55. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.walkRows_edge line 452
56. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.walkRows_tail_value line 457
57. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.walkRows_head_value line 465
58. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.walkRows_length line 473
59. def OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.rowsAccepts line 478
60. theorem OAI.DFVSGames.Foundations.PCP.PoweringOpinionTables.rowsAccepts_walkRows line 483
61. abbrev OAI.DFVSGames.Foundations.PCP.GenericGraphTables.Label line 499
62. abbrev OAI.DFVSGames.Foundations.PCP.GenericGraphTables.RelationTable line 500
63. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.relationIndex line 504
64. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.relationIndex_val line 506
65. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.relationAt line 509
66. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.relationOf line 512
67. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.relationAt_relationOf line 515
68. structure OAI.DFVSGames.Foundations.PCP.GenericGraphTables.DartRow line 519
69. abbrev OAI.DFVSGames.Foundations.PCP.GenericGraphTables.Rows line 524
70. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.reverseAt line 526
71. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.acceptsAt line 529
72. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.Valid line 532
73. instance OAI.DFVSGames.Foundations.PCP.GenericGraphTables.(instance at line 536) line 536
74. structure OAI.DFVSGames.Foundations.PCP.GenericGraphTables.Table line 540
75. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.rowList line 546
76. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.rowList_length line 548
77. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.semantics line 551
78. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.semantics_reverse line 562
79. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.semantics_tail line 565
80. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.semantics_accepts line 568
81. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.graphRows line 571
82. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.reverseAt_graphRows line 574
83. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.acceptsAt_graphRows line 579
84. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.graphRows_valid line 584
85. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.ofGraph line 592
86. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_reverse line 595
87. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_tail line 600
88. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_accepts line 606
89. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_edgeSatisfied line 611
90. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.constraintGraph_ext_inline_GenericGraphTables line 616
91. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph line 630
92. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.semantics_ofGraph_rejectionCount line 639
93. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.enumeratedGraph line 645
94. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.enumeratedGraph_edgeSatisfied line 661
95. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.enumeratedGraph_rejectionCount line 669
96. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.ofEnumeratedGraph line 681
97. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.bitWord line 685
98. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.parseBit line 687
99. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.parseBit_bitWord line 692
100. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.parseBits_bitWords line 695
101. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.relationWords line 701
102. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.relationWords_length line 703
103. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.parseRelation line 706
104. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.parseRelation_encoded line 712
105. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.rowWords line 719
106. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.parseRow line 722
107. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.parseRow_encoded line 730
108. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.parseRows line 738
109. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.parseRows_encoded line 746
110. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.tableWords line 752
111. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.tableBits line 755
112. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.decodeTableWords line 757
113. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.decodeTableWords_encoded line 768
114. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.decodeTableBits line 776
115. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.decodeTableBits_encoded line 779
116. def OAI.DFVSGames.Foundations.PCP.GenericGraphTables.encoding line 783
117. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.tableBits_injective line 788
118. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.rowWords_length line 790
119. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.rowsWords_length line 796
120. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.tableWords_length line 802
121. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.tableWords_length_le_bits line 807
122. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.relationBits_length_le line 812
123. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.rowBits_length_le line 820
124. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.rowsBits_length_le line 829
125. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.tableBits_length_le line 839
126. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.vertices_le_tableBits_length line 848
127. theorem OAI.DFVSGames.Foundations.PCP.GenericGraphTables.darts_le_tableBits_length line 854