OAI/Combinatorics/Ramsey/CycleClique/Construction/CertificatesK5.lean

GitHub source file

303 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CycleClique.Construction.Certificates.k5t3p0 line 10
  2. def OAI.CycleClique.Construction.Certificates.k5t3p0_state_0 line 21
  3. theorem OAI.CycleClique.Construction.Certificates.k5t3p0_initial_eq_row_0 line 26
  4. theorem OAI.CycleClique.Construction.Certificates.k5t3p0_initial_eq_row_1 line 28
  5. theorem OAI.CycleClique.Construction.Certificates.k5t3p0_initial_eq_row_2 line 30
  6. theorem OAI.CycleClique.Construction.Certificates.k5t3p0_initial_eq line 32
  7. theorem OAI.CycleClique.Construction.Certificates.k5t3p0_closure_0 line 42
  8. theorem OAI.CycleClique.Construction.Certificates.k5t3p0_matrix_eq line 44
  9. theorem OAI.CycleClique.Construction.Certificates.k5t3p0_part_0 line 50
  10. theorem OAI.CycleClique.Construction.Certificates.k5t3p0_part_1 line 52
  11. theorem OAI.CycleClique.Construction.Certificates.k5t3p0_part_2 line 54
  12. theorem OAI.CycleClique.Construction.Certificates.k5t3p0_templates_item_0 line 56
  13. theorem OAI.CycleClique.Construction.Certificates.k5t3p0_templates_item_1 line 58
  14. theorem OAI.CycleClique.Construction.Certificates.k5t3p0_templates_item_2 line 60
  15. theorem OAI.CycleClique.Construction.Certificates.k5t3p0_part_3 line 62
  16. theorem OAI.CycleClique.Construction.Certificates.k5t3p0_part_4 line 66
  17. theorem OAI.CycleClique.Construction.Certificates.k5t3p0_part_5 line 68
  18. theorem OAI.CycleClique.Construction.Certificates.k5t3p0_part_6 line 72
  19. theorem OAI.CycleClique.Construction.Certificates.k5t3p0_check line 76
  20. def OAI.CycleClique.Construction.Certificates.k5t3p1_step_0_data line 78
  21. def OAI.CycleClique.Construction.Certificates.k5t3p1_step_0 line 80
  22. def OAI.CycleClique.Construction.Certificates.k5t3p1 line 82
  23. def OAI.CycleClique.Construction.Certificates.k5t3p1_state_0 line 96
  24. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_initial_eq_row_0 line 102
  25. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_initial_eq_row_1 line 104
  26. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_initial_eq_row_2 line 106
  27. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_initial_eq_row_3 line 108
  28. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_initial_eq line 110
  29. def OAI.CycleClique.Construction.Certificates.k5t3p1_state_1 line 122
  30. def OAI.CycleClique.Construction.Certificates.k5t3p1_local_0 line 128
  31. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_local_0_eq_row_0 line 134
  32. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_local_0_eq_row_1 line 136
  33. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_local_0_eq_row_2 line 138
  34. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_local_0_eq_row_3 line 140
  35. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_local_0_eq line 142
  36. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_local_0_paths line 154
  37. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_local_0_bad line 156
  38. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_step_0_check line 158
  39. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_update_0 line 164
  40. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_closure_1 line 168
  41. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_closure_0 line 170
  42. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_matrix_eq line 176
  43. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_part_0 line 183
  44. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_part_1 line 185
  45. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_part_2 line 187
  46. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_templates_item_0 line 189
  47. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_templates_item_1 line 191
  48. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_templates_item_2 line 193
  49. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_templates_item_3 line 195
  50. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_templates_item_4 line 197
  51. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_templates_item_5 line 199
  52. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_part_3 line 201
  53. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_required_item_0 line 205
  54. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_part_4 line 207
  55. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_part_5 line 211
  56. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_part_6 line 215
  57. theorem OAI.CycleClique.Construction.Certificates.k5t3p1_check line 219
  58. def OAI.CycleClique.Construction.Certificates.k5t3p2_step_0_data line 221
  59. def OAI.CycleClique.Construction.Certificates.k5t3p2_step_0 line 223
  60. def OAI.CycleClique.Construction.Certificates.k5t3p2_step_1_data line 225
  61. def OAI.CycleClique.Construction.Certificates.k5t3p2_step_1 line 227
  62. def OAI.CycleClique.Construction.Certificates.k5t3p2_step_2_data line 229
  63. def OAI.CycleClique.Construction.Certificates.k5t3p2_step_2 line 231
  64. def OAI.CycleClique.Construction.Certificates.k5t3p2_step_3_data line 233
  65. def OAI.CycleClique.Construction.Certificates.k5t3p2_step_3 line 235
  66. def OAI.CycleClique.Construction.Certificates.k5t3p2_step_4_data line 237
  67. def OAI.CycleClique.Construction.Certificates.k5t3p2_step_4 line 239
  68. def OAI.CycleClique.Construction.Certificates.k5t3p2_step_5_data line 241
  69. def OAI.CycleClique.Construction.Certificates.k5t3p2_step_5 line 243
  70. def OAI.CycleClique.Construction.Certificates.k5t3p2_step_6_data line 245
  71. def OAI.CycleClique.Construction.Certificates.k5t3p2_step_6 line 247
  72. def OAI.CycleClique.Construction.Certificates.k5t3p2 line 249
  73. def OAI.CycleClique.Construction.Certificates.k5t3p2_state_0 line 271
  74. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_initial_eq_row_0 line 278
  75. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_initial_eq_row_1 line 280
  76. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_initial_eq_row_2 line 282
  77. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_initial_eq_row_3 line 284
  78. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_initial_eq_row_4 line 286
  79. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_initial_eq line 288
  80. def OAI.CycleClique.Construction.Certificates.k5t3p2_state_1 line 302
  81. def OAI.CycleClique.Construction.Certificates.k5t3p2_local_0 line 309
  82. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_0_eq_row_0 line 316
  83. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_0_eq_row_1 line 318
  84. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_0_eq_row_2 line 320
  85. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_0_eq_row_3 line 322
  86. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_0_eq_row_4 line 324
  87. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_0_eq line 326
  88. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_0_paths line 340
  89. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_0_bad line 342
  90. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_step_0_check line 344
  91. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_update_0 line 350
  92. def OAI.CycleClique.Construction.Certificates.k5t3p2_state_2 line 354
  93. def OAI.CycleClique.Construction.Certificates.k5t3p2_local_1 line 361
  94. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_1_eq_row_0 line 368
  95. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_1_eq_row_1 line 370
  96. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_1_eq_row_2 line 372
  97. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_1_eq_row_3 line 374
  98. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_1_eq_row_4 line 376
  99. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_1_eq line 378
  100. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_1_paths line 392
  101. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_1_bad line 394
  102. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_step_1_check line 396
  103. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_update_1 line 402
  104. def OAI.CycleClique.Construction.Certificates.k5t3p2_state_3 line 406
  105. def OAI.CycleClique.Construction.Certificates.k5t3p2_local_2 line 413
  106. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_2_eq_row_0 line 421
  107. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_2_eq_row_1 line 423
  108. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_2_eq_row_2 line 425
  109. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_2_eq_row_3 line 427
  110. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_2_eq_row_4 line 429
  111. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_2_eq_row_5 line 431
  112. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_2_eq line 433
  113. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_2_paths line 449
  114. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_2_bad line 451
  115. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_step_2_check line 453
  116. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_update_2 line 459
  117. def OAI.CycleClique.Construction.Certificates.k5t3p2_state_4 line 463
  118. def OAI.CycleClique.Construction.Certificates.k5t3p2_local_3 line 470
  119. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_3_eq_row_0 line 478
  120. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_3_eq_row_1 line 480
  121. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_3_eq_row_2 line 482
  122. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_3_eq_row_3 line 484
  123. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_3_eq_row_4 line 486
  124. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_3_eq_row_5 line 488
  125. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_3_eq line 490
  126. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_3_paths line 506
  127. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_3_bad line 508
  128. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_step_3_check line 510
  129. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_update_3 line 516
  130. def OAI.CycleClique.Construction.Certificates.k5t3p2_state_5 line 520
  131. def OAI.CycleClique.Construction.Certificates.k5t3p2_local_4 line 527
  132. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_4_eq_row_0 line 535
  133. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_4_eq_row_1 line 537
  134. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_4_eq_row_2 line 539
  135. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_4_eq_row_3 line 541
  136. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_4_eq_row_4 line 543
  137. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_4_eq_row_5 line 545
  138. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_4_eq line 547
  139. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_4_paths line 563
  140. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_4_bad line 565
  141. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_step_4_check line 567
  142. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_update_4 line 573
  143. def OAI.CycleClique.Construction.Certificates.k5t3p2_state_6 line 577
  144. def OAI.CycleClique.Construction.Certificates.k5t3p2_local_5 line 584
  145. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_5_eq_row_0 line 591
  146. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_5_eq_row_1 line 593
  147. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_5_eq_row_2 line 595
  148. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_5_eq_row_3 line 597
  149. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_5_eq_row_4 line 599
  150. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_5_eq line 601
  151. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_5_paths line 615
  152. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_5_bad line 617
  153. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_step_5_check line 619
  154. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_update_5 line 625
  155. def OAI.CycleClique.Construction.Certificates.k5t3p2_state_7 line 629
  156. def OAI.CycleClique.Construction.Certificates.k5t3p2_local_6 line 636
  157. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_6_eq_row_0 line 643
  158. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_6_eq_row_1 line 645
  159. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_6_eq_row_2 line 647
  160. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_6_eq_row_3 line 649
  161. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_6_eq_row_4 line 651
  162. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_6_eq line 653
  163. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_6_paths line 667
  164. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_local_6_bad line 669
  165. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_step_6_check line 671
  166. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_update_6 line 677
  167. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_closure_7 line 681
  168. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_closure_6 line 683
  169. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_closure_5 line 689
  170. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_closure_4 line 695
  171. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_closure_3 line 701
  172. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_closure_2 line 707
  173. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_closure_1 line 713
  174. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_closure_0 line 719
  175. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_matrix_eq line 725
  176. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_part_0 line 732
  177. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_part_1 line 734
  178. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_part_2 line 736
  179. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_templates_item_0 line 738
  180. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_templates_item_1 line 740
  181. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_templates_item_2 line 742
  182. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_templates_item_3 line 744
  183. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_templates_item_4 line 746
  184. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_templates_item_5 line 748
  185. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_templates_item_6 line 750
  186. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_templates_item_7 line 752
  187. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_templates_item_8 line 754
  188. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_templates_item_9 line 756
  189. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_templates_item_10 line 758
  190. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_templates_item_11 line 760
  191. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_templates_item_12 line 762
  192. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_part_3 line 764
  193. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_required_item_0 line 768
  194. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_required_item_1 line 770
  195. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_part_4 line 772
  196. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_part_5 line 776
  197. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_part_6 line 780
  198. theorem OAI.CycleClique.Construction.Certificates.k5t3p2_check line 784
  199. def OAI.CycleClique.Construction.Certificates.k5t3p3 line 786
  200. def OAI.CycleClique.Construction.Certificates.k5t3p3_state_0 line 800
  201. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_initial_eq_row_0 line 807
  202. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_initial_eq_row_1 line 809
  203. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_initial_eq_row_2 line 811
  204. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_initial_eq_row_3 line 813
  205. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_initial_eq_row_4 line 815
  206. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_initial_eq line 817
  207. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_closure_0 line 831
  208. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_matrix_eq line 833
  209. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_part_0 line 839
  210. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_part_1 line 841
  211. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_part_2 line 843
  212. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_templates_item_0 line 845
  213. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_templates_item_1 line 847
  214. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_templates_item_2 line 849
  215. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_templates_item_3 line 851
  216. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_templates_item_4 line 853
  217. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_templates_item_5 line 855
  218. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_part_3 line 857
  219. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_required_item_0 line 861
  220. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_part_4 line 863
  221. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_part_5 line 867
  222. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_part_6 line 871
  223. theorem OAI.CycleClique.Construction.Certificates.k5t3p3_check line 875
  224. def OAI.CycleClique.Construction.Certificates.k5t4p0 line 877
  225. def OAI.CycleClique.Construction.Certificates.k5t4p0_state_0 line 891
  226. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_initial_eq_row_0 line 897
  227. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_initial_eq_row_1 line 899
  228. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_initial_eq_row_2 line 901
  229. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_initial_eq_row_3 line 903
  230. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_initial_eq line 905
  231. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_closure_0 line 917
  232. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_matrix_eq line 919
  233. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_part_0 line 925
  234. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_part_1 line 927
  235. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_part_2 line 929
  236. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_templates_item_0 line 931
  237. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_templates_item_1 line 933
  238. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_templates_item_2 line 935
  239. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_templates_item_3 line 937
  240. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_templates_item_4 line 939
  241. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_templates_item_5 line 941
  242. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_part_3 line 943
  243. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_part_4 line 947
  244. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_part_5 line 949
  245. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_part_6 line 953
  246. theorem OAI.CycleClique.Construction.Certificates.k5t4p0_check line 957
  247. def OAI.CycleClique.Construction.Certificates.k5t4p1 line 959
  248. def OAI.CycleClique.Construction.Certificates.k5t4p1_state_0 line 978
  249. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_initial_eq_row_0 line 985
  250. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_initial_eq_row_1 line 987
  251. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_initial_eq_row_2 line 989
  252. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_initial_eq_row_3 line 991
  253. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_initial_eq_row_4 line 993
  254. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_initial_eq line 995
  255. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_closure_0 line 1009
  256. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_matrix_eq line 1011
  257. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_part_0 line 1017
  258. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_part_1 line 1019
  259. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_part_2 line 1021
  260. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_templates_item_0 line 1023
  261. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_templates_item_1 line 1025
  262. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_templates_item_2 line 1027
  263. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_templates_item_3 line 1029
  264. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_templates_item_4 line 1031
  265. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_templates_item_5 line 1033
  266. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_templates_item_6 line 1035
  267. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_templates_item_7 line 1037
  268. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_templates_item_8 line 1039
  269. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_templates_item_9 line 1041
  270. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_templates_item_10 line 1043
  271. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_part_3 line 1045
  272. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_part_4 line 1049
  273. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_part_5 line 1051
  274. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_part_6 line 1055
  275. theorem OAI.CycleClique.Construction.Certificates.k5t4p1_check line 1059
  276. def OAI.CycleClique.Construction.Certificates.k5t5p0 line 1061
  277. def OAI.CycleClique.Construction.Certificates.k5t5p0_state_0 line 1079
  278. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_initial_eq_row_0 line 1086
  279. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_initial_eq_row_1 line 1088
  280. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_initial_eq_row_2 line 1090
  281. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_initial_eq_row_3 line 1092
  282. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_initial_eq_row_4 line 1094
  283. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_initial_eq line 1096
  284. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_closure_0 line 1110
  285. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_matrix_eq line 1112
  286. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_part_0 line 1118
  287. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_part_1 line 1120
  288. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_part_2 line 1122
  289. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_templates_item_0 line 1124
  290. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_templates_item_1 line 1126
  291. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_templates_item_2 line 1128
  292. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_templates_item_3 line 1130
  293. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_templates_item_4 line 1132
  294. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_templates_item_5 line 1134
  295. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_templates_item_6 line 1136
  296. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_templates_item_7 line 1138
  297. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_templates_item_8 line 1140
  298. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_templates_item_9 line 1142
  299. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_part_3 line 1144
  300. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_part_4 line 1148
  301. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_part_5 line 1150
  302. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_part_6 line 1154
  303. theorem OAI.CycleClique.Construction.Certificates.k5t5p0_check line 1158