OAI/Computability/DirectedFeedback/Machines/RuntimeSpace.lean

GitHub source file

85 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeSpace.configurationLength line 14
2. theorem OAI.DFVSGames.Foundations.Hastad.SourceRuntimeSpace.initial_configurationLength line 17
3. theorem OAI.DFVSGames.Foundations.Hastad.SourceRuntimeSpace.step_configurationLength line 27
4. theorem OAI.DFVSGames.Foundations.Hastad.SourceRuntimeSpace.execution_configurationLength line 36
5. theorem OAI.DFVSGames.Foundations.Hastad.SourceRuntimeSpace.prefix_configurationLength line 44
6. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeSpace.spacePolynomial line 51
7. theorem OAI.DFVSGames.Foundations.Hastad.SourceRuntimeSpace.spacePolynomial_eval line 54
8. theorem OAI.DFVSGames.Foundations.Hastad.SourceRuntimeSpace.prefix_length_polynomial line 59
9. theorem OAI.DFVSGames.Foundations.Hastad.SourceRuntimeSpace.totalLength_eq_configurationLength line 67
10. theorem OAI.DFVSGames.Foundations.Hastad.SourceRuntimeSpace.finishCost_le_of_prefix line 73
11. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeSpace.completedTime line 89
12. theorem OAI.DFVSGames.Foundations.Hastad.SourceRuntimeSpace.completedTime_eval line 93
13. def OAI.DFVSGames.Foundations.Hastad.SourceRuntimeSpace.prefixAndFinishInTime line 100
14. inductive OAI.DFVSGames.Foundations.Complexity.MachineRepeat.ExtraTape line 127
15. instance OAI.DFVSGames.Foundations.Complexity.MachineRepeat.(instance at line 130) line 130
16. inductive OAI.DFVSGames.Foundations.Complexity.MachineRepeat.Phase line 134
17. instance OAI.DFVSGames.Foundations.Complexity.MachineRepeat.(instance at line 137) line 137
18. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRepeat.Tape line 142
19. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRepeat.Symbols line 143
20. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRepeat.Label line 144
21. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRepeat.State line 145
22. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.extraTapes line 147
23. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.auxProgram line 153
24. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.program line 174
25. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.machine line 178
26. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.inputTapes line 196
27. theorem OAI.DFVSGames.Foundations.Complexity.MachineRepeat.inputTapes_input line 199
28. theorem OAI.DFVSGames.Foundations.Complexity.MachineRepeat.inputTapes_counter line 203
29. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.inputConfig line 206
30. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.embedded line 210
31. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.temporaryTapes line 215
32. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.temporaryConfig line 218
33. theorem OAI.DFVSGames.Foundations.Complexity.MachineRepeat.inputTapes_update_input_inline_MachineRepeat line 222
34. theorem OAI.DFVSGames.Foundations.Complexity.MachineRepeat.inputTapes_update_counter_inline_MachineRepeat line 234
35. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.oneStep_inline_MachineRepeat line 243
36. theorem OAI.DFVSGames.Foundations.Complexity.MachineRepeat.parseStep_true line 251
37. theorem OAI.DFVSGames.Foundations.Complexity.MachineRepeat.parseStep_false line 260
38. theorem OAI.DFVSGames.Foundations.Complexity.MachineRepeat.parseTrace line 269
39. theorem OAI.DFVSGames.Foundations.Complexity.MachineRepeat.guardStep_some line 294
40. theorem OAI.DFVSGames.Foundations.Complexity.MachineRepeat.guardStep_none line 303
41. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.bodyExecution line 311
42. theorem OAI.DFVSGames.Foundations.Complexity.MachineRepeat.bodyToTemp_tapes_inline_MachineRepeat line 321
43. theorem OAI.DFVSGames.Foundations.Complexity.MachineRepeat.tempToBody_tapes_inline_MachineRepeat line 337
44. theorem OAI.DFVSGames.Foundations.Complexity.MachineRepeat.finalToTemp_tapes_inline_MachineRepeat line 349
45. theorem OAI.DFVSGames.Foundations.Complexity.MachineRepeat.tempToOutput_tapes_inline_MachineRepeat line 361
46. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.bodyToTemp line 373
47. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.tempToBody line 389
48. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.finalToTemp line 404
49. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.tempToOutput line 416
50. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.bodyReturn line 429
51. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.finish line 440
52. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.loopBudget line 452
53. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.loopExecution line 457
54. theorem OAI.DFVSGames.Foundations.Complexity.MachineRepeat.inputConfig_init_inline_MachineRepeat line 496
55. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.executeSequence line 508
56. theorem OAI.DFVSGames.Foundations.Complexity.MachineRepeat.loopBudget_eq_sum line 537
57. def OAI.DFVSGames.Foundations.Complexity.MachineRepeat.executeSequenceSum line 548
58. theorem OAI.DFVSGames.Foundations.Complexity.MachineRepeat.loopBudget_le line 561
59. def OAI.DFVSGames.Foundations.Complexity.MachineFiniteAlphabet.FiniteAlphabet line 588
60. theorem OAI.DFVSGames.Foundations.Complexity.MachineFiniteAlphabet.input_finite line 590
61. theorem OAI.DFVSGames.Foundations.Complexity.MachineFiniteAlphabet.of_homogeneous line 594
62. theorem OAI.DFVSGames.Foundations.Complexity.MachineFiniteAlphabet.of_bool line 600
63. theorem OAI.DFVSGames.Foundations.Complexity.MachineFiniteAlphabet.of_equiv line 603
64. theorem OAI.DFVSGames.Foundations.Complexity.MachineFiniteAlphabet.symbols_finite line 608
65. theorem OAI.DFVSGames.Foundations.Complexity.MachineFiniteAlphabet.sequential_machine line 614
66. theorem OAI.DFVSGames.Foundations.Complexity.MachineFiniteAlphabet.compose line 625
67. theorem OAI.DFVSGames.Foundations.Complexity.MachineFiniteAlphabet.composeBits line 636
68. theorem OAI.DFVSGames.Foundations.Complexity.MachineFiniteAlphabet.repeat_machine line 645
69. def OAI.DFVSGames.Explicit.MachineUniformRun.outputBits line 664
70. def OAI.DFVSGames.Explicit.MachineUniformRun.afterScale line 667
71. def OAI.DFVSGames.Explicit.MachineUniformRun.afterEmit line 671
72. def OAI.DFVSGames.Explicit.MachineUniformRun.scaleInTime line 675
73. theorem OAI.DFVSGames.Explicit.MachineUniformRun.repeated_template line 697
74. theorem OAI.DFVSGames.Explicit.MachineUniformRun.template_output line 708
75. theorem OAI.DFVSGames.Explicit.MachineUniformRun.template_copiedLength line 720
76. def OAI.DFVSGames.Explicit.MachineUniformRun.emitInTime line 727
77. def OAI.DFVSGames.Explicit.MachineUniformRun.prefixPolynomial line 744
78. theorem OAI.DFVSGames.Explicit.MachineUniformRun.input_length line 747
79. def OAI.DFVSGames.Explicit.MachineUniformRun.prefixInTime line 751
80. def OAI.DFVSGames.Explicit.MachineUniformRun.timePolynomial line 768
81. theorem OAI.DFVSGames.Explicit.MachineUniformRun.haltList_eq line 771
82. def OAI.DFVSGames.Explicit.MachineUniformRun.finishStartInTime line 780
83. def OAI.DFVSGames.Explicit.MachineUniformRun.outputInTime line 791
84. def OAI.DFVSGames.Explicit.MachineUniformRun.computation line 825
85. theorem OAI.DFVSGames.Explicit.MachineUniformRun.finiteAlphabet line 844