OAI/Combinatorics/Ramsey/CycleClique/Certificates009.lean

GitHub source file

500 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.certificate_256_q line 20
  2. def OAI.CycleClique.certificate_256_edges line 22
  3. def OAI.CycleClique.certificate_256_E line 24
  4. def OAI.CycleClique.certificate_256_M line 26
  5. def OAI.CycleClique.certificate_256_part_1_E line 28
  6. def OAI.CycleClique.certificate_256_part_1_M line 30
  7. def OAI.CycleClique.certificate_256_part_2_E line 32
  8. def OAI.CycleClique.certificate_256_part_2_M line 34
  9. def OAI.CycleClique.certificate_256_part_3_E line 36
  10. def OAI.CycleClique.certificate_256_part_3_M line 38
  11. def OAI.CycleClique.certificate_256_part_4_E line 40
  12. def OAI.CycleClique.certificate_256_part_4_M line 42
  13. def OAI.CycleClique.certificate_256_part_5_E line 44
  14. def OAI.CycleClique.certificate_256_part_5_M line 46
  15. def OAI.CycleClique.certificate_256_part_5 line 48
  16. theorem OAI.CycleClique.certificate_256_part_5_checked line 50
  17. def OAI.CycleClique.certificate_256_part_6_E line 52
  18. def OAI.CycleClique.certificate_256_part_6_M line 54
  19. def OAI.CycleClique.certificate_256_part_7_E line 56
  20. def OAI.CycleClique.certificate_256_part_7_M line 58
  21. def OAI.CycleClique.certificate_256_part_8_E line 60
  22. def OAI.CycleClique.certificate_256_part_8_M line 62
  23. def OAI.CycleClique.certificate_256_part_9_E line 64
  24. def OAI.CycleClique.certificate_256_part_9_M line 66
  25. def OAI.CycleClique.certificate_256_part_10_E line 68
  26. def OAI.CycleClique.certificate_256_part_10_M line 70
  27. def OAI.CycleClique.certificate_256_part_11_E line 72
  28. def OAI.CycleClique.certificate_256_part_11_M line 74
  29. def OAI.CycleClique.certificate_256_part_11 line 76
  30. theorem OAI.CycleClique.certificate_256_part_11_checked line 78
  31. def OAI.CycleClique.certificate_256_part_12_E line 80
  32. def OAI.CycleClique.certificate_256_part_12_M line 82
  33. def OAI.CycleClique.certificate_256_part_12 line 84
  34. theorem OAI.CycleClique.certificate_256_part_12_checked line 86
  35. def OAI.CycleClique.certificate_256_part_13_E line 88
  36. def OAI.CycleClique.certificate_256_part_13_M line 90
  37. def OAI.CycleClique.certificate_256_part_14_E line 92
  38. def OAI.CycleClique.certificate_256_part_14_M line 94
  39. def OAI.CycleClique.certificate_256_part_15_E line 96
  40. def OAI.CycleClique.certificate_256_part_15_M line 98
  41. def OAI.CycleClique.certificate_256_part_15 line 100
  42. theorem OAI.CycleClique.certificate_256_part_15_checked line 102
  43. def OAI.CycleClique.certificate_256_part_16_E line 104
  44. def OAI.CycleClique.certificate_256_part_16_M line 106
  45. def OAI.CycleClique.certificate_256_part_17_E line 108
  46. def OAI.CycleClique.certificate_256_part_17_M line 110
  47. def OAI.CycleClique.certificate_256_part_18_E line 112
  48. def OAI.CycleClique.certificate_256_part_18_M line 114
  49. def OAI.CycleClique.certificate_256_part_19_E line 116
  50. def OAI.CycleClique.certificate_256_part_19_M line 118
  51. def OAI.CycleClique.certificate_256_part_20_E line 120
  52. def OAI.CycleClique.certificate_256_part_20_M line 122
  53. def OAI.CycleClique.certificate_256_part_21_E line 124
  54. def OAI.CycleClique.certificate_256_part_21_M line 126
  55. def OAI.CycleClique.certificate_256_part_21 line 128
  56. theorem OAI.CycleClique.certificate_256_part_21_checked line 130
  57. def OAI.CycleClique.certificate_256_part_22_E line 132
  58. def OAI.CycleClique.certificate_256_part_22_M line 134
  59. def OAI.CycleClique.certificate_256_part_22 line 136
  60. theorem OAI.CycleClique.certificate_256_part_22_checked line 138
  61. def OAI.CycleClique.certificate_256_part_20 line 140
  62. theorem OAI.CycleClique.certificate_256_part_20_checked line 142
  63. def OAI.CycleClique.certificate_256_part_19 line 144
  64. theorem OAI.CycleClique.certificate_256_part_19_checked line 146
  65. def OAI.CycleClique.certificate_256_part_18 line 148
  66. theorem OAI.CycleClique.certificate_256_part_18_checked line 150
  67. def OAI.CycleClique.certificate_256_part_17 line 152
  68. theorem OAI.CycleClique.certificate_256_part_17_checked line 154
  69. def OAI.CycleClique.certificate_256_part_16 line 156
  70. theorem OAI.CycleClique.certificate_256_part_16_checked line 158
  71. def OAI.CycleClique.certificate_256_part_14 line 160
  72. theorem OAI.CycleClique.certificate_256_part_14_checked line 162
  73. def OAI.CycleClique.certificate_256_part_13 line 164
  74. theorem OAI.CycleClique.certificate_256_part_13_checked line 166
  75. def OAI.CycleClique.certificate_256_part_10 line 168
  76. theorem OAI.CycleClique.certificate_256_part_10_checked line 170
  77. def OAI.CycleClique.certificate_256_part_9 line 172
  78. theorem OAI.CycleClique.certificate_256_part_9_checked line 174
  79. def OAI.CycleClique.certificate_256_part_8 line 176
  80. theorem OAI.CycleClique.certificate_256_part_8_checked line 178
  81. def OAI.CycleClique.certificate_256_part_7 line 180
  82. theorem OAI.CycleClique.certificate_256_part_7_checked line 182
  83. def OAI.CycleClique.certificate_256_part_6 line 184
  84. theorem OAI.CycleClique.certificate_256_part_6_checked line 186
  85. def OAI.CycleClique.certificate_256_part_4 line 188
  86. theorem OAI.CycleClique.certificate_256_part_4_checked line 190
  87. def OAI.CycleClique.certificate_256_part_3 line 192
  88. theorem OAI.CycleClique.certificate_256_part_3_checked line 194
  89. def OAI.CycleClique.certificate_256_part_2 line 196
  90. theorem OAI.CycleClique.certificate_256_part_2_checked line 198
  91. def OAI.CycleClique.certificate_256_part_1 line 200
  92. theorem OAI.CycleClique.certificate_256_part_1_checked line 202
  93. def OAI.CycleClique.certificate_256 line 204
  94. theorem OAI.CycleClique.certificate_256_checked line 206
  95. theorem OAI.CycleClique.certificate_256_valid line 208
  96. def OAI.CycleClique.certificate_257_q line 210
  97. def OAI.CycleClique.certificate_257_edges line 211
  98. def OAI.CycleClique.certificate_257_part_0 line 213
  99. def OAI.CycleClique.certificate_257 line 215
  100. theorem OAI.CycleClique.certificate_257_checked line 217
  101. theorem OAI.CycleClique.certificate_257_valid line 218
  102. def OAI.CycleClique.certificate_258_q line 220
  103. def OAI.CycleClique.certificate_258_edges line 221
  104. def OAI.CycleClique.certificate_258_part_0 line 223
  105. def OAI.CycleClique.certificate_258 line 225
  106. theorem OAI.CycleClique.certificate_258_checked line 227
  107. theorem OAI.CycleClique.certificate_258_valid line 228
  108. def OAI.CycleClique.certificate_259_q line 230
  109. def OAI.CycleClique.certificate_259_edges line 231
  110. def OAI.CycleClique.certificate_259_part_0 line 233
  111. def OAI.CycleClique.certificate_259 line 235
  112. theorem OAI.CycleClique.certificate_259_checked line 237
  113. theorem OAI.CycleClique.certificate_259_valid line 238
  114. def OAI.CycleClique.certificate_260_q line 240
  115. def OAI.CycleClique.certificate_260_edges line 241
  116. def OAI.CycleClique.certificate_260_part_0 line 243
  117. def OAI.CycleClique.certificate_260_part_1 line 245
  118. def OAI.CycleClique.certificate_260 line 247
  119. theorem OAI.CycleClique.certificate_260_checked line 249
  120. theorem OAI.CycleClique.certificate_260_valid line 250
  121. def OAI.CycleClique.certificate_261_q line 252
  122. def OAI.CycleClique.certificate_261_edges line 253
  123. def OAI.CycleClique.certificate_261_part_0 line 255
  124. def OAI.CycleClique.certificate_261 line 257
  125. theorem OAI.CycleClique.certificate_261_checked line 259
  126. theorem OAI.CycleClique.certificate_261_valid line 260
  127. def OAI.CycleClique.certificate_262_q line 262
  128. def OAI.CycleClique.certificate_262_edges line 263
  129. def OAI.CycleClique.certificate_262_part_0 line 265
  130. def OAI.CycleClique.certificate_262_part_1 line 267
  131. def OAI.CycleClique.certificate_262 line 269
  132. theorem OAI.CycleClique.certificate_262_checked line 271
  133. theorem OAI.CycleClique.certificate_262_valid line 272
  134. def OAI.CycleClique.certificate_263_q line 274
  135. def OAI.CycleClique.certificate_263_edges line 275
  136. def OAI.CycleClique.certificate_263_part_0 line 277
  137. def OAI.CycleClique.certificate_263 line 279
  138. theorem OAI.CycleClique.certificate_263_checked line 281
  139. theorem OAI.CycleClique.certificate_263_valid line 282
  140. def OAI.CycleClique.certificate_264_q line 284
  141. def OAI.CycleClique.certificate_264_edges line 285
  142. def OAI.CycleClique.certificate_264_part_0 line 287
  143. def OAI.CycleClique.certificate_264 line 289
  144. theorem OAI.CycleClique.certificate_264_checked line 291
  145. theorem OAI.CycleClique.certificate_264_valid line 292
  146. def OAI.CycleClique.certificate_265_q line 294
  147. def OAI.CycleClique.certificate_265_edges line 295
  148. def OAI.CycleClique.certificate_265_part_0 line 297
  149. def OAI.CycleClique.certificate_265_part_1 line 299
  150. def OAI.CycleClique.certificate_265 line 301
  151. theorem OAI.CycleClique.certificate_265_checked line 303
  152. theorem OAI.CycleClique.certificate_265_valid line 304
  153. def OAI.CycleClique.certificate_266_q line 306
  154. def OAI.CycleClique.certificate_266_edges line 307
  155. def OAI.CycleClique.certificate_266_part_0 line 309
  156. def OAI.CycleClique.certificate_266 line 311
  157. theorem OAI.CycleClique.certificate_266_checked line 313
  158. theorem OAI.CycleClique.certificate_266_valid line 314
  159. def OAI.CycleClique.certificate_267_q line 316
  160. def OAI.CycleClique.certificate_267_edges line 317
  161. def OAI.CycleClique.certificate_267_part_0 line 319
  162. def OAI.CycleClique.certificate_267 line 321
  163. theorem OAI.CycleClique.certificate_267_checked line 323
  164. theorem OAI.CycleClique.certificate_267_valid line 324
  165. def OAI.CycleClique.certificate_268_q line 326
  166. def OAI.CycleClique.certificate_268_edges line 327
  167. def OAI.CycleClique.certificate_268_part_0 line 329
  168. def OAI.CycleClique.certificate_268_part_1 line 331
  169. def OAI.CycleClique.certificate_268 line 333
  170. theorem OAI.CycleClique.certificate_268_checked line 335
  171. theorem OAI.CycleClique.certificate_268_valid line 336
  172. def OAI.CycleClique.certificate_269_q line 338
  173. def OAI.CycleClique.certificate_269_edges line 339
  174. def OAI.CycleClique.certificate_269_part_0 line 341
  175. def OAI.CycleClique.certificate_269 line 343
  176. theorem OAI.CycleClique.certificate_269_checked line 345
  177. theorem OAI.CycleClique.certificate_269_valid line 346
  178. def OAI.CycleClique.certificate_270_q line 348
  179. def OAI.CycleClique.certificate_270_edges line 349
  180. def OAI.CycleClique.certificate_270_part_0 line 351
  181. def OAI.CycleClique.certificate_270_part_1 line 353
  182. def OAI.CycleClique.certificate_270 line 355
  183. theorem OAI.CycleClique.certificate_270_checked line 357
  184. theorem OAI.CycleClique.certificate_270_valid line 358
  185. def OAI.CycleClique.certificate_271_q line 360
  186. def OAI.CycleClique.certificate_271_edges line 361
  187. def OAI.CycleClique.certificate_271_part_0 line 363
  188. def OAI.CycleClique.certificate_271_part_1 line 365
  189. def OAI.CycleClique.certificate_271 line 367
  190. theorem OAI.CycleClique.certificate_271_checked line 369
  191. theorem OAI.CycleClique.certificate_271_valid line 370
  192. def OAI.CycleClique.certificate_272_q line 372
  193. def OAI.CycleClique.certificate_272_edges line 373
  194. def OAI.CycleClique.certificate_272_part_0 line 375
  195. def OAI.CycleClique.certificate_272 line 377
  196. theorem OAI.CycleClique.certificate_272_checked line 379
  197. theorem OAI.CycleClique.certificate_272_valid line 380
  198. def OAI.CycleClique.certificate_273_q line 382
  199. def OAI.CycleClique.certificate_273_edges line 383
  200. def OAI.CycleClique.certificate_273_part_0 line 385
  201. def OAI.CycleClique.certificate_273_part_1 line 387
  202. def OAI.CycleClique.certificate_273 line 389
  203. theorem OAI.CycleClique.certificate_273_checked line 391
  204. theorem OAI.CycleClique.certificate_273_valid line 392
  205. def OAI.CycleClique.certificate_274_q line 394
  206. def OAI.CycleClique.certificate_274_edges line 395
  207. def OAI.CycleClique.certificate_274_part_0 line 397
  208. def OAI.CycleClique.certificate_274_part_1 line 399
  209. def OAI.CycleClique.certificate_274 line 401
  210. theorem OAI.CycleClique.certificate_274_checked line 403
  211. theorem OAI.CycleClique.certificate_274_valid line 404
  212. def OAI.CycleClique.certificate_275_q line 406
  213. def OAI.CycleClique.certificate_275_edges line 407
  214. def OAI.CycleClique.certificate_275_part_0 line 409
  215. def OAI.CycleClique.certificate_275_part_1 line 411
  216. def OAI.CycleClique.certificate_275 line 413
  217. theorem OAI.CycleClique.certificate_275_checked line 415
  218. theorem OAI.CycleClique.certificate_275_valid line 416
  219. def OAI.CycleClique.certificate_276_q line 418
  220. def OAI.CycleClique.certificate_276_edges line 419
  221. def OAI.CycleClique.certificate_276_part_0 line 421
  222. def OAI.CycleClique.certificate_276_part_1 line 423
  223. def OAI.CycleClique.certificate_276 line 425
  224. theorem OAI.CycleClique.certificate_276_checked line 427
  225. theorem OAI.CycleClique.certificate_276_valid line 428
  226. def OAI.CycleClique.certificate_277_q line 430
  227. def OAI.CycleClique.certificate_277_edges line 431
  228. def OAI.CycleClique.certificate_277_part_0 line 433
  229. def OAI.CycleClique.certificate_277_part_1 line 435
  230. def OAI.CycleClique.certificate_277 line 437
  231. theorem OAI.CycleClique.certificate_277_checked line 439
  232. theorem OAI.CycleClique.certificate_277_valid line 440
  233. def OAI.CycleClique.certificate_278_q line 442
  234. def OAI.CycleClique.certificate_278_edges line 443
  235. def OAI.CycleClique.certificate_278_part_0 line 445
  236. def OAI.CycleClique.certificate_278_part_1 line 447
  237. def OAI.CycleClique.certificate_278 line 449
  238. theorem OAI.CycleClique.certificate_278_checked line 451
  239. theorem OAI.CycleClique.certificate_278_valid line 452
  240. def OAI.CycleClique.certificate_279_q line 454
  241. def OAI.CycleClique.certificate_279_edges line 455
  242. def OAI.CycleClique.certificate_279_part_0 line 457
  243. def OAI.CycleClique.certificate_279 line 459
  244. theorem OAI.CycleClique.certificate_279_checked line 461
  245. theorem OAI.CycleClique.certificate_279_valid line 462
  246. def OAI.CycleClique.certificate_280_q line 464
  247. def OAI.CycleClique.certificate_280_edges line 465
  248. def OAI.CycleClique.certificate_280_part_0 line 467
  249. def OAI.CycleClique.certificate_280 line 469
  250. theorem OAI.CycleClique.certificate_280_checked line 471
  251. theorem OAI.CycleClique.certificate_280_valid line 472
  252. def OAI.CycleClique.certificate_281_q line 474
  253. def OAI.CycleClique.certificate_281_edges line 475
  254. def OAI.CycleClique.certificate_281_part_0 line 477
  255. def OAI.CycleClique.certificate_281 line 479
  256. theorem OAI.CycleClique.certificate_281_checked line 481
  257. theorem OAI.CycleClique.certificate_281_valid line 482
  258. def OAI.CycleClique.certificate_282_q line 484
  259. def OAI.CycleClique.certificate_282_edges line 485
  260. def OAI.CycleClique.certificate_282_part_0 line 487
  261. def OAI.CycleClique.certificate_282 line 489
  262. theorem OAI.CycleClique.certificate_282_checked line 491
  263. theorem OAI.CycleClique.certificate_282_valid line 492
  264. def OAI.CycleClique.certificate_283_q line 494
  265. def OAI.CycleClique.certificate_283_edges line 495
  266. def OAI.CycleClique.certificate_283_part_0 line 497
  267. def OAI.CycleClique.certificate_283_part_1 line 499
  268. def OAI.CycleClique.certificate_283 line 501
  269. theorem OAI.CycleClique.certificate_283_checked line 503
  270. theorem OAI.CycleClique.certificate_283_valid line 504
  271. def OAI.CycleClique.certificate_284_q line 506
  272. def OAI.CycleClique.certificate_284_edges line 508
  273. def OAI.CycleClique.certificate_284_E line 510
  274. def OAI.CycleClique.certificate_284_M line 512
  275. def OAI.CycleClique.certificate_284_part_1_E line 514
  276. def OAI.CycleClique.certificate_284_part_1_M line 516
  277. def OAI.CycleClique.certificate_284_part_2_E line 518
  278. def OAI.CycleClique.certificate_284_part_2_M line 520
  279. def OAI.CycleClique.certificate_284_part_3_E line 522
  280. def OAI.CycleClique.certificate_284_part_3_M line 524
  281. def OAI.CycleClique.certificate_284_part_4_E line 526
  282. def OAI.CycleClique.certificate_284_part_4_M line 528
  283. def OAI.CycleClique.certificate_284_part_5_E line 530
  284. def OAI.CycleClique.certificate_284_part_5_M line 532
  285. def OAI.CycleClique.certificate_284_part_6_E line 534
  286. def OAI.CycleClique.certificate_284_part_6_M line 536
  287. def OAI.CycleClique.certificate_284_part_6 line 538
  288. theorem OAI.CycleClique.certificate_284_part_6_checked line 540
  289. def OAI.CycleClique.certificate_284_part_7_E line 542
  290. def OAI.CycleClique.certificate_284_part_7_M line 544
  291. def OAI.CycleClique.certificate_284_part_8_E line 546
  292. def OAI.CycleClique.certificate_284_part_8_M line 548
  293. def OAI.CycleClique.certificate_284_part_9_E line 550
  294. def OAI.CycleClique.certificate_284_part_9_M line 552
  295. def OAI.CycleClique.certificate_284_part_10_E line 554
  296. def OAI.CycleClique.certificate_284_part_10_M line 556
  297. def OAI.CycleClique.certificate_284_part_10 line 558
  298. theorem OAI.CycleClique.certificate_284_part_10_checked line 560
  299. def OAI.CycleClique.certificate_284_part_9 line 562
  300. theorem OAI.CycleClique.certificate_284_part_9_checked line 564
  301. def OAI.CycleClique.certificate_284_part_11_E line 566
  302. def OAI.CycleClique.certificate_284_part_11_M line 568
  303. def OAI.CycleClique.certificate_284_part_12_E line 570
  304. def OAI.CycleClique.certificate_284_part_12_M line 572
  305. def OAI.CycleClique.certificate_284_part_13_E line 574
  306. def OAI.CycleClique.certificate_284_part_13_M line 576
  307. def OAI.CycleClique.certificate_284_part_13 line 578
  308. theorem OAI.CycleClique.certificate_284_part_13_checked line 580
  309. def OAI.CycleClique.certificate_284_part_12 line 582
  310. theorem OAI.CycleClique.certificate_284_part_12_checked line 584
  311. def OAI.CycleClique.certificate_284_part_11 line 586
  312. theorem OAI.CycleClique.certificate_284_part_11_checked line 588
  313. def OAI.CycleClique.certificate_284_part_14_E line 590
  314. def OAI.CycleClique.certificate_284_part_14_M line 592
  315. def OAI.CycleClique.certificate_284_part_15_E line 594
  316. def OAI.CycleClique.certificate_284_part_15_M line 596
  317. def OAI.CycleClique.certificate_284_part_15 line 598
  318. theorem OAI.CycleClique.certificate_284_part_15_checked line 600
  319. def OAI.CycleClique.certificate_284_part_14 line 602
  320. theorem OAI.CycleClique.certificate_284_part_14_checked line 604
  321. def OAI.CycleClique.certificate_284_part_16_E line 606
  322. def OAI.CycleClique.certificate_284_part_16_M line 608
  323. def OAI.CycleClique.certificate_284_part_17_E line 610
  324. def OAI.CycleClique.certificate_284_part_17_M line 612
  325. def OAI.CycleClique.certificate_284_part_17 line 614
  326. theorem OAI.CycleClique.certificate_284_part_17_checked line 616
  327. def OAI.CycleClique.certificate_284_part_16 line 618
  328. theorem OAI.CycleClique.certificate_284_part_16_checked line 620
  329. def OAI.CycleClique.certificate_284_part_18_E line 622
  330. def OAI.CycleClique.certificate_284_part_18_M line 624
  331. def OAI.CycleClique.certificate_284_part_19_E line 626
  332. def OAI.CycleClique.certificate_284_part_19_M line 628
  333. def OAI.CycleClique.certificate_284_part_20_E line 630
  334. def OAI.CycleClique.certificate_284_part_20_M line 632
  335. def OAI.CycleClique.certificate_284_part_20 line 634
  336. theorem OAI.CycleClique.certificate_284_part_20_checked line 636
  337. def OAI.CycleClique.certificate_284_part_21_E line 638
  338. def OAI.CycleClique.certificate_284_part_21_M line 640
  339. def OAI.CycleClique.certificate_284_part_21 line 642
  340. theorem OAI.CycleClique.certificate_284_part_21_checked line 644
  341. def OAI.CycleClique.certificate_284_part_22_E line 646
  342. def OAI.CycleClique.certificate_284_part_22_M line 648
  343. def OAI.CycleClique.certificate_284_part_23_E line 650
  344. def OAI.CycleClique.certificate_284_part_23_M line 652
  345. def OAI.CycleClique.certificate_284_part_24_E line 654
  346. def OAI.CycleClique.certificate_284_part_24_M line 656
  347. def OAI.CycleClique.certificate_284_part_24 line 658
  348. theorem OAI.CycleClique.certificate_284_part_24_checked line 660
  349. def OAI.CycleClique.certificate_284_part_23 line 662
  350. theorem OAI.CycleClique.certificate_284_part_23_checked line 664
  351. def OAI.CycleClique.certificate_284_part_25_E line 666
  352. def OAI.CycleClique.certificate_284_part_25_M line 668
  353. def OAI.CycleClique.certificate_284_part_26_E line 670
  354. def OAI.CycleClique.certificate_284_part_26_M line 672
  355. def OAI.CycleClique.certificate_284_part_26 line 674
  356. theorem OAI.CycleClique.certificate_284_part_26_checked line 676
  357. def OAI.CycleClique.certificate_284_part_25 line 678
  358. theorem OAI.CycleClique.certificate_284_part_25_checked line 680
  359. def OAI.CycleClique.certificate_284_part_27_E line 682
  360. def OAI.CycleClique.certificate_284_part_27_M line 684
  361. def OAI.CycleClique.certificate_284_part_28_E line 686
  362. def OAI.CycleClique.certificate_284_part_28_M line 688
  363. def OAI.CycleClique.certificate_284_part_28 line 690
  364. theorem OAI.CycleClique.certificate_284_part_28_checked line 692
  365. def OAI.CycleClique.certificate_284_part_27 line 694
  366. theorem OAI.CycleClique.certificate_284_part_27_checked line 696
  367. def OAI.CycleClique.certificate_284_part_29_E line 698
  368. def OAI.CycleClique.certificate_284_part_29_M line 700
  369. def OAI.CycleClique.certificate_284_part_30_E line 702
  370. def OAI.CycleClique.certificate_284_part_30_M line 704
  371. def OAI.CycleClique.certificate_284_part_30 line 706
  372. theorem OAI.CycleClique.certificate_284_part_30_checked line 708
  373. def OAI.CycleClique.certificate_284_part_29 line 710
  374. theorem OAI.CycleClique.certificate_284_part_29_checked line 712
  375. def OAI.CycleClique.certificate_284_part_31_E line 714
  376. def OAI.CycleClique.certificate_284_part_31_M line 716
  377. def OAI.CycleClique.certificate_284_part_31 line 718
  378. theorem OAI.CycleClique.certificate_284_part_31_checked line 720
  379. def OAI.CycleClique.certificate_284_part_32_E line 722
  380. def OAI.CycleClique.certificate_284_part_32_M line 724
  381. def OAI.CycleClique.certificate_284_part_33_E line 726
  382. def OAI.CycleClique.certificate_284_part_33_M line 728
  383. def OAI.CycleClique.certificate_284_part_33 line 730
  384. theorem OAI.CycleClique.certificate_284_part_33_checked line 732
  385. def OAI.CycleClique.certificate_284_part_34_E line 734
  386. def OAI.CycleClique.certificate_284_part_34_M line 736
  387. def OAI.CycleClique.certificate_284_part_35_E line 738
  388. def OAI.CycleClique.certificate_284_part_35_M line 740
  389. def OAI.CycleClique.certificate_284_part_35 line 742
  390. theorem OAI.CycleClique.certificate_284_part_35_checked line 744
  391. def OAI.CycleClique.certificate_284_part_34 line 746
  392. theorem OAI.CycleClique.certificate_284_part_34_checked line 748
  393. def OAI.CycleClique.certificate_284_part_36_E line 750
  394. def OAI.CycleClique.certificate_284_part_36_M line 752
  395. def OAI.CycleClique.certificate_284_part_37_E line 754
  396. def OAI.CycleClique.certificate_284_part_37_M line 756
  397. def OAI.CycleClique.certificate_284_part_38_E line 758
  398. def OAI.CycleClique.certificate_284_part_38_M line 760
  399. def OAI.CycleClique.certificate_284_part_38 line 762
  400. theorem OAI.CycleClique.certificate_284_part_38_checked line 764
  401. def OAI.CycleClique.certificate_284_part_37 line 766
  402. theorem OAI.CycleClique.certificate_284_part_37_checked line 768
  403. def OAI.CycleClique.certificate_284_part_36 line 770
  404. theorem OAI.CycleClique.certificate_284_part_36_checked line 772
  405. def OAI.CycleClique.certificate_284_part_39_E line 774
  406. def OAI.CycleClique.certificate_284_part_39_M line 776
  407. def OAI.CycleClique.certificate_284_part_40_E line 778
  408. def OAI.CycleClique.certificate_284_part_40_M line 780
  409. def OAI.CycleClique.certificate_284_part_40 line 782
  410. theorem OAI.CycleClique.certificate_284_part_40_checked line 784
  411. def OAI.CycleClique.certificate_284_part_39 line 786
  412. theorem OAI.CycleClique.certificate_284_part_39_checked line 788
  413. def OAI.CycleClique.certificate_284_part_41_E line 790
  414. def OAI.CycleClique.certificate_284_part_41_M line 792
  415. def OAI.CycleClique.certificate_284_part_42_E line 794
  416. def OAI.CycleClique.certificate_284_part_42_M line 796
  417. def OAI.CycleClique.certificate_284_part_42 line 798
  418. theorem OAI.CycleClique.certificate_284_part_42_checked line 800
  419. def OAI.CycleClique.certificate_284_part_41 line 802
  420. theorem OAI.CycleClique.certificate_284_part_41_checked line 804
  421. def OAI.CycleClique.certificate_284_part_43_E line 806
  422. def OAI.CycleClique.certificate_284_part_43_M line 808
  423. def OAI.CycleClique.certificate_284_part_44_E line 810
  424. def OAI.CycleClique.certificate_284_part_44_M line 812
  425. def OAI.CycleClique.certificate_284_part_44 line 814
  426. theorem OAI.CycleClique.certificate_284_part_44_checked line 816
  427. def OAI.CycleClique.certificate_284_part_45_E line 818
  428. def OAI.CycleClique.certificate_284_part_45_M line 820
  429. def OAI.CycleClique.certificate_284_part_46_E line 822
  430. def OAI.CycleClique.certificate_284_part_46_M line 824
  431. def OAI.CycleClique.certificate_284_part_46 line 826
  432. theorem OAI.CycleClique.certificate_284_part_46_checked line 828
  433. def OAI.CycleClique.certificate_284_part_47_E line 830
  434. def OAI.CycleClique.certificate_284_part_47_M line 832
  435. def OAI.CycleClique.certificate_284_part_48_E line 834
  436. def OAI.CycleClique.certificate_284_part_48_M line 836
  437. def OAI.CycleClique.certificate_284_part_48 line 838
  438. theorem OAI.CycleClique.certificate_284_part_48_checked line 840
  439. def OAI.CycleClique.certificate_284_part_47 line 842
  440. theorem OAI.CycleClique.certificate_284_part_47_checked line 844
  441. def OAI.CycleClique.certificate_284_part_49_E line 846
  442. def OAI.CycleClique.certificate_284_part_49_M line 848
  443. def OAI.CycleClique.certificate_284_part_50_E line 850
  444. def OAI.CycleClique.certificate_284_part_50_M line 852
  445. def OAI.CycleClique.certificate_284_part_50 line 854
  446. theorem OAI.CycleClique.certificate_284_part_50_checked line 856
  447. def OAI.CycleClique.certificate_284_part_51_E line 858
  448. def OAI.CycleClique.certificate_284_part_51_M line 860
  449. def OAI.CycleClique.certificate_284_part_51 line 862
  450. theorem OAI.CycleClique.certificate_284_part_51_checked line 864
  451. def OAI.CycleClique.certificate_284_part_49 line 866
  452. theorem OAI.CycleClique.certificate_284_part_49_checked line 868
  453. def OAI.CycleClique.certificate_284_part_45 line 870
  454. theorem OAI.CycleClique.certificate_284_part_45_checked line 872
  455. def OAI.CycleClique.certificate_284_part_43 line 874
  456. theorem OAI.CycleClique.certificate_284_part_43_checked line 876
  457. def OAI.CycleClique.certificate_284_part_32 line 878
  458. theorem OAI.CycleClique.certificate_284_part_32_checked line 880
  459. def OAI.CycleClique.certificate_284_part_22 line 882
  460. theorem OAI.CycleClique.certificate_284_part_22_checked line 884
  461. def OAI.CycleClique.certificate_284_part_19 line 886
  462. theorem OAI.CycleClique.certificate_284_part_19_checked line 888
  463. def OAI.CycleClique.certificate_284_part_18 line 890
  464. theorem OAI.CycleClique.certificate_284_part_18_checked line 892
  465. def OAI.CycleClique.certificate_284_part_8 line 894
  466. theorem OAI.CycleClique.certificate_284_part_8_checked line 896
  467. def OAI.CycleClique.certificate_284_part_7 line 898
  468. theorem OAI.CycleClique.certificate_284_part_7_checked line 900
  469. def OAI.CycleClique.certificate_284_part_5 line 902
  470. theorem OAI.CycleClique.certificate_284_part_5_checked line 904
  471. def OAI.CycleClique.certificate_284_part_4 line 906
  472. theorem OAI.CycleClique.certificate_284_part_4_checked line 908
  473. def OAI.CycleClique.certificate_284_part_3 line 910
  474. theorem OAI.CycleClique.certificate_284_part_3_checked line 912
  475. def OAI.CycleClique.certificate_284_part_2 line 914
  476. theorem OAI.CycleClique.certificate_284_part_2_checked line 916
  477. def OAI.CycleClique.certificate_284_part_1 line 918
  478. theorem OAI.CycleClique.certificate_284_part_1_checked line 920
  479. def OAI.CycleClique.certificate_284 line 922
  480. theorem OAI.CycleClique.certificate_284_checked line 924
  481. theorem OAI.CycleClique.certificate_284_valid line 926
  482. def OAI.CycleClique.certificate_285_q line 928
  483. def OAI.CycleClique.certificate_285_edges line 929
  484. def OAI.CycleClique.certificate_285_part_0 line 931
  485. def OAI.CycleClique.certificate_285 line 933
  486. theorem OAI.CycleClique.certificate_285_checked line 935
  487. theorem OAI.CycleClique.certificate_285_valid line 936
  488. def OAI.CycleClique.certificate_286_q line 938
  489. def OAI.CycleClique.certificate_286_edges line 939
  490. def OAI.CycleClique.certificate_286_part_0 line 941
  491. def OAI.CycleClique.certificate_286 line 943
  492. theorem OAI.CycleClique.certificate_286_checked line 945
  493. theorem OAI.CycleClique.certificate_286_valid line 946
  494. def OAI.CycleClique.certificate_287_q line 948
  495. def OAI.CycleClique.certificate_287_edges line 949
  496. def OAI.CycleClique.certificate_287_part_0 line 951
  497. def OAI.CycleClique.certificate_287_part_1 line 953
  498. def OAI.CycleClique.certificate_287 line 955
  499. theorem OAI.CycleClique.certificate_287_checked line 957
  500. theorem OAI.CycleClique.certificate_287_valid line 958