OAI/Computability/BinPacking/Computation/MachineRegularOwnerProgram.lean

GitHub source file

212 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Lift.statement line 19
2. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Lift.configuration line 25
3. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Lift.stepAux line 33
4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Lift.step line 46
5. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularTable.Lift.trace line 68
6. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.CoreTape line 93
7. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.NativeTape line 94
8. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.Tape line 95
9. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.Alphabet line 96
10. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.SmallTable line 97
11. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.FamilyState line 98
12. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.State line 99
13. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.inputNative line 101
14. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.outputNative line 102
15. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.powerNative line 103
16. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.sizeNative line 104
17. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.levelNative line 105
18. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.powerTape line 107
19. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.sizeTape line 108
20. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.levelTape line 109
21. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.familyTape line 111
22. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.familyView line 114
23. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.familyView_left line 118
24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.familyView_right line 125
25. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.stateEquiv line 146
26. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.seedState line 149
27. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.readyState line 152
28. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.sourceProgram line 154
29. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.Label line 158
30. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.program line 164
31. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.frame line 171
32. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.rotor line 175
33. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.resultCore line 178
34. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.working line 181
35. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.working_power line 186
36. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.working_size line 189
37. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.working_level line 193
38. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.update_working_power line 197
39. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.update_working_size line 204
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.update_working_level line 214
41. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.working_empty line 224
42. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.initial_other line 228
43. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.final_other line 234
44. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.initial_placement line 255
45. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.final_placement line 276
46. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.source_initial_state line 324
47. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.source_final_state line 328
48. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.familyInTime line 333
49. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.appendTrace line 354
50. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.cleanupTrace line 358
51. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.cleanupInTime line 380
52. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.startInTime line 389
53. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.timePolynomial line 399
54. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.totalBudget_le line 403
55. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.familyCleanInTime line 414
56. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.result_output line 430
57. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.result_preserves_core line 433
58. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.result_private_empty line 437
59. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularFamily.placedInTime line 441
60. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.Tape line 468
61. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.Alphabet line 469
62. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.CoreState line 470
63. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.MetaState line 471
64. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.FamilyState line 472
65. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.State line 473
66. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.Data line 474
67. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.BaseTable line 475
68. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.degree_positive line 477
69. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.readyState line 480
70. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.metadataTape line 484
71. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.metadataView line 488
72. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.familyTape line 493
73. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.familyView line 497
74. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.vertexView line 502
75. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.metadataView_left line 506
76. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.metadataView_right line 509
77. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.familyView_left line 517
78. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.familyView_right line 520
79. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.vertexView_left line 528
80. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.vertexView_right line 530
81. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.metadataStates line 536
82. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.familyStates line 542
83. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.vertexStates line 543
84. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.Label line 546
85. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.entry line 553
86. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.clearTape line 555
87. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.clearEntry line 559
88. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.clearSource line 562
89. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.vertexSource line 565
90. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.program line 569
91. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.frame line 580
92. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.coreFrame line 585
93. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.cfg line 588
94. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.initialData line 591
95. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.metadataData line 604
96. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.familyData line 607
97. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.emittedBits line 612
98. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.emittedData line 615
99. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.joinTrace line 619
100. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.metadataPlacement line 623
101. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.metadataTrace line 631
102. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.familyPlacement line 647
103. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.familyResultPlacement line 655
104. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.familyExecution line 668
105. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.familySteps line 673
106. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.familyTrace line 677
107. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.clearMemory line 694
108. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.clearSteps line 699
109. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.identityPlacement line 704
110. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.drainTrace line 707
111. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.clearPrefixTrace line 723
112. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.clearTrace line 738
113. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.clearFrame line 744
114. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.coreFrame_eq line 762
115. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.emittedData_eq line 782
116. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.vertexPlacement line 786
117. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.vertexSteps line 797
118. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.vertexTrace line 801
119. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.totalSteps line 820
120. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.originalTrace line 825
121. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBody.originalExecution line 841
122. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.Tape line 857
123. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.State line 858
124. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.Alphabet line 859
125. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.sumDecidableEq line 861
126. instance OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeDecidableEq line 872
127. instance OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeBEq line 884
128. instance OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeLawfulBEq line 887
129. instance OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.tapeFintype line 891
130. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.core line 898
131. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.localRank line 899
132. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.count line 900
133. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.prefixTape line 901
134. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.rotor line 902
135. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.padding line 903
136. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.level line 904
137. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.dummyFuel line 905
138. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.scratch line 906
139. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.cleanupTapes line 908
140. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.Label line 910
141. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.entry line 916
142. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.cleanupEntry line 920
143. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.instruction line 923
144. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.afterAddition line 932
145. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes line 935
146. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.steps line 938
147. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_apply line 941
148. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_prefix line 948
149. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_empty line 953
150. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_other line 957
151. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.finalTapes_scratch line 962
152. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.drainSteps_eq line 968
153. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.additionTraceAt line 974
154. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.traceAt line 999
155. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerCleanup.executionAt line 1019
156. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.wide line 1042
157. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.rowPolynomial line 1043
158. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.outputPolynomial line 1045
159. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.corePolynomial line 1047
160. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.blockPolynomial line 1051
161. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.cleanupPolynomial line 1054
162. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.timePolynomial line 1055
163. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.bodySize line 1059
164. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.blockPolynomial_eval line 1062
165. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.originalTimeBound_le line 1077
166. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.wide_le line 1088
167. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.vertexSteps_le line 1098
168. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.clearSteps_frame line 1124
169. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.cleanupSteps_le line 1131
170. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.totalSteps_le line 1162
171. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.originalInTime line 1180
172. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.Tape line 1199
173. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.Alphabet line 1200
174. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.State line 1201
175. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.Data line 1202
176. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.CoreState line 1203
177. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.MetaState line 1204
178. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.FamilyState line 1205
179. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.BaseTable line 1206
180. instance OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.(instance at line 1208) line 1208
181. instance OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.(instance at line 1209) line 1209
182. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.core line 1211
183. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.paddingTape line 1212
184. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.levelTape line 1213
185. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.dummyFuel line 1214
186. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.scratch line 1215
187. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.readyState line 1217
188. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.metadataTape line 1219
189. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.metadataView line 1222
190. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.familyTape line 1226
191. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.familyView line 1229
192. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.vertexView line 1233
193. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.metadataView_left line 1237
194. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.metadataView_right line 1240
195. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.familyView_left line 1246
196. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.familyView_right line 1249
197. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.vertexView_left line 1255
198. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.vertexView_right line 1257
199. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.metadataStates line 1263
200. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.familyStates line 1269
201. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.vertexStates line 1275
202. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.Label line 1281
203. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.entry line 1293
204. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.program line 1295
205. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.working line 1328
206. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.frame line 1332
207. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.cfg line 1334
208. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.initialData line 1337
209. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.metadataData line 1350
210. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.seededData line 1353
211. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.ownerBits line 1356
212. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularOwnerBody.finalData line 1359