OAI/Combinatorics/Ramsey/CycleClique/Certificates004.lean

GitHub source file

524 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.certificate_96_q line 20
  2. def OAI.CycleClique.certificate_96_edges line 22
  3. def OAI.CycleClique.certificate_96_E line 24
  4. def OAI.CycleClique.certificate_96_M line 26
  5. def OAI.CycleClique.certificate_96_part_1_E line 28
  6. def OAI.CycleClique.certificate_96_part_1_M line 30
  7. def OAI.CycleClique.certificate_96_part_2_E line 32
  8. def OAI.CycleClique.certificate_96_part_2_M line 34
  9. def OAI.CycleClique.certificate_96_part_3_E line 36
  10. def OAI.CycleClique.certificate_96_part_3_M line 38
  11. def OAI.CycleClique.certificate_96_part_4_E line 40
  12. def OAI.CycleClique.certificate_96_part_4_M line 42
  13. def OAI.CycleClique.certificate_96_part_5_E line 44
  14. def OAI.CycleClique.certificate_96_part_5_M line 46
  15. def OAI.CycleClique.certificate_96_part_5 line 48
  16. theorem OAI.CycleClique.certificate_96_part_5_checked line 50
  17. def OAI.CycleClique.certificate_96_part_6_E line 52
  18. def OAI.CycleClique.certificate_96_part_6_M line 54
  19. def OAI.CycleClique.certificate_96_part_7_E line 56
  20. def OAI.CycleClique.certificate_96_part_7_M line 58
  21. def OAI.CycleClique.certificate_96_part_8_E line 60
  22. def OAI.CycleClique.certificate_96_part_8_M line 62
  23. def OAI.CycleClique.certificate_96_part_9_E line 64
  24. def OAI.CycleClique.certificate_96_part_9_M line 66
  25. def OAI.CycleClique.certificate_96_part_9 line 68
  26. theorem OAI.CycleClique.certificate_96_part_9_checked line 70
  27. def OAI.CycleClique.certificate_96_part_8 line 72
  28. theorem OAI.CycleClique.certificate_96_part_8_checked line 74
  29. def OAI.CycleClique.certificate_96_part_10_E line 76
  30. def OAI.CycleClique.certificate_96_part_10_M line 78
  31. def OAI.CycleClique.certificate_96_part_11_E line 80
  32. def OAI.CycleClique.certificate_96_part_11_M line 82
  33. def OAI.CycleClique.certificate_96_part_12_E line 84
  34. def OAI.CycleClique.certificate_96_part_12_M line 86
  35. def OAI.CycleClique.certificate_96_part_13_E line 88
  36. def OAI.CycleClique.certificate_96_part_13_M line 90
  37. def OAI.CycleClique.certificate_96_part_13 line 92
  38. theorem OAI.CycleClique.certificate_96_part_13_checked line 94
  39. def OAI.CycleClique.certificate_96_part_14_E line 96
  40. def OAI.CycleClique.certificate_96_part_14_M line 98
  41. def OAI.CycleClique.certificate_96_part_15_E line 100
  42. def OAI.CycleClique.certificate_96_part_15_M line 102
  43. def OAI.CycleClique.certificate_96_part_16_E line 104
  44. def OAI.CycleClique.certificate_96_part_16_M line 106
  45. def OAI.CycleClique.certificate_96_part_16 line 108
  46. theorem OAI.CycleClique.certificate_96_part_16_checked line 110
  47. def OAI.CycleClique.certificate_96_part_17_E line 112
  48. def OAI.CycleClique.certificate_96_part_17_M line 114
  49. def OAI.CycleClique.certificate_96_part_17 line 116
  50. theorem OAI.CycleClique.certificate_96_part_17_checked line 118
  51. def OAI.CycleClique.certificate_96_part_18_E line 120
  52. def OAI.CycleClique.certificate_96_part_18_M line 122
  53. def OAI.CycleClique.certificate_96_part_19_E line 124
  54. def OAI.CycleClique.certificate_96_part_19_M line 126
  55. def OAI.CycleClique.certificate_96_part_19 line 128
  56. theorem OAI.CycleClique.certificate_96_part_19_checked line 130
  57. def OAI.CycleClique.certificate_96_part_20_E line 132
  58. def OAI.CycleClique.certificate_96_part_20_M line 134
  59. def OAI.CycleClique.certificate_96_part_21_E line 136
  60. def OAI.CycleClique.certificate_96_part_21_M line 138
  61. def OAI.CycleClique.certificate_96_part_22_E line 140
  62. def OAI.CycleClique.certificate_96_part_22_M line 142
  63. def OAI.CycleClique.certificate_96_part_22 line 144
  64. theorem OAI.CycleClique.certificate_96_part_22_checked line 146
  65. def OAI.CycleClique.certificate_96_part_21 line 148
  66. theorem OAI.CycleClique.certificate_96_part_21_checked line 150
  67. def OAI.CycleClique.certificate_96_part_23_E line 152
  68. def OAI.CycleClique.certificate_96_part_23_M line 154
  69. def OAI.CycleClique.certificate_96_part_23 line 156
  70. theorem OAI.CycleClique.certificate_96_part_23_checked line 158
  71. def OAI.CycleClique.certificate_96_part_20 line 160
  72. theorem OAI.CycleClique.certificate_96_part_20_checked line 162
  73. def OAI.CycleClique.certificate_96_part_18 line 164
  74. theorem OAI.CycleClique.certificate_96_part_18_checked line 166
  75. def OAI.CycleClique.certificate_96_part_15 line 168
  76. theorem OAI.CycleClique.certificate_96_part_15_checked line 170
  77. def OAI.CycleClique.certificate_96_part_14 line 172
  78. theorem OAI.CycleClique.certificate_96_part_14_checked line 174
  79. def OAI.CycleClique.certificate_96_part_12 line 176
  80. theorem OAI.CycleClique.certificate_96_part_12_checked line 178
  81. def OAI.CycleClique.certificate_96_part_11 line 180
  82. theorem OAI.CycleClique.certificate_96_part_11_checked line 182
  83. def OAI.CycleClique.certificate_96_part_10 line 184
  84. theorem OAI.CycleClique.certificate_96_part_10_checked line 186
  85. def OAI.CycleClique.certificate_96_part_7 line 188
  86. theorem OAI.CycleClique.certificate_96_part_7_checked line 190
  87. def OAI.CycleClique.certificate_96_part_6 line 192
  88. theorem OAI.CycleClique.certificate_96_part_6_checked line 194
  89. def OAI.CycleClique.certificate_96_part_4 line 196
  90. theorem OAI.CycleClique.certificate_96_part_4_checked line 198
  91. def OAI.CycleClique.certificate_96_part_3 line 200
  92. theorem OAI.CycleClique.certificate_96_part_3_checked line 202
  93. def OAI.CycleClique.certificate_96_part_2 line 204
  94. theorem OAI.CycleClique.certificate_96_part_2_checked line 206
  95. def OAI.CycleClique.certificate_96_part_1 line 208
  96. theorem OAI.CycleClique.certificate_96_part_1_checked line 210
  97. def OAI.CycleClique.certificate_96 line 212
  98. theorem OAI.CycleClique.certificate_96_checked line 214
  99. theorem OAI.CycleClique.certificate_96_valid line 216
  100. def OAI.CycleClique.certificate_97_q line 218
  101. def OAI.CycleClique.certificate_97_edges line 219
  102. def OAI.CycleClique.certificate_97_part_0 line 221
  103. def OAI.CycleClique.certificate_97 line 223
  104. theorem OAI.CycleClique.certificate_97_checked line 225
  105. theorem OAI.CycleClique.certificate_97_valid line 226
  106. def OAI.CycleClique.certificate_98_q line 228
  107. def OAI.CycleClique.certificate_98_edges line 229
  108. def OAI.CycleClique.certificate_98_part_0 line 231
  109. def OAI.CycleClique.certificate_98 line 233
  110. theorem OAI.CycleClique.certificate_98_checked line 235
  111. theorem OAI.CycleClique.certificate_98_valid line 236
  112. def OAI.CycleClique.certificate_99_q line 238
  113. def OAI.CycleClique.certificate_99_edges line 239
  114. def OAI.CycleClique.certificate_99_part_0 line 241
  115. def OAI.CycleClique.certificate_99 line 243
  116. theorem OAI.CycleClique.certificate_99_checked line 245
  117. theorem OAI.CycleClique.certificate_99_valid line 246
  118. def OAI.CycleClique.certificate_100_q line 248
  119. def OAI.CycleClique.certificate_100_edges line 249
  120. def OAI.CycleClique.certificate_100_part_0 line 251
  121. def OAI.CycleClique.certificate_100 line 253
  122. theorem OAI.CycleClique.certificate_100_checked line 255
  123. theorem OAI.CycleClique.certificate_100_valid line 256
  124. def OAI.CycleClique.certificate_101_q line 258
  125. def OAI.CycleClique.certificate_101_edges line 259
  126. def OAI.CycleClique.certificate_101_part_0 line 261
  127. def OAI.CycleClique.certificate_101 line 263
  128. theorem OAI.CycleClique.certificate_101_checked line 265
  129. theorem OAI.CycleClique.certificate_101_valid line 266
  130. def OAI.CycleClique.certificate_102_q line 268
  131. def OAI.CycleClique.certificate_102_edges line 269
  132. def OAI.CycleClique.certificate_102_part_0 line 271
  133. def OAI.CycleClique.certificate_102 line 273
  134. theorem OAI.CycleClique.certificate_102_checked line 275
  135. theorem OAI.CycleClique.certificate_102_valid line 276
  136. def OAI.CycleClique.certificate_103_q line 278
  137. def OAI.CycleClique.certificate_103_edges line 279
  138. def OAI.CycleClique.certificate_103_part_0 line 281
  139. def OAI.CycleClique.certificate_103 line 283
  140. theorem OAI.CycleClique.certificate_103_checked line 285
  141. theorem OAI.CycleClique.certificate_103_valid line 286
  142. def OAI.CycleClique.certificate_104_q line 288
  143. def OAI.CycleClique.certificate_104_edges line 290
  144. def OAI.CycleClique.certificate_104_E line 292
  145. def OAI.CycleClique.certificate_104_M line 294
  146. def OAI.CycleClique.certificate_104_part_1_E line 296
  147. def OAI.CycleClique.certificate_104_part_1_M line 298
  148. def OAI.CycleClique.certificate_104_part_2_E line 300
  149. def OAI.CycleClique.certificate_104_part_2_M line 302
  150. def OAI.CycleClique.certificate_104_part_3_E line 304
  151. def OAI.CycleClique.certificate_104_part_3_M line 306
  152. def OAI.CycleClique.certificate_104_part_4_E line 308
  153. def OAI.CycleClique.certificate_104_part_4_M line 310
  154. def OAI.CycleClique.certificate_104_part_5_E line 312
  155. def OAI.CycleClique.certificate_104_part_5_M line 314
  156. def OAI.CycleClique.certificate_104_part_6_E line 316
  157. def OAI.CycleClique.certificate_104_part_6_M line 318
  158. def OAI.CycleClique.certificate_104_part_7_E line 320
  159. def OAI.CycleClique.certificate_104_part_7_M line 322
  160. def OAI.CycleClique.certificate_104_part_8_E line 324
  161. def OAI.CycleClique.certificate_104_part_8_M line 326
  162. def OAI.CycleClique.certificate_104_part_9_E line 328
  163. def OAI.CycleClique.certificate_104_part_9_M line 330
  164. def OAI.CycleClique.certificate_104_part_10_E line 332
  165. def OAI.CycleClique.certificate_104_part_10_M line 334
  166. def OAI.CycleClique.certificate_104_part_11_E line 336
  167. def OAI.CycleClique.certificate_104_part_11_M line 338
  168. def OAI.CycleClique.certificate_104_part_12_E line 340
  169. def OAI.CycleClique.certificate_104_part_12_M line 342
  170. def OAI.CycleClique.certificate_104_part_13_E line 344
  171. def OAI.CycleClique.certificate_104_part_13_M line 346
  172. def OAI.CycleClique.certificate_104_part_13 line 348
  173. theorem OAI.CycleClique.certificate_104_part_13_checked line 350
  174. def OAI.CycleClique.certificate_104_part_12 line 352
  175. theorem OAI.CycleClique.certificate_104_part_12_checked line 354
  176. def OAI.CycleClique.certificate_104_part_11 line 356
  177. theorem OAI.CycleClique.certificate_104_part_11_checked line 358
  178. def OAI.CycleClique.certificate_104_part_14_E line 360
  179. def OAI.CycleClique.certificate_104_part_14_M line 362
  180. def OAI.CycleClique.certificate_104_part_15_E line 364
  181. def OAI.CycleClique.certificate_104_part_15_M line 366
  182. def OAI.CycleClique.certificate_104_part_15 line 368
  183. theorem OAI.CycleClique.certificate_104_part_15_checked line 370
  184. def OAI.CycleClique.certificate_104_part_16_E line 372
  185. def OAI.CycleClique.certificate_104_part_16_M line 374
  186. def OAI.CycleClique.certificate_104_part_17_E line 376
  187. def OAI.CycleClique.certificate_104_part_17_M line 378
  188. def OAI.CycleClique.certificate_104_part_18_E line 380
  189. def OAI.CycleClique.certificate_104_part_18_M line 382
  190. def OAI.CycleClique.certificate_104_part_18 line 384
  191. theorem OAI.CycleClique.certificate_104_part_18_checked line 386
  192. def OAI.CycleClique.certificate_104_part_19_E line 388
  193. def OAI.CycleClique.certificate_104_part_19_M line 390
  194. def OAI.CycleClique.certificate_104_part_19 line 392
  195. theorem OAI.CycleClique.certificate_104_part_19_checked line 394
  196. def OAI.CycleClique.certificate_104_part_20_E line 396
  197. def OAI.CycleClique.certificate_104_part_20_M line 398
  198. def OAI.CycleClique.certificate_104_part_20 line 400
  199. theorem OAI.CycleClique.certificate_104_part_20_checked line 402
  200. def OAI.CycleClique.certificate_104_part_17 line 404
  201. theorem OAI.CycleClique.certificate_104_part_17_checked line 406
  202. def OAI.CycleClique.certificate_104_part_16 line 408
  203. theorem OAI.CycleClique.certificate_104_part_16_checked line 410
  204. def OAI.CycleClique.certificate_104_part_14 line 412
  205. theorem OAI.CycleClique.certificate_104_part_14_checked line 414
  206. def OAI.CycleClique.certificate_104_part_10 line 416
  207. theorem OAI.CycleClique.certificate_104_part_10_checked line 418
  208. def OAI.CycleClique.certificate_104_part_9 line 420
  209. theorem OAI.CycleClique.certificate_104_part_9_checked line 422
  210. def OAI.CycleClique.certificate_104_part_8 line 424
  211. theorem OAI.CycleClique.certificate_104_part_8_checked line 426
  212. def OAI.CycleClique.certificate_104_part_7 line 428
  213. theorem OAI.CycleClique.certificate_104_part_7_checked line 430
  214. def OAI.CycleClique.certificate_104_part_6 line 432
  215. theorem OAI.CycleClique.certificate_104_part_6_checked line 434
  216. def OAI.CycleClique.certificate_104_part_5 line 436
  217. theorem OAI.CycleClique.certificate_104_part_5_checked line 438
  218. def OAI.CycleClique.certificate_104_part_4 line 440
  219. theorem OAI.CycleClique.certificate_104_part_4_checked line 442
  220. def OAI.CycleClique.certificate_104_part_3 line 444
  221. theorem OAI.CycleClique.certificate_104_part_3_checked line 446
  222. def OAI.CycleClique.certificate_104_part_2 line 448
  223. theorem OAI.CycleClique.certificate_104_part_2_checked line 450
  224. def OAI.CycleClique.certificate_104_part_1 line 452
  225. theorem OAI.CycleClique.certificate_104_part_1_checked line 454
  226. def OAI.CycleClique.certificate_104 line 456
  227. theorem OAI.CycleClique.certificate_104_checked line 458
  228. theorem OAI.CycleClique.certificate_104_valid line 460
  229. def OAI.CycleClique.certificate_105_q line 462
  230. def OAI.CycleClique.certificate_105_edges line 463
  231. def OAI.CycleClique.certificate_105_part_0 line 465
  232. def OAI.CycleClique.certificate_105 line 467
  233. theorem OAI.CycleClique.certificate_105_checked line 469
  234. theorem OAI.CycleClique.certificate_105_valid line 470
  235. def OAI.CycleClique.certificate_106_q line 472
  236. def OAI.CycleClique.certificate_106_edges line 473
  237. def OAI.CycleClique.certificate_106_part_0 line 475
  238. def OAI.CycleClique.certificate_106 line 477
  239. theorem OAI.CycleClique.certificate_106_checked line 479
  240. theorem OAI.CycleClique.certificate_106_valid line 480
  241. def OAI.CycleClique.certificate_107_q line 482
  242. def OAI.CycleClique.certificate_107_edges line 483
  243. def OAI.CycleClique.certificate_107_part_0 line 485
  244. def OAI.CycleClique.certificate_107 line 487
  245. theorem OAI.CycleClique.certificate_107_checked line 489
  246. theorem OAI.CycleClique.certificate_107_valid line 490
  247. def OAI.CycleClique.certificate_108_q line 492
  248. def OAI.CycleClique.certificate_108_edges line 493
  249. def OAI.CycleClique.certificate_108_part_0 line 495
  250. def OAI.CycleClique.certificate_108 line 497
  251. theorem OAI.CycleClique.certificate_108_checked line 499
  252. theorem OAI.CycleClique.certificate_108_valid line 500
  253. def OAI.CycleClique.certificate_109_q line 502
  254. def OAI.CycleClique.certificate_109_edges line 503
  255. def OAI.CycleClique.certificate_109_part_0 line 505
  256. def OAI.CycleClique.certificate_109 line 507
  257. theorem OAI.CycleClique.certificate_109_checked line 509
  258. theorem OAI.CycleClique.certificate_109_valid line 510
  259. def OAI.CycleClique.certificate_110_q line 512
  260. def OAI.CycleClique.certificate_110_edges line 514
  261. def OAI.CycleClique.certificate_110_E line 516
  262. def OAI.CycleClique.certificate_110_M line 518
  263. def OAI.CycleClique.certificate_110_part_1_E line 520
  264. def OAI.CycleClique.certificate_110_part_1_M line 522
  265. def OAI.CycleClique.certificate_110_part_2_E line 524
  266. def OAI.CycleClique.certificate_110_part_2_M line 526
  267. def OAI.CycleClique.certificate_110_part_3_E line 528
  268. def OAI.CycleClique.certificate_110_part_3_M line 530
  269. def OAI.CycleClique.certificate_110_part_4_E line 532
  270. def OAI.CycleClique.certificate_110_part_4_M line 534
  271. def OAI.CycleClique.certificate_110_part_4 line 536
  272. theorem OAI.CycleClique.certificate_110_part_4_checked line 538
  273. def OAI.CycleClique.certificate_110_part_5_E line 540
  274. def OAI.CycleClique.certificate_110_part_5_M line 542
  275. def OAI.CycleClique.certificate_110_part_6_E line 544
  276. def OAI.CycleClique.certificate_110_part_6_M line 546
  277. def OAI.CycleClique.certificate_110_part_7_E line 548
  278. def OAI.CycleClique.certificate_110_part_7_M line 550
  279. def OAI.CycleClique.certificate_110_part_8_E line 552
  280. def OAI.CycleClique.certificate_110_part_8_M line 554
  281. def OAI.CycleClique.certificate_110_part_8 line 556
  282. theorem OAI.CycleClique.certificate_110_part_8_checked line 558
  283. def OAI.CycleClique.certificate_110_part_7 line 560
  284. theorem OAI.CycleClique.certificate_110_part_7_checked line 562
  285. def OAI.CycleClique.certificate_110_part_9_E line 564
  286. def OAI.CycleClique.certificate_110_part_9_M line 566
  287. def OAI.CycleClique.certificate_110_part_10_E line 568
  288. def OAI.CycleClique.certificate_110_part_10_M line 570
  289. def OAI.CycleClique.certificate_110_part_11_E line 572
  290. def OAI.CycleClique.certificate_110_part_11_M line 574
  291. def OAI.CycleClique.certificate_110_part_12_E line 576
  292. def OAI.CycleClique.certificate_110_part_12_M line 578
  293. def OAI.CycleClique.certificate_110_part_12 line 580
  294. theorem OAI.CycleClique.certificate_110_part_12_checked line 582
  295. def OAI.CycleClique.certificate_110_part_11 line 584
  296. theorem OAI.CycleClique.certificate_110_part_11_checked line 586
  297. def OAI.CycleClique.certificate_110_part_10 line 588
  298. theorem OAI.CycleClique.certificate_110_part_10_checked line 590
  299. def OAI.CycleClique.certificate_110_part_9 line 592
  300. theorem OAI.CycleClique.certificate_110_part_9_checked line 594
  301. def OAI.CycleClique.certificate_110_part_13_E line 596
  302. def OAI.CycleClique.certificate_110_part_13_M line 598
  303. def OAI.CycleClique.certificate_110_part_14_E line 600
  304. def OAI.CycleClique.certificate_110_part_14_M line 602
  305. def OAI.CycleClique.certificate_110_part_14 line 604
  306. theorem OAI.CycleClique.certificate_110_part_14_checked line 606
  307. def OAI.CycleClique.certificate_110_part_15_E line 608
  308. def OAI.CycleClique.certificate_110_part_15_M line 610
  309. def OAI.CycleClique.certificate_110_part_16_E line 612
  310. def OAI.CycleClique.certificate_110_part_16_M line 614
  311. def OAI.CycleClique.certificate_110_part_17_E line 616
  312. def OAI.CycleClique.certificate_110_part_17_M line 618
  313. def OAI.CycleClique.certificate_110_part_17 line 620
  314. theorem OAI.CycleClique.certificate_110_part_17_checked line 622
  315. def OAI.CycleClique.certificate_110_part_16 line 624
  316. theorem OAI.CycleClique.certificate_110_part_16_checked line 626
  317. def OAI.CycleClique.certificate_110_part_15 line 628
  318. theorem OAI.CycleClique.certificate_110_part_15_checked line 630
  319. def OAI.CycleClique.certificate_110_part_18_E line 632
  320. def OAI.CycleClique.certificate_110_part_18_M line 634
  321. def OAI.CycleClique.certificate_110_part_19_E line 636
  322. def OAI.CycleClique.certificate_110_part_19_M line 638
  323. def OAI.CycleClique.certificate_110_part_19 line 640
  324. theorem OAI.CycleClique.certificate_110_part_19_checked line 642
  325. def OAI.CycleClique.certificate_110_part_20_E line 644
  326. def OAI.CycleClique.certificate_110_part_20_M line 646
  327. def OAI.CycleClique.certificate_110_part_20 line 648
  328. theorem OAI.CycleClique.certificate_110_part_20_checked line 650
  329. def OAI.CycleClique.certificate_110_part_21_E line 652
  330. def OAI.CycleClique.certificate_110_part_21_M line 654
  331. def OAI.CycleClique.certificate_110_part_22_E line 656
  332. def OAI.CycleClique.certificate_110_part_22_M line 658
  333. def OAI.CycleClique.certificate_110_part_22 line 660
  334. theorem OAI.CycleClique.certificate_110_part_22_checked line 662
  335. def OAI.CycleClique.certificate_110_part_21 line 664
  336. theorem OAI.CycleClique.certificate_110_part_21_checked line 666
  337. def OAI.CycleClique.certificate_110_part_23_E line 668
  338. def OAI.CycleClique.certificate_110_part_23_M line 670
  339. def OAI.CycleClique.certificate_110_part_24_E line 672
  340. def OAI.CycleClique.certificate_110_part_24_M line 674
  341. def OAI.CycleClique.certificate_110_part_24 line 676
  342. theorem OAI.CycleClique.certificate_110_part_24_checked line 678
  343. def OAI.CycleClique.certificate_110_part_25_E line 680
  344. def OAI.CycleClique.certificate_110_part_25_M line 682
  345. def OAI.CycleClique.certificate_110_part_25 line 684
  346. theorem OAI.CycleClique.certificate_110_part_25_checked line 686
  347. def OAI.CycleClique.certificate_110_part_26_E line 688
  348. def OAI.CycleClique.certificate_110_part_26_M line 690
  349. def OAI.CycleClique.certificate_110_part_27_E line 692
  350. def OAI.CycleClique.certificate_110_part_27_M line 694
  351. def OAI.CycleClique.certificate_110_part_27 line 696
  352. theorem OAI.CycleClique.certificate_110_part_27_checked line 698
  353. def OAI.CycleClique.certificate_110_part_26 line 700
  354. theorem OAI.CycleClique.certificate_110_part_26_checked line 702
  355. def OAI.CycleClique.certificate_110_part_28_E line 704
  356. def OAI.CycleClique.certificate_110_part_28_M line 706
  357. def OAI.CycleClique.certificate_110_part_29_E line 708
  358. def OAI.CycleClique.certificate_110_part_29_M line 710
  359. def OAI.CycleClique.certificate_110_part_29 line 712
  360. theorem OAI.CycleClique.certificate_110_part_29_checked line 714
  361. def OAI.CycleClique.certificate_110_part_30_E line 716
  362. def OAI.CycleClique.certificate_110_part_30_M line 718
  363. def OAI.CycleClique.certificate_110_part_31_E line 720
  364. def OAI.CycleClique.certificate_110_part_31_M line 722
  365. def OAI.CycleClique.certificate_110_part_31 line 724
  366. theorem OAI.CycleClique.certificate_110_part_31_checked line 726
  367. def OAI.CycleClique.certificate_110_part_32_E line 728
  368. def OAI.CycleClique.certificate_110_part_32_M line 730
  369. def OAI.CycleClique.certificate_110_part_33_E line 732
  370. def OAI.CycleClique.certificate_110_part_33_M line 734
  371. def OAI.CycleClique.certificate_110_part_34_E line 736
  372. def OAI.CycleClique.certificate_110_part_34_M line 738
  373. def OAI.CycleClique.certificate_110_part_35_E line 740
  374. def OAI.CycleClique.certificate_110_part_35_M line 742
  375. def OAI.CycleClique.certificate_110_part_35 line 744
  376. theorem OAI.CycleClique.certificate_110_part_35_checked line 746
  377. def OAI.CycleClique.certificate_110_part_34 line 748
  378. theorem OAI.CycleClique.certificate_110_part_34_checked line 750
  379. def OAI.CycleClique.certificate_110_part_36_E line 752
  380. def OAI.CycleClique.certificate_110_part_36_M line 754
  381. def OAI.CycleClique.certificate_110_part_37_E line 756
  382. def OAI.CycleClique.certificate_110_part_37_M line 758
  383. def OAI.CycleClique.certificate_110_part_37 line 760
  384. theorem OAI.CycleClique.certificate_110_part_37_checked line 762
  385. def OAI.CycleClique.certificate_110_part_36 line 764
  386. theorem OAI.CycleClique.certificate_110_part_36_checked line 766
  387. def OAI.CycleClique.certificate_110_part_33 line 768
  388. theorem OAI.CycleClique.certificate_110_part_33_checked line 770
  389. def OAI.CycleClique.certificate_110_part_32 line 772
  390. theorem OAI.CycleClique.certificate_110_part_32_checked line 774
  391. def OAI.CycleClique.certificate_110_part_30 line 776
  392. theorem OAI.CycleClique.certificate_110_part_30_checked line 778
  393. def OAI.CycleClique.certificate_110_part_28 line 780
  394. theorem OAI.CycleClique.certificate_110_part_28_checked line 782
  395. def OAI.CycleClique.certificate_110_part_23 line 784
  396. theorem OAI.CycleClique.certificate_110_part_23_checked line 786
  397. def OAI.CycleClique.certificate_110_part_18 line 788
  398. theorem OAI.CycleClique.certificate_110_part_18_checked line 790
  399. def OAI.CycleClique.certificate_110_part_13 line 792
  400. theorem OAI.CycleClique.certificate_110_part_13_checked line 794
  401. def OAI.CycleClique.certificate_110_part_6 line 796
  402. theorem OAI.CycleClique.certificate_110_part_6_checked line 798
  403. def OAI.CycleClique.certificate_110_part_5 line 800
  404. theorem OAI.CycleClique.certificate_110_part_5_checked line 802
  405. def OAI.CycleClique.certificate_110_part_3 line 804
  406. theorem OAI.CycleClique.certificate_110_part_3_checked line 806
  407. def OAI.CycleClique.certificate_110_part_2 line 808
  408. theorem OAI.CycleClique.certificate_110_part_2_checked line 810
  409. def OAI.CycleClique.certificate_110_part_1 line 812
  410. theorem OAI.CycleClique.certificate_110_part_1_checked line 814
  411. def OAI.CycleClique.certificate_110 line 816
  412. theorem OAI.CycleClique.certificate_110_checked line 818
  413. theorem OAI.CycleClique.certificate_110_valid line 820
  414. def OAI.CycleClique.certificate_111_q line 822
  415. def OAI.CycleClique.certificate_111_edges line 823
  416. def OAI.CycleClique.certificate_111_part_0 line 825
  417. def OAI.CycleClique.certificate_111 line 827
  418. theorem OAI.CycleClique.certificate_111_checked line 829
  419. theorem OAI.CycleClique.certificate_111_valid line 830
  420. def OAI.CycleClique.certificate_112_q line 832
  421. def OAI.CycleClique.certificate_112_edges line 833
  422. def OAI.CycleClique.certificate_112_part_0 line 835
  423. def OAI.CycleClique.certificate_112 line 837
  424. theorem OAI.CycleClique.certificate_112_checked line 839
  425. theorem OAI.CycleClique.certificate_112_valid line 840
  426. def OAI.CycleClique.certificate_113_q line 842
  427. def OAI.CycleClique.certificate_113_edges line 843
  428. def OAI.CycleClique.certificate_113_part_0 line 845
  429. def OAI.CycleClique.certificate_113_part_1 line 847
  430. def OAI.CycleClique.certificate_113 line 849
  431. theorem OAI.CycleClique.certificate_113_checked line 851
  432. theorem OAI.CycleClique.certificate_113_valid line 852
  433. def OAI.CycleClique.certificate_114_q line 854
  434. def OAI.CycleClique.certificate_114_edges line 855
  435. def OAI.CycleClique.certificate_114_part_0 line 857
  436. def OAI.CycleClique.certificate_114_part_1 line 859
  437. def OAI.CycleClique.certificate_114 line 861
  438. theorem OAI.CycleClique.certificate_114_checked line 863
  439. theorem OAI.CycleClique.certificate_114_valid line 864
  440. def OAI.CycleClique.certificate_115_q line 866
  441. def OAI.CycleClique.certificate_115_edges line 867
  442. def OAI.CycleClique.certificate_115_part_0 line 869
  443. def OAI.CycleClique.certificate_115 line 871
  444. theorem OAI.CycleClique.certificate_115_checked line 873
  445. theorem OAI.CycleClique.certificate_115_valid line 874
  446. def OAI.CycleClique.certificate_116_q line 876
  447. def OAI.CycleClique.certificate_116_edges line 877
  448. def OAI.CycleClique.certificate_116_part_0 line 879
  449. def OAI.CycleClique.certificate_116 line 881
  450. theorem OAI.CycleClique.certificate_116_checked line 883
  451. theorem OAI.CycleClique.certificate_116_valid line 884
  452. def OAI.CycleClique.certificate_117_q line 886
  453. def OAI.CycleClique.certificate_117_edges line 887
  454. def OAI.CycleClique.certificate_117_part_0 line 889
  455. def OAI.CycleClique.certificate_117_part_1 line 891
  456. def OAI.CycleClique.certificate_117 line 893
  457. theorem OAI.CycleClique.certificate_117_checked line 895
  458. theorem OAI.CycleClique.certificate_117_valid line 896
  459. def OAI.CycleClique.certificate_118_q line 898
  460. def OAI.CycleClique.certificate_118_edges line 899
  461. def OAI.CycleClique.certificate_118_part_0 line 901
  462. def OAI.CycleClique.certificate_118 line 903
  463. theorem OAI.CycleClique.certificate_118_checked line 905
  464. theorem OAI.CycleClique.certificate_118_valid line 906
  465. def OAI.CycleClique.certificate_119_q line 908
  466. def OAI.CycleClique.certificate_119_edges line 909
  467. def OAI.CycleClique.certificate_119_part_0 line 911
  468. def OAI.CycleClique.certificate_119_part_1 line 913
  469. def OAI.CycleClique.certificate_119 line 915
  470. theorem OAI.CycleClique.certificate_119_checked line 917
  471. theorem OAI.CycleClique.certificate_119_valid line 918
  472. def OAI.CycleClique.certificate_120_q line 920
  473. def OAI.CycleClique.certificate_120_edges line 921
  474. def OAI.CycleClique.certificate_120_part_0 line 923
  475. def OAI.CycleClique.certificate_120_part_1 line 925
  476. def OAI.CycleClique.certificate_120 line 927
  477. theorem OAI.CycleClique.certificate_120_checked line 929
  478. theorem OAI.CycleClique.certificate_120_valid line 930
  479. def OAI.CycleClique.certificate_121_q line 932
  480. def OAI.CycleClique.certificate_121_edges line 933
  481. def OAI.CycleClique.certificate_121_part_0 line 935
  482. def OAI.CycleClique.certificate_121_part_1 line 937
  483. def OAI.CycleClique.certificate_121 line 939
  484. theorem OAI.CycleClique.certificate_121_checked line 941
  485. theorem OAI.CycleClique.certificate_121_valid line 942
  486. def OAI.CycleClique.certificate_122_q line 944
  487. def OAI.CycleClique.certificate_122_edges line 945
  488. def OAI.CycleClique.certificate_122_part_0 line 947
  489. def OAI.CycleClique.certificate_122 line 949
  490. theorem OAI.CycleClique.certificate_122_checked line 951
  491. theorem OAI.CycleClique.certificate_122_valid line 952
  492. def OAI.CycleClique.certificate_123_q line 954
  493. def OAI.CycleClique.certificate_123_edges line 955
  494. def OAI.CycleClique.certificate_123_part_0 line 957
  495. def OAI.CycleClique.certificate_123_part_1 line 959
  496. def OAI.CycleClique.certificate_123 line 961
  497. theorem OAI.CycleClique.certificate_123_checked line 963
  498. theorem OAI.CycleClique.certificate_123_valid line 964
  499. def OAI.CycleClique.certificate_124_q line 966
  500. def OAI.CycleClique.certificate_124_edges line 967
  501. def OAI.CycleClique.certificate_124_part_0 line 969
  502. def OAI.CycleClique.certificate_124_part_1 line 971
  503. def OAI.CycleClique.certificate_124 line 973
  504. theorem OAI.CycleClique.certificate_124_checked line 975
  505. theorem OAI.CycleClique.certificate_124_valid line 976
  506. def OAI.CycleClique.certificate_125_q line 978
  507. def OAI.CycleClique.certificate_125_edges line 979
  508. def OAI.CycleClique.certificate_125_part_0 line 981
  509. def OAI.CycleClique.certificate_125_part_1 line 983
  510. def OAI.CycleClique.certificate_125 line 985
  511. theorem OAI.CycleClique.certificate_125_checked line 987
  512. theorem OAI.CycleClique.certificate_125_valid line 988
  513. def OAI.CycleClique.certificate_126_q line 990
  514. def OAI.CycleClique.certificate_126_edges line 991
  515. def OAI.CycleClique.certificate_126_part_0 line 993
  516. def OAI.CycleClique.certificate_126 line 995
  517. theorem OAI.CycleClique.certificate_126_checked line 997
  518. theorem OAI.CycleClique.certificate_126_valid line 998
  519. def OAI.CycleClique.certificate_127_q line 1000
  520. def OAI.CycleClique.certificate_127_edges line 1001
  521. def OAI.CycleClique.certificate_127_part_0 line 1003
  522. def OAI.CycleClique.certificate_127 line 1005
  523. theorem OAI.CycleClique.certificate_127_checked line 1007
  524. theorem OAI.CycleClique.certificate_127_valid line 1008