OAI/Computability/DirectedFeedback/Machines/MachineExpanderFamilyLoop.lean

GitHub source file

91 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.caller_initialState line 58
2. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.caller_normalizeState line 61
3. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.clearRegister_initialState line 64
4. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.boundaryTapes_update_level line 68
5. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.initialTapes_initialize line 80
6. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.actualStep_of_boolStep line 97
7. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.bool_initializeStep line 110
8. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.bool_levelGuard_succStep line 123
9. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.bool_levelGuard_zeroStep line 136
10. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.bool_doneStep line 148
11. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.initializeStep line 156
12. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_succStep line 168
13. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_zeroStep line 181
14. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.doneStep line 191
15. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.initialize_boundaryStep line 199
16. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_boundary_succStep line 215
17. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_boundary_zeroStep line 226
18. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.levelLoopCost line 247
19. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.levelLoopCost_prefix line 252
20. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.levelLoopCost_zero_start line 265
21. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.levelLoopTapes line 270
22. structure OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.LevelLoopRun line 275
23. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.familySingleStep_inline_MachineExpanderFamilyLoop line 285
24. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.levelLoopInTime line 291
25. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.singleFamilyStep_inline_MachineExpanderFamily line 340
26. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.familyInTime line 346
27. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.familyInOutputSizeTime line 382
28. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.baseDegree_cloud_growth line 393
29. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.baseDegree_cloud_gt_one line 398
30. theorem OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.baseDegree_positive line 402
31. def OAI.DFVSGames.Foundations.Complexity.MachineExpanderFamily.paddedFamilyInTime line 410
32. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree line 436
33. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable line 437
34. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.Tape line 438
35. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.Alphabet line 439
36. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.Label line 440
37. abbrev OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.State line 441
38. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyTape line 443
39. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyView line 445
40. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyView_left line 449
41. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyView_right line 452
42. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingTape line 461
43. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView line 465
44. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView_left line 471
45. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView_right line 475
46. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyLabel line 484
47. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingLabel line 485
48. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.main line 486
49. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyEntry line 487
50. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingStates line 489
51. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingStates_apply line 493
52. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.familySource line 499
53. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingSource line 506
54. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.program line 511
55. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.program_family line 518
56. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.program_ceiling line 524
57. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialState line 529
58. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalState line 532
59. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes line 536
60. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.retainedCeilingTapes line 540
61. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes line 544
62. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes line 549
63. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes_input line 554
64. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_input line 557
65. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_power line 560
66. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingInput line 575
67. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingOutput line 578
68. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.retainedFrame line 583
69. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_initial_tapes line 587
70. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_handoff_tapes line 597
71. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_initial_tapes line 613
72. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_final_tapes line 621
73. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_initial_configuration line 629
74. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_handoff_configuration line 638
75. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_initial_configuration line 647
76. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_final_configuration line 659
77. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes_level line 673
78. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes_level_shadow line 680
79. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_level_shadow line 683
80. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_remainingLevel line 686
81. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_currentSize line 693
82. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_table line 700
83. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.timeCoefficient line 713
84. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.timePolynomial line 716
85. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.timePolynomial_encoding line 719
86. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.ceilingCost_le line 724
87. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.combinedCost_le line 740
88. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.familyCost_le line 750
89. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.outputWord line 760
90. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.outputCoefficient line 765
91. theorem OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.outputWord_length_le line 768