OAI/Computability/BinPacking/Computation/MachineRegularTable.lean

GitHub source file

211 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.Extra line 12
2. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.Extra.enumList line 16
3. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.Extra.enumList_getElem?_ctorIdx_eq line 19
4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.Extra.enumList_nodup line 23
5. instance OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.(instance at line 25) line 25
6. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.Tape line 29
7. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.Alphabet line 30
8. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.State line 31
9. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.tableTape line 33
10. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.nTape line 34
11. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.queryTape line 35
12. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.fuelTape line 36
13. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.sumTape line 37
14. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.mTape line 38
15. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.indexTape line 39
16. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.workTape line 40
17. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.scratchTape line 41
18. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.verticesTape line 42
19. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.dartsTape line 43
20. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.emitTape line 44
21. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.outputTape line 45
22. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.memory line 47
23. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.frame line 59
24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.frame_table line 62
25. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.frame_n line 64
26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.frame_query line 66
27. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.frame_fuel line 68
28. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.frame_sum line 70
29. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.frame_m line 72
30. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.frame_index line 74
31. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.frame_work line 76
32. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.frame_scratch line 78
33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.frame_vertices line 80
34. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.frame_darts line 82
35. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.frame_emit line 84
36. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.frame_output line 86
37. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_table line 89
38. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_n line 102
39. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_query line 115
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_fuel line 128
41. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_sum line 141
42. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_m line 154
43. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_index line 167
44. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_work line 180
45. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_scratch line 193
46. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_vertices line 206
47. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_darts line 219
48. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_emit line 232
49. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.update_frame_output line 245
50. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.Field line 258
51. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.Field.enumList line 262
52. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.Field.enumList_getElem?_ctorIdx_eq line 264
53. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.Field.enumList_nodup line 268
54. instance OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.(instance at line 270) line 270
55. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.CopyPhase line 274
56. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.CopyPhase.enumList line 278
57. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.CopyPhase.enumList_getElem?_ctorIdx_eq line 280
58. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.CopyPhase.enumList_nodup line 284
59. instance OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.(instance at line 286) line 286
60. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.Label line 290
61. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.fieldTape line 300
62. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.fieldExit line 304
63. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.lookupSlots line 308
64. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.lookupSlots_injective line 311
65. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.copySource line 316
66. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.copyDestination line 321
67. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.copyExit line 325
68. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.prefixView line 330
69. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.prefixView_left line 334
70. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.prefixView_right line 336
71. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.prefixTapes line 340
72. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.program line 351
73. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.appendTrace line 381
74. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.paddingTotal line 385
75. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.vertexTotal line 388
76. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.dartTotal line 391
77. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.vertexTotal_eq line 393
78. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.initStep line 398
79. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.seedMStep line 407
80. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.clearIndexStep line 416
81. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.readTime line 425
82. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.readTrace line 429
83. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.prefixTrace line 476
84. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.computeTime line 496
85. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.computeTrace line 499
86. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.headerBits line 537
87. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.headerBits_eq line 540
88. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.headerBits_length line 544
89. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.cleanupZerosStep line 550
90. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.emitTime line 559
91. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.emitTrace line 563
92. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.totalTime line 626
93. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.trace line 629
94. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.arithmeticPolynomial line 642
95. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.timePolynomial line 649
96. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.totalTime_le line 652
97. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Header.inTime line 694
98. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Fuel.guard line 714
99. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Fuel.guard_succ line 722
100. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Fuel.guard_zero line 729
101. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Fuel.increment line 736
102. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Fuel.increment_step line 739
103. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.Body line 749
104. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.Tape line 750
105. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.Alphabet line 751
106. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.State line 752
107. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.Data line 753
108. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.BaseTable line 754
109. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.sumDecidableEq line 756
110. instance OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.tapeDecidableEq line 767
111. instance OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.tapeBEq line 782
112. instance OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.tapeLawfulBEq line 785
113. instance OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.tapeFintype line 789
114. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.coreTape line 797
115. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.oldFuel line 798
116. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerFuel line 799
117. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.dummyFuel line 800
118. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.scratch line 801
119. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.headerTape line 803
120. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.headerView line 809
121. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.headerView_left line 820
122. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.headerView_right line 829
123. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.bodyView line 848
124. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.bodyView_left line 852
125. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.bodyView_right line 853
126. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerTape line 859
127. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerView line 863
128. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerView_left line 871
129. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerView_right line 877
130. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.headerStates line 886
131. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.readyState line 894
132. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.CopyPhase line 896
133. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.CopyPhase.enumList line 900
134. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.CopyPhase.enumList_getElem?_ctorIdx_eq line 902
135. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.CopyPhase.enumList_nodup line 906
136. instance OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.(instance at line 908) line 908
137. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.copySource line 912
138. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.copyTarget line 915
139. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.Label line 919
140. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.copyExit line 934
141. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.clearTape line 938
142. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.clearEntry line 942
143. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.program line 945
144. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.machine line 965
145. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.frame line 976
146. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.cfg line 982
147. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.frame_core line 987
148. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.bodyPlacement line 991
149. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.headerAux line 1000
150. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.headerAux_empty line 1006
151. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.headerPlacement line 1010
152. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.inputData line 1037
153. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.headerData line 1050
154. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.headerStacks line 1053
155. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.headerTrace line 1057
156. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.oldData line 1076
157. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.originalData_eq line 1079
158. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.oldBodyTrace line 1082
159. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.counterStacks line 1097
160. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.frame_oldFuel line 1100
161. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.frame_ownerFuel line 1104
162. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_oldFuel line 1108
163. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_ownerFuel line 1119
164. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_global line 1130
165. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_owner line 1143
166. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.oldGuardStep line 1156
167. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.oldGuardExit line 1170
168. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.oldIncrementStep line 1181
169. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.oldPrefix line 1195
170. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.oldElapsed line 1198
171. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.joinTrace line 1205

     Also declared: OAI/Computability/BinPacking/Computation/MachineRegularTableRuntime.lean:12 (same declaration text).

172. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.oldPrefixTrace line 1209
173. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.oldLoopTrace line 1240
174. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.frame_scratch line 1252
175. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.frame_darts line 1256
176. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.frame_header_n line 1259
177. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.oldSeedStep line 1263
178. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.copyOldTrace line 1276
179. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.oldStageTrace line 1291
180. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.update_frame_offset line 1301
181. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerData line 1314
182. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerSeedStep line 1322
183. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.copyOwnerTrace line 1340
184. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerPlacement line 1354
185. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerInitialData_eq line 1366
186. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerBodyTrace line 1369
187. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerGuardStep line 1385
188. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerGuardExit line 1399
189. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerIncrementStep line 1410
190. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerPrefix line 1430
191. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerElapsed line 1433
192. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerPrefixTrace line 1440
193. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerLoopTrace line 1470
194. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.ownerStageTrace line 1482
195. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.owner_output_eq_ownerPrefix line 1492
196. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.cleaned line 1508
197. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTime line 1513
198. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.drainTrace line 1518
199. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.cleanupPrefixTrace line 1526
200. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTrace line 1540
201. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.finalStacks line 1546
202. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.cleaned_finalStacks line 1549
203. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.cleaned_length_le line 1569
204. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTime_le line 1583
205. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.cleanupTime_final_le line 1599
206. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.headerOutput line 1663
207. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.oldOutput line 1666
208. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.finalOutput line 1669
209. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.totalTime line 1672
210. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.old_output_eq_originalPrefix line 1678
211. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Top.finalOutput_eq line 1683