OAI/Combinatorics/Ramsey/CycleClique/Certificates002.lean

GitHub source file

345 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.certificate_32_q line 20
  2. def OAI.CycleClique.certificate_32_edges line 21
  3. def OAI.CycleClique.certificate_32_part_0 line 23
  4. def OAI.CycleClique.certificate_32 line 25
  5. theorem OAI.CycleClique.certificate_32_checked line 27
  6. theorem OAI.CycleClique.certificate_32_valid line 28
  7. def OAI.CycleClique.certificate_33_q line 30
  8. def OAI.CycleClique.certificate_33_edges line 32
  9. def OAI.CycleClique.certificate_33_E line 34
  10. def OAI.CycleClique.certificate_33_M line 36
  11. def OAI.CycleClique.certificate_33_part_1_E line 38
  12. def OAI.CycleClique.certificate_33_part_1_M line 40
  13. def OAI.CycleClique.certificate_33_part_2_E line 42
  14. def OAI.CycleClique.certificate_33_part_2_M line 44
  15. def OAI.CycleClique.certificate_33_part_3_E line 46
  16. def OAI.CycleClique.certificate_33_part_3_M line 48
  17. def OAI.CycleClique.certificate_33_part_3 line 50
  18. theorem OAI.CycleClique.certificate_33_part_3_checked line 52
  19. def OAI.CycleClique.certificate_33_part_4_E line 54
  20. def OAI.CycleClique.certificate_33_part_4_M line 56
  21. def OAI.CycleClique.certificate_33_part_5_E line 58
  22. def OAI.CycleClique.certificate_33_part_5_M line 60
  23. def OAI.CycleClique.certificate_33_part_6_E line 62
  24. def OAI.CycleClique.certificate_33_part_6_M line 64
  25. def OAI.CycleClique.certificate_33_part_7_E line 66
  26. def OAI.CycleClique.certificate_33_part_7_M line 68
  27. def OAI.CycleClique.certificate_33_part_7 line 70
  28. theorem OAI.CycleClique.certificate_33_part_7_checked line 72
  29. def OAI.CycleClique.certificate_33_part_8_E line 74
  30. def OAI.CycleClique.certificate_33_part_8_M line 76
  31. def OAI.CycleClique.certificate_33_part_8 line 78
  32. theorem OAI.CycleClique.certificate_33_part_8_checked line 80
  33. def OAI.CycleClique.certificate_33_part_9_E line 82
  34. def OAI.CycleClique.certificate_33_part_9_M line 84
  35. def OAI.CycleClique.certificate_33_part_10_E line 86
  36. def OAI.CycleClique.certificate_33_part_10_M line 88
  37. def OAI.CycleClique.certificate_33_part_10 line 90
  38. theorem OAI.CycleClique.certificate_33_part_10_checked line 92
  39. def OAI.CycleClique.certificate_33_part_11_E line 94
  40. def OAI.CycleClique.certificate_33_part_11_M line 96
  41. def OAI.CycleClique.certificate_33_part_12_E line 98
  42. def OAI.CycleClique.certificate_33_part_12_M line 100
  43. def OAI.CycleClique.certificate_33_part_12 line 102
  44. theorem OAI.CycleClique.certificate_33_part_12_checked line 104
  45. def OAI.CycleClique.certificate_33_part_11 line 106
  46. theorem OAI.CycleClique.certificate_33_part_11_checked line 108
  47. def OAI.CycleClique.certificate_33_part_9 line 110
  48. theorem OAI.CycleClique.certificate_33_part_9_checked line 112
  49. def OAI.CycleClique.certificate_33_part_6 line 114
  50. theorem OAI.CycleClique.certificate_33_part_6_checked line 116
  51. def OAI.CycleClique.certificate_33_part_5 line 118
  52. theorem OAI.CycleClique.certificate_33_part_5_checked line 120
  53. def OAI.CycleClique.certificate_33_part_4 line 122
  54. theorem OAI.CycleClique.certificate_33_part_4_checked line 124
  55. def OAI.CycleClique.certificate_33_part_2 line 126
  56. theorem OAI.CycleClique.certificate_33_part_2_checked line 128
  57. def OAI.CycleClique.certificate_33_part_1 line 130
  58. theorem OAI.CycleClique.certificate_33_part_1_checked line 132
  59. def OAI.CycleClique.certificate_33 line 134
  60. theorem OAI.CycleClique.certificate_33_checked line 136
  61. theorem OAI.CycleClique.certificate_33_valid line 138
  62. def OAI.CycleClique.certificate_34_q line 140
  63. def OAI.CycleClique.certificate_34_edges line 141
  64. def OAI.CycleClique.certificate_34 line 143
  65. theorem OAI.CycleClique.certificate_34_checked line 145
  66. theorem OAI.CycleClique.certificate_34_valid line 146
  67. def OAI.CycleClique.certificate_35_q line 148
  68. def OAI.CycleClique.certificate_35_edges line 149
  69. def OAI.CycleClique.certificate_35_part_0 line 151
  70. def OAI.CycleClique.certificate_35 line 153
  71. theorem OAI.CycleClique.certificate_35_checked line 155
  72. theorem OAI.CycleClique.certificate_35_valid line 156
  73. def OAI.CycleClique.certificate_36_q line 158
  74. def OAI.CycleClique.certificate_36_edges line 159
  75. def OAI.CycleClique.certificate_36 line 161
  76. theorem OAI.CycleClique.certificate_36_checked line 163
  77. theorem OAI.CycleClique.certificate_36_valid line 164
  78. def OAI.CycleClique.certificate_37_q line 166
  79. def OAI.CycleClique.certificate_37_edges line 167
  80. def OAI.CycleClique.certificate_37_part_0 line 169
  81. def OAI.CycleClique.certificate_37 line 171
  82. theorem OAI.CycleClique.certificate_37_checked line 173
  83. theorem OAI.CycleClique.certificate_37_valid line 174
  84. def OAI.CycleClique.certificate_38_q line 176
  85. def OAI.CycleClique.certificate_38_edges line 177
  86. def OAI.CycleClique.certificate_38_part_0 line 179
  87. def OAI.CycleClique.certificate_38 line 181
  88. theorem OAI.CycleClique.certificate_38_checked line 183
  89. theorem OAI.CycleClique.certificate_38_valid line 184
  90. def OAI.CycleClique.certificate_39_q line 186
  91. def OAI.CycleClique.certificate_39_edges line 187
  92. def OAI.CycleClique.certificate_39_part_0 line 189
  93. def OAI.CycleClique.certificate_39 line 191
  94. theorem OAI.CycleClique.certificate_39_checked line 193
  95. theorem OAI.CycleClique.certificate_39_valid line 194
  96. def OAI.CycleClique.certificate_40_q line 196
  97. def OAI.CycleClique.certificate_40_edges line 197
  98. def OAI.CycleClique.certificate_40_part_0 line 199
  99. def OAI.CycleClique.certificate_40 line 201
  100. theorem OAI.CycleClique.certificate_40_checked line 203
  101. theorem OAI.CycleClique.certificate_40_valid line 204
  102. def OAI.CycleClique.certificate_41_q line 206
  103. def OAI.CycleClique.certificate_41_edges line 207
  104. def OAI.CycleClique.certificate_41_part_0 line 209
  105. def OAI.CycleClique.certificate_41 line 211
  106. theorem OAI.CycleClique.certificate_41_checked line 213
  107. theorem OAI.CycleClique.certificate_41_valid line 214
  108. def OAI.CycleClique.certificate_42_q line 216
  109. def OAI.CycleClique.certificate_42_edges line 217
  110. def OAI.CycleClique.certificate_42_part_0 line 219
  111. def OAI.CycleClique.certificate_42 line 221
  112. theorem OAI.CycleClique.certificate_42_checked line 223
  113. theorem OAI.CycleClique.certificate_42_valid line 224
  114. def OAI.CycleClique.certificate_43_q line 226
  115. def OAI.CycleClique.certificate_43_edges line 227
  116. def OAI.CycleClique.certificate_43_part_0 line 229
  117. def OAI.CycleClique.certificate_43 line 231
  118. theorem OAI.CycleClique.certificate_43_checked line 233
  119. theorem OAI.CycleClique.certificate_43_valid line 234
  120. def OAI.CycleClique.certificate_44_q line 236
  121. def OAI.CycleClique.certificate_44_edges line 237
  122. def OAI.CycleClique.certificate_44_part_0 line 239
  123. def OAI.CycleClique.certificate_44 line 241
  124. theorem OAI.CycleClique.certificate_44_checked line 243
  125. theorem OAI.CycleClique.certificate_44_valid line 244
  126. def OAI.CycleClique.certificate_45_q line 246
  127. def OAI.CycleClique.certificate_45_edges line 247
  128. def OAI.CycleClique.certificate_45_part_0 line 249
  129. def OAI.CycleClique.certificate_45 line 251
  130. theorem OAI.CycleClique.certificate_45_checked line 253
  131. theorem OAI.CycleClique.certificate_45_valid line 254
  132. def OAI.CycleClique.certificate_46_q line 256
  133. def OAI.CycleClique.certificate_46_edges line 257
  134. def OAI.CycleClique.certificate_46_part_0 line 259
  135. def OAI.CycleClique.certificate_46_part_1 line 261
  136. def OAI.CycleClique.certificate_46 line 263
  137. theorem OAI.CycleClique.certificate_46_checked line 265
  138. theorem OAI.CycleClique.certificate_46_valid line 266
  139. def OAI.CycleClique.certificate_47_q line 268
  140. def OAI.CycleClique.certificate_47_edges line 269
  141. def OAI.CycleClique.certificate_47 line 271
  142. theorem OAI.CycleClique.certificate_47_checked line 273
  143. theorem OAI.CycleClique.certificate_47_valid line 274
  144. def OAI.CycleClique.certificate_48_q line 276
  145. def OAI.CycleClique.certificate_48_edges line 277
  146. def OAI.CycleClique.certificate_48 line 279
  147. theorem OAI.CycleClique.certificate_48_checked line 281
  148. theorem OAI.CycleClique.certificate_48_valid line 282
  149. def OAI.CycleClique.certificate_49_q line 284
  150. def OAI.CycleClique.certificate_49_edges line 285
  151. def OAI.CycleClique.certificate_49 line 287
  152. theorem OAI.CycleClique.certificate_49_checked line 289
  153. theorem OAI.CycleClique.certificate_49_valid line 290
  154. def OAI.CycleClique.certificate_50_q line 292
  155. def OAI.CycleClique.certificate_50_edges line 294
  156. def OAI.CycleClique.certificate_50_E line 296
  157. def OAI.CycleClique.certificate_50_M line 298
  158. def OAI.CycleClique.certificate_50_part_1_E line 300
  159. def OAI.CycleClique.certificate_50_part_1_M line 302
  160. def OAI.CycleClique.certificate_50_part_2_E line 304
  161. def OAI.CycleClique.certificate_50_part_2_M line 306
  162. def OAI.CycleClique.certificate_50_part_3_E line 308
  163. def OAI.CycleClique.certificate_50_part_3_M line 310
  164. def OAI.CycleClique.certificate_50_part_4_E line 312
  165. def OAI.CycleClique.certificate_50_part_4_M line 314
  166. def OAI.CycleClique.certificate_50_part_5_E line 316
  167. def OAI.CycleClique.certificate_50_part_5_M line 318
  168. def OAI.CycleClique.certificate_50_part_6_E line 320
  169. def OAI.CycleClique.certificate_50_part_6_M line 322
  170. def OAI.CycleClique.certificate_50_part_6 line 324
  171. theorem OAI.CycleClique.certificate_50_part_6_checked line 326
  172. def OAI.CycleClique.certificate_50_part_5 line 328
  173. theorem OAI.CycleClique.certificate_50_part_5_checked line 330
  174. def OAI.CycleClique.certificate_50_part_4 line 332
  175. theorem OAI.CycleClique.certificate_50_part_4_checked line 334
  176. def OAI.CycleClique.certificate_50_part_3 line 336
  177. theorem OAI.CycleClique.certificate_50_part_3_checked line 338
  178. def OAI.CycleClique.certificate_50_part_2 line 340
  179. theorem OAI.CycleClique.certificate_50_part_2_checked line 342
  180. def OAI.CycleClique.certificate_50_part_1 line 344
  181. theorem OAI.CycleClique.certificate_50_part_1_checked line 346
  182. def OAI.CycleClique.certificate_50 line 348
  183. theorem OAI.CycleClique.certificate_50_checked line 350
  184. theorem OAI.CycleClique.certificate_50_valid line 352
  185. def OAI.CycleClique.certificate_51_q line 354
  186. def OAI.CycleClique.certificate_51_edges line 356
  187. def OAI.CycleClique.certificate_51_E line 358
  188. def OAI.CycleClique.certificate_51_M line 360
  189. def OAI.CycleClique.certificate_51_part_1_E line 362
  190. def OAI.CycleClique.certificate_51_part_1_M line 364
  191. def OAI.CycleClique.certificate_51_part_2_E line 366
  192. def OAI.CycleClique.certificate_51_part_2_M line 368
  193. def OAI.CycleClique.certificate_51_part_3_E line 370
  194. def OAI.CycleClique.certificate_51_part_3_M line 372
  195. def OAI.CycleClique.certificate_51_part_3 line 374
  196. theorem OAI.CycleClique.certificate_51_part_3_checked line 376
  197. def OAI.CycleClique.certificate_51_part_4_E line 378
  198. def OAI.CycleClique.certificate_51_part_4_M line 380
  199. def OAI.CycleClique.certificate_51_part_5_E line 382
  200. def OAI.CycleClique.certificate_51_part_5_M line 384
  201. def OAI.CycleClique.certificate_51_part_5 line 386
  202. theorem OAI.CycleClique.certificate_51_part_5_checked line 388
  203. def OAI.CycleClique.certificate_51_part_6_E line 390
  204. def OAI.CycleClique.certificate_51_part_6_M line 392
  205. def OAI.CycleClique.certificate_51_part_7_E line 394
  206. def OAI.CycleClique.certificate_51_part_7_M line 396
  207. def OAI.CycleClique.certificate_51_part_8_E line 398
  208. def OAI.CycleClique.certificate_51_part_8_M line 400
  209. def OAI.CycleClique.certificate_51_part_8 line 402
  210. theorem OAI.CycleClique.certificate_51_part_8_checked line 404
  211. def OAI.CycleClique.certificate_51_part_9_E line 406
  212. def OAI.CycleClique.certificate_51_part_9_M line 408
  213. def OAI.CycleClique.certificate_51_part_10_E line 410
  214. def OAI.CycleClique.certificate_51_part_10_M line 412
  215. def OAI.CycleClique.certificate_51_part_10 line 414
  216. theorem OAI.CycleClique.certificate_51_part_10_checked line 416
  217. def OAI.CycleClique.certificate_51_part_11_E line 418
  218. def OAI.CycleClique.certificate_51_part_11_M line 420
  219. def OAI.CycleClique.certificate_51_part_12_E line 422
  220. def OAI.CycleClique.certificate_51_part_12_M line 424
  221. def OAI.CycleClique.certificate_51_part_12 line 426
  222. theorem OAI.CycleClique.certificate_51_part_12_checked line 428
  223. def OAI.CycleClique.certificate_51_part_11 line 430
  224. theorem OAI.CycleClique.certificate_51_part_11_checked line 432
  225. def OAI.CycleClique.certificate_51_part_9 line 434
  226. theorem OAI.CycleClique.certificate_51_part_9_checked line 436
  227. def OAI.CycleClique.certificate_51_part_7 line 438
  228. theorem OAI.CycleClique.certificate_51_part_7_checked line 440
  229. def OAI.CycleClique.certificate_51_part_6 line 442
  230. theorem OAI.CycleClique.certificate_51_part_6_checked line 444
  231. def OAI.CycleClique.certificate_51_part_4 line 446
  232. theorem OAI.CycleClique.certificate_51_part_4_checked line 448
  233. def OAI.CycleClique.certificate_51_part_2 line 450
  234. theorem OAI.CycleClique.certificate_51_part_2_checked line 452
  235. def OAI.CycleClique.certificate_51_part_1 line 454
  236. theorem OAI.CycleClique.certificate_51_part_1_checked line 456
  237. def OAI.CycleClique.certificate_51 line 458
  238. theorem OAI.CycleClique.certificate_51_checked line 460
  239. theorem OAI.CycleClique.certificate_51_valid line 462
  240. def OAI.CycleClique.certificate_52_q line 464
  241. def OAI.CycleClique.certificate_52_edges line 465
  242. def OAI.CycleClique.certificate_52 line 467
  243. theorem OAI.CycleClique.certificate_52_checked line 469
  244. theorem OAI.CycleClique.certificate_52_valid line 470
  245. def OAI.CycleClique.certificate_53_q line 472
  246. def OAI.CycleClique.certificate_53_edges line 473
  247. def OAI.CycleClique.certificate_53_part_0 line 475
  248. def OAI.CycleClique.certificate_53 line 477
  249. theorem OAI.CycleClique.certificate_53_checked line 479
  250. theorem OAI.CycleClique.certificate_53_valid line 480
  251. def OAI.CycleClique.certificate_54_q line 482
  252. def OAI.CycleClique.certificate_54_edges line 483
  253. def OAI.CycleClique.certificate_54_part_0 line 485
  254. def OAI.CycleClique.certificate_54 line 487
  255. theorem OAI.CycleClique.certificate_54_checked line 489
  256. theorem OAI.CycleClique.certificate_54_valid line 490
  257. def OAI.CycleClique.certificate_55_q line 492
  258. def OAI.CycleClique.certificate_55_edges line 493
  259. def OAI.CycleClique.certificate_55_part_0 line 495
  260. def OAI.CycleClique.certificate_55 line 497
  261. theorem OAI.CycleClique.certificate_55_checked line 499
  262. theorem OAI.CycleClique.certificate_55_valid line 500
  263. def OAI.CycleClique.certificate_56_q line 502
  264. def OAI.CycleClique.certificate_56_edges line 503
  265. def OAI.CycleClique.certificate_56 line 505
  266. theorem OAI.CycleClique.certificate_56_checked line 507
  267. theorem OAI.CycleClique.certificate_56_valid line 508
  268. def OAI.CycleClique.certificate_57_q line 510
  269. def OAI.CycleClique.certificate_57_edges line 511
  270. def OAI.CycleClique.certificate_57_part_0 line 513
  271. def OAI.CycleClique.certificate_57 line 515
  272. theorem OAI.CycleClique.certificate_57_checked line 517
  273. theorem OAI.CycleClique.certificate_57_valid line 518
  274. def OAI.CycleClique.certificate_58_q line 520
  275. def OAI.CycleClique.certificate_58_edges line 522
  276. def OAI.CycleClique.certificate_58_E line 524
  277. def OAI.CycleClique.certificate_58_M line 526
  278. def OAI.CycleClique.certificate_58_part_1_E line 528
  279. def OAI.CycleClique.certificate_58_part_1_M line 530
  280. def OAI.CycleClique.certificate_58_part_2_E line 532
  281. def OAI.CycleClique.certificate_58_part_2_M line 534
  282. def OAI.CycleClique.certificate_58_part_3_E line 536
  283. def OAI.CycleClique.certificate_58_part_3_M line 538
  284. def OAI.CycleClique.certificate_58_part_3 line 540
  285. theorem OAI.CycleClique.certificate_58_part_3_checked line 542
  286. def OAI.CycleClique.certificate_58_part_4_E line 544
  287. def OAI.CycleClique.certificate_58_part_4_M line 546
  288. def OAI.CycleClique.certificate_58_part_5_E line 548
  289. def OAI.CycleClique.certificate_58_part_5_M line 550
  290. def OAI.CycleClique.certificate_58_part_6_E line 552
  291. def OAI.CycleClique.certificate_58_part_6_M line 554
  292. def OAI.CycleClique.certificate_58_part_6 line 556
  293. theorem OAI.CycleClique.certificate_58_part_6_checked line 558
  294. def OAI.CycleClique.certificate_58_part_7_E line 560
  295. def OAI.CycleClique.certificate_58_part_7_M line 562
  296. def OAI.CycleClique.certificate_58_part_8_E line 564
  297. def OAI.CycleClique.certificate_58_part_8_M line 566
  298. def OAI.CycleClique.certificate_58_part_9_E line 568
  299. def OAI.CycleClique.certificate_58_part_9_M line 570
  300. def OAI.CycleClique.certificate_58_part_9 line 572
  301. theorem OAI.CycleClique.certificate_58_part_9_checked line 574
  302. def OAI.CycleClique.certificate_58_part_8 line 576
  303. theorem OAI.CycleClique.certificate_58_part_8_checked line 578
  304. def OAI.CycleClique.certificate_58_part_7 line 580
  305. theorem OAI.CycleClique.certificate_58_part_7_checked line 582
  306. def OAI.CycleClique.certificate_58_part_5 line 584
  307. theorem OAI.CycleClique.certificate_58_part_5_checked line 586
  308. def OAI.CycleClique.certificate_58_part_4 line 588
  309. theorem OAI.CycleClique.certificate_58_part_4_checked line 590
  310. def OAI.CycleClique.certificate_58_part_2 line 592
  311. theorem OAI.CycleClique.certificate_58_part_2_checked line 594
  312. def OAI.CycleClique.certificate_58_part_1 line 596
  313. theorem OAI.CycleClique.certificate_58_part_1_checked line 598
  314. def OAI.CycleClique.certificate_58 line 600
  315. theorem OAI.CycleClique.certificate_58_checked line 602
  316. theorem OAI.CycleClique.certificate_58_valid line 604
  317. def OAI.CycleClique.certificate_59_q line 606
  318. def OAI.CycleClique.certificate_59_edges line 607
  319. def OAI.CycleClique.certificate_59_part_0 line 609
  320. def OAI.CycleClique.certificate_59 line 611
  321. theorem OAI.CycleClique.certificate_59_checked line 613
  322. theorem OAI.CycleClique.certificate_59_valid line 614
  323. def OAI.CycleClique.certificate_60_q line 616
  324. def OAI.CycleClique.certificate_60_edges line 617
  325. def OAI.CycleClique.certificate_60_part_0 line 619
  326. def OAI.CycleClique.certificate_60 line 621
  327. theorem OAI.CycleClique.certificate_60_checked line 623
  328. theorem OAI.CycleClique.certificate_60_valid line 624
  329. def OAI.CycleClique.certificate_61_q line 626
  330. def OAI.CycleClique.certificate_61_edges line 627
  331. def OAI.CycleClique.certificate_61_part_0 line 629
  332. def OAI.CycleClique.certificate_61 line 631
  333. theorem OAI.CycleClique.certificate_61_checked line 633
  334. theorem OAI.CycleClique.certificate_61_valid line 634
  335. def OAI.CycleClique.certificate_62_q line 636
  336. def OAI.CycleClique.certificate_62_edges line 637
  337. def OAI.CycleClique.certificate_62_part_0 line 639
  338. def OAI.CycleClique.certificate_62 line 641
  339. theorem OAI.CycleClique.certificate_62_checked line 643
  340. theorem OAI.CycleClique.certificate_62_valid line 644
  341. def OAI.CycleClique.certificate_63_q line 646
  342. def OAI.CycleClique.certificate_63_edges line 647
  343. def OAI.CycleClique.certificate_63 line 649
  344. theorem OAI.CycleClique.certificate_63_checked line 651
  345. theorem OAI.CycleClique.certificate_63_valid line 652