OAI/Computability/DirectedFeedback/Machines/MachineOverlayTable.lean

GitHub source file

134 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.Tape line 60
2. abbrev OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.Ambient line 61
3. abbrev OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.State line 62
4. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.graphArchive line 64
5. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.graphStream line 65
6. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.scratch line 66
7. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.vertexCount line 67
8. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.dartCount line 68
9. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.expanderArchive line 69
10. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.expanderStream line 70
11. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.fuel line 71
12. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.vertex line 72
13. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.tail line 73
14. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.oldReverse line 74
15. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.relation line 75
16. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.dividedCopy line 76
17. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.quotient line 77
18. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.newReverse line 78
19. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.rowBuffer line 79
20. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.output line 80
21. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.oldTapes line 82
22. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.expanderTapes line 86
23. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.oldTapes_injective line 90
24. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.expanderTapes_injective line 96
25. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.clean line 102
26. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.expanderState line 105
27. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.expanderState_clean line 114
28. inductive OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.MainLabel line 119
29. abbrev OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.Label line 131
30. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.next line 133
31. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.mainInstruction line 135
32. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.program line 175
33. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.program_main line 181
34. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.extraTapes line 184
35. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.splitView line 187
36. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.combine line 191
37. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.initialTapes line 195
38. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.splitTapes line 198
39. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.placedTapes line 201
40. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.splitTrace line 206
41. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.memory line 226
42. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.memory_graphArchive line 230
43. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.memory_graphStream line 232
44. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.memory_scratch line 234
45. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.memory_vertexCount line 236
46. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.memory_dartCount line 238
47. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.memory_expanderArchive line 240
48. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.memory_expanderStream line 242
49. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.memory_fuel line 244
50. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.memory_vertex line 246
51. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.memory_tail line 248
52. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.memory_oldReverse line 250
53. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.memory_relation line 252
54. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.memory_dividedCopy line 254
55. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.memory_quotient line 256
56. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.memory_newReverse line 258
57. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.memory_rowBuffer line 260
58. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.memory_output line 262
59. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.update_output line 265
60. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.update_expanderStream line 268
61. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.update_graphStream line 272
62. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.update_fuel line 276
63. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.update_vertex line 279
64. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.update_tail line 282
65. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.update_vertexCount line 285
66. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.update_dartCount line 288
67. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.joinTrace_inline_MachineOverlayTable line 292
68. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.initialTapes_memory line 296
69. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.splitTapes_memory line 303
70. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.preparationSteps line 311
71. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.preparationTrace line 313
72. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.encodeWords_flatMap_inline_MachineOverlayTable line 381
73. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.encodeWords_flatten_inline_MachineOverlayTable line 387
74. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.encodeWords_flatten_flatMap_inline_MachineOverlayTable line 393
75. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.oldRows line 402
76. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.expanderValues line 403
77. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.oldBlock line 406
78. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.expanderBlock line 408
79. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.oldOutput line 411
80. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.expanderOutput line 413
81. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.outputBlock line 415
82. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.oldOutput_eq line 418
83. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.expanderOutput_eq line 432
84. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.outputBlock_eq line 436
85. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.graphRows_blocks line 442
86. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.expanderRows_blocks line 451
87. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.tableBits_blocks line 456
88. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.remaining line 467
89. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.emittedPrefix line 469
90. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.remaining_step line 472
91. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.prefix_step line 480
92. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.remaining_zero line 487
93. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.remaining_end line 489
94. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.prefix_zero line 493
95. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.prefix_end line 495
96. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.oldFrame line 502
97. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.expanderFrame line 511
98. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.oldVertexTrace line 519
99. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.expanderVertexTrace line 537
100. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.tailCopyTrace line 568
101. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.tailFinishTrace line 585
102. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.pairSteps line 614
103. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.pairTrace line 620
104. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.cleanupSteps line 640
105. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.cleanupTrace line 642
106. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.rawExpander line 671
107. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.outputPrefix line 674
108. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.outputPrefix_step line 677
109. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.loopBase line 682
110. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.loopCost line 688
111. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.loopBodyTraces line 694
112. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.loopTrace line 730
113. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.tableSteps line 764
114. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.tableTrace line 769
115. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.flatMap_length_le_inline_MachineOverlayTable line 797
116. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.flatten_length_le_inline_MachineOverlayTable line 809
117. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.oldSize line 813
118. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.expanderSize line 814
119. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.blockSize line 815
120. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.oldOutput_length_le line 817
121. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.expanderOutput_length_le line 824
122. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.outputBlock_length_le line 837
123. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.outputCapacity line 845
124. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.outputPrefix_length_le line 847
125. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.pairBudget line 864
126. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.pairSteps_le line 871
127. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.loopSteps_le line 909
128. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.phasePolynomial line 916
129. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.phasePolynomial_eval line 932
130. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.timePolynomial line 940
131. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.tableSteps_le line 943
132. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.tableInTime line 960
133. def OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.machine line 973
134. theorem OAI.DFVSGames.Foundations.Complexity.MachineOverlayTable.machine_alphabet_finite line 984