OAI/Computability/BinPacking/Computation/PoweringMachineRuntime.lean

GitHub source file

161 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.Command line 12
2. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.ports line 14
3. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.direction line 17
4. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.commands line 20
5. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.commands_length line 22
6. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.LocalLabel line 26
7. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.SequenceLabel line 27
8. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.Label line 28
9. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.State line 29
10. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.sequenceEntry line 31
11. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.entry line 36
12. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.sequenceInstruction line 39
13. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.instruction line 48
14. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.result line 54
15. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes line 60
16. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.finalTapes line 66
17. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.sequenceSteps line 71
18. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.costSum line 77
19. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.sequenceSteps_eq line 83
20. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.steps line 96
21. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.budget line 99
22. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.costSum_le line 102
23. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.steps_le line 115
24. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.sequenceTrace line 119
25. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.vertexTrace line 149
26. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes_ready line 167
27. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.finalTapes_ready line 181
28. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes_other line 190
29. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.finalTapes_other line 204
30. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.rowBits line 211
31. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.blockIndex_eq_encodeDart line 215
32. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.rowBits_eq line 226
33. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.encodeWords_flatMap line 233
34. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.rows_eq_vertexRowBits line 239
35. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.sequenceTapes_output line 262
36. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.finalTapes_output line 282
37. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineVertex.vertexInTime line 293
38. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.Placement line 319
39. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.State line 320
40. structure OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.Ready line 322
41. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.counter line 330
42. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.counter_other line 334
43. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.ready_vertex line 342
44. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.ready_of_vertex line 361
45. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.vertexStart line 367
46. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.vertexEntry line 370
47. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.bridge line 388
48. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes line 392
49. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.steps line 400
50. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.steps_le line 406
51. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes_ready line 418
52. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.prefixRows line 443
53. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.prefixRows_ofFn line 448
54. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.prefixRows_all line 465
55. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes_output line 472
56. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.finalTapes_other line 498
57. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.loopTrace line 510
58. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineOuterLoop.loopInTime line 576
59. def OAI.BinPackingGames.Foundations.Complexity.PoweringPolynomialBudget.preBudget line 605
60. def OAI.BinPackingGames.Foundations.Complexity.PoweringPolynomialBudget.finishBudget line 609
61. def OAI.BinPackingGames.Foundations.Complexity.PoweringPolynomialBudget.totalBudget line 614
62. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringPolynomialBudget.preBudget_mono_vertices line 619
63. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringPolynomialBudget.finishBudget_mono line 626
64. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringPolynomialBudget.totalBudget_mono_vertices line 641
65. def OAI.BinPackingGames.Foundations.Complexity.PoweringPolynomialBudget.rowTime line 650
66. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringPolynomialBudget.rowTime_eval line 657
67. def OAI.BinPackingGames.Foundations.Complexity.PoweringPolynomialBudget.vertexTime line 663
68. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringPolynomialBudget.vertexTime_eval line 666
69. def OAI.BinPackingGames.Foundations.Complexity.PoweringPolynomialBudget.preTime line 671
70. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringPolynomialBudget.preTime_eval line 675
71. def OAI.BinPackingGames.Foundations.Complexity.PoweringPolynomialBudget.time line 680
72. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringPolynomialBudget.time_eval line 688
73. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringPolynomialBudget.totalBudget_le_time line 694
74. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringPolynomialBudget.setup_loop_finish_le_time line 701
75. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringPolynomialBudget.execution_budget_le_time line 714
76. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringPolynomialBudget.graph_totalBudget_le_time line 727
77. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.Tape line 740
78. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.State line 743
79. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.placement line 746
80. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.inputTape line 750
81. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.outputTape line 753
82. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.headerVertices line 756
83. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.headerDarts line 757
84. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.enumeration line 759
85. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.FinishLabel line 763
86. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.Label line 765
87. instance OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.labelFintype line 768
88. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.initLabels line 772
89. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.guardLabel line 773
90. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.bridgeLabel line 774
91. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.vertexLabels line 776
92. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.finishLabels line 779
93. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.finishEntry line 782
94. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.main line 784
95. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.program line 786
96. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.atInit line 802
97. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.atGuard line 807
98. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.atBridge line 812
99. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.atVertex line 816
100. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.atFinish line 820
101. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.machine line 826
102. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.machine_code line 837
103. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.machine_main line 840
104. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.machine_initialState line 842
105. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineGlobal.input_ne_output line 845
106. def OAI.BinPackingGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra line 857
107. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra_table line 862
108. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra_other line 866
109. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringInitializeFrame.initialExtra_scratch line 871
110. def OAI.BinPackingGames.Foundations.Complexity.PoweringInitializeFrame.preparedTapes line 876
111. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringInitializeFrame.prepared_commonRole line 882
112. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringInitializeFrame.prepared_ready line 890
113. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringInitializeFrame.prepared_start line 900
114. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringInitializeFrame.prepared_counter line 907
115. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringInitializeFrame.prepared_output line 914
116. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringInitializeFrame.prepared_vertices line 919
117. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringInitializeFrame.prepared_darts line 922
118. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringInitializeFrame.prepared_source line 926
119. def OAI.BinPackingGames.Foundations.Complexity.PoweringInitializeFrame.preparedCfg line 929
120. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringInitializeFrame.initialGlobalTapes_eq line 934
121. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringInitializeFrame.machine_initialStacks line 949
122. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringInitializeFrame.initList_eq line 955
123. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringInitializeFrame.tableBits_head line 964
124. def OAI.BinPackingGames.Foundations.Complexity.PoweringInitializeFrame.initializeInTime line 968
125. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_injective line 988
126. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_ne_output line 991
127. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalConfiguration.output_ne_placement line 997
128. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_placement line 1001
129. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalConfiguration.headerDarts_ne_placement line 1007
130. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_ne_headerVertices line 1013
131. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalConfiguration.placement_ne_headerDarts line 1017
132. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_headerDarts line 1021
133. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_output line 1024
134. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalConfiguration.headerDarts_ne_output line 1027
135. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalConfiguration.headerVertices_ne_scratch line 1030
136. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalConfiguration.headerDarts_ne_scratch line 1035
137. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalConfiguration.scratch_ne_output line 1040
138. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalConfiguration.boolList_mpr_eq line 1045
139. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalConfiguration.haltList_tapes line 1048
140. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringGlobalConfiguration.haltList_eq line 1053
141. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringRuntimeBudget.stackLength_le_of_execution line 1069
142. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringRuntimeBudget.stackLength_le_from_input line 1079
143. abbrev OAI.BinPackingGames.Foundations.Complexity.PoweringRuntimeBudget.tapeCount line 1087
144. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringRuntimeBudget.finish_steps_le_of_execution line 1090
145. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringRuntimeBudget.total_steps_le_of_execution line 1105
146. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish line 1126
147. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRuntime.finishConfiguration line 1130
148. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinishBudget line 1134
149. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_ready line 1138
150. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_output line 1146
151. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_vertices line 1157
152. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinish_darts line 1165
153. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRuntime.serialized_eq line 1174
154. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRuntime.beforeFinishExecution line 1181
155. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRuntime.finishSteps line 1202
156. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRuntime.finishExecution line 1206
157. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRuntime.execution line 1232
158. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRuntime.finishSteps_le line 1244
159. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRuntime.execution_budget_le line 1255
160. def OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRuntime.computableInPolyTime line 1264
161. theorem OAI.BinPackingGames.Foundations.Complexity.PoweringMachineRuntime.computableInPolyTime_finite_alphabet line 1290