OAI/Computability/BinPacking/Computation/PoweringGlobalEnumeration.lean

GitHub source file

197 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineAffineLookup.Alphabet line 14
2. inductive OAI.BinPackingGames.Foundations.Complexity.MachineAffineLookup.Label line 16
3. def OAI.BinPackingGames.Foundations.Complexity.MachineAffineLookup.instruction line 21
4. def OAI.BinPackingGames.Foundations.Complexity.MachineAffineLookup.steps line 36
5. def OAI.BinPackingGames.Foundations.Complexity.MachineAffineLookup.finalTapes line 41
6. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAffineLookup.initialTapes_eq_update line 46
7. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAffineLookup.affineLookupTrace line 66
8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAffineLookup.steps_le line 94
9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAffineLookup.steps_le_table line 102
10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAffineLookup.finalTapes_other line 109
11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAffineLookup.finalTapes_output line 115
12. def OAI.BinPackingGames.Foundations.Complexity.MachineAffineLookup.machine line 120
13. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.Alphabet line 142
14. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.reverseRole line 144
15. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.endpointRole line 147
16. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.reverseRole_injective line 150
17. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.endpointRole_injective line 151
18. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.source_outside_reverse line 152
19. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.reverse_outside_endpoint line 153
20. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.reverseTapes line 155
21. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.endpointTapes line 156
22. inductive OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.Label line 158
23. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.instruction line 163
24. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.reverseId line 172
25. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.reverseAddress line 175
26. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.endpointAddress line 178
27. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.reverse_selected line 181
28. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.endpoint_selected line 191
29. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.afterReverse line 197
30. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.finalTapes line 202
31. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.steps line 208
32. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.rotorTrace line 212
33. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.finalTapes_endpoint line 262
34. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.finalTapes_other line 273
35. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.steps_le line 282
36. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRotor.machine line 299
37. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelation.Alphabet line 321
38. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelation.address line 323
39. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelation.value line 326
40. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelation.selected line 330
41. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelation.instruction line 342
42. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelation.relationTrace line 348
43. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelation.steps_le line 368
44. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelation.value_eq_accepts line 378
45. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelation.machine line 383
46. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineWord.Alphabet line 397
47. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineWord.Tape line 398
48. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineWord.first line 400
49. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineWord.shift line 402
50. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineWord.shift_injective line 404
51. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineWord.rotorRole line 408
52. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineWord.rotorRole_injective line 413
53. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineWord.Label line 417
54. instance OAI.BinPackingGames.Foundations.Complexity.PoweringMachineWord.labelFintype line 421
55. instance OAI.BinPackingGames.Foundations.Complexity.PoweringMachineWord.labelDecidableEq line 428
56. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineWord.entry line 435
57. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineWord.copyInstruction line 439
58. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineWord.instruction line 446
59. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineWord.steps line 459
60. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineWord.finalTapes line 465
61. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineWord.finalTapes_other line 474
62. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineWord.wordTrace line 493
63. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineWord.steps_le line 568
64. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineWord.machine line 582
65. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.Tape line 597
66. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.table line 599
67. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.start line 600
68. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.query line 601
69. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.scan line 602
70. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.reverse line 603
71. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.scratch line 604
72. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.leftEndpoint line 605
73. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.rightEndpoint line 606
74. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.leftCopy line 607
75. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.rightCopy line 608
76. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.rowOutput line 609
77. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.endpoint line 611
78. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.endpoint_false line 614
79. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.endpoint_true line 615
80. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole line 617
81. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.trajectoryPlacement line 621
82. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement line 624
83. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_zero line 629
84. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_one line 631
85. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_two line 633
86. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_three line 635
87. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_four line 637
88. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_inl_five line 639
89. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_first line 641
90. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_succ line 643
91. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement line 646
92. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_zero line 650
93. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_one line 651
94. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_two line 652
95. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_three line 653
96. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_four line 654
97. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_five line 655
98. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement line 657
99. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_zero line 661
100. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_one line 662
101. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_two line 663
102. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_three line 664
103. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_four line 665
104. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_five line 666
105. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole_injective line 668
106. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole_ne_start line 671
107. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.wordSharedRole_ne_rowOutput line 675
108. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.trajectoryPlacement_injective line 679
109. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.wordShared_ne_trajectory line 700
110. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_injective line 713
111. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.relationPlacement_injective line 730
112. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.equalityPlacement_injective line 734
113. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.wordPlacement_ne_rowOutput line 738
114. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineTapes.shared_ne_wordPlacement_succ line 754
115. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.ExtraTape line 768
116. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.GlobalTape line 769
117. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.Label line 770
118. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.finalOutput line 772
119. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement line 774
120. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_injective line 777
121. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_start line 783
122. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_table line 787
123. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_scratch line 792
124. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_rowOutput line 797
125. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_ne_finalOutput line 802
126. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.commonPlacement_ne_header line 807
127. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement line 813
128. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_injective line 817
129. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_rowOutput line 832
130. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_eq_common line 836
131. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_ne_data line 840
132. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.headerPlacement_ne_header line 848
133. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.castTapes line 856
134. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.castStatement line 859
135. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.castConfiguration line 862
136. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.castTapes_apply line 865
137. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.castConfiguration_mk line 871
138. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.stepAux_cast line 877
139. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.boolAlphabet_eq line 885
140. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.mergeTapes line 891
141. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.castTapes_embedding line 896
142. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.dropUnit line 904
143. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.headerStatement line 910
144. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.headerConfiguration line 917
145. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.headerConfiguration_eq line 922
146. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.stepAux_headerStatement line 936
147. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.program line 949
148. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.headerStep line 962
149. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.headerTrace line 978
150. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.initialGlobalTapes line 989
151. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.copyFirstTrace line 992
152. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.initializeTrace line 1023
153. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.initializeInTime line 1035
154. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.instruction line 1048
155. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.initializeAtInTime line 1052
156. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.final_counter line 1067
157. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.final_vertices line 1072
158. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.final_darts line 1075
159. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineInitialize.final_extra line 1078
160. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelationField.Alphabet line 1093
161. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelationField.State line 1094
162. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelationField.Label line 1095
163. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelationField.lookupTapes line 1097
164. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelationField.lookupTapes_injective line 1101
165. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelationField.source_outside_lookup line 1107
166. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelationField.endpoint line 1117
167. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelationField.endpoint_eq_wordEnd line 1120
168. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelationField.bit line 1127
169. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelationField.instruction line 1131
170. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelationField.afterWord line 1140
171. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelationField.finalTapes line 1146
172. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelationField.steps line 1154
173. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelationField.afterWord_frame line 1160
174. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelationField.finalTapes_frame line 1175
175. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelationField.finalTapes_other line 1192
176. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelationField.fieldTrace line 1205
177. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRelationField.steps_le line 1262
178. def OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.headerTapeEquiv line 1278
179. def OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.unitTapeEquiv line 1289
180. def OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.sharedTapeEquiv line 1295
181. def OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.extraTapeEquiv line 1298
182. def OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.globalTapeEquiv line 1301
183. def OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.enumeration line 1304
184. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.globalTapeEquiv_enumeration line 1307
185. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.enumeration_globalTapeEquiv line 1311
186. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.source_index line 1315
187. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.counter_index line 1318
188. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.vertices_index line 1321
189. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.darts_index line 1324
190. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.sharedRole_index line 1327
191. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.trajectory_index line 1330
192. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.finalOutput_index line 1333
193. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.card_globalTape line 1336
194. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.natCard_globalTape line 1340
195. def OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.allTapes line 1344
196. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.allTapes_length line 1346
197. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalEnumeration.mem_allTapes line 1349