OAI/Combinatorics/Ramsey/CycleClique/Certificates012.lean

GitHub source file

691 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.certificate_352_q line 20
  2. def OAI.CycleClique.certificate_352_edges line 21
  3. def OAI.CycleClique.certificate_352_part_0 line 23
  4. def OAI.CycleClique.certificate_352_part_1 line 25
  5. def OAI.CycleClique.certificate_352 line 27
  6. theorem OAI.CycleClique.certificate_352_checked line 29
  7. theorem OAI.CycleClique.certificate_352_valid line 30
  8. def OAI.CycleClique.certificate_353_q line 32
  9. def OAI.CycleClique.certificate_353_edges line 33
  10. def OAI.CycleClique.certificate_353_part_0 line 35
  11. def OAI.CycleClique.certificate_353_part_1 line 37
  12. def OAI.CycleClique.certificate_353_part_2 line 39
  13. def OAI.CycleClique.certificate_353 line 41
  14. theorem OAI.CycleClique.certificate_353_checked line 43
  15. theorem OAI.CycleClique.certificate_353_valid line 44
  16. def OAI.CycleClique.certificate_354_q line 46
  17. def OAI.CycleClique.certificate_354_edges line 47
  18. def OAI.CycleClique.certificate_354_part_0 line 49
  19. def OAI.CycleClique.certificate_354_part_1 line 51
  20. def OAI.CycleClique.certificate_354 line 53
  21. theorem OAI.CycleClique.certificate_354_checked line 55
  22. theorem OAI.CycleClique.certificate_354_valid line 56
  23. def OAI.CycleClique.certificate_355_q line 58
  24. def OAI.CycleClique.certificate_355_edges line 59
  25. def OAI.CycleClique.certificate_355_part_0 line 61
  26. def OAI.CycleClique.certificate_355_part_1 line 63
  27. def OAI.CycleClique.certificate_355_part_2 line 65
  28. def OAI.CycleClique.certificate_355 line 67
  29. theorem OAI.CycleClique.certificate_355_checked line 69
  30. theorem OAI.CycleClique.certificate_355_valid line 70
  31. def OAI.CycleClique.certificate_356_q line 72
  32. def OAI.CycleClique.certificate_356_edges line 73
  33. def OAI.CycleClique.certificate_356_part_0 line 75
  34. def OAI.CycleClique.certificate_356_part_1 line 77
  35. def OAI.CycleClique.certificate_356 line 79
  36. theorem OAI.CycleClique.certificate_356_checked line 81
  37. theorem OAI.CycleClique.certificate_356_valid line 82
  38. def OAI.CycleClique.certificate_357_q line 84
  39. def OAI.CycleClique.certificate_357_edges line 85
  40. def OAI.CycleClique.certificate_357_part_0 line 87
  41. def OAI.CycleClique.certificate_357_part_1 line 89
  42. def OAI.CycleClique.certificate_357_part_2 line 91
  43. def OAI.CycleClique.certificate_357 line 93
  44. theorem OAI.CycleClique.certificate_357_checked line 95
  45. theorem OAI.CycleClique.certificate_357_valid line 96
  46. def OAI.CycleClique.certificate_358_q line 98
  47. def OAI.CycleClique.certificate_358_edges line 99
  48. def OAI.CycleClique.certificate_358_part_0 line 101
  49. def OAI.CycleClique.certificate_358_part_1 line 103
  50. def OAI.CycleClique.certificate_358_part_2 line 105
  51. def OAI.CycleClique.certificate_358 line 107
  52. theorem OAI.CycleClique.certificate_358_checked line 109
  53. theorem OAI.CycleClique.certificate_358_valid line 110
  54. def OAI.CycleClique.certificate_359_q line 112
  55. def OAI.CycleClique.certificate_359_edges line 113
  56. def OAI.CycleClique.certificate_359_part_0 line 115
  57. def OAI.CycleClique.certificate_359_part_1 line 117
  58. def OAI.CycleClique.certificate_359_part_2 line 119
  59. def OAI.CycleClique.certificate_359 line 121
  60. theorem OAI.CycleClique.certificate_359_checked line 123
  61. theorem OAI.CycleClique.certificate_359_valid line 124
  62. def OAI.CycleClique.certificate_360_q line 126
  63. def OAI.CycleClique.certificate_360_edges line 127
  64. def OAI.CycleClique.certificate_360_part_0 line 129
  65. def OAI.CycleClique.certificate_360_part_1 line 131
  66. def OAI.CycleClique.certificate_360_part_2 line 133
  67. def OAI.CycleClique.certificate_360 line 135
  68. theorem OAI.CycleClique.certificate_360_checked line 137
  69. theorem OAI.CycleClique.certificate_360_valid line 138
  70. def OAI.CycleClique.certificate_361_q line 140
  71. def OAI.CycleClique.certificate_361_edges line 141
  72. def OAI.CycleClique.certificate_361_part_0 line 143
  73. def OAI.CycleClique.certificate_361 line 145
  74. theorem OAI.CycleClique.certificate_361_checked line 147
  75. theorem OAI.CycleClique.certificate_361_valid line 148
  76. def OAI.CycleClique.certificate_362_q line 150
  77. def OAI.CycleClique.certificate_362_edges line 151
  78. def OAI.CycleClique.certificate_362_part_0 line 153
  79. def OAI.CycleClique.certificate_362 line 155
  80. theorem OAI.CycleClique.certificate_362_checked line 157
  81. theorem OAI.CycleClique.certificate_362_valid line 158
  82. def OAI.CycleClique.certificate_363_q line 160
  83. def OAI.CycleClique.certificate_363_edges line 161
  84. def OAI.CycleClique.certificate_363_part_0 line 163
  85. def OAI.CycleClique.certificate_363_part_1 line 165
  86. def OAI.CycleClique.certificate_363 line 167
  87. theorem OAI.CycleClique.certificate_363_checked line 169
  88. theorem OAI.CycleClique.certificate_363_valid line 170
  89. def OAI.CycleClique.certificate_364_q line 172
  90. def OAI.CycleClique.certificate_364_edges line 173
  91. def OAI.CycleClique.certificate_364_part_0 line 175
  92. def OAI.CycleClique.certificate_364_part_1 line 177
  93. def OAI.CycleClique.certificate_364 line 179
  94. theorem OAI.CycleClique.certificate_364_checked line 181
  95. theorem OAI.CycleClique.certificate_364_valid line 182
  96. def OAI.CycleClique.certificate_365_q line 184
  97. def OAI.CycleClique.certificate_365_edges line 185
  98. def OAI.CycleClique.certificate_365_part_0 line 187
  99. def OAI.CycleClique.certificate_365_part_1 line 189
  100. def OAI.CycleClique.certificate_365 line 191
  101. theorem OAI.CycleClique.certificate_365_checked line 193
  102. theorem OAI.CycleClique.certificate_365_valid line 194
  103. def OAI.CycleClique.certificate_366_q line 196
  104. def OAI.CycleClique.certificate_366_edges line 197
  105. def OAI.CycleClique.certificate_366_part_0 line 199
  106. def OAI.CycleClique.certificate_366_part_1 line 201
  107. def OAI.CycleClique.certificate_366_part_2 line 203
  108. def OAI.CycleClique.certificate_366 line 205
  109. theorem OAI.CycleClique.certificate_366_checked line 207
  110. theorem OAI.CycleClique.certificate_366_valid line 208
  111. def OAI.CycleClique.certificate_367_q line 210
  112. def OAI.CycleClique.certificate_367_edges line 212
  113. def OAI.CycleClique.certificate_367_E line 214
  114. def OAI.CycleClique.certificate_367_M line 216
  115. def OAI.CycleClique.certificate_367_part_1_E line 218
  116. def OAI.CycleClique.certificate_367_part_1_M line 220
  117. def OAI.CycleClique.certificate_367_part_2_E line 222
  118. def OAI.CycleClique.certificate_367_part_2_M line 224
  119. def OAI.CycleClique.certificate_367_part_3_E line 226
  120. def OAI.CycleClique.certificate_367_part_3_M line 228
  121. def OAI.CycleClique.certificate_367_part_4_E line 230
  122. def OAI.CycleClique.certificate_367_part_4_M line 232
  123. def OAI.CycleClique.certificate_367_part_5_E line 234
  124. def OAI.CycleClique.certificate_367_part_5_M line 236
  125. def OAI.CycleClique.certificate_367_part_6_E line 238
  126. def OAI.CycleClique.certificate_367_part_6_M line 240
  127. def OAI.CycleClique.certificate_367_part_7_E line 242
  128. def OAI.CycleClique.certificate_367_part_7_M line 244
  129. def OAI.CycleClique.certificate_367_part_8_E line 246
  130. def OAI.CycleClique.certificate_367_part_8_M line 248
  131. def OAI.CycleClique.certificate_367_part_9_E line 250
  132. def OAI.CycleClique.certificate_367_part_9_M line 252
  133. def OAI.CycleClique.certificate_367_part_9 line 254
  134. theorem OAI.CycleClique.certificate_367_part_9_checked line 256
  135. def OAI.CycleClique.certificate_367_part_10_E line 258
  136. def OAI.CycleClique.certificate_367_part_10_M line 260
  137. def OAI.CycleClique.certificate_367_part_11_E line 262
  138. def OAI.CycleClique.certificate_367_part_11_M line 264
  139. def OAI.CycleClique.certificate_367_part_12_E line 266
  140. def OAI.CycleClique.certificate_367_part_12_M line 268
  141. def OAI.CycleClique.certificate_367_part_13_E line 270
  142. def OAI.CycleClique.certificate_367_part_13_M line 272
  143. def OAI.CycleClique.certificate_367_part_13 line 274
  144. theorem OAI.CycleClique.certificate_367_part_13_checked line 276
  145. def OAI.CycleClique.certificate_367_part_12 line 278
  146. theorem OAI.CycleClique.certificate_367_part_12_checked line 280
  147. def OAI.CycleClique.certificate_367_part_11 line 282
  148. theorem OAI.CycleClique.certificate_367_part_11_checked line 284
  149. def OAI.CycleClique.certificate_367_part_14_E line 286
  150. def OAI.CycleClique.certificate_367_part_14_M line 288
  151. def OAI.CycleClique.certificate_367_part_15_E line 290
  152. def OAI.CycleClique.certificate_367_part_15_M line 292
  153. def OAI.CycleClique.certificate_367_part_16_E line 294
  154. def OAI.CycleClique.certificate_367_part_16_M line 296
  155. def OAI.CycleClique.certificate_367_part_17_E line 298
  156. def OAI.CycleClique.certificate_367_part_17_M line 300
  157. def OAI.CycleClique.certificate_367_part_17 line 302
  158. theorem OAI.CycleClique.certificate_367_part_17_checked line 304
  159. def OAI.CycleClique.certificate_367_part_16 line 306
  160. theorem OAI.CycleClique.certificate_367_part_16_checked line 308
  161. def OAI.CycleClique.certificate_367_part_15 line 310
  162. theorem OAI.CycleClique.certificate_367_part_15_checked line 312
  163. def OAI.CycleClique.certificate_367_part_14 line 314
  164. theorem OAI.CycleClique.certificate_367_part_14_checked line 316
  165. def OAI.CycleClique.certificate_367_part_18_E line 318
  166. def OAI.CycleClique.certificate_367_part_18_M line 320
  167. def OAI.CycleClique.certificate_367_part_19_E line 322
  168. def OAI.CycleClique.certificate_367_part_19_M line 324
  169. def OAI.CycleClique.certificate_367_part_20_E line 326
  170. def OAI.CycleClique.certificate_367_part_20_M line 328
  171. def OAI.CycleClique.certificate_367_part_21_E line 330
  172. def OAI.CycleClique.certificate_367_part_21_M line 332
  173. def OAI.CycleClique.certificate_367_part_22_E line 334
  174. def OAI.CycleClique.certificate_367_part_22_M line 336
  175. def OAI.CycleClique.certificate_367_part_22 line 338
  176. theorem OAI.CycleClique.certificate_367_part_22_checked line 340
  177. def OAI.CycleClique.certificate_367_part_21 line 342
  178. theorem OAI.CycleClique.certificate_367_part_21_checked line 344
  179. def OAI.CycleClique.certificate_367_part_20 line 346
  180. theorem OAI.CycleClique.certificate_367_part_20_checked line 348
  181. def OAI.CycleClique.certificate_367_part_19 line 350
  182. theorem OAI.CycleClique.certificate_367_part_19_checked line 352
  183. def OAI.CycleClique.certificate_367_part_23_E line 354
  184. def OAI.CycleClique.certificate_367_part_23_M line 356
  185. def OAI.CycleClique.certificate_367_part_24_E line 358
  186. def OAI.CycleClique.certificate_367_part_24_M line 360
  187. def OAI.CycleClique.certificate_367_part_25_E line 362
  188. def OAI.CycleClique.certificate_367_part_25_M line 364
  189. def OAI.CycleClique.certificate_367_part_26_E line 366
  190. def OAI.CycleClique.certificate_367_part_26_M line 368
  191. def OAI.CycleClique.certificate_367_part_26 line 370
  192. theorem OAI.CycleClique.certificate_367_part_26_checked line 372
  193. def OAI.CycleClique.certificate_367_part_25 line 374
  194. theorem OAI.CycleClique.certificate_367_part_25_checked line 376
  195. def OAI.CycleClique.certificate_367_part_24 line 378
  196. theorem OAI.CycleClique.certificate_367_part_24_checked line 380
  197. def OAI.CycleClique.certificate_367_part_23 line 382
  198. theorem OAI.CycleClique.certificate_367_part_23_checked line 384
  199. def OAI.CycleClique.certificate_367_part_27_E line 386
  200. def OAI.CycleClique.certificate_367_part_27_M line 388
  201. def OAI.CycleClique.certificate_367_part_28_E line 390
  202. def OAI.CycleClique.certificate_367_part_28_M line 392
  203. def OAI.CycleClique.certificate_367_part_29_E line 394
  204. def OAI.CycleClique.certificate_367_part_29_M line 396
  205. def OAI.CycleClique.certificate_367_part_30_E line 398
  206. def OAI.CycleClique.certificate_367_part_30_M line 400
  207. def OAI.CycleClique.certificate_367_part_30 line 402
  208. theorem OAI.CycleClique.certificate_367_part_30_checked line 404
  209. def OAI.CycleClique.certificate_367_part_29 line 406
  210. theorem OAI.CycleClique.certificate_367_part_29_checked line 408
  211. def OAI.CycleClique.certificate_367_part_28 line 410
  212. theorem OAI.CycleClique.certificate_367_part_28_checked line 412
  213. def OAI.CycleClique.certificate_367_part_27 line 414
  214. theorem OAI.CycleClique.certificate_367_part_27_checked line 416
  215. def OAI.CycleClique.certificate_367_part_31_E line 418
  216. def OAI.CycleClique.certificate_367_part_31_M line 420
  217. def OAI.CycleClique.certificate_367_part_31 line 422
  218. theorem OAI.CycleClique.certificate_367_part_31_checked line 424
  219. def OAI.CycleClique.certificate_367_part_32_E line 426
  220. def OAI.CycleClique.certificate_367_part_32_M line 428
  221. def OAI.CycleClique.certificate_367_part_33_E line 430
  222. def OAI.CycleClique.certificate_367_part_33_M line 432
  223. def OAI.CycleClique.certificate_367_part_34_E line 434
  224. def OAI.CycleClique.certificate_367_part_34_M line 436
  225. def OAI.CycleClique.certificate_367_part_34 line 438
  226. theorem OAI.CycleClique.certificate_367_part_34_checked line 440
  227. def OAI.CycleClique.certificate_367_part_33 line 442
  228. theorem OAI.CycleClique.certificate_367_part_33_checked line 444
  229. def OAI.CycleClique.certificate_367_part_32 line 446
  230. theorem OAI.CycleClique.certificate_367_part_32_checked line 448
  231. def OAI.CycleClique.certificate_367_part_35_E line 450
  232. def OAI.CycleClique.certificate_367_part_35_M line 452
  233. def OAI.CycleClique.certificate_367_part_36_E line 454
  234. def OAI.CycleClique.certificate_367_part_36_M line 456
  235. def OAI.CycleClique.certificate_367_part_37_E line 458
  236. def OAI.CycleClique.certificate_367_part_37_M line 460
  237. def OAI.CycleClique.certificate_367_part_38_E line 462
  238. def OAI.CycleClique.certificate_367_part_38_M line 464
  239. def OAI.CycleClique.certificate_367_part_38 line 466
  240. theorem OAI.CycleClique.certificate_367_part_38_checked line 468
  241. def OAI.CycleClique.certificate_367_part_37 line 470
  242. theorem OAI.CycleClique.certificate_367_part_37_checked line 472
  243. def OAI.CycleClique.certificate_367_part_36 line 474
  244. theorem OAI.CycleClique.certificate_367_part_36_checked line 476
  245. def OAI.CycleClique.certificate_367_part_39_E line 478
  246. def OAI.CycleClique.certificate_367_part_39_M line 480
  247. def OAI.CycleClique.certificate_367_part_40_E line 482
  248. def OAI.CycleClique.certificate_367_part_40_M line 484
  249. def OAI.CycleClique.certificate_367_part_41_E line 486
  250. def OAI.CycleClique.certificate_367_part_41_M line 488
  251. def OAI.CycleClique.certificate_367_part_41 line 490
  252. theorem OAI.CycleClique.certificate_367_part_41_checked line 492
  253. def OAI.CycleClique.certificate_367_part_40 line 494
  254. theorem OAI.CycleClique.certificate_367_part_40_checked line 496
  255. def OAI.CycleClique.certificate_367_part_39 line 498
  256. theorem OAI.CycleClique.certificate_367_part_39_checked line 500
  257. def OAI.CycleClique.certificate_367_part_42_E line 502
  258. def OAI.CycleClique.certificate_367_part_42_M line 504
  259. def OAI.CycleClique.certificate_367_part_43_E line 506
  260. def OAI.CycleClique.certificate_367_part_43_M line 508
  261. def OAI.CycleClique.certificate_367_part_44_E line 510
  262. def OAI.CycleClique.certificate_367_part_44_M line 512
  263. def OAI.CycleClique.certificate_367_part_45_E line 514
  264. def OAI.CycleClique.certificate_367_part_45_M line 516
  265. def OAI.CycleClique.certificate_367_part_45 line 518
  266. theorem OAI.CycleClique.certificate_367_part_45_checked line 520
  267. def OAI.CycleClique.certificate_367_part_44 line 522
  268. theorem OAI.CycleClique.certificate_367_part_44_checked line 524
  269. def OAI.CycleClique.certificate_367_part_43 line 526
  270. theorem OAI.CycleClique.certificate_367_part_43_checked line 528
  271. def OAI.CycleClique.certificate_367_part_42 line 530
  272. theorem OAI.CycleClique.certificate_367_part_42_checked line 532
  273. def OAI.CycleClique.certificate_367_part_46_E line 534
  274. def OAI.CycleClique.certificate_367_part_46_M line 536
  275. def OAI.CycleClique.certificate_367_part_47_E line 538
  276. def OAI.CycleClique.certificate_367_part_47_M line 540
  277. def OAI.CycleClique.certificate_367_part_48_E line 542
  278. def OAI.CycleClique.certificate_367_part_48_M line 544
  279. def OAI.CycleClique.certificate_367_part_49_E line 546
  280. def OAI.CycleClique.certificate_367_part_49_M line 548
  281. def OAI.CycleClique.certificate_367_part_49 line 550
  282. theorem OAI.CycleClique.certificate_367_part_49_checked line 552
  283. def OAI.CycleClique.certificate_367_part_48 line 554
  284. theorem OAI.CycleClique.certificate_367_part_48_checked line 556
  285. def OAI.CycleClique.certificate_367_part_47 line 558
  286. theorem OAI.CycleClique.certificate_367_part_47_checked line 560
  287. def OAI.CycleClique.certificate_367_part_46 line 562
  288. theorem OAI.CycleClique.certificate_367_part_46_checked line 564
  289. def OAI.CycleClique.certificate_367_part_50_E line 566
  290. def OAI.CycleClique.certificate_367_part_50_M line 568
  291. def OAI.CycleClique.certificate_367_part_50 line 570
  292. theorem OAI.CycleClique.certificate_367_part_50_checked line 572
  293. def OAI.CycleClique.certificate_367_part_51_E line 574
  294. def OAI.CycleClique.certificate_367_part_51_M line 576
  295. def OAI.CycleClique.certificate_367_part_52_E line 578
  296. def OAI.CycleClique.certificate_367_part_52_M line 580
  297. def OAI.CycleClique.certificate_367_part_53_E line 582
  298. def OAI.CycleClique.certificate_367_part_53_M line 584
  299. def OAI.CycleClique.certificate_367_part_53 line 586
  300. theorem OAI.CycleClique.certificate_367_part_53_checked line 588
  301. def OAI.CycleClique.certificate_367_part_52 line 590
  302. theorem OAI.CycleClique.certificate_367_part_52_checked line 592
  303. def OAI.CycleClique.certificate_367_part_51 line 594
  304. theorem OAI.CycleClique.certificate_367_part_51_checked line 596
  305. def OAI.CycleClique.certificate_367_part_54_E line 598
  306. def OAI.CycleClique.certificate_367_part_54_M line 600
  307. def OAI.CycleClique.certificate_367_part_55_E line 602
  308. def OAI.CycleClique.certificate_367_part_55_M line 604
  309. def OAI.CycleClique.certificate_367_part_56_E line 606
  310. def OAI.CycleClique.certificate_367_part_56_M line 608
  311. def OAI.CycleClique.certificate_367_part_57_E line 610
  312. def OAI.CycleClique.certificate_367_part_57_M line 612
  313. def OAI.CycleClique.certificate_367_part_57 line 614
  314. theorem OAI.CycleClique.certificate_367_part_57_checked line 616
  315. def OAI.CycleClique.certificate_367_part_56 line 618
  316. theorem OAI.CycleClique.certificate_367_part_56_checked line 620
  317. def OAI.CycleClique.certificate_367_part_55 line 622
  318. theorem OAI.CycleClique.certificate_367_part_55_checked line 624
  319. def OAI.CycleClique.certificate_367_part_58_E line 626
  320. def OAI.CycleClique.certificate_367_part_58_M line 628
  321. def OAI.CycleClique.certificate_367_part_59_E line 630
  322. def OAI.CycleClique.certificate_367_part_59_M line 632
  323. def OAI.CycleClique.certificate_367_part_60_E line 634
  324. def OAI.CycleClique.certificate_367_part_60_M line 636
  325. def OAI.CycleClique.certificate_367_part_60 line 638
  326. theorem OAI.CycleClique.certificate_367_part_60_checked line 640
  327. def OAI.CycleClique.certificate_367_part_59 line 642
  328. theorem OAI.CycleClique.certificate_367_part_59_checked line 644
  329. def OAI.CycleClique.certificate_367_part_58 line 646
  330. theorem OAI.CycleClique.certificate_367_part_58_checked line 648
  331. def OAI.CycleClique.certificate_367_part_61_E line 650
  332. def OAI.CycleClique.certificate_367_part_61_M line 652
  333. def OAI.CycleClique.certificate_367_part_62_E line 654
  334. def OAI.CycleClique.certificate_367_part_62_M line 656
  335. def OAI.CycleClique.certificate_367_part_63_E line 658
  336. def OAI.CycleClique.certificate_367_part_63_M line 660
  337. def OAI.CycleClique.certificate_367_part_64_E line 662
  338. def OAI.CycleClique.certificate_367_part_64_M line 664
  339. def OAI.CycleClique.certificate_367_part_64 line 666
  340. theorem OAI.CycleClique.certificate_367_part_64_checked line 668
  341. def OAI.CycleClique.certificate_367_part_63 line 670
  342. theorem OAI.CycleClique.certificate_367_part_63_checked line 672
  343. def OAI.CycleClique.certificate_367_part_62 line 674
  344. theorem OAI.CycleClique.certificate_367_part_62_checked line 676
  345. def OAI.CycleClique.certificate_367_part_61 line 678
  346. theorem OAI.CycleClique.certificate_367_part_61_checked line 680
  347. def OAI.CycleClique.certificate_367_part_65_E line 682
  348. def OAI.CycleClique.certificate_367_part_65_M line 684
  349. def OAI.CycleClique.certificate_367_part_66_E line 686
  350. def OAI.CycleClique.certificate_367_part_66_M line 688
  351. def OAI.CycleClique.certificate_367_part_67_E line 690
  352. def OAI.CycleClique.certificate_367_part_67_M line 692
  353. def OAI.CycleClique.certificate_367_part_68_E line 694
  354. def OAI.CycleClique.certificate_367_part_68_M line 696
  355. def OAI.CycleClique.certificate_367_part_68 line 698
  356. theorem OAI.CycleClique.certificate_367_part_68_checked line 700
  357. def OAI.CycleClique.certificate_367_part_67 line 702
  358. theorem OAI.CycleClique.certificate_367_part_67_checked line 704
  359. def OAI.CycleClique.certificate_367_part_66 line 706
  360. theorem OAI.CycleClique.certificate_367_part_66_checked line 708
  361. def OAI.CycleClique.certificate_367_part_65 line 710
  362. theorem OAI.CycleClique.certificate_367_part_65_checked line 712
  363. def OAI.CycleClique.certificate_367_part_69_E line 714
  364. def OAI.CycleClique.certificate_367_part_69_M line 716
  365. def OAI.CycleClique.certificate_367_part_69 line 718
  366. theorem OAI.CycleClique.certificate_367_part_69_checked line 720
  367. def OAI.CycleClique.certificate_367_part_70_E line 722
  368. def OAI.CycleClique.certificate_367_part_70_M line 724
  369. def OAI.CycleClique.certificate_367_part_71_E line 726
  370. def OAI.CycleClique.certificate_367_part_71_M line 728
  371. def OAI.CycleClique.certificate_367_part_72_E line 730
  372. def OAI.CycleClique.certificate_367_part_72_M line 732
  373. def OAI.CycleClique.certificate_367_part_72 line 734
  374. theorem OAI.CycleClique.certificate_367_part_72_checked line 736
  375. def OAI.CycleClique.certificate_367_part_71 line 738
  376. theorem OAI.CycleClique.certificate_367_part_71_checked line 740
  377. def OAI.CycleClique.certificate_367_part_70 line 742
  378. theorem OAI.CycleClique.certificate_367_part_70_checked line 744
  379. def OAI.CycleClique.certificate_367_part_73_E line 746
  380. def OAI.CycleClique.certificate_367_part_73_M line 748
  381. def OAI.CycleClique.certificate_367_part_74_E line 750
  382. def OAI.CycleClique.certificate_367_part_74_M line 752
  383. def OAI.CycleClique.certificate_367_part_75_E line 754
  384. def OAI.CycleClique.certificate_367_part_75_M line 756
  385. def OAI.CycleClique.certificate_367_part_76_E line 758
  386. def OAI.CycleClique.certificate_367_part_76_M line 760
  387. def OAI.CycleClique.certificate_367_part_77_E line 762
  388. def OAI.CycleClique.certificate_367_part_77_M line 764
  389. def OAI.CycleClique.certificate_367_part_78_E line 766
  390. def OAI.CycleClique.certificate_367_part_78_M line 768
  391. def OAI.CycleClique.certificate_367_part_79_E line 770
  392. def OAI.CycleClique.certificate_367_part_79_M line 772
  393. def OAI.CycleClique.certificate_367_part_79 line 774
  394. theorem OAI.CycleClique.certificate_367_part_79_checked line 776
  395. def OAI.CycleClique.certificate_367_part_80_E line 778
  396. def OAI.CycleClique.certificate_367_part_80_M line 780
  397. def OAI.CycleClique.certificate_367_part_80 line 782
  398. theorem OAI.CycleClique.certificate_367_part_80_checked line 784
  399. def OAI.CycleClique.certificate_367_part_78 line 786
  400. theorem OAI.CycleClique.certificate_367_part_78_checked line 788
  401. def OAI.CycleClique.certificate_367_part_77 line 790
  402. theorem OAI.CycleClique.certificate_367_part_77_checked line 792
  403. def OAI.CycleClique.certificate_367_part_76 line 794
  404. theorem OAI.CycleClique.certificate_367_part_76_checked line 796
  405. def OAI.CycleClique.certificate_367_part_75 line 798
  406. theorem OAI.CycleClique.certificate_367_part_75_checked line 800
  407. def OAI.CycleClique.certificate_367_part_74 line 802
  408. theorem OAI.CycleClique.certificate_367_part_74_checked line 804
  409. def OAI.CycleClique.certificate_367_part_73 line 806
  410. theorem OAI.CycleClique.certificate_367_part_73_checked line 808
  411. def OAI.CycleClique.certificate_367_part_54 line 810
  412. theorem OAI.CycleClique.certificate_367_part_54_checked line 812
  413. def OAI.CycleClique.certificate_367_part_35 line 814
  414. theorem OAI.CycleClique.certificate_367_part_35_checked line 816
  415. def OAI.CycleClique.certificate_367_part_18 line 818
  416. theorem OAI.CycleClique.certificate_367_part_18_checked line 820
  417. def OAI.CycleClique.certificate_367_part_10 line 822
  418. theorem OAI.CycleClique.certificate_367_part_10_checked line 824
  419. def OAI.CycleClique.certificate_367_part_8 line 826
  420. theorem OAI.CycleClique.certificate_367_part_8_checked line 828
  421. def OAI.CycleClique.certificate_367_part_7 line 830
  422. theorem OAI.CycleClique.certificate_367_part_7_checked line 832
  423. def OAI.CycleClique.certificate_367_part_6 line 834
  424. theorem OAI.CycleClique.certificate_367_part_6_checked line 836
  425. def OAI.CycleClique.certificate_367_part_5 line 838
  426. theorem OAI.CycleClique.certificate_367_part_5_checked line 840
  427. def OAI.CycleClique.certificate_367_part_4 line 842
  428. theorem OAI.CycleClique.certificate_367_part_4_checked line 844
  429. def OAI.CycleClique.certificate_367_part_3 line 846
  430. theorem OAI.CycleClique.certificate_367_part_3_checked line 848
  431. def OAI.CycleClique.certificate_367_part_2 line 850
  432. theorem OAI.CycleClique.certificate_367_part_2_checked line 852
  433. def OAI.CycleClique.certificate_367_part_1 line 854
  434. theorem OAI.CycleClique.certificate_367_part_1_checked line 856
  435. def OAI.CycleClique.certificate_367 line 858
  436. theorem OAI.CycleClique.certificate_367_checked line 860
  437. theorem OAI.CycleClique.certificate_367_valid line 862
  438. def OAI.CycleClique.certificate_368_q line 864
  439. def OAI.CycleClique.certificate_368_edges line 865
  440. def OAI.CycleClique.certificate_368_part_0 line 867
  441. def OAI.CycleClique.certificate_368_part_1 line 869
  442. def OAI.CycleClique.certificate_368 line 871
  443. theorem OAI.CycleClique.certificate_368_checked line 873
  444. theorem OAI.CycleClique.certificate_368_valid line 874
  445. def OAI.CycleClique.certificate_369_q line 876
  446. def OAI.CycleClique.certificate_369_edges line 877
  447. def OAI.CycleClique.certificate_369_part_0 line 879
  448. def OAI.CycleClique.certificate_369_part_1 line 881
  449. def OAI.CycleClique.certificate_369 line 883
  450. theorem OAI.CycleClique.certificate_369_checked line 885
  451. theorem OAI.CycleClique.certificate_369_valid line 886
  452. def OAI.CycleClique.certificate_370_q line 888
  453. def OAI.CycleClique.certificate_370_edges line 889
  454. def OAI.CycleClique.certificate_370_part_0 line 891
  455. def OAI.CycleClique.certificate_370_part_1 line 893
  456. def OAI.CycleClique.certificate_370 line 895
  457. theorem OAI.CycleClique.certificate_370_checked line 897
  458. theorem OAI.CycleClique.certificate_370_valid line 898
  459. def OAI.CycleClique.certificate_371_q line 900
  460. def OAI.CycleClique.certificate_371_edges line 901
  461. def OAI.CycleClique.certificate_371_part_0 line 903
  462. def OAI.CycleClique.certificate_371_part_1 line 905
  463. def OAI.CycleClique.certificate_371_part_2 line 907
  464. def OAI.CycleClique.certificate_371 line 909
  465. theorem OAI.CycleClique.certificate_371_checked line 911
  466. theorem OAI.CycleClique.certificate_371_valid line 912
  467. def OAI.CycleClique.certificate_372_q line 914
  468. def OAI.CycleClique.certificate_372_edges line 915
  469. def OAI.CycleClique.certificate_372_part_0 line 917
  470. def OAI.CycleClique.certificate_372_part_1 line 919
  471. def OAI.CycleClique.certificate_372_part_2 line 921
  472. def OAI.CycleClique.certificate_372 line 923
  473. theorem OAI.CycleClique.certificate_372_checked line 925
  474. theorem OAI.CycleClique.certificate_372_valid line 926
  475. def OAI.CycleClique.certificate_373_q line 928
  476. def OAI.CycleClique.certificate_373_edges line 929
  477. def OAI.CycleClique.certificate_373_part_0 line 931
  478. def OAI.CycleClique.certificate_373_part_1 line 933
  479. def OAI.CycleClique.certificate_373 line 935
  480. theorem OAI.CycleClique.certificate_373_checked line 937
  481. theorem OAI.CycleClique.certificate_373_valid line 938
  482. def OAI.CycleClique.certificate_374_q line 940
  483. def OAI.CycleClique.certificate_374_edges line 941
  484. def OAI.CycleClique.certificate_374_part_0 line 943
  485. def OAI.CycleClique.certificate_374_part_1 line 945
  486. def OAI.CycleClique.certificate_374_part_2 line 947
  487. def OAI.CycleClique.certificate_374 line 949
  488. theorem OAI.CycleClique.certificate_374_checked line 951
  489. theorem OAI.CycleClique.certificate_374_valid line 952
  490. def OAI.CycleClique.certificate_375_q line 954
  491. def OAI.CycleClique.certificate_375_edges line 955
  492. def OAI.CycleClique.certificate_375_part_0 line 957
  493. def OAI.CycleClique.certificate_375_part_1 line 959
  494. def OAI.CycleClique.certificate_375_part_2 line 961
  495. def OAI.CycleClique.certificate_375 line 963
  496. theorem OAI.CycleClique.certificate_375_checked line 965
  497. theorem OAI.CycleClique.certificate_375_valid line 966
  498. def OAI.CycleClique.certificate_376_q line 968
  499. def OAI.CycleClique.certificate_376_edges line 970
  500. def OAI.CycleClique.certificate_376_E line 972
  501. def OAI.CycleClique.certificate_376_M line 974
  502. def OAI.CycleClique.certificate_376_part_1_E line 976
  503. def OAI.CycleClique.certificate_376_part_1_M line 978
  504. def OAI.CycleClique.certificate_376_part_2_E line 980
  505. def OAI.CycleClique.certificate_376_part_2_M line 982
  506. def OAI.CycleClique.certificate_376_part_3_E line 984
  507. def OAI.CycleClique.certificate_376_part_3_M line 986
  508. def OAI.CycleClique.certificate_376_part_4_E line 988
  509. def OAI.CycleClique.certificate_376_part_4_M line 990
  510. def OAI.CycleClique.certificate_376_part_5_E line 992
  511. def OAI.CycleClique.certificate_376_part_5_M line 994
  512. def OAI.CycleClique.certificate_376_part_6_E line 996
  513. def OAI.CycleClique.certificate_376_part_6_M line 998
  514. def OAI.CycleClique.certificate_376_part_7_E line 1000
  515. def OAI.CycleClique.certificate_376_part_7_M line 1002
  516. def OAI.CycleClique.certificate_376_part_8_E line 1004
  517. def OAI.CycleClique.certificate_376_part_8_M line 1006
  518. def OAI.CycleClique.certificate_376_part_8 line 1008
  519. theorem OAI.CycleClique.certificate_376_part_8_checked line 1010
  520. def OAI.CycleClique.certificate_376_part_9_E line 1012
  521. def OAI.CycleClique.certificate_376_part_9_M line 1014
  522. def OAI.CycleClique.certificate_376_part_10_E line 1016
  523. def OAI.CycleClique.certificate_376_part_10_M line 1018
  524. def OAI.CycleClique.certificate_376_part_10 line 1020
  525. theorem OAI.CycleClique.certificate_376_part_10_checked line 1022
  526. def OAI.CycleClique.certificate_376_part_11_E line 1024
  527. def OAI.CycleClique.certificate_376_part_11_M line 1026
  528. def OAI.CycleClique.certificate_376_part_12_E line 1028
  529. def OAI.CycleClique.certificate_376_part_12_M line 1030
  530. def OAI.CycleClique.certificate_376_part_13_E line 1032
  531. def OAI.CycleClique.certificate_376_part_13_M line 1034
  532. def OAI.CycleClique.certificate_376_part_14_E line 1036
  533. def OAI.CycleClique.certificate_376_part_14_M line 1038
  534. def OAI.CycleClique.certificate_376_part_14 line 1040
  535. theorem OAI.CycleClique.certificate_376_part_14_checked line 1042
  536. def OAI.CycleClique.certificate_376_part_13 line 1044
  537. theorem OAI.CycleClique.certificate_376_part_13_checked line 1046
  538. def OAI.CycleClique.certificate_376_part_15_E line 1048
  539. def OAI.CycleClique.certificate_376_part_15_M line 1050
  540. def OAI.CycleClique.certificate_376_part_15 line 1052
  541. theorem OAI.CycleClique.certificate_376_part_15_checked line 1054
  542. def OAI.CycleClique.certificate_376_part_16_E line 1056
  543. def OAI.CycleClique.certificate_376_part_16_M line 1058
  544. def OAI.CycleClique.certificate_376_part_16 line 1060
  545. theorem OAI.CycleClique.certificate_376_part_16_checked line 1062
  546. def OAI.CycleClique.certificate_376_part_17_E line 1064
  547. def OAI.CycleClique.certificate_376_part_17_M line 1066
  548. def OAI.CycleClique.certificate_376_part_18_E line 1068
  549. def OAI.CycleClique.certificate_376_part_18_M line 1070
  550. def OAI.CycleClique.certificate_376_part_18 line 1072
  551. theorem OAI.CycleClique.certificate_376_part_18_checked line 1074
  552. def OAI.CycleClique.certificate_376_part_19_E line 1076
  553. def OAI.CycleClique.certificate_376_part_19_M line 1078
  554. def OAI.CycleClique.certificate_376_part_19 line 1080
  555. theorem OAI.CycleClique.certificate_376_part_19_checked line 1082
  556. def OAI.CycleClique.certificate_376_part_20_E line 1084
  557. def OAI.CycleClique.certificate_376_part_20_M line 1086
  558. def OAI.CycleClique.certificate_376_part_20 line 1088
  559. theorem OAI.CycleClique.certificate_376_part_20_checked line 1090
  560. def OAI.CycleClique.certificate_376_part_21_E line 1092
  561. def OAI.CycleClique.certificate_376_part_21_M line 1094
  562. def OAI.CycleClique.certificate_376_part_21 line 1096
  563. theorem OAI.CycleClique.certificate_376_part_21_checked line 1098
  564. def OAI.CycleClique.certificate_376_part_22_E line 1100
  565. def OAI.CycleClique.certificate_376_part_22_M line 1102
  566. def OAI.CycleClique.certificate_376_part_23_E line 1104
  567. def OAI.CycleClique.certificate_376_part_23_M line 1106
  568. def OAI.CycleClique.certificate_376_part_23 line 1108
  569. theorem OAI.CycleClique.certificate_376_part_23_checked line 1110
  570. def OAI.CycleClique.certificate_376_part_24_E line 1112
  571. def OAI.CycleClique.certificate_376_part_24_M line 1114
  572. def OAI.CycleClique.certificate_376_part_25_E line 1116
  573. def OAI.CycleClique.certificate_376_part_25_M line 1118
  574. def OAI.CycleClique.certificate_376_part_25 line 1120
  575. theorem OAI.CycleClique.certificate_376_part_25_checked line 1122
  576. def OAI.CycleClique.certificate_376_part_26_E line 1124
  577. def OAI.CycleClique.certificate_376_part_26_M line 1126
  578. def OAI.CycleClique.certificate_376_part_27_E line 1128
  579. def OAI.CycleClique.certificate_376_part_27_M line 1130
  580. def OAI.CycleClique.certificate_376_part_28_E line 1132
  581. def OAI.CycleClique.certificate_376_part_28_M line 1134
  582. def OAI.CycleClique.certificate_376_part_29_E line 1136
  583. def OAI.CycleClique.certificate_376_part_29_M line 1138
  584. def OAI.CycleClique.certificate_376_part_30_E line 1140
  585. def OAI.CycleClique.certificate_376_part_30_M line 1142
  586. def OAI.CycleClique.certificate_376_part_30 line 1144
  587. theorem OAI.CycleClique.certificate_376_part_30_checked line 1146
  588. def OAI.CycleClique.certificate_376_part_29 line 1148
  589. theorem OAI.CycleClique.certificate_376_part_29_checked line 1150
  590. def OAI.CycleClique.certificate_376_part_28 line 1152
  591. theorem OAI.CycleClique.certificate_376_part_28_checked line 1154
  592. def OAI.CycleClique.certificate_376_part_31_E line 1156
  593. def OAI.CycleClique.certificate_376_part_31_M line 1158
  594. def OAI.CycleClique.certificate_376_part_32_E line 1160
  595. def OAI.CycleClique.certificate_376_part_32_M line 1162
  596. def OAI.CycleClique.certificate_376_part_32 line 1164
  597. theorem OAI.CycleClique.certificate_376_part_32_checked line 1166
  598. def OAI.CycleClique.certificate_376_part_33_E line 1168
  599. def OAI.CycleClique.certificate_376_part_33_M line 1170
  600. def OAI.CycleClique.certificate_376_part_33 line 1172
  601. theorem OAI.CycleClique.certificate_376_part_33_checked line 1174
  602. def OAI.CycleClique.certificate_376_part_34_E line 1176
  603. def OAI.CycleClique.certificate_376_part_34_M line 1178
  604. def OAI.CycleClique.certificate_376_part_34 line 1180
  605. theorem OAI.CycleClique.certificate_376_part_34_checked line 1182
  606. def OAI.CycleClique.certificate_376_part_31 line 1184
  607. theorem OAI.CycleClique.certificate_376_part_31_checked line 1186
  608. def OAI.CycleClique.certificate_376_part_27 line 1188
  609. theorem OAI.CycleClique.certificate_376_part_27_checked line 1190
  610. def OAI.CycleClique.certificate_376_part_26 line 1192
  611. theorem OAI.CycleClique.certificate_376_part_26_checked line 1194
  612. def OAI.CycleClique.certificate_376_part_24 line 1196
  613. theorem OAI.CycleClique.certificate_376_part_24_checked line 1198
  614. def OAI.CycleClique.certificate_376_part_22 line 1200
  615. theorem OAI.CycleClique.certificate_376_part_22_checked line 1202
  616. def OAI.CycleClique.certificate_376_part_17 line 1204
  617. theorem OAI.CycleClique.certificate_376_part_17_checked line 1206
  618. def OAI.CycleClique.certificate_376_part_12 line 1208
  619. theorem OAI.CycleClique.certificate_376_part_12_checked line 1210
  620. def OAI.CycleClique.certificate_376_part_11 line 1212
  621. theorem OAI.CycleClique.certificate_376_part_11_checked line 1214
  622. def OAI.CycleClique.certificate_376_part_9 line 1216
  623. theorem OAI.CycleClique.certificate_376_part_9_checked line 1218
  624. def OAI.CycleClique.certificate_376_part_7 line 1220
  625. theorem OAI.CycleClique.certificate_376_part_7_checked line 1222
  626. def OAI.CycleClique.certificate_376_part_6 line 1224
  627. theorem OAI.CycleClique.certificate_376_part_6_checked line 1226
  628. def OAI.CycleClique.certificate_376_part_5 line 1228
  629. theorem OAI.CycleClique.certificate_376_part_5_checked line 1230
  630. def OAI.CycleClique.certificate_376_part_4 line 1232
  631. theorem OAI.CycleClique.certificate_376_part_4_checked line 1234
  632. def OAI.CycleClique.certificate_376_part_3 line 1236
  633. theorem OAI.CycleClique.certificate_376_part_3_checked line 1238
  634. def OAI.CycleClique.certificate_376_part_2 line 1240
  635. theorem OAI.CycleClique.certificate_376_part_2_checked line 1242
  636. def OAI.CycleClique.certificate_376_part_1 line 1244
  637. theorem OAI.CycleClique.certificate_376_part_1_checked line 1246
  638. def OAI.CycleClique.certificate_376 line 1248
  639. theorem OAI.CycleClique.certificate_376_checked line 1250
  640. theorem OAI.CycleClique.certificate_376_valid line 1252
  641. def OAI.CycleClique.certificate_377_q line 1254
  642. def OAI.CycleClique.certificate_377_edges line 1255
  643. def OAI.CycleClique.certificate_377_part_0 line 1257
  644. def OAI.CycleClique.certificate_377_part_1 line 1259
  645. def OAI.CycleClique.certificate_377 line 1261
  646. theorem OAI.CycleClique.certificate_377_checked line 1263
  647. theorem OAI.CycleClique.certificate_377_valid line 1264
  648. def OAI.CycleClique.certificate_378_q line 1266
  649. def OAI.CycleClique.certificate_378_edges line 1267
  650. def OAI.CycleClique.certificate_378_part_0 line 1269
  651. def OAI.CycleClique.certificate_378_part_1 line 1271
  652. def OAI.CycleClique.certificate_378 line 1273
  653. theorem OAI.CycleClique.certificate_378_checked line 1275
  654. theorem OAI.CycleClique.certificate_378_valid line 1276
  655. def OAI.CycleClique.certificate_379_q line 1278
  656. def OAI.CycleClique.certificate_379_edges line 1279
  657. def OAI.CycleClique.certificate_379_part_0 line 1281
  658. def OAI.CycleClique.certificate_379_part_1 line 1283
  659. def OAI.CycleClique.certificate_379 line 1285
  660. theorem OAI.CycleClique.certificate_379_checked line 1287
  661. theorem OAI.CycleClique.certificate_379_valid line 1288
  662. def OAI.CycleClique.certificate_380_q line 1290
  663. def OAI.CycleClique.certificate_380_edges line 1291
  664. def OAI.CycleClique.certificate_380_part_0 line 1293
  665. def OAI.CycleClique.certificate_380_part_1 line 1295
  666. def OAI.CycleClique.certificate_380_part_2 line 1297
  667. def OAI.CycleClique.certificate_380 line 1299
  668. theorem OAI.CycleClique.certificate_380_checked line 1301
  669. theorem OAI.CycleClique.certificate_380_valid line 1302
  670. def OAI.CycleClique.certificate_381_q line 1304
  671. def OAI.CycleClique.certificate_381_edges line 1305
  672. def OAI.CycleClique.certificate_381_part_0 line 1307
  673. def OAI.CycleClique.certificate_381_part_1 line 1309
  674. def OAI.CycleClique.certificate_381_part_2 line 1311
  675. def OAI.CycleClique.certificate_381 line 1313
  676. theorem OAI.CycleClique.certificate_381_checked line 1315
  677. theorem OAI.CycleClique.certificate_381_valid line 1316
  678. def OAI.CycleClique.certificate_382_q line 1318
  679. def OAI.CycleClique.certificate_382_edges line 1319
  680. def OAI.CycleClique.certificate_382_part_0 line 1321
  681. def OAI.CycleClique.certificate_382_part_1 line 1323
  682. def OAI.CycleClique.certificate_382 line 1325
  683. theorem OAI.CycleClique.certificate_382_checked line 1327
  684. theorem OAI.CycleClique.certificate_382_valid line 1328
  685. def OAI.CycleClique.certificate_383_q line 1330
  686. def OAI.CycleClique.certificate_383_edges line 1331
  687. def OAI.CycleClique.certificate_383_part_0 line 1333
  688. def OAI.CycleClique.certificate_383_part_1 line 1335
  689. def OAI.CycleClique.certificate_383 line 1337
  690. theorem OAI.CycleClique.certificate_383_checked line 1339
  691. theorem OAI.CycleClique.certificate_383_valid line 1340