OAI/Computability/MinUncut/Machines/MachineExpanderFamilyCycle.lean

GitHub source file

86 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.installed_returnFrame line 12
2. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.cleaned_multipliedFrame line 23
3. structure OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.ResizeRun line 39
4. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.resizeInTime line 52
5. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.caller_initialState line 124
6. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.caller_normalizeState line 127
7. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.clearRegister_initialState line 130
8. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.boundaryTapes_update_level line 134
9. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.initialTapes_initialize line 146
10. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.actualStep_of_boolStep line 163
11. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.bool_initializeStep line 176
12. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.bool_levelGuard_succStep line 189
13. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.bool_levelGuard_zeroStep line 202
14. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.bool_doneStep line 214
15. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.initializeStep line 222
16. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_succStep line 234
17. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_zeroStep line 247
18. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.doneStep line 257
19. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.initialize_boundaryStep line 265
20. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_boundary_succStep line 281
21. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.levelGuard_boundary_zeroStep line 292
22. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.levelLoopCost line 306
23. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.levelLoopCost_prefix line 311
24. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.levelLoopCost_zero_start line 324
25. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.levelLoopTapes line 329
26. structure OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.LevelLoopRun line 334
27. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.familySingleStep line 344
28. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.levelLoopInTime line 350
29. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.singleFamilyStep line 392
30. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.familyInTime line 398
31. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.familyInOutputSizeTime line 434
32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.baseDegree_cloud_growth line 445
33. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.baseDegree_cloud_gt_one line 450
34. theorem OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.baseDegree_positive line 454
35. def OAI.MinUncutGames.Foundations.Complexity.MachineExpanderFamily.paddedFamilyInTime line 462
36. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree line 485
37. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable line 486
38. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.Tape line 487
39. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.Alphabet line 488
40. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.Label line 489
41. abbrev OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.State line 490
42. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyTape line 492
43. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyView line 494
44. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyView_left line 498
45. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyView_right line 501
46. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingTape line 510
47. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView line 514
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView_left line 520
49. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView_right line 524
50. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyLabel line 536
51. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingLabel line 537
52. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.main line 538
53. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyEntry line 539
54. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingStates line 541
55. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingStates_apply line 545
56. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.familySource line 551
57. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingSource line 558
58. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.program line 563
59. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.program_family line 570
60. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.program_ceiling line 576
61. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialState line 581
62. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalState line 584
63. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes line 588
64. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.retainedCeilingTapes line 592
65. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes line 596
66. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes line 601
67. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes_input line 606
68. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_input line 609
69. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_power line 612
70. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingInput line 620
71. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingOutput line 623
72. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.retainedFrame line 628
73. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_initial_tapes line 632
74. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_handoff_tapes line 642
75. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_initial_tapes line 658
76. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_final_tapes line 666
77. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_initial_configuration line 674
78. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_handoff_configuration line 683
79. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_initial_configuration line 692
80. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_final_configuration line 704
81. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes_level line 718
82. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes_level_shadow line 725
83. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_level_shadow line 728
84. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_remainingLevel line 731
85. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_currentSize line 738
86. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_table line 745