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

GitHub source file

424 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover8 line 8
2. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover7 line 12
3. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover9 line 18
4. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover10 line 22
5. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover11 line 26
6. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover12 line 30
7. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover13 line 34
8. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover14 line 38
9. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover6 line 42
10. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover15 line 70
11. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover16 line 76
12. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover17 line 80
13. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover18 line 84
14. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover19 line 88
15. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover20 line 92
16. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover21 line 96
17. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover22 line 102
18. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover23 line 106
19. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover24 line 110
20. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover25 line 114
21. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover26 line 120
22. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover27 line 124
23. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover28 line 130
24. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover29 line 136
25. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover5 line 142
26. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover31 line 239
27. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover32 line 243
28. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover33 line 247
29. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover34 line 251
30. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover35 line 255
31. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover30 line 259
32. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover36 line 284
33. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover37 line 290
34. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover38 line 294
35. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover39 line 298
36. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover40 line 302
37. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover41 line 306
38. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover42 line 312
39. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover43 line 316
40. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover44 line 320
41. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover45 line 324
42. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover46 line 330
43. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover47 line 334
44. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover48 line 338
45. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover49 line 344
46. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover50 line 348
47. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover52 line 354
48. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover53 line 358
49. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover54 line 362
50. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover51 line 366
51. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover55 line 388
52. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover56 line 392
53. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover57 line 396
54. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover58 line 402
55. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover59 line 406
56. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover60 line 412
57. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover62 line 418
58. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover61 line 422
59. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover63 line 441
60. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover64 line 447
61. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover65 line 463
62. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover66 line 476
63. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_seq4 line 486
64. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover3 line 705
65. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover69 line 710
66. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover70 line 716
67. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover71 line 720
68. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover72 line 724
69. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover73 line 728
70. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover74 line 732
71. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover75 line 738
72. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover76 line 742
73. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover77 line 746
74. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover78 line 752
75. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover79 line 758
76. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover68 line 764
77. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover81 line 839
78. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover82 line 843
79. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover83 line 847
80. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover80 line 851
81. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover84 line 873
82. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover85 line 879
83. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover86 line 883
84. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover87 line 887
85. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover88 line 891
86. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover89 line 897
87. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover90 line 901
88. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover91 line 905
89. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover92 line 911
90. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover93 line 915
91. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover95 line 921
92. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover96 line 925
93. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover94 line 929
94. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover97 line 948
95. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover98 line 954
96. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover99 line 958
97. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover100 line 964
98. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover101 line 968
99. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover103 line 974
100. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover102 line 978
101. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover104 line 994
102. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover105 line 1000
103. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover106 line 1006
104. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover107 line 1019
105. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover108 line 1025
106. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_seq67 line 1035
107. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover110 line 1182
108. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover111 line 1188
109. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover112 line 1192
110. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover113 line 1198
111. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover109 line 1204
112. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover114 line 1260
113. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover115 line 1264
114. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover116 line 1270
115. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover117 line 1276
116. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover118 line 1292
117. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover119 line 1298
118. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover120 line 1311
119. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover122 line 1321
120. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover121 line 1327
121. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover123 line 1367
122. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover124 line 1377
123. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover125 line 1404
124. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover126 line 1421
125. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_seq2 line 1431
126. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t5_cover1 line 1635
127. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k11_t5 line 1640
128. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover10 line 1644
129. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover9 line 1648
130. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover11 line 1654
131. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover12 line 1658
132. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover13 line 1662
133. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover14 line 1666
134. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover15 line 1670
135. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover8 line 1674
136. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover16 line 1699
137. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover17 line 1705
138. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover18 line 1709
139. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover19 line 1713
140. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover20 line 1717
141. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover21 line 1721
142. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover22 line 1727
143. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover23 line 1731
144. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover24 line 1735
145. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover25 line 1741
146. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover26 line 1747
147. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover7 line 1753
148. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover28 line 1828
149. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover29 line 1832
150. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover30 line 1836
151. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover31 line 1840
152. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover27 line 1844
153. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover32 line 1866
154. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover33 line 1872
155. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover34 line 1876
156. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover35 line 1880
157. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover36 line 1884
158. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover37 line 1890
159. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover38 line 1894
160. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover39 line 1898
161. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover40 line 1904
162. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover41 line 1908
163. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover43 line 1914
164. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover44 line 1918
165. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover42 line 1922
166. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover45 line 1941
167. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover46 line 1945
168. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover47 line 1951
169. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover48 line 1957
170. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover49 line 1973
171. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover50 line 1986
172. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_seq6 line 1996
173. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover5 line 2143
174. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover52 line 2148
175. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover53 line 2154
176. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover54 line 2158
177. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover55 line 2162
178. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover56 line 2166
179. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover57 line 2172
180. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover58 line 2176
181. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover59 line 2182
182. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover51 line 2188
183. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover61 line 2244
184. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover62 line 2248
185. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover60 line 2252
186. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover63 line 2271
187. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover64 line 2277
188. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover65 line 2281
189. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover66 line 2285
190. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover67 line 2291
191. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover68 line 2295
192. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover70 line 2301
193. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover69 line 2305
194. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover71 line 2321
195. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover72 line 2327
196. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover73 line 2333
197. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover74 line 2346
198. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover75 line 2352
199. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover77 line 2362
200. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover78 line 2368
201. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover76 line 2374
202. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover79 line 2414
203. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover80 line 2420
204. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover81 line 2433
205. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover82 line 2443
206. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover83 line 2470
207. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover84 line 2487
208. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_seq4 line 2497
209. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover3 line 2699
210. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover87 line 2704
211. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover88 line 2708
212. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover89 line 2712
213. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover86 line 2716
214. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover90 line 2735
215. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover91 line 2741
216. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover92 line 2745
217. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover93 line 2749
218. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover94 line 2755
219. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover95 line 2759
220. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover97 line 2765
221. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover96 line 2769
222. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover98 line 2785
223. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover99 line 2791
224. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover100 line 2804
225. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover85 line 2814
226. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover102 line 2906
227. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover103 line 2910
228. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover104 line 2914
229. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover105 line 2920
230. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover101 line 2926
231. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover107 line 2966
232. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover106 line 2970
233. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover108 line 2986
234. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover109 line 2992
235. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover110 line 2996
236. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover111 line 3002
237. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover112 line 3015
238. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover113 line 3021
239. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover115 line 3031
240. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover114 line 3037
241. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover116 line 3064
242. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover117 line 3077
243. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover118 line 3087
244. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover119 line 3104
245. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover120 line 3114
246. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover122 line 3124
247. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover123 line 3137
248. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover121 line 3147
249. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover124 line 3202
250. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover125 line 3212
251. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover126 line 3229
252. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover127 line 3239
253. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover128 line 3270
254. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover129 line 3287
255. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_seq2 line 3297
256. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t6_cover1 line 3522
257. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k11_t6 line 3527
258. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover8 line 3531
259. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover7 line 3535
260. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover9 line 3541
261. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover10 line 3545
262. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover11 line 3549
263. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover12 line 3553
264. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover6 line 3557
265. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover13 line 3579
266. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover14 line 3585
267. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover15 line 3589
268. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover16 line 3593
269. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover17 line 3597
270. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover18 line 3603
271. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover19 line 3607
272. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover20 line 3613
273. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover5 line 3619
274. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover22 line 3675
275. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover23 line 3679
276. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover24 line 3683
277. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover21 line 3687
278. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover25 line 3706
279. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover26 line 3712
280. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover27 line 3716
281. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover28 line 3720
282. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover29 line 3726
283. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover30 line 3730
284. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover32 line 3736
285. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover31 line 3740
286. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover33 line 3756
287. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover34 line 3762
288. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover35 line 3775
289. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover4 line 3785
290. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover37 line 3877
291. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover38 line 3883
292. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover39 line 3887
293. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover40 line 3891
294. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover41 line 3897
295. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover36 line 3903
296. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover43 line 3943
297. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover42 line 3947
298. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover44 line 3963
299. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover45 line 3969
300. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover46 line 3973
301. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover47 line 3979
302. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover48 line 3992
303. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover49 line 3998
304. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover51 line 4008
305. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover50 line 4014
306. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover52 line 4041
307. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover53 line 4051
308. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover54 line 4068
309. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover3 line 4078
310. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover57 line 4189
311. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover58 line 4193
312. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover56 line 4197
313. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover59 line 4213
314. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover60 line 4219
315. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover61 line 4223
316. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover62 line 4229
317. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover63 line 4242
318. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover55 line 4252
319. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover65 line 4307
320. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover66 line 4311
321. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover64 line 4317
322. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover67 line 4344
323. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover68 line 4357
324. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover69 line 4363
325. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover70 line 4373
326. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover71 line 4390
327. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover72 line 4400
328. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover74 line 4410
329. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover73 line 4420
330. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover75 line 4451
331. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover76 line 4461
332. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover77 line 4478
333. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover2 line 4488
334. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover80 line 4603
335. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover81 line 4609
336. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover82 line 4613
337. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover79 line 4619
338. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover83 line 4646
339. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover84 line 4659
340. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover85 line 4665
341. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover86 line 4675
342. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover87 line 4692
343. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover78 line 4702
344. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover89 line 4761
345. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover90 line 4767
346. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover88 line 4777
347. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover91 line 4808
348. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover92 line 4825
349. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover93 line 4835
350. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover94 line 4845
351. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover95 line 4862
352. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover96 line 4872
353. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover98 line 4882
354. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover97 line 4892
355. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover99 line 4923
356. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover100 line 4933
357. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover101 line 4950
358. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t7_cover1 line 4960
359. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k11_t7 line 5075
360. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover9 line 5079
361. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover8 line 5083
362. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover10 line 5089
363. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover11 line 5093
364. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover12 line 5097
365. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover7 line 5101
366. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover13 line 5120
367. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover14 line 5126
368. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover15 line 5130
369. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover16 line 5134
370. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover17 line 5140
371. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover6 line 5146
372. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover19 line 5186
373. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover20 line 5190
374. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover18 line 5194
375. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover21 line 5210
376. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover22 line 5216
377. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover23 line 5220
378. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover24 line 5226
379. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover25 line 5239
380. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover5 line 5249
381. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover27 line 5304
382. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover28 line 5310
383. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover29 line 5314
384. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover26 line 5320
385. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover30 line 5347
386. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover31 line 5360
387. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover32 line 5366
388. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover33 line 5376
389. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover34 line 5393
390. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover4 line 5403
391. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover37 line 5462
392. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover36 line 5466
393. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover38 line 5479
394. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover39 line 5485
395. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover35 line 5495
396. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover40 line 5526
397. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover41 line 5543
398. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover42 line 5553
399. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover43 line 5563
400. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover44 line 5580
401. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover3 line 5590
402. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover47 line 5649
403. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover46 line 5655
404. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover48 line 5672
405. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover49 line 5682
406. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover45 line 5692
407. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover50 line 5723
408. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover51 line 5740
409. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover52 line 5750
410. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover53 line 5760
411. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover54 line 5777
412. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover2 line 5787
413. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover57 line 5846
414. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover56 line 5856
415. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover58 line 5873
416. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover59 line 5883
417. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover55 line 5893
418. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover60 line 5924
419. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover61 line 5941
420. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover62 line 5951
421. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover63 line 5961
422. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover64 line 5978
423. theorem OAI.CycleClique.Construction.CertifiedCoverage.k11t8_cover1 line 5988
424. theorem OAI.CycleClique.Construction.CertifiedCoverage.coverage_k11_t8 line 6047