OAI/Computability/BinPacking/Computation/MachineUnaryLessAt.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineEmbedding.Alphabet line 13
2. def OAI.BinPackingGames.Foundations.Complexity.MachineEmbedding.tapes line 17
3. theorem OAI.BinPackingGames.Foundations.Complexity.MachineEmbedding.tapes_inl line 22
4. theorem OAI.BinPackingGames.Foundations.Complexity.MachineEmbedding.tapes_inr line 25
5. def OAI.BinPackingGames.Foundations.Complexity.MachineEmbedding.label line 28
6. def OAI.BinPackingGames.Foundations.Complexity.MachineEmbedding.configuration line 32
7. def OAI.BinPackingGames.Foundations.Complexity.MachineEmbedding.statement line 39
8. theorem OAI.BinPackingGames.Foundations.Complexity.MachineEmbedding.tapes_update line 56
9. theorem OAI.BinPackingGames.Foundations.Complexity.MachineEmbedding.stepAux_simulation line 69
10. theorem OAI.BinPackingGames.Foundations.Complexity.MachineEmbedding.stepAux_preserves_extra_state line 95
11. theorem OAI.BinPackingGames.Foundations.Complexity.MachineEmbedding.stepAux_preserves_extra_tape line 103
12. def OAI.BinPackingGames.Foundations.Complexity.MachineEmbedding.program line 111
13. theorem OAI.BinPackingGames.Foundations.Complexity.MachineEmbedding.step_running line 117
14. theorem OAI.BinPackingGames.Foundations.Complexity.MachineEmbedding.step_simulation line 130
15. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineStackSwap.Alphabet line 156
16. def OAI.BinPackingGames.Foundations.Complexity.MachineStackSwap.tapes line 159
17. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStackSwap.tapes_first line 165
18. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStackSwap.tapes_second line 167
19. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStackSwap.tapes_third line 169
20. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStackSwap.tapes_involutive line 172
21. def OAI.BinPackingGames.Foundations.Complexity.MachineStackSwap.configuration line 177
22. def OAI.BinPackingGames.Foundations.Complexity.MachineStackSwap.statement line 183
23. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStackSwap.tapes_update_first line 200
24. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStackSwap.tapes_update_second line 212
25. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStackSwap.tapes_update_third line 224
26. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStackSwap.stepAux_simulation line 236
27. def OAI.BinPackingGames.Foundations.Complexity.MachineStackSwap.program line 284
28. theorem OAI.BinPackingGames.Foundations.Complexity.MachineStackSwap.step_simulation line 287
29. def OAI.BinPackingGames.Foundations.Complexity.MachineComposition.advance line 303
30. theorem OAI.BinPackingGames.Foundations.Complexity.MachineComposition.advance_none line 306
31. theorem OAI.BinPackingGames.Foundations.Complexity.MachineComposition.advance_some line 309
32. theorem OAI.BinPackingGames.Foundations.Complexity.MachineComposition.advance_iterate_none line 312
33. theorem OAI.BinPackingGames.Foundations.Complexity.MachineComposition.liftSuccessfulTrace line 318
34. def OAI.BinPackingGames.Foundations.Complexity.MachineComposition.liftExecutionInTime line 342
35. theorem OAI.BinPackingGames.Foundations.Complexity.MachineComposition.liftExecutionInTime_steps line 356
36. def OAI.BinPackingGames.Foundations.Complexity.MachineComposition.embeddedExecution line 363
37. theorem OAI.BinPackingGames.Foundations.Complexity.MachineComposition.natPolynomial_eval_mono line 381
38. def OAI.BinPackingGames.Foundations.Complexity.MachineComposition.compositionPolynomial line 390
39. theorem OAI.BinPackingGames.Foundations.Complexity.MachineComposition.compositionBudget_le line 393
40. def OAI.BinPackingGames.Foundations.Complexity.MachineComposition.fourPhaseExecution line 404
41. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineCopy.Alphabet line 439
42. def OAI.BinPackingGames.Foundations.Complexity.MachineCopy.forkLoop line 441
43. def OAI.BinPackingGames.Foundations.Complexity.MachineCopy.forkTapes line 449
44. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCopy.forkTapes_source line 454
45. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCopy.forkTapes_left line 460
46. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCopy.forkTapes_right line 465
47. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCopy.forkTapes_self line 470
48. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCopy.update_fork_source line 474
49. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCopy.update_fork_left line 488
50. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCopy.update_fork_right line 499
51. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCopy.forkStep_empty line 505
52. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCopy.forkStep_cons line 521
53. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCopy.forkTrace line 539
54. def OAI.BinPackingGames.Foundations.Complexity.MachineCopy.forkInTime line 566
55. def OAI.BinPackingGames.Foundations.Complexity.MachineCopy.drainedTapes line 586
56. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCopy.restoredTapes line 589
57. theorem OAI.BinPackingGames.Foundations.Complexity.MachineCopy.copyTrace line 607
58. def OAI.BinPackingGames.Foundations.Complexity.MachineCopy.copyInTime line 648
59. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineDrain.Alphabet line 677
60. def OAI.BinPackingGames.Foundations.Complexity.MachineDrain.drain line 679
61. theorem OAI.BinPackingGames.Foundations.Complexity.MachineDrain.drainTrace line 686
62. def OAI.BinPackingGames.Foundations.Complexity.MachineDrain.drainInTime line 707
63. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.Alphabet line 733
64. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.finish line 735
65. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.scan line 738
66. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.seed line 748
67. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.tapes line 752
68. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.tapes_source line 756
69. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.tapes_scratch line 762
70. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.tapes_destination line 767
71. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.update_source line 772
72. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.update_scratch line 786
73. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.update_destination line 797
74. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.prepend_replicate_word line 803
75. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.scan_step_succ line 808
76. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.scan_step_zero line 828
77. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.scanTrace line 845
78. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.restoreTapes line 875
79. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.affineTrace line 894
80. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.affineInTime line 930
81. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.seededAffineTrace line 950
82. inductive OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.Label line 984
83. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.Label.enumList line 988
84. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.Label.enumList_getElem?_ctorIdx_eq line 990
85. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.Label.enumList_nodup line 994
86. instance OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.(instance at line 996) line 996
87. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.program line 1000
88. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryAffineAt.machine line 1006
89. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.Alphabet line 1025
90. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.State line 1026
91. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.zeroTest line 1028
92. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.zeroTestTrace line 1034
93. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.tapes line 1049
94. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.tapes_left line 1054
95. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.tapes_right line 1059
96. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.tapes_savedLeft line 1064
97. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.tapes_savedRight line 1069
98. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.update_tapes line 1074
99. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.tapes_self line 1092
100. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.stop line 1096
101. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.scan line 1100
102. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.scan_step_zero_left line 1115
103. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.scan_step_zero_right line 1128
104. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.scan_step_succ line 1141
105. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.scanTrace line 1156
106. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.transferLeft_tapes line 1187
107. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.transferRight_tapes line 1194
108. inductive OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.Label line 1201
109. instance OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.(instance at line 1207) line 1207
110. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.statement line 1211
111. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.steps line 1219
112. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.comparisonTrace line 1221
113. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.lessThanTrace line 1274
114. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.timePolynomial line 1292
115. theorem OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.steps_le_time line 1294
116. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.lessThanInPolynomialTime line 1300
117. abbrev OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.machine line 1316
118. def OAI.BinPackingGames.Foundations.Complexity.MachineUnaryLessAt.machineInPolynomialTime line 1327