OAI/MathematicalPhysics/Transonic/Shooting/RegularHighEndpoint.lean

GitHub source file

725 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SepticProfile.RegularHighData.R line 8
  2. def OAI.SepticProfile.RegularHighData.Q line 9
  3. def OAI.SepticProfile.RegularHighData.S line 10
  4. def OAI.SepticProfile.RegularHighData.SN line 11
  5. def OAI.SepticProfile.RegularHighData.K line 12
  6. def OAI.SepticProfile.RegularHighData.KN line 13
  7. def OAI.SepticProfile.RegularHighData.step0 line 14
  8. theorem OAI.SepticProfile.RegularHighData.cert0 line 15
  9. def OAI.SepticProfile.RegularHighData.step1 line 16
  10. theorem OAI.SepticProfile.RegularHighData.cert1 line 17
  11. theorem OAI.SepticProfile.RegularHighData.join1 line 18
  12. def OAI.SepticProfile.RegularHighData.step2 line 20
  13. theorem OAI.SepticProfile.RegularHighData.cert2 line 21
  14. theorem OAI.SepticProfile.RegularHighData.join2 line 22
  15. def OAI.SepticProfile.RegularHighData.step3 line 24
  16. theorem OAI.SepticProfile.RegularHighData.cert3 line 25
  17. theorem OAI.SepticProfile.RegularHighData.join3 line 26
  18. def OAI.SepticProfile.RegularHighData.step4 line 28
  19. theorem OAI.SepticProfile.RegularHighData.cert4 line 29
  20. theorem OAI.SepticProfile.RegularHighData.join4 line 30
  21. def OAI.SepticProfile.RegularHighData.step5 line 32
  22. theorem OAI.SepticProfile.RegularHighData.cert5 line 33
  23. theorem OAI.SepticProfile.RegularHighData.join5 line 34
  24. def OAI.SepticProfile.RegularHighData.step6 line 36
  25. theorem OAI.SepticProfile.RegularHighData.cert6 line 37
  26. theorem OAI.SepticProfile.RegularHighData.join6 line 38
  27. def OAI.SepticProfile.RegularHighData.step7 line 40
  28. theorem OAI.SepticProfile.RegularHighData.cert7 line 41
  29. theorem OAI.SepticProfile.RegularHighData.join7 line 42
  30. def OAI.SepticProfile.RegularHighData.step8 line 44
  31. theorem OAI.SepticProfile.RegularHighData.cert8 line 45
  32. theorem OAI.SepticProfile.RegularHighData.join8 line 46
  33. def OAI.SepticProfile.RegularHighData.step9 line 48
  34. theorem OAI.SepticProfile.RegularHighData.cert9 line 49
  35. theorem OAI.SepticProfile.RegularHighData.join9 line 50
  36. def OAI.SepticProfile.RegularHighData.step10 line 52
  37. theorem OAI.SepticProfile.RegularHighData.cert10 line 53
  38. theorem OAI.SepticProfile.RegularHighData.join10 line 54
  39. def OAI.SepticProfile.RegularHighData.step11 line 56
  40. theorem OAI.SepticProfile.RegularHighData.cert11 line 57
  41. theorem OAI.SepticProfile.RegularHighData.join11 line 58
  42. def OAI.SepticProfile.RegularHighData.step12 line 60
  43. theorem OAI.SepticProfile.RegularHighData.cert12 line 61
  44. theorem OAI.SepticProfile.RegularHighData.join12 line 62
  45. def OAI.SepticProfile.RegularHighData.step13 line 64
  46. theorem OAI.SepticProfile.RegularHighData.cert13 line 65
  47. theorem OAI.SepticProfile.RegularHighData.join13 line 66
  48. def OAI.SepticProfile.RegularHighData.step14 line 68
  49. theorem OAI.SepticProfile.RegularHighData.cert14 line 69
  50. theorem OAI.SepticProfile.RegularHighData.join14 line 70
  51. def OAI.SepticProfile.RegularHighData.step15 line 72
  52. theorem OAI.SepticProfile.RegularHighData.cert15 line 73
  53. theorem OAI.SepticProfile.RegularHighData.join15 line 74
  54. def OAI.SepticProfile.RegularHighData.step16 line 76
  55. theorem OAI.SepticProfile.RegularHighData.cert16 line 77
  56. theorem OAI.SepticProfile.RegularHighData.join16 line 78
  57. def OAI.SepticProfile.RegularHighData.step17 line 80
  58. theorem OAI.SepticProfile.RegularHighData.cert17 line 81
  59. theorem OAI.SepticProfile.RegularHighData.join17 line 82
  60. def OAI.SepticProfile.RegularHighData.step18 line 84
  61. theorem OAI.SepticProfile.RegularHighData.cert18 line 85
  62. theorem OAI.SepticProfile.RegularHighData.join18 line 86
  63. def OAI.SepticProfile.RegularHighData.step19 line 88
  64. theorem OAI.SepticProfile.RegularHighData.cert19 line 89
  65. theorem OAI.SepticProfile.RegularHighData.join19 line 90
  66. def OAI.SepticProfile.RegularHighData.step20 line 92
  67. theorem OAI.SepticProfile.RegularHighData.cert20 line 93
  68. theorem OAI.SepticProfile.RegularHighData.join20 line 94
  69. def OAI.SepticProfile.RegularHighData.step21 line 96
  70. theorem OAI.SepticProfile.RegularHighData.cert21 line 97
  71. theorem OAI.SepticProfile.RegularHighData.join21 line 98
  72. def OAI.SepticProfile.RegularHighData.step22 line 100
  73. theorem OAI.SepticProfile.RegularHighData.cert22 line 101
  74. theorem OAI.SepticProfile.RegularHighData.join22 line 102
  75. def OAI.SepticProfile.RegularHighData.step23 line 104
  76. theorem OAI.SepticProfile.RegularHighData.cert23 line 105
  77. theorem OAI.SepticProfile.RegularHighData.join23 line 106
  78. def OAI.SepticProfile.RegularHighData.step24 line 108
  79. theorem OAI.SepticProfile.RegularHighData.cert24 line 109
  80. theorem OAI.SepticProfile.RegularHighData.join24 line 110
  81. def OAI.SepticProfile.RegularHighData.step25 line 112
  82. theorem OAI.SepticProfile.RegularHighData.cert25 line 113
  83. theorem OAI.SepticProfile.RegularHighData.join25 line 114
  84. def OAI.SepticProfile.RegularHighData.step26 line 116
  85. theorem OAI.SepticProfile.RegularHighData.cert26 line 117
  86. theorem OAI.SepticProfile.RegularHighData.join26 line 118
  87. def OAI.SepticProfile.RegularHighData.step27 line 120
  88. theorem OAI.SepticProfile.RegularHighData.cert27 line 121
  89. theorem OAI.SepticProfile.RegularHighData.join27 line 122
  90. def OAI.SepticProfile.RegularHighData.step28 line 124
  91. theorem OAI.SepticProfile.RegularHighData.cert28 line 125
  92. theorem OAI.SepticProfile.RegularHighData.join28 line 126
  93. def OAI.SepticProfile.RegularHighData.step29 line 128
  94. theorem OAI.SepticProfile.RegularHighData.cert29 line 129
  95. theorem OAI.SepticProfile.RegularHighData.join29 line 130
  96. def OAI.SepticProfile.RegularHighData.step30 line 132
  97. theorem OAI.SepticProfile.RegularHighData.cert30 line 133
  98. theorem OAI.SepticProfile.RegularHighData.join30 line 134
  99. def OAI.SepticProfile.RegularHighData.step31 line 136
  100. theorem OAI.SepticProfile.RegularHighData.cert31 line 137
  101. theorem OAI.SepticProfile.RegularHighData.join31 line 138
  102. def OAI.SepticProfile.RegularHighData.step32 line 140
  103. theorem OAI.SepticProfile.RegularHighData.cert32 line 141
  104. theorem OAI.SepticProfile.RegularHighData.join32 line 142
  105. def OAI.SepticProfile.RegularHighData.step33 line 144
  106. theorem OAI.SepticProfile.RegularHighData.cert33 line 145
  107. theorem OAI.SepticProfile.RegularHighData.join33 line 146
  108. def OAI.SepticProfile.RegularHighData.step34 line 148
  109. theorem OAI.SepticProfile.RegularHighData.cert34 line 149
  110. theorem OAI.SepticProfile.RegularHighData.join34 line 150
  111. def OAI.SepticProfile.RegularHighData.step35 line 152
  112. theorem OAI.SepticProfile.RegularHighData.cert35 line 153
  113. theorem OAI.SepticProfile.RegularHighData.join35 line 154
  114. def OAI.SepticProfile.RegularHighData.step36 line 156
  115. theorem OAI.SepticProfile.RegularHighData.cert36 line 157
  116. theorem OAI.SepticProfile.RegularHighData.join36 line 158
  117. def OAI.SepticProfile.RegularHighData.step37 line 160
  118. theorem OAI.SepticProfile.RegularHighData.cert37 line 161
  119. theorem OAI.SepticProfile.RegularHighData.join37 line 162
  120. def OAI.SepticProfile.RegularHighData.step38 line 164
  121. theorem OAI.SepticProfile.RegularHighData.cert38 line 165
  122. theorem OAI.SepticProfile.RegularHighData.join38 line 166
  123. def OAI.SepticProfile.RegularHighData.step39 line 168
  124. theorem OAI.SepticProfile.RegularHighData.cert39 line 169
  125. theorem OAI.SepticProfile.RegularHighData.join39 line 170
  126. def OAI.SepticProfile.RegularHighData.step40 line 172
  127. theorem OAI.SepticProfile.RegularHighData.cert40 line 173
  128. theorem OAI.SepticProfile.RegularHighData.join40 line 174
  129. def OAI.SepticProfile.RegularHighData.step41 line 176
  130. theorem OAI.SepticProfile.RegularHighData.cert41 line 177
  131. theorem OAI.SepticProfile.RegularHighData.join41 line 178
  132. def OAI.SepticProfile.RegularHighData.step42 line 180
  133. theorem OAI.SepticProfile.RegularHighData.cert42 line 181
  134. theorem OAI.SepticProfile.RegularHighData.join42 line 182
  135. def OAI.SepticProfile.RegularHighData.step43 line 184
  136. theorem OAI.SepticProfile.RegularHighData.cert43 line 185
  137. theorem OAI.SepticProfile.RegularHighData.join43 line 186
  138. def OAI.SepticProfile.RegularHighData.step44 line 188
  139. theorem OAI.SepticProfile.RegularHighData.cert44 line 189
  140. theorem OAI.SepticProfile.RegularHighData.join44 line 190
  141. def OAI.SepticProfile.RegularHighData.step45 line 192
  142. theorem OAI.SepticProfile.RegularHighData.cert45 line 193
  143. theorem OAI.SepticProfile.RegularHighData.join45 line 194
  144. def OAI.SepticProfile.RegularHighData.step46 line 196
  145. theorem OAI.SepticProfile.RegularHighData.cert46 line 197
  146. theorem OAI.SepticProfile.RegularHighData.join46 line 198
  147. def OAI.SepticProfile.RegularHighData.step47 line 200
  148. theorem OAI.SepticProfile.RegularHighData.cert47 line 201
  149. theorem OAI.SepticProfile.RegularHighData.join47 line 202
  150. def OAI.SepticProfile.RegularHighData.step48 line 204
  151. theorem OAI.SepticProfile.RegularHighData.cert48 line 205
  152. theorem OAI.SepticProfile.RegularHighData.join48 line 206
  153. def OAI.SepticProfile.RegularHighData.step49 line 208
  154. theorem OAI.SepticProfile.RegularHighData.cert49 line 209
  155. theorem OAI.SepticProfile.RegularHighData.join49 line 210
  156. def OAI.SepticProfile.RegularHighData.step50 line 212
  157. theorem OAI.SepticProfile.RegularHighData.cert50 line 213
  158. theorem OAI.SepticProfile.RegularHighData.join50 line 214
  159. def OAI.SepticProfile.RegularHighData.step51 line 216
  160. theorem OAI.SepticProfile.RegularHighData.cert51 line 217
  161. theorem OAI.SepticProfile.RegularHighData.join51 line 218
  162. def OAI.SepticProfile.RegularHighData.step52 line 220
  163. theorem OAI.SepticProfile.RegularHighData.cert52 line 221
  164. theorem OAI.SepticProfile.RegularHighData.join52 line 222
  165. def OAI.SepticProfile.RegularHighData.step53 line 224
  166. theorem OAI.SepticProfile.RegularHighData.cert53 line 225
  167. theorem OAI.SepticProfile.RegularHighData.join53 line 226
  168. def OAI.SepticProfile.RegularHighData.step54 line 228
  169. theorem OAI.SepticProfile.RegularHighData.cert54 line 229
  170. theorem OAI.SepticProfile.RegularHighData.join54 line 230
  171. def OAI.SepticProfile.RegularHighData.step55 line 232
  172. theorem OAI.SepticProfile.RegularHighData.cert55 line 233
  173. theorem OAI.SepticProfile.RegularHighData.join55 line 234
  174. def OAI.SepticProfile.RegularHighData.step56 line 236
  175. theorem OAI.SepticProfile.RegularHighData.cert56 line 237
  176. theorem OAI.SepticProfile.RegularHighData.join56 line 238
  177. def OAI.SepticProfile.RegularHighData.step57 line 240
  178. theorem OAI.SepticProfile.RegularHighData.cert57 line 241
  179. theorem OAI.SepticProfile.RegularHighData.join57 line 242
  180. def OAI.SepticProfile.RegularHighData.step58 line 244
  181. theorem OAI.SepticProfile.RegularHighData.cert58 line 245
  182. theorem OAI.SepticProfile.RegularHighData.join58 line 246
  183. def OAI.SepticProfile.RegularHighData.step59 line 248
  184. theorem OAI.SepticProfile.RegularHighData.cert59 line 249
  185. theorem OAI.SepticProfile.RegularHighData.join59 line 250
  186. def OAI.SepticProfile.RegularHighData.step60 line 252
  187. theorem OAI.SepticProfile.RegularHighData.cert60 line 253
  188. theorem OAI.SepticProfile.RegularHighData.join60 line 254
  189. def OAI.SepticProfile.RegularHighData.step61 line 256
  190. theorem OAI.SepticProfile.RegularHighData.cert61 line 257
  191. theorem OAI.SepticProfile.RegularHighData.join61 line 258
  192. def OAI.SepticProfile.RegularHighData.step62 line 260
  193. theorem OAI.SepticProfile.RegularHighData.cert62 line 261
  194. theorem OAI.SepticProfile.RegularHighData.join62 line 262
  195. def OAI.SepticProfile.RegularHighData.step63 line 264
  196. theorem OAI.SepticProfile.RegularHighData.cert63 line 265
  197. theorem OAI.SepticProfile.RegularHighData.join63 line 266
  198. def OAI.SepticProfile.RegularHighData.step64 line 268
  199. theorem OAI.SepticProfile.RegularHighData.cert64 line 269
  200. theorem OAI.SepticProfile.RegularHighData.join64 line 270
  201. def OAI.SepticProfile.RegularHighData.step65 line 272
  202. theorem OAI.SepticProfile.RegularHighData.cert65 line 273
  203. theorem OAI.SepticProfile.RegularHighData.join65 line 274
  204. def OAI.SepticProfile.RegularHighData.step66 line 276
  205. theorem OAI.SepticProfile.RegularHighData.cert66 line 277
  206. theorem OAI.SepticProfile.RegularHighData.join66 line 278
  207. def OAI.SepticProfile.RegularHighData.step67 line 280
  208. theorem OAI.SepticProfile.RegularHighData.cert67 line 281
  209. theorem OAI.SepticProfile.RegularHighData.join67 line 282
  210. def OAI.SepticProfile.RegularHighData.step68 line 284
  211. theorem OAI.SepticProfile.RegularHighData.cert68 line 285
  212. theorem OAI.SepticProfile.RegularHighData.join68 line 286
  213. def OAI.SepticProfile.RegularHighData.step69 line 288
  214. theorem OAI.SepticProfile.RegularHighData.cert69 line 289
  215. theorem OAI.SepticProfile.RegularHighData.join69 line 290
  216. def OAI.SepticProfile.RegularHighData.step70 line 292
  217. theorem OAI.SepticProfile.RegularHighData.cert70 line 293
  218. theorem OAI.SepticProfile.RegularHighData.join70 line 294
  219. def OAI.SepticProfile.RegularHighData.step71 line 296
  220. theorem OAI.SepticProfile.RegularHighData.cert71 line 297
  221. theorem OAI.SepticProfile.RegularHighData.join71 line 298
  222. def OAI.SepticProfile.RegularHighData.step72 line 300
  223. theorem OAI.SepticProfile.RegularHighData.cert72 line 301
  224. theorem OAI.SepticProfile.RegularHighData.join72 line 302
  225. def OAI.SepticProfile.RegularHighData.step73 line 304
  226. theorem OAI.SepticProfile.RegularHighData.cert73 line 305
  227. theorem OAI.SepticProfile.RegularHighData.join73 line 306
  228. def OAI.SepticProfile.RegularHighData.step74 line 308
  229. theorem OAI.SepticProfile.RegularHighData.cert74 line 309
  230. theorem OAI.SepticProfile.RegularHighData.join74 line 310
  231. def OAI.SepticProfile.RegularHighData.step75 line 312
  232. theorem OAI.SepticProfile.RegularHighData.cert75 line 313
  233. theorem OAI.SepticProfile.RegularHighData.join75 line 314
  234. def OAI.SepticProfile.RegularHighData.step76 line 316
  235. theorem OAI.SepticProfile.RegularHighData.cert76 line 317
  236. theorem OAI.SepticProfile.RegularHighData.join76 line 318
  237. def OAI.SepticProfile.RegularHighData.step77 line 320
  238. theorem OAI.SepticProfile.RegularHighData.cert77 line 321
  239. theorem OAI.SepticProfile.RegularHighData.join77 line 322
  240. def OAI.SepticProfile.RegularHighData.step78 line 324
  241. theorem OAI.SepticProfile.RegularHighData.cert78 line 325
  242. theorem OAI.SepticProfile.RegularHighData.join78 line 326
  243. def OAI.SepticProfile.RegularHighData.step79 line 328
  244. theorem OAI.SepticProfile.RegularHighData.cert79 line 329
  245. theorem OAI.SepticProfile.RegularHighData.join79 line 330
  246. def OAI.SepticProfile.RegularHighData.step80 line 332
  247. theorem OAI.SepticProfile.RegularHighData.cert80 line 333
  248. theorem OAI.SepticProfile.RegularHighData.join80 line 334
  249. def OAI.SepticProfile.RegularHighData.step81 line 336
  250. theorem OAI.SepticProfile.RegularHighData.cert81 line 337
  251. theorem OAI.SepticProfile.RegularHighData.join81 line 338
  252. def OAI.SepticProfile.RegularHighData.step82 line 340
  253. theorem OAI.SepticProfile.RegularHighData.cert82 line 341
  254. theorem OAI.SepticProfile.RegularHighData.join82 line 342
  255. def OAI.SepticProfile.RegularHighData.step83 line 344
  256. theorem OAI.SepticProfile.RegularHighData.cert83 line 345
  257. theorem OAI.SepticProfile.RegularHighData.join83 line 346
  258. def OAI.SepticProfile.RegularHighData.step84 line 348
  259. theorem OAI.SepticProfile.RegularHighData.cert84 line 349
  260. theorem OAI.SepticProfile.RegularHighData.join84 line 350
  261. def OAI.SepticProfile.RegularHighData.step85 line 352
  262. theorem OAI.SepticProfile.RegularHighData.cert85 line 353
  263. theorem OAI.SepticProfile.RegularHighData.join85 line 354
  264. def OAI.SepticProfile.RegularHighData.step86 line 356
  265. theorem OAI.SepticProfile.RegularHighData.cert86 line 357
  266. theorem OAI.SepticProfile.RegularHighData.join86 line 358
  267. def OAI.SepticProfile.RegularHighData.step87 line 360
  268. theorem OAI.SepticProfile.RegularHighData.cert87 line 361
  269. theorem OAI.SepticProfile.RegularHighData.join87 line 362
  270. def OAI.SepticProfile.RegularHighData.step88 line 364
  271. theorem OAI.SepticProfile.RegularHighData.cert88 line 365
  272. theorem OAI.SepticProfile.RegularHighData.join88 line 366
  273. def OAI.SepticProfile.RegularHighData.step89 line 368
  274. theorem OAI.SepticProfile.RegularHighData.cert89 line 369
  275. theorem OAI.SepticProfile.RegularHighData.join89 line 370
  276. def OAI.SepticProfile.RegularHighData.step90 line 372
  277. theorem OAI.SepticProfile.RegularHighData.cert90 line 373
  278. theorem OAI.SepticProfile.RegularHighData.join90 line 374
  279. def OAI.SepticProfile.RegularHighData.step91 line 376
  280. theorem OAI.SepticProfile.RegularHighData.cert91 line 377
  281. theorem OAI.SepticProfile.RegularHighData.join91 line 378
  282. def OAI.SepticProfile.RegularHighData.step92 line 380
  283. theorem OAI.SepticProfile.RegularHighData.cert92 line 381
  284. theorem OAI.SepticProfile.RegularHighData.join92 line 382
  285. def OAI.SepticProfile.RegularHighData.step93 line 384
  286. theorem OAI.SepticProfile.RegularHighData.cert93 line 385
  287. theorem OAI.SepticProfile.RegularHighData.join93 line 386
  288. def OAI.SepticProfile.RegularHighData.step94 line 388
  289. theorem OAI.SepticProfile.RegularHighData.cert94 line 389
  290. theorem OAI.SepticProfile.RegularHighData.join94 line 390
  291. def OAI.SepticProfile.RegularHighData.step95 line 392
  292. theorem OAI.SepticProfile.RegularHighData.cert95 line 393
  293. theorem OAI.SepticProfile.RegularHighData.join95 line 394
  294. def OAI.SepticProfile.RegularHighData.step96 line 396
  295. theorem OAI.SepticProfile.RegularHighData.cert96 line 397
  296. theorem OAI.SepticProfile.RegularHighData.join96 line 398
  297. def OAI.SepticProfile.RegularHighData.step97 line 400
  298. theorem OAI.SepticProfile.RegularHighData.cert97 line 401
  299. theorem OAI.SepticProfile.RegularHighData.join97 line 402
  300. def OAI.SepticProfile.RegularHighData.step98 line 404
  301. theorem OAI.SepticProfile.RegularHighData.cert98 line 405
  302. theorem OAI.SepticProfile.RegularHighData.join98 line 406
  303. def OAI.SepticProfile.RegularHighData.step99 line 408
  304. theorem OAI.SepticProfile.RegularHighData.cert99 line 409
  305. theorem OAI.SepticProfile.RegularHighData.join99 line 410
  306. def OAI.SepticProfile.RegularHighData.step100 line 412
  307. theorem OAI.SepticProfile.RegularHighData.cert100 line 413
  308. theorem OAI.SepticProfile.RegularHighData.join100 line 414
  309. def OAI.SepticProfile.RegularHighData.step101 line 416
  310. theorem OAI.SepticProfile.RegularHighData.cert101 line 417
  311. theorem OAI.SepticProfile.RegularHighData.join101 line 418
  312. def OAI.SepticProfile.RegularHighData.step102 line 420
  313. theorem OAI.SepticProfile.RegularHighData.cert102 line 421
  314. theorem OAI.SepticProfile.RegularHighData.join102 line 422
  315. def OAI.SepticProfile.RegularHighData.step103 line 424
  316. theorem OAI.SepticProfile.RegularHighData.cert103 line 425
  317. theorem OAI.SepticProfile.RegularHighData.join103 line 426
  318. def OAI.SepticProfile.RegularHighData.step104 line 428
  319. theorem OAI.SepticProfile.RegularHighData.cert104 line 429
  320. theorem OAI.SepticProfile.RegularHighData.join104 line 430
  321. def OAI.SepticProfile.RegularHighData.step105 line 432
  322. theorem OAI.SepticProfile.RegularHighData.cert105 line 433
  323. theorem OAI.SepticProfile.RegularHighData.join105 line 434
  324. def OAI.SepticProfile.RegularHighData.step106 line 436
  325. theorem OAI.SepticProfile.RegularHighData.cert106 line 437
  326. theorem OAI.SepticProfile.RegularHighData.join106 line 438
  327. def OAI.SepticProfile.RegularHighData.step107 line 440
  328. theorem OAI.SepticProfile.RegularHighData.cert107 line 441
  329. theorem OAI.SepticProfile.RegularHighData.join107 line 442
  330. def OAI.SepticProfile.RegularHighData.step108 line 444
  331. theorem OAI.SepticProfile.RegularHighData.cert108 line 445
  332. theorem OAI.SepticProfile.RegularHighData.join108 line 446
  333. def OAI.SepticProfile.RegularHighData.step109 line 448
  334. theorem OAI.SepticProfile.RegularHighData.cert109 line 449
  335. theorem OAI.SepticProfile.RegularHighData.join109 line 450
  336. def OAI.SepticProfile.RegularHighData.step110 line 452
  337. theorem OAI.SepticProfile.RegularHighData.cert110 line 453
  338. theorem OAI.SepticProfile.RegularHighData.join110 line 454
  339. def OAI.SepticProfile.RegularHighData.step111 line 456
  340. theorem OAI.SepticProfile.RegularHighData.cert111 line 457
  341. theorem OAI.SepticProfile.RegularHighData.join111 line 458
  342. def OAI.SepticProfile.RegularHighData.step112 line 460
  343. theorem OAI.SepticProfile.RegularHighData.cert112 line 461
  344. theorem OAI.SepticProfile.RegularHighData.join112 line 462
  345. def OAI.SepticProfile.RegularHighData.step113 line 464
  346. theorem OAI.SepticProfile.RegularHighData.cert113 line 465
  347. theorem OAI.SepticProfile.RegularHighData.join113 line 466
  348. def OAI.SepticProfile.RegularHighData.step114 line 468
  349. theorem OAI.SepticProfile.RegularHighData.cert114 line 469
  350. theorem OAI.SepticProfile.RegularHighData.join114 line 470
  351. def OAI.SepticProfile.RegularHighData.step115 line 472
  352. theorem OAI.SepticProfile.RegularHighData.cert115 line 473
  353. theorem OAI.SepticProfile.RegularHighData.join115 line 474
  354. def OAI.SepticProfile.RegularHighData.step116 line 476
  355. theorem OAI.SepticProfile.RegularHighData.cert116 line 477
  356. theorem OAI.SepticProfile.RegularHighData.join116 line 478
  357. def OAI.SepticProfile.RegularHighData.step117 line 480
  358. theorem OAI.SepticProfile.RegularHighData.cert117 line 481
  359. theorem OAI.SepticProfile.RegularHighData.join117 line 482
  360. def OAI.SepticProfile.RegularHighData.step118 line 484
  361. theorem OAI.SepticProfile.RegularHighData.cert118 line 485
  362. theorem OAI.SepticProfile.RegularHighData.join118 line 486
  363. def OAI.SepticProfile.RegularHighData.step119 line 488
  364. theorem OAI.SepticProfile.RegularHighData.cert119 line 489
  365. theorem OAI.SepticProfile.RegularHighData.join119 line 490
  366. def OAI.SepticProfile.RegularHighData.step120 line 492
  367. theorem OAI.SepticProfile.RegularHighData.cert120 line 493
  368. theorem OAI.SepticProfile.RegularHighData.join120 line 494
  369. def OAI.SepticProfile.RegularHighData.step121 line 496
  370. theorem OAI.SepticProfile.RegularHighData.cert121 line 497
  371. theorem OAI.SepticProfile.RegularHighData.join121 line 498
  372. def OAI.SepticProfile.RegularHighData.step122 line 500
  373. theorem OAI.SepticProfile.RegularHighData.cert122 line 501
  374. theorem OAI.SepticProfile.RegularHighData.join122 line 502
  375. def OAI.SepticProfile.RegularHighData.step123 line 504
  376. theorem OAI.SepticProfile.RegularHighData.cert123 line 505
  377. theorem OAI.SepticProfile.RegularHighData.join123 line 506
  378. def OAI.SepticProfile.RegularHighData.step124 line 508
  379. theorem OAI.SepticProfile.RegularHighData.cert124 line 509
  380. theorem OAI.SepticProfile.RegularHighData.join124 line 510
  381. def OAI.SepticProfile.RegularHighData.step125 line 512
  382. theorem OAI.SepticProfile.RegularHighData.cert125 line 513
  383. theorem OAI.SepticProfile.RegularHighData.join125 line 514
  384. def OAI.SepticProfile.RegularHighData.step126 line 516
  385. theorem OAI.SepticProfile.RegularHighData.cert126 line 517
  386. theorem OAI.SepticProfile.RegularHighData.join126 line 518
  387. def OAI.SepticProfile.RegularHighData.step127 line 520
  388. theorem OAI.SepticProfile.RegularHighData.cert127 line 521
  389. theorem OAI.SepticProfile.RegularHighData.join127 line 522
  390. def OAI.SepticProfile.RegularHighData.step128 line 524
  391. theorem OAI.SepticProfile.RegularHighData.cert128 line 525
  392. theorem OAI.SepticProfile.RegularHighData.join128 line 526
  393. def OAI.SepticProfile.RegularHighData.step129 line 528
  394. theorem OAI.SepticProfile.RegularHighData.cert129 line 529
  395. theorem OAI.SepticProfile.RegularHighData.join129 line 530
  396. def OAI.SepticProfile.RegularHighData.step130 line 532
  397. theorem OAI.SepticProfile.RegularHighData.cert130 line 533
  398. theorem OAI.SepticProfile.RegularHighData.join130 line 534
  399. def OAI.SepticProfile.RegularHighData.step131 line 536
  400. theorem OAI.SepticProfile.RegularHighData.cert131 line 537
  401. theorem OAI.SepticProfile.RegularHighData.join131 line 538
  402. def OAI.SepticProfile.RegularHighData.step132 line 540
  403. theorem OAI.SepticProfile.RegularHighData.cert132 line 541
  404. theorem OAI.SepticProfile.RegularHighData.join132 line 542
  405. def OAI.SepticProfile.RegularHighData.step133 line 544
  406. theorem OAI.SepticProfile.RegularHighData.cert133 line 545
  407. theorem OAI.SepticProfile.RegularHighData.join133 line 546
  408. def OAI.SepticProfile.RegularHighData.step134 line 548
  409. theorem OAI.SepticProfile.RegularHighData.cert134 line 549
  410. theorem OAI.SepticProfile.RegularHighData.join134 line 550
  411. def OAI.SepticProfile.RegularHighData.step135 line 552
  412. theorem OAI.SepticProfile.RegularHighData.cert135 line 553
  413. theorem OAI.SepticProfile.RegularHighData.join135 line 554
  414. def OAI.SepticProfile.RegularHighData.step136 line 556
  415. theorem OAI.SepticProfile.RegularHighData.cert136 line 557
  416. theorem OAI.SepticProfile.RegularHighData.join136 line 558
  417. def OAI.SepticProfile.RegularHighData.step137 line 560
  418. theorem OAI.SepticProfile.RegularHighData.cert137 line 561
  419. theorem OAI.SepticProfile.RegularHighData.join137 line 562
  420. def OAI.SepticProfile.RegularHighData.step138 line 564
  421. theorem OAI.SepticProfile.RegularHighData.cert138 line 565
  422. theorem OAI.SepticProfile.RegularHighData.join138 line 566
  423. def OAI.SepticProfile.RegularHighData.step139 line 568
  424. theorem OAI.SepticProfile.RegularHighData.cert139 line 569
  425. theorem OAI.SepticProfile.RegularHighData.join139 line 570
  426. def OAI.SepticProfile.RegularHighData.step140 line 572
  427. theorem OAI.SepticProfile.RegularHighData.cert140 line 573
  428. theorem OAI.SepticProfile.RegularHighData.join140 line 574
  429. def OAI.SepticProfile.RegularHighData.step141 line 576
  430. theorem OAI.SepticProfile.RegularHighData.cert141 line 577
  431. theorem OAI.SepticProfile.RegularHighData.join141 line 578
  432. def OAI.SepticProfile.RegularHighData.step142 line 580
  433. theorem OAI.SepticProfile.RegularHighData.cert142 line 581
  434. theorem OAI.SepticProfile.RegularHighData.join142 line 582
  435. def OAI.SepticProfile.RegularHighData.step143 line 584
  436. theorem OAI.SepticProfile.RegularHighData.cert143 line 585
  437. theorem OAI.SepticProfile.RegularHighData.join143 line 586
  438. def OAI.SepticProfile.RegularHighData.step144 line 588
  439. theorem OAI.SepticProfile.RegularHighData.cert144 line 589
  440. theorem OAI.SepticProfile.RegularHighData.join144 line 590
  441. def OAI.SepticProfile.RegularHighData.step145 line 592
  442. theorem OAI.SepticProfile.RegularHighData.cert145 line 593
  443. theorem OAI.SepticProfile.RegularHighData.join145 line 594
  444. def OAI.SepticProfile.RegularHighData.step146 line 596
  445. theorem OAI.SepticProfile.RegularHighData.cert146 line 597
  446. theorem OAI.SepticProfile.RegularHighData.join146 line 598
  447. def OAI.SepticProfile.RegularHighData.step147 line 600
  448. theorem OAI.SepticProfile.RegularHighData.cert147 line 601
  449. theorem OAI.SepticProfile.RegularHighData.join147 line 602
  450. def OAI.SepticProfile.RegularHighData.step148 line 604
  451. theorem OAI.SepticProfile.RegularHighData.cert148 line 605
  452. theorem OAI.SepticProfile.RegularHighData.join148 line 606
  453. def OAI.SepticProfile.RegularHighData.step149 line 608
  454. theorem OAI.SepticProfile.RegularHighData.cert149 line 609
  455. theorem OAI.SepticProfile.RegularHighData.join149 line 610
  456. def OAI.SepticProfile.RegularHighData.step150 line 612
  457. theorem OAI.SepticProfile.RegularHighData.cert150 line 613
  458. theorem OAI.SepticProfile.RegularHighData.join150 line 614
  459. def OAI.SepticProfile.RegularHighData.step151 line 616
  460. theorem OAI.SepticProfile.RegularHighData.cert151 line 617
  461. theorem OAI.SepticProfile.RegularHighData.join151 line 618
  462. def OAI.SepticProfile.RegularHighData.step152 line 620
  463. theorem OAI.SepticProfile.RegularHighData.cert152 line 621
  464. theorem OAI.SepticProfile.RegularHighData.join152 line 622
  465. def OAI.SepticProfile.RegularHighData.step153 line 624
  466. theorem OAI.SepticProfile.RegularHighData.cert153 line 625
  467. theorem OAI.SepticProfile.RegularHighData.join153 line 626
  468. def OAI.SepticProfile.RegularHighData.step154 line 628
  469. theorem OAI.SepticProfile.RegularHighData.cert154 line 629
  470. theorem OAI.SepticProfile.RegularHighData.join154 line 630
  471. def OAI.SepticProfile.RegularHighData.step155 line 632
  472. theorem OAI.SepticProfile.RegularHighData.cert155 line 633
  473. theorem OAI.SepticProfile.RegularHighData.join155 line 634
  474. def OAI.SepticProfile.RegularHighData.step156 line 636
  475. theorem OAI.SepticProfile.RegularHighData.cert156 line 637
  476. theorem OAI.SepticProfile.RegularHighData.join156 line 638
  477. def OAI.SepticProfile.RegularHighData.step157 line 640
  478. theorem OAI.SepticProfile.RegularHighData.cert157 line 641
  479. theorem OAI.SepticProfile.RegularHighData.join157 line 642
  480. def OAI.SepticProfile.RegularHighData.step158 line 644
  481. theorem OAI.SepticProfile.RegularHighData.cert158 line 645
  482. theorem OAI.SepticProfile.RegularHighData.join158 line 646
  483. def OAI.SepticProfile.RegularHighData.step159 line 648
  484. theorem OAI.SepticProfile.RegularHighData.cert159 line 649
  485. theorem OAI.SepticProfile.RegularHighData.join159 line 650
  486. def OAI.SepticProfile.RegularHighData.step160 line 652
  487. theorem OAI.SepticProfile.RegularHighData.cert160 line 653
  488. theorem OAI.SepticProfile.RegularHighData.join160 line 654
  489. def OAI.SepticProfile.RegularHighData.step161 line 656
  490. theorem OAI.SepticProfile.RegularHighData.cert161 line 657
  491. theorem OAI.SepticProfile.RegularHighData.join161 line 658
  492. def OAI.SepticProfile.RegularHighData.step162 line 660
  493. theorem OAI.SepticProfile.RegularHighData.cert162 line 661
  494. theorem OAI.SepticProfile.RegularHighData.join162 line 662
  495. def OAI.SepticProfile.RegularHighData.step163 line 664
  496. theorem OAI.SepticProfile.RegularHighData.cert163 line 665
  497. theorem OAI.SepticProfile.RegularHighData.join163 line 666
  498. def OAI.SepticProfile.RegularHighData.step164 line 668
  499. theorem OAI.SepticProfile.RegularHighData.cert164 line 669
  500. theorem OAI.SepticProfile.RegularHighData.join164 line 670
  501. def OAI.SepticProfile.RegularHighData.step165 line 672
  502. theorem OAI.SepticProfile.RegularHighData.cert165 line 673
  503. theorem OAI.SepticProfile.RegularHighData.join165 line 674
  504. def OAI.SepticProfile.RegularHighData.step166 line 676
  505. theorem OAI.SepticProfile.RegularHighData.cert166 line 677
  506. theorem OAI.SepticProfile.RegularHighData.join166 line 678
  507. def OAI.SepticProfile.RegularHighData.step167 line 680
  508. theorem OAI.SepticProfile.RegularHighData.cert167 line 681
  509. theorem OAI.SepticProfile.RegularHighData.join167 line 682
  510. def OAI.SepticProfile.RegularHighData.step168 line 684
  511. theorem OAI.SepticProfile.RegularHighData.cert168 line 685
  512. theorem OAI.SepticProfile.RegularHighData.join168 line 686
  513. def OAI.SepticProfile.RegularHighData.step169 line 688
  514. theorem OAI.SepticProfile.RegularHighData.cert169 line 689
  515. theorem OAI.SepticProfile.RegularHighData.join169 line 690
  516. def OAI.SepticProfile.RegularHighData.step170 line 692
  517. theorem OAI.SepticProfile.RegularHighData.cert170 line 693
  518. theorem OAI.SepticProfile.RegularHighData.join170 line 694
  519. def OAI.SepticProfile.RegularHighData.step171 line 696
  520. theorem OAI.SepticProfile.RegularHighData.cert171 line 697
  521. theorem OAI.SepticProfile.RegularHighData.join171 line 698
  522. def OAI.SepticProfile.RegularHighData.step172 line 700
  523. theorem OAI.SepticProfile.RegularHighData.cert172 line 701
  524. theorem OAI.SepticProfile.RegularHighData.join172 line 702
  525. def OAI.SepticProfile.RegularHighData.step173 line 704
  526. theorem OAI.SepticProfile.RegularHighData.cert173 line 705
  527. theorem OAI.SepticProfile.RegularHighData.join173 line 706
  528. def OAI.SepticProfile.RegularHighData.step174 line 708
  529. theorem OAI.SepticProfile.RegularHighData.cert174 line 709
  530. theorem OAI.SepticProfile.RegularHighData.join174 line 710
  531. def OAI.SepticProfile.RegularHighData.step175 line 712
  532. theorem OAI.SepticProfile.RegularHighData.cert175 line 713
  533. theorem OAI.SepticProfile.RegularHighData.join175 line 714
  534. def OAI.SepticProfile.RegularHighData.step176 line 716
  535. theorem OAI.SepticProfile.RegularHighData.cert176 line 717
  536. theorem OAI.SepticProfile.RegularHighData.join176 line 718
  537. def OAI.SepticProfile.RegularHighData.step177 line 720
  538. theorem OAI.SepticProfile.RegularHighData.cert177 line 721
  539. theorem OAI.SepticProfile.RegularHighData.join177 line 722
  540. def OAI.SepticProfile.RegularHighData.step178 line 724
  541. theorem OAI.SepticProfile.RegularHighData.cert178 line 725
  542. theorem OAI.SepticProfile.RegularHighData.join178 line 726
  543. def OAI.SepticProfile.RegularHighData.step179 line 728
  544. theorem OAI.SepticProfile.RegularHighData.cert179 line 729
  545. theorem OAI.SepticProfile.RegularHighData.join179 line 730
  546. def OAI.SepticProfile.RegularHighData.step180 line 732
  547. theorem OAI.SepticProfile.RegularHighData.cert180 line 733
  548. theorem OAI.SepticProfile.RegularHighData.join180 line 734
  549. def OAI.SepticProfile.RegularHighData.step181 line 736
  550. theorem OAI.SepticProfile.RegularHighData.cert181 line 737
  551. theorem OAI.SepticProfile.RegularHighData.join181 line 738
  552. def OAI.SepticProfile.RegularHighData.step182 line 740
  553. theorem OAI.SepticProfile.RegularHighData.cert182 line 741
  554. theorem OAI.SepticProfile.RegularHighData.join182 line 742
  555. def OAI.SepticProfile.RegularHighData.step183 line 744
  556. theorem OAI.SepticProfile.RegularHighData.cert183 line 745
  557. theorem OAI.SepticProfile.RegularHighData.join183 line 746
  558. def OAI.SepticProfile.RegularHighData.step184 line 748
  559. theorem OAI.SepticProfile.RegularHighData.cert184 line 749
  560. theorem OAI.SepticProfile.RegularHighData.join184 line 750
  561. def OAI.SepticProfile.RegularHighData.step185 line 752
  562. theorem OAI.SepticProfile.RegularHighData.cert185 line 753
  563. theorem OAI.SepticProfile.RegularHighData.join185 line 754
  564. def OAI.SepticProfile.RegularHighData.step186 line 756
  565. theorem OAI.SepticProfile.RegularHighData.cert186 line 757
  566. theorem OAI.SepticProfile.RegularHighData.join186 line 758
  567. def OAI.SepticProfile.RegularHighData.step187 line 760
  568. theorem OAI.SepticProfile.RegularHighData.cert187 line 761
  569. theorem OAI.SepticProfile.RegularHighData.join187 line 762
  570. def OAI.SepticProfile.RegularHighData.step188 line 764
  571. theorem OAI.SepticProfile.RegularHighData.cert188 line 765
  572. theorem OAI.SepticProfile.RegularHighData.join188 line 766
  573. def OAI.SepticProfile.RegularHighData.step189 line 768
  574. theorem OAI.SepticProfile.RegularHighData.cert189 line 769
  575. theorem OAI.SepticProfile.RegularHighData.join189 line 770
  576. def OAI.SepticProfile.RegularHighData.step190 line 772
  577. theorem OAI.SepticProfile.RegularHighData.cert190 line 773
  578. theorem OAI.SepticProfile.RegularHighData.join190 line 774
  579. def OAI.SepticProfile.RegularHighData.step191 line 776
  580. theorem OAI.SepticProfile.RegularHighData.cert191 line 777
  581. theorem OAI.SepticProfile.RegularHighData.join191 line 778
  582. def OAI.SepticProfile.RegularHighData.step192 line 780
  583. theorem OAI.SepticProfile.RegularHighData.cert192 line 781
  584. theorem OAI.SepticProfile.RegularHighData.join192 line 782
  585. def OAI.SepticProfile.RegularHighData.step193 line 784
  586. theorem OAI.SepticProfile.RegularHighData.cert193 line 785
  587. theorem OAI.SepticProfile.RegularHighData.join193 line 786
  588. def OAI.SepticProfile.RegularHighData.step194 line 788
  589. theorem OAI.SepticProfile.RegularHighData.cert194 line 789
  590. theorem OAI.SepticProfile.RegularHighData.join194 line 790
  591. def OAI.SepticProfile.RegularHighData.step195 line 792
  592. theorem OAI.SepticProfile.RegularHighData.cert195 line 793
  593. theorem OAI.SepticProfile.RegularHighData.join195 line 794
  594. def OAI.SepticProfile.RegularHighData.step196 line 796
  595. theorem OAI.SepticProfile.RegularHighData.cert196 line 797
  596. theorem OAI.SepticProfile.RegularHighData.join196 line 798
  597. def OAI.SepticProfile.RegularHighData.step197 line 800
  598. theorem OAI.SepticProfile.RegularHighData.cert197 line 801
  599. theorem OAI.SepticProfile.RegularHighData.join197 line 802
  600. def OAI.SepticProfile.RegularHighData.step198 line 804
  601. theorem OAI.SepticProfile.RegularHighData.cert198 line 805
  602. theorem OAI.SepticProfile.RegularHighData.join198 line 806
  603. def OAI.SepticProfile.RegularHighData.step199 line 808
  604. theorem OAI.SepticProfile.RegularHighData.cert199 line 809
  605. theorem OAI.SepticProfile.RegularHighData.join199 line 810
  606. def OAI.SepticProfile.RegularHighData.step200 line 812
  607. theorem OAI.SepticProfile.RegularHighData.cert200 line 813
  608. theorem OAI.SepticProfile.RegularHighData.join200 line 814
  609. def OAI.SepticProfile.RegularHighData.step201 line 816
  610. theorem OAI.SepticProfile.RegularHighData.cert201 line 817
  611. theorem OAI.SepticProfile.RegularHighData.join201 line 818
  612. def OAI.SepticProfile.RegularHighData.step202 line 820
  613. theorem OAI.SepticProfile.RegularHighData.cert202 line 821
  614. theorem OAI.SepticProfile.RegularHighData.join202 line 822
  615. def OAI.SepticProfile.RegularHighData.step203 line 824
  616. theorem OAI.SepticProfile.RegularHighData.cert203 line 825
  617. theorem OAI.SepticProfile.RegularHighData.join203 line 826
  618. def OAI.SepticProfile.RegularHighData.step204 line 828
  619. theorem OAI.SepticProfile.RegularHighData.cert204 line 829
  620. theorem OAI.SepticProfile.RegularHighData.join204 line 830
  621. def OAI.SepticProfile.RegularHighData.step205 line 832
  622. theorem OAI.SepticProfile.RegularHighData.cert205 line 833
  623. theorem OAI.SepticProfile.RegularHighData.join205 line 834
  624. def OAI.SepticProfile.RegularHighData.step206 line 836
  625. theorem OAI.SepticProfile.RegularHighData.cert206 line 837
  626. theorem OAI.SepticProfile.RegularHighData.join206 line 838
  627. def OAI.SepticProfile.RegularHighData.step207 line 840
  628. theorem OAI.SepticProfile.RegularHighData.cert207 line 841
  629. theorem OAI.SepticProfile.RegularHighData.join207 line 842
  630. def OAI.SepticProfile.RegularHighData.step208 line 844
  631. theorem OAI.SepticProfile.RegularHighData.cert208 line 845
  632. theorem OAI.SepticProfile.RegularHighData.join208 line 846
  633. def OAI.SepticProfile.RegularHighData.step209 line 848
  634. theorem OAI.SepticProfile.RegularHighData.cert209 line 849
  635. theorem OAI.SepticProfile.RegularHighData.join209 line 850
  636. def OAI.SepticProfile.RegularHighData.step210 line 852
  637. theorem OAI.SepticProfile.RegularHighData.cert210 line 853
  638. theorem OAI.SepticProfile.RegularHighData.join210 line 854
  639. def OAI.SepticProfile.RegularHighData.step211 line 856
  640. theorem OAI.SepticProfile.RegularHighData.cert211 line 857
  641. theorem OAI.SepticProfile.RegularHighData.join211 line 858
  642. def OAI.SepticProfile.RegularHighData.step212 line 860
  643. theorem OAI.SepticProfile.RegularHighData.cert212 line 861
  644. theorem OAI.SepticProfile.RegularHighData.join212 line 862
  645. def OAI.SepticProfile.RegularHighData.step213 line 864
  646. theorem OAI.SepticProfile.RegularHighData.cert213 line 865
  647. theorem OAI.SepticProfile.RegularHighData.join213 line 866
  648. def OAI.SepticProfile.RegularHighData.step214 line 868
  649. theorem OAI.SepticProfile.RegularHighData.cert214 line 869
  650. theorem OAI.SepticProfile.RegularHighData.join214 line 870
  651. def OAI.SepticProfile.RegularHighData.step215 line 872
  652. theorem OAI.SepticProfile.RegularHighData.cert215 line 873
  653. theorem OAI.SepticProfile.RegularHighData.join215 line 874
  654. def OAI.SepticProfile.RegularHighData.step216 line 876
  655. theorem OAI.SepticProfile.RegularHighData.cert216 line 877
  656. theorem OAI.SepticProfile.RegularHighData.join216 line 878
  657. def OAI.SepticProfile.RegularHighData.step217 line 880
  658. theorem OAI.SepticProfile.RegularHighData.cert217 line 881
  659. theorem OAI.SepticProfile.RegularHighData.join217 line 882
  660. def OAI.SepticProfile.RegularHighData.step218 line 884
  661. theorem OAI.SepticProfile.RegularHighData.cert218 line 885
  662. theorem OAI.SepticProfile.RegularHighData.join218 line 886
  663. def OAI.SepticProfile.RegularHighData.step219 line 888
  664. theorem OAI.SepticProfile.RegularHighData.cert219 line 889
  665. theorem OAI.SepticProfile.RegularHighData.join219 line 890
  666. def OAI.SepticProfile.RegularHighData.step220 line 892
  667. theorem OAI.SepticProfile.RegularHighData.cert220 line 893
  668. theorem OAI.SepticProfile.RegularHighData.join220 line 894
  669. def OAI.SepticProfile.RegularHighData.step221 line 896
  670. theorem OAI.SepticProfile.RegularHighData.cert221 line 897
  671. theorem OAI.SepticProfile.RegularHighData.join221 line 898
  672. def OAI.SepticProfile.RegularHighData.step222 line 900
  673. theorem OAI.SepticProfile.RegularHighData.cert222 line 901
  674. theorem OAI.SepticProfile.RegularHighData.join222 line 902
  675. def OAI.SepticProfile.RegularHighData.step223 line 904
  676. theorem OAI.SepticProfile.RegularHighData.cert223 line 905
  677. theorem OAI.SepticProfile.RegularHighData.join223 line 906
  678. def OAI.SepticProfile.RegularHighData.step224 line 908
  679. theorem OAI.SepticProfile.RegularHighData.cert224 line 909
  680. theorem OAI.SepticProfile.RegularHighData.join224 line 910
  681. def OAI.SepticProfile.RegularHighData.step225 line 912
  682. theorem OAI.SepticProfile.RegularHighData.cert225 line 913
  683. theorem OAI.SepticProfile.RegularHighData.join225 line 914
  684. def OAI.SepticProfile.RegularHighData.step226 line 916
  685. theorem OAI.SepticProfile.RegularHighData.cert226 line 917
  686. theorem OAI.SepticProfile.RegularHighData.join226 line 918
  687. def OAI.SepticProfile.RegularHighData.step227 line 920
  688. theorem OAI.SepticProfile.RegularHighData.cert227 line 921
  689. theorem OAI.SepticProfile.RegularHighData.join227 line 922
  690. def OAI.SepticProfile.RegularHighData.step228 line 924
  691. theorem OAI.SepticProfile.RegularHighData.cert228 line 925
  692. theorem OAI.SepticProfile.RegularHighData.join228 line 926
  693. def OAI.SepticProfile.RegularHighData.step229 line 928
  694. theorem OAI.SepticProfile.RegularHighData.cert229 line 929
  695. theorem OAI.SepticProfile.RegularHighData.join229 line 930
  696. def OAI.SepticProfile.RegularHighData.step230 line 932
  697. theorem OAI.SepticProfile.RegularHighData.cert230 line 933
  698. theorem OAI.SepticProfile.RegularHighData.join230 line 934
  699. def OAI.SepticProfile.RegularHighData.step231 line 936
  700. theorem OAI.SepticProfile.RegularHighData.cert231 line 937
  701. theorem OAI.SepticProfile.RegularHighData.join231 line 938
  702. theorem OAI.SepticProfile.RegularHighData.S_pos line 942
  703. theorem OAI.SepticProfile.RegularHighData.K_pos line 943
  704. theorem OAI.SepticProfile.RegularHighData.R_pos line 944
  705. theorem OAI.SepticProfile.RegularHighData.Q_pos line 945
  706. theorem OAI.SepticProfile.RegularHighData.sigma_mem line 946
  707. theorem OAI.SepticProfile.RegularHighData.first_time line 947
  708. theorem OAI.SepticProfile.RegularHighData.last_time line 948
  709. theorem OAI.SepticProfile.RegularHighData.final_integer_bound line 949
  710. theorem OAI.SepticProfile.RegularHighData.propagate_0 line 951
  711. theorem OAI.SepticProfile.RegularHighData.propagate_16 line 987
  712. theorem OAI.SepticProfile.RegularHighData.propagate_32 line 1023
  713. theorem OAI.SepticProfile.RegularHighData.propagate_48 line 1059
  714. theorem OAI.SepticProfile.RegularHighData.propagate_64 line 1095
  715. theorem OAI.SepticProfile.RegularHighData.propagate_80 line 1131
  716. theorem OAI.SepticProfile.RegularHighData.propagate_96 line 1167
  717. theorem OAI.SepticProfile.RegularHighData.propagate_112 line 1203
  718. theorem OAI.SepticProfile.RegularHighData.propagate_128 line 1239
  719. theorem OAI.SepticProfile.RegularHighData.propagate_144 line 1275
  720. theorem OAI.SepticProfile.RegularHighData.propagate_160 line 1311
  721. theorem OAI.SepticProfile.RegularHighData.propagate_176 line 1347
  722. theorem OAI.SepticProfile.RegularHighData.propagate_192 line 1383
  723. theorem OAI.SepticProfile.RegularHighData.propagate_208 line 1419
  724. theorem OAI.SepticProfile.RegularHighData.propagate_224 line 1455
  725. theorem OAI.SepticProfile.RegularHighData.endpoint_bound line 1475