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

GitHub source file

815 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CycleClique.Construction.Certificates.k6t3p0 line 10
2. def OAI.CycleClique.Construction.Certificates.k6t3p0_state_0 line 21
3. theorem OAI.CycleClique.Construction.Certificates.k6t3p0_initial_eq_row_0 line 26
4. theorem OAI.CycleClique.Construction.Certificates.k6t3p0_initial_eq_row_1 line 28
5. theorem OAI.CycleClique.Construction.Certificates.k6t3p0_initial_eq_row_2 line 30
6. theorem OAI.CycleClique.Construction.Certificates.k6t3p0_initial_eq line 32
7. theorem OAI.CycleClique.Construction.Certificates.k6t3p0_closure_0 line 42
8. theorem OAI.CycleClique.Construction.Certificates.k6t3p0_matrix_eq line 44
9. theorem OAI.CycleClique.Construction.Certificates.k6t3p0_part_0 line 50
10. theorem OAI.CycleClique.Construction.Certificates.k6t3p0_part_1 line 52
11. theorem OAI.CycleClique.Construction.Certificates.k6t3p0_part_2 line 54
12. theorem OAI.CycleClique.Construction.Certificates.k6t3p0_templates_item_0 line 56
13. theorem OAI.CycleClique.Construction.Certificates.k6t3p0_templates_item_1 line 58
14. theorem OAI.CycleClique.Construction.Certificates.k6t3p0_templates_item_2 line 60
15. theorem OAI.CycleClique.Construction.Certificates.k6t3p0_part_3 line 62
16. theorem OAI.CycleClique.Construction.Certificates.k6t3p0_part_4 line 66
17. theorem OAI.CycleClique.Construction.Certificates.k6t3p0_part_5 line 68
18. theorem OAI.CycleClique.Construction.Certificates.k6t3p0_part_6 line 72
19. theorem OAI.CycleClique.Construction.Certificates.k6t3p0_check line 76
20. def OAI.CycleClique.Construction.Certificates.k6t3p1 line 78
21. def OAI.CycleClique.Construction.Certificates.k6t3p1_state_0 line 92
22. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_initial_eq_row_0 line 98
23. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_initial_eq_row_1 line 100
24. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_initial_eq_row_2 line 102
25. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_initial_eq_row_3 line 104
26. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_initial_eq line 106
27. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_closure_0 line 118
28. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_matrix_eq line 120
29. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_part_0 line 126
30. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_part_1 line 128
31. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_part_2 line 130
32. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_templates_item_0 line 132
33. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_templates_item_1 line 134
34. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_templates_item_2 line 136
35. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_templates_item_3 line 138
36. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_templates_item_4 line 140
37. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_templates_item_5 line 142
38. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_part_3 line 144
39. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_part_4 line 148
40. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_part_5 line 150
41. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_part_6 line 154
42. theorem OAI.CycleClique.Construction.Certificates.k6t3p1_check line 158
43. def OAI.CycleClique.Construction.Certificates.k6t3p2_step_0_data line 160
44. def OAI.CycleClique.Construction.Certificates.k6t3p2_step_0 line 162
45. def OAI.CycleClique.Construction.Certificates.k6t3p2_step_1_data line 164
46. def OAI.CycleClique.Construction.Certificates.k6t3p2_step_1 line 166
47. def OAI.CycleClique.Construction.Certificates.k6t3p2_step_2_data line 168
48. def OAI.CycleClique.Construction.Certificates.k6t3p2_step_2 line 170
49. def OAI.CycleClique.Construction.Certificates.k6t3p2_step_3_data line 172
50. def OAI.CycleClique.Construction.Certificates.k6t3p2_step_3 line 174
51. def OAI.CycleClique.Construction.Certificates.k6t3p2_step_4_data line 176
52. def OAI.CycleClique.Construction.Certificates.k6t3p2_step_4 line 178
53. def OAI.CycleClique.Construction.Certificates.k6t3p2 line 180
54. def OAI.CycleClique.Construction.Certificates.k6t3p2_state_0 line 201
55. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_initial_eq_row_0 line 208
56. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_initial_eq_row_1 line 210
57. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_initial_eq_row_2 line 212
58. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_initial_eq_row_3 line 214
59. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_initial_eq_row_4 line 216
60. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_initial_eq line 218
61. def OAI.CycleClique.Construction.Certificates.k6t3p2_state_1 line 232
62. def OAI.CycleClique.Construction.Certificates.k6t3p2_local_0 line 239
63. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_0_eq_row_0 line 246
64. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_0_eq_row_1 line 248
65. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_0_eq_row_2 line 250
66. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_0_eq_row_3 line 252
67. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_0_eq_row_4 line 254
68. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_0_eq line 256
69. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_0_paths line 270
70. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_0_bad line 272
71. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_step_0_check line 274
72. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_update_0 line 280
73. def OAI.CycleClique.Construction.Certificates.k6t3p2_state_2 line 284
74. def OAI.CycleClique.Construction.Certificates.k6t3p2_local_1 line 291
75. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_1_eq_row_0 line 298
76. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_1_eq_row_1 line 300
77. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_1_eq_row_2 line 302
78. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_1_eq_row_3 line 304
79. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_1_eq_row_4 line 306
80. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_1_eq line 308
81. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_1_paths line 322
82. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_1_bad line 324
83. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_step_1_check line 326
84. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_update_1 line 332
85. def OAI.CycleClique.Construction.Certificates.k6t3p2_state_3 line 336
86. def OAI.CycleClique.Construction.Certificates.k6t3p2_local_2 line 343
87. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_2_eq_row_0 line 350
88. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_2_eq_row_1 line 352
89. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_2_eq_row_2 line 354
90. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_2_eq_row_3 line 356
91. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_2_eq_row_4 line 358
92. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_2_eq line 360
93. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_2_paths line 374
94. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_2_bad line 376
95. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_step_2_check line 378
96. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_update_2 line 384
97. def OAI.CycleClique.Construction.Certificates.k6t3p2_state_4 line 388
98. def OAI.CycleClique.Construction.Certificates.k6t3p2_local_3 line 395
99. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_3_eq_row_0 line 402
100. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_3_eq_row_1 line 404
101. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_3_eq_row_2 line 406
102. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_3_eq_row_3 line 408
103. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_3_eq_row_4 line 410
104. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_3_eq line 412
105. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_3_paths line 426
106. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_3_bad line 428
107. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_step_3_check line 430
108. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_update_3 line 436
109. def OAI.CycleClique.Construction.Certificates.k6t3p2_state_5 line 440
110. def OAI.CycleClique.Construction.Certificates.k6t3p2_local_4 line 447
111. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_4_eq_row_0 line 455
112. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_4_eq_row_1 line 457
113. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_4_eq_row_2 line 459
114. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_4_eq_row_3 line 461
115. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_4_eq_row_4 line 463
116. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_4_eq_row_5 line 465
117. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_4_eq line 467
118. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_4_paths line 483
119. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_local_4_bad line 485
120. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_step_4_check line 487
121. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_update_4 line 493
122. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_closure_5 line 497
123. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_closure_4 line 499
124. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_closure_3 line 505
125. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_closure_2 line 511
126. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_closure_1 line 517
127. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_closure_0 line 523
128. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_matrix_eq line 529
129. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_part_0 line 536
130. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_part_1 line 538
131. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_part_2 line 540
132. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_templates_item_0 line 542
133. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_templates_item_1 line 544
134. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_templates_item_2 line 546
135. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_templates_item_3 line 548
136. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_templates_item_4 line 550
137. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_templates_item_5 line 552
138. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_templates_item_6 line 554
139. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_templates_item_7 line 556
140. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_templates_item_8 line 558
141. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_templates_item_9 line 560
142. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_templates_item_10 line 562
143. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_templates_item_11 line 564
144. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_part_3 line 566
145. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_required_item_0 line 570
146. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_required_item_1 line 572
147. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_part_4 line 574
148. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_part_5 line 578
149. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_part_6 line 582
150. theorem OAI.CycleClique.Construction.Certificates.k6t3p2_check line 586
151. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_0_data line 588
152. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_0 line 590
153. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_1_data line 592
154. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_1 line 594
155. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_2_data line 596
156. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_2 line 598
157. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_3_data line 600
158. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_3 line 602
159. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_4_data line 604
160. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_4 line 606
161. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_5_data line 608
162. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_5 line 610
163. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_6_data line 612
164. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_6 line 614
165. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_7_data line 616
166. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_7 line 618
167. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_8_data line 620
168. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_8 line 622
169. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_9_data line 624
170. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_9 line 626
171. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_10_data line 628
172. def OAI.CycleClique.Construction.Certificates.k6t3p3_step_10 line 630
173. def OAI.CycleClique.Construction.Certificates.k6t3p3 line 632
174. def OAI.CycleClique.Construction.Certificates.k6t3p3_state_0 line 658
175. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_initial_eq_row_0 line 666
176. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_initial_eq_row_1 line 668
177. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_initial_eq_row_2 line 670
178. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_initial_eq_row_3 line 672
179. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_initial_eq_row_4 line 674
180. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_initial_eq_row_5 line 676
181. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_initial_eq line 678
182. def OAI.CycleClique.Construction.Certificates.k6t3p3_state_1 line 694
183. def OAI.CycleClique.Construction.Certificates.k6t3p3_local_0 line 702
184. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_0_eq_row_0 line 710
185. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_0_eq_row_1 line 712
186. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_0_eq_row_2 line 714
187. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_0_eq_row_3 line 716
188. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_0_eq_row_4 line 718
189. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_0_eq_row_5 line 720
190. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_0_eq line 722
191. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_0_paths line 738
192. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_0_bad line 740
193. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_step_0_check line 742
194. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_update_0 line 748
195. def OAI.CycleClique.Construction.Certificates.k6t3p3_state_2 line 752
196. def OAI.CycleClique.Construction.Certificates.k6t3p3_local_1 line 760
197. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_1_eq_row_0 line 769
198. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_1_eq_row_1 line 771
199. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_1_eq_row_2 line 773
200. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_1_eq_row_3 line 775
201. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_1_eq_row_4 line 777
202. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_1_eq_row_5 line 779
203. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_1_eq_row_6 line 781
204. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_1_eq line 783
205. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_1_paths line 801
206. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_1_bad line 803
207. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_step_1_check line 805
208. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_update_1 line 811
209. def OAI.CycleClique.Construction.Certificates.k6t3p3_state_3 line 815
210. def OAI.CycleClique.Construction.Certificates.k6t3p3_local_2 line 823
211. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_2_eq_row_0 line 832
212. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_2_eq_row_1 line 834
213. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_2_eq_row_2 line 836
214. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_2_eq_row_3 line 838
215. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_2_eq_row_4 line 840
216. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_2_eq_row_5 line 842
217. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_2_eq_row_6 line 844
218. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_2_eq line 846
219. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_2_paths line 864
220. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_2_bad line 866
221. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_step_2_check line 868
222. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_update_2 line 874
223. def OAI.CycleClique.Construction.Certificates.k6t3p3_state_4 line 878
224. def OAI.CycleClique.Construction.Certificates.k6t3p3_local_3 line 886
225. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_3_eq_row_0 line 895
226. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_3_eq_row_1 line 897
227. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_3_eq_row_2 line 899
228. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_3_eq_row_3 line 901
229. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_3_eq_row_4 line 903
230. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_3_eq_row_5 line 905
231. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_3_eq_row_6 line 907
232. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_3_eq line 909
233. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_3_paths line 927
234. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_3_bad line 929
235. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_step_3_check line 931
236. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_update_3 line 937
237. def OAI.CycleClique.Construction.Certificates.k6t3p3_state_5 line 941
238. def OAI.CycleClique.Construction.Certificates.k6t3p3_local_4 line 949
239. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_4_eq_row_0 line 958
240. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_4_eq_row_1 line 960
241. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_4_eq_row_2 line 962
242. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_4_eq_row_3 line 964
243. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_4_eq_row_4 line 966
244. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_4_eq_row_5 line 968
245. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_4_eq_row_6 line 970
246. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_4_eq line 972
247. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_4_paths line 990
248. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_4_bad line 992
249. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_step_4_check line 994
250. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_update_4 line 1000
251. def OAI.CycleClique.Construction.Certificates.k6t3p3_state_6 line 1004
252. def OAI.CycleClique.Construction.Certificates.k6t3p3_local_5 line 1012
253. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_5_eq_row_0 line 1021
254. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_5_eq_row_1 line 1023
255. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_5_eq_row_2 line 1025
256. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_5_eq_row_3 line 1027
257. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_5_eq_row_4 line 1029
258. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_5_eq_row_5 line 1031
259. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_5_eq_row_6 line 1033
260. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_5_eq line 1035
261. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_5_paths line 1053
262. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_5_bad line 1055
263. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_step_5_check line 1057
264. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_update_5 line 1063
265. def OAI.CycleClique.Construction.Certificates.k6t3p3_state_7 line 1067
266. def OAI.CycleClique.Construction.Certificates.k6t3p3_local_6 line 1075
267. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_6_eq_row_0 line 1083
268. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_6_eq_row_1 line 1085
269. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_6_eq_row_2 line 1087
270. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_6_eq_row_3 line 1089
271. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_6_eq_row_4 line 1091
272. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_6_eq_row_5 line 1093
273. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_6_eq line 1095
274. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_6_paths line 1111
275. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_6_bad line 1113
276. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_step_6_check line 1115
277. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_update_6 line 1121
278. def OAI.CycleClique.Construction.Certificates.k6t3p3_state_8 line 1125
279. def OAI.CycleClique.Construction.Certificates.k6t3p3_local_7 line 1133
280. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_7_eq_row_0 line 1141
281. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_7_eq_row_1 line 1143
282. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_7_eq_row_2 line 1145
283. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_7_eq_row_3 line 1147
284. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_7_eq_row_4 line 1149
285. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_7_eq_row_5 line 1151
286. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_7_eq line 1153
287. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_7_paths line 1169
288. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_7_bad line 1171
289. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_step_7_check line 1173
290. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_update_7 line 1179
291. def OAI.CycleClique.Construction.Certificates.k6t3p3_state_9 line 1183
292. def OAI.CycleClique.Construction.Certificates.k6t3p3_local_8 line 1191
293. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_8_eq_row_0 line 1199
294. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_8_eq_row_1 line 1201
295. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_8_eq_row_2 line 1203
296. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_8_eq_row_3 line 1205
297. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_8_eq_row_4 line 1207
298. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_8_eq_row_5 line 1209
299. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_8_eq line 1211
300. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_8_paths line 1227
301. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_8_bad line 1229
302. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_step_8_check line 1231
303. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_update_8 line 1237
304. def OAI.CycleClique.Construction.Certificates.k6t3p3_state_10 line 1241
305. def OAI.CycleClique.Construction.Certificates.k6t3p3_local_9 line 1249
306. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_9_eq_row_0 line 1257
307. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_9_eq_row_1 line 1259
308. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_9_eq_row_2 line 1261
309. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_9_eq_row_3 line 1263
310. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_9_eq_row_4 line 1265
311. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_9_eq_row_5 line 1267
312. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_9_eq line 1269
313. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_9_paths line 1285
314. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_9_bad line 1287
315. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_step_9_check line 1289
316. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_update_9 line 1295
317. def OAI.CycleClique.Construction.Certificates.k6t3p3_state_11 line 1299
318. def OAI.CycleClique.Construction.Certificates.k6t3p3_local_10 line 1307
319. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_10_eq_row_0 line 1315
320. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_10_eq_row_1 line 1317
321. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_10_eq_row_2 line 1319
322. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_10_eq_row_3 line 1321
323. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_10_eq_row_4 line 1323
324. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_10_eq_row_5 line 1325
325. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_10_eq line 1327
326. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_10_paths line 1343
327. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_local_10_bad line 1345
328. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_step_10_check line 1347
329. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_update_10 line 1353
330. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_closure_11 line 1357
331. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_closure_10 line 1359
332. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_closure_9 line 1365
333. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_closure_8 line 1371
334. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_closure_7 line 1377
335. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_closure_6 line 1383
336. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_closure_5 line 1389
337. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_closure_4 line 1395
338. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_closure_3 line 1401
339. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_closure_2 line 1407
340. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_closure_1 line 1413
341. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_closure_0 line 1419
342. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_matrix_eq line 1425
343. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_part_0 line 1432
344. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_part_1 line 1434
345. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_part_2 line 1436
346. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_templates_item_0 line 1438
347. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_templates_item_1 line 1440
348. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_templates_item_2 line 1442
349. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_templates_item_3 line 1444
350. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_templates_item_4 line 1446
351. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_templates_item_5 line 1448
352. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_templates_item_6 line 1450
353. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_templates_item_7 line 1452
354. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_templates_item_8 line 1454
355. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_templates_item_9 line 1456
356. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_templates_item_10 line 1458
357. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_templates_item_11 line 1460
358. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_templates_item_12 line 1462
359. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_templates_item_13 line 1464
360. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_templates_item_14 line 1466
361. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_templates_item_15 line 1468
362. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_part_3 line 1470
363. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_required_item_0 line 1474
364. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_required_item_1 line 1476
365. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_required_item_2 line 1478
366. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_part_4 line 1480
367. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_part_5 line 1484
368. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_part_6 line 1488
369. theorem OAI.CycleClique.Construction.Certificates.k6t3p3_check line 1492
370. def OAI.CycleClique.Construction.Certificates.k6t3p4 line 1494
371. def OAI.CycleClique.Construction.Certificates.k6t3p4_state_0 line 1511
372. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_initial_eq_row_0 line 1518
373. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_initial_eq_row_1 line 1520
374. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_initial_eq_row_2 line 1522
375. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_initial_eq_row_3 line 1524
376. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_initial_eq_row_4 line 1526
377. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_initial_eq line 1528
378. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_closure_0 line 1542
379. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_matrix_eq line 1544
380. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_part_0 line 1550
381. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_part_1 line 1552
382. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_part_2 line 1554
383. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_templates_item_0 line 1556
384. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_templates_item_1 line 1558
385. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_templates_item_2 line 1560
386. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_templates_item_3 line 1562
387. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_templates_item_4 line 1564
388. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_templates_item_5 line 1566
389. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_templates_item_6 line 1568
390. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_part_3 line 1570
391. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_required_item_0 line 1574
392. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_required_item_1 line 1576
393. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_required_item_2 line 1578
394. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_part_4 line 1580
395. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_part_5 line 1584
396. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_part_6 line 1588
397. theorem OAI.CycleClique.Construction.Certificates.k6t3p4_check line 1592
398. def OAI.CycleClique.Construction.Certificates.k6t3p5 line 1594
399. def OAI.CycleClique.Construction.Certificates.k6t3p5_state_0 line 1614
400. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_initial_eq_row_0 line 1622
401. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_initial_eq_row_1 line 1624
402. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_initial_eq_row_2 line 1626
403. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_initial_eq_row_3 line 1628
404. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_initial_eq_row_4 line 1630
405. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_initial_eq_row_5 line 1632
406. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_initial_eq line 1634
407. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_closure_0 line 1650
408. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_matrix_eq line 1652
409. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_part_0 line 1658
410. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_part_1 line 1660
411. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_part_2 line 1662
412. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_templates_item_0 line 1664
413. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_templates_item_1 line 1666
414. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_templates_item_2 line 1668
415. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_templates_item_3 line 1670
416. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_templates_item_4 line 1672
417. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_templates_item_5 line 1674
418. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_templates_item_6 line 1676
419. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_templates_item_7 line 1678
420. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_templates_item_8 line 1680
421. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_templates_item_9 line 1682
422. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_templates_item_10 line 1684
423. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_templates_item_11 line 1686
424. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_part_3 line 1688
425. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_required_item_0 line 1692
426. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_part_4 line 1694
427. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_part_5 line 1698
428. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_part_6 line 1702
429. theorem OAI.CycleClique.Construction.Certificates.k6t3p5_check line 1706
430. def OAI.CycleClique.Construction.Certificates.k6t4p0 line 1708
431. def OAI.CycleClique.Construction.Certificates.k6t4p0_state_0 line 1722
432. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_initial_eq_row_0 line 1728
433. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_initial_eq_row_1 line 1730
434. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_initial_eq_row_2 line 1732
435. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_initial_eq_row_3 line 1734
436. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_initial_eq line 1736
437. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_closure_0 line 1748
438. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_matrix_eq line 1750
439. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_part_0 line 1756
440. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_part_1 line 1758
441. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_part_2 line 1760
442. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_templates_item_0 line 1762
443. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_templates_item_1 line 1764
444. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_templates_item_2 line 1766
445. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_templates_item_3 line 1768
446. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_templates_item_4 line 1770
447. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_templates_item_5 line 1772
448. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_part_3 line 1774
449. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_part_4 line 1778
450. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_part_5 line 1780
451. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_part_6 line 1784
452. theorem OAI.CycleClique.Construction.Certificates.k6t4p0_check line 1788
453. def OAI.CycleClique.Construction.Certificates.k6t4p1 line 1790
454. def OAI.CycleClique.Construction.Certificates.k6t4p1_state_0 line 1810
455. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_initial_eq_row_0 line 1817
456. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_initial_eq_row_1 line 1819
457. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_initial_eq_row_2 line 1821
458. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_initial_eq_row_3 line 1823
459. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_initial_eq_row_4 line 1825
460. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_initial_eq line 1827
461. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_closure_0 line 1841
462. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_matrix_eq line 1843
463. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_part_0 line 1849
464. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_part_1 line 1851
465. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_part_2 line 1853
466. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_templates_item_0 line 1855
467. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_templates_item_1 line 1857
468. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_templates_item_2 line 1859
469. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_templates_item_3 line 1861
470. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_templates_item_4 line 1863
471. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_templates_item_5 line 1865
472. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_templates_item_6 line 1867
473. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_templates_item_7 line 1869
474. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_templates_item_8 line 1871
475. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_templates_item_9 line 1873
476. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_templates_item_10 line 1875
477. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_templates_item_11 line 1877
478. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_part_3 line 1879
479. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_part_4 line 1883
480. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_part_5 line 1885
481. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_part_6 line 1889
482. theorem OAI.CycleClique.Construction.Certificates.k6t4p1_check line 1893
483. def OAI.CycleClique.Construction.Certificates.k6t4p2_step_0_data line 1895
484. def OAI.CycleClique.Construction.Certificates.k6t4p2_step_0 line 1897
485. def OAI.CycleClique.Construction.Certificates.k6t4p2_step_1_data line 1899
486. def OAI.CycleClique.Construction.Certificates.k6t4p2_step_1 line 1901
487. def OAI.CycleClique.Construction.Certificates.k6t4p2_step_2_data line 1903
488. def OAI.CycleClique.Construction.Certificates.k6t4p2_step_2 line 1905
489. def OAI.CycleClique.Construction.Certificates.k6t4p2_step_3_data line 1907
490. def OAI.CycleClique.Construction.Certificates.k6t4p2_step_3 line 1909
491. def OAI.CycleClique.Construction.Certificates.k6t4p2_step_4_data line 1911
492. def OAI.CycleClique.Construction.Certificates.k6t4p2_step_4 line 1913
493. def OAI.CycleClique.Construction.Certificates.k6t4p2_step_5_data line 1915
494. def OAI.CycleClique.Construction.Certificates.k6t4p2_step_5 line 1917
495. def OAI.CycleClique.Construction.Certificates.k6t4p2_step_6_data line 1919
496. def OAI.CycleClique.Construction.Certificates.k6t4p2_step_6 line 1921
497. def OAI.CycleClique.Construction.Certificates.k6t4p2_step_7_data line 1923
498. def OAI.CycleClique.Construction.Certificates.k6t4p2_step_7 line 1925
499. def OAI.CycleClique.Construction.Certificates.k6t4p2 line 1927
500. def OAI.CycleClique.Construction.Certificates.k6t4p2_state_0 line 1959
501. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_initial_eq_row_0 line 1967
502. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_initial_eq_row_1 line 1969
503. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_initial_eq_row_2 line 1971
504. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_initial_eq_row_3 line 1973
505. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_initial_eq_row_4 line 1975
506. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_initial_eq_row_5 line 1977
507. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_initial_eq line 1979
508. def OAI.CycleClique.Construction.Certificates.k6t4p2_state_1 line 1995
509. def OAI.CycleClique.Construction.Certificates.k6t4p2_local_0 line 2003
510. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_0_eq_row_0 line 2011
511. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_0_eq_row_1 line 2013
512. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_0_eq_row_2 line 2015
513. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_0_eq_row_3 line 2017
514. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_0_eq_row_4 line 2019
515. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_0_eq_row_5 line 2021
516. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_0_eq line 2023
517. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_0_paths line 2039
518. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_0_bad line 2041
519. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_step_0_check line 2043
520. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_update_0 line 2049
521. def OAI.CycleClique.Construction.Certificates.k6t4p2_state_2 line 2053
522. def OAI.CycleClique.Construction.Certificates.k6t4p2_local_1 line 2061
523. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_1_eq_row_0 line 2069
524. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_1_eq_row_1 line 2071
525. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_1_eq_row_2 line 2073
526. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_1_eq_row_3 line 2075
527. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_1_eq_row_4 line 2077
528. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_1_eq_row_5 line 2079
529. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_1_eq line 2081
530. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_1_paths line 2097
531. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_1_bad line 2099
532. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_step_1_check line 2101
533. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_update_1 line 2107
534. def OAI.CycleClique.Construction.Certificates.k6t4p2_state_3 line 2111
535. def OAI.CycleClique.Construction.Certificates.k6t4p2_local_2 line 2119
536. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_2_eq_row_0 line 2127
537. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_2_eq_row_1 line 2129
538. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_2_eq_row_2 line 2131
539. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_2_eq_row_3 line 2133
540. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_2_eq_row_4 line 2135
541. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_2_eq_row_5 line 2137
542. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_2_eq line 2139
543. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_2_paths line 2155
544. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_2_bad line 2157
545. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_step_2_check line 2159
546. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_update_2 line 2165
547. def OAI.CycleClique.Construction.Certificates.k6t4p2_state_4 line 2169
548. def OAI.CycleClique.Construction.Certificates.k6t4p2_local_3 line 2177
549. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_3_eq_row_0 line 2185
550. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_3_eq_row_1 line 2187
551. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_3_eq_row_2 line 2189
552. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_3_eq_row_3 line 2191
553. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_3_eq_row_4 line 2193
554. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_3_eq_row_5 line 2195
555. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_3_eq line 2197
556. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_3_paths line 2213
557. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_3_bad line 2215
558. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_step_3_check line 2217
559. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_update_3 line 2223
560. def OAI.CycleClique.Construction.Certificates.k6t4p2_state_5 line 2227
561. def OAI.CycleClique.Construction.Certificates.k6t4p2_local_4 line 2235
562. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_4_eq_row_0 line 2243
563. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_4_eq_row_1 line 2245
564. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_4_eq_row_2 line 2247
565. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_4_eq_row_3 line 2249
566. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_4_eq_row_4 line 2251
567. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_4_eq_row_5 line 2253
568. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_4_eq line 2255
569. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_4_paths line 2271
570. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_4_bad line 2273
571. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_step_4_check line 2275
572. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_update_4 line 2281
573. def OAI.CycleClique.Construction.Certificates.k6t4p2_state_6 line 2285
574. def OAI.CycleClique.Construction.Certificates.k6t4p2_local_5 line 2293
575. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_5_eq_row_0 line 2302
576. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_5_eq_row_1 line 2304
577. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_5_eq_row_2 line 2306
578. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_5_eq_row_3 line 2308
579. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_5_eq_row_4 line 2310
580. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_5_eq_row_5 line 2312
581. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_5_eq_row_6 line 2314
582. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_5_eq line 2316
583. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_5_paths line 2334
584. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_5_bad line 2336
585. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_step_5_check line 2338
586. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_update_5 line 2344
587. def OAI.CycleClique.Construction.Certificates.k6t4p2_state_7 line 2348
588. def OAI.CycleClique.Construction.Certificates.k6t4p2_local_6 line 2356
589. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_6_eq_row_0 line 2365
590. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_6_eq_row_1 line 2367
591. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_6_eq_row_2 line 2369
592. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_6_eq_row_3 line 2371
593. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_6_eq_row_4 line 2373
594. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_6_eq_row_5 line 2375
595. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_6_eq_row_6 line 2377
596. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_6_eq line 2379
597. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_6_paths line 2397
598. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_6_bad line 2399
599. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_step_6_check line 2401
600. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_update_6 line 2407
601. def OAI.CycleClique.Construction.Certificates.k6t4p2_state_8 line 2411
602. def OAI.CycleClique.Construction.Certificates.k6t4p2_local_7 line 2419
603. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_7_eq_row_0 line 2427
604. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_7_eq_row_1 line 2429
605. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_7_eq_row_2 line 2431
606. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_7_eq_row_3 line 2433
607. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_7_eq_row_4 line 2435
608. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_7_eq_row_5 line 2437
609. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_7_eq line 2439
610. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_7_paths line 2455
611. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_local_7_bad line 2457
612. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_step_7_check line 2459
613. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_update_7 line 2465
614. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_closure_8 line 2469
615. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_closure_7 line 2471
616. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_closure_6 line 2477
617. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_closure_5 line 2483
618. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_closure_4 line 2489
619. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_closure_3 line 2495
620. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_closure_2 line 2501
621. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_closure_1 line 2507
622. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_closure_0 line 2513
623. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_matrix_eq line 2519
624. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_part_0 line 2526
625. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_part_1 line 2528
626. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_part_2 line 2530
627. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_0 line 2532
628. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_1 line 2534
629. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_2 line 2536
630. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_3 line 2538
631. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_4 line 2540
632. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_5 line 2542
633. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_6 line 2544
634. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_7 line 2546
635. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_8 line 2548
636. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_9 line 2550
637. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_10 line 2552
638. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_11 line 2554
639. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_12 line 2556
640. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_13 line 2558
641. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_14 line 2560
642. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_15 line 2562
643. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_16 line 2564
644. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_17 line 2566
645. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_18 line 2568
646. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_19 line 2570
647. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_20 line 2572
648. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_21 line 2574
649. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_22 line 2576
650. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_templates_item_23 line 2578
651. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_part_3 line 2580
652. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_part_4 line 2584
653. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_part_5 line 2586
654. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_part_6 line 2590
655. theorem OAI.CycleClique.Construction.Certificates.k6t4p2_check line 2594
656. def OAI.CycleClique.Construction.Certificates.k6t4p3 line 2596
657. def OAI.CycleClique.Construction.Certificates.k6t4p3_state_0 line 2616
658. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_initial_eq_row_0 line 2624
659. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_initial_eq_row_1 line 2626
660. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_initial_eq_row_2 line 2628
661. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_initial_eq_row_3 line 2630
662. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_initial_eq_row_4 line 2632
663. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_initial_eq_row_5 line 2634
664. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_initial_eq line 2636
665. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_closure_0 line 2652
666. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_matrix_eq line 2654
667. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_part_0 line 2660
668. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_part_1 line 2662
669. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_part_2 line 2664
670. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_templates_item_0 line 2666
671. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_templates_item_1 line 2668
672. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_templates_item_2 line 2670
673. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_templates_item_3 line 2672
674. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_templates_item_4 line 2674
675. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_templates_item_5 line 2676
676. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_templates_item_6 line 2678
677. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_templates_item_7 line 2680
678. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_templates_item_8 line 2682
679. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_templates_item_9 line 2684
680. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_templates_item_10 line 2686
681. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_templates_item_11 line 2688
682. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_part_3 line 2690
683. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_required_item_0 line 2694
684. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_part_4 line 2696
685. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_part_5 line 2700
686. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_part_6 line 2704
687. theorem OAI.CycleClique.Construction.Certificates.k6t4p3_check line 2708
688. def OAI.CycleClique.Construction.Certificates.k6t4p4 line 2710
689. def OAI.CycleClique.Construction.Certificates.k6t4p4_state_0 line 2729
690. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_initial_eq_row_0 line 2737
691. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_initial_eq_row_1 line 2739
692. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_initial_eq_row_2 line 2741
693. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_initial_eq_row_3 line 2743
694. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_initial_eq_row_4 line 2745
695. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_initial_eq_row_5 line 2747
696. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_initial_eq line 2749
697. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_closure_0 line 2765
698. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_matrix_eq line 2767
699. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_part_0 line 2773
700. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_part_1 line 2775
701. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_part_2 line 2777
702. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_templates_item_0 line 2779
703. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_templates_item_1 line 2781
704. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_templates_item_2 line 2783
705. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_templates_item_3 line 2785
706. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_templates_item_4 line 2787
707. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_templates_item_5 line 2789
708. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_templates_item_6 line 2791
709. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_templates_item_7 line 2793
710. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_templates_item_8 line 2795
711. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_templates_item_9 line 2797
712. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_templates_item_10 line 2799
713. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_part_3 line 2801
714. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_part_4 line 2805
715. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_part_5 line 2807
716. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_part_6 line 2811
717. theorem OAI.CycleClique.Construction.Certificates.k6t4p4_check line 2815
718. def OAI.CycleClique.Construction.Certificates.k6t5p0 line 2817
719. def OAI.CycleClique.Construction.Certificates.k6t5p0_state_0 line 2835
720. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_initial_eq_row_0 line 2842
721. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_initial_eq_row_1 line 2844
722. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_initial_eq_row_2 line 2846
723. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_initial_eq_row_3 line 2848
724. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_initial_eq_row_4 line 2850
725. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_initial_eq line 2852
726. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_closure_0 line 2866
727. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_matrix_eq line 2868
728. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_part_0 line 2874
729. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_part_1 line 2876
730. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_part_2 line 2878
731. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_templates_item_0 line 2880
732. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_templates_item_1 line 2882
733. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_templates_item_2 line 2884
734. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_templates_item_3 line 2886
735. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_templates_item_4 line 2888
736. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_templates_item_5 line 2890
737. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_templates_item_6 line 2892
738. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_templates_item_7 line 2894
739. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_templates_item_8 line 2896
740. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_templates_item_9 line 2898
741. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_part_3 line 2900
742. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_part_4 line 2904
743. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_part_5 line 2906
744. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_part_6 line 2910
745. theorem OAI.CycleClique.Construction.Certificates.k6t5p0_check line 2914
746. def OAI.CycleClique.Construction.Certificates.k6t5p1 line 2916
747. def OAI.CycleClique.Construction.Certificates.k6t5p1_state_0 line 2941
748. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_initial_eq_row_0 line 2949
749. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_initial_eq_row_1 line 2951
750. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_initial_eq_row_2 line 2953
751. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_initial_eq_row_3 line 2955
752. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_initial_eq_row_4 line 2957
753. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_initial_eq_row_5 line 2959
754. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_initial_eq line 2961
755. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_closure_0 line 2977
756. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_matrix_eq line 2979
757. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_part_0 line 2985
758. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_part_1 line 2987
759. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_part_2 line 2989
760. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_templates_item_0 line 2991
761. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_templates_item_1 line 2993
762. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_templates_item_2 line 2995
763. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_templates_item_3 line 2997
764. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_templates_item_4 line 2999
765. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_templates_item_5 line 3001
766. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_templates_item_6 line 3003
767. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_templates_item_7 line 3005
768. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_templates_item_8 line 3007
769. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_templates_item_9 line 3009
770. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_templates_item_10 line 3011
771. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_templates_item_11 line 3013
772. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_templates_item_12 line 3015
773. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_templates_item_13 line 3017
774. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_templates_item_14 line 3019
775. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_templates_item_15 line 3021
776. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_templates_item_16 line 3023
777. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_part_3 line 3025
778. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_part_4 line 3029
779. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_part_5 line 3031
780. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_part_6 line 3035
781. theorem OAI.CycleClique.Construction.Certificates.k6t5p1_check line 3039
782. def OAI.CycleClique.Construction.Certificates.k6t6p0 line 3041
783. def OAI.CycleClique.Construction.Certificates.k6t6p0_state_0 line 3064
784. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_initial_eq_row_0 line 3072
785. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_initial_eq_row_1 line 3074
786. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_initial_eq_row_2 line 3076
787. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_initial_eq_row_3 line 3078
788. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_initial_eq_row_4 line 3080
789. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_initial_eq_row_5 line 3082
790. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_initial_eq line 3084
791. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_closure_0 line 3100
792. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_matrix_eq line 3102
793. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_part_0 line 3108
794. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_part_1 line 3110
795. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_part_2 line 3112
796. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_templates_item_0 line 3114
797. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_templates_item_1 line 3116
798. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_templates_item_2 line 3118
799. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_templates_item_3 line 3120
800. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_templates_item_4 line 3122
801. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_templates_item_5 line 3124
802. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_templates_item_6 line 3126
803. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_templates_item_7 line 3128
804. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_templates_item_8 line 3130
805. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_templates_item_9 line 3132
806. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_templates_item_10 line 3134
807. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_templates_item_11 line 3136
808. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_templates_item_12 line 3138
809. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_templates_item_13 line 3140
810. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_templates_item_14 line 3142
811. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_part_3 line 3144
812. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_part_4 line 3148
813. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_part_5 line 3150
814. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_part_6 line 3154
815. theorem OAI.CycleClique.Construction.Certificates.k6t6p0_check line 3158