OAI/Computability/BinPacking/PCP/RoundTableGap.lean

GitHub source file

216 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.bitValue line 12
2. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.boolEquiv line 14
3. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.boolEquiv_val line 16
4. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.productEquiv line 19
5. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.productEquiv_val line 23
6. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv line 29
7. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv_inl_val line 33
8. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.sumEquiv_inr_val line 37
9. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.tapeCount line 41
10. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.pairTapeCount line 42
11. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.fiveTapeCount line 43
12. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.localCount line 44
13. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.eventCount line 45
14. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.addressCount line 46
15. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.vertexCount line 47
16. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.dartCount line 48
17. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.cubeEquiv line 50
18. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.cubeRank line 53
19. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank line 54
20. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank_cubeRank line 57
21. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.cubeRank_cubeUnrank line 60
22. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.cubeUnrank_digit line 63
23. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.cubeEquiv_val line 71
24. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.pairIndex line 77
25. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.pairIndex_val line 79
26. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeEquiv line 84
27. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeRank line 87
28. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeUnrank line 90
29. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeUnrank_pairCubeRank line 93
30. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeRank_pairCubeUnrank line 96
31. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.pairCubeEquiv_val line 99
32. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.inputCoordinateEquiv line 104
33. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.fivePairTapesEquiv line 108
34. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.localEventEquiv line 117
35. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.eventEquiv line 122
36. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv line 126
37. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv line 131
38. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv line 136
39. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv line 141
40. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.labelEquiv_val line 143
41. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.inputCoordinateEquiv_val line 147
42. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.fivePairTapesEquiv_val line 152
43. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.localEventEquiv_val line 160
44. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.eventEquiv_val line 169
45. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv_inl_val line 176
46. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.addressEquiv_inr_val line 183
47. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_event_val line 190
48. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_vertexAddress_val line 194
49. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.vertexEquiv_edgeAddress_val line 201
50. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv_val line 209
51. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.dartEquiv_reverse_val line 217
52. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.ordered line 223
53. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_length line 226
54. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.mem_ordered line 229
55. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_nodup line 234
56. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_refl line 239
57. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_bool line 241
58. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_trans_finCongr line 243
59. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_product line 249
60. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_sum line 265
61. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.localEvents line 285
62. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.localEvents_length line 288
63. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_event line 291
64. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.ordered_dart line 298
65. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.card_cube line 308
66. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.card_pairCube line 311
67. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.card_localEvent line 315
68. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.card_event line 319
69. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.card_address line 323
70. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.card_vertex line 327
71. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.card_dart line 332
72. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Enumeration.localCount_formula line 337
73. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.sameAddress line 349
74. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.sameAddress_refl line 354
75. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.globalize_eq_iff line 358
76. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.eqProfile line 374
77. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.eqProfile_refl line 377
78. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot line 380
79. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot_profile line 383
80. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot_le line 389
81. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.RepeatedConsistent line 394
82. instance OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.repeatedConsistentDecidable line 398
83. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.incidenceAccept line 403
84. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.predicate line 409
85. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.relation line 415
86. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.relationAt_relation line 422
87. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.relation_reverse line 430
88. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.oldPredicate line 438
89. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.relationFromTable line 441
90. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.oldPredicate_relationAt line 445
91. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.relationFromTable_eq line 448
92. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.eqProfile_query_iff line 456
93. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.canonicalSlot_eq line 464
94. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.repeatedConsistent_iff line 473
95. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.verifier_accepts line 484
96. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.incidenceAccept_eq line 491
97. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Relations.relationAt_relation_graph line 503
98. abbrev OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.Terms line 521
99. structure OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.Field line 523
100. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.values line 527
101. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.eval line 529
102. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.fieldBound line 532
103. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.fieldBound_pos line 535
104. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.tapeCount_lt_bound line 539
105. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.pairTapeCount_lt_bound line 543
106. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.localCount_lt_bound line 547
107. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.local_add_pair_lt_bound line 551
108. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.twelve_local_lt_bound line 555
109. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.zeroOffset line 559
110. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.eventOffset line 561
111. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryOffset line 565
112. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.reverseOffset line 571
113. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.headerVertices line 581
114. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.headerDarts line 584
115. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.eventVertexField line 587
116. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.vertexQueryTerms line 591
117. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.edgeQueryTerms line 594
118. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms line 597
119. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryField line 601
120. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.reverseDartField line 604
121. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.headerVertices_eval line 608
122. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.headerDarts_eval line 614
123. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.eventVertexField_eval line 619
124. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryField_eval line 626
125. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.reverseDartField_eval line 642
126. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.queryEventTerms line 652
127. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms_query line 656
128. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.queryEventOffset line 664
129. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent line 668
130. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent_eq_rawQueryField line 672
131. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent_eval line 679
132. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.fieldForQueryEvent_eval_verifier line 688
133. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.dartTailTerms line 697
134. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.dartTailOffset line 701
135. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.fieldForDartTail line 705
136. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.fieldForDartTail_eval line 709
137. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.CoefficientsBounded line 721
138. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.headerVertices_coefficients line 724
139. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.headerDarts_coefficients line 731
140. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.eventVertexField_coefficients line 737
141. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms_coefficients line 744
142. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.queryEventTerms_coefficients line 762
143. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.reverseDartField_coefficients line 766
144. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.rawQueryTerms_length_le line 774
145. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.queryEventTerms_length_le line 780
146. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.dartTailTerms_coefficients line 784
147. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.dartTailTerms_length_le line 791
148. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Addresses.offset_lt line 798
149. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.rowFromDart line 807
150. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.rows line 825
151. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.rows_at line 831
152. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.rows_reverseIndex line 837
153. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.dartRow_ext line 845
154. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.relation_ext line 855
155. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.rowFromDart_eq_graphRow line 866
156. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.rows_eq_graphRows line 905
157. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.rows_valid line 916
158. def OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.build line 920
159. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.build_vertices line 926
160. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.build_darts line 929
161. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.table_rows_congr line 932
162. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.semantics_rows_congr line 938
163. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.build_eq_ofEnumeratedGraph line 945
164. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.semantics_build line 953
165. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.decode_build line 961
166. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.edgeSatisfied_build line 969
167. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.rejectionCount_build line 982
168. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.perfect_completeness line 993
169. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.gap_transfer line 1007
170. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.rowList_eq_ordered line 1031
171. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.tableWords_eq_ordered line 1040
172. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.rowList_length line 1049
173. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.tableWords_length line 1053
174. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTable.Table.tableBits_length_le line 1058
175. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTableBounds.gap_transfer_real line 1074
176. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTableBounds.build_vertices line 1102
177. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTableBounds.build_darts line 1112
178. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTableBounds.build_total line 1120
179. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTableBounds.build_total_le line 1127
180. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTableBounds.build_vertices_le line 1144
181. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTableBounds.build_darts_le line 1149
182. theorem OAI.BinPackingGames.Foundations.PCP.AlphabetTableBounds.sizeFactor_positive line 1154
183. abbrev OAI.BinPackingGames.Foundations.PCP.RoundTables.BaseTable line 1161
184. opaque OAI.BinPackingGames.Foundations.PCP.RoundTables.fixedWalkParameter line 1163
185. def OAI.BinPackingGames.Foundations.PCP.RoundTables.walkParameter line 1166
186. theorem OAI.BinPackingGames.Foundations.PCP.RoundTables.walkParameter_eq line 1168
187. def OAI.BinPackingGames.Foundations.PCP.RoundTables.alphabet line 1171
188. theorem OAI.BinPackingGames.Foundations.PCP.RoundTables.alphabet_positive line 1173
189. def OAI.BinPackingGames.Foundations.PCP.RoundTables.powered line 1177
190. def OAI.BinPackingGames.Foundations.PCP.RoundTables.build line 1180
191. def OAI.BinPackingGames.Foundations.PCP.RoundTables.sizeFactor line 1183
192. theorem OAI.BinPackingGames.Foundations.PCP.RoundTables.degree_positive line 1186
193. theorem OAI.BinPackingGames.Foundations.PCP.RoundTables.dartFactor_positive line 1190
194. theorem OAI.BinPackingGames.Foundations.PCP.RoundTables.sizeFactor_positive line 1194
195. theorem OAI.BinPackingGames.Foundations.PCP.RoundTables.powered_vertices line 1201
196. theorem OAI.BinPackingGames.Foundations.PCP.RoundTables.powered_darts line 1204
197. theorem OAI.BinPackingGames.Foundations.PCP.RoundTables.build_darts_positive line 1208
198. theorem OAI.BinPackingGames.Foundations.PCP.RoundTables.build_size_le line 1216
199. theorem OAI.BinPackingGames.Foundations.PCP.RoundTables.build_completeness line 1243
200. abbrev OAI.BinPackingGames.Foundations.PCP.RoundTables.Input line 1252
201. instance OAI.BinPackingGames.Foundations.PCP.RoundTables.(instance at line 1254) line 1254
202. def OAI.BinPackingGames.Foundations.PCP.RoundTables.step line 1256
203. def OAI.BinPackingGames.Foundations.PCP.RoundTables.initial line 1259
204. def OAI.BinPackingGames.Foundations.PCP.RoundTables.size line 1262
205. def OAI.BinPackingGames.Foundations.PCP.RoundTables.Satisfiable line 1264
206. def OAI.BinPackingGames.Foundations.PCP.RoundTables.gap line 1266
207. theorem OAI.BinPackingGames.Foundations.PCP.RoundTables.size_positive line 1268
208. theorem OAI.BinPackingGames.Foundations.PCP.RoundTables.gap_nonnegative line 1271
209. theorem OAI.BinPackingGames.Foundations.PCP.RoundTables.gap_eq_zero_iff line 1274
210. theorem OAI.BinPackingGames.Foundations.PCP.RoundTables.one_le_size_mul_gap line 1277
211. theorem OAI.BinPackingGames.Foundations.PCP.RoundTables.initial_satisfiable_iff line 1289
212. theorem OAI.BinPackingGames.Foundations.PCP.RoundTables.step_completeness line 1292
213. theorem OAI.BinPackingGames.Foundations.PCP.RoundTables.step_size line 1295
214. theorem OAI.BinPackingGames.Foundations.PCP.RoundTableGap.powered_count_gap line 1310
215. theorem OAI.BinPackingGames.Foundations.PCP.RoundTableGap.build_count_gap line 1341
216. theorem OAI.BinPackingGames.Foundations.PCP.RoundTableGap.step_gap line 1356