OAI/Computability/DirectedFeedback/Machines/PoweringMachineWord.lean

GitHub source file

143 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineWord.Alphabet line 60
2. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineWord.Tape line 61
3. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineWord.first line 63
4. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineWord.shift line 65
5. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineWord.shift_injective line 67
6. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineWord.rotorRole line 71
7. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineWord.rotorRole_injective line 76
8. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineWord.Label line 80
9. instance OAI.DFVSGames.Foundations.Complexity.PoweringMachineWord.labelFintype line 84
10. instance OAI.DFVSGames.Foundations.Complexity.PoweringMachineWord.labelDecidableEq line 91
11. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineWord.entry line 98
12. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineWord.copyInstruction line 102
13. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineWord.instruction line 109
14. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineWord.steps line 122
15. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineWord.finalTapes line 128
16. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineWord.finalTapes_other line 137
17. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineWord.wordTrace line 156
18. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineWord.steps_le line 231
19. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineWord.machine line 245
20. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.Tape line 263
21. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.table line 265
22. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.start line 266
23. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.query line 267
24. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.scan line 268
25. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.reverse line 269
26. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.scratch line 270
27. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.leftEndpoint line 271
28. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.rightEndpoint line 272
29. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.leftCopy line 273
30. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.rightCopy line 274
31. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.rowOutput line 275
32. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.endpoint line 277
33. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.endpoint_false line 280
34. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.endpoint_true line 281
35. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole line 283
36. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.trajectoryPlacement line 287
37. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement line 290
38. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_zero line 295
39. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_one line 297
40. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_two line 299
41. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_three line 301
42. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_four line 303
43. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_five line 305
44. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_first line 307
45. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_succ line 309
46. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement line 312
47. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_zero line 316
48. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_one line 317
49. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_two line 318
50. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_three line 319
51. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_four line 320
52. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_five line 321
53. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement line 323
54. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_zero line 327
55. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_one line 328
56. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_two line 329
57. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_three line 330
58. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_four line 331
59. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_five line 332
60. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole_injective line 334
61. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole_ne_start line 337
62. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole_ne_rowOutput line 341
63. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.trajectoryPlacement_injective line 345
64. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.wordShared_ne_trajectory line 366
65. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_injective line 379
66. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_injective line 396
67. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_injective line 400
68. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_ne_rowOutput line 404
69. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineTapes.shared_ne_wordPlacement_succ line 420
70. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.ExtraTape line 437
71. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.GlobalTape line 438
72. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.Label line 439
73. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.finalOutput line 441
74. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement line 443
75. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_injective line 446
76. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_start line 452
77. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_table line 456
78. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_scratch line 461
79. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_rowOutput line 466
80. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_ne_finalOutput line 471
81. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_ne_header line 476
82. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement line 482
83. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_injective line 486
84. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_rowOutput line 501
85. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_eq_common line 505
86. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_ne_data line 509
87. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_ne_header line 517
88. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.castTapes_inline_PoweringMachineInitialize line 525
89. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.castStatement_inline_PoweringMachineInitialize line 528
90. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.castConfiguration_inline_PoweringMachineInitialize line 531
91. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.castTapes_apply_inline_PoweringMachineInitialize line 534
92. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.castConfiguration_mk_inline_PoweringMachineInitialize line 540
93. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.stepAux_cast_inline_PoweringMachineInitialize line 546
94. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.boolAlphabet_eq_inline_PoweringMachineInitialize line 554
95. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.mergeTapes line 560
96. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.castTapes_embedding_inline_PoweringMachineInitialize line 565
97. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.dropUnit_inline_PoweringMachineInitialize line 573
98. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.headerStatement line 579
99. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.headerConfiguration line 586
100. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.headerConfiguration_eq_inline_PoweringMachineInitialize line 591
101. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.stepAux_headerStatement line 605
102. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.program line 618
103. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.headerStep line 631
104. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.headerTrace line 647
105. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.initialGlobalTapes line 658
106. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.copyFirstTrace line 661
107. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.initializeTrace line 692
108. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.initializeInTime line 704
109. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.instruction line 717
110. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.initializeAtInTime line 721
111. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.final_counter line 736
112. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.final_vertices line 741
113. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.final_darts line 744
114. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineInitialize.final_extra line 747
115. def OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.headerTapeEquiv line 760
116. def OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.unitTapeEquiv line 771
117. def OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.sharedTapeEquiv line 777
118. def OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.extraTapeEquiv line 780
119. def OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.globalTapeEquiv line 783
120. def OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.enumeration line 786
121. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.globalTapeEquiv_enumeration line 789
122. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.enumeration_globalTapeEquiv line 793
123. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.source_index line 797
124. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.counter_index line 800
125. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.vertices_index line 803
126. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.darts_index line 806
127. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.sharedRole_index line 809
128. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.trajectory_index line 812
129. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.finalOutput_index line 815
130. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.card_globalTape line 818
131. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.natCard_globalTape line 822
132. def OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.allTapes line 826
133. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.allTapes_length line 828
134. theorem OAI.DFVSGames.Foundations.Complexity.PoweringGlobalEnumeration.mem_allTapes line 831
135. abbrev OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelation.Alphabet line 850
136. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelation.address line 852
137. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelation.value line 855
138. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelation.selected line 859
139. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelation.instruction line 871
140. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelation.relationTrace line 877
141. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelation.steps_le line 897
142. theorem OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelation.value_eq_accepts line 907
143. def OAI.DFVSGames.Foundations.Complexity.PoweringMachineRelation.machine line 912