OAI/Combinatorics/Ramsey/CycleClique/Construction/CoverageK12.lean

GitHub source file

527 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover10 line 8
2. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover9 line 12
3. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover11 line 18
4. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover12 line 22
5. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover13 line 26
6. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover14 line 30
7. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover15 line 34
8. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover16 line 38
9. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover8 line 42
10. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover17 line 70
11. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover18 line 76
12. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover19 line 80
13. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover20 line 84
14. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover21 line 88
15. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover22 line 92
16. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover23 line 96
17. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover24 line 102
18. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover25 line 106
19. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover26 line 110
20. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover27 line 114
21. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover28 line 120
22. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover29 line 124
23. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover30 line 130
24. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover31 line 136
25. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover7 line 142
26. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover33 line 239
27. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover34 line 243
28. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover35 line 247
29. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover36 line 251
30. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover37 line 255
31. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover32 line 259
32. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover38 line 284
33. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover39 line 290
34. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover40 line 294
35. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover41 line 298
36. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover42 line 302
37. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover43 line 306
38. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover44 line 312
39. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover45 line 316
40. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover46 line 320
41. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover47 line 324
42. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover48 line 330
43. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover49 line 334
44. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover50 line 338
45. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover51 line 344
46. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover52 line 348
47. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover54 line 354
48. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover55 line 358
49. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover56 line 362
50. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover53 line 366
51. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover57 line 388
52. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover58 line 392
53. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover59 line 396
54. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover60 line 402
55. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover61 line 406
56. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover62 line 412
57. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover64 line 418
58. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover63 line 422
59. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover65 line 441
60. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover66 line 447
61. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover67 line 463
62. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover68 line 476
63. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_seq6 line 486
64. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover5 line 705
65. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover71 line 710
66. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover72 line 716
67. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover73 line 720
68. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover74 line 724
69. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover75 line 728
70. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover76 line 732
71. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover77 line 738
72. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover78 line 742
73. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover79 line 746
74. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover80 line 752
75. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover81 line 758
76. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover70 line 764
77. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover83 line 839
78. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover84 line 843
79. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover85 line 847
80. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover82 line 851
81. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover86 line 873
82. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover87 line 879
83. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover88 line 883
84. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover89 line 887
85. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover90 line 891
86. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover91 line 897
87. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover92 line 901
88. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover93 line 905
89. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover94 line 911
90. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover95 line 915
91. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover97 line 921
92. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover98 line 925
93. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover96 line 929
94. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover99 line 948
95. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover100 line 954
96. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover101 line 958
97. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover102 line 964
98. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover103 line 968
99. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover105 line 974
100. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover104 line 978
101. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover106 line 994
102. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover107 line 1000
103. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover108 line 1006
104. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover109 line 1019
105. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover110 line 1025
106. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_seq69 line 1035
107. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover112 line 1182
108. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover113 line 1188
109. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover114 line 1192
110. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover115 line 1198
111. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover111 line 1204
112. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover116 line 1260
113. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover117 line 1264
114. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover118 line 1270
115. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover119 line 1276
116. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover120 line 1292
117. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover121 line 1298
118. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover122 line 1311
119. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover124 line 1321
120. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover123 line 1327
121. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover125 line 1367
122. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover126 line 1377
123. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover127 line 1404
124. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover128 line 1421
125. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_seq4 line 1431
126. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover3 line 1635
127. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover133 line 1640
128. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover134 line 1644
129. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover135 line 1648
130. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover136 line 1652
131. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover132 line 1656
132. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover137 line 1678
133. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover138 line 1684
134. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover139 line 1688
135. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover140 line 1692
136. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover141 line 1696
137. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover142 line 1702
138. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover143 line 1706
139. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover144 line 1710
140. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover145 line 1716
141. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover146 line 1720
142. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover148 line 1726
143. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover149 line 1730
144. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover147 line 1734
145. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover150 line 1753
146. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover151 line 1757
147. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover152 line 1763
148. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover153 line 1769
149. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover154 line 1785
150. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover155 line 1798
151. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_seq131 line 1808
152. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover130 line 1955
153. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover157 line 1960
154. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover158 line 1964
155. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover159 line 1968
156. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover160 line 1972
157. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover161 line 1978
158. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover162 line 1982
159. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover163 line 1988
160. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover156 line 1994
161. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover165 line 2050
162. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover166 line 2054
163. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover164 line 2058
164. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover167 line 2077
165. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover168 line 2083
166. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover169 line 2087
167. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover170 line 2091
168. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover171 line 2097
169. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover172 line 2101
170. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover174 line 2107
171. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover173 line 2111
172. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover175 line 2127
173. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover176 line 2133
174. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover177 line 2137
175. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover178 line 2143
176. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover179 line 2156
177. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover180 line 2162
178. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover182 line 2172
179. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover183 line 2176
180. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover184 line 2182
181. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover181 line 2188
182. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover186 line 2228
183. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover185 line 2232
184. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover187 line 2248
185. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover188 line 2254
186. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover189 line 2267
187. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover190 line 2273
188. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover192 line 2283
189. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover191 line 2289
190. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover193 line 2316
191. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover194 line 2329
192. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover195 line 2339
193. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover196 line 2356
194. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover197 line 2366
195. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_seq129 line 2376
196. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover200 line 2578
197. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover199 line 2582
198. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover201 line 2598
199. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover202 line 2604
200. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover203 line 2617
201. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover198 line 2627
202. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover204 line 2719
203. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover205 line 2725
204. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover206 line 2738
205. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover207 line 2748
206. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover208 line 2775
207. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover209 line 2785
208. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover210 line 2802
209. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover212 line 2812
210. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover211 line 2822
211. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover213 line 2877
212. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover214 line 2887
213. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover215 line 2918
214. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover216 line 2935
215. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_seq2 line 2945
216. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t6_cover1 line 3172
217. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k12_t6 line 3177
218. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover12 line 3181
219. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover11 line 3185
220. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover13 line 3191
221. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover14 line 3195
222. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover15 line 3199
223. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover16 line 3203
224. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover17 line 3207
225. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover10 line 3211
226. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover18 line 3236
227. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover19 line 3242
228. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover20 line 3246
229. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover21 line 3250
230. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover22 line 3254
231. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover23 line 3258
232. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover24 line 3264
233. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover25 line 3268
234. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover26 line 3272
235. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover27 line 3278
236. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover28 line 3284
237. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover9 line 3290
238. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover30 line 3365
239. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover31 line 3369
240. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover32 line 3373
241. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover33 line 3377
242. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover29 line 3381
243. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover34 line 3403
244. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover35 line 3409
245. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover36 line 3413
246. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover37 line 3417
247. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover38 line 3421
248. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover39 line 3427
249. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover40 line 3431
250. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover41 line 3435
251. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover42 line 3441
252. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover43 line 3445
253. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover45 line 3451
254. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover46 line 3455
255. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover44 line 3459
256. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover47 line 3478
257. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover48 line 3482
258. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover49 line 3488
259. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover50 line 3494
260. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover51 line 3510
261. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover52 line 3523
262. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_seq8 line 3533
263. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover7 line 3680
264. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover54 line 3685
265. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover55 line 3691
266. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover56 line 3695
267. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover57 line 3699
268. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover58 line 3703
269. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover59 line 3709
270. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover60 line 3713
271. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover61 line 3719
272. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover53 line 3725
273. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover63 line 3781
274. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover64 line 3785
275. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover62 line 3789
276. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover65 line 3808
277. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover66 line 3814
278. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover67 line 3818
279. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover68 line 3822
280. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover69 line 3828
281. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover70 line 3832
282. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover72 line 3838
283. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover71 line 3842
284. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover73 line 3858
285. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover74 line 3864
286. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover75 line 3870
287. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover76 line 3883
288. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover77 line 3889
289. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover79 line 3899
290. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover80 line 3905
291. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover78 line 3911
292. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover81 line 3951
293. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover82 line 3957
294. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover83 line 3970
295. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover84 line 3980
296. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover85 line 4007
297. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover86 line 4024
298. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_seq6 line 4034
299. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover5 line 4236
300. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover89 line 4241
301. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover90 line 4245
302. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover91 line 4249
303. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover88 line 4253
304. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover92 line 4272
305. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover93 line 4278
306. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover94 line 4282
307. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover95 line 4286
308. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover96 line 4292
309. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover97 line 4296
310. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover99 line 4302
311. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover98 line 4306
312. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover100 line 4322
313. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover101 line 4328
314. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover102 line 4341
315. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover87 line 4351
316. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover104 line 4443
317. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover105 line 4447
318. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover106 line 4451
319. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover107 line 4457
320. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover103 line 4463
321. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover109 line 4503
322. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover108 line 4507
323. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover110 line 4523
324. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover111 line 4529
325. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover112 line 4533
326. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover113 line 4539
327. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover114 line 4552
328. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover115 line 4558
329. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover117 line 4568
330. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover116 line 4574
331. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover118 line 4601
332. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover119 line 4614
333. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover120 line 4624
334. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover121 line 4641
335. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover122 line 4651
336. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover124 line 4661
337. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover125 line 4674
338. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover123 line 4684
339. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover126 line 4739
340. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover127 line 4749
341. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover128 line 4766
342. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover129 line 4776
343. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover130 line 4807
344. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover131 line 4824
345. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_seq4 line 4834
346. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover3 line 5059
347. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover134 line 5064
348. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover135 line 5070
349. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover136 line 5074
350. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover137 line 5078
351. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover138 line 5084
352. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover133 line 5090
353. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover140 line 5130
354. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover139 line 5134
355. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover141 line 5150
356. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover142 line 5156
357. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover143 line 5160
358. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover144 line 5166
359. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover145 line 5179
360. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover146 line 5185
361. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover148 line 5195
362. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover147 line 5201
363. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover149 line 5228
364. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover150 line 5238
365. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover151 line 5255
366. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover132 line 5265
367. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover153 line 5376
368. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover154 line 5382
369. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover155 line 5386
370. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover156 line 5392
371. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover157 line 5405
372. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover152 line 5415
373. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover159 line 5470
374. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover158 line 5476
375. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover160 line 5503
376. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover161 line 5516
377. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover162 line 5522
378. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover163 line 5532
379. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover164 line 5549
380. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover165 line 5559
381. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover167 line 5569
382. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover166 line 5579
383. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover168 line 5610
384. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover169 line 5627
385. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover170 line 5637
386. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover171 line 5654
387. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover172 line 5664
388. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover174 line 5674
389. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover175 line 5691
390. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover173 line 5701
391. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover176 line 5760
392. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover177 line 5770
393. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover178 line 5787
394. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover179 line 5797
395. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover180 line 5828
396. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover181 line 5845
397. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_seq2 line 5855
398. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t7_cover1 line 6084
399. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k12_t7 line 6089
400. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover9 line 6093
401. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover8 line 6097
402. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover10 line 6103
403. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover11 line 6107
404. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover12 line 6111
405. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover13 line 6115
406. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover7 line 6119
407. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover14 line 6141
408. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover15 line 6147
409. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover16 line 6151
410. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover17 line 6155
411. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover18 line 6159
412. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover19 line 6165
413. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover20 line 6169
414. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover21 line 6175
415. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover6 line 6181
416. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover23 line 6237
417. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover24 line 6241
418. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover25 line 6245
419. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover22 line 6249
420. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover26 line 6268
421. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover27 line 6274
422. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover28 line 6278
423. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover29 line 6282
424. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover30 line 6288
425. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover31 line 6292
426. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover33 line 6298
427. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover32 line 6302
428. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover34 line 6318
429. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover35 line 6324
430. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover36 line 6337
431. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover5 line 6347
432. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover38 line 6439
433. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover39 line 6445
434. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover40 line 6449
435. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover41 line 6453
436. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover42 line 6459
437. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover37 line 6465
438. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover44 line 6505
439. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover43 line 6509
440. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover45 line 6525
441. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover46 line 6531
442. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover47 line 6535
443. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover48 line 6541
444. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover49 line 6554
445. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover50 line 6560
446. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover52 line 6570
447. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover51 line 6576
448. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover53 line 6603
449. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover54 line 6613
450. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover55 line 6630
451. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover4 line 6640
452. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover58 line 6751
453. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover59 line 6755
454. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover57 line 6759
455. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover60 line 6775
456. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover61 line 6781
457. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover62 line 6785
458. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover63 line 6791
459. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover64 line 6804
460. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover56 line 6814
461. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover66 line 6869
462. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover67 line 6873
463. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover65 line 6879
464. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover68 line 6906
465. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover69 line 6919
466. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover70 line 6925
467. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover71 line 6935
468. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover72 line 6952
469. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover73 line 6962
470. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover75 line 6972
471. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover74 line 6982
472. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover76 line 7013
473. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover77 line 7023
474. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover78 line 7040
475. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover3 line 7050
476. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover81 line 7165
477. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover82 line 7171
478. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover83 line 7175
479. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover80 line 7181
480. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover84 line 7208
481. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover85 line 7221
482. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover86 line 7227
483. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover87 line 7237
484. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover88 line 7254
485. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover79 line 7264
486. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover90 line 7323
487. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover91 line 7329
488. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover89 line 7339
489. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover92 line 7370
490. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover93 line 7387
491. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover94 line 7397
492. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover95 line 7407
493. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover96 line 7424
494. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover97 line 7434
495. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover99 line 7444
496. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover98 line 7454
497. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover100 line 7485
498. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover101 line 7495
499. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover102 line 7512
500. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover2 line 7522
501. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover106 line 7637
502. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover105 line 7641
503. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover107 line 7654
504. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover108 line 7660
505. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover104 line 7670
506. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover109 line 7701
507. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover110 line 7718
508. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover111 line 7728
509. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover112 line 7738
510. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover113 line 7755
511. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover103 line 7765
512. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover115 line 7824
513. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover116 line 7834
514. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover114 line 7844
515. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover117 line 7875
516. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover118 line 7892
517. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover119 line 7902
518. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover120 line 7912
519. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover121 line 7929
520. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover122 line 7939
521. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover124 line 7949
522. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover123 line 7959
523. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover125 line 7990
524. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover126 line 8000
525. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover127 line 8017
526. theorem OAI.CycleClique.Construction.CertifiedCoverage.k12t8_cover1 line 8027
527. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k12_t8 line 8142