OAI/Computability/BinPacking/Computation/MachineExpanderRowDivision.lean

GitHub source file

108 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.Complexity.MachineSubroutine.label line 12
2. def OAI.BinPackingGames.Foundations.Complexity.MachineSubroutine.configuration line 16
3. def OAI.BinPackingGames.Foundations.Complexity.MachineSubroutine.statement line 19
4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineSubroutine.stepAux_simulation line 33
5. theorem OAI.BinPackingGames.Foundations.Complexity.MachineSubroutine.step_simulation line 54
6. theorem OAI.BinPackingGames.Foundations.Complexity.MachineSubroutine.trace line 70
7. def OAI.BinPackingGames.Foundations.Complexity.MachineSubroutine.execution line 80
8. def OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.frameStatement line 98
9. def OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.frameConfiguration line 110
10. def OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.frameProgram line 113
11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.frameConfiguration_state line 116
12. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.frameConfiguration_metadata line 119
13. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.frameConfiguration_tapes line 122
14. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.frameStatement_pushBound line 125
15. def OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.statement line 129
16. def OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.configuration line 133
17. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.configuration_state line 137
18. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.configuration_metadata line 141
19. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.configuration_tapes line 145
20. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.statement_pushBound line 149
21. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.frame_stepAux line 159
22. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.frame_step line 180
23. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.frame_advance line 192
24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.frame_iterate line 201
25. def OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.frameExecution line 213
26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.frameExecution_steps line 227
27. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.stepAux_simulation line 232
28. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.step_simulation line 239
29. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.trace line 252
30. def OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.execution line 263
31. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStateFrame.execution_steps line 273
32. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.guard_step_succ line 289
33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.guard_step_zero line 302
34. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.select_step_nonempty line 315
35. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.select_step_empty line 331
36. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.copyTrace line 342
37. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.selectTrace line 357
38. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.skipCycleTrace line 372
39. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.emptyCycleTrace line 390
40. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.successPrefixTrace line 406
41. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.lookupTrace_some line 433
42. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.emptyTrace line 462
43. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.lookupTrace_invalid line 483
44. def OAI.BinPackingGames.Foundations.Complexity.MachineLookup.resultLabel line 505
45. def OAI.BinPackingGames.Foundations.Complexity.MachineLookup.resultOutput line 510
46. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.lookupTrace line 515
47. def OAI.BinPackingGames.Foundations.Complexity.MachineLookup.lookupInTime line 537
48. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.lookupHaltTrace line 553
49. def OAI.BinPackingGames.Foundations.Complexity.MachineLookup.timePolynomial line 567
50. theorem OAI.BinPackingGames.Foundations.Complexity.MachineLookup.timePolynomial_bounds line 569
51. def OAI.BinPackingGames.Foundations.Complexity.MachineLookup.machineInTime line 577
52. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookup.Alphabet line 600
53. def OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookup.initialTapes line 602
54. def OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookup.finalTapes line 607
55. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookup.lookupFramedHaltTrace_some line 614
56. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookup.preservingLookupTrace line 632
57. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookup.preservingLookup_steps_le line 682
58. def OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookup.preservingLookupInTime line 690
59. inductive OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookup.Label line 712
60. def OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookup.program line 716
61. def OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookup.machine line 723
62. abbrev OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookupClean.Alphabet line 743
63. inductive OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookupClean.Label line 745
64. def OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookupClean.statement line 750
65. def OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookupClean.program line 756
66. def OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookupClean.steps line 760
67. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookupClean.remaining_length_le line 764
68. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookupClean.steps_le line 771
69. def OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookupClean.timePolynomial line 779
70. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookupClean.steps_le_timePolynomial line 781
71. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookupClean.traceAt line 787
72. def OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookupClean.inTimeAt line 843
73. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookupClean.initialTapes_eq line 864
74. theorem OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookupClean.traceAt_fromTapes line 873
75. def OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookupClean.machine line 894
76. def OAI.BinPackingGames.Foundations.Complexity.MachinePreservingLookupClean.machineInTime line 905
77. inductive OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.Tape line 928
78. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.Tape.enumList line 935
79. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.Tape.enumList_getElem?_ctorIdx_eq line 939
80. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.Tape.enumList_nodup line 943
81. instance OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.(instance at line 945) line 945
82. inductive OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.Label line 949
83. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.Ambient line 967
84. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.State line 968
85. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.divisionStates line 971
86. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.firstFinish line 978
87. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.secondFinish line 982
88. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.affinePlan line 986
89. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.firstPlan line 991
90. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.secondPlan line 995
91. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.outputPlan line 999
92. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.lookupTape line 1003
93. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.dirtyTape line 1010
94. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.statement line 1020
95. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.program line 1085
96. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.controlStatement_inverse line 1094
97. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.transportedDivision line 1101
98. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.divisionStates_apply line 1160
99. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.divisionState line 1164
100. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.divisionOutput line 1169
101. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.firstDivisionTrace line 1175
102. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.secondDivisionTrace line 1216
103. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_source line 1260
104. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_quotient line 1272
105. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_remainder line 1281
106. theorem OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.divisionOutput_other line 1288
107. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.firstDivisionInTime line 1298
108. def OAI.BinPackingGames.Foundations.Complexity.MachineExpanderRow.secondDivisionInTime line 1322