OAI/MathematicalPhysics/Transonic/Certificates/Jet23.lean

GitHub source file

753 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SepticProfile.ExteriorCertificates.C23.Q line 8
2. def OAI.SepticProfile.ExteriorCertificates.C23.sig line 9
3. def OAI.SepticProfile.ExteriorCertificates.C23.kap line 10
4. def OAI.SepticProfile.ExteriorCertificates.C23.s line 11
5. def OAI.SepticProfile.ExteriorCertificates.C23.rho line 12
6. def OAI.SepticProfile.ExteriorCertificates.C23.st line 13
7. def OAI.SepticProfile.ExteriorCertificates.C23.L0 line 14
8. def OAI.SepticProfile.ExteriorCertificates.C23.weights line 15
9. def OAI.SepticProfile.ExteriorCertificates.C23.bData line 16
10. def OAI.SepticProfile.ExteriorCertificates.C23.rData line 17
11. def OAI.SepticProfile.ExteriorCertificates.C23.scData line 18
12. def OAI.SepticProfile.ExteriorCertificates.C23.srData line 19
13. def OAI.SepticProfile.ExteriorCertificates.C23.numData line 20
14. def OAI.SepticProfile.ExteriorCertificates.C23.denData line 21
15. def OAI.SepticProfile.ExteriorCertificates.C23.relRow0 line 22
16. def OAI.SepticProfile.ExteriorCertificates.C23.relRow1 line 23
17. def OAI.SepticProfile.ExteriorCertificates.C23.relRow2 line 24
18. def OAI.SepticProfile.ExteriorCertificates.C23.relRow3 line 25
19. def OAI.SepticProfile.ExteriorCertificates.C23.relRow4 line 26
20. def OAI.SepticProfile.ExteriorCertificates.C23.relRow5 line 27
21. def OAI.SepticProfile.ExteriorCertificates.C23.relRow6 line 28
22. def OAI.SepticProfile.ExteriorCertificates.C23.relRow7 line 29
23. def OAI.SepticProfile.ExteriorCertificates.C23.relRow8 line 30
24. def OAI.SepticProfile.ExteriorCertificates.C23.relRow9 line 31
25. def OAI.SepticProfile.ExteriorCertificates.C23.relRow10 line 32
26. def OAI.SepticProfile.ExteriorCertificates.C23.relRow11 line 33
27. def OAI.SepticProfile.ExteriorCertificates.C23.relRow12 line 34
28. def OAI.SepticProfile.ExteriorCertificates.C23.relRow13 line 35
29. def OAI.SepticProfile.ExteriorCertificates.C23.relRow14 line 36
30. def OAI.SepticProfile.ExteriorCertificates.C23.relRow15 line 37
31. def OAI.SepticProfile.ExteriorCertificates.C23.relRow16 line 38
32. def OAI.SepticProfile.ExteriorCertificates.C23.relRow17 line 39
33. def OAI.SepticProfile.ExteriorCertificates.C23.relRow18 line 40
34. def OAI.SepticProfile.ExteriorCertificates.C23.relRow19 line 41
35. def OAI.SepticProfile.ExteriorCertificates.C23.relRow20 line 42
36. def OAI.SepticProfile.ExteriorCertificates.C23.relRow21 line 43
37. def OAI.SepticProfile.ExteriorCertificates.C23.relRow22 line 44
38. def OAI.SepticProfile.ExteriorCertificates.C23.relRow23 line 45
39. def OAI.SepticProfile.ExteriorCertificates.C23.relRow24 line 46
40. def OAI.SepticProfile.ExteriorCertificates.C23.relRow25 line 47
41. def OAI.SepticProfile.ExteriorCertificates.C23.relRow26 line 48
42. def OAI.SepticProfile.ExteriorCertificates.C23.relRow27 line 49
43. def OAI.SepticProfile.ExteriorCertificates.C23.relRow28 line 50
44. def OAI.SepticProfile.ExteriorCertificates.C23.relRow29 line 51
45. def OAI.SepticProfile.ExteriorCertificates.C23.relRow30 line 52
46. def OAI.SepticProfile.ExteriorCertificates.C23.relRow31 line 53
47. def OAI.SepticProfile.ExteriorCertificates.C23.relRow32 line 54
48. def OAI.SepticProfile.ExteriorCertificates.C23.relRow33 line 55
49. def OAI.SepticProfile.ExteriorCertificates.C23.relRow34 line 56
50. def OAI.SepticProfile.ExteriorCertificates.C23.relRow35 line 57
51. def OAI.SepticProfile.ExteriorCertificates.C23.relRow36 line 58
52. def OAI.SepticProfile.ExteriorCertificates.C23.relRow37 line 59
53. def OAI.SepticProfile.ExteriorCertificates.C23.relRow38 line 60
54. def OAI.SepticProfile.ExteriorCertificates.C23.relRow39 line 61
55. def OAI.SepticProfile.ExteriorCertificates.C23.relRow40 line 62
56. def OAI.SepticProfile.ExteriorCertificates.C23.relRow41 line 63
57. def OAI.SepticProfile.ExteriorCertificates.C23.relRow42 line 64
58. def OAI.SepticProfile.ExteriorCertificates.C23.relRow43 line 65
59. def OAI.SepticProfile.ExteriorCertificates.C23.relRow44 line 66
60. def OAI.SepticProfile.ExteriorCertificates.C23.relRow45 line 67
61. def OAI.SepticProfile.ExteriorCertificates.C23.relRow46 line 68
62. def OAI.SepticProfile.ExteriorCertificates.C23.relRow47 line 69
63. def OAI.SepticProfile.ExteriorCertificates.C23.relRow48 line 70
64. def OAI.SepticProfile.ExteriorCertificates.C23.relRow49 line 71
65. def OAI.SepticProfile.ExteriorCertificates.C23.relRow50 line 72
66. def OAI.SepticProfile.ExteriorCertificates.C23.relRow51 line 73
67. def OAI.SepticProfile.ExteriorCertificates.C23.relRow52 line 74
68. def OAI.SepticProfile.ExteriorCertificates.C23.relRow53 line 75
69. def OAI.SepticProfile.ExteriorCertificates.C23.relRow54 line 76
70. def OAI.SepticProfile.ExteriorCertificates.C23.relRow55 line 77
71. def OAI.SepticProfile.ExteriorCertificates.C23.relRow56 line 78
72. def OAI.SepticProfile.ExteriorCertificates.C23.relRow57 line 79
73. def OAI.SepticProfile.ExteriorCertificates.C23.relRow58 line 80
74. def OAI.SepticProfile.ExteriorCertificates.C23.relRow59 line 81
75. def OAI.SepticProfile.ExteriorCertificates.C23.relRow60 line 82
76. def OAI.SepticProfile.ExteriorCertificates.C23.relRow61 line 83
77. def OAI.SepticProfile.ExteriorCertificates.C23.relRow62 line 84
78. def OAI.SepticProfile.ExteriorCertificates.C23.relRow63 line 85
79. def OAI.SepticProfile.ExteriorCertificates.C23.relRow64 line 86
80. def OAI.SepticProfile.ExteriorCertificates.C23.relRow65 line 87
81. def OAI.SepticProfile.ExteriorCertificates.C23.relRow66 line 88
82. def OAI.SepticProfile.ExteriorCertificates.C23.relRow67 line 89
83. def OAI.SepticProfile.ExteriorCertificates.C23.relRow68 line 90
84. def OAI.SepticProfile.ExteriorCertificates.C23.relRow69 line 91
85. def OAI.SepticProfile.ExteriorCertificates.C23.relRow70 line 92
86. def OAI.SepticProfile.ExteriorCertificates.C23.relRow71 line 93
87. def OAI.SepticProfile.ExteriorCertificates.C23.relRow72 line 94
88. def OAI.SepticProfile.ExteriorCertificates.C23.relRow73 line 95
89. def OAI.SepticProfile.ExteriorCertificates.C23.relRow74 line 96
90. def OAI.SepticProfile.ExteriorCertificates.C23.relData line 97
91. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow0 line 98
92. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow1 line 99
93. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow2 line 100
94. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow3 line 101
95. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow4 line 102
96. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow5 line 103
97. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow6 line 104
98. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow7 line 105
99. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow8 line 106
100. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow9 line 107
101. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow10 line 108
102. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow11 line 109
103. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow12 line 110
104. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow13 line 111
105. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow14 line 112
106. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow15 line 113
107. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow16 line 114
108. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow17 line 115
109. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow18 line 116
110. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow19 line 117
111. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow20 line 118
112. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow21 line 119
113. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow22 line 120
114. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow23 line 121
115. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow24 line 122
116. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow25 line 123
117. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow26 line 124
118. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow27 line 125
119. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow28 line 126
120. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow29 line 127
121. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow30 line 128
122. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow31 line 129
123. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow32 line 130
124. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow33 line 131
125. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow34 line 132
126. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow35 line 133
127. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow36 line 134
128. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow37 line 135
129. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow38 line 136
130. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow39 line 137
131. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow40 line 138
132. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow41 line 139
133. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow42 line 140
134. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow43 line 141
135. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow44 line 142
136. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow45 line 143
137. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow46 line 144
138. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow47 line 145
139. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow48 line 146
140. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow49 line 147
141. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow50 line 148
142. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow51 line 149
143. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow52 line 150
144. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow53 line 151
145. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow54 line 152
146. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow55 line 153
147. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow56 line 154
148. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow57 line 155
149. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow58 line 156
150. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow59 line 157
151. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow60 line 158
152. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow61 line 159
153. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow62 line 160
154. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow63 line 161
155. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow64 line 162
156. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow65 line 163
157. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow66 line 164
158. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow67 line 165
159. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow68 line 166
160. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow69 line 167
161. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow70 line 168
162. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow71 line 169
163. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow72 line 170
164. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow73 line 171
165. def OAI.SepticProfile.ExteriorCertificates.C23.sqRow74 line 172
166. def OAI.SepticProfile.ExteriorCertificates.C23.sqData line 173
167. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow0 line 174
168. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow1 line 175
169. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow2 line 176
170. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow3 line 177
171. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow4 line 178
172. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow5 line 179
173. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow6 line 180
174. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow7 line 181
175. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow8 line 182
176. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow9 line 183
177. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow10 line 184
178. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow11 line 185
179. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow12 line 186
180. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow13 line 187
181. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow14 line 188
182. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow15 line 189
183. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow16 line 190
184. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow17 line 191
185. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow18 line 192
186. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow19 line 193
187. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow20 line 194
188. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow21 line 195
189. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow22 line 196
190. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow23 line 197
191. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow24 line 198
192. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow25 line 199
193. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow26 line 200
194. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow27 line 201
195. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow28 line 202
196. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow29 line 203
197. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow30 line 204
198. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow31 line 205
199. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow32 line 206
200. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow33 line 207
201. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow34 line 208
202. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow35 line 209
203. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow36 line 210
204. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow37 line 211
205. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow38 line 212
206. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow39 line 213
207. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow40 line 214
208. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow41 line 215
209. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow42 line 216
210. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow43 line 217
211. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow44 line 218
212. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow45 line 219
213. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow46 line 220
214. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow47 line 221
215. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow48 line 222
216. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow49 line 223
217. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow50 line 224
218. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow51 line 225
219. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow52 line 226
220. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow53 line 227
221. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow54 line 228
222. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow55 line 229
223. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow56 line 230
224. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow57 line 231
225. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow58 line 232
226. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow59 line 233
227. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow60 line 234
228. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow61 line 235
229. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow62 line 236
230. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow63 line 237
231. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow64 line 238
232. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow65 line 239
233. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow66 line 240
234. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow67 line 241
235. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow68 line 242
236. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow69 line 243
237. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow70 line 244
238. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow71 line 245
239. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow72 line 246
240. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow73 line 247
241. def OAI.SepticProfile.ExteriorCertificates.C23.cuRow74 line 248
242. def OAI.SepticProfile.ExteriorCertificates.C23.cuData line 249
243. def OAI.SepticProfile.ExteriorCertificates.C23.quRow0 line 250
244. def OAI.SepticProfile.ExteriorCertificates.C23.quRow1 line 251
245. def OAI.SepticProfile.ExteriorCertificates.C23.quRow2 line 252
246. def OAI.SepticProfile.ExteriorCertificates.C23.quRow3 line 253
247. def OAI.SepticProfile.ExteriorCertificates.C23.quRow4 line 254
248. def OAI.SepticProfile.ExteriorCertificates.C23.quRow5 line 255
249. def OAI.SepticProfile.ExteriorCertificates.C23.quRow6 line 256
250. def OAI.SepticProfile.ExteriorCertificates.C23.quRow7 line 257
251. def OAI.SepticProfile.ExteriorCertificates.C23.quRow8 line 258
252. def OAI.SepticProfile.ExteriorCertificates.C23.quRow9 line 259
253. def OAI.SepticProfile.ExteriorCertificates.C23.quRow10 line 260
254. def OAI.SepticProfile.ExteriorCertificates.C23.quRow11 line 261
255. def OAI.SepticProfile.ExteriorCertificates.C23.quRow12 line 262
256. def OAI.SepticProfile.ExteriorCertificates.C23.quRow13 line 263
257. def OAI.SepticProfile.ExteriorCertificates.C23.quRow14 line 264
258. def OAI.SepticProfile.ExteriorCertificates.C23.quRow15 line 265
259. def OAI.SepticProfile.ExteriorCertificates.C23.quRow16 line 266
260. def OAI.SepticProfile.ExteriorCertificates.C23.quRow17 line 267
261. def OAI.SepticProfile.ExteriorCertificates.C23.quRow18 line 268
262. def OAI.SepticProfile.ExteriorCertificates.C23.quRow19 line 269
263. def OAI.SepticProfile.ExteriorCertificates.C23.quRow20 line 270
264. def OAI.SepticProfile.ExteriorCertificates.C23.quRow21 line 271
265. def OAI.SepticProfile.ExteriorCertificates.C23.quRow22 line 272
266. def OAI.SepticProfile.ExteriorCertificates.C23.quRow23 line 273
267. def OAI.SepticProfile.ExteriorCertificates.C23.quRow24 line 274
268. def OAI.SepticProfile.ExteriorCertificates.C23.quRow25 line 275
269. def OAI.SepticProfile.ExteriorCertificates.C23.quRow26 line 276
270. def OAI.SepticProfile.ExteriorCertificates.C23.quRow27 line 277
271. def OAI.SepticProfile.ExteriorCertificates.C23.quRow28 line 278
272. def OAI.SepticProfile.ExteriorCertificates.C23.quRow29 line 279
273. def OAI.SepticProfile.ExteriorCertificates.C23.quRow30 line 280
274. def OAI.SepticProfile.ExteriorCertificates.C23.quRow31 line 281
275. def OAI.SepticProfile.ExteriorCertificates.C23.quRow32 line 282
276. def OAI.SepticProfile.ExteriorCertificates.C23.quRow33 line 283
277. def OAI.SepticProfile.ExteriorCertificates.C23.quRow34 line 284
278. def OAI.SepticProfile.ExteriorCertificates.C23.quRow35 line 285
279. def OAI.SepticProfile.ExteriorCertificates.C23.quRow36 line 286
280. def OAI.SepticProfile.ExteriorCertificates.C23.quRow37 line 287
281. def OAI.SepticProfile.ExteriorCertificates.C23.quRow38 line 288
282. def OAI.SepticProfile.ExteriorCertificates.C23.quRow39 line 289
283. def OAI.SepticProfile.ExteriorCertificates.C23.quRow40 line 290
284. def OAI.SepticProfile.ExteriorCertificates.C23.quRow41 line 291
285. def OAI.SepticProfile.ExteriorCertificates.C23.quRow42 line 292
286. def OAI.SepticProfile.ExteriorCertificates.C23.quRow43 line 293
287. def OAI.SepticProfile.ExteriorCertificates.C23.quRow44 line 294
288. def OAI.SepticProfile.ExteriorCertificates.C23.quRow45 line 295
289. def OAI.SepticProfile.ExteriorCertificates.C23.quRow46 line 296
290. def OAI.SepticProfile.ExteriorCertificates.C23.quRow47 line 297
291. def OAI.SepticProfile.ExteriorCertificates.C23.quRow48 line 298
292. def OAI.SepticProfile.ExteriorCertificates.C23.quRow49 line 299
293. def OAI.SepticProfile.ExteriorCertificates.C23.quRow50 line 300
294. def OAI.SepticProfile.ExteriorCertificates.C23.quRow51 line 301
295. def OAI.SepticProfile.ExteriorCertificates.C23.quRow52 line 302
296. def OAI.SepticProfile.ExteriorCertificates.C23.quRow53 line 303
297. def OAI.SepticProfile.ExteriorCertificates.C23.quRow54 line 304
298. def OAI.SepticProfile.ExteriorCertificates.C23.quRow55 line 305
299. def OAI.SepticProfile.ExteriorCertificates.C23.quRow56 line 306
300. def OAI.SepticProfile.ExteriorCertificates.C23.quRow57 line 307
301. def OAI.SepticProfile.ExteriorCertificates.C23.quRow58 line 308
302. def OAI.SepticProfile.ExteriorCertificates.C23.quRow59 line 309
303. def OAI.SepticProfile.ExteriorCertificates.C23.quRow60 line 310
304. def OAI.SepticProfile.ExteriorCertificates.C23.quRow61 line 311
305. def OAI.SepticProfile.ExteriorCertificates.C23.quRow62 line 312
306. def OAI.SepticProfile.ExteriorCertificates.C23.quRow63 line 313
307. def OAI.SepticProfile.ExteriorCertificates.C23.quRow64 line 314
308. def OAI.SepticProfile.ExteriorCertificates.C23.quRow65 line 315
309. def OAI.SepticProfile.ExteriorCertificates.C23.quRow66 line 316
310. def OAI.SepticProfile.ExteriorCertificates.C23.quRow67 line 317
311. def OAI.SepticProfile.ExteriorCertificates.C23.quRow68 line 318
312. def OAI.SepticProfile.ExteriorCertificates.C23.quRow69 line 319
313. def OAI.SepticProfile.ExteriorCertificates.C23.quRow70 line 320
314. def OAI.SepticProfile.ExteriorCertificates.C23.quRow71 line 321
315. def OAI.SepticProfile.ExteriorCertificates.C23.quRow72 line 322
316. def OAI.SepticProfile.ExteriorCertificates.C23.quRow73 line 323
317. def OAI.SepticProfile.ExteriorCertificates.C23.quRow74 line 324
318. def OAI.SepticProfile.ExteriorCertificates.C23.quData line 325
319. def OAI.SepticProfile.ExteriorCertificates.C23.trace line 326
320. theorem OAI.SepticProfile.ExteriorCertificates.C23.row2 line 337
321. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos2 line 347
322. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos2 line 348
323. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos2 line 349
324. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio2 line 350
325. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff2 line 351
326. theorem OAI.SepticProfile.ExteriorCertificates.C23.row3 line 352
327. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos3 line 362
328. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos3 line 363
329. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos3 line 364
330. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio3 line 365
331. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff3 line 366
332. theorem OAI.SepticProfile.ExteriorCertificates.C23.row4 line 367
333. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos4 line 377
334. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos4 line 378
335. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos4 line 379
336. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio4 line 380
337. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff4 line 381
338. theorem OAI.SepticProfile.ExteriorCertificates.C23.row5 line 382
339. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos5 line 392
340. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos5 line 393
341. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos5 line 394
342. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio5 line 395
343. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff5 line 396
344. theorem OAI.SepticProfile.ExteriorCertificates.C23.row6 line 397
345. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos6 line 407
346. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos6 line 408
347. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos6 line 409
348. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio6 line 410
349. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff6 line 411
350. theorem OAI.SepticProfile.ExteriorCertificates.C23.row7 line 412
351. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos7 line 422
352. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos7 line 423
353. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos7 line 424
354. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio7 line 425
355. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff7 line 426
356. theorem OAI.SepticProfile.ExteriorCertificates.C23.row8 line 427
357. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos8 line 437
358. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos8 line 438
359. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos8 line 439
360. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio8 line 440
361. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff8 line 441
362. theorem OAI.SepticProfile.ExteriorCertificates.C23.row9 line 442
363. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos9 line 452
364. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos9 line 453
365. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos9 line 454
366. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio9 line 455
367. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff9 line 456
368. theorem OAI.SepticProfile.ExteriorCertificates.C23.row10 line 457
369. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos10 line 467
370. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos10 line 468
371. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos10 line 469
372. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio10 line 470
373. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff10 line 471
374. theorem OAI.SepticProfile.ExteriorCertificates.C23.row11 line 472
375. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos11 line 482
376. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos11 line 483
377. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos11 line 484
378. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio11 line 485
379. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff11 line 486
380. theorem OAI.SepticProfile.ExteriorCertificates.C23.row12 line 487
381. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos12 line 497
382. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos12 line 498
383. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos12 line 499
384. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio12 line 500
385. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff12 line 501
386. theorem OAI.SepticProfile.ExteriorCertificates.C23.row13 line 502
387. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos13 line 512
388. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos13 line 513
389. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos13 line 514
390. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio13 line 515
391. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff13 line 516
392. theorem OAI.SepticProfile.ExteriorCertificates.C23.row14 line 517
393. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos14 line 527
394. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos14 line 528
395. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos14 line 529
396. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio14 line 530
397. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff14 line 531
398. theorem OAI.SepticProfile.ExteriorCertificates.C23.row15 line 532
399. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos15 line 542
400. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos15 line 543
401. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos15 line 544
402. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio15 line 545
403. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff15 line 546
404. theorem OAI.SepticProfile.ExteriorCertificates.C23.row16 line 547
405. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos16 line 557
406. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos16 line 558
407. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos16 line 559
408. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio16 line 560
409. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff16 line 561
410. theorem OAI.SepticProfile.ExteriorCertificates.C23.row17 line 562
411. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos17 line 572
412. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos17 line 573
413. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos17 line 574
414. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio17 line 575
415. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff17 line 576
416. theorem OAI.SepticProfile.ExteriorCertificates.C23.row18 line 577
417. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos18 line 587
418. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos18 line 588
419. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos18 line 589
420. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio18 line 590
421. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff18 line 591
422. theorem OAI.SepticProfile.ExteriorCertificates.C23.row19 line 592
423. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos19 line 602
424. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos19 line 603
425. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos19 line 604
426. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio19 line 605
427. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff19 line 606
428. theorem OAI.SepticProfile.ExteriorCertificates.C23.row20 line 607
429. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos20 line 617
430. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos20 line 618
431. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos20 line 619
432. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio20 line 620
433. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff20 line 621
434. theorem OAI.SepticProfile.ExteriorCertificates.C23.row21 line 622
435. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos21 line 632
436. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos21 line 633
437. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos21 line 634
438. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio21 line 635
439. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff21 line 636
440. theorem OAI.SepticProfile.ExteriorCertificates.C23.row22 line 637
441. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos22 line 647
442. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos22 line 648
443. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos22 line 649
444. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio22 line 650
445. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff22 line 651
446. theorem OAI.SepticProfile.ExteriorCertificates.C23.row23 line 652
447. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos23 line 662
448. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos23 line 663
449. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos23 line 664
450. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio23 line 665
451. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff23 line 666
452. theorem OAI.SepticProfile.ExteriorCertificates.C23.row24 line 667
453. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos24 line 677
454. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos24 line 678
455. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos24 line 679
456. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio24 line 680
457. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff24 line 681
458. theorem OAI.SepticProfile.ExteriorCertificates.C23.row25 line 682
459. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos25 line 692
460. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos25 line 693
461. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos25 line 694
462. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio25 line 695
463. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff25 line 696
464. theorem OAI.SepticProfile.ExteriorCertificates.C23.row26 line 697
465. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos26 line 707
466. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos26 line 708
467. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos26 line 709
468. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio26 line 710
469. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff26 line 711
470. theorem OAI.SepticProfile.ExteriorCertificates.C23.row27 line 712
471. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos27 line 722
472. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos27 line 723
473. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos27 line 724
474. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio27 line 725
475. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff27 line 726
476. theorem OAI.SepticProfile.ExteriorCertificates.C23.row28 line 727
477. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos28 line 737
478. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos28 line 738
479. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos28 line 739
480. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio28 line 740
481. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff28 line 741
482. theorem OAI.SepticProfile.ExteriorCertificates.C23.row29 line 742
483. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos29 line 752
484. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos29 line 753
485. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos29 line 754
486. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio29 line 755
487. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff29 line 756
488. theorem OAI.SepticProfile.ExteriorCertificates.C23.row30 line 757
489. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos30 line 767
490. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos30 line 768
491. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos30 line 769
492. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio30 line 770
493. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff30 line 771
494. theorem OAI.SepticProfile.ExteriorCertificates.C23.row31 line 772
495. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos31 line 782
496. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos31 line 783
497. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos31 line 784
498. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio31 line 785
499. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff31 line 786
500. theorem OAI.SepticProfile.ExteriorCertificates.C23.row32 line 787
501. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos32 line 797
502. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos32 line 798
503. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos32 line 799
504. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio32 line 800
505. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff32 line 801
506. theorem OAI.SepticProfile.ExteriorCertificates.C23.row33 line 802
507. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos33 line 812
508. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos33 line 813
509. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos33 line 814
510. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio33 line 815
511. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff33 line 816
512. theorem OAI.SepticProfile.ExteriorCertificates.C23.row34 line 817
513. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos34 line 827
514. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos34 line 828
515. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos34 line 829
516. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio34 line 830
517. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff34 line 831
518. theorem OAI.SepticProfile.ExteriorCertificates.C23.row35 line 832
519. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos35 line 842
520. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos35 line 843
521. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos35 line 844
522. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio35 line 845
523. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff35 line 846
524. theorem OAI.SepticProfile.ExteriorCertificates.C23.row36 line 847
525. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos36 line 857
526. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos36 line 858
527. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos36 line 859
528. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio36 line 860
529. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff36 line 861
530. theorem OAI.SepticProfile.ExteriorCertificates.C23.row37 line 862
531. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos37 line 872
532. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos37 line 873
533. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos37 line 874
534. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio37 line 875
535. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff37 line 876
536. theorem OAI.SepticProfile.ExteriorCertificates.C23.row38 line 877
537. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos38 line 887
538. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos38 line 888
539. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos38 line 889
540. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio38 line 890
541. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff38 line 891
542. theorem OAI.SepticProfile.ExteriorCertificates.C23.row39 line 892
543. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos39 line 902
544. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos39 line 903
545. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos39 line 904
546. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio39 line 905
547. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff39 line 906
548. theorem OAI.SepticProfile.ExteriorCertificates.C23.row40 line 907
549. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos40 line 917
550. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos40 line 918
551. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos40 line 919
552. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio40 line 920
553. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff40 line 921
554. theorem OAI.SepticProfile.ExteriorCertificates.C23.row41 line 922
555. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos41 line 932
556. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos41 line 933
557. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos41 line 934
558. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio41 line 935
559. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff41 line 936
560. theorem OAI.SepticProfile.ExteriorCertificates.C23.row42 line 937
561. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos42 line 947
562. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos42 line 948
563. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos42 line 949
564. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio42 line 950
565. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff42 line 951
566. theorem OAI.SepticProfile.ExteriorCertificates.C23.row43 line 952
567. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos43 line 962
568. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos43 line 963
569. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos43 line 964
570. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio43 line 965
571. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff43 line 966
572. theorem OAI.SepticProfile.ExteriorCertificates.C23.row44 line 967
573. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos44 line 977
574. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos44 line 978
575. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos44 line 979
576. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio44 line 980
577. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff44 line 981
578. theorem OAI.SepticProfile.ExteriorCertificates.C23.row45 line 982
579. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos45 line 992
580. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos45 line 993
581. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos45 line 994
582. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio45 line 995
583. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff45 line 996
584. theorem OAI.SepticProfile.ExteriorCertificates.C23.row46 line 997
585. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos46 line 1007
586. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos46 line 1008
587. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos46 line 1009
588. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio46 line 1010
589. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff46 line 1011
590. theorem OAI.SepticProfile.ExteriorCertificates.C23.row47 line 1012
591. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos47 line 1022
592. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos47 line 1023
593. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos47 line 1024
594. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio47 line 1025
595. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff47 line 1026
596. theorem OAI.SepticProfile.ExteriorCertificates.C23.row48 line 1027
597. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos48 line 1037
598. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos48 line 1038
599. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos48 line 1039
600. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio48 line 1040
601. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff48 line 1041
602. theorem OAI.SepticProfile.ExteriorCertificates.C23.row49 line 1042
603. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos49 line 1052
604. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos49 line 1053
605. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos49 line 1054
606. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio49 line 1055
607. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff49 line 1056
608. theorem OAI.SepticProfile.ExteriorCertificates.C23.row50 line 1057
609. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos50 line 1067
610. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos50 line 1068
611. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos50 line 1069
612. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio50 line 1070
613. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff50 line 1071
614. theorem OAI.SepticProfile.ExteriorCertificates.C23.row51 line 1072
615. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos51 line 1082
616. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos51 line 1083
617. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos51 line 1084
618. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio51 line 1085
619. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff51 line 1086
620. theorem OAI.SepticProfile.ExteriorCertificates.C23.row52 line 1087
621. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos52 line 1097
622. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos52 line 1098
623. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos52 line 1099
624. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio52 line 1100
625. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff52 line 1101
626. theorem OAI.SepticProfile.ExteriorCertificates.C23.row53 line 1102
627. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos53 line 1112
628. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos53 line 1113
629. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos53 line 1114
630. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio53 line 1115
631. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff53 line 1116
632. theorem OAI.SepticProfile.ExteriorCertificates.C23.row54 line 1117
633. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos54 line 1127
634. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos54 line 1128
635. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos54 line 1129
636. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio54 line 1130
637. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff54 line 1131
638. theorem OAI.SepticProfile.ExteriorCertificates.C23.row55 line 1132
639. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos55 line 1142
640. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos55 line 1143
641. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos55 line 1144
642. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio55 line 1145
643. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff55 line 1146
644. theorem OAI.SepticProfile.ExteriorCertificates.C23.row56 line 1147
645. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos56 line 1157
646. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos56 line 1158
647. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos56 line 1159
648. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio56 line 1160
649. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff56 line 1161
650. theorem OAI.SepticProfile.ExteriorCertificates.C23.row57 line 1162
651. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos57 line 1172
652. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos57 line 1173
653. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos57 line 1174
654. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio57 line 1175
655. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff57 line 1176
656. theorem OAI.SepticProfile.ExteriorCertificates.C23.row58 line 1177
657. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos58 line 1187
658. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos58 line 1188
659. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos58 line 1189
660. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio58 line 1190
661. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff58 line 1191
662. theorem OAI.SepticProfile.ExteriorCertificates.C23.row59 line 1192
663. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos59 line 1202
664. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos59 line 1203
665. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos59 line 1204
666. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio59 line 1205
667. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff59 line 1206
668. theorem OAI.SepticProfile.ExteriorCertificates.C23.row60 line 1207
669. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos60 line 1217
670. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos60 line 1218
671. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos60 line 1219
672. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio60 line 1220
673. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff60 line 1221
674. theorem OAI.SepticProfile.ExteriorCertificates.C23.row61 line 1222
675. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos61 line 1232
676. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos61 line 1233
677. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos61 line 1234
678. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio61 line 1235
679. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff61 line 1236
680. theorem OAI.SepticProfile.ExteriorCertificates.C23.row62 line 1237
681. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos62 line 1247
682. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos62 line 1248
683. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos62 line 1249
684. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio62 line 1250
685. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff62 line 1251
686. theorem OAI.SepticProfile.ExteriorCertificates.C23.row63 line 1252
687. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos63 line 1262
688. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos63 line 1263
689. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos63 line 1264
690. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio63 line 1265
691. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff63 line 1266
692. theorem OAI.SepticProfile.ExteriorCertificates.C23.row64 line 1267
693. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos64 line 1277
694. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos64 line 1278
695. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos64 line 1279
696. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio64 line 1280
697. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff64 line 1281
698. theorem OAI.SepticProfile.ExteriorCertificates.C23.row65 line 1282
699. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos65 line 1292
700. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos65 line 1293
701. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos65 line 1294
702. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio65 line 1295
703. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff65 line 1296
704. theorem OAI.SepticProfile.ExteriorCertificates.C23.row66 line 1297
705. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos66 line 1307
706. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos66 line 1308
707. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos66 line 1309
708. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio66 line 1310
709. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff66 line 1311
710. theorem OAI.SepticProfile.ExteriorCertificates.C23.row67 line 1312
711. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos67 line 1322
712. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos67 line 1323
713. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos67 line 1324
714. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio67 line 1325
715. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff67 line 1326
716. theorem OAI.SepticProfile.ExteriorCertificates.C23.row68 line 1327
717. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos68 line 1337
718. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos68 line 1338
719. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos68 line 1339
720. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio68 line 1340
721. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff68 line 1341
722. theorem OAI.SepticProfile.ExteriorCertificates.C23.row69 line 1342
723. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos69 line 1352
724. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos69 line 1353
725. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos69 line 1354
726. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio69 line 1355
727. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff69 line 1356
728. theorem OAI.SepticProfile.ExteriorCertificates.C23.row70 line 1357
729. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos70 line 1367
730. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos70 line 1368
731. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos70 line 1369
732. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio70 line 1370
733. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff70 line 1371
734. theorem OAI.SepticProfile.ExteriorCertificates.C23.row71 line 1372
735. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos71 line 1382
736. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos71 line 1383
737. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos71 line 1384
738. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio71 line 1385
739. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff71 line 1386
740. theorem OAI.SepticProfile.ExteriorCertificates.C23.row72 line 1387
741. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos72 line 1397
742. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos72 line 1398
743. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos72 line 1399
744. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio72 line 1400
745. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff72 line 1401
746. theorem OAI.SepticProfile.ExteriorCertificates.C23.row73 line 1402
747. theorem OAI.SepticProfile.ExteriorCertificates.C23.bpos73 line 1412
748. theorem OAI.SepticProfile.ExteriorCertificates.C23.rpos73 line 1413
749. theorem OAI.SepticProfile.ExteriorCertificates.C23.dpos73 line 1414
750. theorem OAI.SepticProfile.ExteriorCertificates.C23.ratio73 line 1415
751. theorem OAI.SepticProfile.ExteriorCertificates.C23.coeff73 line 1416
752. theorem OAI.SepticProfile.ExteriorCertificates.C23.row74 line 1417
753. theorem OAI.SepticProfile.ExteriorCertificates.C23.valid line 1427