OAI/Combinatorics/Ramsey/CycleClique/Certificates039.lean

GitHub source file

985 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.certificate_1216_q line 20
  2. def OAI.CycleClique.certificate_1216_edges line 21
  3. def OAI.CycleClique.certificate_1216_part_0 line 23
  4. def OAI.CycleClique.certificate_1216_part_1 line 25
  5. def OAI.CycleClique.certificate_1216_part_2 line 27
  6. def OAI.CycleClique.certificate_1216_part_3 line 29
  7. def OAI.CycleClique.certificate_1216 line 31
  8. theorem OAI.CycleClique.certificate_1216_checked line 33
  9. theorem OAI.CycleClique.certificate_1216_valid line 34
  10. def OAI.CycleClique.certificate_1217_q line 36
  11. def OAI.CycleClique.certificate_1217_edges line 37
  12. def OAI.CycleClique.certificate_1217_part_0 line 39
  13. def OAI.CycleClique.certificate_1217_part_1 line 41
  14. def OAI.CycleClique.certificate_1217_part_2 line 43
  15. def OAI.CycleClique.certificate_1217_part_3 line 45
  16. def OAI.CycleClique.certificate_1217_part_4 line 47
  17. def OAI.CycleClique.certificate_1217 line 49
  18. theorem OAI.CycleClique.certificate_1217_checked line 51
  19. theorem OAI.CycleClique.certificate_1217_valid line 52
  20. def OAI.CycleClique.certificate_1218_q line 54
  21. def OAI.CycleClique.certificate_1218_edges line 55
  22. def OAI.CycleClique.certificate_1218_part_0 line 57
  23. def OAI.CycleClique.certificate_1218_part_1 line 59
  24. def OAI.CycleClique.certificate_1218_part_2 line 61
  25. def OAI.CycleClique.certificate_1218_part_3 line 63
  26. def OAI.CycleClique.certificate_1218_part_4 line 65
  27. def OAI.CycleClique.certificate_1218 line 67
  28. theorem OAI.CycleClique.certificate_1218_checked line 69
  29. theorem OAI.CycleClique.certificate_1218_valid line 70
  30. def OAI.CycleClique.certificate_1219_q line 72
  31. def OAI.CycleClique.certificate_1219_edges line 73
  32. def OAI.CycleClique.certificate_1219_part_0 line 75
  33. def OAI.CycleClique.certificate_1219_part_1 line 77
  34. def OAI.CycleClique.certificate_1219_part_2 line 79
  35. def OAI.CycleClique.certificate_1219_part_3 line 81
  36. def OAI.CycleClique.certificate_1219 line 83
  37. theorem OAI.CycleClique.certificate_1219_checked line 85
  38. theorem OAI.CycleClique.certificate_1219_valid line 86
  39. def OAI.CycleClique.certificate_1220_q line 88
  40. def OAI.CycleClique.certificate_1220_edges line 89
  41. def OAI.CycleClique.certificate_1220_part_0 line 91
  42. def OAI.CycleClique.certificate_1220_part_1 line 93
  43. def OAI.CycleClique.certificate_1220_part_2 line 95
  44. def OAI.CycleClique.certificate_1220_part_3 line 97
  45. def OAI.CycleClique.certificate_1220 line 99
  46. theorem OAI.CycleClique.certificate_1220_checked line 101
  47. theorem OAI.CycleClique.certificate_1220_valid line 102
  48. def OAI.CycleClique.certificate_1221_q line 104
  49. def OAI.CycleClique.certificate_1221_edges line 106
  50. def OAI.CycleClique.certificate_1221_E line 108
  51. def OAI.CycleClique.certificate_1221_M line 110
  52. def OAI.CycleClique.certificate_1221_part_1_E line 112
  53. def OAI.CycleClique.certificate_1221_part_1_M line 114
  54. def OAI.CycleClique.certificate_1221_part_2_E line 116
  55. def OAI.CycleClique.certificate_1221_part_2_M line 118
  56. def OAI.CycleClique.certificate_1221_part_3_E line 120
  57. def OAI.CycleClique.certificate_1221_part_3_M line 122
  58. def OAI.CycleClique.certificate_1221_part_4_E line 124
  59. def OAI.CycleClique.certificate_1221_part_4_M line 126
  60. def OAI.CycleClique.certificate_1221_part_5_E line 128
  61. def OAI.CycleClique.certificate_1221_part_5_M line 130
  62. def OAI.CycleClique.certificate_1221_part_6_E line 132
  63. def OAI.CycleClique.certificate_1221_part_6_M line 134
  64. def OAI.CycleClique.certificate_1221_part_7_E line 136
  65. def OAI.CycleClique.certificate_1221_part_7_M line 138
  66. def OAI.CycleClique.certificate_1221_part_8_E line 140
  67. def OAI.CycleClique.certificate_1221_part_8_M line 142
  68. def OAI.CycleClique.certificate_1221_part_9_E line 144
  69. def OAI.CycleClique.certificate_1221_part_9_M line 146
  70. def OAI.CycleClique.certificate_1221_part_10_E line 148
  71. def OAI.CycleClique.certificate_1221_part_10_M line 150
  72. def OAI.CycleClique.certificate_1221_part_11_E line 152
  73. def OAI.CycleClique.certificate_1221_part_11_M line 154
  74. def OAI.CycleClique.certificate_1221_part_12_E line 156
  75. def OAI.CycleClique.certificate_1221_part_12_M line 158
  76. def OAI.CycleClique.certificate_1221_part_12 line 160
  77. theorem OAI.CycleClique.certificate_1221_part_12_checked line 162
  78. def OAI.CycleClique.certificate_1221_part_13_E line 164
  79. def OAI.CycleClique.certificate_1221_part_13_M line 166
  80. def OAI.CycleClique.certificate_1221_part_14_E line 168
  81. def OAI.CycleClique.certificate_1221_part_14_M line 170
  82. def OAI.CycleClique.certificate_1221_part_15_E line 172
  83. def OAI.CycleClique.certificate_1221_part_15_M line 174
  84. def OAI.CycleClique.certificate_1221_part_16_E line 176
  85. def OAI.CycleClique.certificate_1221_part_16_M line 178
  86. def OAI.CycleClique.certificate_1221_part_17_E line 180
  87. def OAI.CycleClique.certificate_1221_part_17_M line 182
  88. def OAI.CycleClique.certificate_1221_part_17 line 184
  89. theorem OAI.CycleClique.certificate_1221_part_17_checked line 186
  90. def OAI.CycleClique.certificate_1221_part_18_E line 188
  91. def OAI.CycleClique.certificate_1221_part_18_M line 190
  92. def OAI.CycleClique.certificate_1221_part_19_E line 192
  93. def OAI.CycleClique.certificate_1221_part_19_M line 194
  94. def OAI.CycleClique.certificate_1221_part_20_E line 196
  95. def OAI.CycleClique.certificate_1221_part_20_M line 198
  96. def OAI.CycleClique.certificate_1221_part_21_E line 200
  97. def OAI.CycleClique.certificate_1221_part_21_M line 202
  98. def OAI.CycleClique.certificate_1221_part_22_E line 204
  99. def OAI.CycleClique.certificate_1221_part_22_M line 206
  100. def OAI.CycleClique.certificate_1221_part_23_E line 208
  101. def OAI.CycleClique.certificate_1221_part_23_M line 210
  102. def OAI.CycleClique.certificate_1221_part_23 line 212
  103. theorem OAI.CycleClique.certificate_1221_part_23_checked line 214
  104. def OAI.CycleClique.certificate_1221_part_22 line 216
  105. theorem OAI.CycleClique.certificate_1221_part_22_checked line 218
  106. def OAI.CycleClique.certificate_1221_part_21 line 220
  107. theorem OAI.CycleClique.certificate_1221_part_21_checked line 222
  108. def OAI.CycleClique.certificate_1221_part_24_E line 224
  109. def OAI.CycleClique.certificate_1221_part_24_M line 226
  110. def OAI.CycleClique.certificate_1221_part_25_E line 228
  111. def OAI.CycleClique.certificate_1221_part_25_M line 230
  112. def OAI.CycleClique.certificate_1221_part_25 line 232
  113. theorem OAI.CycleClique.certificate_1221_part_25_checked line 234
  114. def OAI.CycleClique.certificate_1221_part_26_E line 236
  115. def OAI.CycleClique.certificate_1221_part_26_M line 238
  116. def OAI.CycleClique.certificate_1221_part_27_E line 240
  117. def OAI.CycleClique.certificate_1221_part_27_M line 242
  118. def OAI.CycleClique.certificate_1221_part_28_E line 244
  119. def OAI.CycleClique.certificate_1221_part_28_M line 246
  120. def OAI.CycleClique.certificate_1221_part_29_E line 248
  121. def OAI.CycleClique.certificate_1221_part_29_M line 250
  122. def OAI.CycleClique.certificate_1221_part_30_E line 252
  123. def OAI.CycleClique.certificate_1221_part_30_M line 254
  124. def OAI.CycleClique.certificate_1221_part_31_E line 256
  125. def OAI.CycleClique.certificate_1221_part_31_M line 258
  126. def OAI.CycleClique.certificate_1221_part_32_E line 260
  127. def OAI.CycleClique.certificate_1221_part_32_M line 262
  128. def OAI.CycleClique.certificate_1221_part_33_E line 264
  129. def OAI.CycleClique.certificate_1221_part_33_M line 266
  130. def OAI.CycleClique.certificate_1221_part_33 line 268
  131. theorem OAI.CycleClique.certificate_1221_part_33_checked line 270
  132. def OAI.CycleClique.certificate_1221_part_34_E line 272
  133. def OAI.CycleClique.certificate_1221_part_34_M line 274
  134. def OAI.CycleClique.certificate_1221_part_34 line 276
  135. theorem OAI.CycleClique.certificate_1221_part_34_checked line 278
  136. def OAI.CycleClique.certificate_1221_part_35_E line 280
  137. def OAI.CycleClique.certificate_1221_part_35_M line 282
  138. def OAI.CycleClique.certificate_1221_part_35 line 284
  139. theorem OAI.CycleClique.certificate_1221_part_35_checked line 286
  140. def OAI.CycleClique.certificate_1221_part_36_E line 288
  141. def OAI.CycleClique.certificate_1221_part_36_M line 290
  142. def OAI.CycleClique.certificate_1221_part_36 line 292
  143. theorem OAI.CycleClique.certificate_1221_part_36_checked line 294
  144. def OAI.CycleClique.certificate_1221_part_37_E line 296
  145. def OAI.CycleClique.certificate_1221_part_37_M line 298
  146. def OAI.CycleClique.certificate_1221_part_38_E line 300
  147. def OAI.CycleClique.certificate_1221_part_38_M line 302
  148. def OAI.CycleClique.certificate_1221_part_38 line 304
  149. theorem OAI.CycleClique.certificate_1221_part_38_checked line 306
  150. def OAI.CycleClique.certificate_1221_part_39_E line 308
  151. def OAI.CycleClique.certificate_1221_part_39_M line 310
  152. def OAI.CycleClique.certificate_1221_part_39 line 312
  153. theorem OAI.CycleClique.certificate_1221_part_39_checked line 314
  154. def OAI.CycleClique.certificate_1221_part_40_E line 316
  155. def OAI.CycleClique.certificate_1221_part_40_M line 318
  156. def OAI.CycleClique.certificate_1221_part_40 line 320
  157. theorem OAI.CycleClique.certificate_1221_part_40_checked line 322
  158. def OAI.CycleClique.certificate_1221_part_41_E line 324
  159. def OAI.CycleClique.certificate_1221_part_41_M line 326
  160. def OAI.CycleClique.certificate_1221_part_42_E line 328
  161. def OAI.CycleClique.certificate_1221_part_42_M line 330
  162. def OAI.CycleClique.certificate_1221_part_43_E line 332
  163. def OAI.CycleClique.certificate_1221_part_43_M line 334
  164. def OAI.CycleClique.certificate_1221_part_44_E line 336
  165. def OAI.CycleClique.certificate_1221_part_44_M line 338
  166. def OAI.CycleClique.certificate_1221_part_45_E line 340
  167. def OAI.CycleClique.certificate_1221_part_45_M line 342
  168. def OAI.CycleClique.certificate_1221_part_46_E line 344
  169. def OAI.CycleClique.certificate_1221_part_46_M line 346
  170. def OAI.CycleClique.certificate_1221_part_46 line 348
  171. theorem OAI.CycleClique.certificate_1221_part_46_checked line 350
  172. def OAI.CycleClique.certificate_1221_part_45 line 352
  173. theorem OAI.CycleClique.certificate_1221_part_45_checked line 354
  174. def OAI.CycleClique.certificate_1221_part_44 line 356
  175. theorem OAI.CycleClique.certificate_1221_part_44_checked line 358
  176. def OAI.CycleClique.certificate_1221_part_43 line 360
  177. theorem OAI.CycleClique.certificate_1221_part_43_checked line 362
  178. def OAI.CycleClique.certificate_1221_part_47_E line 364
  179. def OAI.CycleClique.certificate_1221_part_47_M line 366
  180. def OAI.CycleClique.certificate_1221_part_47 line 368
  181. theorem OAI.CycleClique.certificate_1221_part_47_checked line 370
  182. def OAI.CycleClique.certificate_1221_part_48_E line 372
  183. def OAI.CycleClique.certificate_1221_part_48_M line 374
  184. def OAI.CycleClique.certificate_1221_part_48 line 376
  185. theorem OAI.CycleClique.certificate_1221_part_48_checked line 378
  186. def OAI.CycleClique.certificate_1221_part_49_E line 380
  187. def OAI.CycleClique.certificate_1221_part_49_M line 382
  188. def OAI.CycleClique.certificate_1221_part_50_E line 384
  189. def OAI.CycleClique.certificate_1221_part_50_M line 386
  190. def OAI.CycleClique.certificate_1221_part_50 line 388
  191. theorem OAI.CycleClique.certificate_1221_part_50_checked line 390
  192. def OAI.CycleClique.certificate_1221_part_51_E line 392
  193. def OAI.CycleClique.certificate_1221_part_51_M line 394
  194. def OAI.CycleClique.certificate_1221_part_51 line 396
  195. theorem OAI.CycleClique.certificate_1221_part_51_checked line 398
  196. def OAI.CycleClique.certificate_1221_part_52_E line 400
  197. def OAI.CycleClique.certificate_1221_part_52_M line 402
  198. def OAI.CycleClique.certificate_1221_part_52 line 404
  199. theorem OAI.CycleClique.certificate_1221_part_52_checked line 406
  200. def OAI.CycleClique.certificate_1221_part_53_E line 408
  201. def OAI.CycleClique.certificate_1221_part_53_M line 410
  202. def OAI.CycleClique.certificate_1221_part_53 line 412
  203. theorem OAI.CycleClique.certificate_1221_part_53_checked line 414
  204. def OAI.CycleClique.certificate_1221_part_54_E line 416
  205. def OAI.CycleClique.certificate_1221_part_54_M line 418
  206. def OAI.CycleClique.certificate_1221_part_54 line 420
  207. theorem OAI.CycleClique.certificate_1221_part_54_checked line 422
  208. def OAI.CycleClique.certificate_1221_part_55_E line 424
  209. def OAI.CycleClique.certificate_1221_part_55_M line 426
  210. def OAI.CycleClique.certificate_1221_part_56_E line 428
  211. def OAI.CycleClique.certificate_1221_part_56_M line 430
  212. def OAI.CycleClique.certificate_1221_part_56 line 432
  213. theorem OAI.CycleClique.certificate_1221_part_56_checked line 434
  214. def OAI.CycleClique.certificate_1221_part_57_E line 436
  215. def OAI.CycleClique.certificate_1221_part_57_M line 438
  216. def OAI.CycleClique.certificate_1221_part_57 line 440
  217. theorem OAI.CycleClique.certificate_1221_part_57_checked line 442
  218. def OAI.CycleClique.certificate_1221_part_58_E line 444
  219. def OAI.CycleClique.certificate_1221_part_58_M line 446
  220. def OAI.CycleClique.certificate_1221_part_58 line 448
  221. theorem OAI.CycleClique.certificate_1221_part_58_checked line 450
  222. def OAI.CycleClique.certificate_1221_part_55 line 452
  223. theorem OAI.CycleClique.certificate_1221_part_55_checked line 454
  224. def OAI.CycleClique.certificate_1221_part_49 line 456
  225. theorem OAI.CycleClique.certificate_1221_part_49_checked line 458
  226. def OAI.CycleClique.certificate_1221_part_42 line 460
  227. theorem OAI.CycleClique.certificate_1221_part_42_checked line 462
  228. def OAI.CycleClique.certificate_1221_part_41 line 464
  229. theorem OAI.CycleClique.certificate_1221_part_41_checked line 466
  230. def OAI.CycleClique.certificate_1221_part_37 line 468
  231. theorem OAI.CycleClique.certificate_1221_part_37_checked line 470
  232. def OAI.CycleClique.certificate_1221_part_32 line 472
  233. theorem OAI.CycleClique.certificate_1221_part_32_checked line 474
  234. def OAI.CycleClique.certificate_1221_part_31 line 476
  235. theorem OAI.CycleClique.certificate_1221_part_31_checked line 478
  236. def OAI.CycleClique.certificate_1221_part_30 line 480
  237. theorem OAI.CycleClique.certificate_1221_part_30_checked line 482
  238. def OAI.CycleClique.certificate_1221_part_29 line 484
  239. theorem OAI.CycleClique.certificate_1221_part_29_checked line 486
  240. def OAI.CycleClique.certificate_1221_part_28 line 488
  241. theorem OAI.CycleClique.certificate_1221_part_28_checked line 490
  242. def OAI.CycleClique.certificate_1221_part_27 line 492
  243. theorem OAI.CycleClique.certificate_1221_part_27_checked line 494
  244. def OAI.CycleClique.certificate_1221_part_26 line 496
  245. theorem OAI.CycleClique.certificate_1221_part_26_checked line 498
  246. def OAI.CycleClique.certificate_1221_part_24 line 500
  247. theorem OAI.CycleClique.certificate_1221_part_24_checked line 502
  248. def OAI.CycleClique.certificate_1221_part_20 line 504
  249. theorem OAI.CycleClique.certificate_1221_part_20_checked line 506
  250. def OAI.CycleClique.certificate_1221_part_19 line 508
  251. theorem OAI.CycleClique.certificate_1221_part_19_checked line 510
  252. def OAI.CycleClique.certificate_1221_part_18 line 512
  253. theorem OAI.CycleClique.certificate_1221_part_18_checked line 514
  254. def OAI.CycleClique.certificate_1221_part_16 line 516
  255. theorem OAI.CycleClique.certificate_1221_part_16_checked line 518
  256. def OAI.CycleClique.certificate_1221_part_15 line 520
  257. theorem OAI.CycleClique.certificate_1221_part_15_checked line 522
  258. def OAI.CycleClique.certificate_1221_part_14 line 524
  259. theorem OAI.CycleClique.certificate_1221_part_14_checked line 526
  260. def OAI.CycleClique.certificate_1221_part_13 line 528
  261. theorem OAI.CycleClique.certificate_1221_part_13_checked line 530
  262. def OAI.CycleClique.certificate_1221_part_11 line 532
  263. theorem OAI.CycleClique.certificate_1221_part_11_checked line 534
  264. def OAI.CycleClique.certificate_1221_part_10 line 536
  265. theorem OAI.CycleClique.certificate_1221_part_10_checked line 538
  266. def OAI.CycleClique.certificate_1221_part_9 line 540
  267. theorem OAI.CycleClique.certificate_1221_part_9_checked line 542
  268. def OAI.CycleClique.certificate_1221_part_8 line 544
  269. theorem OAI.CycleClique.certificate_1221_part_8_checked line 546
  270. def OAI.CycleClique.certificate_1221_part_7 line 548
  271. theorem OAI.CycleClique.certificate_1221_part_7_checked line 550
  272. def OAI.CycleClique.certificate_1221_part_6 line 552
  273. theorem OAI.CycleClique.certificate_1221_part_6_checked line 554
  274. def OAI.CycleClique.certificate_1221_part_5 line 556
  275. theorem OAI.CycleClique.certificate_1221_part_5_checked line 558
  276. def OAI.CycleClique.certificate_1221_part_4 line 560
  277. theorem OAI.CycleClique.certificate_1221_part_4_checked line 562
  278. def OAI.CycleClique.certificate_1221_part_3 line 564
  279. theorem OAI.CycleClique.certificate_1221_part_3_checked line 566
  280. def OAI.CycleClique.certificate_1221_part_2 line 568
  281. theorem OAI.CycleClique.certificate_1221_part_2_checked line 570
  282. def OAI.CycleClique.certificate_1221_part_1 line 572
  283. theorem OAI.CycleClique.certificate_1221_part_1_checked line 574
  284. def OAI.CycleClique.certificate_1221 line 576
  285. theorem OAI.CycleClique.certificate_1221_checked line 578
  286. theorem OAI.CycleClique.certificate_1221_valid line 580
  287. def OAI.CycleClique.certificate_1222_q line 582
  288. def OAI.CycleClique.certificate_1222_edges line 583
  289. def OAI.CycleClique.certificate_1222_part_0 line 585
  290. def OAI.CycleClique.certificate_1222_part_1 line 587
  291. def OAI.CycleClique.certificate_1222_part_2 line 589
  292. def OAI.CycleClique.certificate_1222_part_3 line 591
  293. def OAI.CycleClique.certificate_1222 line 593
  294. theorem OAI.CycleClique.certificate_1222_checked line 595
  295. theorem OAI.CycleClique.certificate_1222_valid line 596
  296. def OAI.CycleClique.certificate_1223_q line 598
  297. def OAI.CycleClique.certificate_1223_edges line 599
  298. def OAI.CycleClique.certificate_1223_part_0 line 601
  299. def OAI.CycleClique.certificate_1223_part_1 line 603
  300. def OAI.CycleClique.certificate_1223_part_2 line 605
  301. def OAI.CycleClique.certificate_1223_part_3 line 607
  302. def OAI.CycleClique.certificate_1223_part_4 line 609
  303. def OAI.CycleClique.certificate_1223 line 611
  304. theorem OAI.CycleClique.certificate_1223_checked line 613
  305. theorem OAI.CycleClique.certificate_1223_valid line 614
  306. def OAI.CycleClique.certificate_1224_q line 616
  307. def OAI.CycleClique.certificate_1224_edges line 617
  308. def OAI.CycleClique.certificate_1224_part_0 line 619
  309. def OAI.CycleClique.certificate_1224_part_1 line 621
  310. def OAI.CycleClique.certificate_1224_part_2 line 623
  311. def OAI.CycleClique.certificate_1224_part_3 line 625
  312. def OAI.CycleClique.certificate_1224_part_4 line 627
  313. def OAI.CycleClique.certificate_1224 line 629
  314. theorem OAI.CycleClique.certificate_1224_checked line 631
  315. theorem OAI.CycleClique.certificate_1224_valid line 632
  316. def OAI.CycleClique.certificate_1225_q line 634
  317. def OAI.CycleClique.certificate_1225_edges line 636
  318. def OAI.CycleClique.certificate_1225_E line 638
  319. def OAI.CycleClique.certificate_1225_M line 640
  320. def OAI.CycleClique.certificate_1225_part_1_E line 642
  321. def OAI.CycleClique.certificate_1225_part_1_M line 644
  322. def OAI.CycleClique.certificate_1225_part_2_E line 646
  323. def OAI.CycleClique.certificate_1225_part_2_M line 648
  324. def OAI.CycleClique.certificate_1225_part_3_E line 650
  325. def OAI.CycleClique.certificate_1225_part_3_M line 652
  326. def OAI.CycleClique.certificate_1225_part_4_E line 654
  327. def OAI.CycleClique.certificate_1225_part_4_M line 656
  328. def OAI.CycleClique.certificate_1225_part_5_E line 658
  329. def OAI.CycleClique.certificate_1225_part_5_M line 660
  330. def OAI.CycleClique.certificate_1225_part_6_E line 662
  331. def OAI.CycleClique.certificate_1225_part_6_M line 664
  332. def OAI.CycleClique.certificate_1225_part_7_E line 666
  333. def OAI.CycleClique.certificate_1225_part_7_M line 668
  334. def OAI.CycleClique.certificate_1225_part_8_E line 670
  335. def OAI.CycleClique.certificate_1225_part_8_M line 672
  336. def OAI.CycleClique.certificate_1225_part_9_E line 674
  337. def OAI.CycleClique.certificate_1225_part_9_M line 676
  338. def OAI.CycleClique.certificate_1225_part_10_E line 678
  339. def OAI.CycleClique.certificate_1225_part_10_M line 680
  340. def OAI.CycleClique.certificate_1225_part_11_E line 682
  341. def OAI.CycleClique.certificate_1225_part_11_M line 684
  342. def OAI.CycleClique.certificate_1225_part_12_E line 686
  343. def OAI.CycleClique.certificate_1225_part_12_M line 688
  344. def OAI.CycleClique.certificate_1225_part_12 line 690
  345. theorem OAI.CycleClique.certificate_1225_part_12_checked line 692
  346. def OAI.CycleClique.certificate_1225_part_13_E line 694
  347. def OAI.CycleClique.certificate_1225_part_13_M line 696
  348. def OAI.CycleClique.certificate_1225_part_14_E line 698
  349. def OAI.CycleClique.certificate_1225_part_14_M line 700
  350. def OAI.CycleClique.certificate_1225_part_15_E line 702
  351. def OAI.CycleClique.certificate_1225_part_15_M line 704
  352. def OAI.CycleClique.certificate_1225_part_16_E line 706
  353. def OAI.CycleClique.certificate_1225_part_16_M line 708
  354. def OAI.CycleClique.certificate_1225_part_17_E line 710
  355. def OAI.CycleClique.certificate_1225_part_17_M line 712
  356. def OAI.CycleClique.certificate_1225_part_18_E line 714
  357. def OAI.CycleClique.certificate_1225_part_18_M line 716
  358. def OAI.CycleClique.certificate_1225_part_19_E line 718
  359. def OAI.CycleClique.certificate_1225_part_19_M line 720
  360. def OAI.CycleClique.certificate_1225_part_20_E line 722
  361. def OAI.CycleClique.certificate_1225_part_20_M line 724
  362. def OAI.CycleClique.certificate_1225_part_21_E line 726
  363. def OAI.CycleClique.certificate_1225_part_21_M line 728
  364. def OAI.CycleClique.certificate_1225_part_22_E line 730
  365. def OAI.CycleClique.certificate_1225_part_22_M line 732
  366. def OAI.CycleClique.certificate_1225_part_22 line 734
  367. theorem OAI.CycleClique.certificate_1225_part_22_checked line 736
  368. def OAI.CycleClique.certificate_1225_part_21 line 738
  369. theorem OAI.CycleClique.certificate_1225_part_21_checked line 740
  370. def OAI.CycleClique.certificate_1225_part_23_E line 742
  371. def OAI.CycleClique.certificate_1225_part_23_M line 744
  372. def OAI.CycleClique.certificate_1225_part_24_E line 746
  373. def OAI.CycleClique.certificate_1225_part_24_M line 748
  374. def OAI.CycleClique.certificate_1225_part_25_E line 750
  375. def OAI.CycleClique.certificate_1225_part_25_M line 752
  376. def OAI.CycleClique.certificate_1225_part_26_E line 754
  377. def OAI.CycleClique.certificate_1225_part_26_M line 756
  378. def OAI.CycleClique.certificate_1225_part_27_E line 758
  379. def OAI.CycleClique.certificate_1225_part_27_M line 760
  380. def OAI.CycleClique.certificate_1225_part_28_E line 762
  381. def OAI.CycleClique.certificate_1225_part_28_M line 764
  382. def OAI.CycleClique.certificate_1225_part_29_E line 766
  383. def OAI.CycleClique.certificate_1225_part_29_M line 768
  384. def OAI.CycleClique.certificate_1225_part_29 line 770
  385. theorem OAI.CycleClique.certificate_1225_part_29_checked line 772
  386. def OAI.CycleClique.certificate_1225_part_28 line 774
  387. theorem OAI.CycleClique.certificate_1225_part_28_checked line 776
  388. def OAI.CycleClique.certificate_1225_part_27 line 778
  389. theorem OAI.CycleClique.certificate_1225_part_27_checked line 780
  390. def OAI.CycleClique.certificate_1225_part_30_E line 782
  391. def OAI.CycleClique.certificate_1225_part_30_M line 784
  392. def OAI.CycleClique.certificate_1225_part_31_E line 786
  393. def OAI.CycleClique.certificate_1225_part_31_M line 788
  394. def OAI.CycleClique.certificate_1225_part_32_E line 790
  395. def OAI.CycleClique.certificate_1225_part_32_M line 792
  396. def OAI.CycleClique.certificate_1225_part_32 line 794
  397. theorem OAI.CycleClique.certificate_1225_part_32_checked line 796
  398. def OAI.CycleClique.certificate_1225_part_31 line 798
  399. theorem OAI.CycleClique.certificate_1225_part_31_checked line 800
  400. def OAI.CycleClique.certificate_1225_part_33_E line 802
  401. def OAI.CycleClique.certificate_1225_part_33_M line 804
  402. def OAI.CycleClique.certificate_1225_part_34_E line 806
  403. def OAI.CycleClique.certificate_1225_part_34_M line 808
  404. def OAI.CycleClique.certificate_1225_part_35_E line 810
  405. def OAI.CycleClique.certificate_1225_part_35_M line 812
  406. def OAI.CycleClique.certificate_1225_part_35 line 814
  407. theorem OAI.CycleClique.certificate_1225_part_35_checked line 816
  408. def OAI.CycleClique.certificate_1225_part_34 line 818
  409. theorem OAI.CycleClique.certificate_1225_part_34_checked line 820
  410. def OAI.CycleClique.certificate_1225_part_33 line 822
  411. theorem OAI.CycleClique.certificate_1225_part_33_checked line 824
  412. def OAI.CycleClique.certificate_1225_part_36_E line 826
  413. def OAI.CycleClique.certificate_1225_part_36_M line 828
  414. def OAI.CycleClique.certificate_1225_part_37_E line 830
  415. def OAI.CycleClique.certificate_1225_part_37_M line 832
  416. def OAI.CycleClique.certificate_1225_part_38_E line 834
  417. def OAI.CycleClique.certificate_1225_part_38_M line 836
  418. def OAI.CycleClique.certificate_1225_part_38 line 838
  419. theorem OAI.CycleClique.certificate_1225_part_38_checked line 840
  420. def OAI.CycleClique.certificate_1225_part_39_E line 842
  421. def OAI.CycleClique.certificate_1225_part_39_M line 844
  422. def OAI.CycleClique.certificate_1225_part_40_E line 846
  423. def OAI.CycleClique.certificate_1225_part_40_M line 848
  424. def OAI.CycleClique.certificate_1225_part_41_E line 850
  425. def OAI.CycleClique.certificate_1225_part_41_M line 852
  426. def OAI.CycleClique.certificate_1225_part_42_E line 854
  427. def OAI.CycleClique.certificate_1225_part_42_M line 856
  428. def OAI.CycleClique.certificate_1225_part_42 line 858
  429. theorem OAI.CycleClique.certificate_1225_part_42_checked line 860
  430. def OAI.CycleClique.certificate_1225_part_43_E line 862
  431. def OAI.CycleClique.certificate_1225_part_43_M line 864
  432. def OAI.CycleClique.certificate_1225_part_44_E line 866
  433. def OAI.CycleClique.certificate_1225_part_44_M line 868
  434. def OAI.CycleClique.certificate_1225_part_45_E line 870
  435. def OAI.CycleClique.certificate_1225_part_45_M line 872
  436. def OAI.CycleClique.certificate_1225_part_45 line 874
  437. theorem OAI.CycleClique.certificate_1225_part_45_checked line 876
  438. def OAI.CycleClique.certificate_1225_part_44 line 878
  439. theorem OAI.CycleClique.certificate_1225_part_44_checked line 880
  440. def OAI.CycleClique.certificate_1225_part_46_E line 882
  441. def OAI.CycleClique.certificate_1225_part_46_M line 884
  442. def OAI.CycleClique.certificate_1225_part_47_E line 886
  443. def OAI.CycleClique.certificate_1225_part_47_M line 888
  444. def OAI.CycleClique.certificate_1225_part_48_E line 890
  445. def OAI.CycleClique.certificate_1225_part_48_M line 892
  446. def OAI.CycleClique.certificate_1225_part_49_E line 894
  447. def OAI.CycleClique.certificate_1225_part_49_M line 896
  448. def OAI.CycleClique.certificate_1225_part_50_E line 898
  449. def OAI.CycleClique.certificate_1225_part_50_M line 900
  450. def OAI.CycleClique.certificate_1225_part_50 line 902
  451. theorem OAI.CycleClique.certificate_1225_part_50_checked line 904
  452. def OAI.CycleClique.certificate_1225_part_49 line 906
  453. theorem OAI.CycleClique.certificate_1225_part_49_checked line 908
  454. def OAI.CycleClique.certificate_1225_part_51_E line 910
  455. def OAI.CycleClique.certificate_1225_part_51_M line 912
  456. def OAI.CycleClique.certificate_1225_part_51 line 914
  457. theorem OAI.CycleClique.certificate_1225_part_51_checked line 916
  458. def OAI.CycleClique.certificate_1225_part_52_E line 918
  459. def OAI.CycleClique.certificate_1225_part_52_M line 920
  460. def OAI.CycleClique.certificate_1225_part_53_E line 922
  461. def OAI.CycleClique.certificate_1225_part_53_M line 924
  462. def OAI.CycleClique.certificate_1225_part_53 line 926
  463. theorem OAI.CycleClique.certificate_1225_part_53_checked line 928
  464. def OAI.CycleClique.certificate_1225_part_52 line 930
  465. theorem OAI.CycleClique.certificate_1225_part_52_checked line 932
  466. def OAI.CycleClique.certificate_1225_part_54_E line 934
  467. def OAI.CycleClique.certificate_1225_part_54_M line 936
  468. def OAI.CycleClique.certificate_1225_part_55_E line 938
  469. def OAI.CycleClique.certificate_1225_part_55_M line 940
  470. def OAI.CycleClique.certificate_1225_part_55 line 942
  471. theorem OAI.CycleClique.certificate_1225_part_55_checked line 944
  472. def OAI.CycleClique.certificate_1225_part_54 line 946
  473. theorem OAI.CycleClique.certificate_1225_part_54_checked line 948
  474. def OAI.CycleClique.certificate_1225_part_56_E line 950
  475. def OAI.CycleClique.certificate_1225_part_56_M line 952
  476. def OAI.CycleClique.certificate_1225_part_56 line 954
  477. theorem OAI.CycleClique.certificate_1225_part_56_checked line 956
  478. def OAI.CycleClique.certificate_1225_part_57_E line 958
  479. def OAI.CycleClique.certificate_1225_part_57_M line 960
  480. def OAI.CycleClique.certificate_1225_part_58_E line 962
  481. def OAI.CycleClique.certificate_1225_part_58_M line 964
  482. def OAI.CycleClique.certificate_1225_part_58 line 966
  483. theorem OAI.CycleClique.certificate_1225_part_58_checked line 968
  484. def OAI.CycleClique.certificate_1225_part_57 line 970
  485. theorem OAI.CycleClique.certificate_1225_part_57_checked line 972
  486. def OAI.CycleClique.certificate_1225_part_59_E line 974
  487. def OAI.CycleClique.certificate_1225_part_59_M line 976
  488. def OAI.CycleClique.certificate_1225_part_60_E line 978
  489. def OAI.CycleClique.certificate_1225_part_60_M line 980
  490. def OAI.CycleClique.certificate_1225_part_61_E line 982
  491. def OAI.CycleClique.certificate_1225_part_61_M line 984
  492. def OAI.CycleClique.certificate_1225_part_61 line 986
  493. theorem OAI.CycleClique.certificate_1225_part_61_checked line 988
  494. def OAI.CycleClique.certificate_1225_part_62_E line 990
  495. def OAI.CycleClique.certificate_1225_part_62_M line 992
  496. def OAI.CycleClique.certificate_1225_part_63_E line 994
  497. def OAI.CycleClique.certificate_1225_part_63_M line 996
  498. def OAI.CycleClique.certificate_1225_part_63 line 998
  499. theorem OAI.CycleClique.certificate_1225_part_63_checked line 1000
  500. def OAI.CycleClique.certificate_1225_part_62 line 1002
  501. theorem OAI.CycleClique.certificate_1225_part_62_checked line 1004
  502. def OAI.CycleClique.certificate_1225_part_64_E line 1006
  503. def OAI.CycleClique.certificate_1225_part_64_M line 1008
  504. def OAI.CycleClique.certificate_1225_part_65_E line 1010
  505. def OAI.CycleClique.certificate_1225_part_65_M line 1012
  506. def OAI.CycleClique.certificate_1225_part_65 line 1014
  507. theorem OAI.CycleClique.certificate_1225_part_65_checked line 1016
  508. def OAI.CycleClique.certificate_1225_part_64 line 1018
  509. theorem OAI.CycleClique.certificate_1225_part_64_checked line 1020
  510. def OAI.CycleClique.certificate_1225_part_66_E line 1022
  511. def OAI.CycleClique.certificate_1225_part_66_M line 1024
  512. def OAI.CycleClique.certificate_1225_part_67_E line 1026
  513. def OAI.CycleClique.certificate_1225_part_67_M line 1028
  514. def OAI.CycleClique.certificate_1225_part_67 line 1030
  515. theorem OAI.CycleClique.certificate_1225_part_67_checked line 1032
  516. def OAI.CycleClique.certificate_1225_part_68_E line 1034
  517. def OAI.CycleClique.certificate_1225_part_68_M line 1036
  518. def OAI.CycleClique.certificate_1225_part_69_E line 1038
  519. def OAI.CycleClique.certificate_1225_part_69_M line 1040
  520. def OAI.CycleClique.certificate_1225_part_69 line 1042
  521. theorem OAI.CycleClique.certificate_1225_part_69_checked line 1044
  522. def OAI.CycleClique.certificate_1225_part_68 line 1046
  523. theorem OAI.CycleClique.certificate_1225_part_68_checked line 1048
  524. def OAI.CycleClique.certificate_1225_part_70_E line 1050
  525. def OAI.CycleClique.certificate_1225_part_70_M line 1052
  526. def OAI.CycleClique.certificate_1225_part_71_E line 1054
  527. def OAI.CycleClique.certificate_1225_part_71_M line 1056
  528. def OAI.CycleClique.certificate_1225_part_71 line 1058
  529. theorem OAI.CycleClique.certificate_1225_part_71_checked line 1060
  530. def OAI.CycleClique.certificate_1225_part_70 line 1062
  531. theorem OAI.CycleClique.certificate_1225_part_70_checked line 1064
  532. def OAI.CycleClique.certificate_1225_part_72_E line 1066
  533. def OAI.CycleClique.certificate_1225_part_72_M line 1068
  534. def OAI.CycleClique.certificate_1225_part_72 line 1070
  535. theorem OAI.CycleClique.certificate_1225_part_72_checked line 1072
  536. def OAI.CycleClique.certificate_1225_part_73_E line 1074
  537. def OAI.CycleClique.certificate_1225_part_73_M line 1076
  538. def OAI.CycleClique.certificate_1225_part_74_E line 1078
  539. def OAI.CycleClique.certificate_1225_part_74_M line 1080
  540. def OAI.CycleClique.certificate_1225_part_74 line 1082
  541. theorem OAI.CycleClique.certificate_1225_part_74_checked line 1084
  542. def OAI.CycleClique.certificate_1225_part_73 line 1086
  543. theorem OAI.CycleClique.certificate_1225_part_73_checked line 1088
  544. def OAI.CycleClique.certificate_1225_part_75_E line 1090
  545. def OAI.CycleClique.certificate_1225_part_75_M line 1092
  546. def OAI.CycleClique.certificate_1225_part_76_E line 1094
  547. def OAI.CycleClique.certificate_1225_part_76_M line 1096
  548. def OAI.CycleClique.certificate_1225_part_76 line 1098
  549. theorem OAI.CycleClique.certificate_1225_part_76_checked line 1100
  550. def OAI.CycleClique.certificate_1225_part_77_E line 1102
  551. def OAI.CycleClique.certificate_1225_part_77_M line 1104
  552. def OAI.CycleClique.certificate_1225_part_78_E line 1106
  553. def OAI.CycleClique.certificate_1225_part_78_M line 1108
  554. def OAI.CycleClique.certificate_1225_part_79_E line 1110
  555. def OAI.CycleClique.certificate_1225_part_79_M line 1112
  556. def OAI.CycleClique.certificate_1225_part_80_E line 1114
  557. def OAI.CycleClique.certificate_1225_part_80_M line 1116
  558. def OAI.CycleClique.certificate_1225_part_81_E line 1118
  559. def OAI.CycleClique.certificate_1225_part_81_M line 1120
  560. def OAI.CycleClique.certificate_1225_part_82_E line 1122
  561. def OAI.CycleClique.certificate_1225_part_82_M line 1124
  562. def OAI.CycleClique.certificate_1225_part_82 line 1126
  563. theorem OAI.CycleClique.certificate_1225_part_82_checked line 1128
  564. def OAI.CycleClique.certificate_1225_part_81 line 1130
  565. theorem OAI.CycleClique.certificate_1225_part_81_checked line 1132
  566. def OAI.CycleClique.certificate_1225_part_80 line 1134
  567. theorem OAI.CycleClique.certificate_1225_part_80_checked line 1136
  568. def OAI.CycleClique.certificate_1225_part_79 line 1138
  569. theorem OAI.CycleClique.certificate_1225_part_79_checked line 1140
  570. def OAI.CycleClique.certificate_1225_part_83_E line 1142
  571. def OAI.CycleClique.certificate_1225_part_83_M line 1144
  572. def OAI.CycleClique.certificate_1225_part_84_E line 1146
  573. def OAI.CycleClique.certificate_1225_part_84_M line 1148
  574. def OAI.CycleClique.certificate_1225_part_85_E line 1150
  575. def OAI.CycleClique.certificate_1225_part_85_M line 1152
  576. def OAI.CycleClique.certificate_1225_part_85 line 1154
  577. theorem OAI.CycleClique.certificate_1225_part_85_checked line 1156
  578. def OAI.CycleClique.certificate_1225_part_84 line 1158
  579. theorem OAI.CycleClique.certificate_1225_part_84_checked line 1160
  580. def OAI.CycleClique.certificate_1225_part_83 line 1162
  581. theorem OAI.CycleClique.certificate_1225_part_83_checked line 1164
  582. def OAI.CycleClique.certificate_1225_part_86_E line 1166
  583. def OAI.CycleClique.certificate_1225_part_86_M line 1168
  584. def OAI.CycleClique.certificate_1225_part_87_E line 1170
  585. def OAI.CycleClique.certificate_1225_part_87_M line 1172
  586. def OAI.CycleClique.certificate_1225_part_87 line 1174
  587. theorem OAI.CycleClique.certificate_1225_part_87_checked line 1176
  588. def OAI.CycleClique.certificate_1225_part_86 line 1178
  589. theorem OAI.CycleClique.certificate_1225_part_86_checked line 1180
  590. def OAI.CycleClique.certificate_1225_part_88_E line 1182
  591. def OAI.CycleClique.certificate_1225_part_88_M line 1184
  592. def OAI.CycleClique.certificate_1225_part_89_E line 1186
  593. def OAI.CycleClique.certificate_1225_part_89_M line 1188
  594. def OAI.CycleClique.certificate_1225_part_89 line 1190
  595. theorem OAI.CycleClique.certificate_1225_part_89_checked line 1192
  596. def OAI.CycleClique.certificate_1225_part_88 line 1194
  597. theorem OAI.CycleClique.certificate_1225_part_88_checked line 1196
  598. def OAI.CycleClique.certificate_1225_part_90_E line 1198
  599. def OAI.CycleClique.certificate_1225_part_90_M line 1200
  600. def OAI.CycleClique.certificate_1225_part_91_E line 1202
  601. def OAI.CycleClique.certificate_1225_part_91_M line 1204
  602. def OAI.CycleClique.certificate_1225_part_91 line 1206
  603. theorem OAI.CycleClique.certificate_1225_part_91_checked line 1208
  604. def OAI.CycleClique.certificate_1225_part_92_E line 1210
  605. def OAI.CycleClique.certificate_1225_part_92_M line 1212
  606. def OAI.CycleClique.certificate_1225_part_92 line 1214
  607. theorem OAI.CycleClique.certificate_1225_part_92_checked line 1216
  608. def OAI.CycleClique.certificate_1225_part_93_E line 1218
  609. def OAI.CycleClique.certificate_1225_part_93_M line 1220
  610. def OAI.CycleClique.certificate_1225_part_94_E line 1222
  611. def OAI.CycleClique.certificate_1225_part_94_M line 1224
  612. def OAI.CycleClique.certificate_1225_part_94 line 1226
  613. theorem OAI.CycleClique.certificate_1225_part_94_checked line 1228
  614. def OAI.CycleClique.certificate_1225_part_93 line 1230
  615. theorem OAI.CycleClique.certificate_1225_part_93_checked line 1232
  616. def OAI.CycleClique.certificate_1225_part_95_E line 1234
  617. def OAI.CycleClique.certificate_1225_part_95_M line 1236
  618. def OAI.CycleClique.certificate_1225_part_96_E line 1238
  619. def OAI.CycleClique.certificate_1225_part_96_M line 1240
  620. def OAI.CycleClique.certificate_1225_part_96 line 1242
  621. theorem OAI.CycleClique.certificate_1225_part_96_checked line 1244
  622. def OAI.CycleClique.certificate_1225_part_95 line 1246
  623. theorem OAI.CycleClique.certificate_1225_part_95_checked line 1248
  624. def OAI.CycleClique.certificate_1225_part_97_E line 1250
  625. def OAI.CycleClique.certificate_1225_part_97_M line 1252
  626. def OAI.CycleClique.certificate_1225_part_98_E line 1254
  627. def OAI.CycleClique.certificate_1225_part_98_M line 1256
  628. def OAI.CycleClique.certificate_1225_part_98 line 1258
  629. theorem OAI.CycleClique.certificate_1225_part_98_checked line 1260
  630. def OAI.CycleClique.certificate_1225_part_97 line 1262
  631. theorem OAI.CycleClique.certificate_1225_part_97_checked line 1264
  632. def OAI.CycleClique.certificate_1225_part_99_E line 1266
  633. def OAI.CycleClique.certificate_1225_part_99_M line 1268
  634. def OAI.CycleClique.certificate_1225_part_100_E line 1270
  635. def OAI.CycleClique.certificate_1225_part_100_M line 1272
  636. def OAI.CycleClique.certificate_1225_part_101_E line 1274
  637. def OAI.CycleClique.certificate_1225_part_101_M line 1276
  638. def OAI.CycleClique.certificate_1225_part_102_E line 1278
  639. def OAI.CycleClique.certificate_1225_part_102_M line 1280
  640. def OAI.CycleClique.certificate_1225_part_103_E line 1282
  641. def OAI.CycleClique.certificate_1225_part_103_M line 1284
  642. def OAI.CycleClique.certificate_1225_part_104_E line 1286
  643. def OAI.CycleClique.certificate_1225_part_104_M line 1288
  644. def OAI.CycleClique.certificate_1225_part_105_E line 1290
  645. def OAI.CycleClique.certificate_1225_part_105_M line 1292
  646. def OAI.CycleClique.certificate_1225_part_106_E line 1294
  647. def OAI.CycleClique.certificate_1225_part_106_M line 1296
  648. def OAI.CycleClique.certificate_1225_part_106 line 1298
  649. theorem OAI.CycleClique.certificate_1225_part_106_checked line 1300
  650. def OAI.CycleClique.certificate_1225_part_105 line 1302
  651. theorem OAI.CycleClique.certificate_1225_part_105_checked line 1304
  652. def OAI.CycleClique.certificate_1225_part_104 line 1306
  653. theorem OAI.CycleClique.certificate_1225_part_104_checked line 1308
  654. def OAI.CycleClique.certificate_1225_part_103 line 1310
  655. theorem OAI.CycleClique.certificate_1225_part_103_checked line 1312
  656. def OAI.CycleClique.certificate_1225_part_102 line 1314
  657. theorem OAI.CycleClique.certificate_1225_part_102_checked line 1316
  658. def OAI.CycleClique.certificate_1225_part_101 line 1318
  659. theorem OAI.CycleClique.certificate_1225_part_101_checked line 1320
  660. def OAI.CycleClique.certificate_1225_part_107_E line 1322
  661. def OAI.CycleClique.certificate_1225_part_107_M line 1324
  662. def OAI.CycleClique.certificate_1225_part_108_E line 1326
  663. def OAI.CycleClique.certificate_1225_part_108_M line 1328
  664. def OAI.CycleClique.certificate_1225_part_109_E line 1330
  665. def OAI.CycleClique.certificate_1225_part_109_M line 1332
  666. def OAI.CycleClique.certificate_1225_part_110_E line 1334
  667. def OAI.CycleClique.certificate_1225_part_110_M line 1336
  668. def OAI.CycleClique.certificate_1225_part_111_E line 1338
  669. def OAI.CycleClique.certificate_1225_part_111_M line 1340
  670. def OAI.CycleClique.certificate_1225_part_112_E line 1342
  671. def OAI.CycleClique.certificate_1225_part_112_M line 1344
  672. def OAI.CycleClique.certificate_1225_part_113_E line 1346
  673. def OAI.CycleClique.certificate_1225_part_113_M line 1348
  674. def OAI.CycleClique.certificate_1225_part_114_E line 1350
  675. def OAI.CycleClique.certificate_1225_part_114_M line 1352
  676. def OAI.CycleClique.certificate_1225_part_114 line 1354
  677. theorem OAI.CycleClique.certificate_1225_part_114_checked line 1356
  678. def OAI.CycleClique.certificate_1225_part_113 line 1358
  679. theorem OAI.CycleClique.certificate_1225_part_113_checked line 1360
  680. def OAI.CycleClique.certificate_1225_part_112 line 1362
  681. theorem OAI.CycleClique.certificate_1225_part_112_checked line 1364
  682. def OAI.CycleClique.certificate_1225_part_111 line 1366
  683. theorem OAI.CycleClique.certificate_1225_part_111_checked line 1368
  684. def OAI.CycleClique.certificate_1225_part_110 line 1370
  685. theorem OAI.CycleClique.certificate_1225_part_110_checked line 1372
  686. def OAI.CycleClique.certificate_1225_part_109 line 1374
  687. theorem OAI.CycleClique.certificate_1225_part_109_checked line 1376
  688. def OAI.CycleClique.certificate_1225_part_115_E line 1378
  689. def OAI.CycleClique.certificate_1225_part_115_M line 1380
  690. def OAI.CycleClique.certificate_1225_part_115 line 1382
  691. theorem OAI.CycleClique.certificate_1225_part_115_checked line 1384
  692. def OAI.CycleClique.certificate_1225_part_108 line 1386
  693. theorem OAI.CycleClique.certificate_1225_part_108_checked line 1388
  694. def OAI.CycleClique.certificate_1225_part_107 line 1390
  695. theorem OAI.CycleClique.certificate_1225_part_107_checked line 1392
  696. def OAI.CycleClique.certificate_1225_part_100 line 1394
  697. theorem OAI.CycleClique.certificate_1225_part_100_checked line 1396
  698. def OAI.CycleClique.certificate_1225_part_99 line 1398
  699. theorem OAI.CycleClique.certificate_1225_part_99_checked line 1400
  700. def OAI.CycleClique.certificate_1225_part_90 line 1402
  701. theorem OAI.CycleClique.certificate_1225_part_90_checked line 1404
  702. def OAI.CycleClique.certificate_1225_part_78 line 1406
  703. theorem OAI.CycleClique.certificate_1225_part_78_checked line 1408
  704. def OAI.CycleClique.certificate_1225_part_77 line 1410
  705. theorem OAI.CycleClique.certificate_1225_part_77_checked line 1412
  706. def OAI.CycleClique.certificate_1225_part_75 line 1414
  707. theorem OAI.CycleClique.certificate_1225_part_75_checked line 1416
  708. def OAI.CycleClique.certificate_1225_part_66 line 1418
  709. theorem OAI.CycleClique.certificate_1225_part_66_checked line 1420
  710. def OAI.CycleClique.certificate_1225_part_60 line 1422
  711. theorem OAI.CycleClique.certificate_1225_part_60_checked line 1424
  712. def OAI.CycleClique.certificate_1225_part_59 line 1426
  713. theorem OAI.CycleClique.certificate_1225_part_59_checked line 1428
  714. def OAI.CycleClique.certificate_1225_part_48 line 1430
  715. theorem OAI.CycleClique.certificate_1225_part_48_checked line 1432
  716. def OAI.CycleClique.certificate_1225_part_47 line 1434
  717. theorem OAI.CycleClique.certificate_1225_part_47_checked line 1436
  718. def OAI.CycleClique.certificate_1225_part_46 line 1438
  719. theorem OAI.CycleClique.certificate_1225_part_46_checked line 1440
  720. def OAI.CycleClique.certificate_1225_part_43 line 1442
  721. theorem OAI.CycleClique.certificate_1225_part_43_checked line 1444
  722. def OAI.CycleClique.certificate_1225_part_41 line 1446
  723. theorem OAI.CycleClique.certificate_1225_part_41_checked line 1448
  724. def OAI.CycleClique.certificate_1225_part_40 line 1450
  725. theorem OAI.CycleClique.certificate_1225_part_40_checked line 1452
  726. def OAI.CycleClique.certificate_1225_part_39 line 1454
  727. theorem OAI.CycleClique.certificate_1225_part_39_checked line 1456
  728. def OAI.CycleClique.certificate_1225_part_37 line 1458
  729. theorem OAI.CycleClique.certificate_1225_part_37_checked line 1460
  730. def OAI.CycleClique.certificate_1225_part_36 line 1462
  731. theorem OAI.CycleClique.certificate_1225_part_36_checked line 1464
  732. def OAI.CycleClique.certificate_1225_part_30 line 1466
  733. theorem OAI.CycleClique.certificate_1225_part_30_checked line 1468
  734. def OAI.CycleClique.certificate_1225_part_26 line 1470
  735. theorem OAI.CycleClique.certificate_1225_part_26_checked line 1472
  736. def OAI.CycleClique.certificate_1225_part_25 line 1474
  737. theorem OAI.CycleClique.certificate_1225_part_25_checked line 1476
  738. def OAI.CycleClique.certificate_1225_part_24 line 1478
  739. theorem OAI.CycleClique.certificate_1225_part_24_checked line 1480
  740. def OAI.CycleClique.certificate_1225_part_23 line 1482
  741. theorem OAI.CycleClique.certificate_1225_part_23_checked line 1484
  742. def OAI.CycleClique.certificate_1225_part_20 line 1486
  743. theorem OAI.CycleClique.certificate_1225_part_20_checked line 1488
  744. def OAI.CycleClique.certificate_1225_part_19 line 1490
  745. theorem OAI.CycleClique.certificate_1225_part_19_checked line 1492
  746. def OAI.CycleClique.certificate_1225_part_18 line 1494
  747. theorem OAI.CycleClique.certificate_1225_part_18_checked line 1496
  748. def OAI.CycleClique.certificate_1225_part_17 line 1498
  749. theorem OAI.CycleClique.certificate_1225_part_17_checked line 1500
  750. def OAI.CycleClique.certificate_1225_part_16 line 1502
  751. theorem OAI.CycleClique.certificate_1225_part_16_checked line 1504
  752. def OAI.CycleClique.certificate_1225_part_15 line 1506
  753. theorem OAI.CycleClique.certificate_1225_part_15_checked line 1508
  754. def OAI.CycleClique.certificate_1225_part_14 line 1510
  755. theorem OAI.CycleClique.certificate_1225_part_14_checked line 1512
  756. def OAI.CycleClique.certificate_1225_part_13 line 1514
  757. theorem OAI.CycleClique.certificate_1225_part_13_checked line 1516
  758. def OAI.CycleClique.certificate_1225_part_11 line 1518
  759. theorem OAI.CycleClique.certificate_1225_part_11_checked line 1520
  760. def OAI.CycleClique.certificate_1225_part_10 line 1522
  761. theorem OAI.CycleClique.certificate_1225_part_10_checked line 1524
  762. def OAI.CycleClique.certificate_1225_part_9 line 1526
  763. theorem OAI.CycleClique.certificate_1225_part_9_checked line 1528
  764. def OAI.CycleClique.certificate_1225_part_8 line 1530
  765. theorem OAI.CycleClique.certificate_1225_part_8_checked line 1532
  766. def OAI.CycleClique.certificate_1225_part_7 line 1534
  767. theorem OAI.CycleClique.certificate_1225_part_7_checked line 1536
  768. def OAI.CycleClique.certificate_1225_part_6 line 1538
  769. theorem OAI.CycleClique.certificate_1225_part_6_checked line 1540
  770. def OAI.CycleClique.certificate_1225_part_5 line 1542
  771. theorem OAI.CycleClique.certificate_1225_part_5_checked line 1544
  772. def OAI.CycleClique.certificate_1225_part_4 line 1546
  773. theorem OAI.CycleClique.certificate_1225_part_4_checked line 1548
  774. def OAI.CycleClique.certificate_1225_part_3 line 1550
  775. theorem OAI.CycleClique.certificate_1225_part_3_checked line 1552
  776. def OAI.CycleClique.certificate_1225_part_2 line 1554
  777. theorem OAI.CycleClique.certificate_1225_part_2_checked line 1556
  778. def OAI.CycleClique.certificate_1225_part_1 line 1558
  779. theorem OAI.CycleClique.certificate_1225_part_1_checked line 1560
  780. def OAI.CycleClique.certificate_1225 line 1562
  781. theorem OAI.CycleClique.certificate_1225_checked line 1564
  782. theorem OAI.CycleClique.certificate_1225_valid line 1566
  783. def OAI.CycleClique.certificate_1226_q line 1568
  784. def OAI.CycleClique.certificate_1226_edges line 1569
  785. def OAI.CycleClique.certificate_1226_part_0 line 1571
  786. def OAI.CycleClique.certificate_1226_part_1 line 1573
  787. def OAI.CycleClique.certificate_1226_part_2 line 1575
  788. def OAI.CycleClique.certificate_1226_part_3 line 1577
  789. def OAI.CycleClique.certificate_1226 line 1579
  790. theorem OAI.CycleClique.certificate_1226_checked line 1581
  791. theorem OAI.CycleClique.certificate_1226_valid line 1582
  792. def OAI.CycleClique.certificate_1227_q line 1584
  793. def OAI.CycleClique.certificate_1227_edges line 1585
  794. def OAI.CycleClique.certificate_1227_part_0 line 1587
  795. def OAI.CycleClique.certificate_1227_part_1 line 1589
  796. def OAI.CycleClique.certificate_1227_part_2 line 1591
  797. def OAI.CycleClique.certificate_1227_part_3 line 1593
  798. def OAI.CycleClique.certificate_1227 line 1595
  799. theorem OAI.CycleClique.certificate_1227_checked line 1597
  800. theorem OAI.CycleClique.certificate_1227_valid line 1598
  801. def OAI.CycleClique.certificate_1228_q line 1600
  802. def OAI.CycleClique.certificate_1228_edges line 1601
  803. def OAI.CycleClique.certificate_1228_part_0 line 1603
  804. def OAI.CycleClique.certificate_1228_part_1 line 1605
  805. def OAI.CycleClique.certificate_1228_part_2 line 1607
  806. def OAI.CycleClique.certificate_1228_part_3 line 1609
  807. def OAI.CycleClique.certificate_1228 line 1611
  808. theorem OAI.CycleClique.certificate_1228_checked line 1613
  809. theorem OAI.CycleClique.certificate_1228_valid line 1614
  810. def OAI.CycleClique.certificate_1229_q line 1616
  811. def OAI.CycleClique.certificate_1229_edges line 1617
  812. def OAI.CycleClique.certificate_1229_part_0 line 1619
  813. def OAI.CycleClique.certificate_1229_part_1 line 1621
  814. def OAI.CycleClique.certificate_1229_part_2 line 1623
  815. def OAI.CycleClique.certificate_1229_part_3 line 1625
  816. def OAI.CycleClique.certificate_1229 line 1627
  817. theorem OAI.CycleClique.certificate_1229_checked line 1629
  818. theorem OAI.CycleClique.certificate_1229_valid line 1630
  819. def OAI.CycleClique.certificate_1230_q line 1632
  820. def OAI.CycleClique.certificate_1230_edges line 1633
  821. def OAI.CycleClique.certificate_1230_part_0 line 1635
  822. def OAI.CycleClique.certificate_1230_part_1 line 1637
  823. def OAI.CycleClique.certificate_1230_part_2 line 1639
  824. def OAI.CycleClique.certificate_1230_part_3 line 1641
  825. def OAI.CycleClique.certificate_1230 line 1643
  826. theorem OAI.CycleClique.certificate_1230_checked line 1645
  827. theorem OAI.CycleClique.certificate_1230_valid line 1646
  828. def OAI.CycleClique.certificate_1231_q line 1648
  829. def OAI.CycleClique.certificate_1231_edges line 1649
  830. def OAI.CycleClique.certificate_1231_part_0 line 1651
  831. def OAI.CycleClique.certificate_1231_part_1 line 1653
  832. def OAI.CycleClique.certificate_1231_part_2 line 1655
  833. def OAI.CycleClique.certificate_1231_part_3 line 1657
  834. def OAI.CycleClique.certificate_1231_part_4 line 1659
  835. def OAI.CycleClique.certificate_1231 line 1661
  836. theorem OAI.CycleClique.certificate_1231_checked line 1663
  837. theorem OAI.CycleClique.certificate_1231_valid line 1664
  838. def OAI.CycleClique.certificate_1232_q line 1666
  839. def OAI.CycleClique.certificate_1232_edges line 1667
  840. def OAI.CycleClique.certificate_1232_part_0 line 1669
  841. def OAI.CycleClique.certificate_1232_part_1 line 1671
  842. def OAI.CycleClique.certificate_1232_part_2 line 1673
  843. def OAI.CycleClique.certificate_1232_part_3 line 1675
  844. def OAI.CycleClique.certificate_1232 line 1677
  845. theorem OAI.CycleClique.certificate_1232_checked line 1679
  846. theorem OAI.CycleClique.certificate_1232_valid line 1680
  847. def OAI.CycleClique.certificate_1233_q line 1682
  848. def OAI.CycleClique.certificate_1233_edges line 1683
  849. def OAI.CycleClique.certificate_1233_part_0 line 1685
  850. def OAI.CycleClique.certificate_1233_part_1 line 1687
  851. def OAI.CycleClique.certificate_1233_part_2 line 1689
  852. def OAI.CycleClique.certificate_1233_part_3 line 1691
  853. def OAI.CycleClique.certificate_1233 line 1693
  854. theorem OAI.CycleClique.certificate_1233_checked line 1695
  855. theorem OAI.CycleClique.certificate_1233_valid line 1696
  856. def OAI.CycleClique.certificate_1234_q line 1698
  857. def OAI.CycleClique.certificate_1234_edges line 1699
  858. def OAI.CycleClique.certificate_1234_part_0 line 1701
  859. def OAI.CycleClique.certificate_1234_part_1 line 1703
  860. def OAI.CycleClique.certificate_1234_part_2 line 1705
  861. def OAI.CycleClique.certificate_1234_part_3 line 1707
  862. def OAI.CycleClique.certificate_1234 line 1709
  863. theorem OAI.CycleClique.certificate_1234_checked line 1711
  864. theorem OAI.CycleClique.certificate_1234_valid line 1712
  865. def OAI.CycleClique.certificate_1235_q line 1714
  866. def OAI.CycleClique.certificate_1235_edges line 1715
  867. def OAI.CycleClique.certificate_1235_part_0 line 1717
  868. def OAI.CycleClique.certificate_1235_part_1 line 1719
  869. def OAI.CycleClique.certificate_1235_part_2 line 1721
  870. def OAI.CycleClique.certificate_1235_part_3 line 1723
  871. def OAI.CycleClique.certificate_1235_part_4 line 1725
  872. def OAI.CycleClique.certificate_1235 line 1727
  873. theorem OAI.CycleClique.certificate_1235_checked line 1729
  874. theorem OAI.CycleClique.certificate_1235_valid line 1730
  875. def OAI.CycleClique.certificate_1236_q line 1732
  876. def OAI.CycleClique.certificate_1236_edges line 1733
  877. def OAI.CycleClique.certificate_1236_part_0 line 1735
  878. def OAI.CycleClique.certificate_1236_part_1 line 1737
  879. def OAI.CycleClique.certificate_1236_part_2 line 1739
  880. def OAI.CycleClique.certificate_1236_part_3 line 1741
  881. def OAI.CycleClique.certificate_1236 line 1743
  882. theorem OAI.CycleClique.certificate_1236_checked line 1745
  883. theorem OAI.CycleClique.certificate_1236_valid line 1746
  884. def OAI.CycleClique.certificate_1237_q line 1748
  885. def OAI.CycleClique.certificate_1237_edges line 1749
  886. def OAI.CycleClique.certificate_1237_part_0 line 1751
  887. def OAI.CycleClique.certificate_1237_part_1 line 1753
  888. def OAI.CycleClique.certificate_1237_part_2 line 1755
  889. def OAI.CycleClique.certificate_1237_part_3 line 1757
  890. def OAI.CycleClique.certificate_1237_part_4 line 1759
  891. def OAI.CycleClique.certificate_1237 line 1761
  892. theorem OAI.CycleClique.certificate_1237_checked line 1763
  893. theorem OAI.CycleClique.certificate_1237_valid line 1764
  894. def OAI.CycleClique.certificate_1238_q line 1766
  895. def OAI.CycleClique.certificate_1238_edges line 1767
  896. def OAI.CycleClique.certificate_1238_part_0 line 1769
  897. def OAI.CycleClique.certificate_1238_part_1 line 1771
  898. def OAI.CycleClique.certificate_1238_part_2 line 1773
  899. def OAI.CycleClique.certificate_1238_part_3 line 1775
  900. def OAI.CycleClique.certificate_1238 line 1777
  901. theorem OAI.CycleClique.certificate_1238_checked line 1779
  902. theorem OAI.CycleClique.certificate_1238_valid line 1780
  903. def OAI.CycleClique.certificate_1239_q line 1782
  904. def OAI.CycleClique.certificate_1239_edges line 1783
  905. def OAI.CycleClique.certificate_1239_part_0 line 1785
  906. def OAI.CycleClique.certificate_1239_part_1 line 1787
  907. def OAI.CycleClique.certificate_1239_part_2 line 1789
  908. def OAI.CycleClique.certificate_1239_part_3 line 1791
  909. def OAI.CycleClique.certificate_1239 line 1793
  910. theorem OAI.CycleClique.certificate_1239_checked line 1795
  911. theorem OAI.CycleClique.certificate_1239_valid line 1796
  912. def OAI.CycleClique.certificate_1240_q line 1798
  913. def OAI.CycleClique.certificate_1240_edges line 1799
  914. def OAI.CycleClique.certificate_1240_part_0 line 1801
  915. def OAI.CycleClique.certificate_1240_part_1 line 1803
  916. def OAI.CycleClique.certificate_1240_part_2 line 1805
  917. def OAI.CycleClique.certificate_1240_part_3 line 1807
  918. def OAI.CycleClique.certificate_1240 line 1809
  919. theorem OAI.CycleClique.certificate_1240_checked line 1811
  920. theorem OAI.CycleClique.certificate_1240_valid line 1812
  921. def OAI.CycleClique.certificate_1241_q line 1814
  922. def OAI.CycleClique.certificate_1241_edges line 1815
  923. def OAI.CycleClique.certificate_1241_part_0 line 1817
  924. def OAI.CycleClique.certificate_1241_part_1 line 1819
  925. def OAI.CycleClique.certificate_1241_part_2 line 1821
  926. def OAI.CycleClique.certificate_1241_part_3 line 1823
  927. def OAI.CycleClique.certificate_1241 line 1825
  928. theorem OAI.CycleClique.certificate_1241_checked line 1827
  929. theorem OAI.CycleClique.certificate_1241_valid line 1828
  930. def OAI.CycleClique.certificate_1242_q line 1830
  931. def OAI.CycleClique.certificate_1242_edges line 1831
  932. def OAI.CycleClique.certificate_1242_part_0 line 1833
  933. def OAI.CycleClique.certificate_1242_part_1 line 1835
  934. def OAI.CycleClique.certificate_1242_part_2 line 1837
  935. def OAI.CycleClique.certificate_1242_part_3 line 1839
  936. def OAI.CycleClique.certificate_1242_part_4 line 1841
  937. def OAI.CycleClique.certificate_1242 line 1843
  938. theorem OAI.CycleClique.certificate_1242_checked line 1845
  939. theorem OAI.CycleClique.certificate_1242_valid line 1846
  940. def OAI.CycleClique.certificate_1243_q line 1848
  941. def OAI.CycleClique.certificate_1243_edges line 1849
  942. def OAI.CycleClique.certificate_1243_part_0 line 1851
  943. def OAI.CycleClique.certificate_1243_part_1 line 1853
  944. def OAI.CycleClique.certificate_1243_part_2 line 1855
  945. def OAI.CycleClique.certificate_1243_part_3 line 1857
  946. def OAI.CycleClique.certificate_1243 line 1859
  947. theorem OAI.CycleClique.certificate_1243_checked line 1861
  948. theorem OAI.CycleClique.certificate_1243_valid line 1862
  949. def OAI.CycleClique.certificate_1244_q line 1864
  950. def OAI.CycleClique.certificate_1244_edges line 1865
  951. def OAI.CycleClique.certificate_1244_part_0 line 1867
  952. def OAI.CycleClique.certificate_1244_part_1 line 1869
  953. def OAI.CycleClique.certificate_1244_part_2 line 1871
  954. def OAI.CycleClique.certificate_1244_part_3 line 1873
  955. def OAI.CycleClique.certificate_1244 line 1875
  956. theorem OAI.CycleClique.certificate_1244_checked line 1877
  957. theorem OAI.CycleClique.certificate_1244_valid line 1878
  958. def OAI.CycleClique.certificate_1245_q line 1880
  959. def OAI.CycleClique.certificate_1245_edges line 1881
  960. def OAI.CycleClique.certificate_1245_part_0 line 1883
  961. def OAI.CycleClique.certificate_1245_part_1 line 1885
  962. def OAI.CycleClique.certificate_1245_part_2 line 1887
  963. def OAI.CycleClique.certificate_1245_part_3 line 1889
  964. def OAI.CycleClique.certificate_1245 line 1891
  965. theorem OAI.CycleClique.certificate_1245_checked line 1893
  966. theorem OAI.CycleClique.certificate_1245_valid line 1894
  967. def OAI.CycleClique.certificate_1246_q line 1896
  968. def OAI.CycleClique.certificate_1246_edges line 1897
  969. def OAI.CycleClique.certificate_1246_part_0 line 1899
  970. def OAI.CycleClique.certificate_1246_part_1 line 1901
  971. def OAI.CycleClique.certificate_1246_part_2 line 1903
  972. def OAI.CycleClique.certificate_1246_part_3 line 1905
  973. def OAI.CycleClique.certificate_1246 line 1907
  974. theorem OAI.CycleClique.certificate_1246_checked line 1909
  975. theorem OAI.CycleClique.certificate_1246_valid line 1910
  976. def OAI.CycleClique.certificate_1247_q line 1912
  977. def OAI.CycleClique.certificate_1247_edges line 1913
  978. def OAI.CycleClique.certificate_1247_part_0 line 1915
  979. def OAI.CycleClique.certificate_1247_part_1 line 1917
  980. def OAI.CycleClique.certificate_1247_part_2 line 1919
  981. def OAI.CycleClique.certificate_1247_part_3 line 1921
  982. def OAI.CycleClique.certificate_1247_part_4 line 1923
  983. def OAI.CycleClique.certificate_1247 line 1925
  984. theorem OAI.CycleClique.certificate_1247_checked line 1927
  985. theorem OAI.CycleClique.certificate_1247_valid line 1928