OAI/Computability/BinPacking/Computation/MachineExpanderTable.lean

GitHub source file

186 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseLabel line 15
2. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.scanPhaseLabel line 19
3. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.reversePhaseLabel line 22
4. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.lookupPhasePort line 25
5. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseAddress line 28
6. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseAddress_eq_rowIndex line 31
7. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.lookupTape_injective line 39
8. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes line 43
9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_index line 48
10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_work line 56
11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_output line 62
12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_other line 68
13. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_table line 75
14. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_restore line 81
15. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseTrace line 106
16. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.lookupPhaseInTime line 128
17. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.reversePhaseTrace line 154
18. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.reversePhaseInTime line 170
19. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.reversePhaseTrace_unary line 182
20. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_zero line 202
21. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_one line 203
22. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_two line 204
23. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_three line 205
24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_four line 206
25. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.dirtyTape_five line 207
26. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes line 211
27. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.cleanupSteps line 224
28. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.cleanupSteps_eq_sum line 233
29. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_dirty line 237
30. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_other line 243
31. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_table line 260
32. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_inputVertex line 265
33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.cleanupTapes_output line 270
34. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.join_trace line 275
35. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.cleanupOneTraceAt line 281
36. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.cleanupTraceAt line 298
37. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.doneStepAt line 323
38. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.cleanupExitTraceAt line 333
39. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.initializedTapes line 350
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.initializeStepAt line 359
41. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.clearedQueryTapes line 372
42. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.clearQueryStepAt line 377
43. structure OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData line 396
44. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.rowData line 403
45. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.control0 line 411
46. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.firstRow line 412
47. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue line 413
48. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.firstPair line 414
49. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.firstVertex line 415
50. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.firstReturn line 416
51. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.control1 line 417
52. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.secondRow line 418
53. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue line 419
54. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.secondPair line 420
55. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.secondVertex line 421
56. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.secondReturn line 422
57. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.control2 line 423
58. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.query1 line 424
59. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.query2 line 425
60. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.finalValue line 426
61. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.tableLength line 427
62. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.query1_eq_firstRow line 429
63. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.query2_eq_secondRow line 432
64. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue_div_degree line 435
65. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue_mod_degree line 436
66. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue_div_degree line 437
67. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue_mod_degree line 438
68. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.firstReturn_eq_residue line 440
69. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.secondReturn_eq_residue line 444
70. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.receiveFirst_residue_eq_control1 line 448
71. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.receiveSecond_residue_eq_control2 line 454
72. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.firstSelected line 460
73. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.secondSelected line 464
74. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.evaluateRow_eq line 468
75. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.finalValue_eq_step_reverseIndex line 471
76. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.rows_le_tableLength line 478
77. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.query1_le_tableLength line 482
78. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.query2_le_tableLength line 486
79. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.firstValue_le_tableLength line 490
80. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.secondValue_le_tableLength line 493
81. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.inputVertex_le_tableLength line 496
82. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.firstVertex_le_tableLength line 501
83. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.secondVertex_le_tableLength line 505
84. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.firstReturn_le_tableLength line 509
85. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.RowData.secondReturn_le_tableLength line 513
86. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frameContents line 521
87. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame0 line 535
88. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame1 line 537
89. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame2 line 539
90. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame3 line 541
91. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame4 line 544
92. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame5 line 546
93. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame6 line 548
94. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame7 line 550
95. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame8 line 552
96. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame9 line 555
97. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame10 line 557
98. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame11 line 559
99. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame12 line 561
100. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.lookupResultTapes_id_eq line 564
101. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame1_eq line 572
102. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame2_eq line 578
103. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame3_eq line 584
104. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame4_eq line 590
105. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame5_eq line 596
106. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame6_eq line 604
107. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame7_eq line 610
108. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame8_eq line 617
109. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame9_eq line 624
110. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame10_eq line 631
111. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame11_eq line 639
112. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame12_eq line 647
113. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.final_frame_eq line 653
114. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame0_inputVertex line 658
115. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame0_table line 661
116. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame0_output line 664
117. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame1_inputVertex line 667
118. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame1_emitScratch line 670
119. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame2_queryReverse line 673
120. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame2_queryIndex line 676
121. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame3_table line 679
122. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame3_lookupRestore line 682
123. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame3_lookupWork line 685
124. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame3_lookupOutput line 688
125. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame3_queryIndex line 691
126. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame4_lookupOutput line 694
127. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame4_quotientFirst line 697
128. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame4_remainderFirst line 700
129. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame6_quotientFirst line 703
130. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame6_emitScratch line 706
131. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame7_queryReverse line 709
132. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame7_queryIndex line 712
133. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame8_table line 715
134. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame8_lookupRestore line 718
135. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame8_lookupWork line 721
136. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame8_lookupOutput line 724
137. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame8_queryIndex line 727
138. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame9_lookupOutput line 730
139. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame9_quotientSecond line 733
140. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame9_remainderSecond line 736
141. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame10_quotientSecond line 739
142. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame10_emitScratch line 742
143. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.frame10_output line 745
144. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.final_dirty_word_length_le line 748
145. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.cleanupSteps_le_tableLength line 756
146. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.concatenate line 770
147. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.rowSteps line 774
148. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.rowTraceAt line 792
149. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.rowSteps_le line 916
150. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.rowInTimeAt line 934
151. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.rowInTime line 949
152. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.singleStep line 968
153. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.sequence line 974
154. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.widen line 981
155. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.tableRowData line 987
156. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.tableRowData_finalValue line 991
157. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.tableRowData_frame0 line 995
158. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.tableRowData_finalFrame line 1002
159. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.rowAfterState line 1015
160. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.rowAfterState_position line 1021
161. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.caller_rowAfterState line 1026
162. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.preparedRowInTime line 1030
163. structure OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.VertexSuffixRun line 1059
164. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.suffixRun_aux line 1073
165. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.suffixInTime line 1127
166. structure OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.VertexRun line 1134
167. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.vertexInTime line 1148
168. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.oldTableWord line 1164
169. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices line 1167
170. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices_zero line 1171
171. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices_succ line 1175
172. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.accumulatedVertices_full line 1181
173. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.vertexBodyBudget line 1186
174. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.vertexLoopBudget line 1189
175. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.vertexLoopTapes line 1192
176. structure OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.VertexLoopRun line 1196
177. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.boundarySingleStep line 1207
178. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.vertexLoopInTime line 1213
179. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.completeBudget line 1261
180. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.timeCoefficient line 1264
181. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.timePolynomial line 1267
182. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.vertices_le_word_length line 1270
183. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.completeBudget_le line 1279
184. structure OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.TableRun line 1314
185. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.initializeInTime line 1326
186. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderTable.tableInTime line 1343