OAI/Combinatorics/Ramsey/CycleClique/Certificates019.lean

GitHub source file

445 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.certificate_576_q line 20
  2. def OAI.CycleClique.certificate_576_edges line 21
  3. def OAI.CycleClique.certificate_576_part_0 line 23
  4. def OAI.CycleClique.certificate_576_part_1 line 25
  5. def OAI.CycleClique.certificate_576_part_2 line 27
  6. def OAI.CycleClique.certificate_576 line 29
  7. theorem OAI.CycleClique.certificate_576_checked line 31
  8. theorem OAI.CycleClique.certificate_576_valid line 32
  9. def OAI.CycleClique.certificate_577_q line 34
  10. def OAI.CycleClique.certificate_577_edges line 36
  11. def OAI.CycleClique.certificate_577_E line 38
  12. def OAI.CycleClique.certificate_577_M line 40
  13. def OAI.CycleClique.certificate_577_part_1_E line 42
  14. def OAI.CycleClique.certificate_577_part_1_M line 44
  15. def OAI.CycleClique.certificate_577_part_2_E line 46
  16. def OAI.CycleClique.certificate_577_part_2_M line 48
  17. def OAI.CycleClique.certificate_577_part_3_E line 50
  18. def OAI.CycleClique.certificate_577_part_3_M line 52
  19. def OAI.CycleClique.certificate_577_part_4_E line 54
  20. def OAI.CycleClique.certificate_577_part_4_M line 56
  21. def OAI.CycleClique.certificate_577_part_5_E line 58
  22. def OAI.CycleClique.certificate_577_part_5_M line 60
  23. def OAI.CycleClique.certificate_577_part_6_E line 62
  24. def OAI.CycleClique.certificate_577_part_6_M line 64
  25. def OAI.CycleClique.certificate_577_part_7_E line 66
  26. def OAI.CycleClique.certificate_577_part_7_M line 68
  27. def OAI.CycleClique.certificate_577_part_8_E line 70
  28. def OAI.CycleClique.certificate_577_part_8_M line 72
  29. def OAI.CycleClique.certificate_577_part_8 line 74
  30. theorem OAI.CycleClique.certificate_577_part_8_checked line 76
  31. def OAI.CycleClique.certificate_577_part_9_E line 78
  32. def OAI.CycleClique.certificate_577_part_9_M line 80
  33. def OAI.CycleClique.certificate_577_part_10_E line 82
  34. def OAI.CycleClique.certificate_577_part_10_M line 84
  35. def OAI.CycleClique.certificate_577_part_11_E line 86
  36. def OAI.CycleClique.certificate_577_part_11_M line 88
  37. def OAI.CycleClique.certificate_577_part_12_E line 90
  38. def OAI.CycleClique.certificate_577_part_12_M line 92
  39. def OAI.CycleClique.certificate_577_part_13_E line 94
  40. def OAI.CycleClique.certificate_577_part_13_M line 96
  41. def OAI.CycleClique.certificate_577_part_14_E line 98
  42. def OAI.CycleClique.certificate_577_part_14_M line 100
  43. def OAI.CycleClique.certificate_577_part_14 line 102
  44. theorem OAI.CycleClique.certificate_577_part_14_checked line 104
  45. def OAI.CycleClique.certificate_577_part_15_E line 106
  46. def OAI.CycleClique.certificate_577_part_15_M line 108
  47. def OAI.CycleClique.certificate_577_part_16_E line 110
  48. def OAI.CycleClique.certificate_577_part_16_M line 112
  49. def OAI.CycleClique.certificate_577_part_17_E line 114
  50. def OAI.CycleClique.certificate_577_part_17_M line 116
  51. def OAI.CycleClique.certificate_577_part_18_E line 118
  52. def OAI.CycleClique.certificate_577_part_18_M line 120
  53. def OAI.CycleClique.certificate_577_part_19_E line 122
  54. def OAI.CycleClique.certificate_577_part_19_M line 124
  55. def OAI.CycleClique.certificate_577_part_19 line 126
  56. theorem OAI.CycleClique.certificate_577_part_19_checked line 128
  57. def OAI.CycleClique.certificate_577_part_20_E line 130
  58. def OAI.CycleClique.certificate_577_part_20_M line 132
  59. def OAI.CycleClique.certificate_577_part_21_E line 134
  60. def OAI.CycleClique.certificate_577_part_21_M line 136
  61. def OAI.CycleClique.certificate_577_part_21 line 138
  62. theorem OAI.CycleClique.certificate_577_part_21_checked line 140
  63. def OAI.CycleClique.certificate_577_part_20 line 142
  64. theorem OAI.CycleClique.certificate_577_part_20_checked line 144
  65. def OAI.CycleClique.certificate_577_part_22_E line 146
  66. def OAI.CycleClique.certificate_577_part_22_M line 148
  67. def OAI.CycleClique.certificate_577_part_23_E line 150
  68. def OAI.CycleClique.certificate_577_part_23_M line 152
  69. def OAI.CycleClique.certificate_577_part_24_E line 154
  70. def OAI.CycleClique.certificate_577_part_24_M line 156
  71. def OAI.CycleClique.certificate_577_part_25_E line 158
  72. def OAI.CycleClique.certificate_577_part_25_M line 160
  73. def OAI.CycleClique.certificate_577_part_26_E line 162
  74. def OAI.CycleClique.certificate_577_part_26_M line 164
  75. def OAI.CycleClique.certificate_577_part_26 line 166
  76. theorem OAI.CycleClique.certificate_577_part_26_checked line 168
  77. def OAI.CycleClique.certificate_577_part_27_E line 170
  78. def OAI.CycleClique.certificate_577_part_27_M line 172
  79. def OAI.CycleClique.certificate_577_part_27 line 174
  80. theorem OAI.CycleClique.certificate_577_part_27_checked line 176
  81. def OAI.CycleClique.certificate_577_part_28_E line 178
  82. def OAI.CycleClique.certificate_577_part_28_M line 180
  83. def OAI.CycleClique.certificate_577_part_28 line 182
  84. theorem OAI.CycleClique.certificate_577_part_28_checked line 184
  85. def OAI.CycleClique.certificate_577_part_29_E line 186
  86. def OAI.CycleClique.certificate_577_part_29_M line 188
  87. def OAI.CycleClique.certificate_577_part_29 line 190
  88. theorem OAI.CycleClique.certificate_577_part_29_checked line 192
  89. def OAI.CycleClique.certificate_577_part_30_E line 194
  90. def OAI.CycleClique.certificate_577_part_30_M line 196
  91. def OAI.CycleClique.certificate_577_part_31_E line 198
  92. def OAI.CycleClique.certificate_577_part_31_M line 200
  93. def OAI.CycleClique.certificate_577_part_31 line 202
  94. theorem OAI.CycleClique.certificate_577_part_31_checked line 204
  95. def OAI.CycleClique.certificate_577_part_32_E line 206
  96. def OAI.CycleClique.certificate_577_part_32_M line 208
  97. def OAI.CycleClique.certificate_577_part_33_E line 210
  98. def OAI.CycleClique.certificate_577_part_33_M line 212
  99. def OAI.CycleClique.certificate_577_part_34_E line 214
  100. def OAI.CycleClique.certificate_577_part_34_M line 216
  101. def OAI.CycleClique.certificate_577_part_35_E line 218
  102. def OAI.CycleClique.certificate_577_part_35_M line 220
  103. def OAI.CycleClique.certificate_577_part_36_E line 222
  104. def OAI.CycleClique.certificate_577_part_36_M line 224
  105. def OAI.CycleClique.certificate_577_part_36 line 226
  106. theorem OAI.CycleClique.certificate_577_part_36_checked line 228
  107. def OAI.CycleClique.certificate_577_part_37_E line 230
  108. def OAI.CycleClique.certificate_577_part_37_M line 232
  109. def OAI.CycleClique.certificate_577_part_38_E line 234
  110. def OAI.CycleClique.certificate_577_part_38_M line 236
  111. def OAI.CycleClique.certificate_577_part_38 line 238
  112. theorem OAI.CycleClique.certificate_577_part_38_checked line 240
  113. def OAI.CycleClique.certificate_577_part_39_E line 242
  114. def OAI.CycleClique.certificate_577_part_39_M line 244
  115. def OAI.CycleClique.certificate_577_part_40_E line 246
  116. def OAI.CycleClique.certificate_577_part_40_M line 248
  117. def OAI.CycleClique.certificate_577_part_41_E line 250
  118. def OAI.CycleClique.certificate_577_part_41_M line 252
  119. def OAI.CycleClique.certificate_577_part_42_E line 254
  120. def OAI.CycleClique.certificate_577_part_42_M line 256
  121. def OAI.CycleClique.certificate_577_part_42 line 258
  122. theorem OAI.CycleClique.certificate_577_part_42_checked line 260
  123. def OAI.CycleClique.certificate_577_part_41 line 262
  124. theorem OAI.CycleClique.certificate_577_part_41_checked line 264
  125. def OAI.CycleClique.certificate_577_part_40 line 266
  126. theorem OAI.CycleClique.certificate_577_part_40_checked line 268
  127. def OAI.CycleClique.certificate_577_part_43_E line 270
  128. def OAI.CycleClique.certificate_577_part_43_M line 272
  129. def OAI.CycleClique.certificate_577_part_43 line 274
  130. theorem OAI.CycleClique.certificate_577_part_43_checked line 276
  131. def OAI.CycleClique.certificate_577_part_44_E line 278
  132. def OAI.CycleClique.certificate_577_part_44_M line 280
  133. def OAI.CycleClique.certificate_577_part_44 line 282
  134. theorem OAI.CycleClique.certificate_577_part_44_checked line 284
  135. def OAI.CycleClique.certificate_577_part_45_E line 286
  136. def OAI.CycleClique.certificate_577_part_45_M line 288
  137. def OAI.CycleClique.certificate_577_part_46_E line 290
  138. def OAI.CycleClique.certificate_577_part_46_M line 292
  139. def OAI.CycleClique.certificate_577_part_46 line 294
  140. theorem OAI.CycleClique.certificate_577_part_46_checked line 296
  141. def OAI.CycleClique.certificate_577_part_47_E line 298
  142. def OAI.CycleClique.certificate_577_part_47_M line 300
  143. def OAI.CycleClique.certificate_577_part_47 line 302
  144. theorem OAI.CycleClique.certificate_577_part_47_checked line 304
  145. def OAI.CycleClique.certificate_577_part_48_E line 306
  146. def OAI.CycleClique.certificate_577_part_48_M line 308
  147. def OAI.CycleClique.certificate_577_part_49_E line 310
  148. def OAI.CycleClique.certificate_577_part_49_M line 312
  149. def OAI.CycleClique.certificate_577_part_50_E line 314
  150. def OAI.CycleClique.certificate_577_part_50_M line 316
  151. def OAI.CycleClique.certificate_577_part_50 line 318
  152. theorem OAI.CycleClique.certificate_577_part_50_checked line 320
  153. def OAI.CycleClique.certificate_577_part_49 line 322
  154. theorem OAI.CycleClique.certificate_577_part_49_checked line 324
  155. def OAI.CycleClique.certificate_577_part_48 line 326
  156. theorem OAI.CycleClique.certificate_577_part_48_checked line 328
  157. def OAI.CycleClique.certificate_577_part_45 line 330
  158. theorem OAI.CycleClique.certificate_577_part_45_checked line 332
  159. def OAI.CycleClique.certificate_577_part_39 line 334
  160. theorem OAI.CycleClique.certificate_577_part_39_checked line 336
  161. def OAI.CycleClique.certificate_577_part_37 line 338
  162. theorem OAI.CycleClique.certificate_577_part_37_checked line 340
  163. def OAI.CycleClique.certificate_577_part_35 line 342
  164. theorem OAI.CycleClique.certificate_577_part_35_checked line 344
  165. def OAI.CycleClique.certificate_577_part_34 line 346
  166. theorem OAI.CycleClique.certificate_577_part_34_checked line 348
  167. def OAI.CycleClique.certificate_577_part_33 line 350
  168. theorem OAI.CycleClique.certificate_577_part_33_checked line 352
  169. def OAI.CycleClique.certificate_577_part_32 line 354
  170. theorem OAI.CycleClique.certificate_577_part_32_checked line 356
  171. def OAI.CycleClique.certificate_577_part_30 line 358
  172. theorem OAI.CycleClique.certificate_577_part_30_checked line 360
  173. def OAI.CycleClique.certificate_577_part_25 line 362
  174. theorem OAI.CycleClique.certificate_577_part_25_checked line 364
  175. def OAI.CycleClique.certificate_577_part_24 line 366
  176. theorem OAI.CycleClique.certificate_577_part_24_checked line 368
  177. def OAI.CycleClique.certificate_577_part_23 line 370
  178. theorem OAI.CycleClique.certificate_577_part_23_checked line 372
  179. def OAI.CycleClique.certificate_577_part_22 line 374
  180. theorem OAI.CycleClique.certificate_577_part_22_checked line 376
  181. def OAI.CycleClique.certificate_577_part_18 line 378
  182. theorem OAI.CycleClique.certificate_577_part_18_checked line 380
  183. def OAI.CycleClique.certificate_577_part_17 line 382
  184. theorem OAI.CycleClique.certificate_577_part_17_checked line 384
  185. def OAI.CycleClique.certificate_577_part_16 line 386
  186. theorem OAI.CycleClique.certificate_577_part_16_checked line 388
  187. def OAI.CycleClique.certificate_577_part_15 line 390
  188. theorem OAI.CycleClique.certificate_577_part_15_checked line 392
  189. def OAI.CycleClique.certificate_577_part_13 line 394
  190. theorem OAI.CycleClique.certificate_577_part_13_checked line 396
  191. def OAI.CycleClique.certificate_577_part_12 line 398
  192. theorem OAI.CycleClique.certificate_577_part_12_checked line 400
  193. def OAI.CycleClique.certificate_577_part_11 line 402
  194. theorem OAI.CycleClique.certificate_577_part_11_checked line 404
  195. def OAI.CycleClique.certificate_577_part_10 line 406
  196. theorem OAI.CycleClique.certificate_577_part_10_checked line 408
  197. def OAI.CycleClique.certificate_577_part_9 line 410
  198. theorem OAI.CycleClique.certificate_577_part_9_checked line 412
  199. def OAI.CycleClique.certificate_577_part_7 line 414
  200. theorem OAI.CycleClique.certificate_577_part_7_checked line 416
  201. def OAI.CycleClique.certificate_577_part_6 line 418
  202. theorem OAI.CycleClique.certificate_577_part_6_checked line 420
  203. def OAI.CycleClique.certificate_577_part_5 line 422
  204. theorem OAI.CycleClique.certificate_577_part_5_checked line 424
  205. def OAI.CycleClique.certificate_577_part_4 line 426
  206. theorem OAI.CycleClique.certificate_577_part_4_checked line 428
  207. def OAI.CycleClique.certificate_577_part_3 line 430
  208. theorem OAI.CycleClique.certificate_577_part_3_checked line 432
  209. def OAI.CycleClique.certificate_577_part_2 line 434
  210. theorem OAI.CycleClique.certificate_577_part_2_checked line 436
  211. def OAI.CycleClique.certificate_577_part_1 line 438
  212. theorem OAI.CycleClique.certificate_577_part_1_checked line 440
  213. def OAI.CycleClique.certificate_577 line 442
  214. theorem OAI.CycleClique.certificate_577_checked line 444
  215. theorem OAI.CycleClique.certificate_577_valid line 446
  216. def OAI.CycleClique.certificate_578_q line 448
  217. def OAI.CycleClique.certificate_578_edges line 449
  218. def OAI.CycleClique.certificate_578_part_0 line 451
  219. def OAI.CycleClique.certificate_578_part_1 line 453
  220. def OAI.CycleClique.certificate_578_part_2 line 455
  221. def OAI.CycleClique.certificate_578 line 457
  222. theorem OAI.CycleClique.certificate_578_checked line 459
  223. theorem OAI.CycleClique.certificate_578_valid line 460
  224. def OAI.CycleClique.certificate_579_q line 462
  225. def OAI.CycleClique.certificate_579_edges line 463
  226. def OAI.CycleClique.certificate_579_part_0 line 465
  227. def OAI.CycleClique.certificate_579_part_1 line 467
  228. def OAI.CycleClique.certificate_579 line 469
  229. theorem OAI.CycleClique.certificate_579_checked line 471
  230. theorem OAI.CycleClique.certificate_579_valid line 472
  231. def OAI.CycleClique.certificate_580_q line 474
  232. def OAI.CycleClique.certificate_580_edges line 475
  233. def OAI.CycleClique.certificate_580_part_0 line 477
  234. def OAI.CycleClique.certificate_580_part_1 line 479
  235. def OAI.CycleClique.certificate_580 line 481
  236. theorem OAI.CycleClique.certificate_580_checked line 483
  237. theorem OAI.CycleClique.certificate_580_valid line 484
  238. def OAI.CycleClique.certificate_581_q line 486
  239. def OAI.CycleClique.certificate_581_edges line 487
  240. def OAI.CycleClique.certificate_581_part_0 line 489
  241. def OAI.CycleClique.certificate_581_part_1 line 491
  242. def OAI.CycleClique.certificate_581 line 493
  243. theorem OAI.CycleClique.certificate_581_checked line 495
  244. theorem OAI.CycleClique.certificate_581_valid line 496
  245. def OAI.CycleClique.certificate_582_q line 498
  246. def OAI.CycleClique.certificate_582_edges line 499
  247. def OAI.CycleClique.certificate_582_part_0 line 501
  248. def OAI.CycleClique.certificate_582_part_1 line 503
  249. def OAI.CycleClique.certificate_582_part_2 line 505
  250. def OAI.CycleClique.certificate_582 line 507
  251. theorem OAI.CycleClique.certificate_582_checked line 509
  252. theorem OAI.CycleClique.certificate_582_valid line 510
  253. def OAI.CycleClique.certificate_583_q line 512
  254. def OAI.CycleClique.certificate_583_edges line 513
  255. def OAI.CycleClique.certificate_583_part_0 line 515
  256. def OAI.CycleClique.certificate_583_part_1 line 517
  257. def OAI.CycleClique.certificate_583_part_2 line 519
  258. def OAI.CycleClique.certificate_583 line 521
  259. theorem OAI.CycleClique.certificate_583_checked line 523
  260. theorem OAI.CycleClique.certificate_583_valid line 524
  261. def OAI.CycleClique.certificate_584_q line 526
  262. def OAI.CycleClique.certificate_584_edges line 527
  263. def OAI.CycleClique.certificate_584_part_0 line 529
  264. def OAI.CycleClique.certificate_584_part_1 line 531
  265. def OAI.CycleClique.certificate_584 line 533
  266. theorem OAI.CycleClique.certificate_584_checked line 535
  267. theorem OAI.CycleClique.certificate_584_valid line 536
  268. def OAI.CycleClique.certificate_585_q line 538
  269. def OAI.CycleClique.certificate_585_edges line 539
  270. def OAI.CycleClique.certificate_585_part_0 line 541
  271. def OAI.CycleClique.certificate_585_part_1 line 543
  272. def OAI.CycleClique.certificate_585_part_2 line 545
  273. def OAI.CycleClique.certificate_585 line 547
  274. theorem OAI.CycleClique.certificate_585_checked line 549
  275. theorem OAI.CycleClique.certificate_585_valid line 550
  276. def OAI.CycleClique.certificate_586_q line 552
  277. def OAI.CycleClique.certificate_586_edges line 553
  278. def OAI.CycleClique.certificate_586_part_0 line 555
  279. def OAI.CycleClique.certificate_586_part_1 line 557
  280. def OAI.CycleClique.certificate_586_part_2 line 559
  281. def OAI.CycleClique.certificate_586 line 561
  282. theorem OAI.CycleClique.certificate_586_checked line 563
  283. theorem OAI.CycleClique.certificate_586_valid line 564
  284. def OAI.CycleClique.certificate_587_q line 566
  285. def OAI.CycleClique.certificate_587_edges line 567
  286. def OAI.CycleClique.certificate_587_part_0 line 569
  287. def OAI.CycleClique.certificate_587_part_1 line 571
  288. def OAI.CycleClique.certificate_587_part_2 line 573
  289. def OAI.CycleClique.certificate_587 line 575
  290. theorem OAI.CycleClique.certificate_587_checked line 577
  291. theorem OAI.CycleClique.certificate_587_valid line 578
  292. def OAI.CycleClique.certificate_588_q line 580
  293. def OAI.CycleClique.certificate_588_edges line 581
  294. def OAI.CycleClique.certificate_588_part_0 line 583
  295. def OAI.CycleClique.certificate_588_part_1 line 585
  296. def OAI.CycleClique.certificate_588 line 587
  297. theorem OAI.CycleClique.certificate_588_checked line 589
  298. theorem OAI.CycleClique.certificate_588_valid line 590
  299. def OAI.CycleClique.certificate_589_q line 592
  300. def OAI.CycleClique.certificate_589_edges line 593
  301. def OAI.CycleClique.certificate_589_part_0 line 595
  302. def OAI.CycleClique.certificate_589_part_1 line 597
  303. def OAI.CycleClique.certificate_589 line 599
  304. theorem OAI.CycleClique.certificate_589_checked line 601
  305. theorem OAI.CycleClique.certificate_589_valid line 602
  306. def OAI.CycleClique.certificate_590_q line 604
  307. def OAI.CycleClique.certificate_590_edges line 605
  308. def OAI.CycleClique.certificate_590_part_0 line 607
  309. def OAI.CycleClique.certificate_590_part_1 line 609
  310. def OAI.CycleClique.certificate_590_part_2 line 611
  311. def OAI.CycleClique.certificate_590 line 613
  312. theorem OAI.CycleClique.certificate_590_checked line 615
  313. theorem OAI.CycleClique.certificate_590_valid line 616
  314. def OAI.CycleClique.certificate_591_q line 618
  315. def OAI.CycleClique.certificate_591_edges line 619
  316. def OAI.CycleClique.certificate_591_part_0 line 621
  317. def OAI.CycleClique.certificate_591_part_1 line 623
  318. def OAI.CycleClique.certificate_591_part_2 line 625
  319. def OAI.CycleClique.certificate_591 line 627
  320. theorem OAI.CycleClique.certificate_591_checked line 629
  321. theorem OAI.CycleClique.certificate_591_valid line 630
  322. def OAI.CycleClique.certificate_592_q line 632
  323. def OAI.CycleClique.certificate_592_edges line 633
  324. def OAI.CycleClique.certificate_592_part_0 line 635
  325. def OAI.CycleClique.certificate_592_part_1 line 637
  326. def OAI.CycleClique.certificate_592 line 639
  327. theorem OAI.CycleClique.certificate_592_checked line 641
  328. theorem OAI.CycleClique.certificate_592_valid line 642
  329. def OAI.CycleClique.certificate_593_q line 644
  330. def OAI.CycleClique.certificate_593_edges line 645
  331. def OAI.CycleClique.certificate_593_part_0 line 647
  332. def OAI.CycleClique.certificate_593_part_1 line 649
  333. def OAI.CycleClique.certificate_593 line 651
  334. theorem OAI.CycleClique.certificate_593_checked line 653
  335. theorem OAI.CycleClique.certificate_593_valid line 654
  336. def OAI.CycleClique.certificate_594_q line 656
  337. def OAI.CycleClique.certificate_594_edges line 657
  338. def OAI.CycleClique.certificate_594_part_0 line 659
  339. def OAI.CycleClique.certificate_594_part_1 line 661
  340. def OAI.CycleClique.certificate_594_part_2 line 663
  341. def OAI.CycleClique.certificate_594 line 665
  342. theorem OAI.CycleClique.certificate_594_checked line 667
  343. theorem OAI.CycleClique.certificate_594_valid line 668
  344. def OAI.CycleClique.certificate_595_q line 670
  345. def OAI.CycleClique.certificate_595_edges line 671
  346. def OAI.CycleClique.certificate_595_part_0 line 673
  347. def OAI.CycleClique.certificate_595_part_1 line 675
  348. def OAI.CycleClique.certificate_595_part_2 line 677
  349. def OAI.CycleClique.certificate_595 line 679
  350. theorem OAI.CycleClique.certificate_595_checked line 681
  351. theorem OAI.CycleClique.certificate_595_valid line 682
  352. def OAI.CycleClique.certificate_596_q line 684
  353. def OAI.CycleClique.certificate_596_edges line 685
  354. def OAI.CycleClique.certificate_596_part_0 line 687
  355. def OAI.CycleClique.certificate_596_part_1 line 689
  356. def OAI.CycleClique.certificate_596 line 691
  357. theorem OAI.CycleClique.certificate_596_checked line 693
  358. theorem OAI.CycleClique.certificate_596_valid line 694
  359. def OAI.CycleClique.certificate_597_q line 696
  360. def OAI.CycleClique.certificate_597_edges line 697
  361. def OAI.CycleClique.certificate_597_part_0 line 699
  362. def OAI.CycleClique.certificate_597_part_1 line 701
  363. def OAI.CycleClique.certificate_597_part_2 line 703
  364. def OAI.CycleClique.certificate_597 line 705
  365. theorem OAI.CycleClique.certificate_597_checked line 707
  366. theorem OAI.CycleClique.certificate_597_valid line 708
  367. def OAI.CycleClique.certificate_598_q line 710
  368. def OAI.CycleClique.certificate_598_edges line 711
  369. def OAI.CycleClique.certificate_598_part_0 line 713
  370. def OAI.CycleClique.certificate_598_part_1 line 715
  371. def OAI.CycleClique.certificate_598_part_2 line 717
  372. def OAI.CycleClique.certificate_598 line 719
  373. theorem OAI.CycleClique.certificate_598_checked line 721
  374. theorem OAI.CycleClique.certificate_598_valid line 722
  375. def OAI.CycleClique.certificate_599_q line 724
  376. def OAI.CycleClique.certificate_599_edges line 725
  377. def OAI.CycleClique.certificate_599_part_0 line 727
  378. def OAI.CycleClique.certificate_599_part_1 line 729
  379. def OAI.CycleClique.certificate_599_part_2 line 731
  380. def OAI.CycleClique.certificate_599 line 733
  381. theorem OAI.CycleClique.certificate_599_checked line 735
  382. theorem OAI.CycleClique.certificate_599_valid line 736
  383. def OAI.CycleClique.certificate_600_q line 738
  384. def OAI.CycleClique.certificate_600_edges line 739
  385. def OAI.CycleClique.certificate_600_part_0 line 741
  386. def OAI.CycleClique.certificate_600_part_1 line 743
  387. def OAI.CycleClique.certificate_600_part_2 line 745
  388. def OAI.CycleClique.certificate_600 line 747
  389. theorem OAI.CycleClique.certificate_600_checked line 749
  390. theorem OAI.CycleClique.certificate_600_valid line 750
  391. def OAI.CycleClique.certificate_601_q line 752
  392. def OAI.CycleClique.certificate_601_edges line 753
  393. def OAI.CycleClique.certificate_601_part_0 line 755
  394. def OAI.CycleClique.certificate_601_part_1 line 757
  395. def OAI.CycleClique.certificate_601_part_2 line 759
  396. def OAI.CycleClique.certificate_601 line 761
  397. theorem OAI.CycleClique.certificate_601_checked line 763
  398. theorem OAI.CycleClique.certificate_601_valid line 764
  399. def OAI.CycleClique.certificate_602_q line 766
  400. def OAI.CycleClique.certificate_602_edges line 767
  401. def OAI.CycleClique.certificate_602_part_0 line 769
  402. def OAI.CycleClique.certificate_602_part_1 line 771
  403. def OAI.CycleClique.certificate_602 line 773
  404. theorem OAI.CycleClique.certificate_602_checked line 775
  405. theorem OAI.CycleClique.certificate_602_valid line 776
  406. def OAI.CycleClique.certificate_603_q line 778
  407. def OAI.CycleClique.certificate_603_edges line 779
  408. def OAI.CycleClique.certificate_603_part_0 line 781
  409. def OAI.CycleClique.certificate_603_part_1 line 783
  410. def OAI.CycleClique.certificate_603_part_2 line 785
  411. def OAI.CycleClique.certificate_603 line 787
  412. theorem OAI.CycleClique.certificate_603_checked line 789
  413. theorem OAI.CycleClique.certificate_603_valid line 790
  414. def OAI.CycleClique.certificate_604_q line 792
  415. def OAI.CycleClique.certificate_604_edges line 793
  416. def OAI.CycleClique.certificate_604_part_0 line 795
  417. def OAI.CycleClique.certificate_604_part_1 line 797
  418. def OAI.CycleClique.certificate_604_part_2 line 799
  419. def OAI.CycleClique.certificate_604 line 801
  420. theorem OAI.CycleClique.certificate_604_checked line 803
  421. theorem OAI.CycleClique.certificate_604_valid line 804
  422. def OAI.CycleClique.certificate_605_q line 806
  423. def OAI.CycleClique.certificate_605_edges line 807
  424. def OAI.CycleClique.certificate_605_part_0 line 809
  425. def OAI.CycleClique.certificate_605_part_1 line 811
  426. def OAI.CycleClique.certificate_605_part_2 line 813
  427. def OAI.CycleClique.certificate_605 line 815
  428. theorem OAI.CycleClique.certificate_605_checked line 817
  429. theorem OAI.CycleClique.certificate_605_valid line 818
  430. def OAI.CycleClique.certificate_606_q line 820
  431. def OAI.CycleClique.certificate_606_edges line 821
  432. def OAI.CycleClique.certificate_606_part_0 line 823
  433. def OAI.CycleClique.certificate_606_part_1 line 825
  434. def OAI.CycleClique.certificate_606_part_2 line 827
  435. def OAI.CycleClique.certificate_606 line 829
  436. theorem OAI.CycleClique.certificate_606_checked line 831
  437. theorem OAI.CycleClique.certificate_606_valid line 832
  438. def OAI.CycleClique.certificate_607_q line 834
  439. def OAI.CycleClique.certificate_607_edges line 835
  440. def OAI.CycleClique.certificate_607_part_0 line 837
  441. def OAI.CycleClique.certificate_607_part_1 line 839
  442. def OAI.CycleClique.certificate_607_part_2 line 841
  443. def OAI.CycleClique.certificate_607 line 843
  444. theorem OAI.CycleClique.certificate_607_checked line 845
  445. theorem OAI.CycleClique.certificate_607_valid line 846