OAI/Computability/BinPacking/Computation/MachinePaddedExpanderFamily.lean

GitHub source file

112 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.cycleWords line 10
2. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.cycleTapes line 20
3. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.toBool_cycleTapes line 24
4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.boundaryTapes_eq_cycleTapes line 29
5. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.copyFrame line 39
6. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.returnFrame line 44
7. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.installedFrame line 49
8. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.multipliedFrame line 53
9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.copyFrame_eq_cycleTapes line 58
10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.returnFrame_eq_cycleTapes line 70
11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.copyFrame_eq_update line 84
12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.multipliedFrame_eq_update line 95
13. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCost line 112
14. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCoefficient line 118
15. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamilyBounds.wordLength_add_one_le line 122
16. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeCost_le line 133
17. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamilyBounds.vertexCount_monotone line 171
18. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamilyBounds.level_le_vertexCount line 177
19. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum line 189
20. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_zero line 192
21. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_succ line 195
22. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_add line 199
23. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget line 204
24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_zero line 207
25. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_succ line 210
26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamilyBounds.resizeSum_le line 216
27. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_le line 243
28. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamilyBounds.paddedSize_le_succ_input line 257
29. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamilyBounds.inputCoefficient line 267
30. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamilyBounds.familyBudget_at_boundedLevel_le line 270
31. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.installed_returnFrame line 301
32. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.cleaned_multipliedFrame line 312
33. structure OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.ResizeRun line 328
34. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.resizeInTime line 341
35. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.timeCoefficient line 414
36. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.timePolynomial line 417
37. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.timePolynomial_encoding line 420
38. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.ceilingCost_le line 425
39. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.combinedCost_le line 441
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.familyCost_le line 451
41. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.outputWord line 461
42. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.outputCoefficient line 466
43. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.outputWord_length_le line 469
44. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.levelLoopCost line 498
45. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.levelLoopCost_prefix line 503
46. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.levelLoopCost_zero_start line 516
47. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.levelLoopTapes line 521
48. structure OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.LevelLoopRun line 526
49. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.familySingleStep line 536
50. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.levelLoopInTime line 542
51. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.singleFamilyStep line 580
52. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.familyInTime line 586
53. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.familyInOutputSizeTime line 622
54. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.baseDegree_cloud_growth line 633
55. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.baseDegree_cloud_gt_one line 638
56. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.baseDegree_positive line 642
57. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderFamily.paddedFamilyInTime line 650
58. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.fixedDegree line 675
59. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.SmallTable line 676
60. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.Tape line 677
61. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.Alphabet line 678
62. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.Label line 679
63. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.State line 680
64. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyTape line 682
65. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyView line 684
66. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyView_left line 688
67. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyView_right line 691
68. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingTape line 700
69. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView line 704
70. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView_left line 710
71. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingView_right line 714
72. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyLabel line 726
73. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingLabel line 727
74. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.main line 728
75. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.familyEntry line 729
76. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingStates line 731
77. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingStates_apply line 735
78. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.familySource line 741
79. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingSource line 748
80. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.program line 753
81. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.program_family line 760
82. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.program_ceiling line 766
83. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialState line 771
84. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalState line 774
85. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes line 778
86. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.retainedCeilingTapes line 782
87. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes line 786
88. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes line 791
89. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.initialTapes_input line 796
90. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_input line 799
91. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_power line 802
92. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingInput line 814
93. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingOutput line 817
94. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.retainedFrame line 822
95. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_initial_tapes line 826
96. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_handoff_tapes line 836
97. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_initial_tapes line 852
98. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_final_tapes line 860
99. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_initial_configuration line 868
100. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceiling_handoff_configuration line 877
101. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_initial_configuration line 886
102. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.family_final_configuration line 898
103. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes_level line 912
104. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.handoffTapes_level_shadow line 919
105. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_level_shadow line 922
106. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_remainingLevel line 925
107. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_currentSize line 932
108. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.finalTapes_table line 939
109. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingInTime line 951
110. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.materializeInTime line 973
111. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.paddedInTime line 993
112. def OAI.BinPackingGames.Foundations.Complexity.MachinePaddedExpanderFamily.placedInTime line 1009