OAI/Topology/EilenbergGanea/SeedContraction.lean

GitHub source file

937 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.EilenbergGanea.SeedChainCertificate.d1Data_0 line 11
2. def OAI.EilenbergGanea.SeedChainCertificate.d1Data_1 line 29
3. def OAI.EilenbergGanea.SeedChainCertificate.d1Data_2 line 47
4. def OAI.EilenbergGanea.SeedChainCertificate.d1Data_3 line 65
5. def OAI.EilenbergGanea.SeedChainCertificate.d1Data_4 line 83
6. def OAI.EilenbergGanea.SeedChainCertificate.d1Data_5 line 101
7. def OAI.EilenbergGanea.SeedChainCertificate.d1Data_6 line 119
8. def OAI.EilenbergGanea.SeedChainCertificate.d1Data line 128
9. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_0 line 130
10. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_1 line 148
11. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_2 line 166
12. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_3 line 184
13. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_4 line 202
14. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_5 line 220
15. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_6 line 238
16. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_7 line 256
17. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_8 line 274
18. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_9 line 292
19. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_10 line 310
20. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_11 line 328
21. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_12 line 346
22. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_13 line 364
23. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_14 line 382
24. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_15 line 400
25. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_16 line 418
26. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_17 line 436
27. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_18 line 454
28. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_19 line 472
29. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_20 line 490
30. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_21 line 508
31. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_22 line 526
32. def OAI.EilenbergGanea.SeedChainCertificate.d2Data_23 line 544
33. def OAI.EilenbergGanea.SeedChainCertificate.d2Data line 550
34. def OAI.EilenbergGanea.SeedChainCertificate.h0CodeData_0 line 552
35. def OAI.EilenbergGanea.SeedChainCertificate.h0CodeData_1 line 570
36. def OAI.EilenbergGanea.SeedChainCertificate.h0CodeData_2 line 588
37. def OAI.EilenbergGanea.SeedChainCertificate.h0CodeData_3 line 606
38. def OAI.EilenbergGanea.SeedChainCertificate.h0CodeData_4 line 624
39. def OAI.EilenbergGanea.SeedChainCertificate.h0CodeData_5 line 642
40. def OAI.EilenbergGanea.SeedChainCertificate.h0CodeData_6 line 660
41. def OAI.EilenbergGanea.SeedChainCertificate.h0CodeData line 669
42. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_0 line 671
43. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_1 line 689
44. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_2 line 707
45. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_3 line 725
46. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_4 line 743
47. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_5 line 761
48. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_6 line 779
49. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_7 line 797
50. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_8 line 815
51. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_9 line 833
52. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_10 line 851
53. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_11 line 869
54. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_12 line 887
55. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_13 line 905
56. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_14 line 923
57. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_15 line 941
58. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_16 line 959
59. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_17 line 977
60. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_18 line 995
61. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_19 line 1013
62. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_20 line 1031
63. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_21 line 1049
64. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_22 line 1067
65. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData_23 line 1085
66. def OAI.EilenbergGanea.SeedChainCertificate.h1CodeData line 1091
67. def OAI.EilenbergGanea.SeedChainCertificate.d1Row line 1093
68. def OAI.EilenbergGanea.SeedChainCertificate.d2Row line 1094
69. def OAI.EilenbergGanea.SeedChainCertificate.h0Coeff line 1095
70. def OAI.EilenbergGanea.SeedChainCertificate.h1Coeff line 1097
71. def OAI.EilenbergGanea.SeedChainCertificate.rowEval line 1100
72. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_0 line 1103
73. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_1 line 1107
74. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_2 line 1111
75. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_3 line 1115
76. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_4 line 1119
77. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_5 line 1123
78. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_6 line 1127
79. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_7 line 1131
80. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_8 line 1135
81. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_9 line 1139
82. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_10 line 1143
83. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_11 line 1147
84. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_12 line 1151
85. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_13 line 1155
86. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_14 line 1159
87. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_15 line 1163
88. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_16 line 1167
89. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_17 line 1171
90. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_18 line 1175
91. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_19 line 1179
92. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_20 line 1183
93. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_21 line 1187
94. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_22 line 1191
95. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_23 line 1195
96. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_24 line 1199
97. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_25 line 1203
98. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_26 line 1207
99. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_27 line 1211
100. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_28 line 1215
101. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_29 line 1219
102. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_30 line 1223
103. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_31 line 1227
104. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_32 line 1231
105. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_33 line 1235
106. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_34 line 1239
107. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_35 line 1243
108. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_36 line 1247
109. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_37 line 1251
110. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_38 line 1255
111. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_39 line 1259
112. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_40 line 1263
113. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_41 line 1267
114. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_42 line 1271
115. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_43 line 1275
116. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_44 line 1279
117. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_45 line 1283
118. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_46 line 1287
119. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_47 line 1291
120. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_48 line 1295
121. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_49 line 1299
122. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_50 line 1303
123. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_51 line 1307
124. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_52 line 1311
125. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_53 line 1315
126. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_54 line 1319
127. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_55 line 1323
128. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_56 line 1327
129. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_57 line 1331
130. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_58 line 1335
131. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_59 line 1339
132. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_60 line 1343
133. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_61 line 1347
134. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_62 line 1351
135. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_63 line 1355
136. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_64 line 1359
137. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_65 line 1363
138. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_66 line 1367
139. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_67 line 1371
140. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_68 line 1375
141. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_69 line 1379
142. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_70 line 1383
143. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_71 line 1387
144. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_72 line 1391
145. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_73 line 1395
146. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_74 line 1399
147. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_75 line 1403
148. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_76 line 1407
149. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_77 line 1411
150. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_78 line 1415
151. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_79 line 1419
152. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_80 line 1423
153. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_81 line 1427
154. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_82 line 1431
155. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_83 line 1435
156. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_84 line 1439
157. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_85 line 1443
158. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_86 line 1447
159. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_87 line 1451
160. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_88 line 1455
161. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_89 line 1459
162. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_90 line 1463
163. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_91 line 1467
164. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_92 line 1471
165. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_93 line 1475
166. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_94 line 1479
167. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_95 line 1483
168. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_96 line 1487
169. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_97 line 1491
170. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_98 line 1495
171. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_99 line 1499
172. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_100 line 1503
173. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_101 line 1507
174. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_102 line 1511
175. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_103 line 1515
176. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_104 line 1519
177. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_105 line 1523
178. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_106 line 1527
179. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_107 line 1531
180. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_108 line 1535
181. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_109 line 1539
182. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_110 line 1543
183. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_111 line 1547
184. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_112 line 1551
185. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_113 line 1555
186. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_114 line 1559
187. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_115 line 1563
188. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_116 line 1567
189. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_117 line 1571
190. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_118 line 1575
191. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_119 line 1579
192. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_120 line 1583
193. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_121 line 1587
194. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_122 line 1591
195. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_123 line 1595
196. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_124 line 1599
197. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_125 line 1603
198. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_126 line 1607
199. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_127 line 1611
200. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_128 line 1615
201. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_129 line 1619
202. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_130 line 1623
203. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_131 line 1627
204. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_132 line 1631
205. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_133 line 1635
206. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_134 line 1639
207. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_135 line 1643
208. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_136 line 1647
209. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_137 line 1651
210. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_138 line 1655
211. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_139 line 1659
212. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_140 line 1663
213. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_141 line 1667
214. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_142 line 1671
215. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_143 line 1675
216. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_144 line 1679
217. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_145 line 1683
218. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_146 line 1687
219. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_147 line 1691
220. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_148 line 1695
221. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_149 line 1699
222. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_150 line 1703
223. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_151 line 1707
224. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_152 line 1711
225. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_153 line 1715
226. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_154 line 1719
227. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_155 line 1723
228. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_156 line 1727
229. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_157 line 1731
230. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_158 line 1735
231. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_159 line 1739
232. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_160 line 1743
233. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_161 line 1747
234. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_162 line 1751
235. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_163 line 1755
236. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_164 line 1759
237. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_165 line 1763
238. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_166 line 1767
239. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_167 line 1771
240. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_168 line 1775
241. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_169 line 1779
242. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_170 line 1783
243. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_171 line 1787
244. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_172 line 1791
245. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_173 line 1795
246. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_174 line 1799
247. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_175 line 1803
248. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_176 line 1807
249. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_177 line 1811
250. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_178 line 1815
251. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_179 line 1819
252. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_180 line 1823
253. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_181 line 1827
254. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_182 line 1831
255. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_183 line 1835
256. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_184 line 1839
257. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_185 line 1843
258. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_186 line 1847
259. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_187 line 1851
260. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_188 line 1855
261. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_189 line 1859
262. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_190 line 1863
263. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_191 line 1867
264. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_192 line 1871
265. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_193 line 1875
266. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_194 line 1879
267. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_195 line 1883
268. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_196 line 1887
269. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_197 line 1891
270. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_198 line 1895
271. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_199 line 1899
272. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_200 line 1903
273. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_201 line 1907
274. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_202 line 1911
275. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_203 line 1915
276. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_204 line 1919
277. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_205 line 1923
278. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_206 line 1927
279. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_207 line 1931
280. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_208 line 1935
281. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_209 line 1939
282. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_210 line 1943
283. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_211 line 1947
284. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_212 line 1951
285. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_213 line 1955
286. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_214 line 1959
287. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_215 line 1963
288. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_216 line 1967
289. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_217 line 1971
290. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_218 line 1975
291. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_219 line 1979
292. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_220 line 1983
293. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_221 line 1987
294. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_222 line 1991
295. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_223 line 1995
296. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_224 line 1999
297. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_225 line 2003
298. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_226 line 2007
299. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_227 line 2011
300. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_228 line 2015
301. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_229 line 2019
302. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_230 line 2023
303. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_231 line 2027
304. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_232 line 2031
305. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_233 line 2035
306. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_234 line 2039
307. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_235 line 2043
308. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_236 line 2047
309. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_237 line 2051
310. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_238 line 2055
311. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_239 line 2059
312. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_240 line 2063
313. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_241 line 2067
314. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_242 line 2071
315. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_243 line 2075
316. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_244 line 2079
317. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_245 line 2083
318. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_246 line 2087
319. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_247 line 2091
320. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_248 line 2095
321. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_249 line 2099
322. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_250 line 2103
323. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_251 line 2107
324. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_252 line 2111
325. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_253 line 2115
326. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_254 line 2119
327. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_255 line 2123
328. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_256 line 2127
329. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_257 line 2131
330. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_258 line 2135
331. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_259 line 2139
332. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_260 line 2143
333. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_261 line 2147
334. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_262 line 2151
335. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_263 line 2155
336. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_264 line 2159
337. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_265 line 2163
338. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_266 line 2167
339. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_267 line 2171
340. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_268 line 2175
341. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert_269 line 2179
342. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_0 line 2183
343. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_1 line 2188
344. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_2 line 2193
345. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_3 line 2198
346. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_4 line 2203
347. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_5 line 2208
348. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_6 line 2213
349. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_7 line 2218
350. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_8 line 2223
351. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_9 line 2228
352. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_10 line 2233
353. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_11 line 2238
354. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_12 line 2243
355. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_13 line 2248
356. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_14 line 2253
357. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_15 line 2258
358. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_16 line 2263
359. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_17 line 2268
360. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_18 line 2273
361. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_19 line 2278
362. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_20 line 2283
363. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_21 line 2288
364. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_22 line 2293
365. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_23 line 2298
366. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_24 line 2303
367. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_25 line 2308
368. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_26 line 2313
369. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_27 line 2318
370. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_28 line 2323
371. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_29 line 2328
372. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_30 line 2333
373. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_31 line 2338
374. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_32 line 2343
375. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_33 line 2348
376. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_34 line 2353
377. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_35 line 2358
378. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_36 line 2363
379. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_37 line 2368
380. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_38 line 2373
381. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_39 line 2378
382. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_40 line 2383
383. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_41 line 2388
384. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_42 line 2393
385. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_43 line 2398
386. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_44 line 2403
387. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_45 line 2408
388. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_46 line 2413
389. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_47 line 2418
390. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_48 line 2423
391. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_49 line 2428
392. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_50 line 2433
393. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_51 line 2438
394. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_52 line 2443
395. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_53 line 2448
396. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_54 line 2453
397. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_55 line 2458
398. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_56 line 2463
399. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_57 line 2468
400. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_58 line 2473
401. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_59 line 2478
402. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_60 line 2483
403. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_61 line 2488
404. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_62 line 2493
405. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_63 line 2498
406. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_64 line 2503
407. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_65 line 2508
408. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_66 line 2513
409. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_67 line 2518
410. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_68 line 2523
411. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_69 line 2528
412. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_70 line 2533
413. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_71 line 2538
414. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_72 line 2543
415. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_73 line 2548
416. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_74 line 2553
417. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_75 line 2558
418. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_76 line 2563
419. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_77 line 2568
420. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_78 line 2573
421. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_79 line 2578
422. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_80 line 2583
423. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_81 line 2588
424. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_82 line 2593
425. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_83 line 2598
426. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_84 line 2603
427. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_85 line 2608
428. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_86 line 2613
429. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_87 line 2618
430. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_88 line 2623
431. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_89 line 2628
432. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_90 line 2633
433. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_91 line 2638
434. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_92 line 2643
435. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_93 line 2648
436. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_94 line 2653
437. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_95 line 2658
438. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_96 line 2663
439. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_97 line 2668
440. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_98 line 2673
441. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_99 line 2678
442. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_100 line 2683
443. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_101 line 2688
444. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert_102 line 2693
445. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_0 line 2698
446. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_1 line 2704
447. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_2 line 2710
448. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_3 line 2716
449. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_4 line 2722
450. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_5 line 2728
451. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_6 line 2734
452. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_7 line 2740
453. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_8 line 2746
454. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_9 line 2752
455. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_10 line 2758
456. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_11 line 2764
457. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_12 line 2770
458. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_13 line 2776
459. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_14 line 2782
460. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_15 line 2788
461. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_16 line 2794
462. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_17 line 2800
463. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_18 line 2806
464. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_19 line 2812
465. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_20 line 2818
466. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_21 line 2824
467. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_22 line 2830
468. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_23 line 2836
469. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_24 line 2842
470. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_25 line 2848
471. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_26 line 2854
472. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_27 line 2860
473. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_28 line 2866
474. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_29 line 2872
475. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_30 line 2878
476. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_31 line 2884
477. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_32 line 2890
478. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_33 line 2896
479. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_34 line 2902
480. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_35 line 2908
481. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_36 line 2914
482. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_37 line 2920
483. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_38 line 2926
484. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_39 line 2932
485. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_40 line 2938
486. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_41 line 2944
487. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_42 line 2950
488. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_43 line 2956
489. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_44 line 2962
490. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_45 line 2968
491. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_46 line 2974
492. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_47 line 2980
493. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_48 line 2986
494. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_49 line 2992
495. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_50 line 2998
496. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_51 line 3004
497. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_52 line 3010
498. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_53 line 3016
499. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_54 line 3022
500. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_55 line 3028
501. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_56 line 3034
502. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_57 line 3040
503. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_58 line 3046
504. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_59 line 3052
505. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_60 line 3058
506. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_61 line 3064
507. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_62 line 3070
508. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_63 line 3076
509. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_64 line 3082
510. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_65 line 3088
511. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_66 line 3094
512. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_67 line 3100
513. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_68 line 3106
514. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_69 line 3112
515. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_70 line 3118
516. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_71 line 3124
517. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_72 line 3130
518. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_73 line 3136
519. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_74 line 3142
520. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_75 line 3148
521. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_76 line 3154
522. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_77 line 3160
523. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_78 line 3166
524. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_79 line 3172
525. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_80 line 3178
526. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_81 line 3184
527. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_82 line 3190
528. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_83 line 3196
529. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_84 line 3202
530. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_85 line 3208
531. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_86 line 3214
532. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_87 line 3220
533. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_88 line 3226
534. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_89 line 3232
535. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_90 line 3238
536. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_91 line 3244
537. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_92 line 3250
538. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_93 line 3256
539. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_94 line 3262
540. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_95 line 3268
541. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_96 line 3274
542. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_97 line 3280
543. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_98 line 3286
544. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_99 line 3292
545. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_100 line 3298
546. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_101 line 3304
547. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_102 line 3310
548. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_103 line 3316
549. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_104 line 3322
550. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_105 line 3328
551. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_106 line 3334
552. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_107 line 3340
553. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_108 line 3346
554. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_109 line 3352
555. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_110 line 3358
556. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_111 line 3364
557. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_112 line 3370
558. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_113 line 3376
559. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_114 line 3382
560. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_115 line 3388
561. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_116 line 3394
562. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_117 line 3400
563. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_118 line 3406
564. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_119 line 3412
565. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_120 line 3418
566. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_121 line 3424
567. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_122 line 3430
568. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_123 line 3436
569. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_124 line 3442
570. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_125 line 3448
571. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_126 line 3454
572. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_127 line 3460
573. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_128 line 3466
574. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_129 line 3472
575. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_130 line 3478
576. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_131 line 3484
577. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_132 line 3490
578. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_133 line 3496
579. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_134 line 3502
580. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_135 line 3508
581. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_136 line 3514
582. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_137 line 3520
583. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_138 line 3526
584. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_139 line 3532
585. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_140 line 3538
586. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_141 line 3544
587. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_142 line 3550
588. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_143 line 3556
589. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_144 line 3562
590. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_145 line 3568
591. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_146 line 3574
592. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_147 line 3580
593. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_148 line 3586
594. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_149 line 3592
595. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_150 line 3598
596. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_151 line 3604
597. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_152 line 3610
598. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_153 line 3616
599. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_154 line 3622
600. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_155 line 3628
601. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_156 line 3634
602. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_157 line 3640
603. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_158 line 3646
604. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_159 line 3652
605. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_160 line 3658
606. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_161 line 3664
607. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_162 line 3670
608. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_163 line 3676
609. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_164 line 3682
610. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_165 line 3688
611. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_166 line 3694
612. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_167 line 3700
613. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_168 line 3706
614. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_169 line 3712
615. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_170 line 3718
616. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_171 line 3724
617. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_172 line 3730
618. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_173 line 3736
619. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_174 line 3742
620. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_175 line 3748
621. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_176 line 3754
622. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_177 line 3760
623. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_178 line 3766
624. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_179 line 3772
625. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_180 line 3778
626. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_181 line 3784
627. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_182 line 3790
628. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_183 line 3796
629. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_184 line 3802
630. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_185 line 3808
631. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_186 line 3814
632. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_187 line 3820
633. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_188 line 3826
634. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_189 line 3832
635. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_190 line 3838
636. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_191 line 3844
637. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_192 line 3850
638. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_193 line 3856
639. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_194 line 3862
640. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_195 line 3868
641. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_196 line 3874
642. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_197 line 3880
643. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_198 line 3886
644. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_199 line 3892
645. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_200 line 3898
646. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_201 line 3904
647. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_202 line 3910
648. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_203 line 3916
649. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_204 line 3922
650. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_205 line 3928
651. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_206 line 3934
652. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_207 line 3940
653. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_208 line 3946
654. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_209 line 3952
655. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_210 line 3958
656. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_211 line 3964
657. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_212 line 3970
658. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_213 line 3976
659. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_214 line 3982
660. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_215 line 3988
661. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_216 line 3994
662. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_217 line 4000
663. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_218 line 4006
664. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_219 line 4012
665. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_220 line 4018
666. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_221 line 4024
667. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_222 line 4030
668. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_223 line 4036
669. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_224 line 4042
670. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_225 line 4048
671. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_226 line 4054
672. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_227 line 4060
673. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_228 line 4066
674. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_229 line 4072
675. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_230 line 4078
676. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_231 line 4084
677. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_232 line 4090
678. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_233 line 4096
679. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_234 line 4102
680. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_235 line 4108
681. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_236 line 4114
682. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_237 line 4120
683. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_238 line 4126
684. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_239 line 4132
685. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_240 line 4138
686. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_241 line 4144
687. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_242 line 4150
688. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_243 line 4156
689. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_244 line 4162
690. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_245 line 4168
691. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_246 line 4174
692. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_247 line 4180
693. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_248 line 4186
694. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_249 line 4192
695. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_250 line 4198
696. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_251 line 4204
697. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_252 line 4210
698. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_253 line 4216
699. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_254 line 4222
700. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_255 line 4228
701. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_256 line 4234
702. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_257 line 4240
703. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_258 line 4246
704. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_259 line 4252
705. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_260 line 4258
706. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_261 line 4264
707. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_262 line 4270
708. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_263 line 4276
709. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_264 line 4282
710. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_265 line 4288
711. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_266 line 4294
712. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_267 line 4300
713. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_268 line 4306
714. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_269 line 4312
715. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_270 line 4318
716. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_271 line 4324
717. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_272 line 4330
718. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_273 line 4336
719. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_274 line 4342
720. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_275 line 4348
721. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_276 line 4354
722. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_277 line 4360
723. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_278 line 4366
724. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_279 line 4372
725. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_280 line 4378
726. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_281 line 4384
727. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_282 line 4390
728. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_283 line 4396
729. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_284 line 4402
730. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_285 line 4408
731. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_286 line 4414
732. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_287 line 4420
733. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_288 line 4426
734. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_289 line 4432
735. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_290 line 4438
736. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_291 line 4444
737. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_292 line 4450
738. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_293 line 4456
739. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_294 line 4462
740. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_295 line 4468
741. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_296 line 4474
742. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_297 line 4480
743. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_298 line 4486
744. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_299 line 4492
745. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_300 line 4498
746. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_301 line 4504
747. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_302 line 4510
748. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_303 line 4516
749. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_304 line 4522
750. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_305 line 4528
751. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_306 line 4534
752. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_307 line 4540
753. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_308 line 4546
754. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_309 line 4552
755. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_310 line 4558
756. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_311 line 4564
757. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_312 line 4570
758. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_313 line 4576
759. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_314 line 4582
760. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_315 line 4588
761. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_316 line 4594
762. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_317 line 4600
763. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_318 line 4606
764. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_319 line 4612
765. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_320 line 4618
766. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_321 line 4624
767. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_322 line 4630
768. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_323 line 4636
769. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_324 line 4642
770. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_325 line 4648
771. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_326 line 4654
772. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_327 line 4660
773. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_328 line 4666
774. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_329 line 4672
775. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_330 line 4678
776. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_331 line 4684
777. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_332 line 4690
778. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_333 line 4696
779. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_334 line 4702
780. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_335 line 4708
781. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_336 line 4714
782. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_337 line 4720
783. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_338 line 4726
784. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_339 line 4732
785. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_340 line 4738
786. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_341 line 4744
787. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_342 line 4750
788. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_343 line 4756
789. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_344 line 4762
790. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_345 line 4768
791. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_346 line 4774
792. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_347 line 4780
793. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_348 line 4786
794. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_349 line 4792
795. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_350 line 4798
796. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_351 line 4804
797. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_352 line 4810
798. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_353 line 4816
799. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_354 line 4822
800. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_355 line 4828
801. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_356 line 4834
802. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_357 line 4840
803. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_358 line 4846
804. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_359 line 4852
805. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_360 line 4858
806. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_361 line 4864
807. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_362 line 4870
808. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_363 line 4876
809. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_364 line 4882
810. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_365 line 4888
811. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_366 line 4894
812. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_367 line 4900
813. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_368 line 4906
814. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_369 line 4912
815. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_370 line 4918
816. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert_371 line 4924
817. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_0 line 4930
818. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_1 line 4934
819. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_2 line 4938
820. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_3 line 4942
821. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_4 line 4946
822. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_5 line 4950
823. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_6 line 4954
824. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_7 line 4958
825. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_8 line 4962
826. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_9 line 4966
827. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_10 line 4970
828. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_11 line 4974
829. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_12 line 4978
830. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_13 line 4982
831. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_14 line 4986
832. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_15 line 4990
833. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_16 line 4994
834. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_17 line 4998
835. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_18 line 5002
836. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_19 line 5006
837. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_20 line 5010
838. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_21 line 5014
839. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_22 line 5018
840. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_23 line 5022
841. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_24 line 5026
842. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_25 line 5030
843. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_26 line 5034
844. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_27 line 5038
845. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_28 line 5042
846. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_29 line 5046
847. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_30 line 5050
848. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_31 line 5054
849. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_32 line 5058
850. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_33 line 5062
851. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_34 line 5066
852. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_35 line 5070
853. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_36 line 5074
854. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_37 line 5078
855. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_38 line 5082
856. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_39 line 5086
857. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_40 line 5090
858. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_41 line 5094
859. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_42 line 5098
860. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_43 line 5102
861. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_44 line 5106
862. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_45 line 5110
863. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_46 line 5114
864. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_47 line 5118
865. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_48 line 5122
866. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_49 line 5126
867. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_50 line 5130
868. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_51 line 5134
869. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_52 line 5138
870. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_53 line 5142
871. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_54 line 5146
872. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_55 line 5150
873. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_56 line 5154
874. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_57 line 5158
875. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_58 line 5162
876. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_59 line 5166
877. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_60 line 5170
878. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_61 line 5174
879. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_62 line 5178
880. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_63 line 5182
881. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_64 line 5186
882. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_65 line 5190
883. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_66 line 5194
884. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_67 line 5198
885. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_68 line 5202
886. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_69 line 5206
887. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_70 line 5210
888. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_71 line 5214
889. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_72 line 5218
890. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_73 line 5222
891. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_74 line 5226
892. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_75 line 5230
893. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_76 line 5234
894. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_77 line 5238
895. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_78 line 5242
896. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_79 line 5246
897. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_80 line 5250
898. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_81 line 5254
899. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_82 line 5258
900. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_83 line 5262
901. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_84 line 5266
902. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_85 line 5270
903. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_86 line 5274
904. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_87 line 5278
905. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_88 line 5282
906. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_89 line 5286
907. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_90 line 5290
908. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_91 line 5294
909. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_92 line 5298
910. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_93 line 5302
911. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_94 line 5306
912. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_95 line 5310
913. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_96 line 5314
914. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_97 line 5318
915. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_98 line 5322
916. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_99 line 5326
917. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_100 line 5330
918. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_101 line 5334
919. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert_102 line 5338
920. theorem OAI.EilenbergGanea.SeedChainCertificate.h1_boundary_cert line 5342
921. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_basis_cert line 5617
922. theorem OAI.EilenbergGanea.SeedChainCertificate.d2_basis_cert line 5725
923. theorem OAI.EilenbergGanea.SeedChainCertificate.d1_h0_cert line 6103
924. theorem OAI.EilenbergGanea.SeedChainCertificate.fin_ite line 6211
925. def OAI.EilenbergGanea.SeedChainCertificate.d₁ line 6220
926. def OAI.EilenbergGanea.SeedChainCertificate.d₂ line 6221
927. def OAI.EilenbergGanea.SeedChainCertificate.h₀ line 6222
928. def OAI.EilenbergGanea.SeedChainCertificate.h₁ line 6223
929. def OAI.EilenbergGanea.SeedChainCertificate.h₁' line 6224
930. theorem OAI.EilenbergGanea.SeedChainCertificate.d₁_single line 6226
931. theorem OAI.EilenbergGanea.SeedChainCertificate.d₂_single line 6233
932. theorem OAI.EilenbergGanea.SeedChainCertificate.bottom_identity line 6241
933. theorem OAI.EilenbergGanea.SeedChainCertificate.left_identity line 6247
934. theorem OAI.EilenbergGanea.SeedChainCertificate.d₁_d₂_single line 6253
935. theorem OAI.EilenbergGanea.SeedChainCertificate.corrected_identities line 6260
936. theorem OAI.EilenbergGanea.SeedChainCertificate.fin_single line 6266
937. def OAI.EilenbergGanea.SeedChainCertificate.contraction line 6275

     Source documentation

     An augmented integral chain contraction of the actual103-vertex source cell-order complex, not an assumed homology property of the seed.

     noncomputable def contraction : SimplicialChains.Contraction graph :=
     …

     Mentions: OAI.SimplicialChains.Contraction, OAI.EilenbergGanea.SeedChainCertificate.graph