OAI/Computability/DirectedFeedback/Encoding/PreprocessingStageMaps.lean

GitHub source file

126 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DFVSGames.Foundations.PCP.PreprocessingStageMaps.BaseTable line 9
2. def OAI.DFVSGames.Foundations.PCP.PreprocessingStageMaps.regular line 11
3. def OAI.DFVSGames.Foundations.PCP.PreprocessingStageMaps.padding line 14
4. def OAI.DFVSGames.Foundations.PCP.PreprocessingStageMaps.familyAt line 18
5. def OAI.DFVSGames.Foundations.PCP.PreprocessingStageMaps.paddedOverlay line 23
6. def OAI.DFVSGames.Foundations.PCP.PreprocessingStageMaps.lazy line 28
7. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingStageMaps.output_eq line 31
8. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTableRuntime.rawProgram line 44
9. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTableRuntime.sourceMachine_eq line 52
10. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTableRuntime.cleanupTapes line 56
11. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTableRuntime.cleanup_complete line 59
12. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTableRuntime.terminalRun line 63
13. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTableRuntime.computableInPolyTime line 75
14. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTableRuntime.finite_alphabet line 83
15. abbrev OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.Tape line 95
16. abbrev OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.State line 96
17. inductive OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.Label line 98
18. instance OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.(instance at line 102) line 102
19. def OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.tapes line 104
20. def OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.initialTapes line 108
21. def OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.resultTapes line 110
22. theorem OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.resultTapes_original line 113
23. theorem OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.resultTapes_work line 117
24. theorem OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.resultTapes_scratch line 120
25. theorem OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.resultTapes_vertices line 123
26. theorem OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.resultTapes_darts line 126
27. def OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.program line 129
28. def OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.exactSteps line 137
29. theorem OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.splitTrace line 140
30. def OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.timePolynomial line 210
31. theorem OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.timePolynomial_eval line 212
32. theorem OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.exactSteps_le line 215
33. def OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.splitInTime line 222
34. def OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.machine line 232
35. theorem OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.initial_configuration line 243
36. def OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.rowsBits line 251
37. theorem OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.tableBits_header_rows line 254
38. theorem OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.tableTrace line 258
39. def OAI.DFVSGames.Foundations.Complexity.MachineTableSplit.initializedTableInTime line 266
40. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddingBounds.rowsBits_length_le line 277
41. def OAI.DFVSGames.Foundations.Complexity.MachinePaddingBounds.rowBound line 292
42. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddingBounds.rowBound_next line 294
43. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddingBounds.blockRow_le_rowBound line 299
44. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddingBounds.steps_le_bound line 304
45. def OAI.DFVSGames.Foundations.Complexity.MachinePaddingBounds.inputSize line 354
46. def OAI.DFVSGames.Foundations.Complexity.MachinePaddingBounds.rowCap line 357
47. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddingBounds.rowBound_le_cap line 359
48. def OAI.DFVSGames.Foundations.Complexity.MachinePaddingBounds.rowPolynomial line 372
49. def OAI.DFVSGames.Foundations.Complexity.MachinePaddingBounds.timePolynomial line 375
50. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddingBounds.timePolynomial_bounds line 381
51. def OAI.DFVSGames.Foundations.Complexity.MachinePaddingCertificate.timePolynomial line 407
52. def OAI.DFVSGames.Foundations.Complexity.MachinePaddingCertificate.execution line 410
53. def OAI.DFVSGames.Foundations.Complexity.MachinePaddingTable.initialOutput line 430
54. def OAI.DFVSGames.Foundations.Complexity.MachinePaddingTable.execution line 433
55. inductive OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.Tape line 465
56. instance OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.(instance at line 470) line 470
57. inductive OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.Label line 472
58. abbrev OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.Alphabet line 481
59. abbrev OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.State line 482
60. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.memory line 484
61. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.update_output line 495
62. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.update_vertex line 498
63. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.update_edge line 501
64. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.update_power line 504
65. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.update_fuel line 507
66. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.update_relation line 510
67. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.splitTape line 514
68. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.splitView line 515
69. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.splitView_left line 523
70. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.splitView_right line 525
71. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.powerTape line 529
72. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.powerView line 538
73. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.powerView_left line 549
74. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.powerView_right line 551
75. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.subtractTape line 555
76. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.subtractView line 566
77. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.subtractView_left line 579
78. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.subtractView_right line 581
79. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.rowTape line 585
80. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.rowView line 588
81. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.rowView_left line 598
82. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.rowView_right line 602
83. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.rowAlphabet_eq line 608
84. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.rowStateEquiv line 611
85. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.rowProgram line 617
86. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.program line 624
87. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.appendTrace_inline_MachineVertexPadding line 650
88. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.tableBits_split line 654
89. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.splitInitialTapes line 660
90. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.splitResultTapes line 666
91. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.splitTrace line 672
92. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.powerTapes line 689
93. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.powerTrace line 694
94. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.affineTapes line 708
95. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.affineOutputTrace line 715
96. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.headersTrace line 757
97. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.copyPowerTrace line 773
98. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.subtractTapes line 787
99. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.subtractTrace line 794
100. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.rowBoolTapes line 809
101. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.transport_tapes_apply_inline_MachineVertexPadding line 814
102. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.rowCastTapes line 821
103. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.rowInitialTapes line 827
104. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.rowFinalTapes line 834
105. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.rowTime line 842
106. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.frameTrace_inline_MachineVertexPadding line 845
107. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.rowsTrace line 854
108. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.cleanupTime line 888
109. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.cleanupTrace line 890
110. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.otherTime line 925
111. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.totalTime line 932
112. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.vertexPaddingTrace line 935
113. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.rows_length_le line 971
114. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.darts_length_le line 976
115. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.power_length_bound line 980
116. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.initialOutput_length line 985
117. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.intermediateCoefficient line 992
118. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.intermediatePolynomial line 994
119. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.intermediate_bound line 997
120. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.otherPolynomial line 1012
121. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.otherTime_le line 1016
122. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.timePolynomial line 1032
123. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.totalTime_le line 1035
124. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.vertexPaddingInTime line 1046
125. def OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.machine line 1060
126. theorem OAI.DFVSGames.Foundations.Complexity.MachineVertexPadding.alphabet_finite line 1071