OAI/Combinatorics/Ramsey/CycleClique/Certificates013.lean

GitHub source file

421 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.certificate_384_q line 20
  2. def OAI.CycleClique.certificate_384_edges line 21
  3. def OAI.CycleClique.certificate_384_part_0 line 23
  4. def OAI.CycleClique.certificate_384_part_1 line 25
  5. def OAI.CycleClique.certificate_384_part_2 line 27
  6. def OAI.CycleClique.certificate_384 line 29
  7. theorem OAI.CycleClique.certificate_384_checked line 31
  8. theorem OAI.CycleClique.certificate_384_valid line 32
  9. def OAI.CycleClique.certificate_385_q line 34
  10. def OAI.CycleClique.certificate_385_edges line 35
  11. def OAI.CycleClique.certificate_385_part_0 line 37
  12. def OAI.CycleClique.certificate_385_part_1 line 39
  13. def OAI.CycleClique.certificate_385_part_2 line 41
  14. def OAI.CycleClique.certificate_385 line 43
  15. theorem OAI.CycleClique.certificate_385_checked line 45
  16. theorem OAI.CycleClique.certificate_385_valid line 46
  17. def OAI.CycleClique.certificate_386_q line 48
  18. def OAI.CycleClique.certificate_386_edges line 49
  19. def OAI.CycleClique.certificate_386_part_0 line 51
  20. def OAI.CycleClique.certificate_386_part_1 line 53
  21. def OAI.CycleClique.certificate_386 line 55
  22. theorem OAI.CycleClique.certificate_386_checked line 57
  23. theorem OAI.CycleClique.certificate_386_valid line 58
  24. def OAI.CycleClique.certificate_387_q line 60
  25. def OAI.CycleClique.certificate_387_edges line 61
  26. def OAI.CycleClique.certificate_387_part_0 line 63
  27. def OAI.CycleClique.certificate_387_part_1 line 65
  28. def OAI.CycleClique.certificate_387_part_2 line 67
  29. def OAI.CycleClique.certificate_387 line 69
  30. theorem OAI.CycleClique.certificate_387_checked line 71
  31. theorem OAI.CycleClique.certificate_387_valid line 72
  32. def OAI.CycleClique.certificate_388_q line 74
  33. def OAI.CycleClique.certificate_388_edges line 75
  34. def OAI.CycleClique.certificate_388_part_0 line 77
  35. def OAI.CycleClique.certificate_388_part_1 line 79
  36. def OAI.CycleClique.certificate_388_part_2 line 81
  37. def OAI.CycleClique.certificate_388 line 83
  38. theorem OAI.CycleClique.certificate_388_checked line 85
  39. theorem OAI.CycleClique.certificate_388_valid line 86
  40. def OAI.CycleClique.certificate_389_q line 88
  41. def OAI.CycleClique.certificate_389_edges line 89
  42. def OAI.CycleClique.certificate_389_part_0 line 91
  43. def OAI.CycleClique.certificate_389_part_1 line 93
  44. def OAI.CycleClique.certificate_389_part_2 line 95
  45. def OAI.CycleClique.certificate_389 line 97
  46. theorem OAI.CycleClique.certificate_389_checked line 99
  47. theorem OAI.CycleClique.certificate_389_valid line 100
  48. def OAI.CycleClique.certificate_390_q line 102
  49. def OAI.CycleClique.certificate_390_edges line 103
  50. def OAI.CycleClique.certificate_390_part_0 line 105
  51. def OAI.CycleClique.certificate_390_part_1 line 107
  52. def OAI.CycleClique.certificate_390_part_2 line 109
  53. def OAI.CycleClique.certificate_390 line 111
  54. theorem OAI.CycleClique.certificate_390_checked line 113
  55. theorem OAI.CycleClique.certificate_390_valid line 114
  56. def OAI.CycleClique.certificate_391_q line 116
  57. def OAI.CycleClique.certificate_391_edges line 117
  58. def OAI.CycleClique.certificate_391_part_0 line 119
  59. def OAI.CycleClique.certificate_391_part_1 line 121
  60. def OAI.CycleClique.certificate_391_part_2 line 123
  61. def OAI.CycleClique.certificate_391 line 125
  62. theorem OAI.CycleClique.certificate_391_checked line 127
  63. theorem OAI.CycleClique.certificate_391_valid line 128
  64. def OAI.CycleClique.certificate_392_q line 130
  65. def OAI.CycleClique.certificate_392_edges line 131
  66. def OAI.CycleClique.certificate_392_part_0 line 133
  67. def OAI.CycleClique.certificate_392_part_1 line 135
  68. def OAI.CycleClique.certificate_392 line 137
  69. theorem OAI.CycleClique.certificate_392_checked line 139
  70. theorem OAI.CycleClique.certificate_392_valid line 140
  71. def OAI.CycleClique.certificate_393_q line 142
  72. def OAI.CycleClique.certificate_393_edges line 143
  73. def OAI.CycleClique.certificate_393_part_0 line 145
  74. def OAI.CycleClique.certificate_393_part_1 line 147
  75. def OAI.CycleClique.certificate_393_part_2 line 149
  76. def OAI.CycleClique.certificate_393 line 151
  77. theorem OAI.CycleClique.certificate_393_checked line 153
  78. theorem OAI.CycleClique.certificate_393_valid line 154
  79. def OAI.CycleClique.certificate_394_q line 156
  80. def OAI.CycleClique.certificate_394_edges line 157
  81. def OAI.CycleClique.certificate_394_part_0 line 159
  82. def OAI.CycleClique.certificate_394_part_1 line 161
  83. def OAI.CycleClique.certificate_394_part_2 line 163
  84. def OAI.CycleClique.certificate_394 line 165
  85. theorem OAI.CycleClique.certificate_394_checked line 167
  86. theorem OAI.CycleClique.certificate_394_valid line 168
  87. def OAI.CycleClique.certificate_395_q line 170
  88. def OAI.CycleClique.certificate_395_edges line 171
  89. def OAI.CycleClique.certificate_395_part_0 line 173
  90. def OAI.CycleClique.certificate_395_part_1 line 175
  91. def OAI.CycleClique.certificate_395_part_2 line 177
  92. def OAI.CycleClique.certificate_395 line 179
  93. theorem OAI.CycleClique.certificate_395_checked line 181
  94. theorem OAI.CycleClique.certificate_395_valid line 182
  95. def OAI.CycleClique.certificate_396_q line 184
  96. def OAI.CycleClique.certificate_396_edges line 185
  97. def OAI.CycleClique.certificate_396_part_0 line 187
  98. def OAI.CycleClique.certificate_396_part_1 line 189
  99. def OAI.CycleClique.certificate_396_part_2 line 191
  100. def OAI.CycleClique.certificate_396 line 193
  101. theorem OAI.CycleClique.certificate_396_checked line 195
  102. theorem OAI.CycleClique.certificate_396_valid line 196
  103. def OAI.CycleClique.certificate_397_q line 198
  104. def OAI.CycleClique.certificate_397_edges line 199
  105. def OAI.CycleClique.certificate_397_part_0 line 201
  106. def OAI.CycleClique.certificate_397_part_1 line 203
  107. def OAI.CycleClique.certificate_397_part_2 line 205
  108. def OAI.CycleClique.certificate_397 line 207
  109. theorem OAI.CycleClique.certificate_397_checked line 209
  110. theorem OAI.CycleClique.certificate_397_valid line 210
  111. def OAI.CycleClique.certificate_398_q line 212
  112. def OAI.CycleClique.certificate_398_edges line 214
  113. def OAI.CycleClique.certificate_398_E line 216
  114. def OAI.CycleClique.certificate_398_M line 218
  115. def OAI.CycleClique.certificate_398_part_1_E line 220
  116. def OAI.CycleClique.certificate_398_part_1_M line 222
  117. def OAI.CycleClique.certificate_398_part_2_E line 224
  118. def OAI.CycleClique.certificate_398_part_2_M line 226
  119. def OAI.CycleClique.certificate_398_part_3_E line 228
  120. def OAI.CycleClique.certificate_398_part_3_M line 230
  121. def OAI.CycleClique.certificate_398_part_4_E line 232
  122. def OAI.CycleClique.certificate_398_part_4_M line 234
  123. def OAI.CycleClique.certificate_398_part_5_E line 236
  124. def OAI.CycleClique.certificate_398_part_5_M line 238
  125. def OAI.CycleClique.certificate_398_part_6_E line 240
  126. def OAI.CycleClique.certificate_398_part_6_M line 242
  127. def OAI.CycleClique.certificate_398_part_7_E line 244
  128. def OAI.CycleClique.certificate_398_part_7_M line 246
  129. def OAI.CycleClique.certificate_398_part_8_E line 248
  130. def OAI.CycleClique.certificate_398_part_8_M line 250
  131. def OAI.CycleClique.certificate_398_part_8 line 252
  132. theorem OAI.CycleClique.certificate_398_part_8_checked line 254
  133. def OAI.CycleClique.certificate_398_part_9_E line 256
  134. def OAI.CycleClique.certificate_398_part_9_M line 258
  135. def OAI.CycleClique.certificate_398_part_10_E line 260
  136. def OAI.CycleClique.certificate_398_part_10_M line 262
  137. def OAI.CycleClique.certificate_398_part_11_E line 264
  138. def OAI.CycleClique.certificate_398_part_11_M line 266
  139. def OAI.CycleClique.certificate_398_part_12_E line 268
  140. def OAI.CycleClique.certificate_398_part_12_M line 270
  141. def OAI.CycleClique.certificate_398_part_13_E line 272
  142. def OAI.CycleClique.certificate_398_part_13_M line 274
  143. def OAI.CycleClique.certificate_398_part_14_E line 276
  144. def OAI.CycleClique.certificate_398_part_14_M line 278
  145. def OAI.CycleClique.certificate_398_part_14 line 280
  146. theorem OAI.CycleClique.certificate_398_part_14_checked line 282
  147. def OAI.CycleClique.certificate_398_part_15_E line 284
  148. def OAI.CycleClique.certificate_398_part_15_M line 286
  149. def OAI.CycleClique.certificate_398_part_16_E line 288
  150. def OAI.CycleClique.certificate_398_part_16_M line 290
  151. def OAI.CycleClique.certificate_398_part_17_E line 292
  152. def OAI.CycleClique.certificate_398_part_17_M line 294
  153. def OAI.CycleClique.certificate_398_part_18_E line 296
  154. def OAI.CycleClique.certificate_398_part_18_M line 298
  155. def OAI.CycleClique.certificate_398_part_19_E line 300
  156. def OAI.CycleClique.certificate_398_part_19_M line 302
  157. def OAI.CycleClique.certificate_398_part_19 line 304
  158. theorem OAI.CycleClique.certificate_398_part_19_checked line 306
  159. def OAI.CycleClique.certificate_398_part_20_E line 308
  160. def OAI.CycleClique.certificate_398_part_20_M line 310
  161. def OAI.CycleClique.certificate_398_part_21_E line 312
  162. def OAI.CycleClique.certificate_398_part_21_M line 314
  163. def OAI.CycleClique.certificate_398_part_21 line 316
  164. theorem OAI.CycleClique.certificate_398_part_21_checked line 318
  165. def OAI.CycleClique.certificate_398_part_20 line 320
  166. theorem OAI.CycleClique.certificate_398_part_20_checked line 322
  167. def OAI.CycleClique.certificate_398_part_22_E line 324
  168. def OAI.CycleClique.certificate_398_part_22_M line 326
  169. def OAI.CycleClique.certificate_398_part_23_E line 328
  170. def OAI.CycleClique.certificate_398_part_23_M line 330
  171. def OAI.CycleClique.certificate_398_part_24_E line 332
  172. def OAI.CycleClique.certificate_398_part_24_M line 334
  173. def OAI.CycleClique.certificate_398_part_24 line 336
  174. theorem OAI.CycleClique.certificate_398_part_24_checked line 338
  175. def OAI.CycleClique.certificate_398_part_25_E line 340
  176. def OAI.CycleClique.certificate_398_part_25_M line 342
  177. def OAI.CycleClique.certificate_398_part_25 line 344
  178. theorem OAI.CycleClique.certificate_398_part_25_checked line 346
  179. def OAI.CycleClique.certificate_398_part_26_E line 348
  180. def OAI.CycleClique.certificate_398_part_26_M line 350
  181. def OAI.CycleClique.certificate_398_part_26 line 352
  182. theorem OAI.CycleClique.certificate_398_part_26_checked line 354
  183. def OAI.CycleClique.certificate_398_part_27_E line 356
  184. def OAI.CycleClique.certificate_398_part_27_M line 358
  185. def OAI.CycleClique.certificate_398_part_28_E line 360
  186. def OAI.CycleClique.certificate_398_part_28_M line 362
  187. def OAI.CycleClique.certificate_398_part_28 line 364
  188. theorem OAI.CycleClique.certificate_398_part_28_checked line 366
  189. def OAI.CycleClique.certificate_398_part_27 line 368
  190. theorem OAI.CycleClique.certificate_398_part_27_checked line 370
  191. def OAI.CycleClique.certificate_398_part_29_E line 372
  192. def OAI.CycleClique.certificate_398_part_29_M line 374
  193. def OAI.CycleClique.certificate_398_part_30_E line 376
  194. def OAI.CycleClique.certificate_398_part_30_M line 378
  195. def OAI.CycleClique.certificate_398_part_31_E line 380
  196. def OAI.CycleClique.certificate_398_part_31_M line 382
  197. def OAI.CycleClique.certificate_398_part_32_E line 384
  198. def OAI.CycleClique.certificate_398_part_32_M line 386
  199. def OAI.CycleClique.certificate_398_part_33_E line 388
  200. def OAI.CycleClique.certificate_398_part_33_M line 390
  201. def OAI.CycleClique.certificate_398_part_33 line 392
  202. theorem OAI.CycleClique.certificate_398_part_33_checked line 394
  203. def OAI.CycleClique.certificate_398_part_32 line 396
  204. theorem OAI.CycleClique.certificate_398_part_32_checked line 398
  205. def OAI.CycleClique.certificate_398_part_31 line 400
  206. theorem OAI.CycleClique.certificate_398_part_31_checked line 402
  207. def OAI.CycleClique.certificate_398_part_34_E line 404
  208. def OAI.CycleClique.certificate_398_part_34_M line 406
  209. def OAI.CycleClique.certificate_398_part_34 line 408
  210. theorem OAI.CycleClique.certificate_398_part_34_checked line 410
  211. def OAI.CycleClique.certificate_398_part_35_E line 412
  212. def OAI.CycleClique.certificate_398_part_35_M line 414
  213. def OAI.CycleClique.certificate_398_part_36_E line 416
  214. def OAI.CycleClique.certificate_398_part_36_M line 418
  215. def OAI.CycleClique.certificate_398_part_36 line 420
  216. theorem OAI.CycleClique.certificate_398_part_36_checked line 422
  217. def OAI.CycleClique.certificate_398_part_37_E line 424
  218. def OAI.CycleClique.certificate_398_part_37_M line 426
  219. def OAI.CycleClique.certificate_398_part_37 line 428
  220. theorem OAI.CycleClique.certificate_398_part_37_checked line 430
  221. def OAI.CycleClique.certificate_398_part_38_E line 432
  222. def OAI.CycleClique.certificate_398_part_38_M line 434
  223. def OAI.CycleClique.certificate_398_part_38 line 436
  224. theorem OAI.CycleClique.certificate_398_part_38_checked line 438
  225. def OAI.CycleClique.certificate_398_part_39_E line 440
  226. def OAI.CycleClique.certificate_398_part_39_M line 442
  227. def OAI.CycleClique.certificate_398_part_39 line 444
  228. theorem OAI.CycleClique.certificate_398_part_39_checked line 446
  229. def OAI.CycleClique.certificate_398_part_40_E line 448
  230. def OAI.CycleClique.certificate_398_part_40_M line 450
  231. def OAI.CycleClique.certificate_398_part_41_E line 452
  232. def OAI.CycleClique.certificate_398_part_41_M line 454
  233. def OAI.CycleClique.certificate_398_part_42_E line 456
  234. def OAI.CycleClique.certificate_398_part_42_M line 458
  235. def OAI.CycleClique.certificate_398_part_43_E line 460
  236. def OAI.CycleClique.certificate_398_part_43_M line 462
  237. def OAI.CycleClique.certificate_398_part_43 line 464
  238. theorem OAI.CycleClique.certificate_398_part_43_checked line 466
  239. def OAI.CycleClique.certificate_398_part_42 line 468
  240. theorem OAI.CycleClique.certificate_398_part_42_checked line 470
  241. def OAI.CycleClique.certificate_398_part_41 line 472
  242. theorem OAI.CycleClique.certificate_398_part_41_checked line 474
  243. def OAI.CycleClique.certificate_398_part_40 line 476
  244. theorem OAI.CycleClique.certificate_398_part_40_checked line 478
  245. def OAI.CycleClique.certificate_398_part_35 line 480
  246. theorem OAI.CycleClique.certificate_398_part_35_checked line 482
  247. def OAI.CycleClique.certificate_398_part_30 line 484
  248. theorem OAI.CycleClique.certificate_398_part_30_checked line 486
  249. def OAI.CycleClique.certificate_398_part_29 line 488
  250. theorem OAI.CycleClique.certificate_398_part_29_checked line 490
  251. def OAI.CycleClique.certificate_398_part_23 line 492
  252. theorem OAI.CycleClique.certificate_398_part_23_checked line 494
  253. def OAI.CycleClique.certificate_398_part_22 line 496
  254. theorem OAI.CycleClique.certificate_398_part_22_checked line 498
  255. def OAI.CycleClique.certificate_398_part_18 line 500
  256. theorem OAI.CycleClique.certificate_398_part_18_checked line 502
  257. def OAI.CycleClique.certificate_398_part_17 line 504
  258. theorem OAI.CycleClique.certificate_398_part_17_checked line 506
  259. def OAI.CycleClique.certificate_398_part_16 line 508
  260. theorem OAI.CycleClique.certificate_398_part_16_checked line 510
  261. def OAI.CycleClique.certificate_398_part_15 line 512
  262. theorem OAI.CycleClique.certificate_398_part_15_checked line 514
  263. def OAI.CycleClique.certificate_398_part_13 line 516
  264. theorem OAI.CycleClique.certificate_398_part_13_checked line 518
  265. def OAI.CycleClique.certificate_398_part_12 line 520
  266. theorem OAI.CycleClique.certificate_398_part_12_checked line 522
  267. def OAI.CycleClique.certificate_398_part_11 line 524
  268. theorem OAI.CycleClique.certificate_398_part_11_checked line 526
  269. def OAI.CycleClique.certificate_398_part_10 line 528
  270. theorem OAI.CycleClique.certificate_398_part_10_checked line 530
  271. def OAI.CycleClique.certificate_398_part_9 line 532
  272. theorem OAI.CycleClique.certificate_398_part_9_checked line 534
  273. def OAI.CycleClique.certificate_398_part_7 line 536
  274. theorem OAI.CycleClique.certificate_398_part_7_checked line 538
  275. def OAI.CycleClique.certificate_398_part_6 line 540
  276. theorem OAI.CycleClique.certificate_398_part_6_checked line 542
  277. def OAI.CycleClique.certificate_398_part_5 line 544
  278. theorem OAI.CycleClique.certificate_398_part_5_checked line 546
  279. def OAI.CycleClique.certificate_398_part_4 line 548
  280. theorem OAI.CycleClique.certificate_398_part_4_checked line 550
  281. def OAI.CycleClique.certificate_398_part_3 line 552
  282. theorem OAI.CycleClique.certificate_398_part_3_checked line 554
  283. def OAI.CycleClique.certificate_398_part_2 line 556
  284. theorem OAI.CycleClique.certificate_398_part_2_checked line 558
  285. def OAI.CycleClique.certificate_398_part_1 line 560
  286. theorem OAI.CycleClique.certificate_398_part_1_checked line 562
  287. def OAI.CycleClique.certificate_398 line 564
  288. theorem OAI.CycleClique.certificate_398_checked line 566
  289. theorem OAI.CycleClique.certificate_398_valid line 568
  290. def OAI.CycleClique.certificate_399_q line 570
  291. def OAI.CycleClique.certificate_399_edges line 571
  292. def OAI.CycleClique.certificate_399_part_0 line 573
  293. def OAI.CycleClique.certificate_399_part_1 line 575
  294. def OAI.CycleClique.certificate_399 line 577
  295. theorem OAI.CycleClique.certificate_399_checked line 579
  296. theorem OAI.CycleClique.certificate_399_valid line 580
  297. def OAI.CycleClique.certificate_400_q line 582
  298. def OAI.CycleClique.certificate_400_edges line 583
  299. def OAI.CycleClique.certificate_400_part_0 line 585
  300. def OAI.CycleClique.certificate_400_part_1 line 587
  301. def OAI.CycleClique.certificate_400 line 589
  302. theorem OAI.CycleClique.certificate_400_checked line 591
  303. theorem OAI.CycleClique.certificate_400_valid line 592
  304. def OAI.CycleClique.certificate_401_q line 594
  305. def OAI.CycleClique.certificate_401_edges line 595
  306. def OAI.CycleClique.certificate_401_part_0 line 597
  307. def OAI.CycleClique.certificate_401_part_1 line 599
  308. def OAI.CycleClique.certificate_401_part_2 line 601
  309. def OAI.CycleClique.certificate_401 line 603
  310. theorem OAI.CycleClique.certificate_401_checked line 605
  311. theorem OAI.CycleClique.certificate_401_valid line 606
  312. def OAI.CycleClique.certificate_402_q line 608
  313. def OAI.CycleClique.certificate_402_edges line 609
  314. def OAI.CycleClique.certificate_402_part_0 line 611
  315. def OAI.CycleClique.certificate_402_part_1 line 613
  316. def OAI.CycleClique.certificate_402_part_2 line 615
  317. def OAI.CycleClique.certificate_402 line 617
  318. theorem OAI.CycleClique.certificate_402_checked line 619
  319. theorem OAI.CycleClique.certificate_402_valid line 620
  320. def OAI.CycleClique.certificate_403_q line 622
  321. def OAI.CycleClique.certificate_403_edges line 623
  322. def OAI.CycleClique.certificate_403_part_0 line 625
  323. def OAI.CycleClique.certificate_403_part_1 line 627
  324. def OAI.CycleClique.certificate_403_part_2 line 629
  325. def OAI.CycleClique.certificate_403 line 631
  326. theorem OAI.CycleClique.certificate_403_checked line 633
  327. theorem OAI.CycleClique.certificate_403_valid line 634
  328. def OAI.CycleClique.certificate_404_q line 636
  329. def OAI.CycleClique.certificate_404_edges line 637
  330. def OAI.CycleClique.certificate_404_part_0 line 639
  331. def OAI.CycleClique.certificate_404_part_1 line 641
  332. def OAI.CycleClique.certificate_404_part_2 line 643
  333. def OAI.CycleClique.certificate_404 line 645
  334. theorem OAI.CycleClique.certificate_404_checked line 647
  335. theorem OAI.CycleClique.certificate_404_valid line 648
  336. def OAI.CycleClique.certificate_405_q line 650
  337. def OAI.CycleClique.certificate_405_edges line 651
  338. def OAI.CycleClique.certificate_405_part_0 line 653
  339. def OAI.CycleClique.certificate_405_part_1 line 655
  340. def OAI.CycleClique.certificate_405 line 657
  341. theorem OAI.CycleClique.certificate_405_checked line 659
  342. theorem OAI.CycleClique.certificate_405_valid line 660
  343. def OAI.CycleClique.certificate_406_q line 662
  344. def OAI.CycleClique.certificate_406_edges line 663
  345. def OAI.CycleClique.certificate_406_part_0 line 665
  346. def OAI.CycleClique.certificate_406_part_1 line 667
  347. def OAI.CycleClique.certificate_406_part_2 line 669
  348. def OAI.CycleClique.certificate_406 line 671
  349. theorem OAI.CycleClique.certificate_406_checked line 673
  350. theorem OAI.CycleClique.certificate_406_valid line 674
  351. def OAI.CycleClique.certificate_407_q line 676
  352. def OAI.CycleClique.certificate_407_edges line 677
  353. def OAI.CycleClique.certificate_407_part_0 line 679
  354. def OAI.CycleClique.certificate_407_part_1 line 681
  355. def OAI.CycleClique.certificate_407_part_2 line 683
  356. def OAI.CycleClique.certificate_407 line 685
  357. theorem OAI.CycleClique.certificate_407_checked line 687
  358. theorem OAI.CycleClique.certificate_407_valid line 688
  359. def OAI.CycleClique.certificate_408_q line 690
  360. def OAI.CycleClique.certificate_408_edges line 691
  361. def OAI.CycleClique.certificate_408_part_0 line 693
  362. def OAI.CycleClique.certificate_408_part_1 line 695
  363. def OAI.CycleClique.certificate_408 line 697
  364. theorem OAI.CycleClique.certificate_408_checked line 699
  365. theorem OAI.CycleClique.certificate_408_valid line 700
  366. def OAI.CycleClique.certificate_409_q line 702
  367. def OAI.CycleClique.certificate_409_edges line 703
  368. def OAI.CycleClique.certificate_409_part_0 line 705
  369. def OAI.CycleClique.certificate_409_part_1 line 707
  370. def OAI.CycleClique.certificate_409_part_2 line 709
  371. def OAI.CycleClique.certificate_409 line 711
  372. theorem OAI.CycleClique.certificate_409_checked line 713
  373. theorem OAI.CycleClique.certificate_409_valid line 714
  374. def OAI.CycleClique.certificate_410_q line 716
  375. def OAI.CycleClique.certificate_410_edges line 717
  376. def OAI.CycleClique.certificate_410_part_0 line 719
  377. def OAI.CycleClique.certificate_410_part_1 line 721
  378. def OAI.CycleClique.certificate_410_part_2 line 723
  379. def OAI.CycleClique.certificate_410 line 725
  380. theorem OAI.CycleClique.certificate_410_checked line 727
  381. theorem OAI.CycleClique.certificate_410_valid line 728
  382. def OAI.CycleClique.certificate_411_q line 730
  383. def OAI.CycleClique.certificate_411_edges line 731
  384. def OAI.CycleClique.certificate_411_part_0 line 733
  385. def OAI.CycleClique.certificate_411_part_1 line 735
  386. def OAI.CycleClique.certificate_411_part_2 line 737
  387. def OAI.CycleClique.certificate_411 line 739
  388. theorem OAI.CycleClique.certificate_411_checked line 741
  389. theorem OAI.CycleClique.certificate_411_valid line 742
  390. def OAI.CycleClique.certificate_412_q line 744
  391. def OAI.CycleClique.certificate_412_edges line 745
  392. def OAI.CycleClique.certificate_412_part_0 line 747
  393. def OAI.CycleClique.certificate_412_part_1 line 749
  394. def OAI.CycleClique.certificate_412_part_2 line 751
  395. def OAI.CycleClique.certificate_412 line 753
  396. theorem OAI.CycleClique.certificate_412_checked line 755
  397. theorem OAI.CycleClique.certificate_412_valid line 756
  398. def OAI.CycleClique.certificate_413_q line 758
  399. def OAI.CycleClique.certificate_413_edges line 759
  400. def OAI.CycleClique.certificate_413_part_0 line 761
  401. def OAI.CycleClique.certificate_413_part_1 line 763
  402. def OAI.CycleClique.certificate_413_part_2 line 765
  403. def OAI.CycleClique.certificate_413 line 767
  404. theorem OAI.CycleClique.certificate_413_checked line 769
  405. theorem OAI.CycleClique.certificate_413_valid line 770
  406. def OAI.CycleClique.certificate_414_q line 772
  407. def OAI.CycleClique.certificate_414_edges line 773
  408. def OAI.CycleClique.certificate_414_part_0 line 775
  409. def OAI.CycleClique.certificate_414_part_1 line 777
  410. def OAI.CycleClique.certificate_414_part_2 line 779
  411. def OAI.CycleClique.certificate_414 line 781
  412. theorem OAI.CycleClique.certificate_414_checked line 783
  413. theorem OAI.CycleClique.certificate_414_valid line 784
  414. def OAI.CycleClique.certificate_415_q line 786
  415. def OAI.CycleClique.certificate_415_edges line 787
  416. def OAI.CycleClique.certificate_415_part_0 line 789
  417. def OAI.CycleClique.certificate_415_part_1 line 791
  418. def OAI.CycleClique.certificate_415_part_2 line 793
  419. def OAI.CycleClique.certificate_415 line 795
  420. theorem OAI.CycleClique.certificate_415_checked line 797
  421. theorem OAI.CycleClique.certificate_415_valid line 798