OAI/Computability/DirectedFeedback/Machines/MachineLazyTableRuntime.lean

GitHub source file

90 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTableRuntime.rawProgram line 56
2. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTableRuntime.sourceMachine_eq line 64
3. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTableRuntime.cleanupTapes line 68
4. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTableRuntime.cleanup_complete line 72
5. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTableRuntime.terminalRun line 76
6. def OAI.DFVSGames.Foundations.Complexity.MachineLazyTableRuntime.computableInPolyTime line 86
7. theorem OAI.DFVSGames.Foundations.Complexity.MachineLazyTableRuntime.finite_alphabet line 93
8. def OAI.DFVSGames.Foundations.PCP.PreprocessingFinishRuntime.finish line 109
9. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingFinishRuntime.output_eq_finish line 114
10. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingFinishRuntime.finish_degree_positive line 118
11. def OAI.DFVSGames.Foundations.PCP.PreprocessingFinishRuntime.computableInPolyTime line 121
12. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingFinishRuntime.finite_alphabet line 132
13. def OAI.DFVSGames.Foundations.PCP.PreprocessingRuntime.tablePolynomialTime line 151
14. theorem OAI.DFVSGames.Foundations.PCP.PreprocessingRuntime.finiteAlphabet line 164
15. def OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.bitLength line 183
16. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.bitLength_zero line 185
17. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.bitLength_positive line 187
18. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.bitLength_half line 190
19. def OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.increments line 197
20. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.increments_true line 200
21. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.increments_half line 203
22. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.increments_false line 207
23. def OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.coreTime line 212
24. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.coreTime_zero line 217
25. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.coreTime_positive line 219
26. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.coreTime_bound line 223
27. abbrev OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.Alphabet line 233
28. abbrev OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.State line 234
29. def OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.initialState line 236
30. def OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.rawTapes line 238
31. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.update_input_inline_MachineLogCounter line 243
32. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.update_scratch_inline_MachineLogCounter line 248
33. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.update_output_inline_MachineLogCounter line 253
34. def OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.stripLoop line 258
35. def OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.guardLoop line 264
36. def OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.halfLoop line 273
37. def OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.program line 282
38. def OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.machine line 289
39. def OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.configuration line 300
40. def OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.next line 304
41. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.stripStep_true line 306
42. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.stripStep_false line 314
43. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.stripTrace line 322
44. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.halfStep_nil line 338
45. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.halfStep_false line 346
46. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.halfStep_true line 355
47. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.halfTrace line 364
48. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.restoreTrace line 396
49. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.guardStep_zero line 413
50. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.guardStep_positive line 422
51. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.coreTrace line 434
52. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.initList_eq line 467
53. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.haltList_eq line 475
54. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.initialStep line 483
55. def OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.totalTime line 492
56. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.totalTime_bound line 494
57. theorem OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.machineTrace line 499
58. def OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.outputsInTime line 514
59. def OAI.DFVSGames.Foundations.Complexity.MachineLogCounter.computableInPolyTime line 520
60. inductive OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.ExtraTape line 551
61. instance OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.(instance at line 555) line 555
62. inductive OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.ExtraLabel line 557
63. instance OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.(instance at line 562) line 562
64. abbrev OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.Tape line 564
65. abbrev OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.Label line 565
66. abbrev OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.Alphabet line 566
67. abbrev OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.State line 567
68. def OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.initialState line 569
69. def OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.clockLabel line 571
70. def OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.clockStatement line 575
71. def OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.readHeader line 585
72. def OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.program line 591
73. def OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.machine line 609
74. def OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.clockTapes line 620
75. def OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.clockConfiguration line 624
76. theorem OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.clockTapes_update line 628
77. theorem OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.clockStatement_simulation line 635
78. theorem OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.clockStep line 660
79. def OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.clockInTime line 675
80. def OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.startExtra line 693
81. def OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.startMemory line 698
82. theorem OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.startMemory_input_update line 702
83. theorem OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.startMemory_sum_update line 710
84. theorem OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.headerStep_zero line 718
85. theorem OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.headerStep_succ line 732
86. theorem OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.headerTrace line 749
87. def OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.headerInTime line 766
88. theorem OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.initialMemory line 778
89. theorem OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.clockInitialMemory line 790
90. def OAI.DFVSGames.Foundations.Complexity.GraphCounterModel.startInTime line 802