OAI/Combinatorics/Ramsey/CycleClique/Certificates005.lean

GitHub source file

603 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.certificate_128_q line 20
  2. def OAI.CycleClique.certificate_128_edges line 21
  3. def OAI.CycleClique.certificate_128_part_0 line 23
  4. def OAI.CycleClique.certificate_128_part_1 line 25
  5. def OAI.CycleClique.certificate_128 line 27
  6. theorem OAI.CycleClique.certificate_128_checked line 29
  7. theorem OAI.CycleClique.certificate_128_valid line 30
  8. def OAI.CycleClique.certificate_129_q line 32
  9. def OAI.CycleClique.certificate_129_edges line 33
  10. def OAI.CycleClique.certificate_129_part_0 line 35
  11. def OAI.CycleClique.certificate_129_part_1 line 37
  12. def OAI.CycleClique.certificate_129 line 39
  13. theorem OAI.CycleClique.certificate_129_checked line 41
  14. theorem OAI.CycleClique.certificate_129_valid line 42
  15. def OAI.CycleClique.certificate_130_q line 44
  16. def OAI.CycleClique.certificate_130_edges line 45
  17. def OAI.CycleClique.certificate_130_part_0 line 47
  18. def OAI.CycleClique.certificate_130_part_1 line 49
  19. def OAI.CycleClique.certificate_130 line 51
  20. theorem OAI.CycleClique.certificate_130_checked line 53
  21. theorem OAI.CycleClique.certificate_130_valid line 54
  22. def OAI.CycleClique.certificate_131_q line 56
  23. def OAI.CycleClique.certificate_131_edges line 57
  24. def OAI.CycleClique.certificate_131_part_0 line 59
  25. def OAI.CycleClique.certificate_131_part_1 line 61
  26. def OAI.CycleClique.certificate_131 line 63
  27. theorem OAI.CycleClique.certificate_131_checked line 65
  28. theorem OAI.CycleClique.certificate_131_valid line 66
  29. def OAI.CycleClique.certificate_132_q line 68
  30. def OAI.CycleClique.certificate_132_edges line 69
  31. def OAI.CycleClique.certificate_132_part_0 line 71
  32. def OAI.CycleClique.certificate_132_part_1 line 73
  33. def OAI.CycleClique.certificate_132 line 75
  34. theorem OAI.CycleClique.certificate_132_checked line 77
  35. theorem OAI.CycleClique.certificate_132_valid line 78
  36. def OAI.CycleClique.certificate_133_q line 80
  37. def OAI.CycleClique.certificate_133_edges line 81
  38. def OAI.CycleClique.certificate_133_part_0 line 83
  39. def OAI.CycleClique.certificate_133_part_1 line 85
  40. def OAI.CycleClique.certificate_133 line 87
  41. theorem OAI.CycleClique.certificate_133_checked line 89
  42. theorem OAI.CycleClique.certificate_133_valid line 90
  43. def OAI.CycleClique.certificate_134_q line 92
  44. def OAI.CycleClique.certificate_134_edges line 93
  45. def OAI.CycleClique.certificate_134_part_0 line 95
  46. def OAI.CycleClique.certificate_134_part_1 line 97
  47. def OAI.CycleClique.certificate_134 line 99
  48. theorem OAI.CycleClique.certificate_134_checked line 101
  49. theorem OAI.CycleClique.certificate_134_valid line 102
  50. def OAI.CycleClique.certificate_135_q line 104
  51. def OAI.CycleClique.certificate_135_edges line 105
  52. def OAI.CycleClique.certificate_135_part_0 line 107
  53. def OAI.CycleClique.certificate_135_part_1 line 109
  54. def OAI.CycleClique.certificate_135 line 111
  55. theorem OAI.CycleClique.certificate_135_checked line 113
  56. theorem OAI.CycleClique.certificate_135_valid line 114
  57. def OAI.CycleClique.certificate_136_q line 116
  58. def OAI.CycleClique.certificate_136_edges line 117
  59. def OAI.CycleClique.certificate_136_part_0 line 119
  60. def OAI.CycleClique.certificate_136_part_1 line 121
  61. def OAI.CycleClique.certificate_136 line 123
  62. theorem OAI.CycleClique.certificate_136_checked line 125
  63. theorem OAI.CycleClique.certificate_136_valid line 126
  64. def OAI.CycleClique.certificate_137_q line 128
  65. def OAI.CycleClique.certificate_137_edges line 129
  66. def OAI.CycleClique.certificate_137_part_0 line 131
  67. def OAI.CycleClique.certificate_137_part_1 line 133
  68. def OAI.CycleClique.certificate_137 line 135
  69. theorem OAI.CycleClique.certificate_137_checked line 137
  70. theorem OAI.CycleClique.certificate_137_valid line 138
  71. def OAI.CycleClique.certificate_138_q line 140
  72. def OAI.CycleClique.certificate_138_edges line 141
  73. def OAI.CycleClique.certificate_138_part_0 line 143
  74. def OAI.CycleClique.certificate_138_part_1 line 145
  75. def OAI.CycleClique.certificate_138 line 147
  76. theorem OAI.CycleClique.certificate_138_checked line 149
  77. theorem OAI.CycleClique.certificate_138_valid line 150
  78. def OAI.CycleClique.certificate_139_q line 152
  79. def OAI.CycleClique.certificate_139_edges line 153
  80. def OAI.CycleClique.certificate_139_part_0 line 155
  81. def OAI.CycleClique.certificate_139_part_1 line 157
  82. def OAI.CycleClique.certificate_139 line 159
  83. theorem OAI.CycleClique.certificate_139_checked line 161
  84. theorem OAI.CycleClique.certificate_139_valid line 162
  85. def OAI.CycleClique.certificate_140_q line 164
  86. def OAI.CycleClique.certificate_140_edges line 165
  87. def OAI.CycleClique.certificate_140_part_0 line 167
  88. def OAI.CycleClique.certificate_140_part_1 line 169
  89. def OAI.CycleClique.certificate_140 line 171
  90. theorem OAI.CycleClique.certificate_140_checked line 173
  91. theorem OAI.CycleClique.certificate_140_valid line 174
  92. def OAI.CycleClique.certificate_141_q line 176
  93. def OAI.CycleClique.certificate_141_edges line 177
  94. def OAI.CycleClique.certificate_141_part_0 line 179
  95. def OAI.CycleClique.certificate_141_part_1 line 181
  96. def OAI.CycleClique.certificate_141 line 183
  97. theorem OAI.CycleClique.certificate_141_checked line 185
  98. theorem OAI.CycleClique.certificate_141_valid line 186
  99. def OAI.CycleClique.certificate_142_q line 188
  100. def OAI.CycleClique.certificate_142_edges line 189
  101. def OAI.CycleClique.certificate_142_part_0 line 191
  102. def OAI.CycleClique.certificate_142_part_1 line 193
  103. def OAI.CycleClique.certificate_142_part_2 line 195
  104. def OAI.CycleClique.certificate_142 line 197
  105. theorem OAI.CycleClique.certificate_142_checked line 199
  106. theorem OAI.CycleClique.certificate_142_valid line 200
  107. def OAI.CycleClique.certificate_143_q line 202
  108. def OAI.CycleClique.certificate_143_edges line 203
  109. def OAI.CycleClique.certificate_143_part_0 line 205
  110. def OAI.CycleClique.certificate_143_part_1 line 207
  111. def OAI.CycleClique.certificate_143_part_2 line 209
  112. def OAI.CycleClique.certificate_143 line 211
  113. theorem OAI.CycleClique.certificate_143_checked line 213
  114. theorem OAI.CycleClique.certificate_143_valid line 214
  115. def OAI.CycleClique.certificate_144_q line 216
  116. def OAI.CycleClique.certificate_144_edges line 217
  117. def OAI.CycleClique.certificate_144_part_0 line 219
  118. def OAI.CycleClique.certificate_144 line 221
  119. theorem OAI.CycleClique.certificate_144_checked line 223
  120. theorem OAI.CycleClique.certificate_144_valid line 224
  121. def OAI.CycleClique.certificate_145_q line 226
  122. def OAI.CycleClique.certificate_145_edges line 227
  123. def OAI.CycleClique.certificate_145_part_0 line 229
  124. def OAI.CycleClique.certificate_145 line 231
  125. theorem OAI.CycleClique.certificate_145_checked line 233
  126. theorem OAI.CycleClique.certificate_145_valid line 234
  127. def OAI.CycleClique.certificate_146_q line 236
  128. def OAI.CycleClique.certificate_146_edges line 237
  129. def OAI.CycleClique.certificate_146_part_0 line 239
  130. def OAI.CycleClique.certificate_146 line 241
  131. theorem OAI.CycleClique.certificate_146_checked line 243
  132. theorem OAI.CycleClique.certificate_146_valid line 244
  133. def OAI.CycleClique.certificate_147_q line 246
  134. def OAI.CycleClique.certificate_147_edges line 247
  135. def OAI.CycleClique.certificate_147_part_0 line 249
  136. def OAI.CycleClique.certificate_147 line 251
  137. theorem OAI.CycleClique.certificate_147_checked line 253
  138. theorem OAI.CycleClique.certificate_147_valid line 254
  139. def OAI.CycleClique.certificate_148_q line 256
  140. def OAI.CycleClique.certificate_148_edges line 258
  141. def OAI.CycleClique.certificate_148_E line 260
  142. def OAI.CycleClique.certificate_148_M line 262
  143. def OAI.CycleClique.certificate_148_part_1_E line 264
  144. def OAI.CycleClique.certificate_148_part_1_M line 266
  145. def OAI.CycleClique.certificate_148_part_2_E line 268
  146. def OAI.CycleClique.certificate_148_part_2_M line 270
  147. def OAI.CycleClique.certificate_148_part_3_E line 272
  148. def OAI.CycleClique.certificate_148_part_3_M line 274
  149. def OAI.CycleClique.certificate_148_part_4_E line 276
  150. def OAI.CycleClique.certificate_148_part_4_M line 278
  151. def OAI.CycleClique.certificate_148_part_5_E line 280
  152. def OAI.CycleClique.certificate_148_part_5_M line 282
  153. def OAI.CycleClique.certificate_148_part_5 line 284
  154. theorem OAI.CycleClique.certificate_148_part_5_checked line 286
  155. def OAI.CycleClique.certificate_148_part_6_E line 288
  156. def OAI.CycleClique.certificate_148_part_6_M line 290
  157. def OAI.CycleClique.certificate_148_part_7_E line 292
  158. def OAI.CycleClique.certificate_148_part_7_M line 294
  159. def OAI.CycleClique.certificate_148_part_8_E line 296
  160. def OAI.CycleClique.certificate_148_part_8_M line 298
  161. def OAI.CycleClique.certificate_148_part_8 line 300
  162. theorem OAI.CycleClique.certificate_148_part_8_checked line 302
  163. def OAI.CycleClique.certificate_148_part_9_E line 304
  164. def OAI.CycleClique.certificate_148_part_9_M line 306
  165. def OAI.CycleClique.certificate_148_part_9 line 308
  166. theorem OAI.CycleClique.certificate_148_part_9_checked line 310
  167. def OAI.CycleClique.certificate_148_part_10_E line 312
  168. def OAI.CycleClique.certificate_148_part_10_M line 314
  169. def OAI.CycleClique.certificate_148_part_10 line 316
  170. theorem OAI.CycleClique.certificate_148_part_10_checked line 318
  171. def OAI.CycleClique.certificate_148_part_11_E line 320
  172. def OAI.CycleClique.certificate_148_part_11_M line 322
  173. def OAI.CycleClique.certificate_148_part_12_E line 324
  174. def OAI.CycleClique.certificate_148_part_12_M line 326
  175. def OAI.CycleClique.certificate_148_part_12 line 328
  176. theorem OAI.CycleClique.certificate_148_part_12_checked line 330
  177. def OAI.CycleClique.certificate_148_part_11 line 332
  178. theorem OAI.CycleClique.certificate_148_part_11_checked line 334
  179. def OAI.CycleClique.certificate_148_part_7 line 336
  180. theorem OAI.CycleClique.certificate_148_part_7_checked line 338
  181. def OAI.CycleClique.certificate_148_part_6 line 340
  182. theorem OAI.CycleClique.certificate_148_part_6_checked line 342
  183. def OAI.CycleClique.certificate_148_part_4 line 344
  184. theorem OAI.CycleClique.certificate_148_part_4_checked line 346
  185. def OAI.CycleClique.certificate_148_part_3 line 348
  186. theorem OAI.CycleClique.certificate_148_part_3_checked line 350
  187. def OAI.CycleClique.certificate_148_part_2 line 352
  188. theorem OAI.CycleClique.certificate_148_part_2_checked line 354
  189. def OAI.CycleClique.certificate_148_part_1 line 356
  190. theorem OAI.CycleClique.certificate_148_part_1_checked line 358
  191. def OAI.CycleClique.certificate_148 line 360
  192. theorem OAI.CycleClique.certificate_148_checked line 362
  193. theorem OAI.CycleClique.certificate_148_valid line 364
  194. def OAI.CycleClique.certificate_149_q line 366
  195. def OAI.CycleClique.certificate_149_edges line 368
  196. def OAI.CycleClique.certificate_149_E line 370
  197. def OAI.CycleClique.certificate_149_M line 372
  198. def OAI.CycleClique.certificate_149_part_1_E line 374
  199. def OAI.CycleClique.certificate_149_part_1_M line 376
  200. def OAI.CycleClique.certificate_149_part_2_E line 378
  201. def OAI.CycleClique.certificate_149_part_2_M line 380
  202. def OAI.CycleClique.certificate_149_part_3_E line 382
  203. def OAI.CycleClique.certificate_149_part_3_M line 384
  204. def OAI.CycleClique.certificate_149_part_4_E line 386
  205. def OAI.CycleClique.certificate_149_part_4_M line 388
  206. def OAI.CycleClique.certificate_149_part_5_E line 390
  207. def OAI.CycleClique.certificate_149_part_5_M line 392
  208. def OAI.CycleClique.certificate_149_part_5 line 394
  209. theorem OAI.CycleClique.certificate_149_part_5_checked line 396
  210. def OAI.CycleClique.certificate_149_part_6_E line 398
  211. def OAI.CycleClique.certificate_149_part_6_M line 400
  212. def OAI.CycleClique.certificate_149_part_7_E line 402
  213. def OAI.CycleClique.certificate_149_part_7_M line 404
  214. def OAI.CycleClique.certificate_149_part_8_E line 406
  215. def OAI.CycleClique.certificate_149_part_8_M line 408
  216. def OAI.CycleClique.certificate_149_part_9_E line 410
  217. def OAI.CycleClique.certificate_149_part_9_M line 412
  218. def OAI.CycleClique.certificate_149_part_9 line 414
  219. theorem OAI.CycleClique.certificate_149_part_9_checked line 416
  220. def OAI.CycleClique.certificate_149_part_8 line 418
  221. theorem OAI.CycleClique.certificate_149_part_8_checked line 420
  222. def OAI.CycleClique.certificate_149_part_10_E line 422
  223. def OAI.CycleClique.certificate_149_part_10_M line 424
  224. def OAI.CycleClique.certificate_149_part_11_E line 426
  225. def OAI.CycleClique.certificate_149_part_11_M line 428
  226. def OAI.CycleClique.certificate_149_part_12_E line 430
  227. def OAI.CycleClique.certificate_149_part_12_M line 432
  228. def OAI.CycleClique.certificate_149_part_12 line 434
  229. theorem OAI.CycleClique.certificate_149_part_12_checked line 436
  230. def OAI.CycleClique.certificate_149_part_11 line 438
  231. theorem OAI.CycleClique.certificate_149_part_11_checked line 440
  232. def OAI.CycleClique.certificate_149_part_13_E line 442
  233. def OAI.CycleClique.certificate_149_part_13_M line 444
  234. def OAI.CycleClique.certificate_149_part_14_E line 446
  235. def OAI.CycleClique.certificate_149_part_14_M line 448
  236. def OAI.CycleClique.certificate_149_part_15_E line 450
  237. def OAI.CycleClique.certificate_149_part_15_M line 452
  238. def OAI.CycleClique.certificate_149_part_16_E line 454
  239. def OAI.CycleClique.certificate_149_part_16_M line 456
  240. def OAI.CycleClique.certificate_149_part_16 line 458
  241. theorem OAI.CycleClique.certificate_149_part_16_checked line 460
  242. def OAI.CycleClique.certificate_149_part_15 line 462
  243. theorem OAI.CycleClique.certificate_149_part_15_checked line 464
  244. def OAI.CycleClique.certificate_149_part_17_E line 466
  245. def OAI.CycleClique.certificate_149_part_17_M line 468
  246. def OAI.CycleClique.certificate_149_part_18_E line 470
  247. def OAI.CycleClique.certificate_149_part_18_M line 472
  248. def OAI.CycleClique.certificate_149_part_18 line 474
  249. theorem OAI.CycleClique.certificate_149_part_18_checked line 476
  250. def OAI.CycleClique.certificate_149_part_17 line 478
  251. theorem OAI.CycleClique.certificate_149_part_17_checked line 480
  252. def OAI.CycleClique.certificate_149_part_19_E line 482
  253. def OAI.CycleClique.certificate_149_part_19_M line 484
  254. def OAI.CycleClique.certificate_149_part_20_E line 486
  255. def OAI.CycleClique.certificate_149_part_20_M line 488
  256. def OAI.CycleClique.certificate_149_part_20 line 490
  257. theorem OAI.CycleClique.certificate_149_part_20_checked line 492
  258. def OAI.CycleClique.certificate_149_part_19 line 494
  259. theorem OAI.CycleClique.certificate_149_part_19_checked line 496
  260. def OAI.CycleClique.certificate_149_part_21_E line 498
  261. def OAI.CycleClique.certificate_149_part_21_M line 500
  262. def OAI.CycleClique.certificate_149_part_22_E line 502
  263. def OAI.CycleClique.certificate_149_part_22_M line 504
  264. def OAI.CycleClique.certificate_149_part_22 line 506
  265. theorem OAI.CycleClique.certificate_149_part_22_checked line 508
  266. def OAI.CycleClique.certificate_149_part_23_E line 510
  267. def OAI.CycleClique.certificate_149_part_23_M line 512
  268. def OAI.CycleClique.certificate_149_part_23 line 514
  269. theorem OAI.CycleClique.certificate_149_part_23_checked line 516
  270. def OAI.CycleClique.certificate_149_part_24_E line 518
  271. def OAI.CycleClique.certificate_149_part_24_M line 520
  272. def OAI.CycleClique.certificate_149_part_25_E line 522
  273. def OAI.CycleClique.certificate_149_part_25_M line 524
  274. def OAI.CycleClique.certificate_149_part_26_E line 526
  275. def OAI.CycleClique.certificate_149_part_26_M line 528
  276. def OAI.CycleClique.certificate_149_part_27_E line 530
  277. def OAI.CycleClique.certificate_149_part_27_M line 532
  278. def OAI.CycleClique.certificate_149_part_27 line 534
  279. theorem OAI.CycleClique.certificate_149_part_27_checked line 536
  280. def OAI.CycleClique.certificate_149_part_26 line 538
  281. theorem OAI.CycleClique.certificate_149_part_26_checked line 540
  282. def OAI.CycleClique.certificate_149_part_28_E line 542
  283. def OAI.CycleClique.certificate_149_part_28_M line 544
  284. def OAI.CycleClique.certificate_149_part_29_E line 546
  285. def OAI.CycleClique.certificate_149_part_29_M line 548
  286. def OAI.CycleClique.certificate_149_part_30_E line 550
  287. def OAI.CycleClique.certificate_149_part_30_M line 552
  288. def OAI.CycleClique.certificate_149_part_31_E line 554
  289. def OAI.CycleClique.certificate_149_part_31_M line 556
  290. def OAI.CycleClique.certificate_149_part_32_E line 558
  291. def OAI.CycleClique.certificate_149_part_32_M line 560
  292. def OAI.CycleClique.certificate_149_part_32 line 562
  293. theorem OAI.CycleClique.certificate_149_part_32_checked line 564
  294. def OAI.CycleClique.certificate_149_part_31 line 566
  295. theorem OAI.CycleClique.certificate_149_part_31_checked line 568
  296. def OAI.CycleClique.certificate_149_part_30 line 570
  297. theorem OAI.CycleClique.certificate_149_part_30_checked line 572
  298. def OAI.CycleClique.certificate_149_part_33_E line 574
  299. def OAI.CycleClique.certificate_149_part_33_M line 576
  300. def OAI.CycleClique.certificate_149_part_34_E line 578
  301. def OAI.CycleClique.certificate_149_part_34_M line 580
  302. def OAI.CycleClique.certificate_149_part_35_E line 582
  303. def OAI.CycleClique.certificate_149_part_35_M line 584
  304. def OAI.CycleClique.certificate_149_part_35 line 586
  305. theorem OAI.CycleClique.certificate_149_part_35_checked line 588
  306. def OAI.CycleClique.certificate_149_part_36_E line 590
  307. def OAI.CycleClique.certificate_149_part_36_M line 592
  308. def OAI.CycleClique.certificate_149_part_37_E line 594
  309. def OAI.CycleClique.certificate_149_part_37_M line 596
  310. def OAI.CycleClique.certificate_149_part_37 line 598
  311. theorem OAI.CycleClique.certificate_149_part_37_checked line 600
  312. def OAI.CycleClique.certificate_149_part_36 line 602
  313. theorem OAI.CycleClique.certificate_149_part_36_checked line 604
  314. def OAI.CycleClique.certificate_149_part_38_E line 606
  315. def OAI.CycleClique.certificate_149_part_38_M line 608
  316. def OAI.CycleClique.certificate_149_part_39_E line 610
  317. def OAI.CycleClique.certificate_149_part_39_M line 612
  318. def OAI.CycleClique.certificate_149_part_39 line 614
  319. theorem OAI.CycleClique.certificate_149_part_39_checked line 616
  320. def OAI.CycleClique.certificate_149_part_38 line 618
  321. theorem OAI.CycleClique.certificate_149_part_38_checked line 620
  322. def OAI.CycleClique.certificate_149_part_40_E line 622
  323. def OAI.CycleClique.certificate_149_part_40_M line 624
  324. def OAI.CycleClique.certificate_149_part_40 line 626
  325. theorem OAI.CycleClique.certificate_149_part_40_checked line 628
  326. def OAI.CycleClique.certificate_149_part_41_E line 630
  327. def OAI.CycleClique.certificate_149_part_41_M line 632
  328. def OAI.CycleClique.certificate_149_part_42_E line 634
  329. def OAI.CycleClique.certificate_149_part_42_M line 636
  330. def OAI.CycleClique.certificate_149_part_42 line 638
  331. theorem OAI.CycleClique.certificate_149_part_42_checked line 640
  332. def OAI.CycleClique.certificate_149_part_43_E line 642
  333. def OAI.CycleClique.certificate_149_part_43_M line 644
  334. def OAI.CycleClique.certificate_149_part_43 line 646
  335. theorem OAI.CycleClique.certificate_149_part_43_checked line 648
  336. def OAI.CycleClique.certificate_149_part_44_E line 650
  337. def OAI.CycleClique.certificate_149_part_44_M line 652
  338. def OAI.CycleClique.certificate_149_part_44 line 654
  339. theorem OAI.CycleClique.certificate_149_part_44_checked line 656
  340. def OAI.CycleClique.certificate_149_part_45_E line 658
  341. def OAI.CycleClique.certificate_149_part_45_M line 660
  342. def OAI.CycleClique.certificate_149_part_46_E line 662
  343. def OAI.CycleClique.certificate_149_part_46_M line 664
  344. def OAI.CycleClique.certificate_149_part_47_E line 666
  345. def OAI.CycleClique.certificate_149_part_47_M line 668
  346. def OAI.CycleClique.certificate_149_part_47 line 670
  347. theorem OAI.CycleClique.certificate_149_part_47_checked line 672
  348. def OAI.CycleClique.certificate_149_part_46 line 674
  349. theorem OAI.CycleClique.certificate_149_part_46_checked line 676
  350. def OAI.CycleClique.certificate_149_part_45 line 678
  351. theorem OAI.CycleClique.certificate_149_part_45_checked line 680
  352. def OAI.CycleClique.certificate_149_part_48_E line 682
  353. def OAI.CycleClique.certificate_149_part_48_M line 684
  354. def OAI.CycleClique.certificate_149_part_48 line 686
  355. theorem OAI.CycleClique.certificate_149_part_48_checked line 688
  356. def OAI.CycleClique.certificate_149_part_49_E line 690
  357. def OAI.CycleClique.certificate_149_part_49_M line 692
  358. def OAI.CycleClique.certificate_149_part_50_E line 694
  359. def OAI.CycleClique.certificate_149_part_50_M line 696
  360. def OAI.CycleClique.certificate_149_part_51_E line 698
  361. def OAI.CycleClique.certificate_149_part_51_M line 700
  362. def OAI.CycleClique.certificate_149_part_52_E line 702
  363. def OAI.CycleClique.certificate_149_part_52_M line 704
  364. def OAI.CycleClique.certificate_149_part_52 line 706
  365. theorem OAI.CycleClique.certificate_149_part_52_checked line 708
  366. def OAI.CycleClique.certificate_149_part_51 line 710
  367. theorem OAI.CycleClique.certificate_149_part_51_checked line 712
  368. def OAI.CycleClique.certificate_149_part_53_E line 714
  369. def OAI.CycleClique.certificate_149_part_53_M line 716
  370. def OAI.CycleClique.certificate_149_part_54_E line 718
  371. def OAI.CycleClique.certificate_149_part_54_M line 720
  372. def OAI.CycleClique.certificate_149_part_54 line 722
  373. theorem OAI.CycleClique.certificate_149_part_54_checked line 724
  374. def OAI.CycleClique.certificate_149_part_53 line 726
  375. theorem OAI.CycleClique.certificate_149_part_53_checked line 728
  376. def OAI.CycleClique.certificate_149_part_55_E line 730
  377. def OAI.CycleClique.certificate_149_part_55_M line 732
  378. def OAI.CycleClique.certificate_149_part_56_E line 734
  379. def OAI.CycleClique.certificate_149_part_56_M line 736
  380. def OAI.CycleClique.certificate_149_part_57_E line 738
  381. def OAI.CycleClique.certificate_149_part_57_M line 740
  382. def OAI.CycleClique.certificate_149_part_57 line 742
  383. theorem OAI.CycleClique.certificate_149_part_57_checked line 744
  384. def OAI.CycleClique.certificate_149_part_56 line 746
  385. theorem OAI.CycleClique.certificate_149_part_56_checked line 748
  386. def OAI.CycleClique.certificate_149_part_55 line 750
  387. theorem OAI.CycleClique.certificate_149_part_55_checked line 752
  388. def OAI.CycleClique.certificate_149_part_58_E line 754
  389. def OAI.CycleClique.certificate_149_part_58_M line 756
  390. def OAI.CycleClique.certificate_149_part_59_E line 758
  391. def OAI.CycleClique.certificate_149_part_59_M line 760
  392. def OAI.CycleClique.certificate_149_part_60_E line 762
  393. def OAI.CycleClique.certificate_149_part_60_M line 764
  394. def OAI.CycleClique.certificate_149_part_60 line 766
  395. theorem OAI.CycleClique.certificate_149_part_60_checked line 768
  396. def OAI.CycleClique.certificate_149_part_59 line 770
  397. theorem OAI.CycleClique.certificate_149_part_59_checked line 772
  398. def OAI.CycleClique.certificate_149_part_58 line 774
  399. theorem OAI.CycleClique.certificate_149_part_58_checked line 776
  400. def OAI.CycleClique.certificate_149_part_50 line 778
  401. theorem OAI.CycleClique.certificate_149_part_50_checked line 780
  402. def OAI.CycleClique.certificate_149_part_49 line 782
  403. theorem OAI.CycleClique.certificate_149_part_49_checked line 784
  404. def OAI.CycleClique.certificate_149_part_41 line 786
  405. theorem OAI.CycleClique.certificate_149_part_41_checked line 788
  406. def OAI.CycleClique.certificate_149_part_34 line 790
  407. theorem OAI.CycleClique.certificate_149_part_34_checked line 792
  408. def OAI.CycleClique.certificate_149_part_33 line 794
  409. theorem OAI.CycleClique.certificate_149_part_33_checked line 796
  410. def OAI.CycleClique.certificate_149_part_29 line 798
  411. theorem OAI.CycleClique.certificate_149_part_29_checked line 800
  412. def OAI.CycleClique.certificate_149_part_28 line 802
  413. theorem OAI.CycleClique.certificate_149_part_28_checked line 804
  414. def OAI.CycleClique.certificate_149_part_25 line 806
  415. theorem OAI.CycleClique.certificate_149_part_25_checked line 808
  416. def OAI.CycleClique.certificate_149_part_24 line 810
  417. theorem OAI.CycleClique.certificate_149_part_24_checked line 812
  418. def OAI.CycleClique.certificate_149_part_21 line 814
  419. theorem OAI.CycleClique.certificate_149_part_21_checked line 816
  420. def OAI.CycleClique.certificate_149_part_14 line 818
  421. theorem OAI.CycleClique.certificate_149_part_14_checked line 820
  422. def OAI.CycleClique.certificate_149_part_13 line 822
  423. theorem OAI.CycleClique.certificate_149_part_13_checked line 824
  424. def OAI.CycleClique.certificate_149_part_10 line 826
  425. theorem OAI.CycleClique.certificate_149_part_10_checked line 828
  426. def OAI.CycleClique.certificate_149_part_7 line 830
  427. theorem OAI.CycleClique.certificate_149_part_7_checked line 832
  428. def OAI.CycleClique.certificate_149_part_6 line 834
  429. theorem OAI.CycleClique.certificate_149_part_6_checked line 836
  430. def OAI.CycleClique.certificate_149_part_4 line 838
  431. theorem OAI.CycleClique.certificate_149_part_4_checked line 840
  432. def OAI.CycleClique.certificate_149_part_3 line 842
  433. theorem OAI.CycleClique.certificate_149_part_3_checked line 844
  434. def OAI.CycleClique.certificate_149_part_2 line 846
  435. theorem OAI.CycleClique.certificate_149_part_2_checked line 848
  436. def OAI.CycleClique.certificate_149_part_1 line 850
  437. theorem OAI.CycleClique.certificate_149_part_1_checked line 852
  438. def OAI.CycleClique.certificate_149 line 854
  439. theorem OAI.CycleClique.certificate_149_checked line 856
  440. theorem OAI.CycleClique.certificate_149_valid line 858
  441. def OAI.CycleClique.certificate_150_q line 860
  442. def OAI.CycleClique.certificate_150_edges line 861
  443. def OAI.CycleClique.certificate_150_part_0 line 863
  444. def OAI.CycleClique.certificate_150 line 865
  445. theorem OAI.CycleClique.certificate_150_checked line 867
  446. theorem OAI.CycleClique.certificate_150_valid line 868
  447. def OAI.CycleClique.certificate_151_q line 870
  448. def OAI.CycleClique.certificate_151_edges line 871
  449. def OAI.CycleClique.certificate_151_part_0 line 873
  450. def OAI.CycleClique.certificate_151 line 875
  451. theorem OAI.CycleClique.certificate_151_checked line 877
  452. theorem OAI.CycleClique.certificate_151_valid line 878
  453. def OAI.CycleClique.certificate_152_q line 880
  454. def OAI.CycleClique.certificate_152_edges line 881
  455. def OAI.CycleClique.certificate_152_part_0 line 883
  456. def OAI.CycleClique.certificate_152 line 885
  457. theorem OAI.CycleClique.certificate_152_checked line 887
  458. theorem OAI.CycleClique.certificate_152_valid line 888
  459. def OAI.CycleClique.certificate_153_q line 890
  460. def OAI.CycleClique.certificate_153_edges line 891
  461. def OAI.CycleClique.certificate_153_part_0 line 893
  462. def OAI.CycleClique.certificate_153_part_1 line 895
  463. def OAI.CycleClique.certificate_153 line 897
  464. theorem OAI.CycleClique.certificate_153_checked line 899
  465. theorem OAI.CycleClique.certificate_153_valid line 900
  466. def OAI.CycleClique.certificate_154_q line 902
  467. def OAI.CycleClique.certificate_154_edges line 903
  468. def OAI.CycleClique.certificate_154_part_0 line 905
  469. def OAI.CycleClique.certificate_154 line 907
  470. theorem OAI.CycleClique.certificate_154_checked line 909
  471. theorem OAI.CycleClique.certificate_154_valid line 910
  472. def OAI.CycleClique.certificate_155_q line 912
  473. def OAI.CycleClique.certificate_155_edges line 913
  474. def OAI.CycleClique.certificate_155_part_0 line 915
  475. def OAI.CycleClique.certificate_155_part_1 line 917
  476. def OAI.CycleClique.certificate_155 line 919
  477. theorem OAI.CycleClique.certificate_155_checked line 921
  478. theorem OAI.CycleClique.certificate_155_valid line 922
  479. def OAI.CycleClique.certificate_156_q line 924
  480. def OAI.CycleClique.certificate_156_edges line 925
  481. def OAI.CycleClique.certificate_156_part_0 line 927
  482. def OAI.CycleClique.certificate_156 line 929
  483. theorem OAI.CycleClique.certificate_156_checked line 931
  484. theorem OAI.CycleClique.certificate_156_valid line 932
  485. def OAI.CycleClique.certificate_157_q line 934
  486. def OAI.CycleClique.certificate_157_edges line 935
  487. def OAI.CycleClique.certificate_157_part_0 line 937
  488. def OAI.CycleClique.certificate_157 line 939
  489. theorem OAI.CycleClique.certificate_157_checked line 941
  490. theorem OAI.CycleClique.certificate_157_valid line 942
  491. def OAI.CycleClique.certificate_158_q line 944
  492. def OAI.CycleClique.certificate_158_edges line 945
  493. def OAI.CycleClique.certificate_158_part_0 line 947
  494. def OAI.CycleClique.certificate_158 line 949
  495. theorem OAI.CycleClique.certificate_158_checked line 951
  496. theorem OAI.CycleClique.certificate_158_valid line 952
  497. def OAI.CycleClique.certificate_159_q line 954
  498. def OAI.CycleClique.certificate_159_edges line 956
  499. def OAI.CycleClique.certificate_159_E line 958
  500. def OAI.CycleClique.certificate_159_M line 960
  501. def OAI.CycleClique.certificate_159_part_1_E line 962
  502. def OAI.CycleClique.certificate_159_part_1_M line 964
  503. def OAI.CycleClique.certificate_159_part_2_E line 966
  504. def OAI.CycleClique.certificate_159_part_2_M line 968
  505. def OAI.CycleClique.certificate_159_part_3_E line 970
  506. def OAI.CycleClique.certificate_159_part_3_M line 972
  507. def OAI.CycleClique.certificate_159_part_4_E line 974
  508. def OAI.CycleClique.certificate_159_part_4_M line 976
  509. def OAI.CycleClique.certificate_159_part_5_E line 978
  510. def OAI.CycleClique.certificate_159_part_5_M line 980
  511. def OAI.CycleClique.certificate_159_part_6_E line 982
  512. def OAI.CycleClique.certificate_159_part_6_M line 984
  513. def OAI.CycleClique.certificate_159_part_7_E line 986
  514. def OAI.CycleClique.certificate_159_part_7_M line 988
  515. def OAI.CycleClique.certificate_159_part_8_E line 990
  516. def OAI.CycleClique.certificate_159_part_8_M line 992
  517. def OAI.CycleClique.certificate_159_part_8 line 994
  518. theorem OAI.CycleClique.certificate_159_part_8_checked line 996
  519. def OAI.CycleClique.certificate_159_part_9_E line 998
  520. def OAI.CycleClique.certificate_159_part_9_M line 1000
  521. def OAI.CycleClique.certificate_159_part_9 line 1002
  522. theorem OAI.CycleClique.certificate_159_part_9_checked line 1004
  523. def OAI.CycleClique.certificate_159_part_10_E line 1006
  524. def OAI.CycleClique.certificate_159_part_10_M line 1008
  525. def OAI.CycleClique.certificate_159_part_11_E line 1010
  526. def OAI.CycleClique.certificate_159_part_11_M line 1012
  527. def OAI.CycleClique.certificate_159_part_12_E line 1014
  528. def OAI.CycleClique.certificate_159_part_12_M line 1016
  529. def OAI.CycleClique.certificate_159_part_13_E line 1018
  530. def OAI.CycleClique.certificate_159_part_13_M line 1020
  531. def OAI.CycleClique.certificate_159_part_13 line 1022
  532. theorem OAI.CycleClique.certificate_159_part_13_checked line 1024
  533. def OAI.CycleClique.certificate_159_part_14_E line 1026
  534. def OAI.CycleClique.certificate_159_part_14_M line 1028
  535. def OAI.CycleClique.certificate_159_part_15_E line 1030
  536. def OAI.CycleClique.certificate_159_part_15_M line 1032
  537. def OAI.CycleClique.certificate_159_part_16_E line 1034
  538. def OAI.CycleClique.certificate_159_part_16_M line 1036
  539. def OAI.CycleClique.certificate_159_part_16 line 1038
  540. theorem OAI.CycleClique.certificate_159_part_16_checked line 1040
  541. def OAI.CycleClique.certificate_159_part_17_E line 1042
  542. def OAI.CycleClique.certificate_159_part_17_M line 1044
  543. def OAI.CycleClique.certificate_159_part_17 line 1046
  544. theorem OAI.CycleClique.certificate_159_part_17_checked line 1048
  545. def OAI.CycleClique.certificate_159_part_18_E line 1050
  546. def OAI.CycleClique.certificate_159_part_18_M line 1052
  547. def OAI.CycleClique.certificate_159_part_18 line 1054
  548. theorem OAI.CycleClique.certificate_159_part_18_checked line 1056
  549. def OAI.CycleClique.certificate_159_part_19_E line 1058
  550. def OAI.CycleClique.certificate_159_part_19_M line 1060
  551. def OAI.CycleClique.certificate_159_part_19 line 1062
  552. theorem OAI.CycleClique.certificate_159_part_19_checked line 1064
  553. def OAI.CycleClique.certificate_159_part_20_E line 1066
  554. def OAI.CycleClique.certificate_159_part_20_M line 1068
  555. def OAI.CycleClique.certificate_159_part_21_E line 1070
  556. def OAI.CycleClique.certificate_159_part_21_M line 1072
  557. def OAI.CycleClique.certificate_159_part_22_E line 1074
  558. def OAI.CycleClique.certificate_159_part_22_M line 1076
  559. def OAI.CycleClique.certificate_159_part_23_E line 1078
  560. def OAI.CycleClique.certificate_159_part_23_M line 1080
  561. def OAI.CycleClique.certificate_159_part_24_E line 1082
  562. def OAI.CycleClique.certificate_159_part_24_M line 1084
  563. def OAI.CycleClique.certificate_159_part_24 line 1086
  564. theorem OAI.CycleClique.certificate_159_part_24_checked line 1088
  565. def OAI.CycleClique.certificate_159_part_23 line 1090
  566. theorem OAI.CycleClique.certificate_159_part_23_checked line 1092
  567. def OAI.CycleClique.certificate_159_part_22 line 1094
  568. theorem OAI.CycleClique.certificate_159_part_22_checked line 1096
  569. def OAI.CycleClique.certificate_159_part_25_E line 1098
  570. def OAI.CycleClique.certificate_159_part_25_M line 1100
  571. def OAI.CycleClique.certificate_159_part_25 line 1102
  572. theorem OAI.CycleClique.certificate_159_part_25_checked line 1104
  573. def OAI.CycleClique.certificate_159_part_21 line 1106
  574. theorem OAI.CycleClique.certificate_159_part_21_checked line 1108
  575. def OAI.CycleClique.certificate_159_part_20 line 1110
  576. theorem OAI.CycleClique.certificate_159_part_20_checked line 1112
  577. def OAI.CycleClique.certificate_159_part_15 line 1114
  578. theorem OAI.CycleClique.certificate_159_part_15_checked line 1116
  579. def OAI.CycleClique.certificate_159_part_14 line 1118
  580. theorem OAI.CycleClique.certificate_159_part_14_checked line 1120
  581. def OAI.CycleClique.certificate_159_part_12 line 1122
  582. theorem OAI.CycleClique.certificate_159_part_12_checked line 1124
  583. def OAI.CycleClique.certificate_159_part_11 line 1126
  584. theorem OAI.CycleClique.certificate_159_part_11_checked line 1128
  585. def OAI.CycleClique.certificate_159_part_10 line 1130
  586. theorem OAI.CycleClique.certificate_159_part_10_checked line 1132
  587. def OAI.CycleClique.certificate_159_part_7 line 1134
  588. theorem OAI.CycleClique.certificate_159_part_7_checked line 1136
  589. def OAI.CycleClique.certificate_159_part_6 line 1138
  590. theorem OAI.CycleClique.certificate_159_part_6_checked line 1140
  591. def OAI.CycleClique.certificate_159_part_5 line 1142
  592. theorem OAI.CycleClique.certificate_159_part_5_checked line 1144
  593. def OAI.CycleClique.certificate_159_part_4 line 1146
  594. theorem OAI.CycleClique.certificate_159_part_4_checked line 1148
  595. def OAI.CycleClique.certificate_159_part_3 line 1150
  596. theorem OAI.CycleClique.certificate_159_part_3_checked line 1152
  597. def OAI.CycleClique.certificate_159_part_2 line 1154
  598. theorem OAI.CycleClique.certificate_159_part_2_checked line 1156
  599. def OAI.CycleClique.certificate_159_part_1 line 1158
  600. theorem OAI.CycleClique.certificate_159_part_1_checked line 1160
  601. def OAI.CycleClique.certificate_159 line 1162
  602. theorem OAI.CycleClique.certificate_159_checked line 1164
  603. theorem OAI.CycleClique.certificate_159_valid line 1166