OAI/Computability/BinPacking/CookLevin/OutputOrder.lean

GitHub source file

166 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Position line 11
2. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Position.eval line 18
3. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Batch.cost line 34
4. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Batch.gates line 36
5. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Batch.roots line 40
6. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Batch.cost_nil line 44
7. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Batch.cost_cons line 46
8. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Batch.gates_length line 49
9. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Batch.roots_length line 55
10. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Batch.gates_ordered line 59
11. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Batch.roots_bounds line 68
12. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Batch.eval_roots line 85
13. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Batch.rootAt line 96
14. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Batch.rootAt_lt line 99
15. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Batch.eval_rootAt line 106
16. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Batch.cost_le line 115
17. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Batch.cost_ofFn line 125
18. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Batch.cost_ofFn_le line 129
19. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Fragment line 139
20. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Fragment.empty line 147
21. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Fragment.evalWires line 149
22. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Fragment.evalWires_input line 152
23. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Fragment.evalWires_consistent line 157
24. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Fragment.append line 161
25. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Fragment.evalWires_append line 165
26. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Fragment.evalWires_append_old line 171
27. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Fragment.toCircuit line 178
28. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Fragment.toCircuit_eval line 181
29. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Frame line 187
30. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Frame.eval line 195
31. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Frame.initial line 198
32. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Frame.initial_eval line 202
33. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Frame.step line 206
34. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Frame.step_gate_count line 217
35. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Frame.step_gate_count_sum line 223
36. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Frame.step_gate_count_le line 228
37. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Frame.step_eval line 234
38. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Frame.step_eval_fun line 255
39. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Frame.network line 261
40. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Frame.«repeat» line 264
41. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Frame.repeat_eval line 269
42. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Frame.repeat_gate_count line 278
43. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Frame.repeat_gate_count_sum line 288
44. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Frame.repeat_gate_count_le line 293
45. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Frame.toCircuit line 299
46. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Frame.toCircuit_eval line 302
47. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.CircuitBatch.Frame.repeat_toCircuit_eval line 305
48. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.usesCurrent line 319
49. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.initialValue line 325
50. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.transform line 328
51. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.transform_initialValue line 334
52. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.Alphabet line 350
53. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.State line 351
54. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.decrement line 353
55. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.stepAux_decrement line 361
56. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.suffixStatement line 371
57. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.stepAux_suffixStatement line 380
58. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.Label line 398
59. instance OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.(instance at line 405) line 405
60. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.statement line 409
61. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.seedSteps line 421
62. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.steps line 424
63. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.seedTrace line 426
64. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.finishTrace line 453
65. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.positionTrace line 468
66. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.timePolynomial line 486
67. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.steps_le_time line 488
68. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.positionInPolynomialTime line 494
69. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.machine line 514
70. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PositionMachine.machineInPolynomialTime line 525
71. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.exprTokens line 543
72. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.forestTokens line 550
73. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.exprTokens_length line 553
74. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.exprTokens_rename line 557
75. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.forestTokens_nil line 561
76. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.forestTokens_cons line 564
77. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.forestTokens_length line 567
78. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.compileTokens_append line 574
79. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.compile_exprTokens line 601
80. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.compile_forestTokens line 637
81. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.exprTokens_lowered_ordered line 651
82. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.forestTokens_lowered_ordered line 655
83. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.forestTokens_preserves_root_suffix line 659
84. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.expr_inputBits line 671
85. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.forest_inputBits line 676
86. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.forest_gateRecords_alignment line 681
87. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.tokenWords_length_le line 689
88. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.exprTokens_member line 705
89. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.expr_tokenWords_bounded line 734
90. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.forest_tokenWords_bounded line 747
91. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.forest_tokenBits_length_le line 755
92. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.PostfixAlignment.forest_inputBits_length_le line 765
93. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Term line 782
94. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Term.instantiate line 794
95. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Term.nodeCount line 807
96. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Term.instantiate_size_le line 814
97. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Term.disjoin line 830
98. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Term.mux line 834
99. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.instantiate_disjoin line 838
100. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.instantiate_mux line 844
101. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.finiteTable line 848
102. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.finiteTable₂ line 852
103. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.instantiate_table line 857
104. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.instantiate_table₂ line 864
105. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Data line 871
106. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Result line 875
107. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Data.Matches line 878
108. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Result.Matches line 884
109. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.initial line 889
110. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.initial_matches line 894
111. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.read line 900
112. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.instantiate_read line 904
113. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.push line 915
114. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.peek line 921
115. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.pop line 926
116. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.load line 931
117. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.mux line 936
118. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.push_matches line 943
119. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.peek_matches line 961
120. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.pop_matches line 975
121. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.load_matches line 987
122. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.mux_matches line 996
123. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.compile line 1010
124. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.compile_matches line 1023
125. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.OutputKind line 1047
126. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.bitKind line 1050
127. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.bitCursor line 1055
128. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.select line 1059
129. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.transition line 1064
130. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.transition_instantiate line 1067
131. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Global line 1077
132. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Global.instantiate line 1084
133. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Global.nodeCount line 1092
134. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Global.instantiate_size_le line 1099
135. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Global.disjoin line 1110
136. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.instantiate_global_disjoin line 1117
137. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.self line 1123
138. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.self_instantiate line 1130
139. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.sticky line 1140
140. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.sticky_instantiate line 1146
141. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.kindIndexEquiv line 1155
142. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.templateBank line 1164
143. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.templateBank_select line 1170
144. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.rootLookup line 1175
145. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.configWire line 1177
146. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.labelAddress_lt_width line 1183
147. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.stateAddress_lt_width line 1191
148. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.cellAddress_lt_width line 1199
149. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.rootLookup_present line 1208
150. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.configWire_present line 1217
151. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Term.tokens line 1222
152. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Term.tokens_eq line 1241
153. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Global.tokens line 1260
154. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Global.tokens_eq line 1270
155. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.sticky_tokens_eq line 1283
156. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.Global.tokens_length_le line 1292
157. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.sticky_tokens_length_le line 1298
158. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.outputOrder line 1305
159. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.forestTokens line 1309
160. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.forestTokens_eq line 1314
161. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.outputOrder_length line 1326
162. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.TransitionTemplate.forestTokens_length_le line 1330
163. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OutputOrder.unindex_label line 1354
164. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OutputOrder.unindex_state line 1364
165. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OutputOrder.unindex_cell line 1374
166. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.OutputOrder.outputOrder_eq_blocks line 1388