OAI/Computability/BinPacking/Computation/MachineRegularDummyRow.lean

GitHub source file

137 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineAppendAt.Alphabet line 13
2. def OAI.BinPackingGames.Foundations.Complexity.MachineAppendAt.appendTapes line 15
3. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAppendAt.appendTapes_source line 19
4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAppendAt.appendTapes_destination line 24
5. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAppendAt.appendTapes_other line 28
6. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAppendAt.appendTapes_scratch line 33
7. def OAI.BinPackingGames.Foundations.Complexity.MachineAppendAt.firstTapes line 40
8. def OAI.BinPackingGames.Foundations.Complexity.MachineAppendAt.secondTapes line 43
9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAppendAt.finalTapes_eq line 47
10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineAppendAt.appendTrace line 69
11. def OAI.BinPackingGames.Foundations.Complexity.MachineAppendAt.appendInTime line 139
12. inductive OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.Label line 169
13. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.Label.enumList line 174
14. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.Label.enumList_getElem?_ctorIdx_eq line 177
15. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.Label.enumList_nodup line 181
16. instance OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.(instance at line 183) line 183
17. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.Alphabet line 189
18. def OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.routine line 191
19. def OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.fieldBits line 213
20. def OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.fieldSize line 216
21. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.fieldBits_length line 220
22. def OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.prefixTapes line 224
23. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.prefixTrace line 227
24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.appendTrace line 279
25. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.rowBits_eq line 323
26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.fieldBits_eq_rowBits line 329
27. def OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.timePolynomial line 337
28. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.timePolynomial_bounds line 340
29. def OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.rowAppendInTime line 347
30. def OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.machine line 372
31. def OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.machineRowInTime line 383
32. theorem OAI.BinPackingGames.Foundations.Complexity.MachineTableRows.outputFrame line 413
33. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.trueRelation line 426
34. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.trueBits line 428
35. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.trueBits_length line 430
36. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.rowBits line 436
37. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.rowBits_length line 438
38. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.rowBits_eq_graph_row line 442
39. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.rowsBits line 447
40. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.Label line 451
41. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.start line 453
42. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.rowLabel line 454
43. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.bumpLabel line 456
44. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.fields line 458
45. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.afterPort line 460
46. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.entry line 463
47. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.Alphabet line 468
48. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.continueAt line 470
49. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.stepAux_continueAt line 476
50. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.program line 481
51. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.fieldTapes line 488
52. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.initialTapes line 491
53. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.initializeStep line 494
54. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.rowTrace line 507
55. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.bumpStep line 528
56. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.rowAndBumpTrace line 539
57. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.steps line 550
58. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.suffixTrace line 555
59. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.allTrace line 578
60. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.graphRows line 593
61. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.graphRows_length line 600
62. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.rowsBits_eq_graphRows line 606
63. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.dummyRows line 616
64. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.dummyRows_length line 621
65. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.dummyRowsTrace line 624
66. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.steps_le_bound line 636
67. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.inputSize line 668
68. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.timePolynomial line 671
69. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.timePolynomial_bounds line 677
70. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.machine line 698
71. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.machineInTime line 709
72. def OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.machineDummyInTime line 720
73. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDummyRows.finalFrame line 733
74. inductive OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.Control line 745
75. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.Control.enumList line 749
76. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.Control.enumList_getElem?_ctorIdx_eq line 751
77. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.Control.enumList_nodup line 755
78. instance OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.(instance at line 757) line 757
79. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.Tape line 761
80. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.Label line 762
81. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.Alphabet line 763
82. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.State line 765
83. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.bodyEntry line 767
84. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.extra line 770
85. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.program line 781
86. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.tapes line 784
87. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.cfg line 788
88. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.bodyTrace line 792
89. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.guard_succ line 810
90. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.guard_zero line 821
91. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.bump_step line 832
92. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.paddingBits line 844
93. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.steps line 848
94. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.loopTrace line 853
95. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.initialTapes line 875
96. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.initialize_step line 878
97. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.paddingTrace line 893
98. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.machine line 900
99. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddingRows.execution line 911
100. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddingBounds.rowsBits_length_le line 927
101. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddingBounds.rowBound line 942
102. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddingBounds.rowBound_next line 944
103. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddingBounds.blockRow_le_rowBound line 949
104. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddingBounds.steps_le_bound line 954
105. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddingBounds.inputSize line 1004
106. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddingBounds.rowCap line 1007
107. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddingBounds.rowBound_le_cap line 1009
108. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddingBounds.rowPolynomial line 1022
109. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddingBounds.timePolynomial line 1025
110. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddingBounds.timePolynomial_bounds line 1031
111. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddingCertificate.timePolynomial line 1057
112. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddingCertificate.execution line 1060
113. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyCodec.rowsBits_ofFn line 1080
114. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyCodec.encodeWords_flatMap line 1097
115. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyCodec.rowBits_stay line 1103
116. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLazyCodec.rowsBits_stay line 1110
117. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.Tape line 1126
118. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.Alphabet line 1127
119. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.State line 1128
120. inductive OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.Label line 1130
121. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.reverseIndex line 1136
122. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.emittedBits line 1138
123. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.instruction line 1141
124. structure OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.Input line 1154
125. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.memory line 1161
126. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.memory_input line 1164
127. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.join_trace line 1167
128. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.affine_frame line 1171
129. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.cleanup_frame line 1179
130. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.rowTraceAt line 1188
131. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.cleanupTraceAt line 1210
132. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.steps line 1235
133. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.timeBound line 1240
134. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.steps_eq line 1243
135. theorem OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.traceAt line 1249
136. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.machine line 1276
137. def OAI.BinPackingGames.Foundations.Complexity.MachineRegularDummyRow.machineInTime line 1287