OAI/Computability/MinUncut/Machines/MachinePaddedExpanderFamilyBounds.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.timeCoefficient line 11
2. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.timePolynomial line 14
3. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.timePolynomial_encoding line 17
4. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.ceilingCost_le line 22
5. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.combinedCost_le line 38
6. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.familyCost_le line 48
7. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.outputWord line 58
8. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.outputCoefficient line 63
9. theorem OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamilyBounds.outputWord_length_le line 66
10. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingInTime line 100
11. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.materializeInTime line 122
12. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.paddedInTime line 142
13. def OAI.MinUncutGames.Foundations.Complexity.MachinePaddedExpanderFamily.placedInTime line 158
14. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.CoreTape line 188
15. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.NativeTape line 189
16. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.Tape line 190
17. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.Alphabet line 191
18. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.SmallTable line 192
19. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.FamilyState line 193
20. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.State line 194
21. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.inputNative line 196
22. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.outputNative line 197
23. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.powerNative line 198
24. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.sizeNative line 199
25. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.levelNative line 200
26. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.powerTape line 202
27. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.sizeTape line 203
28. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.levelTape line 204
29. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.familyTape line 206
30. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.familyView line 209
31. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.familyView_left line 213
32. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.familyView_right line 220
33. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.stateEquiv line 241
34. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.seedState line 244
35. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.readyState line 247
36. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.sourceProgram line 249
37. inductive OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.Label line 253
38. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.program line 259
39. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.frame line 266
40. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.rotor line 270
41. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.resultCore line 273
42. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.working line 276
43. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.working_power line 281
44. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.working_size line 284
45. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.working_level line 288
46. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.update_working_power line 292
47. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.update_working_size line 299
48. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.update_working_level line 309
49. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.working_empty line 319
50. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.initial_other line 323
51. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.final_other line 329
52. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.initial_placement line 350
53. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.final_placement line 371
54. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.source_initial_state line 419
55. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.source_final_state line 423
56. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.familyInTime line 428
57. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.appendTrace line 449
58. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.cleanupTrace line 453
59. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.cleanupInTime line 475
60. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.startInTime line 484
61. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.timePolynomial line 494
62. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.totalBudget_le line 498
63. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.familyCleanInTime line 509
64. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.result_output line 525
65. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.result_preserves_core line 528
66. theorem OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.result_private_empty line 532
67. def OAI.MinUncutGames.Foundations.Complexity.MachineRegularFamily.placedInTime line 536
68. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.Alphabet line 565
69. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.State line 566
70. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.zeroTest line 568
71. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.zeroTestTrace line 574
72. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.tapes line 589
73. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.tapes_left line 594
74. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.tapes_right line 599
75. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.tapes_savedLeft line 604
76. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.tapes_savedRight line 609
77. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.update_tapes line 614
78. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.tapes_self line 632
79. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.stop line 636
80. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.scan line 640
81. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.scan_step_zero_left line 655
82. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.scan_step_zero_right line 668
83. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.scan_step_succ line 681
84. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.scanTrace line 696
85. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.transferLeft_tapes line 727
86. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.transferRight_tapes line 734
87. inductive OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.Label line 741
88. instance OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.(instance at line 747) line 747
89. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.statement line 751
90. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.steps line 759
91. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.comparisonTrace line 761
92. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.lessThanTrace line 814
93. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.timePolynomial line 832
94. theorem OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.steps_le_time line 834
95. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.lessThanInPolynomialTime line 840
96. abbrev OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.machine line 856
97. def OAI.MinUncutGames.Foundations.Complexity.MachineUnaryLessAt.machineInPolynomialTime line 867