OAI/Computability/BinPacking/Computation/MachineOverlayTable.lean

GitHub source file

134 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.Tape line 14
2. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.Ambient line 15
3. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.State line 16
4. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.graphArchive line 18
5. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.graphStream line 19
6. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.scratch line 20
7. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.vertexCount line 21
8. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.dartCount line 22
9. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.expanderArchive line 23
10. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.expanderStream line 24
11. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.fuel line 25
12. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.vertex line 26
13. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.tail line 27
14. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.oldReverse line 28
15. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.relation line 29
16. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.dividedCopy line 30
17. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.quotient line 31
18. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.newReverse line 32
19. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.rowBuffer line 33
20. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.output line 34
21. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.oldTapes line 36
22. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.expanderTapes line 40
23. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.oldTapes_injective line 44
24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.expanderTapes_injective line 50
25. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.clean line 56
26. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.expanderState line 59
27. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.expanderState_clean line 68
28. inductive OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.MainLabel line 73
29. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.Label line 85
30. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.next line 87
31. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.mainInstruction line 89
32. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.program line 129
33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.program_main line 135
34. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.extraTapes line 138
35. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.splitView line 141
36. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.combine line 145
37. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.initialTapes line 149
38. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.splitTapes line 152
39. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.placedTapes line 155
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.splitTrace line 160
41. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.memory line 180
42. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.memory_graphArchive line 184
43. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.memory_graphStream line 186
44. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.memory_scratch line 188
45. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.memory_vertexCount line 190
46. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.memory_dartCount line 192
47. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.memory_expanderArchive line 194
48. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.memory_expanderStream line 196
49. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.memory_fuel line 198
50. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.memory_vertex line 200
51. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.memory_tail line 202
52. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.memory_oldReverse line 204
53. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.memory_relation line 206
54. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.memory_dividedCopy line 208
55. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.memory_quotient line 210
56. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.memory_newReverse line 212
57. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.memory_rowBuffer line 214
58. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.memory_output line 216
59. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.update_output line 219
60. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.update_expanderStream line 222
61. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.update_graphStream line 226
62. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.update_fuel line 230
63. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.update_vertex line 233
64. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.update_tail line 236
65. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.update_vertexCount line 239
66. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.update_dartCount line 242
67. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.joinTrace line 246
68. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.initialTapes_memory line 250
69. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.splitTapes_memory line 257
70. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.preparationSteps line 265
71. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.preparationTrace line 267
72. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.encodeWords_flatMap line 335
73. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.encodeWords_flatten line 341
74. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.encodeWords_flatten_flatMap line 347
75. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.oldRows line 356
76. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.expanderValues line 357
77. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.oldBlock line 360
78. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.expanderBlock line 362
79. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.oldOutput line 365
80. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.expanderOutput line 367
81. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.outputBlock line 369
82. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.oldOutput_eq line 372
83. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.expanderOutput_eq line 386
84. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.outputBlock_eq line 390
85. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.graphRows_blocks line 396
86. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.expanderRows_blocks line 405
87. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.tableBits_blocks line 410
88. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.remaining line 421
89. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.emittedPrefix line 423
90. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.remaining_step line 426
91. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.prefix_step line 434
92. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.remaining_zero line 441
93. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.remaining_end line 443
94. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.prefix_zero line 447
95. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.prefix_end line 449
96. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.oldFrame line 456
97. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.expanderFrame line 465
98. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.oldVertexTrace line 473
99. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.expanderVertexTrace line 491
100. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.tailCopyTrace line 522
101. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.tailFinishTrace line 539
102. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.pairSteps line 568
103. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.pairTrace line 574
104. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.cleanupSteps line 594
105. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.cleanupTrace line 596
106. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.rawExpander line 625
107. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.outputPrefix line 628
108. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.outputPrefix_step line 631
109. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.loopBase line 636
110. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.loopCost line 642
111. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.loopBodyTraces line 648
112. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.loopTrace line 684
113. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.tableSteps line 718
114. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.tableTrace line 723
115. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.flatMap_length_le line 751
116. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.flatten_length_le line 763
117. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.oldSize line 767
118. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.expanderSize line 768
119. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.blockSize line 769
120. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.oldOutput_length_le line 771
121. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.expanderOutput_length_le line 778
122. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.outputBlock_length_le line 791
123. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.outputCapacity line 799
124. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.outputPrefix_length_le line 801
125. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.pairBudget line 818
126. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.pairSteps_le line 825
127. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.loopSteps_le line 862
128. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.phasePolynomial line 869
129. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.phasePolynomial_eval line 885
130. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.timePolynomial line 893
131. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.tableSteps_le line 896
132. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.tableInTime line 913
133. def OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.machine line 926
134. theorem OAI.BinPackingGames.Foundations.Complexity.MachineOverlayTable.machine_alphabet_finite line 937