OAI/Computability/DirectedFeedback/Machines/MachinePaddedExpanderFamily.lean

GitHub source file

88 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.ceilingInTime line 59
2. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.materializeInTime line 81
3. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.paddedInTime line 101
4. def OAI.DFVSGames.Foundations.Complexity.MachinePaddedExpanderFamily.placedInTime line 117
5. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.CoreTape line 147
6. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.NativeTape line 148
7. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.Tape line 149
8. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.Alphabet line 150
9. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.SmallTable line 151
10. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.FamilyState line 152
11. abbrev OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.State line 153
12. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.inputNative line 155
13. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.outputNative line 156
14. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.powerNative line 157
15. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.sizeNative line 158
16. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.levelNative line 159
17. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.powerTape line 161
18. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.sizeTape line 162
19. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.levelTape line 163
20. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.familyTape line 165
21. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.familyView line 168
22. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.familyView_left line 172
23. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.familyView_right line 179
24. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.stateEquiv line 200
25. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.seedState line 203
26. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.readyState line 206
27. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.sourceProgram line 208
28. inductive OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.Label line 212
29. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.program line 218
30. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.frame line 225
31. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.rotor line 229
32. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.resultCore line 232
33. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.working line 235
34. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.working_power line 240
35. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.working_size line 243
36. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.working_level line 247
37. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.update_working_power line 251
38. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.update_working_size line 258
39. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.update_working_level line 268
40. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.working_empty line 278
41. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.initial_other_inline_MachineRegularFamily line 282
42. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.final_other_inline_MachineRegularFamily line 288
43. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.initial_placement line 309
44. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.final_placement line 330
45. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.source_initial_state line 378
46. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.source_final_state line 382
47. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.familyInTime line 387
48. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.appendTrace_inline_MachineRegularFamily line 408
49. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.cleanupTrace line 412
50. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.cleanupInTime line 434
51. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.startInTime line 443
52. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.timePolynomial line 453
53. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.totalBudget_le line 457
54. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.familyCleanInTime line 468
55. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.result_output line 484
56. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.result_preserves_core line 487
57. theorem OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.result_private_empty line 491
58. def OAI.DFVSGames.Foundations.Complexity.MachineRegularFamily.placedInTime line 495
59. abbrev OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.Alphabet line 525
60. abbrev OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.State line 526
61. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.zeroTest line 528
62. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.zeroTestTrace line 534
63. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.tapes line 549
64. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.tapes_left line 554
65. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.tapes_right line 559
66. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.tapes_savedLeft line 564
67. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.tapes_savedRight line 569
68. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.update_tapes line 574
69. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.tapes_self line 592
70. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.stop line 596
71. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.scan line 600
72. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.scan_step_zero_left line 615
73. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.scan_step_zero_right line 628
74. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.scan_step_succ line 641
75. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.scanTrace line 656
76. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.transferLeft_tapes line 687
77. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.transferRight_tapes line 694
78. inductive OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.Label line 701
79. instance OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.(instance at line 707) line 707
80. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.statement line 711
81. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.steps line 719
82. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.comparisonTrace line 721
83. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.lessThanTrace line 774
84. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.timePolynomial line 792
85. theorem OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.steps_le_time line 794
86. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.lessThanInPolynomialTime line 800
87. abbrev OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.machine line 816
88. def OAI.DFVSGames.Foundations.Complexity.MachineUnaryLessAt.machineInPolynomialTime line 827