OAI/Topology/EilenbergGanea/SeedChains.lean

GitHub source file

586 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EilenbergGanea.SeedEncoding.finite line 13
2. def OAI.EilenbergGanea.SeedEncoding.roseAt line 14
3. def OAI.EilenbergGanea.SeedEncoding.sectorAt line 21
4. def OAI.EilenbergGanea.SeedEncoding.cellAt line 25
5. def OAI.EilenbergGanea.SeedEncoding.sectorCode line 32
6. def OAI.EilenbergGanea.SeedEncoding.cellCode line 34
7. theorem OAI.EilenbergGanea.SeedEncoding.cellAt_code line 42
8. theorem OAI.EilenbergGanea.SeedEncoding.code_cellAt line 55
9. def OAI.EilenbergGanea.SeedEncoding.cellEquiv line 57
10. instance OAI.EilenbergGanea.SeedEncoding.properFaceDecidable line 63
11. instance OAI.EilenbergGanea.SeedEncoding.seedAdjDecidable line 68
12. def OAI.EilenbergGanea.SeedEncoding.adjCodes line 71
13. def OAI.EilenbergGanea.SeedEncoding.indexedAdj line 73
14. instance OAI.EilenbergGanea.SeedEncoding.(instance at line 74) line 74
15. theorem OAI.EilenbergGanea.SeedEncoding.adjacency_certificate line 76
16. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_0 line 82
17. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_1 line 100
18. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_2 line 118
19. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_3 line 136
20. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_4 line 154
21. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_5 line 172
22. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_6 line 190
23. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_7 line 208
24. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_8 line 226
25. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_9 line 244
26. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_10 line 262
27. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_11 line 280
28. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_12 line 298
29. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_13 line 316
30. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_14 line 334
31. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_15 line 352
32. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_16 line 370
33. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_17 line 388
34. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_18 line 406
35. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_19 line 424
36. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_20 line 442
37. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_21 line 460
38. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_22 line 478
39. def OAI.EilenbergGanea.SeedChainCertificate.edgeData_23 line 496
40. def OAI.EilenbergGanea.SeedChainCertificate.edgeData line 502
41. def OAI.EilenbergGanea.SeedChainCertificate.triangleEdgeData_0 line 504
42. def OAI.EilenbergGanea.SeedChainCertificate.triangleEdgeData_1 line 522
43. def OAI.EilenbergGanea.SeedChainCertificate.triangleEdgeData_2 line 540
44. def OAI.EilenbergGanea.SeedChainCertificate.triangleEdgeData_3 line 558
45. def OAI.EilenbergGanea.SeedChainCertificate.triangleEdgeData_4 line 576
46. def OAI.EilenbergGanea.SeedChainCertificate.triangleEdgeData_5 line 594
47. def OAI.EilenbergGanea.SeedChainCertificate.triangleEdgeData_6 line 612
48. def OAI.EilenbergGanea.SeedChainCertificate.triangleEdgeData_7 line 630
49. def OAI.EilenbergGanea.SeedChainCertificate.triangleEdgeData_8 line 648
50. def OAI.EilenbergGanea.SeedChainCertificate.triangleEdgeData_9 line 666
51. def OAI.EilenbergGanea.SeedChainCertificate.triangleEdgeData_10 line 684
52. def OAI.EilenbergGanea.SeedChainCertificate.triangleEdgeData_11 line 702
53. def OAI.EilenbergGanea.SeedChainCertificate.triangleEdgeData_12 line 720
54. def OAI.EilenbergGanea.SeedChainCertificate.triangleEdgeData_13 line 738
55. def OAI.EilenbergGanea.SeedChainCertificate.triangleEdgeData_14 line 756
56. def OAI.EilenbergGanea.SeedChainCertificate.triangleEdgeData_15 line 774
57. def OAI.EilenbergGanea.SeedChainCertificate.triangleEdgeData_16 line 792
58. def OAI.EilenbergGanea.SeedChainCertificate.triangleEdgeData line 808
59. def OAI.EilenbergGanea.SeedChainCertificate.edge line 810
60. def OAI.EilenbergGanea.SeedChainCertificate.triangleEdges line 811
61. def OAI.EilenbergGanea.SeedChainCertificate.triangle line 813
62. def OAI.EilenbergGanea.SeedChainCertificate.edgeLookupCodes_0 line 816
63. def OAI.EilenbergGanea.SeedChainCertificate.edgeLookupCodes_1 line 833
64. def OAI.EilenbergGanea.SeedChainCertificate.edgeLookupCodes_2 line 850
65. def OAI.EilenbergGanea.SeedChainCertificate.edgeLookupCodes_3 line 867
66. def OAI.EilenbergGanea.SeedChainCertificate.edgeLookupCodes_4 line 884
67. def OAI.EilenbergGanea.SeedChainCertificate.edgeLookupCodes_5 line 901
68. def OAI.EilenbergGanea.SeedChainCertificate.edgeLookupCodes_6 line 918
69. def OAI.EilenbergGanea.SeedChainCertificate.edgeLookupCodes line 926
70. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_0 line 927
71. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_1 line 944
72. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_2 line 961
73. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_3 line 978
74. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_4 line 995
75. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_5 line 1012
76. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_6 line 1029
77. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_7 line 1046
78. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_8 line 1063
79. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_9 line 1080
80. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_10 line 1097
81. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_11 line 1114
82. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_12 line 1131
83. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_13 line 1148
84. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_14 line 1165
85. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_15 line 1182
86. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_16 line 1199
87. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_17 line 1216
88. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_18 line 1233
89. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_19 line 1250
90. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_20 line 1267
91. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_21 line 1284
92. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_22 line 1301
93. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes_23 line 1318
94. def OAI.EilenbergGanea.SeedChainCertificate.triangleLookupCodes line 1323
95. def OAI.EilenbergGanea.SeedChainCertificate.edgeIndex line 1324
96. def OAI.EilenbergGanea.SeedChainCertificate.triangleIndex line 1327
97. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_0 line 1330
98. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_1 line 1333
99. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_2 line 1336
100. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_3 line 1339
101. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_4 line 1342
102. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_5 line 1345
103. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_6 line 1348
104. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_7 line 1351
105. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_8 line 1354
106. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_9 line 1357
107. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_10 line 1360
108. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_11 line 1363
109. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_12 line 1366
110. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_13 line 1369
111. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_14 line 1372
112. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_15 line 1375
113. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_16 line 1378
114. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_17 line 1381
115. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_18 line 1384
116. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_19 line 1387
117. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_20 line 1390
118. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_21 line 1393
119. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_22 line 1396
120. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_23 line 1399
121. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_24 line 1402
122. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_25 line 1405
123. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_26 line 1408
124. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_27 line 1411
125. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_28 line 1414
126. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_29 line 1417
127. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_30 line 1420
128. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_31 line 1423
129. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_32 line 1426
130. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_33 line 1429
131. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_34 line 1432
132. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_35 line 1435
133. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_36 line 1438
134. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_37 line 1441
135. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_38 line 1444
136. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_39 line 1447
137. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_40 line 1450
138. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_41 line 1453
139. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_42 line 1456
140. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_43 line 1459
141. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_44 line 1462
142. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_45 line 1465
143. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_46 line 1468
144. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_47 line 1471
145. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_48 line 1474
146. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_49 line 1477
147. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_50 line 1480
148. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_51 line 1483
149. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_52 line 1486
150. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_53 line 1489
151. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_54 line 1492
152. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_55 line 1495
153. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_56 line 1498
154. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_57 line 1501
155. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_58 line 1504
156. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_59 line 1507
157. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_60 line 1510
158. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_61 line 1513
159. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_62 line 1516
160. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_63 line 1519
161. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_64 line 1522
162. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_65 line 1525
163. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_66 line 1528
164. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_67 line 1531
165. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_68 line 1534
166. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_69 line 1537
167. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_70 line 1540
168. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_71 line 1543
169. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_72 line 1546
170. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_73 line 1549
171. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_74 line 1552
172. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_75 line 1555
173. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_76 line 1558
174. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_77 line 1561
175. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_78 line 1564
176. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_79 line 1567
177. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_80 line 1570
178. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_81 line 1573
179. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_82 line 1576
180. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_83 line 1579
181. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_84 line 1582
182. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_85 line 1585
183. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_86 line 1588
184. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_87 line 1591
185. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_88 line 1594
186. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_89 line 1597
187. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_90 line 1600
188. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_91 line 1603
189. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_92 line 1606
190. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_93 line 1609
191. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_94 line 1612
192. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_95 line 1615
193. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_96 line 1618
194. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_97 line 1621
195. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_98 line 1624
196. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_99 line 1627
197. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_100 line 1630
198. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_101 line 1633
199. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete_102 line 1636
200. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_0 line 1639
201. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_1 line 1643
202. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_2 line 1647
203. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_3 line 1651
204. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_4 line 1655
205. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_5 line 1659
206. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_6 line 1663
207. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_7 line 1667
208. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_8 line 1671
209. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_9 line 1675
210. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_10 line 1679
211. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_11 line 1683
212. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_12 line 1687
213. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_13 line 1691
214. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_14 line 1695
215. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_15 line 1699
216. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_16 line 1703
217. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_17 line 1707
218. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_18 line 1711
219. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_19 line 1715
220. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_20 line 1719
221. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_21 line 1723
222. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_22 line 1727
223. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_23 line 1731
224. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_24 line 1735
225. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_25 line 1739
226. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_26 line 1743
227. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_27 line 1747
228. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_28 line 1751
229. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_29 line 1755
230. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_30 line 1759
231. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_31 line 1763
232. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_32 line 1767
233. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_33 line 1771
234. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_34 line 1775
235. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_35 line 1779
236. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_36 line 1783
237. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_37 line 1787
238. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_38 line 1791
239. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_39 line 1795
240. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_40 line 1799
241. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_41 line 1803
242. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_42 line 1807
243. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_43 line 1811
244. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_44 line 1815
245. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_45 line 1819
246. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_46 line 1823
247. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_47 line 1827
248. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_48 line 1831
249. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_49 line 1835
250. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_50 line 1839
251. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_51 line 1843
252. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_52 line 1847
253. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_53 line 1851
254. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_54 line 1855
255. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_55 line 1859
256. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_56 line 1863
257. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_57 line 1867
258. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_58 line 1871
259. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_59 line 1875
260. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_60 line 1879
261. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_61 line 1883
262. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_62 line 1887
263. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_63 line 1891
264. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_64 line 1895
265. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_65 line 1899
266. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_66 line 1903
267. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_67 line 1907
268. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_68 line 1911
269. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_69 line 1915
270. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_70 line 1919
271. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_71 line 1923
272. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_72 line 1927
273. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_73 line 1931
274. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_74 line 1935
275. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_75 line 1939
276. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_76 line 1943
277. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_77 line 1947
278. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_78 line 1951
279. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_79 line 1955
280. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_80 line 1959
281. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_81 line 1963
282. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_82 line 1967
283. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_83 line 1971
284. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_84 line 1975
285. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_85 line 1979
286. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_86 line 1983
287. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_87 line 1987
288. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_88 line 1991
289. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_89 line 1995
290. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_90 line 1999
291. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_91 line 2003
292. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_92 line 2007
293. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_93 line 2011
294. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_94 line 2015
295. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_95 line 2019
296. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_96 line 2023
297. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_97 line 2027
298. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_98 line 2031
299. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_99 line 2035
300. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_100 line 2039
301. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_101 line 2043
302. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_102 line 2047
303. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_103 line 2051
304. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_104 line 2055
305. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_105 line 2059
306. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_106 line 2063
307. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_107 line 2067
308. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_108 line 2071
309. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_109 line 2075
310. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_110 line 2079
311. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_111 line 2083
312. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_112 line 2087
313. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_113 line 2091
314. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_114 line 2095
315. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_115 line 2099
316. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_116 line 2103
317. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_117 line 2107
318. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_118 line 2111
319. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_119 line 2115
320. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_120 line 2119
321. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_121 line 2123
322. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_122 line 2127
323. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_123 line 2131
324. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_124 line 2135
325. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_125 line 2139
326. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_126 line 2143
327. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_127 line 2147
328. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_128 line 2151
329. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_129 line 2155
330. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_130 line 2159
331. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_131 line 2163
332. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_132 line 2167
333. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_133 line 2171
334. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_134 line 2175
335. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_135 line 2179
336. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_136 line 2183
337. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_137 line 2187
338. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_138 line 2191
339. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_139 line 2195
340. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_140 line 2199
341. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_141 line 2203
342. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_142 line 2207
343. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_143 line 2211
344. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_144 line 2215
345. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_145 line 2219
346. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_146 line 2223
347. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_147 line 2227
348. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_148 line 2231
349. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_149 line 2235
350. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_150 line 2239
351. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_151 line 2243
352. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_152 line 2247
353. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_153 line 2251
354. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_154 line 2255
355. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_155 line 2259
356. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_156 line 2263
357. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_157 line 2267
358. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_158 line 2271
359. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_159 line 2275
360. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_160 line 2279
361. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_161 line 2283
362. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_162 line 2287
363. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_163 line 2291
364. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_164 line 2295
365. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_165 line 2299
366. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_166 line 2303
367. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_167 line 2307
368. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_168 line 2311
369. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_169 line 2315
370. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_170 line 2319
371. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_171 line 2323
372. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_172 line 2327
373. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_173 line 2331
374. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_174 line 2335
375. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_175 line 2339
376. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_176 line 2343
377. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_177 line 2347
378. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_178 line 2351
379. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_179 line 2355
380. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_180 line 2359
381. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_181 line 2363
382. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_182 line 2367
383. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_183 line 2371
384. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_184 line 2375
385. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_185 line 2379
386. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_186 line 2383
387. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_187 line 2387
388. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_188 line 2391
389. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_189 line 2395
390. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_190 line 2399
391. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_191 line 2403
392. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_192 line 2407
393. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_193 line 2411
394. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_194 line 2415
395. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_195 line 2419
396. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_196 line 2423
397. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_197 line 2427
398. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_198 line 2431
399. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_199 line 2435
400. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_200 line 2439
401. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_201 line 2443
402. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_202 line 2447
403. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_203 line 2451
404. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_204 line 2455
405. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_205 line 2459
406. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_206 line 2463
407. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_207 line 2467
408. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_208 line 2471
409. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_209 line 2475
410. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_210 line 2479
411. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_211 line 2483
412. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_212 line 2487
413. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_213 line 2491
414. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_214 line 2495
415. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_215 line 2499
416. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_216 line 2503
417. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_217 line 2507
418. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_218 line 2511
419. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_219 line 2515
420. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_220 line 2519
421. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_221 line 2523
422. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_222 line 2527
423. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_223 line 2531
424. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_224 line 2535
425. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_225 line 2539
426. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_226 line 2543
427. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_227 line 2547
428. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_228 line 2551
429. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_229 line 2555
430. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_230 line 2559
431. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_231 line 2563
432. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_232 line 2567
433. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_233 line 2571
434. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_234 line 2575
435. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_235 line 2579
436. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_236 line 2583
437. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_237 line 2587
438. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_238 line 2591
439. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_239 line 2595
440. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_240 line 2599
441. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_241 line 2603
442. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_242 line 2607
443. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_243 line 2611
444. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_244 line 2615
445. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_245 line 2619
446. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_246 line 2623
447. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_247 line 2627
448. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_248 line 2631
449. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_249 line 2635
450. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_250 line 2639
451. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_251 line 2643
452. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_252 line 2647
453. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_253 line 2651
454. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_254 line 2655
455. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_255 line 2659
456. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_256 line 2663
457. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_257 line 2667
458. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_258 line 2671
459. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_259 line 2675
460. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_260 line 2679
461. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_261 line 2683
462. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_262 line 2687
463. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_263 line 2691
464. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_264 line 2695
465. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_265 line 2699
466. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_266 line 2703
467. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_267 line 2707
468. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_268 line 2711
469. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_269 line 2715
470. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_270 line 2719
471. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_271 line 2723
472. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_272 line 2727
473. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_273 line 2731
474. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_274 line 2735
475. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_275 line 2739
476. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_276 line 2743
477. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_277 line 2747
478. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_278 line 2751
479. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_279 line 2755
480. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_280 line 2759
481. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_281 line 2763
482. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_282 line 2767
483. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_283 line 2771
484. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_284 line 2775
485. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_285 line 2779
486. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_286 line 2783
487. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_287 line 2787
488. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_288 line 2791
489. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_289 line 2795
490. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_290 line 2799
491. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_291 line 2803
492. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_292 line 2807
493. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_293 line 2811
494. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_294 line 2815
495. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_295 line 2819
496. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_296 line 2823
497. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_297 line 2827
498. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_298 line 2831
499. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_299 line 2835
500. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_300 line 2839
501. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_301 line 2843
502. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_302 line 2847
503. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_303 line 2851
504. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_304 line 2855
505. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_305 line 2859
506. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_306 line 2863
507. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_307 line 2867
508. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_308 line 2871
509. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_309 line 2875
510. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_310 line 2879
511. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_311 line 2883
512. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_312 line 2887
513. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_313 line 2891
514. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_314 line 2895
515. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_315 line 2899
516. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_316 line 2903
517. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_317 line 2907
518. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_318 line 2911
519. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_319 line 2915
520. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_320 line 2919
521. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_321 line 2923
522. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_322 line 2927
523. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_323 line 2931
524. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_324 line 2935
525. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_325 line 2939
526. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_326 line 2943
527. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_327 line 2947
528. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_328 line 2951
529. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_329 line 2955
530. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_330 line 2959
531. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_331 line 2963
532. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_332 line 2967
533. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_333 line 2971
534. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_334 line 2975
535. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_335 line 2979
536. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_336 line 2983
537. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_337 line 2987
538. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_338 line 2991
539. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_339 line 2995
540. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_340 line 2999
541. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_341 line 3003
542. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_342 line 3007
543. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_343 line 3011
544. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_344 line 3015
545. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_345 line 3019
546. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_346 line 3023
547. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_347 line 3027
548. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_348 line 3031
549. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_349 line 3035
550. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_350 line 3039
551. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_351 line 3043
552. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_352 line 3047
553. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_353 line 3051
554. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_354 line 3055
555. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_355 line 3059
556. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_356 line 3063
557. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_357 line 3067
558. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_358 line 3071
559. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_359 line 3075
560. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_360 line 3079
561. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_361 line 3083
562. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_362 line 3087
563. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_363 line 3091
564. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_364 line 3095
565. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_365 line 3099
566. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_366 line 3103
567. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_367 line 3107
568. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_368 line 3111
569. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_369 line 3115
570. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_370 line 3119
571. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete_371 line 3123
572. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_valid line 3127
573. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_index_inverse line 3130
574. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_valid line 3132
575. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_edges_valid line 3138
576. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_index_inverse line 3143
577. theorem OAI.EilenbergGanea.SeedChainCertificate.edge_complete line 3145
578. theorem OAI.EilenbergGanea.SeedChainCertificate.triangle_complete line 3251
579. def OAI.EilenbergGanea.SeedChainCertificate.rankIndex line 3628
580. theorem OAI.EilenbergGanea.SeedChainCertificate.sorted_adj_rank line 3629
581. def OAI.EilenbergGanea.SeedChainCertificate.graph line 3635
582. theorem OAI.EilenbergGanea.SeedChainCertificate.graph_adj line 3636
583. theorem OAI.EilenbergGanea.SeedChainCertificate.valid_pair_iff line 3639
584. theorem OAI.EilenbergGanea.SeedChainCertificate.valid_triple_iff line 3641
585. theorem OAI.EilenbergGanea.SeedChainCertificate.valid_length_le line 3651
586. def OAI.EilenbergGanea.SeedChainCertificate.indices line 3662