OAI/Computability/MinUncut/Machines/MachineRegularTableRuntime.lean

GitHub source file

125 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTableRuntime.rawProgram line 16
2. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTableRuntime.sourceMachine_eq line 24
3. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTableRuntime.cleanupTapes line 28
4. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTableRuntime.cleanup_complete line 31
5. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTableRuntime.terminalRun line 35
6. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularTableRuntime.computableInPolyTime line 51
7. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularTableRuntime.finite_alphabet line 59
8. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.Tape line 74
9. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.State line 75
10. inductive OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.Label line 77
11. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.Label.enumList line 81
12. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.Label.enumList_getElem?_ctorIdx_eq line 84
13. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.Label.enumList_nodup line 88
14. instance OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.(instance at line 90) line 90
15. def OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.tapes line 94
16. def OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.initialTapes line 98
17. def OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.resultTapes line 100
18. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.resultTapes_original line 103
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.resultTapes_work line 107
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.resultTapes_scratch line 110
21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.resultTapes_vertices line 113
22. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.resultTapes_darts line 116
23. def OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.program line 119
24. def OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.exactSteps line 127
25. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.splitTrace line 130
26. def OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.timePolynomial line 200
27. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.timePolynomial_eval line 202
28. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.exactSteps_le line 205
29. def OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.splitInTime line 212
30. def OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.machine line 222
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.initial_configuration line 233
32. def OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.rowsBits line 242
33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.tableBits_header_rows line 245
34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.tableTrace line 249
35. def OAI.MinUncutGames.Foundations.Complexity.MachineTableSplit.initializedTableInTime line 257
36. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddingBounds.rowsBits_length_le line 270
37. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddingBounds.rowBound line 285
38. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddingBounds.rowBound_next line 287
39. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddingBounds.blockRow_le_rowBound line 292
40. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddingBounds.steps_le_bound line 297
41. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddingBounds.inputSize line 347
42. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddingBounds.rowCap line 350
43. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddingBounds.rowBound_le_cap line 352
44. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddingBounds.rowPolynomial line 365
45. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddingBounds.timePolynomial line 368
46. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddingBounds.timePolynomial_bounds line 374
47. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddingCertificate.timePolynomial line 402
48. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddingCertificate.execution line 405
49. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddingTable.initialOutput line 428
50. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddingTable.execution line 431
51. inductive OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.Tape line 467
52. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.Tape.enumList line 472
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.Tape.enumList_getElem?_ctorIdx_eq line 475
54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.Tape.enumList_nodup line 479
55. instance OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.(instance at line 481) line 481
56. inductive OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.Label line 485
57. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.Alphabet line 494
58. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.State line 495
59. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.memory line 497
60. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.update_output line 508
61. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.update_vertex line 511
62. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.update_edge line 514
63. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.update_power line 517
64. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.update_fuel line 520
65. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.update_relation line 523
66. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.splitTape line 527
67. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.splitView line 528
68. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.splitView_left line 536
69. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.splitView_right line 538
70. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.powerTape line 542
71. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.powerView line 551
72. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.powerView_left line 562
73. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.powerView_right line 564
74. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.subtractTape line 568
75. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.subtractView line 579
76. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.subtractView_left line 592
77. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.subtractView_right line 594
78. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.rowTape line 598
79. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.rowView line 601
80. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.rowView_left line 611
81. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.rowView_right line 615
82. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.rowAlphabet_eq line 621
83. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.rowStateEquiv line 624
84. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.rowProgram line 630
85. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.program line 637
86. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.appendTrace line 663
87. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.tableBits_split line 667
88. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.splitInitialTapes line 673
89. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.splitResultTapes line 679
90. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.splitTrace line 685
91. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.powerTapes line 702
92. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.powerTrace line 707
93. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.affineTapes line 721
94. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.affineOutputTrace line 728
95. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.headersTrace line 770
96. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.copyPowerTrace line 786
97. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.subtractTapes line 800
98. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.subtractTrace line 807
99. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.rowBoolTapes line 822
100. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.transport_tapes_apply line 827
101. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.rowCastTapes line 834
102. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.rowInitialTapes line 840
103. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.rowFinalTapes line 847
104. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.rowTime line 855
105. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.frameTrace line 858
106. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.rowsTrace line 867
107. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.cleanupTime line 901
108. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.cleanupTrace line 903
109. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.otherTime line 938
110. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.totalTime line 945
111. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.vertexPaddingTrace line 948
112. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.rows_length_le line 984
113. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.darts_length_le line 989
114. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.power_length_bound line 993
115. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.initialOutput_length line 998
116. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.intermediateCoefficient line 1005
117. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.intermediatePolynomial line 1007
118. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.intermediate_bound line 1010
119. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.otherPolynomial line 1025
120. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.otherTime_le line 1029
121. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.timePolynomial line 1045
122. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.totalTime_le line 1048
123. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.vertexPaddingInTime line 1059
124. def OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.machine line 1073
125. theorem OAI.MinUncutGames.Foundations.Complexity.MachineVertexPadding.alphabet_finite line 1084