OAI/GameTheory/SnakyTwentyOne/Cards/Height09Part01.lean

GitHub source file

396 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_322 line 21
  2. def OAI.SnakyPrototype.Certificate21.envelope_322 line 22
  3. def OAI.SnakyPrototype.Certificate21.childrenC_322 line 23
  4. def OAI.SnakyPrototype.Certificate21.childrenD_322 line 24
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_322 line 25
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_322 line 26
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_322 line 27
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_322 line 28
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_322 line 29
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_322 line 35
  11. def OAI.SnakyPrototype.Certificate21.required_325 line 40
  12. def OAI.SnakyPrototype.Certificate21.envelope_325 line 41
  13. def OAI.SnakyPrototype.Certificate21.childrenC_325 line 42
  14. def OAI.SnakyPrototype.Certificate21.childrenD_325 line 43
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_325 line 44
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_325 line 45
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_325 line 46
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_325 line 47
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_325 line 48
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_325 line 53
  21. def OAI.SnakyPrototype.Certificate21.required_326 line 58
  22. def OAI.SnakyPrototype.Certificate21.envelope_326 line 59
  23. def OAI.SnakyPrototype.Certificate21.childrenC_326 line 60
  24. def OAI.SnakyPrototype.Certificate21.childrenD_326 line 61
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_326 line 62
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_326 line 63
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_326 line 64
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_326 line 65
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_326 line 66
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_326 line 71
  31. def OAI.SnakyPrototype.Certificate21.required_327 line 76
  32. def OAI.SnakyPrototype.Certificate21.envelope_327 line 77
  33. def OAI.SnakyPrototype.Certificate21.childrenC_327 line 78
  34. def OAI.SnakyPrototype.Certificate21.childrenD_327 line 79
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_327 line 80
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_327 line 81
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_327 line 82
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_327 line 83
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_327 line 84
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_327 line 89
  41. def OAI.SnakyPrototype.Certificate21.required_328 line 94
  42. def OAI.SnakyPrototype.Certificate21.envelope_328 line 95
  43. def OAI.SnakyPrototype.Certificate21.childrenC_328 line 96
  44. def OAI.SnakyPrototype.Certificate21.childrenD_328 line 97
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_328 line 98
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_328 line 99
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_328 line 100
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_328 line 101
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_328 line 102
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_328 line 108
  51. def OAI.SnakyPrototype.Certificate21.required_330 line 113
  52. def OAI.SnakyPrototype.Certificate21.envelope_330 line 114
  53. def OAI.SnakyPrototype.Certificate21.childrenC_330 line 115
  54. def OAI.SnakyPrototype.Certificate21.childrenD_330 line 116
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_330 line 117
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_330 line 118
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_330 line 119
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_330 line 120
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_330 line 121
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_330 line 127
  61. def OAI.SnakyPrototype.Certificate21.required_368 line 132
  62. def OAI.SnakyPrototype.Certificate21.envelope_368 line 133
  63. def OAI.SnakyPrototype.Certificate21.childrenC_368 line 134
  64. def OAI.SnakyPrototype.Certificate21.childrenD_368 line 135
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_368 line 136
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_368 line 137
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_368 line 138
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_368 line 139
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_368 line 140
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_368 line 150
  71. def OAI.SnakyPrototype.Certificate21.required_380_i0 line 155
  72. def OAI.SnakyPrototype.Certificate21.envelope_380_i0 line 156
  73. def OAI.SnakyPrototype.Certificate21.childrenC_380_i0 line 157
  74. def OAI.SnakyPrototype.Certificate21.childrenD_380_i0 line 158
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_380_i0 line 159
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_380_i0 line 160
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_380_i0 line 161
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_380_i0 line 162
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_380_i0 line 163
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_380_i0 line 168
  81. def OAI.SnakyPrototype.Certificate21.required_380 line 173
  82. def OAI.SnakyPrototype.Certificate21.envelope_380 line 174
  83. def OAI.SnakyPrototype.Certificate21.childrenC_380 line 175
  84. def OAI.SnakyPrototype.Certificate21.childrenD_380 line 176
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_380 line 177
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_380 line 178
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_380 line 179
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_380 line 180
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_380 line 181
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_380 line 186
  91. def OAI.SnakyPrototype.Certificate21.required_396 line 191
  92. def OAI.SnakyPrototype.Certificate21.envelope_396 line 192
  93. def OAI.SnakyPrototype.Certificate21.childrenC_396 line 193
  94. def OAI.SnakyPrototype.Certificate21.childrenD_396 line 194
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_396 line 195
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_396 line 196
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_396 line 197
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_396 line 198
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_396 line 199
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_396 line 205
  101. def OAI.SnakyPrototype.Certificate21.required_397 line 210
  102. def OAI.SnakyPrototype.Certificate21.envelope_397 line 211
  103. def OAI.SnakyPrototype.Certificate21.childrenC_397 line 212
  104. def OAI.SnakyPrototype.Certificate21.childrenD_397 line 213
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_397 line 214
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_397 line 215
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_397 line 216
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_397 line 217
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_397 line 218
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_397 line 225
  111. def OAI.SnakyPrototype.Certificate21.required_398 line 230
  112. def OAI.SnakyPrototype.Certificate21.envelope_398 line 231
  113. def OAI.SnakyPrototype.Certificate21.childrenC_398 line 232
  114. def OAI.SnakyPrototype.Certificate21.childrenD_398 line 233
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_398 line 234
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_398 line 235
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_398 line 236
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_398 line 237
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_398 line 238
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_398 line 246
  121. def OAI.SnakyPrototype.Certificate21.required_400 line 251
  122. def OAI.SnakyPrototype.Certificate21.envelope_400 line 252
  123. def OAI.SnakyPrototype.Certificate21.childrenC_400 line 253
  124. def OAI.SnakyPrototype.Certificate21.childrenD_400 line 254
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_400 line 255
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_400 line 256
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_400 line 257
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_400 line 258
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_400 line 259
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_400 line 264
  131. def OAI.SnakyPrototype.Certificate21.required_406 line 269
  132. def OAI.SnakyPrototype.Certificate21.envelope_406 line 270
  133. def OAI.SnakyPrototype.Certificate21.childrenC_406 line 271
  134. def OAI.SnakyPrototype.Certificate21.childrenD_406 line 272
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_406 line 273
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_406 line 274
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_406 line 275
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_406 line 276
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_406 line 277
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_406 line 284
  141. def OAI.SnakyPrototype.Certificate21.required_407_i0 line 289
  142. def OAI.SnakyPrototype.Certificate21.envelope_407_i0 line 290
  143. def OAI.SnakyPrototype.Certificate21.childrenC_407_i0 line 291
  144. def OAI.SnakyPrototype.Certificate21.childrenD_407_i0 line 292
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_407_i0 line 293
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_407_i0 line 294
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_407_i0 line 295
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_407_i0 line 296
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_407_i0 line 297
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_407_i0 line 302
  151. def OAI.SnakyPrototype.Certificate21.required_407 line 307
  152. def OAI.SnakyPrototype.Certificate21.envelope_407 line 308
  153. def OAI.SnakyPrototype.Certificate21.childrenC_407 line 309
  154. def OAI.SnakyPrototype.Certificate21.childrenD_407 line 310
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_407 line 311
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_407 line 312
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_407 line 313
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_407 line 314
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_407 line 315
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_407 line 322
  161. def OAI.SnakyPrototype.Certificate21.required_421 line 327
  162. def OAI.SnakyPrototype.Certificate21.envelope_421 line 328
  163. def OAI.SnakyPrototype.Certificate21.childrenC_421 line 329
  164. def OAI.SnakyPrototype.Certificate21.childrenD_421 line 330
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_421 line 331
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_421 line 332
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_421 line 333
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_421 line 334
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_421 line 335
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_421 line 341
  171. def OAI.SnakyPrototype.Certificate21.required_434_i0 line 346
  172. def OAI.SnakyPrototype.Certificate21.envelope_434_i0 line 347
  173. def OAI.SnakyPrototype.Certificate21.childrenC_434_i0 line 348
  174. def OAI.SnakyPrototype.Certificate21.childrenD_434_i0 line 349
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_434_i0 line 350
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_434_i0 line 351
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_434_i0 line 352
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_434_i0 line 353
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_434_i0 line 354
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_434_i0 line 359
  181. def OAI.SnakyPrototype.Certificate21.required_434_i1 line 364
  182. def OAI.SnakyPrototype.Certificate21.envelope_434_i1 line 365
  183. def OAI.SnakyPrototype.Certificate21.childrenC_434_i1 line 366
  184. def OAI.SnakyPrototype.Certificate21.childrenD_434_i1 line 367
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_434_i1 line 368
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_434_i1 line 369
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_434_i1 line 370
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_434_i1 line 371
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_434_i1 line 372
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_434_i1 line 380
  191. def OAI.SnakyPrototype.Certificate21.required_434 line 385
  192. def OAI.SnakyPrototype.Certificate21.envelope_434 line 386
  193. def OAI.SnakyPrototype.Certificate21.childrenC_434 line 387
  194. def OAI.SnakyPrototype.Certificate21.childrenD_434 line 388
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_434 line 389
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_434 line 390
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_434 line 391
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_434 line 392
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_434 line 393
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_434 line 399
  201. def OAI.SnakyPrototype.Certificate21.required_441 line 404
  202. def OAI.SnakyPrototype.Certificate21.envelope_441 line 405
  203. def OAI.SnakyPrototype.Certificate21.childrenC_441 line 406
  204. def OAI.SnakyPrototype.Certificate21.childrenD_441 line 407
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_441 line 408
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_441 line 409
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_441 line 410
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_441 line 411
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_441 line 412
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_441 line 418
  211. def OAI.SnakyPrototype.Certificate21.required_442 line 423
  212. def OAI.SnakyPrototype.Certificate21.envelope_442 line 424
  213. def OAI.SnakyPrototype.Certificate21.childrenC_442 line 425
  214. def OAI.SnakyPrototype.Certificate21.childrenD_442 line 426
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_442 line 427
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_442 line 428
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_442 line 429
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_442 line 430
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_442 line 431
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_442 line 437
  221. def OAI.SnakyPrototype.Certificate21.height_322 line 442
  222. def OAI.SnakyPrototype.Certificate21.childrenH_322 line 443
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_322 line 444
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_322 line 445
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_322 line 447
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_322 line 451
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_322 line 453
  228. def OAI.SnakyPrototype.Certificate21.checked_322 line 457
  229. def OAI.SnakyPrototype.Certificate21.height_325 line 465
  230. def OAI.SnakyPrototype.Certificate21.childrenH_325 line 466
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_325 line 467
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_325 line 468
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_325 line 470
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_325 line 474
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_325 line 476
  236. def OAI.SnakyPrototype.Certificate21.checked_325 line 480
  237. def OAI.SnakyPrototype.Certificate21.height_326 line 488
  238. def OAI.SnakyPrototype.Certificate21.childrenH_326 line 489
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_326 line 490
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_326 line 491
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_326 line 493
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_326 line 497
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_326 line 499
  244. def OAI.SnakyPrototype.Certificate21.checked_326 line 503
  245. def OAI.SnakyPrototype.Certificate21.height_327 line 511
  246. def OAI.SnakyPrototype.Certificate21.childrenH_327 line 512
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_327 line 513
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_327 line 514
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_327 line 516
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_327 line 520
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_327 line 522
  252. def OAI.SnakyPrototype.Certificate21.checked_327 line 526
  253. def OAI.SnakyPrototype.Certificate21.height_328 line 534
  254. def OAI.SnakyPrototype.Certificate21.childrenH_328 line 535
  255. theorem OAI.SnakyPrototype.Certificate21.height_exact_328 line 536
  256. theorem OAI.SnakyPrototype.Certificate21.required_origin_328 line 537
  257. theorem OAI.SnakyPrototype.Certificate21.required_exact_328 line 539
  258. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_328 line 543
  259. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_328 line 545
  260. def OAI.SnakyPrototype.Certificate21.checked_328 line 549
  261. def OAI.SnakyPrototype.Certificate21.height_330 line 557
  262. def OAI.SnakyPrototype.Certificate21.childrenH_330 line 558
  263. theorem OAI.SnakyPrototype.Certificate21.height_exact_330 line 559
  264. theorem OAI.SnakyPrototype.Certificate21.required_origin_330 line 560
  265. theorem OAI.SnakyPrototype.Certificate21.required_exact_330 line 562
  266. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_330 line 566
  267. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_330 line 568
  268. def OAI.SnakyPrototype.Certificate21.checked_330 line 572
  269. def OAI.SnakyPrototype.Certificate21.height_368 line 580
  270. def OAI.SnakyPrototype.Certificate21.childrenH_368 line 581
  271. theorem OAI.SnakyPrototype.Certificate21.height_exact_368 line 582
  272. theorem OAI.SnakyPrototype.Certificate21.required_origin_368 line 583
  273. theorem OAI.SnakyPrototype.Certificate21.required_exact_368 line 585
  274. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_368 line 589
  275. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_368 line 591
  276. def OAI.SnakyPrototype.Certificate21.checked_368 line 595
  277. def OAI.SnakyPrototype.Certificate21.height_380_i0 line 603
  278. def OAI.SnakyPrototype.Certificate21.childrenH_380_i0 line 604
  279. theorem OAI.SnakyPrototype.Certificate21.height_exact_380_i0 line 605
  280. theorem OAI.SnakyPrototype.Certificate21.required_origin_380_i0 line 606
  281. theorem OAI.SnakyPrototype.Certificate21.required_exact_380_i0 line 608
  282. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_380_i0 line 612
  283. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_380_i0 line 614
  284. def OAI.SnakyPrototype.Certificate21.checked_380_i0 line 618
  285. def OAI.SnakyPrototype.Certificate21.height_380 line 626
  286. def OAI.SnakyPrototype.Certificate21.childrenH_380 line 627
  287. theorem OAI.SnakyPrototype.Certificate21.height_exact_380 line 628
  288. theorem OAI.SnakyPrototype.Certificate21.required_origin_380 line 629
  289. theorem OAI.SnakyPrototype.Certificate21.required_exact_380 line 631
  290. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_380 line 635
  291. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_380 line 637
  292. def OAI.SnakyPrototype.Certificate21.checked_380 line 641
  293. def OAI.SnakyPrototype.Certificate21.height_396 line 649
  294. def OAI.SnakyPrototype.Certificate21.childrenH_396 line 650
  295. theorem OAI.SnakyPrototype.Certificate21.height_exact_396 line 651
  296. theorem OAI.SnakyPrototype.Certificate21.required_origin_396 line 652
  297. theorem OAI.SnakyPrototype.Certificate21.required_exact_396 line 654
  298. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_396 line 658
  299. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_396 line 660
  300. def OAI.SnakyPrototype.Certificate21.checked_396 line 664
  301. def OAI.SnakyPrototype.Certificate21.height_397 line 672
  302. def OAI.SnakyPrototype.Certificate21.childrenH_397 line 673
  303. theorem OAI.SnakyPrototype.Certificate21.height_exact_397 line 674
  304. theorem OAI.SnakyPrototype.Certificate21.required_origin_397 line 675
  305. theorem OAI.SnakyPrototype.Certificate21.required_exact_397 line 677
  306. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_397 line 681
  307. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_397 line 683
  308. def OAI.SnakyPrototype.Certificate21.checked_397 line 687
  309. def OAI.SnakyPrototype.Certificate21.height_398 line 695
  310. def OAI.SnakyPrototype.Certificate21.childrenH_398 line 696
  311. theorem OAI.SnakyPrototype.Certificate21.height_exact_398 line 697
  312. theorem OAI.SnakyPrototype.Certificate21.required_origin_398 line 698
  313. theorem OAI.SnakyPrototype.Certificate21.required_exact_398 line 700
  314. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_398 line 704
  315. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_398 line 706
  316. def OAI.SnakyPrototype.Certificate21.checked_398 line 710
  317. def OAI.SnakyPrototype.Certificate21.height_400 line 718
  318. def OAI.SnakyPrototype.Certificate21.childrenH_400 line 719
  319. theorem OAI.SnakyPrototype.Certificate21.height_exact_400 line 720
  320. theorem OAI.SnakyPrototype.Certificate21.required_origin_400 line 721
  321. theorem OAI.SnakyPrototype.Certificate21.required_exact_400 line 723
  322. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_400 line 727
  323. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_400 line 729
  324. def OAI.SnakyPrototype.Certificate21.checked_400 line 733
  325. def OAI.SnakyPrototype.Certificate21.height_406 line 741
  326. def OAI.SnakyPrototype.Certificate21.childrenH_406 line 742
  327. theorem OAI.SnakyPrototype.Certificate21.height_exact_406 line 743
  328. theorem OAI.SnakyPrototype.Certificate21.required_origin_406 line 744
  329. theorem OAI.SnakyPrototype.Certificate21.required_exact_406 line 746
  330. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_406 line 750
  331. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_406 line 752
  332. def OAI.SnakyPrototype.Certificate21.checked_406 line 756
  333. def OAI.SnakyPrototype.Certificate21.height_407_i0 line 764
  334. def OAI.SnakyPrototype.Certificate21.childrenH_407_i0 line 765
  335. theorem OAI.SnakyPrototype.Certificate21.height_exact_407_i0 line 766
  336. theorem OAI.SnakyPrototype.Certificate21.required_origin_407_i0 line 767
  337. theorem OAI.SnakyPrototype.Certificate21.required_exact_407_i0 line 769
  338. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_407_i0 line 773
  339. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_407_i0 line 775
  340. def OAI.SnakyPrototype.Certificate21.checked_407_i0 line 779
  341. def OAI.SnakyPrototype.Certificate21.height_407 line 787
  342. def OAI.SnakyPrototype.Certificate21.childrenH_407 line 788
  343. theorem OAI.SnakyPrototype.Certificate21.height_exact_407 line 789
  344. theorem OAI.SnakyPrototype.Certificate21.required_origin_407 line 790
  345. theorem OAI.SnakyPrototype.Certificate21.required_exact_407 line 792
  346. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_407 line 796
  347. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_407 line 798
  348. def OAI.SnakyPrototype.Certificate21.checked_407 line 802
  349. def OAI.SnakyPrototype.Certificate21.height_421 line 810
  350. def OAI.SnakyPrototype.Certificate21.childrenH_421 line 811
  351. theorem OAI.SnakyPrototype.Certificate21.height_exact_421 line 812
  352. theorem OAI.SnakyPrototype.Certificate21.required_origin_421 line 813
  353. theorem OAI.SnakyPrototype.Certificate21.required_exact_421 line 815
  354. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_421 line 819
  355. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_421 line 821
  356. def OAI.SnakyPrototype.Certificate21.checked_421 line 825
  357. def OAI.SnakyPrototype.Certificate21.height_434_i0 line 833
  358. def OAI.SnakyPrototype.Certificate21.childrenH_434_i0 line 834
  359. theorem OAI.SnakyPrototype.Certificate21.height_exact_434_i0 line 835
  360. theorem OAI.SnakyPrototype.Certificate21.required_origin_434_i0 line 836
  361. theorem OAI.SnakyPrototype.Certificate21.required_exact_434_i0 line 838
  362. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_434_i0 line 842
  363. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_434_i0 line 844
  364. def OAI.SnakyPrototype.Certificate21.checked_434_i0 line 848
  365. def OAI.SnakyPrototype.Certificate21.height_434_i1 line 856
  366. def OAI.SnakyPrototype.Certificate21.childrenH_434_i1 line 857
  367. theorem OAI.SnakyPrototype.Certificate21.height_exact_434_i1 line 858
  368. theorem OAI.SnakyPrototype.Certificate21.required_origin_434_i1 line 859
  369. theorem OAI.SnakyPrototype.Certificate21.required_exact_434_i1 line 861
  370. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_434_i1 line 865
  371. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_434_i1 line 867
  372. def OAI.SnakyPrototype.Certificate21.checked_434_i1 line 871
  373. def OAI.SnakyPrototype.Certificate21.height_434 line 879
  374. def OAI.SnakyPrototype.Certificate21.childrenH_434 line 880
  375. theorem OAI.SnakyPrototype.Certificate21.height_exact_434 line 881
  376. theorem OAI.SnakyPrototype.Certificate21.required_origin_434 line 882
  377. theorem OAI.SnakyPrototype.Certificate21.required_exact_434 line 884
  378. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_434 line 888
  379. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_434 line 890
  380. def OAI.SnakyPrototype.Certificate21.checked_434 line 894
  381. def OAI.SnakyPrototype.Certificate21.height_441 line 902
  382. def OAI.SnakyPrototype.Certificate21.childrenH_441 line 903
  383. theorem OAI.SnakyPrototype.Certificate21.height_exact_441 line 904
  384. theorem OAI.SnakyPrototype.Certificate21.required_origin_441 line 905
  385. theorem OAI.SnakyPrototype.Certificate21.required_exact_441 line 907
  386. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_441 line 911
  387. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_441 line 913
  388. def OAI.SnakyPrototype.Certificate21.checked_441 line 917
  389. def OAI.SnakyPrototype.Certificate21.height_442 line 925
  390. def OAI.SnakyPrototype.Certificate21.childrenH_442 line 926
  391. theorem OAI.SnakyPrototype.Certificate21.height_exact_442 line 927
  392. theorem OAI.SnakyPrototype.Certificate21.required_origin_442 line 928
  393. theorem OAI.SnakyPrototype.Certificate21.required_exact_442 line 930
  394. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_442 line 934
  395. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_442 line 936
  396. def OAI.SnakyPrototype.Certificate21.checked_442 line 940