OAI/GameTheory/SnakyTwentyOne/Cards/Height04Part04.lean

GitHub source file

396 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_268 line 13
  2. def OAI.SnakyPrototype.Certificate21.envelope_268 line 14
  3. def OAI.SnakyPrototype.Certificate21.childrenC_268 line 15
  4. def OAI.SnakyPrototype.Certificate21.childrenD_268 line 16
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_268 line 17
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_268 line 18
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_268 line 19
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_268 line 20
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_268 line 21
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_268 line 27
  11. def OAI.SnakyPrototype.Certificate21.required_269 line 32
  12. def OAI.SnakyPrototype.Certificate21.envelope_269 line 33
  13. def OAI.SnakyPrototype.Certificate21.childrenC_269 line 34
  14. def OAI.SnakyPrototype.Certificate21.childrenD_269 line 35
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_269 line 36
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_269 line 37
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_269 line 38
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_269 line 39
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_269 line 40
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_269 line 45
  21. def OAI.SnakyPrototype.Certificate21.required_271 line 50
  22. def OAI.SnakyPrototype.Certificate21.envelope_271 line 51
  23. def OAI.SnakyPrototype.Certificate21.childrenC_271 line 52
  24. def OAI.SnakyPrototype.Certificate21.childrenD_271 line 53
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_271 line 54
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_271 line 55
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_271 line 56
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_271 line 57
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_271 line 58
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_271 line 63
  31. def OAI.SnakyPrototype.Certificate21.required_277 line 68
  32. def OAI.SnakyPrototype.Certificate21.envelope_277 line 69
  33. def OAI.SnakyPrototype.Certificate21.childrenC_277 line 70
  34. def OAI.SnakyPrototype.Certificate21.childrenD_277 line 71
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_277 line 72
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_277 line 73
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_277 line 74
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_277 line 75
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_277 line 76
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_277 line 81
  41. def OAI.SnakyPrototype.Certificate21.required_288 line 86
  42. def OAI.SnakyPrototype.Certificate21.envelope_288 line 87
  43. def OAI.SnakyPrototype.Certificate21.childrenC_288 line 88
  44. def OAI.SnakyPrototype.Certificate21.childrenD_288 line 89
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_288 line 90
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_288 line 91
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_288 line 92
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_288 line 93
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_288 line 94
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_288 line 99
  51. def OAI.SnakyPrototype.Certificate21.required_289 line 104
  52. def OAI.SnakyPrototype.Certificate21.envelope_289 line 105
  53. def OAI.SnakyPrototype.Certificate21.childrenC_289 line 106
  54. def OAI.SnakyPrototype.Certificate21.childrenD_289 line 107
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_289 line 108
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_289 line 109
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_289 line 110
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_289 line 111
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_289 line 112
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_289 line 118
  61. def OAI.SnakyPrototype.Certificate21.required_291 line 123
  62. def OAI.SnakyPrototype.Certificate21.envelope_291 line 124
  63. def OAI.SnakyPrototype.Certificate21.childrenC_291 line 125
  64. def OAI.SnakyPrototype.Certificate21.childrenD_291 line 126
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_291 line 127
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_291 line 128
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_291 line 129
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_291 line 130
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_291 line 131
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_291 line 136
  71. def OAI.SnakyPrototype.Certificate21.required_304 line 141
  72. def OAI.SnakyPrototype.Certificate21.envelope_304 line 142
  73. def OAI.SnakyPrototype.Certificate21.childrenC_304 line 143
  74. def OAI.SnakyPrototype.Certificate21.childrenD_304 line 144
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_304 line 145
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_304 line 146
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_304 line 147
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_304 line 148
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_304 line 149
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_304 line 155
  81. def OAI.SnakyPrototype.Certificate21.required_305 line 160
  82. def OAI.SnakyPrototype.Certificate21.envelope_305 line 161
  83. def OAI.SnakyPrototype.Certificate21.childrenC_305 line 162
  84. def OAI.SnakyPrototype.Certificate21.childrenD_305 line 163
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_305 line 164
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_305 line 165
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_305 line 166
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_305 line 167
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_305 line 168
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_305 line 173
  91. def OAI.SnakyPrototype.Certificate21.required_307 line 178
  92. def OAI.SnakyPrototype.Certificate21.envelope_307 line 179
  93. def OAI.SnakyPrototype.Certificate21.childrenC_307 line 180
  94. def OAI.SnakyPrototype.Certificate21.childrenD_307 line 181
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_307 line 182
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_307 line 183
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_307 line 184
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_307 line 185
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_307 line 186
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_307 line 191
  101. def OAI.SnakyPrototype.Certificate21.required_311_i0 line 196
  102. def OAI.SnakyPrototype.Certificate21.envelope_311_i0 line 197
  103. def OAI.SnakyPrototype.Certificate21.childrenC_311_i0 line 198
  104. def OAI.SnakyPrototype.Certificate21.childrenD_311_i0 line 199
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_311_i0 line 200
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_311_i0 line 201
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_311_i0 line 202
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_311_i0 line 203
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_311_i0 line 204
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_311_i0 line 209
  111. def OAI.SnakyPrototype.Certificate21.required_311 line 214
  112. def OAI.SnakyPrototype.Certificate21.envelope_311 line 215
  113. def OAI.SnakyPrototype.Certificate21.childrenC_311 line 216
  114. def OAI.SnakyPrototype.Certificate21.childrenD_311 line 217
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_311 line 218
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_311 line 219
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_311 line 220
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_311 line 221
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_311 line 222
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_311 line 227
  121. def OAI.SnakyPrototype.Certificate21.required_334 line 232
  122. def OAI.SnakyPrototype.Certificate21.envelope_334 line 233
  123. def OAI.SnakyPrototype.Certificate21.childrenC_334 line 234
  124. def OAI.SnakyPrototype.Certificate21.childrenD_334 line 235
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_334 line 236
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_334 line 237
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_334 line 238
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_334 line 239
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_334 line 240
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_334 line 247
  131. def OAI.SnakyPrototype.Certificate21.required_351 line 252
  132. def OAI.SnakyPrototype.Certificate21.envelope_351 line 253
  133. def OAI.SnakyPrototype.Certificate21.childrenC_351 line 254
  134. def OAI.SnakyPrototype.Certificate21.childrenD_351 line 255
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_351 line 256
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_351 line 257
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_351 line 258
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_351 line 259
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_351 line 260
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_351 line 265
  141. def OAI.SnakyPrototype.Certificate21.required_354_i0 line 270
  142. def OAI.SnakyPrototype.Certificate21.envelope_354_i0 line 271
  143. def OAI.SnakyPrototype.Certificate21.childrenC_354_i0 line 272
  144. def OAI.SnakyPrototype.Certificate21.childrenD_354_i0 line 273
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_354_i0 line 274
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_354_i0 line 275
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_354_i0 line 276
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_354_i0 line 277
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_354_i0 line 278
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_354_i0 line 283
  151. def OAI.SnakyPrototype.Certificate21.required_354 line 288
  152. def OAI.SnakyPrototype.Certificate21.envelope_354 line 289
  153. def OAI.SnakyPrototype.Certificate21.childrenC_354 line 290
  154. def OAI.SnakyPrototype.Certificate21.childrenD_354 line 291
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_354 line 292
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_354 line 293
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_354 line 294
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_354 line 295
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_354 line 296
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_354 line 301
  161. def OAI.SnakyPrototype.Certificate21.required_365_i1 line 306
  162. def OAI.SnakyPrototype.Certificate21.envelope_365_i1 line 307
  163. def OAI.SnakyPrototype.Certificate21.childrenC_365_i1 line 308
  164. def OAI.SnakyPrototype.Certificate21.childrenD_365_i1 line 309
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_365_i1 line 310
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_365_i1 line 311
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_365_i1 line 312
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_365_i1 line 313
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_365_i1 line 314
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_365_i1 line 319
  171. def OAI.SnakyPrototype.Certificate21.required_365_i0 line 324
  172. def OAI.SnakyPrototype.Certificate21.envelope_365_i0 line 325
  173. def OAI.SnakyPrototype.Certificate21.childrenC_365_i0 line 326
  174. def OAI.SnakyPrototype.Certificate21.childrenD_365_i0 line 327
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_365_i0 line 328
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_365_i0 line 329
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_365_i0 line 330
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_365_i0 line 331
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_365_i0 line 332
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_365_i0 line 337
  181. def OAI.SnakyPrototype.Certificate21.required_365 line 342
  182. def OAI.SnakyPrototype.Certificate21.envelope_365 line 343
  183. def OAI.SnakyPrototype.Certificate21.childrenC_365 line 344
  184. def OAI.SnakyPrototype.Certificate21.childrenD_365 line 345
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_365 line 346
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_365 line 347
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_365 line 348
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_365 line 349
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_365 line 350
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_365 line 355
  191. def OAI.SnakyPrototype.Certificate21.required_375 line 360
  192. def OAI.SnakyPrototype.Certificate21.envelope_375 line 361
  193. def OAI.SnakyPrototype.Certificate21.childrenC_375 line 362
  194. def OAI.SnakyPrototype.Certificate21.childrenD_375 line 363
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_375 line 364
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_375 line 365
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_375 line 366
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_375 line 367
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_375 line 368
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_375 line 373
  201. def OAI.SnakyPrototype.Certificate21.required_376_i0 line 378
  202. def OAI.SnakyPrototype.Certificate21.envelope_376_i0 line 379
  203. def OAI.SnakyPrototype.Certificate21.childrenC_376_i0 line 380
  204. def OAI.SnakyPrototype.Certificate21.childrenD_376_i0 line 381
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_376_i0 line 382
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_376_i0 line 383
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_376_i0 line 384
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_376_i0 line 385
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_376_i0 line 386
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_376_i0 line 391
  211. def OAI.SnakyPrototype.Certificate21.required_376 line 396
  212. def OAI.SnakyPrototype.Certificate21.envelope_376 line 397
  213. def OAI.SnakyPrototype.Certificate21.childrenC_376 line 398
  214. def OAI.SnakyPrototype.Certificate21.childrenD_376 line 399
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_376 line 400
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_376 line 401
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_376 line 402
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_376 line 403
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_376 line 404
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_376 line 409
  221. def OAI.SnakyPrototype.Certificate21.height_268 line 414
  222. def OAI.SnakyPrototype.Certificate21.childrenH_268 line 415
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_268 line 416
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_268 line 417
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_268 line 419
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_268 line 423
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_268 line 425
  228. def OAI.SnakyPrototype.Certificate21.checked_268 line 429
  229. def OAI.SnakyPrototype.Certificate21.height_269 line 437
  230. def OAI.SnakyPrototype.Certificate21.childrenH_269 line 438
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_269 line 439
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_269 line 440
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_269 line 442
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_269 line 446
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_269 line 448
  236. def OAI.SnakyPrototype.Certificate21.checked_269 line 452
  237. def OAI.SnakyPrototype.Certificate21.height_271 line 460
  238. def OAI.SnakyPrototype.Certificate21.childrenH_271 line 461
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_271 line 462
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_271 line 463
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_271 line 465
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_271 line 469
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_271 line 471
  244. def OAI.SnakyPrototype.Certificate21.checked_271 line 475
  245. def OAI.SnakyPrototype.Certificate21.height_277 line 483
  246. def OAI.SnakyPrototype.Certificate21.childrenH_277 line 484
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_277 line 485
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_277 line 486
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_277 line 488
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_277 line 492
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_277 line 494
  252. def OAI.SnakyPrototype.Certificate21.checked_277 line 498
  253. def OAI.SnakyPrototype.Certificate21.height_288 line 506
  254. def OAI.SnakyPrototype.Certificate21.childrenH_288 line 507
  255. theorem OAI.SnakyPrototype.Certificate21.height_exact_288 line 508
  256. theorem OAI.SnakyPrototype.Certificate21.required_origin_288 line 509
  257. theorem OAI.SnakyPrototype.Certificate21.required_exact_288 line 511
  258. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_288 line 515
  259. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_288 line 517
  260. def OAI.SnakyPrototype.Certificate21.checked_288 line 521
  261. def OAI.SnakyPrototype.Certificate21.height_289 line 529
  262. def OAI.SnakyPrototype.Certificate21.childrenH_289 line 530
  263. theorem OAI.SnakyPrototype.Certificate21.height_exact_289 line 531
  264. theorem OAI.SnakyPrototype.Certificate21.required_origin_289 line 532
  265. theorem OAI.SnakyPrototype.Certificate21.required_exact_289 line 534
  266. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_289 line 538
  267. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_289 line 540
  268. def OAI.SnakyPrototype.Certificate21.checked_289 line 544
  269. def OAI.SnakyPrototype.Certificate21.height_291 line 552
  270. def OAI.SnakyPrototype.Certificate21.childrenH_291 line 553
  271. theorem OAI.SnakyPrototype.Certificate21.height_exact_291 line 554
  272. theorem OAI.SnakyPrototype.Certificate21.required_origin_291 line 555
  273. theorem OAI.SnakyPrototype.Certificate21.required_exact_291 line 557
  274. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_291 line 561
  275. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_291 line 563
  276. def OAI.SnakyPrototype.Certificate21.checked_291 line 567
  277. def OAI.SnakyPrototype.Certificate21.height_304 line 575
  278. def OAI.SnakyPrototype.Certificate21.childrenH_304 line 576
  279. theorem OAI.SnakyPrototype.Certificate21.height_exact_304 line 577
  280. theorem OAI.SnakyPrototype.Certificate21.required_origin_304 line 578
  281. theorem OAI.SnakyPrototype.Certificate21.required_exact_304 line 580
  282. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_304 line 584
  283. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_304 line 586
  284. def OAI.SnakyPrototype.Certificate21.checked_304 line 590
  285. def OAI.SnakyPrototype.Certificate21.height_305 line 598
  286. def OAI.SnakyPrototype.Certificate21.childrenH_305 line 599
  287. theorem OAI.SnakyPrototype.Certificate21.height_exact_305 line 600
  288. theorem OAI.SnakyPrototype.Certificate21.required_origin_305 line 601
  289. theorem OAI.SnakyPrototype.Certificate21.required_exact_305 line 603
  290. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_305 line 607
  291. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_305 line 609
  292. def OAI.SnakyPrototype.Certificate21.checked_305 line 613
  293. def OAI.SnakyPrototype.Certificate21.height_307 line 621
  294. def OAI.SnakyPrototype.Certificate21.childrenH_307 line 622
  295. theorem OAI.SnakyPrototype.Certificate21.height_exact_307 line 623
  296. theorem OAI.SnakyPrototype.Certificate21.required_origin_307 line 624
  297. theorem OAI.SnakyPrototype.Certificate21.required_exact_307 line 626
  298. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_307 line 630
  299. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_307 line 632
  300. def OAI.SnakyPrototype.Certificate21.checked_307 line 636
  301. def OAI.SnakyPrototype.Certificate21.height_311_i0 line 644
  302. def OAI.SnakyPrototype.Certificate21.childrenH_311_i0 line 645
  303. theorem OAI.SnakyPrototype.Certificate21.height_exact_311_i0 line 646
  304. theorem OAI.SnakyPrototype.Certificate21.required_origin_311_i0 line 647
  305. theorem OAI.SnakyPrototype.Certificate21.required_exact_311_i0 line 649
  306. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_311_i0 line 653
  307. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_311_i0 line 655
  308. def OAI.SnakyPrototype.Certificate21.checked_311_i0 line 659
  309. def OAI.SnakyPrototype.Certificate21.height_311 line 667
  310. def OAI.SnakyPrototype.Certificate21.childrenH_311 line 668
  311. theorem OAI.SnakyPrototype.Certificate21.height_exact_311 line 669
  312. theorem OAI.SnakyPrototype.Certificate21.required_origin_311 line 670
  313. theorem OAI.SnakyPrototype.Certificate21.required_exact_311 line 672
  314. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_311 line 676
  315. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_311 line 678
  316. def OAI.SnakyPrototype.Certificate21.checked_311 line 682
  317. def OAI.SnakyPrototype.Certificate21.height_334 line 690
  318. def OAI.SnakyPrototype.Certificate21.childrenH_334 line 691
  319. theorem OAI.SnakyPrototype.Certificate21.height_exact_334 line 692
  320. theorem OAI.SnakyPrototype.Certificate21.required_origin_334 line 693
  321. theorem OAI.SnakyPrototype.Certificate21.required_exact_334 line 695
  322. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_334 line 699
  323. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_334 line 701
  324. def OAI.SnakyPrototype.Certificate21.checked_334 line 705
  325. def OAI.SnakyPrototype.Certificate21.height_351 line 713
  326. def OAI.SnakyPrototype.Certificate21.childrenH_351 line 714
  327. theorem OAI.SnakyPrototype.Certificate21.height_exact_351 line 715
  328. theorem OAI.SnakyPrototype.Certificate21.required_origin_351 line 716
  329. theorem OAI.SnakyPrototype.Certificate21.required_exact_351 line 718
  330. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_351 line 722
  331. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_351 line 724
  332. def OAI.SnakyPrototype.Certificate21.checked_351 line 728
  333. def OAI.SnakyPrototype.Certificate21.height_354_i0 line 736
  334. def OAI.SnakyPrototype.Certificate21.childrenH_354_i0 line 737
  335. theorem OAI.SnakyPrototype.Certificate21.height_exact_354_i0 line 738
  336. theorem OAI.SnakyPrototype.Certificate21.required_origin_354_i0 line 739
  337. theorem OAI.SnakyPrototype.Certificate21.required_exact_354_i0 line 741
  338. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_354_i0 line 745
  339. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_354_i0 line 747
  340. def OAI.SnakyPrototype.Certificate21.checked_354_i0 line 751
  341. def OAI.SnakyPrototype.Certificate21.height_354 line 759
  342. def OAI.SnakyPrototype.Certificate21.childrenH_354 line 760
  343. theorem OAI.SnakyPrototype.Certificate21.height_exact_354 line 761
  344. theorem OAI.SnakyPrototype.Certificate21.required_origin_354 line 762
  345. theorem OAI.SnakyPrototype.Certificate21.required_exact_354 line 764
  346. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_354 line 768
  347. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_354 line 770
  348. def OAI.SnakyPrototype.Certificate21.checked_354 line 774
  349. def OAI.SnakyPrototype.Certificate21.height_365_i1 line 782
  350. def OAI.SnakyPrototype.Certificate21.childrenH_365_i1 line 783
  351. theorem OAI.SnakyPrototype.Certificate21.height_exact_365_i1 line 784
  352. theorem OAI.SnakyPrototype.Certificate21.required_origin_365_i1 line 785
  353. theorem OAI.SnakyPrototype.Certificate21.required_exact_365_i1 line 787
  354. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_365_i1 line 791
  355. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_365_i1 line 793
  356. def OAI.SnakyPrototype.Certificate21.checked_365_i1 line 797
  357. def OAI.SnakyPrototype.Certificate21.height_365_i0 line 805
  358. def OAI.SnakyPrototype.Certificate21.childrenH_365_i0 line 806
  359. theorem OAI.SnakyPrototype.Certificate21.height_exact_365_i0 line 807
  360. theorem OAI.SnakyPrototype.Certificate21.required_origin_365_i0 line 808
  361. theorem OAI.SnakyPrototype.Certificate21.required_exact_365_i0 line 810
  362. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_365_i0 line 814
  363. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_365_i0 line 816
  364. def OAI.SnakyPrototype.Certificate21.checked_365_i0 line 820
  365. def OAI.SnakyPrototype.Certificate21.height_365 line 828
  366. def OAI.SnakyPrototype.Certificate21.childrenH_365 line 829
  367. theorem OAI.SnakyPrototype.Certificate21.height_exact_365 line 830
  368. theorem OAI.SnakyPrototype.Certificate21.required_origin_365 line 831
  369. theorem OAI.SnakyPrototype.Certificate21.required_exact_365 line 833
  370. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_365 line 837
  371. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_365 line 839
  372. def OAI.SnakyPrototype.Certificate21.checked_365 line 843
  373. def OAI.SnakyPrototype.Certificate21.height_375 line 851
  374. def OAI.SnakyPrototype.Certificate21.childrenH_375 line 852
  375. theorem OAI.SnakyPrototype.Certificate21.height_exact_375 line 853
  376. theorem OAI.SnakyPrototype.Certificate21.required_origin_375 line 854
  377. theorem OAI.SnakyPrototype.Certificate21.required_exact_375 line 856
  378. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_375 line 860
  379. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_375 line 862
  380. def OAI.SnakyPrototype.Certificate21.checked_375 line 866
  381. def OAI.SnakyPrototype.Certificate21.height_376_i0 line 874
  382. def OAI.SnakyPrototype.Certificate21.childrenH_376_i0 line 875
  383. theorem OAI.SnakyPrototype.Certificate21.height_exact_376_i0 line 876
  384. theorem OAI.SnakyPrototype.Certificate21.required_origin_376_i0 line 877
  385. theorem OAI.SnakyPrototype.Certificate21.required_exact_376_i0 line 879
  386. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_376_i0 line 883
  387. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_376_i0 line 885
  388. def OAI.SnakyPrototype.Certificate21.checked_376_i0 line 889
  389. def OAI.SnakyPrototype.Certificate21.height_376 line 897
  390. def OAI.SnakyPrototype.Certificate21.childrenH_376 line 898
  391. theorem OAI.SnakyPrototype.Certificate21.height_exact_376 line 899
  392. theorem OAI.SnakyPrototype.Certificate21.required_origin_376 line 900
  393. theorem OAI.SnakyPrototype.Certificate21.required_exact_376 line 902
  394. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_376 line 906
  395. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_376 line 908
  396. def OAI.SnakyPrototype.Certificate21.checked_376 line 912