OAI/Computability/BinPacking/CookLevin/ConfigIndex.lean

GitHub source file

163 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.Cells line 17
2. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.encode line 19
3. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.read line 21
4. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.head line 24
5. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.isEmpty line 26
6. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.popShift line 28
7. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.pushShift line 31
8. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.encode_apply line 34
9. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.encode_nil line 37
10. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.read_at line 41
11. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.read_of_capacity_le line 45
12. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.read_encode line 49
13. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.head_encode line 56
14. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.head_encode_eq_none_iff line 60
15. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.isEmpty_encode line 64
16. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.isEmpty_encode_eq_true_iff line 69
17. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.encode_tail line 74
18. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.encode_cons line 80
19. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.tail_length_le line 85
20. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.cons_length_le line 90
21. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.encode_injective line 95
22. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.encode_eq_iff line 102
23. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.BoundedStack line 107
24. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.boundedEncoding line 109
25. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.boundedPop line 116
26. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.boundedPush line 119
27. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.boundedPop_correct line 123
28. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.boundedPush_correct line 127
29. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.encodeTapes line 134
30. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.encodeTapes_update line 137
31. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.encodeTapes_pop line 146
32. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.encodeTapes_push line 152
33. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StackEncoding.encodeTapes_injective line 159
34. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.Gate line 171
35. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Gate.Bounded line 178
36. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Gate.eval line 184
37. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Gate.bounded_mono line 191
38. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Gate.eval_congr line 199
39. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Ordered line 208
40. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Consistent line 211
41. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ordered_nil line 214
42. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ordered_cons line 218
43. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.consistent_nil line 238
44. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.consistent_cons line 243
45. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.consistent_append line 263
46. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.run line 272
47. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.run_eq_of_lt line 276
48. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.run_append line 284
49. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.run_singleton line 292
50. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.run_singleton_here line 295
51. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.run_singleton_other line 298
52. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Ordered.append line 302
53. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.run_consistent line 313
54. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.run_unique line 329
55. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit line 353
56. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.wires line 359
57. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.inputEnv line 361
58. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.evalWires line 364
59. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.eval line 367
60. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.evalWires_input line 370
61. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.evalWires_consistent line 375
62. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Consistent.congr line 379
63. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.unitClause line 391
64. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.gateClauses line 394
65. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.gateClauses_length line 414
66. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.gateClauses_correct line 418
67. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.gateAt line 445
68. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.gateOutput line 447
69. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.gateBounded line 450
70. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.gateBlock line 455
71. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.toFormula line 458
72. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.toFormula_variables line 462
73. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.toFormula_clause_count line 465
74. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.toFormula_satisfied_iff line 478
75. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.restrictAssignment line 511
76. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.toFormula_satisfiable_iff_eval line 515
77. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.Circuit.toFormula_extending_iff_eval line 540
78. inductive OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr line 574
79. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.eval line 585
80. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.eval_congr line 592
81. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.rename line 597
82. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.eval_rename line 604
83. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.size line 608
84. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.size_pos line 613
85. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.size_rename line 616
86. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.root line 620
87. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.root_lt line 622
88. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.root_not line 627
89. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.root_and line 632
90. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.root_or line 637
91. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.gates line 642
92. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.gates_length line 651
93. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.ordered_singleton line 655
94. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.gates_ordered line 659
95. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.consistent_singleton line 687
96. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.eval_of_consistent line 691
97. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.circuit line 727
98. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.circuit_eval line 733
99. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.mux line 743
100. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.eval_mux line 746
101. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.disjoin line 750
102. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.eval_disjoin_true line 754
103. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.Expr.size_disjoin_le line 760
104. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.bool_ext line 772
105. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.table line 775
106. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.eval_table line 779
107. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.table₂ line 795
108. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.eval_table₂ line 799
109. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.size_table_le line 809
110. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.size_table₂_le line 820
111. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.DataBits line 838
112. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.ResultBits line 842
113. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.DataBits.Realizes line 846
114. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.ResultBits.Realizes line 851
115. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.readBits line 856
116. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.eval_readBits line 860
117. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.pushBits line 872
118. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.peekBits line 879
119. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.popBits line 884
120. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.loadBits line 889
121. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.muxResult line 894
122. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.realizes_pushBits line 901
123. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.realizes_peekBits line 920
124. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.realizes_popBits line 931
125. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.realizes_loadBits line 946
126. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.realizes_muxResult line 952
127. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.compileAux line 972
128. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.compileAux_correct line 985
129. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.InputBit line 1024
130. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.ConfigBit line 1027
131. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.inputBits line 1030
132. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.inputEncoding line 1034
133. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.configEncoding line 1038
134. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.resultExpr line 1042
135. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.inputBits_realizes line 1049
136. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.resultExpr_eval line 1054
137. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.transitionExpr line 1063
138. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.transitionExpr_eval line 1067
139. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.outputCircuit line 1075
140. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.outputCircuit_eval line 1079
141. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.DataBits.Bounded line 1098
142. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.ResultBits.Bounded line 1101
143. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.size_readBits_le line 1104
144. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.unaryCost line 1113
145. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.headCost line 1116
146. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.statementCost line 1119
147. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.pushBits_bounded line 1130
148. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.peekBits_bounded line 1145
149. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.popBits_bounded line 1153
150. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.loadBits_bounded line 1167
151. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.muxResult_bounded line 1175
152. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.compileAux_bounded line 1186
153. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.transitionExpr_size_le line 1210
154. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.StatementCircuit.outputCircuit_gates_le line 1220
155. abbrev OAI.BinPackingGames.Foundations.Complexity.CookLevin.ConfigIndex.SymbolBit line 1234
156. structure OAI.BinPackingGames.Foundations.Complexity.CookLevin.ConfigIndex.Indexing line 1236
157. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ConfigIndex.Indexing.width line 1246
158. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ConfigIndex.cellReorder line 1249
159. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ConfigIndex.Indexing.configIndexEquiv line 1255
160. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ConfigIndex.Indexing.configIndex_label line 1266
161. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ConfigIndex.Indexing.configIndex_state line 1271
162. theorem OAI.BinPackingGames.Foundations.Complexity.CookLevin.ConfigIndex.Indexing.configIndex_cell line 1277
163. def OAI.BinPackingGames.Foundations.Complexity.CookLevin.ConfigIndex.ofMachine line 1287