OAI/Combinatorics/Ramsey/CycleClique/Certificates073.lean

GitHub source file

633 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.certificate_2304_q line 20
  2. def OAI.CycleClique.certificate_2304_edges line 21
  3. def OAI.CycleClique.certificate_2304_part_0 line 23
  4. def OAI.CycleClique.certificate_2304_part_1 line 25
  5. def OAI.CycleClique.certificate_2304_part_2 line 27
  6. def OAI.CycleClique.certificate_2304_part_3 line 29
  7. def OAI.CycleClique.certificate_2304_part_4 line 31
  8. def OAI.CycleClique.certificate_2304 line 33
  9. theorem OAI.CycleClique.certificate_2304_checked line 35
  10. theorem OAI.CycleClique.certificate_2304_valid line 36
  11. def OAI.CycleClique.certificate_2305_q line 38
  12. def OAI.CycleClique.certificate_2305_edges line 39
  13. def OAI.CycleClique.certificate_2305_part_0 line 41
  14. def OAI.CycleClique.certificate_2305_part_1 line 43
  15. def OAI.CycleClique.certificate_2305_part_2 line 45
  16. def OAI.CycleClique.certificate_2305_part_3 line 47
  17. def OAI.CycleClique.certificate_2305_part_4 line 49
  18. def OAI.CycleClique.certificate_2305 line 51
  19. theorem OAI.CycleClique.certificate_2305_checked line 53
  20. theorem OAI.CycleClique.certificate_2305_valid line 54
  21. def OAI.CycleClique.certificate_2306_q line 56
  22. def OAI.CycleClique.certificate_2306_edges line 57
  23. def OAI.CycleClique.certificate_2306_part_0 line 59
  24. def OAI.CycleClique.certificate_2306_part_1 line 61
  25. def OAI.CycleClique.certificate_2306_part_2 line 63
  26. def OAI.CycleClique.certificate_2306_part_3 line 65
  27. def OAI.CycleClique.certificate_2306_part_4 line 67
  28. def OAI.CycleClique.certificate_2306 line 69
  29. theorem OAI.CycleClique.certificate_2306_checked line 71
  30. theorem OAI.CycleClique.certificate_2306_valid line 72
  31. def OAI.CycleClique.certificate_2307_q line 74
  32. def OAI.CycleClique.certificate_2307_edges line 75
  33. def OAI.CycleClique.certificate_2307_part_0 line 77
  34. def OAI.CycleClique.certificate_2307_part_1 line 79
  35. def OAI.CycleClique.certificate_2307_part_2 line 81
  36. def OAI.CycleClique.certificate_2307_part_3 line 83
  37. def OAI.CycleClique.certificate_2307 line 85
  38. theorem OAI.CycleClique.certificate_2307_checked line 87
  39. theorem OAI.CycleClique.certificate_2307_valid line 88
  40. def OAI.CycleClique.certificate_2308_q line 90
  41. def OAI.CycleClique.certificate_2308_edges line 91
  42. def OAI.CycleClique.certificate_2308_part_0 line 93
  43. def OAI.CycleClique.certificate_2308_part_1 line 95
  44. def OAI.CycleClique.certificate_2308_part_2 line 97
  45. def OAI.CycleClique.certificate_2308_part_3 line 99
  46. def OAI.CycleClique.certificate_2308 line 101
  47. theorem OAI.CycleClique.certificate_2308_checked line 103
  48. theorem OAI.CycleClique.certificate_2308_valid line 104
  49. def OAI.CycleClique.certificate_2309_q line 106
  50. def OAI.CycleClique.certificate_2309_edges line 107
  51. def OAI.CycleClique.certificate_2309_part_0 line 109
  52. def OAI.CycleClique.certificate_2309_part_1 line 111
  53. def OAI.CycleClique.certificate_2309_part_2 line 113
  54. def OAI.CycleClique.certificate_2309_part_3 line 115
  55. def OAI.CycleClique.certificate_2309_part_4 line 117
  56. def OAI.CycleClique.certificate_2309 line 119
  57. theorem OAI.CycleClique.certificate_2309_checked line 121
  58. theorem OAI.CycleClique.certificate_2309_valid line 122
  59. def OAI.CycleClique.certificate_2310_q line 124
  60. def OAI.CycleClique.certificate_2310_edges line 125
  61. def OAI.CycleClique.certificate_2310_part_0 line 127
  62. def OAI.CycleClique.certificate_2310_part_1 line 129
  63. def OAI.CycleClique.certificate_2310_part_2 line 131
  64. def OAI.CycleClique.certificate_2310_part_3 line 133
  65. def OAI.CycleClique.certificate_2310_part_4 line 135
  66. def OAI.CycleClique.certificate_2310 line 137
  67. theorem OAI.CycleClique.certificate_2310_checked line 139
  68. theorem OAI.CycleClique.certificate_2310_valid line 140
  69. def OAI.CycleClique.certificate_2311_q line 142
  70. def OAI.CycleClique.certificate_2311_edges line 143
  71. def OAI.CycleClique.certificate_2311_part_0 line 145
  72. def OAI.CycleClique.certificate_2311_part_1 line 147
  73. def OAI.CycleClique.certificate_2311_part_2 line 149
  74. def OAI.CycleClique.certificate_2311_part_3 line 151
  75. def OAI.CycleClique.certificate_2311 line 153
  76. theorem OAI.CycleClique.certificate_2311_checked line 155
  77. theorem OAI.CycleClique.certificate_2311_valid line 156
  78. def OAI.CycleClique.certificate_2312_q line 158
  79. def OAI.CycleClique.certificate_2312_edges line 159
  80. def OAI.CycleClique.certificate_2312_part_0 line 161
  81. def OAI.CycleClique.certificate_2312_part_1 line 163
  82. def OAI.CycleClique.certificate_2312_part_2 line 165
  83. def OAI.CycleClique.certificate_2312_part_3 line 167
  84. def OAI.CycleClique.certificate_2312_part_4 line 169
  85. def OAI.CycleClique.certificate_2312 line 171
  86. theorem OAI.CycleClique.certificate_2312_checked line 173
  87. theorem OAI.CycleClique.certificate_2312_valid line 174
  88. def OAI.CycleClique.certificate_2313_q line 176
  89. def OAI.CycleClique.certificate_2313_edges line 177
  90. def OAI.CycleClique.certificate_2313_part_0 line 179
  91. def OAI.CycleClique.certificate_2313_part_1 line 181
  92. def OAI.CycleClique.certificate_2313_part_2 line 183
  93. def OAI.CycleClique.certificate_2313_part_3 line 185
  94. def OAI.CycleClique.certificate_2313_part_4 line 187
  95. def OAI.CycleClique.certificate_2313 line 189
  96. theorem OAI.CycleClique.certificate_2313_checked line 191
  97. theorem OAI.CycleClique.certificate_2313_valid line 192
  98. def OAI.CycleClique.certificate_2314_q line 194
  99. def OAI.CycleClique.certificate_2314_edges line 195
  100. def OAI.CycleClique.certificate_2314_part_0 line 197
  101. def OAI.CycleClique.certificate_2314_part_1 line 199
  102. def OAI.CycleClique.certificate_2314_part_2 line 201
  103. def OAI.CycleClique.certificate_2314_part_3 line 203
  104. def OAI.CycleClique.certificate_2314_part_4 line 205
  105. def OAI.CycleClique.certificate_2314 line 207
  106. theorem OAI.CycleClique.certificate_2314_checked line 209
  107. theorem OAI.CycleClique.certificate_2314_valid line 210
  108. def OAI.CycleClique.certificate_2315_q line 212
  109. def OAI.CycleClique.certificate_2315_edges line 213
  110. def OAI.CycleClique.certificate_2315_part_0 line 215
  111. def OAI.CycleClique.certificate_2315_part_1 line 217
  112. def OAI.CycleClique.certificate_2315_part_2 line 219
  113. def OAI.CycleClique.certificate_2315_part_3 line 221
  114. def OAI.CycleClique.certificate_2315_part_4 line 223
  115. def OAI.CycleClique.certificate_2315 line 225
  116. theorem OAI.CycleClique.certificate_2315_checked line 227
  117. theorem OAI.CycleClique.certificate_2315_valid line 228
  118. def OAI.CycleClique.certificate_2316_q line 230
  119. def OAI.CycleClique.certificate_2316_edges line 231
  120. def OAI.CycleClique.certificate_2316_part_0 line 233
  121. def OAI.CycleClique.certificate_2316_part_1 line 235
  122. def OAI.CycleClique.certificate_2316_part_2 line 237
  123. def OAI.CycleClique.certificate_2316_part_3 line 239
  124. def OAI.CycleClique.certificate_2316_part_4 line 241
  125. def OAI.CycleClique.certificate_2316 line 243
  126. theorem OAI.CycleClique.certificate_2316_checked line 245
  127. theorem OAI.CycleClique.certificate_2316_valid line 246
  128. def OAI.CycleClique.certificate_2317_q line 248
  129. def OAI.CycleClique.certificate_2317_edges line 249
  130. def OAI.CycleClique.certificate_2317_part_0 line 251
  131. def OAI.CycleClique.certificate_2317_part_1 line 253
  132. def OAI.CycleClique.certificate_2317_part_2 line 255
  133. def OAI.CycleClique.certificate_2317_part_3 line 257
  134. def OAI.CycleClique.certificate_2317_part_4 line 259
  135. def OAI.CycleClique.certificate_2317 line 261
  136. theorem OAI.CycleClique.certificate_2317_checked line 263
  137. theorem OAI.CycleClique.certificate_2317_valid line 264
  138. def OAI.CycleClique.certificate_2318_q line 266
  139. def OAI.CycleClique.certificate_2318_edges line 268
  140. def OAI.CycleClique.certificate_2318_E line 270
  141. def OAI.CycleClique.certificate_2318_M line 272
  142. def OAI.CycleClique.certificate_2318_part_1_E line 274
  143. def OAI.CycleClique.certificate_2318_part_1_M line 276
  144. def OAI.CycleClique.certificate_2318_part_2_E line 278
  145. def OAI.CycleClique.certificate_2318_part_2_M line 280
  146. def OAI.CycleClique.certificate_2318_part_3_E line 282
  147. def OAI.CycleClique.certificate_2318_part_3_M line 284
  148. def OAI.CycleClique.certificate_2318_part_4_E line 286
  149. def OAI.CycleClique.certificate_2318_part_4_M line 288
  150. def OAI.CycleClique.certificate_2318_part_5_E line 290
  151. def OAI.CycleClique.certificate_2318_part_5_M line 292
  152. def OAI.CycleClique.certificate_2318_part_6_E line 294
  153. def OAI.CycleClique.certificate_2318_part_6_M line 296
  154. def OAI.CycleClique.certificate_2318_part_7_E line 298
  155. def OAI.CycleClique.certificate_2318_part_7_M line 300
  156. def OAI.CycleClique.certificate_2318_part_8_E line 302
  157. def OAI.CycleClique.certificate_2318_part_8_M line 304
  158. def OAI.CycleClique.certificate_2318_part_9_E line 306
  159. def OAI.CycleClique.certificate_2318_part_9_M line 308
  160. def OAI.CycleClique.certificate_2318_part_10_E line 310
  161. def OAI.CycleClique.certificate_2318_part_10_M line 312
  162. def OAI.CycleClique.certificate_2318_part_11_E line 314
  163. def OAI.CycleClique.certificate_2318_part_11_M line 316
  164. def OAI.CycleClique.certificate_2318_part_12_E line 318
  165. def OAI.CycleClique.certificate_2318_part_12_M line 320
  166. def OAI.CycleClique.certificate_2318_part_13_E line 322
  167. def OAI.CycleClique.certificate_2318_part_13_M line 324
  168. def OAI.CycleClique.certificate_2318_part_13 line 326
  169. theorem OAI.CycleClique.certificate_2318_part_13_checked line 328
  170. def OAI.CycleClique.certificate_2318_part_12 line 330
  171. theorem OAI.CycleClique.certificate_2318_part_12_checked line 332
  172. def OAI.CycleClique.certificate_2318_part_14_E line 334
  173. def OAI.CycleClique.certificate_2318_part_14_M line 336
  174. def OAI.CycleClique.certificate_2318_part_15_E line 338
  175. def OAI.CycleClique.certificate_2318_part_15_M line 340
  176. def OAI.CycleClique.certificate_2318_part_15 line 342
  177. theorem OAI.CycleClique.certificate_2318_part_15_checked line 344
  178. def OAI.CycleClique.certificate_2318_part_16_E line 346
  179. def OAI.CycleClique.certificate_2318_part_16_M line 348
  180. def OAI.CycleClique.certificate_2318_part_17_E line 350
  181. def OAI.CycleClique.certificate_2318_part_17_M line 352
  182. def OAI.CycleClique.certificate_2318_part_18_E line 354
  183. def OAI.CycleClique.certificate_2318_part_18_M line 356
  184. def OAI.CycleClique.certificate_2318_part_18 line 358
  185. theorem OAI.CycleClique.certificate_2318_part_18_checked line 360
  186. def OAI.CycleClique.certificate_2318_part_17 line 362
  187. theorem OAI.CycleClique.certificate_2318_part_17_checked line 364
  188. def OAI.CycleClique.certificate_2318_part_16 line 366
  189. theorem OAI.CycleClique.certificate_2318_part_16_checked line 368
  190. def OAI.CycleClique.certificate_2318_part_19_E line 370
  191. def OAI.CycleClique.certificate_2318_part_19_M line 372
  192. def OAI.CycleClique.certificate_2318_part_20_E line 374
  193. def OAI.CycleClique.certificate_2318_part_20_M line 376
  194. def OAI.CycleClique.certificate_2318_part_20 line 378
  195. theorem OAI.CycleClique.certificate_2318_part_20_checked line 380
  196. def OAI.CycleClique.certificate_2318_part_21_E line 382
  197. def OAI.CycleClique.certificate_2318_part_21_M line 384
  198. def OAI.CycleClique.certificate_2318_part_22_E line 386
  199. def OAI.CycleClique.certificate_2318_part_22_M line 388
  200. def OAI.CycleClique.certificate_2318_part_22 line 390
  201. theorem OAI.CycleClique.certificate_2318_part_22_checked line 392
  202. def OAI.CycleClique.certificate_2318_part_21 line 394
  203. theorem OAI.CycleClique.certificate_2318_part_21_checked line 396
  204. def OAI.CycleClique.certificate_2318_part_23_E line 398
  205. def OAI.CycleClique.certificate_2318_part_23_M line 400
  206. def OAI.CycleClique.certificate_2318_part_24_E line 402
  207. def OAI.CycleClique.certificate_2318_part_24_M line 404
  208. def OAI.CycleClique.certificate_2318_part_25_E line 406
  209. def OAI.CycleClique.certificate_2318_part_25_M line 408
  210. def OAI.CycleClique.certificate_2318_part_26_E line 410
  211. def OAI.CycleClique.certificate_2318_part_26_M line 412
  212. def OAI.CycleClique.certificate_2318_part_27_E line 414
  213. def OAI.CycleClique.certificate_2318_part_27_M line 416
  214. def OAI.CycleClique.certificate_2318_part_28_E line 418
  215. def OAI.CycleClique.certificate_2318_part_28_M line 420
  216. def OAI.CycleClique.certificate_2318_part_29_E line 422
  217. def OAI.CycleClique.certificate_2318_part_29_M line 424
  218. def OAI.CycleClique.certificate_2318_part_30_E line 426
  219. def OAI.CycleClique.certificate_2318_part_30_M line 428
  220. def OAI.CycleClique.certificate_2318_part_30 line 430
  221. theorem OAI.CycleClique.certificate_2318_part_30_checked line 432
  222. def OAI.CycleClique.certificate_2318_part_31_E line 434
  223. def OAI.CycleClique.certificate_2318_part_31_M line 436
  224. def OAI.CycleClique.certificate_2318_part_31 line 438
  225. theorem OAI.CycleClique.certificate_2318_part_31_checked line 440
  226. def OAI.CycleClique.certificate_2318_part_32_E line 442
  227. def OAI.CycleClique.certificate_2318_part_32_M line 444
  228. def OAI.CycleClique.certificate_2318_part_33_E line 446
  229. def OAI.CycleClique.certificate_2318_part_33_M line 448
  230. def OAI.CycleClique.certificate_2318_part_33 line 450
  231. theorem OAI.CycleClique.certificate_2318_part_33_checked line 452
  232. def OAI.CycleClique.certificate_2318_part_32 line 454
  233. theorem OAI.CycleClique.certificate_2318_part_32_checked line 456
  234. def OAI.CycleClique.certificate_2318_part_34_E line 458
  235. def OAI.CycleClique.certificate_2318_part_34_M line 460
  236. def OAI.CycleClique.certificate_2318_part_35_E line 462
  237. def OAI.CycleClique.certificate_2318_part_35_M line 464
  238. def OAI.CycleClique.certificate_2318_part_35 line 466
  239. theorem OAI.CycleClique.certificate_2318_part_35_checked line 468
  240. def OAI.CycleClique.certificate_2318_part_34 line 470
  241. theorem OAI.CycleClique.certificate_2318_part_34_checked line 472
  242. def OAI.CycleClique.certificate_2318_part_36_E line 474
  243. def OAI.CycleClique.certificate_2318_part_36_M line 476
  244. def OAI.CycleClique.certificate_2318_part_36 line 478
  245. theorem OAI.CycleClique.certificate_2318_part_36_checked line 480
  246. def OAI.CycleClique.certificate_2318_part_37_E line 482
  247. def OAI.CycleClique.certificate_2318_part_37_M line 484
  248. def OAI.CycleClique.certificate_2318_part_38_E line 486
  249. def OAI.CycleClique.certificate_2318_part_38_M line 488
  250. def OAI.CycleClique.certificate_2318_part_38 line 490
  251. theorem OAI.CycleClique.certificate_2318_part_38_checked line 492
  252. def OAI.CycleClique.certificate_2318_part_37 line 494
  253. theorem OAI.CycleClique.certificate_2318_part_37_checked line 496
  254. def OAI.CycleClique.certificate_2318_part_39_E line 498
  255. def OAI.CycleClique.certificate_2318_part_39_M line 500
  256. def OAI.CycleClique.certificate_2318_part_40_E line 502
  257. def OAI.CycleClique.certificate_2318_part_40_M line 504
  258. def OAI.CycleClique.certificate_2318_part_40 line 506
  259. theorem OAI.CycleClique.certificate_2318_part_40_checked line 508
  260. def OAI.CycleClique.certificate_2318_part_41_E line 510
  261. def OAI.CycleClique.certificate_2318_part_41_M line 512
  262. def OAI.CycleClique.certificate_2318_part_42_E line 514
  263. def OAI.CycleClique.certificate_2318_part_42_M line 516
  264. def OAI.CycleClique.certificate_2318_part_43_E line 518
  265. def OAI.CycleClique.certificate_2318_part_43_M line 520
  266. def OAI.CycleClique.certificate_2318_part_43 line 522
  267. theorem OAI.CycleClique.certificate_2318_part_43_checked line 524
  268. def OAI.CycleClique.certificate_2318_part_42 line 526
  269. theorem OAI.CycleClique.certificate_2318_part_42_checked line 528
  270. def OAI.CycleClique.certificate_2318_part_44_E line 530
  271. def OAI.CycleClique.certificate_2318_part_44_M line 532
  272. def OAI.CycleClique.certificate_2318_part_45_E line 534
  273. def OAI.CycleClique.certificate_2318_part_45_M line 536
  274. def OAI.CycleClique.certificate_2318_part_45 line 538
  275. theorem OAI.CycleClique.certificate_2318_part_45_checked line 540
  276. def OAI.CycleClique.certificate_2318_part_44 line 542
  277. theorem OAI.CycleClique.certificate_2318_part_44_checked line 544
  278. def OAI.CycleClique.certificate_2318_part_46_E line 546
  279. def OAI.CycleClique.certificate_2318_part_46_M line 548
  280. def OAI.CycleClique.certificate_2318_part_47_E line 550
  281. def OAI.CycleClique.certificate_2318_part_47_M line 552
  282. def OAI.CycleClique.certificate_2318_part_48_E line 554
  283. def OAI.CycleClique.certificate_2318_part_48_M line 556
  284. def OAI.CycleClique.certificate_2318_part_48 line 558
  285. theorem OAI.CycleClique.certificate_2318_part_48_checked line 560
  286. def OAI.CycleClique.certificate_2318_part_49_E line 562
  287. def OAI.CycleClique.certificate_2318_part_49_M line 564
  288. def OAI.CycleClique.certificate_2318_part_50_E line 566
  289. def OAI.CycleClique.certificate_2318_part_50_M line 568
  290. def OAI.CycleClique.certificate_2318_part_51_E line 570
  291. def OAI.CycleClique.certificate_2318_part_51_M line 572
  292. def OAI.CycleClique.certificate_2318_part_52_E line 574
  293. def OAI.CycleClique.certificate_2318_part_52_M line 576
  294. def OAI.CycleClique.certificate_2318_part_53_E line 578
  295. def OAI.CycleClique.certificate_2318_part_53_M line 580
  296. def OAI.CycleClique.certificate_2318_part_53 line 582
  297. theorem OAI.CycleClique.certificate_2318_part_53_checked line 584
  298. def OAI.CycleClique.certificate_2318_part_52 line 586
  299. theorem OAI.CycleClique.certificate_2318_part_52_checked line 588
  300. def OAI.CycleClique.certificate_2318_part_51 line 590
  301. theorem OAI.CycleClique.certificate_2318_part_51_checked line 592
  302. def OAI.CycleClique.certificate_2318_part_50 line 594
  303. theorem OAI.CycleClique.certificate_2318_part_50_checked line 596
  304. def OAI.CycleClique.certificate_2318_part_49 line 598
  305. theorem OAI.CycleClique.certificate_2318_part_49_checked line 600
  306. def OAI.CycleClique.certificate_2318_part_54_E line 602
  307. def OAI.CycleClique.certificate_2318_part_54_M line 604
  308. def OAI.CycleClique.certificate_2318_part_55_E line 606
  309. def OAI.CycleClique.certificate_2318_part_55_M line 608
  310. def OAI.CycleClique.certificate_2318_part_55 line 610
  311. theorem OAI.CycleClique.certificate_2318_part_55_checked line 612
  312. def OAI.CycleClique.certificate_2318_part_54 line 614
  313. theorem OAI.CycleClique.certificate_2318_part_54_checked line 616
  314. def OAI.CycleClique.certificate_2318_part_56_E line 618
  315. def OAI.CycleClique.certificate_2318_part_56_M line 620
  316. def OAI.CycleClique.certificate_2318_part_57_E line 622
  317. def OAI.CycleClique.certificate_2318_part_57_M line 624
  318. def OAI.CycleClique.certificate_2318_part_57 line 626
  319. theorem OAI.CycleClique.certificate_2318_part_57_checked line 628
  320. def OAI.CycleClique.certificate_2318_part_58_E line 630
  321. def OAI.CycleClique.certificate_2318_part_58_M line 632
  322. def OAI.CycleClique.certificate_2318_part_58 line 634
  323. theorem OAI.CycleClique.certificate_2318_part_58_checked line 636
  324. def OAI.CycleClique.certificate_2318_part_59_E line 638
  325. def OAI.CycleClique.certificate_2318_part_59_M line 640
  326. def OAI.CycleClique.certificate_2318_part_59 line 642
  327. theorem OAI.CycleClique.certificate_2318_part_59_checked line 644
  328. def OAI.CycleClique.certificate_2318_part_60_E line 646
  329. def OAI.CycleClique.certificate_2318_part_60_M line 648
  330. def OAI.CycleClique.certificate_2318_part_60 line 650
  331. theorem OAI.CycleClique.certificate_2318_part_60_checked line 652
  332. def OAI.CycleClique.certificate_2318_part_61_E line 654
  333. def OAI.CycleClique.certificate_2318_part_61_M line 656
  334. def OAI.CycleClique.certificate_2318_part_62_E line 658
  335. def OAI.CycleClique.certificate_2318_part_62_M line 660
  336. def OAI.CycleClique.certificate_2318_part_62 line 662
  337. theorem OAI.CycleClique.certificate_2318_part_62_checked line 664
  338. def OAI.CycleClique.certificate_2318_part_63_E line 666
  339. def OAI.CycleClique.certificate_2318_part_63_M line 668
  340. def OAI.CycleClique.certificate_2318_part_63 line 670
  341. theorem OAI.CycleClique.certificate_2318_part_63_checked line 672
  342. def OAI.CycleClique.certificate_2318_part_64_E line 674
  343. def OAI.CycleClique.certificate_2318_part_64_M line 676
  344. def OAI.CycleClique.certificate_2318_part_64 line 678
  345. theorem OAI.CycleClique.certificate_2318_part_64_checked line 680
  346. def OAI.CycleClique.certificate_2318_part_65_E line 682
  347. def OAI.CycleClique.certificate_2318_part_65_M line 684
  348. def OAI.CycleClique.certificate_2318_part_65 line 686
  349. theorem OAI.CycleClique.certificate_2318_part_65_checked line 688
  350. def OAI.CycleClique.certificate_2318_part_66_E line 690
  351. def OAI.CycleClique.certificate_2318_part_66_M line 692
  352. def OAI.CycleClique.certificate_2318_part_66 line 694
  353. theorem OAI.CycleClique.certificate_2318_part_66_checked line 696
  354. def OAI.CycleClique.certificate_2318_part_67_E line 698
  355. def OAI.CycleClique.certificate_2318_part_67_M line 700
  356. def OAI.CycleClique.certificate_2318_part_68_E line 702
  357. def OAI.CycleClique.certificate_2318_part_68_M line 704
  358. def OAI.CycleClique.certificate_2318_part_68 line 706
  359. theorem OAI.CycleClique.certificate_2318_part_68_checked line 708
  360. def OAI.CycleClique.certificate_2318_part_67 line 710
  361. theorem OAI.CycleClique.certificate_2318_part_67_checked line 712
  362. def OAI.CycleClique.certificate_2318_part_69_E line 714
  363. def OAI.CycleClique.certificate_2318_part_69_M line 716
  364. def OAI.CycleClique.certificate_2318_part_70_E line 718
  365. def OAI.CycleClique.certificate_2318_part_70_M line 720
  366. def OAI.CycleClique.certificate_2318_part_70 line 722
  367. theorem OAI.CycleClique.certificate_2318_part_70_checked line 724
  368. def OAI.CycleClique.certificate_2318_part_69 line 726
  369. theorem OAI.CycleClique.certificate_2318_part_69_checked line 728
  370. def OAI.CycleClique.certificate_2318_part_71_E line 730
  371. def OAI.CycleClique.certificate_2318_part_71_M line 732
  372. def OAI.CycleClique.certificate_2318_part_72_E line 734
  373. def OAI.CycleClique.certificate_2318_part_72_M line 736
  374. def OAI.CycleClique.certificate_2318_part_72 line 738
  375. theorem OAI.CycleClique.certificate_2318_part_72_checked line 740
  376. def OAI.CycleClique.certificate_2318_part_71 line 742
  377. theorem OAI.CycleClique.certificate_2318_part_71_checked line 744
  378. def OAI.CycleClique.certificate_2318_part_73_E line 746
  379. def OAI.CycleClique.certificate_2318_part_73_M line 748
  380. def OAI.CycleClique.certificate_2318_part_74_E line 750
  381. def OAI.CycleClique.certificate_2318_part_74_M line 752
  382. def OAI.CycleClique.certificate_2318_part_74 line 754
  383. theorem OAI.CycleClique.certificate_2318_part_74_checked line 756
  384. def OAI.CycleClique.certificate_2318_part_75_E line 758
  385. def OAI.CycleClique.certificate_2318_part_75_M line 760
  386. def OAI.CycleClique.certificate_2318_part_76_E line 762
  387. def OAI.CycleClique.certificate_2318_part_76_M line 764
  388. def OAI.CycleClique.certificate_2318_part_76 line 766
  389. theorem OAI.CycleClique.certificate_2318_part_76_checked line 768
  390. def OAI.CycleClique.certificate_2318_part_75 line 770
  391. theorem OAI.CycleClique.certificate_2318_part_75_checked line 772
  392. def OAI.CycleClique.certificate_2318_part_77_E line 774
  393. def OAI.CycleClique.certificate_2318_part_77_M line 776
  394. def OAI.CycleClique.certificate_2318_part_78_E line 778
  395. def OAI.CycleClique.certificate_2318_part_78_M line 780
  396. def OAI.CycleClique.certificate_2318_part_78 line 782
  397. theorem OAI.CycleClique.certificate_2318_part_78_checked line 784
  398. def OAI.CycleClique.certificate_2318_part_79_E line 786
  399. def OAI.CycleClique.certificate_2318_part_79_M line 788
  400. def OAI.CycleClique.certificate_2318_part_79 line 790
  401. theorem OAI.CycleClique.certificate_2318_part_79_checked line 792
  402. def OAI.CycleClique.certificate_2318_part_80_E line 794
  403. def OAI.CycleClique.certificate_2318_part_80_M line 796
  404. def OAI.CycleClique.certificate_2318_part_80 line 798
  405. theorem OAI.CycleClique.certificate_2318_part_80_checked line 800
  406. def OAI.CycleClique.certificate_2318_part_81_E line 802
  407. def OAI.CycleClique.certificate_2318_part_81_M line 804
  408. def OAI.CycleClique.certificate_2318_part_81 line 806
  409. theorem OAI.CycleClique.certificate_2318_part_81_checked line 808
  410. def OAI.CycleClique.certificate_2318_part_82_E line 810
  411. def OAI.CycleClique.certificate_2318_part_82_M line 812
  412. def OAI.CycleClique.certificate_2318_part_82 line 814
  413. theorem OAI.CycleClique.certificate_2318_part_82_checked line 816
  414. def OAI.CycleClique.certificate_2318_part_77 line 818
  415. theorem OAI.CycleClique.certificate_2318_part_77_checked line 820
  416. def OAI.CycleClique.certificate_2318_part_73 line 822
  417. theorem OAI.CycleClique.certificate_2318_part_73_checked line 824
  418. def OAI.CycleClique.certificate_2318_part_61 line 826
  419. theorem OAI.CycleClique.certificate_2318_part_61_checked line 828
  420. def OAI.CycleClique.certificate_2318_part_56 line 830
  421. theorem OAI.CycleClique.certificate_2318_part_56_checked line 832
  422. def OAI.CycleClique.certificate_2318_part_47 line 834
  423. theorem OAI.CycleClique.certificate_2318_part_47_checked line 836
  424. def OAI.CycleClique.certificate_2318_part_46 line 838
  425. theorem OAI.CycleClique.certificate_2318_part_46_checked line 840
  426. def OAI.CycleClique.certificate_2318_part_41 line 842
  427. theorem OAI.CycleClique.certificate_2318_part_41_checked line 844
  428. def OAI.CycleClique.certificate_2318_part_39 line 846
  429. theorem OAI.CycleClique.certificate_2318_part_39_checked line 848
  430. def OAI.CycleClique.certificate_2318_part_29 line 850
  431. theorem OAI.CycleClique.certificate_2318_part_29_checked line 852
  432. def OAI.CycleClique.certificate_2318_part_28 line 854
  433. theorem OAI.CycleClique.certificate_2318_part_28_checked line 856
  434. def OAI.CycleClique.certificate_2318_part_27 line 858
  435. theorem OAI.CycleClique.certificate_2318_part_27_checked line 860
  436. def OAI.CycleClique.certificate_2318_part_26 line 862
  437. theorem OAI.CycleClique.certificate_2318_part_26_checked line 864
  438. def OAI.CycleClique.certificate_2318_part_25 line 866
  439. theorem OAI.CycleClique.certificate_2318_part_25_checked line 868
  440. def OAI.CycleClique.certificate_2318_part_24 line 870
  441. theorem OAI.CycleClique.certificate_2318_part_24_checked line 872
  442. def OAI.CycleClique.certificate_2318_part_23 line 874
  443. theorem OAI.CycleClique.certificate_2318_part_23_checked line 876
  444. def OAI.CycleClique.certificate_2318_part_19 line 878
  445. theorem OAI.CycleClique.certificate_2318_part_19_checked line 880
  446. def OAI.CycleClique.certificate_2318_part_14 line 882
  447. theorem OAI.CycleClique.certificate_2318_part_14_checked line 884
  448. def OAI.CycleClique.certificate_2318_part_11 line 886
  449. theorem OAI.CycleClique.certificate_2318_part_11_checked line 888
  450. def OAI.CycleClique.certificate_2318_part_10 line 890
  451. theorem OAI.CycleClique.certificate_2318_part_10_checked line 892
  452. def OAI.CycleClique.certificate_2318_part_9 line 894
  453. theorem OAI.CycleClique.certificate_2318_part_9_checked line 896
  454. def OAI.CycleClique.certificate_2318_part_8 line 898
  455. theorem OAI.CycleClique.certificate_2318_part_8_checked line 900
  456. def OAI.CycleClique.certificate_2318_part_7 line 902
  457. theorem OAI.CycleClique.certificate_2318_part_7_checked line 904
  458. def OAI.CycleClique.certificate_2318_part_6 line 906
  459. theorem OAI.CycleClique.certificate_2318_part_6_checked line 908
  460. def OAI.CycleClique.certificate_2318_part_5 line 910
  461. theorem OAI.CycleClique.certificate_2318_part_5_checked line 912
  462. def OAI.CycleClique.certificate_2318_part_4 line 914
  463. theorem OAI.CycleClique.certificate_2318_part_4_checked line 916
  464. def OAI.CycleClique.certificate_2318_part_3 line 918
  465. theorem OAI.CycleClique.certificate_2318_part_3_checked line 920
  466. def OAI.CycleClique.certificate_2318_part_2 line 922
  467. theorem OAI.CycleClique.certificate_2318_part_2_checked line 924
  468. def OAI.CycleClique.certificate_2318_part_1 line 926
  469. theorem OAI.CycleClique.certificate_2318_part_1_checked line 928
  470. def OAI.CycleClique.certificate_2318 line 930
  471. theorem OAI.CycleClique.certificate_2318_checked line 932
  472. theorem OAI.CycleClique.certificate_2318_valid line 934
  473. def OAI.CycleClique.certificate_2319_q line 936
  474. def OAI.CycleClique.certificate_2319_edges line 937
  475. def OAI.CycleClique.certificate_2319_part_0 line 939
  476. def OAI.CycleClique.certificate_2319_part_1 line 941
  477. def OAI.CycleClique.certificate_2319_part_2 line 943
  478. def OAI.CycleClique.certificate_2319_part_3 line 945
  479. def OAI.CycleClique.certificate_2319_part_4 line 947
  480. def OAI.CycleClique.certificate_2319 line 949
  481. theorem OAI.CycleClique.certificate_2319_checked line 951
  482. theorem OAI.CycleClique.certificate_2319_valid line 952
  483. def OAI.CycleClique.certificate_2320_q line 954
  484. def OAI.CycleClique.certificate_2320_edges line 955
  485. def OAI.CycleClique.certificate_2320_part_0 line 957
  486. def OAI.CycleClique.certificate_2320_part_1 line 959
  487. def OAI.CycleClique.certificate_2320_part_2 line 961
  488. def OAI.CycleClique.certificate_2320_part_3 line 963
  489. def OAI.CycleClique.certificate_2320 line 965
  490. theorem OAI.CycleClique.certificate_2320_checked line 967
  491. theorem OAI.CycleClique.certificate_2320_valid line 968
  492. def OAI.CycleClique.certificate_2321_q line 970
  493. def OAI.CycleClique.certificate_2321_edges line 971
  494. def OAI.CycleClique.certificate_2321_part_0 line 973
  495. def OAI.CycleClique.certificate_2321_part_1 line 975
  496. def OAI.CycleClique.certificate_2321_part_2 line 977
  497. def OAI.CycleClique.certificate_2321_part_3 line 979
  498. def OAI.CycleClique.certificate_2321 line 981
  499. theorem OAI.CycleClique.certificate_2321_checked line 983
  500. theorem OAI.CycleClique.certificate_2321_valid line 984
  501. def OAI.CycleClique.certificate_2322_q line 986
  502. def OAI.CycleClique.certificate_2322_edges line 987
  503. def OAI.CycleClique.certificate_2322_part_0 line 989
  504. def OAI.CycleClique.certificate_2322_part_1 line 991
  505. def OAI.CycleClique.certificate_2322_part_2 line 993
  506. def OAI.CycleClique.certificate_2322_part_3 line 995
  507. def OAI.CycleClique.certificate_2322 line 997
  508. theorem OAI.CycleClique.certificate_2322_checked line 999
  509. theorem OAI.CycleClique.certificate_2322_valid line 1000
  510. def OAI.CycleClique.certificate_2323_q line 1002
  511. def OAI.CycleClique.certificate_2323_edges line 1003
  512. def OAI.CycleClique.certificate_2323_part_0 line 1005
  513. def OAI.CycleClique.certificate_2323_part_1 line 1007
  514. def OAI.CycleClique.certificate_2323_part_2 line 1009
  515. def OAI.CycleClique.certificate_2323_part_3 line 1011
  516. def OAI.CycleClique.certificate_2323 line 1013
  517. theorem OAI.CycleClique.certificate_2323_checked line 1015
  518. theorem OAI.CycleClique.certificate_2323_valid line 1016
  519. def OAI.CycleClique.certificate_2324_q line 1018
  520. def OAI.CycleClique.certificate_2324_edges line 1019
  521. def OAI.CycleClique.certificate_2324_part_0 line 1021
  522. def OAI.CycleClique.certificate_2324_part_1 line 1023
  523. def OAI.CycleClique.certificate_2324_part_2 line 1025
  524. def OAI.CycleClique.certificate_2324_part_3 line 1027
  525. def OAI.CycleClique.certificate_2324 line 1029
  526. theorem OAI.CycleClique.certificate_2324_checked line 1031
  527. theorem OAI.CycleClique.certificate_2324_valid line 1032
  528. def OAI.CycleClique.certificate_2325_q line 1034
  529. def OAI.CycleClique.certificate_2325_edges line 1035
  530. def OAI.CycleClique.certificate_2325_part_0 line 1037
  531. def OAI.CycleClique.certificate_2325_part_1 line 1039
  532. def OAI.CycleClique.certificate_2325_part_2 line 1041
  533. def OAI.CycleClique.certificate_2325_part_3 line 1043
  534. def OAI.CycleClique.certificate_2325_part_4 line 1045
  535. def OAI.CycleClique.certificate_2325 line 1047
  536. theorem OAI.CycleClique.certificate_2325_checked line 1049
  537. theorem OAI.CycleClique.certificate_2325_valid line 1050
  538. def OAI.CycleClique.certificate_2326_q line 1052
  539. def OAI.CycleClique.certificate_2326_edges line 1053
  540. def OAI.CycleClique.certificate_2326_part_0 line 1055
  541. def OAI.CycleClique.certificate_2326_part_1 line 1057
  542. def OAI.CycleClique.certificate_2326_part_2 line 1059
  543. def OAI.CycleClique.certificate_2326_part_3 line 1061
  544. def OAI.CycleClique.certificate_2326_part_4 line 1063
  545. def OAI.CycleClique.certificate_2326 line 1065
  546. theorem OAI.CycleClique.certificate_2326_checked line 1067
  547. theorem OAI.CycleClique.certificate_2326_valid line 1068
  548. def OAI.CycleClique.certificate_2327_q line 1070
  549. def OAI.CycleClique.certificate_2327_edges line 1071
  550. def OAI.CycleClique.certificate_2327_part_0 line 1073
  551. def OAI.CycleClique.certificate_2327_part_1 line 1075
  552. def OAI.CycleClique.certificate_2327_part_2 line 1077
  553. def OAI.CycleClique.certificate_2327_part_3 line 1079
  554. def OAI.CycleClique.certificate_2327 line 1081
  555. theorem OAI.CycleClique.certificate_2327_checked line 1083
  556. theorem OAI.CycleClique.certificate_2327_valid line 1084
  557. def OAI.CycleClique.certificate_2328_q line 1086
  558. def OAI.CycleClique.certificate_2328_edges line 1087
  559. def OAI.CycleClique.certificate_2328_part_0 line 1089
  560. def OAI.CycleClique.certificate_2328_part_1 line 1091
  561. def OAI.CycleClique.certificate_2328_part_2 line 1093
  562. def OAI.CycleClique.certificate_2328_part_3 line 1095
  563. def OAI.CycleClique.certificate_2328 line 1097
  564. theorem OAI.CycleClique.certificate_2328_checked line 1099
  565. theorem OAI.CycleClique.certificate_2328_valid line 1100
  566. def OAI.CycleClique.certificate_2329_q line 1102
  567. def OAI.CycleClique.certificate_2329_edges line 1103
  568. def OAI.CycleClique.certificate_2329_part_0 line 1105
  569. def OAI.CycleClique.certificate_2329_part_1 line 1107
  570. def OAI.CycleClique.certificate_2329_part_2 line 1109
  571. def OAI.CycleClique.certificate_2329_part_3 line 1111
  572. def OAI.CycleClique.certificate_2329 line 1113
  573. theorem OAI.CycleClique.certificate_2329_checked line 1115
  574. theorem OAI.CycleClique.certificate_2329_valid line 1116
  575. def OAI.CycleClique.certificate_2330_q line 1118
  576. def OAI.CycleClique.certificate_2330_edges line 1119
  577. def OAI.CycleClique.certificate_2330_part_0 line 1121
  578. def OAI.CycleClique.certificate_2330_part_1 line 1123
  579. def OAI.CycleClique.certificate_2330_part_2 line 1125
  580. def OAI.CycleClique.certificate_2330_part_3 line 1127
  581. def OAI.CycleClique.certificate_2330_part_4 line 1129
  582. def OAI.CycleClique.certificate_2330 line 1131
  583. theorem OAI.CycleClique.certificate_2330_checked line 1133
  584. theorem OAI.CycleClique.certificate_2330_valid line 1134
  585. def OAI.CycleClique.certificate_2331_q line 1136
  586. def OAI.CycleClique.certificate_2331_edges line 1137
  587. def OAI.CycleClique.certificate_2331_part_0 line 1139
  588. def OAI.CycleClique.certificate_2331_part_1 line 1141
  589. def OAI.CycleClique.certificate_2331_part_2 line 1143
  590. def OAI.CycleClique.certificate_2331_part_3 line 1145
  591. def OAI.CycleClique.certificate_2331_part_4 line 1147
  592. def OAI.CycleClique.certificate_2331 line 1149
  593. theorem OAI.CycleClique.certificate_2331_checked line 1151
  594. theorem OAI.CycleClique.certificate_2331_valid line 1152
  595. def OAI.CycleClique.certificate_2332_q line 1154
  596. def OAI.CycleClique.certificate_2332_edges line 1155
  597. def OAI.CycleClique.certificate_2332_part_0 line 1157
  598. def OAI.CycleClique.certificate_2332_part_1 line 1159
  599. def OAI.CycleClique.certificate_2332_part_2 line 1161
  600. def OAI.CycleClique.certificate_2332_part_3 line 1163
  601. def OAI.CycleClique.certificate_2332 line 1165
  602. theorem OAI.CycleClique.certificate_2332_checked line 1167
  603. theorem OAI.CycleClique.certificate_2332_valid line 1168
  604. def OAI.CycleClique.certificate_2333_q line 1170
  605. def OAI.CycleClique.certificate_2333_edges line 1171
  606. def OAI.CycleClique.certificate_2333_part_0 line 1173
  607. def OAI.CycleClique.certificate_2333_part_1 line 1175
  608. def OAI.CycleClique.certificate_2333_part_2 line 1177
  609. def OAI.CycleClique.certificate_2333_part_3 line 1179
  610. def OAI.CycleClique.certificate_2333_part_4 line 1181
  611. def OAI.CycleClique.certificate_2333 line 1183
  612. theorem OAI.CycleClique.certificate_2333_checked line 1185
  613. theorem OAI.CycleClique.certificate_2333_valid line 1186
  614. def OAI.CycleClique.certificate_2334_q line 1188
  615. def OAI.CycleClique.certificate_2334_edges line 1189
  616. def OAI.CycleClique.certificate_2334_part_0 line 1191
  617. def OAI.CycleClique.certificate_2334_part_1 line 1193
  618. def OAI.CycleClique.certificate_2334_part_2 line 1195
  619. def OAI.CycleClique.certificate_2334_part_3 line 1197
  620. def OAI.CycleClique.certificate_2334_part_4 line 1199
  621. def OAI.CycleClique.certificate_2334 line 1201
  622. theorem OAI.CycleClique.certificate_2334_checked line 1203
  623. theorem OAI.CycleClique.certificate_2334_valid line 1204
  624. def OAI.CycleClique.certificate_2335_q line 1206
  625. def OAI.CycleClique.certificate_2335_edges line 1207
  626. def OAI.CycleClique.certificate_2335_part_0 line 1209
  627. def OAI.CycleClique.certificate_2335_part_1 line 1211
  628. def OAI.CycleClique.certificate_2335_part_2 line 1213
  629. def OAI.CycleClique.certificate_2335_part_3 line 1215
  630. def OAI.CycleClique.certificate_2335_part_4 line 1217
  631. def OAI.CycleClique.certificate_2335 line 1219
  632. theorem OAI.CycleClique.certificate_2335_checked line 1221
  633. theorem OAI.CycleClique.certificate_2335_valid line 1222