OAI/Computability/MinUncut/Machines/PoweringMachineRotor.lean

GitHub source file

138 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.Alphabet line 17
2. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.reverseRole line 19
3. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.endpointRole line 22
4. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.reverseRole_injective line 25
5. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.endpointRole_injective line 26
6. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.source_outside_reverse line 27
7. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.reverse_outside_endpoint line 28
8. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.reverseTapes line 30
9. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.endpointTapes line 31
10. inductive OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.Label line 33
11. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.instruction line 38
12. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.reverseId line 47
13. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.reverseAddress line 50
14. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.endpointAddress line 53
15. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.reverse_selected line 56
16. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.endpoint_selected line 66
17. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.afterReverse line 72
18. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.finalTapes line 77
19. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.steps line 83
20. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.rotorTrace line 87
21. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.finalTapes_endpoint line 137
22. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.finalTapes_other line 148
23. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.steps_le line 157
24. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineRotor.machine line 174
25. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineWord.Alphabet line 196
26. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineWord.Tape line 197
27. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineWord.first line 199
28. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineWord.shift line 201
29. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineWord.shift_injective line 203
30. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineWord.rotorRole line 207
31. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineWord.rotorRole_injective line 212
32. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineWord.Label line 216
33. instance OAI.MinUncutGames.Foundations.Complexity.PoweringMachineWord.labelFintype line 220
34. instance OAI.MinUncutGames.Foundations.Complexity.PoweringMachineWord.labelDecidableEq line 227
35. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineWord.entry line 234
36. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineWord.copyInstruction line 238
37. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineWord.instruction line 245
38. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineWord.steps line 258
39. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineWord.finalTapes line 264
40. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineWord.finalTapes_other line 273
41. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineWord.wordTrace line 292
42. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineWord.steps_le line 367
43. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineWord.machine line 381
44. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.Tape line 396
45. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.table line 398
46. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.start line 399
47. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.query line 400
48. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.scan line 401
49. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.reverse line 402
50. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.scratch line 403
51. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.leftEndpoint line 404
52. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.rightEndpoint line 405
53. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.leftCopy line 406
54. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.rightCopy line 407
55. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.rowOutput line 408
56. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.endpoint line 410
57. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.endpoint_false line 413
58. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.endpoint_true line 414
59. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole line 416
60. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.trajectoryPlacement line 420
61. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement line 423
62. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_zero line 428
63. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_one line 430
64. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_two line 432
65. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_three line 434
66. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_four line 436
67. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_five line 438
68. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_first line 440
69. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_succ line 442
70. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement line 445
71. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_zero line 449
72. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_one line 450
73. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_two line 451
74. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_three line 452
75. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_four line 453
76. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_five line 454
77. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement line 456
78. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_zero line 460
79. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_one line 461
80. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_two line 462
81. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_three line 463
82. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_four line 464
83. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_five line 465
84. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole_injective line 467
85. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole_ne_start line 470
86. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole_ne_rowOutput line 474
87. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.trajectoryPlacement_injective line 478
88. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.wordShared_ne_trajectory line 499
89. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_injective line 512
90. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_injective line 529
91. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_injective line 533
92. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_ne_rowOutput line 537
93. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineTapes.shared_ne_wordPlacement_succ line 553
94. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.ExtraTape line 567
95. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.GlobalTape line 568
96. abbrev OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.Label line 569
97. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.finalOutput line 571
98. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement line 573
99. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_injective line 576
100. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_start line 582
101. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_table line 586
102. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_scratch line 591
103. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_rowOutput line 596
104. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_ne_finalOutput line 601
105. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_ne_header line 606
106. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement line 612
107. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_injective line 616
108. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_rowOutput line 631
109. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_eq_common line 635
110. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_ne_data line 639
111. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_ne_header line 647
112. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.castTapes line 655
113. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.castStatement line 658
114. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.castConfiguration line 661
115. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.castTapes_apply line 664
116. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.castConfiguration_mk line 670
117. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.stepAux_cast line 676
118. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.boolAlphabet_eq line 684
119. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.mergeTapes line 690
120. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.castTapes_embedding line 695
121. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.dropUnit line 703
122. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.headerStatement line 709
123. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.headerConfiguration line 716
124. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.headerConfiguration_eq line 721
125. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.stepAux_headerStatement line 735
126. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.program line 748
127. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.headerStep line 761
128. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.headerTrace line 777
129. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.initialGlobalTapes line 788
130. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.copyFirstTrace line 791
131. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.initializeTrace line 822
132. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.initializeInTime line 834
133. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.instruction line 847
134. def OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.initializeAtInTime line 851
135. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.final_counter line 866
136. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.final_vertices line 871
137. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.final_darts line 874
138. theorem OAI.MinUncutGames.Foundations.Complexity.PoweringMachineInitialize.final_extra line 877