OAI/Combinatorics/Ramsey/CycleClique/Certificates003.lean

GitHub source file

596 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.certificate_64_q line 20
  2. def OAI.CycleClique.certificate_64_edges line 21
  3. def OAI.CycleClique.certificate_64_part_0 line 23
  4. def OAI.CycleClique.certificate_64 line 25
  5. theorem OAI.CycleClique.certificate_64_checked line 27
  6. theorem OAI.CycleClique.certificate_64_valid line 28
  7. def OAI.CycleClique.certificate_65_q line 30
  8. def OAI.CycleClique.certificate_65_edges line 31
  9. def OAI.CycleClique.certificate_65_part_0 line 33
  10. def OAI.CycleClique.certificate_65 line 35
  11. theorem OAI.CycleClique.certificate_65_checked line 37
  12. theorem OAI.CycleClique.certificate_65_valid line 38
  13. def OAI.CycleClique.certificate_66_q line 40
  14. def OAI.CycleClique.certificate_66_edges line 42
  15. def OAI.CycleClique.certificate_66_E line 44
  16. def OAI.CycleClique.certificate_66_M line 46
  17. def OAI.CycleClique.certificate_66_part_1_E line 48
  18. def OAI.CycleClique.certificate_66_part_1_M line 50
  19. def OAI.CycleClique.certificate_66_part_2_E line 52
  20. def OAI.CycleClique.certificate_66_part_2_M line 54
  21. def OAI.CycleClique.certificate_66_part_3_E line 56
  22. def OAI.CycleClique.certificate_66_part_3_M line 58
  23. def OAI.CycleClique.certificate_66_part_3 line 60
  24. theorem OAI.CycleClique.certificate_66_part_3_checked line 62
  25. def OAI.CycleClique.certificate_66_part_4_E line 64
  26. def OAI.CycleClique.certificate_66_part_4_M line 66
  27. def OAI.CycleClique.certificate_66_part_5_E line 68
  28. def OAI.CycleClique.certificate_66_part_5_M line 70
  29. def OAI.CycleClique.certificate_66_part_5 line 72
  30. theorem OAI.CycleClique.certificate_66_part_5_checked line 74
  31. def OAI.CycleClique.certificate_66_part_6_E line 76
  32. def OAI.CycleClique.certificate_66_part_6_M line 78
  33. def OAI.CycleClique.certificate_66_part_7_E line 80
  34. def OAI.CycleClique.certificate_66_part_7_M line 82
  35. def OAI.CycleClique.certificate_66_part_8_E line 84
  36. def OAI.CycleClique.certificate_66_part_8_M line 86
  37. def OAI.CycleClique.certificate_66_part_8 line 88
  38. theorem OAI.CycleClique.certificate_66_part_8_checked line 90
  39. def OAI.CycleClique.certificate_66_part_9_E line 92
  40. def OAI.CycleClique.certificate_66_part_9_M line 94
  41. def OAI.CycleClique.certificate_66_part_10_E line 96
  42. def OAI.CycleClique.certificate_66_part_10_M line 98
  43. def OAI.CycleClique.certificate_66_part_10 line 100
  44. theorem OAI.CycleClique.certificate_66_part_10_checked line 102
  45. def OAI.CycleClique.certificate_66_part_11_E line 104
  46. def OAI.CycleClique.certificate_66_part_11_M line 106
  47. def OAI.CycleClique.certificate_66_part_11 line 108
  48. theorem OAI.CycleClique.certificate_66_part_11_checked line 110
  49. def OAI.CycleClique.certificate_66_part_12_E line 112
  50. def OAI.CycleClique.certificate_66_part_12_M line 114
  51. def OAI.CycleClique.certificate_66_part_12 line 116
  52. theorem OAI.CycleClique.certificate_66_part_12_checked line 118
  53. def OAI.CycleClique.certificate_66_part_9 line 120
  54. theorem OAI.CycleClique.certificate_66_part_9_checked line 122
  55. def OAI.CycleClique.certificate_66_part_7 line 124
  56. theorem OAI.CycleClique.certificate_66_part_7_checked line 126
  57. def OAI.CycleClique.certificate_66_part_6 line 128
  58. theorem OAI.CycleClique.certificate_66_part_6_checked line 130
  59. def OAI.CycleClique.certificate_66_part_4 line 132
  60. theorem OAI.CycleClique.certificate_66_part_4_checked line 134
  61. def OAI.CycleClique.certificate_66_part_2 line 136
  62. theorem OAI.CycleClique.certificate_66_part_2_checked line 138
  63. def OAI.CycleClique.certificate_66_part_1 line 140
  64. theorem OAI.CycleClique.certificate_66_part_1_checked line 142
  65. def OAI.CycleClique.certificate_66 line 144
  66. theorem OAI.CycleClique.certificate_66_checked line 146
  67. theorem OAI.CycleClique.certificate_66_valid line 148
  68. def OAI.CycleClique.certificate_67_q line 150
  69. def OAI.CycleClique.certificate_67_edges line 151
  70. def OAI.CycleClique.certificate_67_part_0 line 153
  71. def OAI.CycleClique.certificate_67 line 155
  72. theorem OAI.CycleClique.certificate_67_checked line 157
  73. theorem OAI.CycleClique.certificate_67_valid line 158
  74. def OAI.CycleClique.certificate_68_q line 160
  75. def OAI.CycleClique.certificate_68_edges line 161
  76. def OAI.CycleClique.certificate_68_part_0 line 163
  77. def OAI.CycleClique.certificate_68 line 165
  78. theorem OAI.CycleClique.certificate_68_checked line 167
  79. theorem OAI.CycleClique.certificate_68_valid line 168
  80. def OAI.CycleClique.certificate_69_q line 170
  81. def OAI.CycleClique.certificate_69_edges line 171
  82. def OAI.CycleClique.certificate_69_part_0 line 173
  83. def OAI.CycleClique.certificate_69 line 175
  84. theorem OAI.CycleClique.certificate_69_checked line 177
  85. theorem OAI.CycleClique.certificate_69_valid line 178
  86. def OAI.CycleClique.certificate_70_q line 180
  87. def OAI.CycleClique.certificate_70_edges line 181
  88. def OAI.CycleClique.certificate_70_part_0 line 183
  89. def OAI.CycleClique.certificate_70 line 185
  90. theorem OAI.CycleClique.certificate_70_checked line 187
  91. theorem OAI.CycleClique.certificate_70_valid line 188
  92. def OAI.CycleClique.certificate_71_q line 190
  93. def OAI.CycleClique.certificate_71_edges line 191
  94. def OAI.CycleClique.certificate_71_part_0 line 193
  95. def OAI.CycleClique.certificate_71 line 195
  96. theorem OAI.CycleClique.certificate_71_checked line 197
  97. theorem OAI.CycleClique.certificate_71_valid line 198
  98. def OAI.CycleClique.certificate_72_q line 200
  99. def OAI.CycleClique.certificate_72_edges line 201
  100. def OAI.CycleClique.certificate_72_part_0 line 203
  101. def OAI.CycleClique.certificate_72 line 205
  102. theorem OAI.CycleClique.certificate_72_checked line 207
  103. theorem OAI.CycleClique.certificate_72_valid line 208
  104. def OAI.CycleClique.certificate_73_q line 210
  105. def OAI.CycleClique.certificate_73_edges line 211
  106. def OAI.CycleClique.certificate_73_part_0 line 213
  107. def OAI.CycleClique.certificate_73 line 215
  108. theorem OAI.CycleClique.certificate_73_checked line 217
  109. theorem OAI.CycleClique.certificate_73_valid line 218
  110. def OAI.CycleClique.certificate_74_q line 220
  111. def OAI.CycleClique.certificate_74_edges line 221
  112. def OAI.CycleClique.certificate_74_part_0 line 223
  113. def OAI.CycleClique.certificate_74 line 225
  114. theorem OAI.CycleClique.certificate_74_checked line 227
  115. theorem OAI.CycleClique.certificate_74_valid line 228
  116. def OAI.CycleClique.certificate_75_q line 230
  117. def OAI.CycleClique.certificate_75_edges line 231
  118. def OAI.CycleClique.certificate_75_part_0 line 233
  119. def OAI.CycleClique.certificate_75 line 235
  120. theorem OAI.CycleClique.certificate_75_checked line 237
  121. theorem OAI.CycleClique.certificate_75_valid line 238
  122. def OAI.CycleClique.certificate_76_q line 240
  123. def OAI.CycleClique.certificate_76_edges line 241
  124. def OAI.CycleClique.certificate_76_part_0 line 243
  125. def OAI.CycleClique.certificate_76 line 245
  126. theorem OAI.CycleClique.certificate_76_checked line 247
  127. theorem OAI.CycleClique.certificate_76_valid line 248
  128. def OAI.CycleClique.certificate_77_q line 250
  129. def OAI.CycleClique.certificate_77_edges line 251
  130. def OAI.CycleClique.certificate_77_part_0 line 253
  131. def OAI.CycleClique.certificate_77 line 255
  132. theorem OAI.CycleClique.certificate_77_checked line 257
  133. theorem OAI.CycleClique.certificate_77_valid line 258
  134. def OAI.CycleClique.certificate_78_q line 260
  135. def OAI.CycleClique.certificate_78_edges line 261
  136. def OAI.CycleClique.certificate_78_part_0 line 263
  137. def OAI.CycleClique.certificate_78 line 265
  138. theorem OAI.CycleClique.certificate_78_checked line 267
  139. theorem OAI.CycleClique.certificate_78_valid line 268
  140. def OAI.CycleClique.certificate_79_q line 270
  141. def OAI.CycleClique.certificate_79_edges line 271
  142. def OAI.CycleClique.certificate_79_part_0 line 273
  143. def OAI.CycleClique.certificate_79_part_1 line 275
  144. def OAI.CycleClique.certificate_79 line 277
  145. theorem OAI.CycleClique.certificate_79_checked line 279
  146. theorem OAI.CycleClique.certificate_79_valid line 280
  147. def OAI.CycleClique.certificate_80_q line 282
  148. def OAI.CycleClique.certificate_80_edges line 283
  149. def OAI.CycleClique.certificate_80_part_0 line 285
  150. def OAI.CycleClique.certificate_80_part_1 line 287
  151. def OAI.CycleClique.certificate_80_part_2 line 289
  152. def OAI.CycleClique.certificate_80_part_3 line 291
  153. def OAI.CycleClique.certificate_80 line 293
  154. theorem OAI.CycleClique.certificate_80_checked line 295
  155. theorem OAI.CycleClique.certificate_80_valid line 296
  156. def OAI.CycleClique.certificate_81_q line 298
  157. def OAI.CycleClique.certificate_81_edges line 299
  158. def OAI.CycleClique.certificate_81_part_0 line 301
  159. def OAI.CycleClique.certificate_81 line 303
  160. theorem OAI.CycleClique.certificate_81_checked line 305
  161. theorem OAI.CycleClique.certificate_81_valid line 306
  162. def OAI.CycleClique.certificate_82_q line 308
  163. def OAI.CycleClique.certificate_82_edges line 309
  164. def OAI.CycleClique.certificate_82_part_0 line 311
  165. def OAI.CycleClique.certificate_82 line 313
  166. theorem OAI.CycleClique.certificate_82_checked line 315
  167. theorem OAI.CycleClique.certificate_82_valid line 316
  168. def OAI.CycleClique.certificate_83_q line 318
  169. def OAI.CycleClique.certificate_83_edges line 319
  170. def OAI.CycleClique.certificate_83_part_0 line 321
  171. def OAI.CycleClique.certificate_83 line 323
  172. theorem OAI.CycleClique.certificate_83_checked line 325
  173. theorem OAI.CycleClique.certificate_83_valid line 326
  174. def OAI.CycleClique.certificate_84_q line 328
  175. def OAI.CycleClique.certificate_84_edges line 329
  176. def OAI.CycleClique.certificate_84_part_0 line 331
  177. def OAI.CycleClique.certificate_84 line 333
  178. theorem OAI.CycleClique.certificate_84_checked line 335
  179. theorem OAI.CycleClique.certificate_84_valid line 336
  180. def OAI.CycleClique.certificate_85_q line 338
  181. def OAI.CycleClique.certificate_85_edges line 340
  182. def OAI.CycleClique.certificate_85_E line 342
  183. def OAI.CycleClique.certificate_85_M line 344
  184. def OAI.CycleClique.certificate_85_part_1_E line 346
  185. def OAI.CycleClique.certificate_85_part_1_M line 348
  186. def OAI.CycleClique.certificate_85_part_2_E line 350
  187. def OAI.CycleClique.certificate_85_part_2_M line 352
  188. def OAI.CycleClique.certificate_85_part_3_E line 354
  189. def OAI.CycleClique.certificate_85_part_3_M line 356
  190. def OAI.CycleClique.certificate_85_part_4_E line 358
  191. def OAI.CycleClique.certificate_85_part_4_M line 360
  192. def OAI.CycleClique.certificate_85_part_4 line 362
  193. theorem OAI.CycleClique.certificate_85_part_4_checked line 364
  194. def OAI.CycleClique.certificate_85_part_5_E line 366
  195. def OAI.CycleClique.certificate_85_part_5_M line 368
  196. def OAI.CycleClique.certificate_85_part_6_E line 370
  197. def OAI.CycleClique.certificate_85_part_6_M line 372
  198. def OAI.CycleClique.certificate_85_part_7_E line 374
  199. def OAI.CycleClique.certificate_85_part_7_M line 376
  200. def OAI.CycleClique.certificate_85_part_8_E line 378
  201. def OAI.CycleClique.certificate_85_part_8_M line 380
  202. def OAI.CycleClique.certificate_85_part_8 line 382
  203. theorem OAI.CycleClique.certificate_85_part_8_checked line 384
  204. def OAI.CycleClique.certificate_85_part_9_E line 386
  205. def OAI.CycleClique.certificate_85_part_9_M line 388
  206. def OAI.CycleClique.certificate_85_part_9 line 390
  207. theorem OAI.CycleClique.certificate_85_part_9_checked line 392
  208. def OAI.CycleClique.certificate_85_part_10_E line 394
  209. def OAI.CycleClique.certificate_85_part_10_M line 396
  210. def OAI.CycleClique.certificate_85_part_11_E line 398
  211. def OAI.CycleClique.certificate_85_part_11_M line 400
  212. def OAI.CycleClique.certificate_85_part_11 line 402
  213. theorem OAI.CycleClique.certificate_85_part_11_checked line 404
  214. def OAI.CycleClique.certificate_85_part_12_E line 406
  215. def OAI.CycleClique.certificate_85_part_12_M line 408
  216. def OAI.CycleClique.certificate_85_part_12 line 410
  217. theorem OAI.CycleClique.certificate_85_part_12_checked line 412
  218. def OAI.CycleClique.certificate_85_part_13_E line 414
  219. def OAI.CycleClique.certificate_85_part_13_M line 416
  220. def OAI.CycleClique.certificate_85_part_13 line 418
  221. theorem OAI.CycleClique.certificate_85_part_13_checked line 420
  222. def OAI.CycleClique.certificate_85_part_10 line 422
  223. theorem OAI.CycleClique.certificate_85_part_10_checked line 424
  224. def OAI.CycleClique.certificate_85_part_7 line 426
  225. theorem OAI.CycleClique.certificate_85_part_7_checked line 428
  226. def OAI.CycleClique.certificate_85_part_6 line 430
  227. theorem OAI.CycleClique.certificate_85_part_6_checked line 432
  228. def OAI.CycleClique.certificate_85_part_5 line 434
  229. theorem OAI.CycleClique.certificate_85_part_5_checked line 436
  230. def OAI.CycleClique.certificate_85_part_3 line 438
  231. theorem OAI.CycleClique.certificate_85_part_3_checked line 440
  232. def OAI.CycleClique.certificate_85_part_2 line 442
  233. theorem OAI.CycleClique.certificate_85_part_2_checked line 444
  234. def OAI.CycleClique.certificate_85_part_1 line 446
  235. theorem OAI.CycleClique.certificate_85_part_1_checked line 448
  236. def OAI.CycleClique.certificate_85 line 450
  237. theorem OAI.CycleClique.certificate_85_checked line 452
  238. theorem OAI.CycleClique.certificate_85_valid line 454
  239. def OAI.CycleClique.certificate_86_q line 456
  240. def OAI.CycleClique.certificate_86_edges line 458
  241. def OAI.CycleClique.certificate_86_E line 460
  242. def OAI.CycleClique.certificate_86_M line 462
  243. def OAI.CycleClique.certificate_86_part_1_E line 464
  244. def OAI.CycleClique.certificate_86_part_1_M line 466
  245. def OAI.CycleClique.certificate_86_part_2_E line 468
  246. def OAI.CycleClique.certificate_86_part_2_M line 470
  247. def OAI.CycleClique.certificate_86_part_3_E line 472
  248. def OAI.CycleClique.certificate_86_part_3_M line 474
  249. def OAI.CycleClique.certificate_86_part_3 line 476
  250. theorem OAI.CycleClique.certificate_86_part_3_checked line 478
  251. def OAI.CycleClique.certificate_86_part_4_E line 480
  252. def OAI.CycleClique.certificate_86_part_4_M line 482
  253. def OAI.CycleClique.certificate_86_part_5_E line 484
  254. def OAI.CycleClique.certificate_86_part_5_M line 486
  255. def OAI.CycleClique.certificate_86_part_6_E line 488
  256. def OAI.CycleClique.certificate_86_part_6_M line 490
  257. def OAI.CycleClique.certificate_86_part_6 line 492
  258. theorem OAI.CycleClique.certificate_86_part_6_checked line 494
  259. def OAI.CycleClique.certificate_86_part_5 line 496
  260. theorem OAI.CycleClique.certificate_86_part_5_checked line 498
  261. def OAI.CycleClique.certificate_86_part_4 line 500
  262. theorem OAI.CycleClique.certificate_86_part_4_checked line 502
  263. def OAI.CycleClique.certificate_86_part_7_E line 504
  264. def OAI.CycleClique.certificate_86_part_7_M line 506
  265. def OAI.CycleClique.certificate_86_part_8_E line 508
  266. def OAI.CycleClique.certificate_86_part_8_M line 510
  267. def OAI.CycleClique.certificate_86_part_8 line 512
  268. theorem OAI.CycleClique.certificate_86_part_8_checked line 514
  269. def OAI.CycleClique.certificate_86_part_9_E line 516
  270. def OAI.CycleClique.certificate_86_part_9_M line 518
  271. def OAI.CycleClique.certificate_86_part_10_E line 520
  272. def OAI.CycleClique.certificate_86_part_10_M line 522
  273. def OAI.CycleClique.certificate_86_part_10 line 524
  274. theorem OAI.CycleClique.certificate_86_part_10_checked line 526
  275. def OAI.CycleClique.certificate_86_part_11_E line 528
  276. def OAI.CycleClique.certificate_86_part_11_M line 530
  277. def OAI.CycleClique.certificate_86_part_12_E line 532
  278. def OAI.CycleClique.certificate_86_part_12_M line 534
  279. def OAI.CycleClique.certificate_86_part_13_E line 536
  280. def OAI.CycleClique.certificate_86_part_13_M line 538
  281. def OAI.CycleClique.certificate_86_part_13 line 540
  282. theorem OAI.CycleClique.certificate_86_part_13_checked line 542
  283. def OAI.CycleClique.certificate_86_part_12 line 544
  284. theorem OAI.CycleClique.certificate_86_part_12_checked line 546
  285. def OAI.CycleClique.certificate_86_part_11 line 548
  286. theorem OAI.CycleClique.certificate_86_part_11_checked line 550
  287. def OAI.CycleClique.certificate_86_part_14_E line 552
  288. def OAI.CycleClique.certificate_86_part_14_M line 554
  289. def OAI.CycleClique.certificate_86_part_15_E line 556
  290. def OAI.CycleClique.certificate_86_part_15_M line 558
  291. def OAI.CycleClique.certificate_86_part_16_E line 560
  292. def OAI.CycleClique.certificate_86_part_16_M line 562
  293. def OAI.CycleClique.certificate_86_part_17_E line 564
  294. def OAI.CycleClique.certificate_86_part_17_M line 566
  295. def OAI.CycleClique.certificate_86_part_18_E line 568
  296. def OAI.CycleClique.certificate_86_part_18_M line 570
  297. def OAI.CycleClique.certificate_86_part_18 line 572
  298. theorem OAI.CycleClique.certificate_86_part_18_checked line 574
  299. def OAI.CycleClique.certificate_86_part_17 line 576
  300. theorem OAI.CycleClique.certificate_86_part_17_checked line 578
  301. def OAI.CycleClique.certificate_86_part_16 line 580
  302. theorem OAI.CycleClique.certificate_86_part_16_checked line 582
  303. def OAI.CycleClique.certificate_86_part_19_E line 584
  304. def OAI.CycleClique.certificate_86_part_19_M line 586
  305. def OAI.CycleClique.certificate_86_part_20_E line 588
  306. def OAI.CycleClique.certificate_86_part_20_M line 590
  307. def OAI.CycleClique.certificate_86_part_21_E line 592
  308. def OAI.CycleClique.certificate_86_part_21_M line 594
  309. def OAI.CycleClique.certificate_86_part_21 line 596
  310. theorem OAI.CycleClique.certificate_86_part_21_checked line 598
  311. def OAI.CycleClique.certificate_86_part_20 line 600
  312. theorem OAI.CycleClique.certificate_86_part_20_checked line 602
  313. def OAI.CycleClique.certificate_86_part_19 line 604
  314. theorem OAI.CycleClique.certificate_86_part_19_checked line 606
  315. def OAI.CycleClique.certificate_86_part_22_E line 608
  316. def OAI.CycleClique.certificate_86_part_22_M line 610
  317. def OAI.CycleClique.certificate_86_part_23_E line 612
  318. def OAI.CycleClique.certificate_86_part_23_M line 614
  319. def OAI.CycleClique.certificate_86_part_24_E line 616
  320. def OAI.CycleClique.certificate_86_part_24_M line 618
  321. def OAI.CycleClique.certificate_86_part_25_E line 620
  322. def OAI.CycleClique.certificate_86_part_25_M line 622
  323. def OAI.CycleClique.certificate_86_part_25 line 624
  324. theorem OAI.CycleClique.certificate_86_part_25_checked line 626
  325. def OAI.CycleClique.certificate_86_part_24 line 628
  326. theorem OAI.CycleClique.certificate_86_part_24_checked line 630
  327. def OAI.CycleClique.certificate_86_part_23 line 632
  328. theorem OAI.CycleClique.certificate_86_part_23_checked line 634
  329. def OAI.CycleClique.certificate_86_part_26_E line 636
  330. def OAI.CycleClique.certificate_86_part_26_M line 638
  331. def OAI.CycleClique.certificate_86_part_27_E line 640
  332. def OAI.CycleClique.certificate_86_part_27_M line 642
  333. def OAI.CycleClique.certificate_86_part_27 line 644
  334. theorem OAI.CycleClique.certificate_86_part_27_checked line 646
  335. def OAI.CycleClique.certificate_86_part_28_E line 648
  336. def OAI.CycleClique.certificate_86_part_28_M line 650
  337. def OAI.CycleClique.certificate_86_part_28 line 652
  338. theorem OAI.CycleClique.certificate_86_part_28_checked line 654
  339. def OAI.CycleClique.certificate_86_part_29_E line 656
  340. def OAI.CycleClique.certificate_86_part_29_M line 658
  341. def OAI.CycleClique.certificate_86_part_30_E line 660
  342. def OAI.CycleClique.certificate_86_part_30_M line 662
  343. def OAI.CycleClique.certificate_86_part_31_E line 664
  344. def OAI.CycleClique.certificate_86_part_31_M line 666
  345. def OAI.CycleClique.certificate_86_part_32_E line 668
  346. def OAI.CycleClique.certificate_86_part_32_M line 670
  347. def OAI.CycleClique.certificate_86_part_32 line 672
  348. theorem OAI.CycleClique.certificate_86_part_32_checked line 674
  349. def OAI.CycleClique.certificate_86_part_31 line 676
  350. theorem OAI.CycleClique.certificate_86_part_31_checked line 678
  351. def OAI.CycleClique.certificate_86_part_30 line 680
  352. theorem OAI.CycleClique.certificate_86_part_30_checked line 682
  353. def OAI.CycleClique.certificate_86_part_33_E line 684
  354. def OAI.CycleClique.certificate_86_part_33_M line 686
  355. def OAI.CycleClique.certificate_86_part_33 line 688
  356. theorem OAI.CycleClique.certificate_86_part_33_checked line 690
  357. def OAI.CycleClique.certificate_86_part_34_E line 692
  358. def OAI.CycleClique.certificate_86_part_34_M line 694
  359. def OAI.CycleClique.certificate_86_part_35_E line 696
  360. def OAI.CycleClique.certificate_86_part_35_M line 698
  361. def OAI.CycleClique.certificate_86_part_36_E line 700
  362. def OAI.CycleClique.certificate_86_part_36_M line 702
  363. def OAI.CycleClique.certificate_86_part_36 line 704
  364. theorem OAI.CycleClique.certificate_86_part_36_checked line 706
  365. def OAI.CycleClique.certificate_86_part_35 line 708
  366. theorem OAI.CycleClique.certificate_86_part_35_checked line 710
  367. def OAI.CycleClique.certificate_86_part_37_E line 712
  368. def OAI.CycleClique.certificate_86_part_37_M line 714
  369. def OAI.CycleClique.certificate_86_part_37 line 716
  370. theorem OAI.CycleClique.certificate_86_part_37_checked line 718
  371. def OAI.CycleClique.certificate_86_part_38_E line 720
  372. def OAI.CycleClique.certificate_86_part_38_M line 722
  373. def OAI.CycleClique.certificate_86_part_39_E line 724
  374. def OAI.CycleClique.certificate_86_part_39_M line 726
  375. def OAI.CycleClique.certificate_86_part_39 line 728
  376. theorem OAI.CycleClique.certificate_86_part_39_checked line 730
  377. def OAI.CycleClique.certificate_86_part_40_E line 732
  378. def OAI.CycleClique.certificate_86_part_40_M line 734
  379. def OAI.CycleClique.certificate_86_part_40 line 736
  380. theorem OAI.CycleClique.certificate_86_part_40_checked line 738
  381. def OAI.CycleClique.certificate_86_part_41_E line 740
  382. def OAI.CycleClique.certificate_86_part_41_M line 742
  383. def OAI.CycleClique.certificate_86_part_42_E line 744
  384. def OAI.CycleClique.certificate_86_part_42_M line 746
  385. def OAI.CycleClique.certificate_86_part_42 line 748
  386. theorem OAI.CycleClique.certificate_86_part_42_checked line 750
  387. def OAI.CycleClique.certificate_86_part_43_E line 752
  388. def OAI.CycleClique.certificate_86_part_43_M line 754
  389. def OAI.CycleClique.certificate_86_part_43 line 756
  390. theorem OAI.CycleClique.certificate_86_part_43_checked line 758
  391. def OAI.CycleClique.certificate_86_part_44_E line 760
  392. def OAI.CycleClique.certificate_86_part_44_M line 762
  393. def OAI.CycleClique.certificate_86_part_45_E line 764
  394. def OAI.CycleClique.certificate_86_part_45_M line 766
  395. def OAI.CycleClique.certificate_86_part_46_E line 768
  396. def OAI.CycleClique.certificate_86_part_46_M line 770
  397. def OAI.CycleClique.certificate_86_part_46 line 772
  398. theorem OAI.CycleClique.certificate_86_part_46_checked line 774
  399. def OAI.CycleClique.certificate_86_part_45 line 776
  400. theorem OAI.CycleClique.certificate_86_part_45_checked line 778
  401. def OAI.CycleClique.certificate_86_part_47_E line 780
  402. def OAI.CycleClique.certificate_86_part_47_M line 782
  403. def OAI.CycleClique.certificate_86_part_47 line 784
  404. theorem OAI.CycleClique.certificate_86_part_47_checked line 786
  405. def OAI.CycleClique.certificate_86_part_48_E line 788
  406. def OAI.CycleClique.certificate_86_part_48_M line 790
  407. def OAI.CycleClique.certificate_86_part_48 line 792
  408. theorem OAI.CycleClique.certificate_86_part_48_checked line 794
  409. def OAI.CycleClique.certificate_86_part_49_E line 796
  410. def OAI.CycleClique.certificate_86_part_49_M line 798
  411. def OAI.CycleClique.certificate_86_part_49 line 800
  412. theorem OAI.CycleClique.certificate_86_part_49_checked line 802
  413. def OAI.CycleClique.certificate_86_part_44 line 804
  414. theorem OAI.CycleClique.certificate_86_part_44_checked line 806
  415. def OAI.CycleClique.certificate_86_part_41 line 808
  416. theorem OAI.CycleClique.certificate_86_part_41_checked line 810
  417. def OAI.CycleClique.certificate_86_part_38 line 812
  418. theorem OAI.CycleClique.certificate_86_part_38_checked line 814
  419. def OAI.CycleClique.certificate_86_part_34 line 816
  420. theorem OAI.CycleClique.certificate_86_part_34_checked line 818
  421. def OAI.CycleClique.certificate_86_part_29 line 820
  422. theorem OAI.CycleClique.certificate_86_part_29_checked line 822
  423. def OAI.CycleClique.certificate_86_part_26 line 824
  424. theorem OAI.CycleClique.certificate_86_part_26_checked line 826
  425. def OAI.CycleClique.certificate_86_part_22 line 828
  426. theorem OAI.CycleClique.certificate_86_part_22_checked line 830
  427. def OAI.CycleClique.certificate_86_part_15 line 832
  428. theorem OAI.CycleClique.certificate_86_part_15_checked line 834
  429. def OAI.CycleClique.certificate_86_part_14 line 836
  430. theorem OAI.CycleClique.certificate_86_part_14_checked line 838
  431. def OAI.CycleClique.certificate_86_part_9 line 840
  432. theorem OAI.CycleClique.certificate_86_part_9_checked line 842
  433. def OAI.CycleClique.certificate_86_part_7 line 844
  434. theorem OAI.CycleClique.certificate_86_part_7_checked line 846
  435. def OAI.CycleClique.certificate_86_part_2 line 848
  436. theorem OAI.CycleClique.certificate_86_part_2_checked line 850
  437. def OAI.CycleClique.certificate_86_part_1 line 852
  438. theorem OAI.CycleClique.certificate_86_part_1_checked line 854
  439. def OAI.CycleClique.certificate_86 line 856
  440. theorem OAI.CycleClique.certificate_86_checked line 858
  441. theorem OAI.CycleClique.certificate_86_valid line 860
  442. def OAI.CycleClique.certificate_87_q line 862
  443. def OAI.CycleClique.certificate_87_edges line 863
  444. def OAI.CycleClique.certificate_87_part_0 line 865
  445. def OAI.CycleClique.certificate_87 line 867
  446. theorem OAI.CycleClique.certificate_87_checked line 869
  447. theorem OAI.CycleClique.certificate_87_valid line 870
  448. def OAI.CycleClique.certificate_88_q line 872
  449. def OAI.CycleClique.certificate_88_edges line 873
  450. def OAI.CycleClique.certificate_88_part_0 line 875
  451. def OAI.CycleClique.certificate_88 line 877
  452. theorem OAI.CycleClique.certificate_88_checked line 879
  453. theorem OAI.CycleClique.certificate_88_valid line 880
  454. def OAI.CycleClique.certificate_89_q line 882
  455. def OAI.CycleClique.certificate_89_edges line 883
  456. def OAI.CycleClique.certificate_89_part_0 line 885
  457. def OAI.CycleClique.certificate_89 line 887
  458. theorem OAI.CycleClique.certificate_89_checked line 889
  459. theorem OAI.CycleClique.certificate_89_valid line 890
  460. def OAI.CycleClique.certificate_90_q line 892
  461. def OAI.CycleClique.certificate_90_edges line 894
  462. def OAI.CycleClique.certificate_90_E line 896
  463. def OAI.CycleClique.certificate_90_M line 898
  464. def OAI.CycleClique.certificate_90_part_1_E line 900
  465. def OAI.CycleClique.certificate_90_part_1_M line 902
  466. def OAI.CycleClique.certificate_90_part_2_E line 904
  467. def OAI.CycleClique.certificate_90_part_2_M line 906
  468. def OAI.CycleClique.certificate_90_part_3_E line 908
  469. def OAI.CycleClique.certificate_90_part_3_M line 910
  470. def OAI.CycleClique.certificate_90_part_4_E line 912
  471. def OAI.CycleClique.certificate_90_part_4_M line 914
  472. def OAI.CycleClique.certificate_90_part_5_E line 916
  473. def OAI.CycleClique.certificate_90_part_5_M line 918
  474. def OAI.CycleClique.certificate_90_part_5 line 920
  475. theorem OAI.CycleClique.certificate_90_part_5_checked line 922
  476. def OAI.CycleClique.certificate_90_part_6_E line 924
  477. def OAI.CycleClique.certificate_90_part_6_M line 926
  478. def OAI.CycleClique.certificate_90_part_7_E line 928
  479. def OAI.CycleClique.certificate_90_part_7_M line 930
  480. def OAI.CycleClique.certificate_90_part_8_E line 932
  481. def OAI.CycleClique.certificate_90_part_8_M line 934
  482. def OAI.CycleClique.certificate_90_part_8 line 936
  483. theorem OAI.CycleClique.certificate_90_part_8_checked line 938
  484. def OAI.CycleClique.certificate_90_part_7 line 940
  485. theorem OAI.CycleClique.certificate_90_part_7_checked line 942
  486. def OAI.CycleClique.certificate_90_part_6 line 944
  487. theorem OAI.CycleClique.certificate_90_part_6_checked line 946
  488. def OAI.CycleClique.certificate_90_part_9_E line 948
  489. def OAI.CycleClique.certificate_90_part_9_M line 950
  490. def OAI.CycleClique.certificate_90_part_10_E line 952
  491. def OAI.CycleClique.certificate_90_part_10_M line 954
  492. def OAI.CycleClique.certificate_90_part_11_E line 956
  493. def OAI.CycleClique.certificate_90_part_11_M line 958
  494. def OAI.CycleClique.certificate_90_part_11 line 960
  495. theorem OAI.CycleClique.certificate_90_part_11_checked line 962
  496. def OAI.CycleClique.certificate_90_part_10 line 964
  497. theorem OAI.CycleClique.certificate_90_part_10_checked line 966
  498. def OAI.CycleClique.certificate_90_part_12_E line 968
  499. def OAI.CycleClique.certificate_90_part_12_M line 970
  500. def OAI.CycleClique.certificate_90_part_13_E line 972
  501. def OAI.CycleClique.certificate_90_part_13_M line 974
  502. def OAI.CycleClique.certificate_90_part_13 line 976
  503. theorem OAI.CycleClique.certificate_90_part_13_checked line 978
  504. def OAI.CycleClique.certificate_90_part_14_E line 980
  505. def OAI.CycleClique.certificate_90_part_14_M line 982
  506. def OAI.CycleClique.certificate_90_part_14 line 984
  507. theorem OAI.CycleClique.certificate_90_part_14_checked line 986
  508. def OAI.CycleClique.certificate_90_part_15_E line 988
  509. def OAI.CycleClique.certificate_90_part_15_M line 990
  510. def OAI.CycleClique.certificate_90_part_15 line 992
  511. theorem OAI.CycleClique.certificate_90_part_15_checked line 994
  512. def OAI.CycleClique.certificate_90_part_16_E line 996
  513. def OAI.CycleClique.certificate_90_part_16_M line 998
  514. def OAI.CycleClique.certificate_90_part_17_E line 1000
  515. def OAI.CycleClique.certificate_90_part_17_M line 1002
  516. def OAI.CycleClique.certificate_90_part_18_E line 1004
  517. def OAI.CycleClique.certificate_90_part_18_M line 1006
  518. def OAI.CycleClique.certificate_90_part_18 line 1008
  519. theorem OAI.CycleClique.certificate_90_part_18_checked line 1010
  520. def OAI.CycleClique.certificate_90_part_19_E line 1012
  521. def OAI.CycleClique.certificate_90_part_19_M line 1014
  522. def OAI.CycleClique.certificate_90_part_19 line 1016
  523. theorem OAI.CycleClique.certificate_90_part_19_checked line 1018
  524. def OAI.CycleClique.certificate_90_part_20_E line 1020
  525. def OAI.CycleClique.certificate_90_part_20_M line 1022
  526. def OAI.CycleClique.certificate_90_part_21_E line 1024
  527. def OAI.CycleClique.certificate_90_part_21_M line 1026
  528. def OAI.CycleClique.certificate_90_part_22_E line 1028
  529. def OAI.CycleClique.certificate_90_part_22_M line 1030
  530. def OAI.CycleClique.certificate_90_part_23_E line 1032
  531. def OAI.CycleClique.certificate_90_part_23_M line 1034
  532. def OAI.CycleClique.certificate_90_part_23 line 1036
  533. theorem OAI.CycleClique.certificate_90_part_23_checked line 1038
  534. def OAI.CycleClique.certificate_90_part_22 line 1040
  535. theorem OAI.CycleClique.certificate_90_part_22_checked line 1042
  536. def OAI.CycleClique.certificate_90_part_24_E line 1044
  537. def OAI.CycleClique.certificate_90_part_24_M line 1046
  538. def OAI.CycleClique.certificate_90_part_24 line 1048
  539. theorem OAI.CycleClique.certificate_90_part_24_checked line 1050
  540. def OAI.CycleClique.certificate_90_part_25_E line 1052
  541. def OAI.CycleClique.certificate_90_part_25_M line 1054
  542. def OAI.CycleClique.certificate_90_part_25 line 1056
  543. theorem OAI.CycleClique.certificate_90_part_25_checked line 1058
  544. def OAI.CycleClique.certificate_90_part_21 line 1060
  545. theorem OAI.CycleClique.certificate_90_part_21_checked line 1062
  546. def OAI.CycleClique.certificate_90_part_20 line 1064
  547. theorem OAI.CycleClique.certificate_90_part_20_checked line 1066
  548. def OAI.CycleClique.certificate_90_part_17 line 1068
  549. theorem OAI.CycleClique.certificate_90_part_17_checked line 1070
  550. def OAI.CycleClique.certificate_90_part_16 line 1072
  551. theorem OAI.CycleClique.certificate_90_part_16_checked line 1074
  552. def OAI.CycleClique.certificate_90_part_12 line 1076
  553. theorem OAI.CycleClique.certificate_90_part_12_checked line 1078
  554. def OAI.CycleClique.certificate_90_part_9 line 1080
  555. theorem OAI.CycleClique.certificate_90_part_9_checked line 1082
  556. def OAI.CycleClique.certificate_90_part_4 line 1084
  557. theorem OAI.CycleClique.certificate_90_part_4_checked line 1086
  558. def OAI.CycleClique.certificate_90_part_3 line 1088
  559. theorem OAI.CycleClique.certificate_90_part_3_checked line 1090
  560. def OAI.CycleClique.certificate_90_part_2 line 1092
  561. theorem OAI.CycleClique.certificate_90_part_2_checked line 1094
  562. def OAI.CycleClique.certificate_90_part_1 line 1096
  563. theorem OAI.CycleClique.certificate_90_part_1_checked line 1098
  564. def OAI.CycleClique.certificate_90 line 1100
  565. theorem OAI.CycleClique.certificate_90_checked line 1102
  566. theorem OAI.CycleClique.certificate_90_valid line 1104
  567. def OAI.CycleClique.certificate_91_q line 1106
  568. def OAI.CycleClique.certificate_91_edges line 1107
  569. def OAI.CycleClique.certificate_91_part_0 line 1109
  570. def OAI.CycleClique.certificate_91 line 1111
  571. theorem OAI.CycleClique.certificate_91_checked line 1113
  572. theorem OAI.CycleClique.certificate_91_valid line 1114
  573. def OAI.CycleClique.certificate_92_q line 1116
  574. def OAI.CycleClique.certificate_92_edges line 1117
  575. def OAI.CycleClique.certificate_92_part_0 line 1119
  576. def OAI.CycleClique.certificate_92 line 1121
  577. theorem OAI.CycleClique.certificate_92_checked line 1123
  578. theorem OAI.CycleClique.certificate_92_valid line 1124
  579. def OAI.CycleClique.certificate_93_q line 1126
  580. def OAI.CycleClique.certificate_93_edges line 1127
  581. def OAI.CycleClique.certificate_93_part_0 line 1129
  582. def OAI.CycleClique.certificate_93 line 1131
  583. theorem OAI.CycleClique.certificate_93_checked line 1133
  584. theorem OAI.CycleClique.certificate_93_valid line 1134
  585. def OAI.CycleClique.certificate_94_q line 1136
  586. def OAI.CycleClique.certificate_94_edges line 1137
  587. def OAI.CycleClique.certificate_94_part_0 line 1139
  588. def OAI.CycleClique.certificate_94 line 1141
  589. theorem OAI.CycleClique.certificate_94_checked line 1143
  590. theorem OAI.CycleClique.certificate_94_valid line 1144
  591. def OAI.CycleClique.certificate_95_q line 1146
  592. def OAI.CycleClique.certificate_95_edges line 1147
  593. def OAI.CycleClique.certificate_95_part_0 line 1149
  594. def OAI.CycleClique.certificate_95 line 1151
  595. theorem OAI.CycleClique.certificate_95_checked line 1153
  596. theorem OAI.CycleClique.certificate_95_valid line 1154