OAI/Computability/MinUncut/Machines/MachineOverlayTable.lean

GitHub source file

134 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.Tape line 17
2. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.Ambient line 18
3. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.State line 19
4. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.graphArchive line 21
5. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.graphStream line 22
6. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.scratch line 23
7. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.vertexCount line 24
8. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.dartCount line 25
9. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.expanderArchive line 26
10. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.expanderStream line 27
11. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.fuel line 28
12. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.vertex line 29
13. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.tail line 30
14. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.oldReverse line 31
15. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.relation line 32
16. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.dividedCopy line 33
17. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.quotient line 34
18. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.newReverse line 35
19. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.rowBuffer line 36
20. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.output line 37
21. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.oldTapes line 39
22. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.expanderTapes line 43
23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.oldTapes_injective line 47
24. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.expanderTapes_injective line 53
25. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.clean line 59
26. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.expanderState line 62
27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.expanderState_clean line 71
28. inductive OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.MainLabel line 76
29. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.Label line 88
30. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.next line 90
31. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.mainInstruction line 92
32. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.program line 132
33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.program_main line 138
34. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.extraTapes line 141
35. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.splitView line 144
36. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.combine line 148
37. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.initialTapes line 152
38. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.splitTapes line 155
39. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.placedTapes line 158
40. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.splitTrace line 163
41. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.memory line 183
42. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.memory_graphArchive line 187
43. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.memory_graphStream line 189
44. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.memory_scratch line 191
45. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.memory_vertexCount line 193
46. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.memory_dartCount line 195
47. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.memory_expanderArchive line 197
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.memory_expanderStream line 199
49. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.memory_fuel line 201
50. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.memory_vertex line 203
51. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.memory_tail line 205
52. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.memory_oldReverse line 207
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.memory_relation line 209
54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.memory_dividedCopy line 211
55. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.memory_quotient line 213
56. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.memory_newReverse line 215
57. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.memory_rowBuffer line 217
58. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.memory_output line 219
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.update_output line 222
60. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.update_expanderStream line 225
61. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.update_graphStream line 229
62. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.update_fuel line 233
63. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.update_vertex line 236
64. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.update_tail line 239
65. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.update_vertexCount line 242
66. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.update_dartCount line 245
67. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.joinTrace line 249
68. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.initialTapes_memory line 253
69. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.splitTapes_memory line 260
70. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.preparationSteps line 268
71. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.preparationTrace line 270
72. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.encodeWords_flatMap line 338
73. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.encodeWords_flatten line 344
74. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.encodeWords_flatten_flatMap line 350
75. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.oldRows line 359
76. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.expanderValues line 360
77. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.oldBlock line 363
78. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.expanderBlock line 365
79. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.oldOutput line 368
80. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.expanderOutput line 370
81. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.outputBlock line 372
82. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.oldOutput_eq line 375
83. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.expanderOutput_eq line 389
84. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.outputBlock_eq line 393
85. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.graphRows_blocks line 399
86. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.expanderRows_blocks line 408
87. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.tableBits_blocks line 413
88. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.remaining line 424
89. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.emittedPrefix line 426
90. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.remaining_step line 429
91. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.prefix_step line 437
92. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.remaining_zero line 444
93. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.remaining_end line 446
94. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.prefix_zero line 450
95. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.prefix_end line 452
96. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.oldFrame line 459
97. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.expanderFrame line 468
98. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.oldVertexTrace line 476
99. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.expanderVertexTrace line 494
100. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.tailCopyTrace line 525
101. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.tailFinishTrace line 542
102. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.pairSteps line 571
103. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.pairTrace line 577
104. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.cleanupSteps line 597
105. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.cleanupTrace line 599
106. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.rawExpander line 628
107. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.outputPrefix line 631
108. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.outputPrefix_step line 634
109. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.loopBase line 639
110. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.loopCost line 645
111. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.loopBodyTraces line 651
112. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.loopTrace line 687
113. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.tableSteps line 721
114. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.tableTrace line 726
115. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.flatMap_length_le line 754
116. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.flatten_length_le line 766
117. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.oldSize line 770
118. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.expanderSize line 771
119. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.blockSize line 772
120. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.oldOutput_length_le line 774
121. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.expanderOutput_length_le line 781
122. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.outputBlock_length_le line 794
123. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.outputCapacity line 802
124. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.outputPrefix_length_le line 804
125. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.pairBudget line 821
126. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.pairSteps_le line 828
127. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.loopSteps_le line 865
128. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.phasePolynomial line 872
129. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.phasePolynomial_eval line 888
130. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.timePolynomial line 896
131. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.tableSteps_le line 899
132. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.tableInTime line 916
133. def OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.machine line 929
134. theorem OAI.MinUncutGames.Foundations.Complexity.MachineOverlayTable.machine_alphabet_finite line 940