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

GitHub source file

905 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover11 line 8
2. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover10 line 12
3. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover12 line 18
4. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover13 line 22
5. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover14 line 26
6. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover15 line 30
7. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover16 line 34
8. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover17 line 38
9. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover18 line 42
10. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover9 line 46
11. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover19 line 77
12. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover20 line 83
13. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover21 line 87
14. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover22 line 91
15. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover23 line 95
16. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover24 line 99
17. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover25 line 103
18. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover26 line 107
19. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover27 line 113
20. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover28 line 117
21. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover29 line 121
22. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover30 line 125
23. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover31 line 129
24. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover32 line 135
25. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover33 line 139
26. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover34 line 143
27. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover35 line 149
28. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover36 line 155
29. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover37 line 161
30. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_seq8 line 167
31. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover7 line 291
32. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover39 line 296
33. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover40 line 300
34. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover41 line 304
35. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover42 line 308
36. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover43 line 312
37. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover44 line 316
38. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover38 line 320
39. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover45 line 348
40. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover46 line 354
41. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover47 line 358
42. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover48 line 362
43. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover49 line 366
44. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover50 line 370
45. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover51 line 374
46. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover52 line 380
47. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover53 line 384
48. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover54 line 388
49. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover55 line 392
50. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover56 line 396
51. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover57 line 402
52. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover58 line 406
53. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover59 line 410
54. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover60 line 414
55. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover61 line 420
56. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover62 line 424
57. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover63 line 428
58. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover64 line 434
59. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover65 line 438
60. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover67 line 444
61. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover68 line 448
62. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover69 line 452
63. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover70 line 456
64. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover66 line 460
65. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover71 line 485
66. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover72 line 489
67. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover73 line 493
68. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover74 line 497
69. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover75 line 503
70. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover76 line 507
71. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover77 line 511
72. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover78 line 517
73. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover79 line 521
74. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover80 line 527
75. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover82 line 533
76. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover83 line 537
77. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover81 line 541
78. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover84 line 563
79. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover85 line 567
80. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover86 line 573
81. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover87 line 579
82. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover88 line 598
83. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover89 line 614
84. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover90 line 627
85. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_seq6 line 637
86. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover5 line 950
87. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover93 line 955
88. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover94 line 961
89. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover95 line 965
90. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover96 line 969
91. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover97 line 973
92. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover98 line 977
93. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover99 line 981
94. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover100 line 987
95. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover101 line 991
96. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover102 line 995
97. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover103 line 999
98. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover104 line 1005
99. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover105 line 1009
100. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover106 line 1015
101. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover107 line 1021
102. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover92 line 1027
103. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover109 line 1124
104. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover110 line 1128
105. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover111 line 1132
106. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover112 line 1136
107. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover108 line 1140
108. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover113 line 1165
109. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover114 line 1171
110. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover115 line 1175
111. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover116 line 1179
112. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover117 line 1183
113. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover118 line 1187
114. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover119 line 1193
115. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover120 line 1197
116. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover121 line 1201
117. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover122 line 1205
118. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover123 line 1211
119. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover124 line 1215
120. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover125 line 1219
121. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover126 line 1225
122. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover127 line 1229
123. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover129 line 1235
124. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover130 line 1239
125. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover131 line 1243
126. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover128 line 1247
127. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover132 line 1269
128. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover133 line 1275
129. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover134 line 1279
130. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover135 line 1283
131. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover136 line 1289
132. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover137 line 1293
133. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover138 line 1297
134. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover139 line 1303
135. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover140 line 1307
136. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover142 line 1313
137. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover143 line 1317
138. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover141 line 1321
139. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover144 line 1340
140. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover145 line 1346
141. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover146 line 1350
142. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover147 line 1356
143. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover149 line 1362
144. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover148 line 1366
145. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover150 line 1382
146. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover151 line 1388
147. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover152 line 1394
148. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover153 line 1407
149. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover154 line 1413
150. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_seq91 line 1423
151. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover157 line 1642
152. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover158 line 1648
153. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover159 line 1652
154. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover160 line 1656
155. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover161 line 1662
156. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover162 line 1668
157. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover156 line 1674
158. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover163 line 1749
159. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover164 line 1753
160. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover165 line 1757
161. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover166 line 1763
162. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover167 line 1767
163. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover168 line 1773
164. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover170 line 1779
165. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover169 line 1783
166. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover171 line 1802
167. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover172 line 1808
168. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover173 line 1814
169. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover174 line 1830
170. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover175 line 1836
171. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover176 line 1849
172. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_seq155 line 1859
173. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover178 line 2006
174. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover179 line 2012
175. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover177 line 2018
176. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover180 line 2074
177. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover181 line 2080
178. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover182 line 2093
179. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover183 line 2103
180. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover184 line 2143
181. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover185 line 2170
182. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover186 line 2187
183. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_seq4 line 2197
184. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover3 line 2403
185. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover191 line 2408
186. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover192 line 2412
187. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover193 line 2416
188. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover194 line 2420
189. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover195 line 2424
190. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover190 line 2428
191. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover196 line 2453
192. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover197 line 2459
193. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover198 line 2463
194. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover199 line 2467
195. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover200 line 2471
196. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover201 line 2475
197. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover202 line 2481
198. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover203 line 2485
199. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover204 line 2489
200. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover205 line 2493
201. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover206 line 2499
202. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover207 line 2503
203. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover208 line 2507
204. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover209 line 2513
205. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover210 line 2517
206. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover212 line 2523
207. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover213 line 2527
208. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover214 line 2531
209. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover211 line 2535
210. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover215 line 2557
211. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover216 line 2561
212. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover217 line 2565
213. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover218 line 2571
214. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover219 line 2575
215. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover220 line 2581
216. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover222 line 2587
217. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover221 line 2591
218. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover223 line 2610
219. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover224 line 2616
220. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover225 line 2632
221. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover226 line 2645
222. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_seq189 line 2655
223. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover188 line 2874
224. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover229 line 2879
225. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover230 line 2883
226. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover231 line 2887
227. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover232 line 2891
228. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover233 line 2895
229. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover234 line 2901
230. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover235 line 2905
231. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover236 line 2909
232. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover237 line 2915
233. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover238 line 2921
234. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover228 line 2927
235. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover240 line 3002
236. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover241 line 3006
237. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover242 line 3010
238. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover239 line 3014
239. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover243 line 3036
240. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover244 line 3042
241. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover245 line 3046
242. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover246 line 3050
243. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover247 line 3054
244. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover248 line 3060
245. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover249 line 3064
246. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover250 line 3068
247. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover251 line 3074
248. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover252 line 3078
249. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover254 line 3084
250. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover255 line 3088
251. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover253 line 3092
252. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover256 line 3111
253. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover257 line 3117
254. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover258 line 3121
255. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover259 line 3125
256. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover260 line 3131
257. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover261 line 3135
258. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover263 line 3141
259. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover262 line 3145
260. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover264 line 3161
261. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover265 line 3167
262. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover266 line 3171
263. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover267 line 3177
264. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover268 line 3190
265. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover269 line 3196
266. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_seq227 line 3206
267. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover271 line 3353
268. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover272 line 3357
269. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover273 line 3361
270. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover274 line 3367
271. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover275 line 3371
272. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover276 line 3377
273. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover270 line 3383
274. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover278 line 3439
275. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover279 line 3443
276. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover277 line 3447
277. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover280 line 3466
278. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover281 line 3470
279. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover282 line 3476
280. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover283 line 3480
281. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover285 line 3486
282. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover284 line 3490
283. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover286 line 3506
284. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover287 line 3512
285. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover288 line 3518
286. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover289 line 3531
287. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover290 line 3537
288. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover292 line 3547
289. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover293 line 3553
290. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover291 line 3559
291. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover295 line 3599
292. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover294 line 3603
293. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover296 line 3619
294. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover297 line 3625
295. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover298 line 3638
296. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover300 line 3648
297. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover299 line 3654
298. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover301 line 3681
299. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover302 line 3694
300. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover303 line 3704
301. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover304 line 3721
302. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover305 line 3731
303. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_seq187 line 3741
304. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover310 line 3945
305. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover311 line 3949
306. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover309 line 3953
307. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover312 line 3972
308. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover313 line 3976
309. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover314 line 3982
310. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover315 line 3988
311. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover316 line 4004
312. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover317 line 4017
313. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_seq308 line 4027
314. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover307 line 4174
315. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover318 line 4179
316. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover319 line 4183
317. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover320 line 4189
318. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover321 line 4195
319. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover322 line 4211
320. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover323 line 4217
321. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover324 line 4230
322. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover326 line 4240
323. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover325 line 4246
324. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover327 line 4286
325. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover328 line 4299
326. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover329 line 4309
327. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover330 line 4336
328. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover331 line 4346
329. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover332 line 4363
330. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_seq306 line 4373
331. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover334 line 4575
332. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover335 line 4588
333. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover333 line 4598
334. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover336 line 4690
335. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover337 line 4700
336. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover338 line 4717
337. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover339 line 4727
338. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover340 line 4782
339. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover341 line 4813
340. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover342 line 4830
341. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_seq2 line 4840
342. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t6_cover1 line 5069
343. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k13_t6 line 5074
344. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover12 line 5078
345. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover11 line 5082
346. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover13 line 5088
347. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover14 line 5092
348. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover15 line 5096
349. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover16 line 5100
350. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover17 line 5104
351. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover18 line 5108
352. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover10 line 5112
353. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover19 line 5140
354. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover20 line 5146
355. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover21 line 5150
356. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover22 line 5154
357. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover23 line 5158
358. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover24 line 5162
359. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover25 line 5166
360. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover26 line 5172
361. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover27 line 5176
362. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover28 line 5180
363. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover29 line 5184
364. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover30 line 5190
365. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover31 line 5194
366. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover32 line 5200
367. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover33 line 5206
368. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover9 line 5212
369. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover35 line 5309
370. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover36 line 5313
371. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover37 line 5317
372. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover38 line 5321
373. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover39 line 5325
374. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover34 line 5329
375. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover40 line 5354
376. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover41 line 5360
377. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover42 line 5364
378. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover43 line 5368
379. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover44 line 5372
380. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover45 line 5376
381. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover46 line 5382
382. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover47 line 5386
383. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover48 line 5390
384. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover49 line 5394
385. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover50 line 5400
386. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover51 line 5404
387. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover52 line 5408
388. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover53 line 5414
389. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover54 line 5418
390. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover56 line 5424
391. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover57 line 5428
392. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover58 line 5432
393. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover55 line 5436
394. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover59 line 5458
395. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover60 line 5462
396. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover61 line 5466
397. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover62 line 5472
398. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover63 line 5476
399. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover64 line 5482
400. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover66 line 5488
401. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover65 line 5492
402. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover67 line 5511
403. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover68 line 5517
404. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover69 line 5533
405. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover70 line 5546
406. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_seq8 line 5556
407. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover7 line 5775
408. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover73 line 5780
409. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover74 line 5786
410. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover75 line 5790
411. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover76 line 5794
412. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover77 line 5798
413. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover78 line 5802
414. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover79 line 5808
415. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover80 line 5812
416. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover81 line 5816
417. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover82 line 5822
418. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover83 line 5828
419. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover72 line 5834
420. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover85 line 5909
421. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover86 line 5913
422. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover87 line 5917
423. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover84 line 5921
424. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover88 line 5943
425. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover89 line 5949
426. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover90 line 5953
427. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover91 line 5957
428. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover92 line 5961
429. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover93 line 5967
430. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover94 line 5971
431. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover95 line 5975
432. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover96 line 5981
433. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover97 line 5985
434. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover99 line 5991
435. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover100 line 5995
436. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover98 line 5999
437. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover101 line 6018
438. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover102 line 6024
439. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover103 line 6028
440. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover104 line 6034
441. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover105 line 6038
442. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover107 line 6044
443. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover106 line 6048
444. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover108 line 6064
445. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover109 line 6070
446. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover110 line 6076
447. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover111 line 6089
448. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover112 line 6095
449. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_seq71 line 6105
450. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover114 line 6252
451. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover115 line 6258
452. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover116 line 6262
453. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover117 line 6268
454. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover113 line 6274
455. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover118 line 6330
456. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover119 line 6334
457. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover120 line 6340
458. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover121 line 6346
459. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover122 line 6362
460. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover123 line 6368
461. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover124 line 6381
462. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover126 line 6391
463. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover125 line 6397
464. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover127 line 6437
465. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover128 line 6447
466. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover129 line 6474
467. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover130 line 6491
468. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_seq6 line 6501
469. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover5 line 6705
470. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover135 line 6710
471. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover136 line 6714
472. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover137 line 6718
473. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover138 line 6722
474. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover134 line 6726
475. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover139 line 6748
476. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover140 line 6754
477. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover141 line 6758
478. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover142 line 6762
479. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover143 line 6766
480. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover144 line 6772
481. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover145 line 6776
482. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover146 line 6780
483. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover147 line 6786
484. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover148 line 6790
485. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover150 line 6796
486. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover151 line 6800
487. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover149 line 6804
488. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover152 line 6823
489. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover153 line 6827
490. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover154 line 6833
491. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover155 line 6839
492. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover156 line 6855
493. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover157 line 6868
494. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_seq133 line 6878
495. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover132 line 7025
496. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover159 line 7030
497. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover160 line 7034
498. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover161 line 7038
499. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover162 line 7042
500. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover163 line 7048
501. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover164 line 7052
502. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover165 line 7058
503. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover158 line 7064
504. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover167 line 7120
505. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover168 line 7124
506. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover166 line 7128
507. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover169 line 7147
508. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover170 line 7153
509. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover171 line 7157
510. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover172 line 7161
511. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover173 line 7167
512. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover174 line 7171
513. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover176 line 7177
514. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover175 line 7181
515. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover177 line 7197
516. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover178 line 7203
517. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover179 line 7207
518. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover180 line 7213
519. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover181 line 7226
520. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover182 line 7232
521. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover184 line 7242
522. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover185 line 7246
523. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover186 line 7252
524. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover183 line 7258
525. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover188 line 7298
526. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover187 line 7302
527. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover189 line 7318
528. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover190 line 7324
529. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover191 line 7337
530. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover192 line 7343
531. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover194 line 7353
532. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover193 line 7359
533. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover195 line 7386
534. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover196 line 7399
535. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover197 line 7409
536. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover198 line 7426
537. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover199 line 7436
538. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_seq131 line 7446
539. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover202 line 7648
540. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover201 line 7652
541. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover203 line 7668
542. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover204 line 7674
543. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover205 line 7687
544. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover200 line 7697
545. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover206 line 7789
546. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover207 line 7795
547. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover208 line 7808
548. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover209 line 7818
549. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover210 line 7845
550. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover211 line 7855
551. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover212 line 7872
552. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover214 line 7882
553. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover213 line 7892
554. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover215 line 7947
555. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover216 line 7957
556. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover217 line 7988
557. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover218 line 8005
558. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_seq4 line 8015
559. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover3 line 8242
560. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover223 line 8247
561. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover224 line 8253
562. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover225 line 8257
563. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover226 line 8261
564. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover227 line 8265
565. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover228 line 8271
566. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover229 line 8275
567. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover230 line 8281
568. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover222 line 8287
569. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover232 line 8343
570. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover233 line 8347
571. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover231 line 8351
572. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover234 line 8370
573. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover235 line 8376
574. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover236 line 8380
575. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover237 line 8384
576. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover238 line 8390
577. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover239 line 8394
578. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover241 line 8400
579. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover240 line 8404
580. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover242 line 8420
581. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover243 line 8426
582. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover244 line 8432
583. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover245 line 8445
584. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover246 line 8451
585. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover248 line 8461
586. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover249 line 8467
587. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover247 line 8473
588. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover250 line 8513
589. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover251 line 8519
590. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover252 line 8532
591. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover253 line 8542
592. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover254 line 8569
593. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover255 line 8586
594. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_seq221 line 8596
595. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover220 line 8798
596. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover257 line 8803
597. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover258 line 8809
598. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover259 line 8813
599. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover260 line 8817
600. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover261 line 8823
601. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover262 line 8827
602. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover264 line 8833
603. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover263 line 8837
604. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover265 line 8853
605. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover266 line 8859
606. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover267 line 8872
607. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover256 line 8882
608. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover269 line 8974
609. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover270 line 8978
610. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover271 line 8984
611. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover268 line 8990
612. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover273 line 9030
613. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover272 line 9034
614. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover274 line 9050
615. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover275 line 9056
616. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover276 line 9060
617. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover277 line 9066
618. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover278 line 9079
619. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover279 line 9085
620. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover281 line 9095
621. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover280 line 9101
622. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover282 line 9128
623. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover283 line 9141
624. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover284 line 9147
625. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover285 line 9157
626. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover286 line 9174
627. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover287 line 9184
628. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover289 line 9194
629. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover290 line 9200
630. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover291 line 9213
631. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover288 line 9223
632. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover293 line 9278
633. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover292 line 9284
634. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover294 line 9311
635. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover295 line 9321
636. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover296 line 9338
637. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover297 line 9348
638. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover299 line 9358
639. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover298 line 9368
640. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover300 line 9399
641. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover301 line 9416
642. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover302 line 9426
643. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover303 line 9443
644. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover304 line 9453
645. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_seq219 line 9463
646. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover307 line 9688
647. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover306 line 9694
648. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover308 line 9721
649. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover309 line 9731
650. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover310 line 9748
651. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover305 line 9758
652. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover311 line 9869
653. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover312 line 9879
654. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover313 line 9896
655. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover314 line 9906
656. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover315 line 9937
657. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover316 line 9947
658. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover317 line 9964
659. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover319 line 9974
660. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover318 line 9984
661. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover320 line 10043
662. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover321 line 10053
663. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover322 line 10084
664. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover323 line 10101
665. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_seq2 line 10111
666. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t7_cover1 line 10342
667. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k13_t7 line 10347
668. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover14 line 10351
669. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover13 line 10355
670. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover15 line 10361
671. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover16 line 10365
672. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover17 line 10369
673. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover18 line 10373
674. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover19 line 10377
675. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover12 line 10381
676. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover20 line 10406
677. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover21 line 10412
678. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover22 line 10416
679. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover23 line 10420
680. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover24 line 10424
681. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover25 line 10428
682. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover26 line 10434
683. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover27 line 10438
684. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover28 line 10442
685. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover29 line 10448
686. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover30 line 10454
687. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover11 line 10460
688. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover32 line 10535
689. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover33 line 10539
690. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover34 line 10543
691. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover35 line 10547
692. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover31 line 10551
693. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover36 line 10573
694. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover37 line 10579
695. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover38 line 10583
696. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover39 line 10587
697. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover40 line 10591
698. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover41 line 10597
699. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover42 line 10601
700. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover43 line 10605
701. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover44 line 10611
702. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover45 line 10615
703. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover47 line 10621
704. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover48 line 10625
705. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover46 line 10629
706. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover49 line 10648
707. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover50 line 10652
708. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover51 line 10658
709. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover52 line 10664
710. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover53 line 10680
711. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover54 line 10693
712. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_seq10 line 10703
713. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover9 line 10850
714. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover56 line 10855
715. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover57 line 10861
716. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover58 line 10865
717. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover59 line 10869
718. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover60 line 10873
719. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover61 line 10879
720. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover62 line 10883
721. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover63 line 10889
722. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover55 line 10895
723. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover65 line 10951
724. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover66 line 10955
725. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover64 line 10959
726. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover67 line 10978
727. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover68 line 10984
728. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover69 line 10988
729. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover70 line 10992
730. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover71 line 10998
731. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover72 line 11002
732. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover74 line 11008
733. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover73 line 11012
734. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover75 line 11028
735. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover76 line 11034
736. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover77 line 11040
737. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover78 line 11053
738. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover79 line 11059
739. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover81 line 11069
740. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover82 line 11075
741. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover80 line 11081
742. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover83 line 11121
743. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover84 line 11127
744. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover85 line 11140
745. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover86 line 11150
746. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover87 line 11177
747. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover88 line 11194
748. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_seq8 line 11204
749. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover7 line 11406
750. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover91 line 11411
751. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover92 line 11415
752. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover93 line 11419
753. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover90 line 11423
754. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover94 line 11442
755. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover95 line 11448
756. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover96 line 11452
757. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover97 line 11456
758. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover98 line 11462
759. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover99 line 11466
760. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover101 line 11472
761. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover100 line 11476
762. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover102 line 11492
763. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover103 line 11498
764. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover104 line 11511
765. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover89 line 11521
766. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover106 line 11613
767. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover107 line 11617
768. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover108 line 11621
769. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover109 line 11627
770. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover105 line 11633
771. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover111 line 11673
772. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover110 line 11677
773. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover112 line 11693
774. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover113 line 11699
775. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover114 line 11703
776. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover115 line 11709
777. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover116 line 11722
778. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover117 line 11728
779. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover119 line 11738
780. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover118 line 11744
781. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover120 line 11771
782. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover121 line 11784
783. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover122 line 11794
784. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover123 line 11811
785. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover124 line 11821
786. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover126 line 11831
787. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover127 line 11844
788. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover125 line 11854
789. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover128 line 11909
790. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover129 line 11919
791. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover130 line 11936
792. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover131 line 11946
793. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover132 line 11977
794. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover133 line 11994
795. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_seq6 line 12004
796. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover5 line 12229
797. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover136 line 12234
798. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover137 line 12240
799. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover138 line 12244
800. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover139 line 12248
801. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover140 line 12254
802. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover135 line 12260
803. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover142 line 12300
804. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover141 line 12304
805. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover143 line 12320
806. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover144 line 12326
807. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover145 line 12330
808. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover146 line 12336
809. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover147 line 12349
810. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover148 line 12355
811. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover150 line 12365
812. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover149 line 12371
813. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover151 line 12398
814. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover152 line 12408
815. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover153 line 12425
816. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover134 line 12435
817. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover155 line 12546
818. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover156 line 12552
819. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover157 line 12556
820. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover158 line 12562
821. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover159 line 12575
822. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover154 line 12585
823. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover161 line 12640
824. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover160 line 12646
825. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover162 line 12673
826. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover163 line 12686
827. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover164 line 12692
828. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover165 line 12702
829. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover166 line 12719
830. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover167 line 12729
831. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover169 line 12739
832. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover168 line 12749
833. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover170 line 12780
834. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover171 line 12797
835. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover172 line 12807
836. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover173 line 12824
837. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover174 line 12834
838. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover176 line 12844
839. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover177 line 12861
840. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover175 line 12871
841. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover178 line 12930
842. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover179 line 12940
843. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover180 line 12957
844. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover181 line 12967
845. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover182 line 12998
846. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover183 line 13015
847. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_seq4 line 13025
848. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover3 line 13254
849. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover187 line 13259
850. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover188 line 13263
851. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover186 line 13267
852. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover189 line 13283
853. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover190 line 13289
854. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover191 line 13293
855. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover192 line 13299
856. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover193 line 13312
857. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover185 line 13322
858. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover195 line 13377
859. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover196 line 13381
860. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover194 line 13387
861. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover197 line 13414
862. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover198 line 13427
863. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover199 line 13433
864. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover200 line 13443
865. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover201 line 13460
866. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover202 line 13470
867. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover204 line 13480
868. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover203 line 13490
869. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover205 line 13521
870. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover206 line 13531
871. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover207 line 13548
872. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover184 line 13558
873. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover209 line 13673
874. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover210 line 13686
875. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover211 line 13692
876. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover212 line 13702
877. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover213 line 13719
878. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover208 line 13729
879. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover215 line 13788
880. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover214 line 13798
881. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover216 line 13829
882. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover217 line 13846
883. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover218 line 13856
884. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover219 line 13866
885. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover220 line 13883
886. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover221 line 13893
887. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover223 line 13903
888. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover222 line 13913
889. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover224 line 13944
890. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover225 line 13961
891. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover226 line 13971
892. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover227 line 13988
893. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover228 line 13998
894. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover230 line 14008
895. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover231 line 14025
896. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover229 line 14035
897. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover232 line 14094
898. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover233 line 14104
899. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover234 line 14121
900. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover235 line 14131
901. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover236 line 14162
902. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover237 line 14179
903. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_seq2 line 14189
904. theorem OAI.CycleClique.Construction.CertifiedCoverage.k13t8_cover1 line 14418
905. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k13_t8 line 14423