OAI/Computability/DirectedFeedback/Machines/MachineRegularExecutionBounds.lean

GitHub source file

87 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularExecutionBounds.coreTimeBound_mono line 56
2. def OAI.DFVSGames.Foundations.Complexity.MachineRegularExecutionBounds.corePolynomial line 63
3. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularExecutionBounds.corePolynomial_eval line 71
4. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularExecutionBounds.internal_steps_le line 80
5. def OAI.DFVSGames.Foundations.Complexity.MachineRegularExecutionBounds.familyPolynomial line 99
6. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularExecutionBounds.family_budget_le line 103
7. def OAI.DFVSGames.Foundations.Complexity.MachineRegularExecutionBounds.rowPolynomial line 115
8. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularExecutionBounds.rowPolynomial_eval line 119
9. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularExecutionBounds.actual_row_bound_le line 125
10. def OAI.DFVSGames.Foundations.Complexity.MachineRegularExecutionBounds.blockCorePolynomial line 132
11. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularExecutionBounds.coreTimeBound_add_output line 135
12. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularExecutionBounds.block_core_bound_le line 141
13. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.wide line 180
14. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.rowPolynomial line 181
15. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.outputPolynomial line 183
16. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.corePolynomial line 185
17. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.blockPolynomial line 189
18. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.cleanupPolynomial line 192
19. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.timePolynomial line 193
20. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.bodySize line 197
21. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.blockPolynomial_eval line 200
22. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.originalTimeBound_le line 215
23. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.wide_le line 226
24. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.vertexSteps_le line 236
25. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.clearSteps_frame line 262
26. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.cleanupSteps_le line 269
27. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.totalSteps_le line 300
28. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOriginalBodyBounds.originalInTime line 318
29. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.bodySize line 338
30. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.wide line 341
31. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.rowPolynomial line 343
32. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.outputPolynomial line 346
33. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.corePolynomial line 349
34. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.blockPolynomial line 354
35. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.blockPolynomial_eval line 358
36. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.dummyTimeBound_le line 374
37. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.wide_le line 385
38. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.ownerPrefix_length_le line 395
39. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.growingOutput_length_le line 403
40. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.dummySteps_le line 414
41. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.prePolynomial line 445
42. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.loopPolynomial line 448
43. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.cleanupPolynomial line 451
44. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.timePolynomial line 454
45. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.preSteps_le line 458
46. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.loopSteps_le line 477
47. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.allLoopSteps_le line 494
48. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.cleanupSteps_working line 505
49. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.cleanupCost_le line 515
50. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.ownerTime_le line 552
51. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.totalSteps_le line 569
52. def OAI.DFVSGames.Foundations.Complexity.MachineRegularOwnerBodyBounds.ownerInTime line 574
53. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.oldLoopPolynomial line 596
54. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerLoopPolynomial line 601
55. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.timePolynomial line 606
56. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.oldElapsed_prefix_le line 612
57. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.oldElapsed_le line 634
58. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerElapsed_prefix_le line 642
59. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.ownerElapsed_le line 666
60. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.totalTime_le line 675
61. def OAI.DFVSGames.Foundations.Complexity.MachineRegularTable.Top.machineInTime line 691
62. structure OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.Program line 711
63. def OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.extendedLabel line 722
64. def OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.extendedCfg line 726
65. def OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.extendedStmt line 731
66. theorem OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.stepAux_extended line 749
67. def OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.sourceMachine line 775
68. abbrev OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.Label line 786
69. def OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.cleanupLabel line 788
70. def OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.resetLabel line 791
71. def OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.cleanupEntry line 793
72. def OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.completedProgram line 796
73. def OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.completedMachine line 803
74. theorem OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.finiteAlphabet line 814
75. def OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.embeddedCfg line 819
76. theorem OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.step_simulation line 823
77. theorem OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.embedded_init line 839
78. theorem OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.finalTapes_eq line 844
79. theorem OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.haltList_eq line 855
80. def OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.cleanupExecution line 860
81. def OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.outputsInTime line 891
82. def OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.completedTime line 916
83. theorem OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.completedTime_eval line 921
84. structure OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.TerminalRun line 928
85. def OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.computableInPolyTime line 935
86. theorem OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.computableInPolyTime_finite_alphabet line 958
87. def OAI.DFVSGames.Foundations.Complexity.MachineCanonicalOutput.computableInPolyTimeOfEnumeration line 969