OAI/GameTheory/SnakyTwentyOne/Cards/Height09Part02.lean

GitHub source file

324 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_443_i6 line 14
  2. def OAI.SnakyPrototype.Certificate21.envelope_443_i6 line 15
  3. def OAI.SnakyPrototype.Certificate21.childrenC_443_i6 line 16
  4. def OAI.SnakyPrototype.Certificate21.childrenD_443_i6 line 17
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_443_i6 line 18
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_443_i6 line 19
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_443_i6 line 20
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_443_i6 line 21
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_443_i6 line 22
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_443_i6 line 27
  11. def OAI.SnakyPrototype.Certificate21.required_443_i5 line 32
  12. def OAI.SnakyPrototype.Certificate21.envelope_443_i5 line 33
  13. def OAI.SnakyPrototype.Certificate21.childrenC_443_i5 line 34
  14. def OAI.SnakyPrototype.Certificate21.childrenD_443_i5 line 35
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_443_i5 line 36
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_443_i5 line 37
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_443_i5 line 38
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_443_i5 line 39
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_443_i5 line 40
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_443_i5 line 45
  21. def OAI.SnakyPrototype.Certificate21.required_443_i4 line 50
  22. def OAI.SnakyPrototype.Certificate21.envelope_443_i4 line 51
  23. def OAI.SnakyPrototype.Certificate21.childrenC_443_i4 line 52
  24. def OAI.SnakyPrototype.Certificate21.childrenD_443_i4 line 53
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_443_i4 line 54
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_443_i4 line 55
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_443_i4 line 56
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_443_i4 line 57
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_443_i4 line 58
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_443_i4 line 63
  31. def OAI.SnakyPrototype.Certificate21.required_443_i3 line 68
  32. def OAI.SnakyPrototype.Certificate21.envelope_443_i3 line 69
  33. def OAI.SnakyPrototype.Certificate21.childrenC_443_i3 line 70
  34. def OAI.SnakyPrototype.Certificate21.childrenD_443_i3 line 71
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_443_i3 line 72
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_443_i3 line 73
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_443_i3 line 74
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_443_i3 line 75
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_443_i3 line 76
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_443_i3 line 81
  41. def OAI.SnakyPrototype.Certificate21.required_443_i2 line 86
  42. def OAI.SnakyPrototype.Certificate21.envelope_443_i2 line 87
  43. def OAI.SnakyPrototype.Certificate21.childrenC_443_i2 line 88
  44. def OAI.SnakyPrototype.Certificate21.childrenD_443_i2 line 89
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_443_i2 line 90
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_443_i2 line 91
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_443_i2 line 92
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_443_i2 line 93
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_443_i2 line 94
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_443_i2 line 99
  51. def OAI.SnakyPrototype.Certificate21.required_443_i1 line 104
  52. def OAI.SnakyPrototype.Certificate21.envelope_443_i1 line 105
  53. def OAI.SnakyPrototype.Certificate21.childrenC_443_i1 line 106
  54. def OAI.SnakyPrototype.Certificate21.childrenD_443_i1 line 107
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_443_i1 line 108
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_443_i1 line 109
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_443_i1 line 110
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_443_i1 line 111
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_443_i1 line 112
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_443_i1 line 117
  61. def OAI.SnakyPrototype.Certificate21.required_443_i0 line 122
  62. def OAI.SnakyPrototype.Certificate21.envelope_443_i0 line 123
  63. def OAI.SnakyPrototype.Certificate21.childrenC_443_i0 line 124
  64. def OAI.SnakyPrototype.Certificate21.childrenD_443_i0 line 125
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_443_i0 line 126
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_443_i0 line 127
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_443_i0 line 128
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_443_i0 line 129
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_443_i0 line 130
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_443_i0 line 135
  71. def OAI.SnakyPrototype.Certificate21.required_443 line 140
  72. def OAI.SnakyPrototype.Certificate21.envelope_443 line 141
  73. def OAI.SnakyPrototype.Certificate21.childrenC_443 line 142
  74. def OAI.SnakyPrototype.Certificate21.childrenD_443 line 143
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_443 line 144
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_443 line 145
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_443 line 146
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_443 line 147
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_443 line 148
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_443 line 153
  81. def OAI.SnakyPrototype.Certificate21.required_449 line 158
  82. def OAI.SnakyPrototype.Certificate21.envelope_449 line 159
  83. def OAI.SnakyPrototype.Certificate21.childrenC_449 line 160
  84. def OAI.SnakyPrototype.Certificate21.childrenD_449 line 161
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_449 line 162
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_449 line 163
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_449 line 164
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_449 line 165
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_449 line 166
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_449 line 174
  91. def OAI.SnakyPrototype.Certificate21.required_450 line 179
  92. def OAI.SnakyPrototype.Certificate21.envelope_450 line 180
  93. def OAI.SnakyPrototype.Certificate21.childrenC_450 line 181
  94. def OAI.SnakyPrototype.Certificate21.childrenD_450 line 182
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_450 line 183
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_450 line 184
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_450 line 185
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_450 line 186
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_450 line 187
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_450 line 192
  101. def OAI.SnakyPrototype.Certificate21.required_457 line 197
  102. def OAI.SnakyPrototype.Certificate21.envelope_457 line 198
  103. def OAI.SnakyPrototype.Certificate21.childrenC_457 line 199
  104. def OAI.SnakyPrototype.Certificate21.childrenD_457 line 200
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_457 line 201
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_457 line 202
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_457 line 203
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_457 line 204
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_457 line 205
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_457 line 212
  111. def OAI.SnakyPrototype.Certificate21.required_458 line 217
  112. def OAI.SnakyPrototype.Certificate21.envelope_458 line 218
  113. def OAI.SnakyPrototype.Certificate21.childrenC_458 line 219
  114. def OAI.SnakyPrototype.Certificate21.childrenD_458 line 220
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_458 line 221
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_458 line 222
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_458 line 223
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_458 line 224
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_458 line 225
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_458 line 232
  121. def OAI.SnakyPrototype.Certificate21.required_470_i0 line 237
  122. def OAI.SnakyPrototype.Certificate21.envelope_470_i0 line 238
  123. def OAI.SnakyPrototype.Certificate21.childrenC_470_i0 line 239
  124. def OAI.SnakyPrototype.Certificate21.childrenD_470_i0 line 240
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_470_i0 line 241
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_470_i0 line 242
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_470_i0 line 243
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_470_i0 line 244
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_470_i0 line 245
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_470_i0 line 250
  131. def OAI.SnakyPrototype.Certificate21.required_470_i2 line 255
  132. def OAI.SnakyPrototype.Certificate21.envelope_470_i2 line 256
  133. def OAI.SnakyPrototype.Certificate21.childrenC_470_i2 line 257
  134. def OAI.SnakyPrototype.Certificate21.childrenD_470_i2 line 258
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_470_i2 line 259
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_470_i2 line 260
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_470_i2 line 261
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_470_i2 line 262
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_470_i2 line 263
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_470_i2 line 268
  141. def OAI.SnakyPrototype.Certificate21.required_470_i1 line 273
  142. def OAI.SnakyPrototype.Certificate21.envelope_470_i1 line 274
  143. def OAI.SnakyPrototype.Certificate21.childrenC_470_i1 line 275
  144. def OAI.SnakyPrototype.Certificate21.childrenD_470_i1 line 276
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_470_i1 line 277
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_470_i1 line 278
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_470_i1 line 279
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_470_i1 line 280
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_470_i1 line 281
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_470_i1 line 286
  151. def OAI.SnakyPrototype.Certificate21.required_470 line 291
  152. def OAI.SnakyPrototype.Certificate21.envelope_470 line 292
  153. def OAI.SnakyPrototype.Certificate21.childrenC_470 line 293
  154. def OAI.SnakyPrototype.Certificate21.childrenD_470 line 294
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_470 line 295
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_470 line 296
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_470 line 297
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_470 line 298
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_470 line 299
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_470 line 306
  161. def OAI.SnakyPrototype.Certificate21.required_474 line 311
  162. def OAI.SnakyPrototype.Certificate21.envelope_474 line 312
  163. def OAI.SnakyPrototype.Certificate21.childrenC_474 line 313
  164. def OAI.SnakyPrototype.Certificate21.childrenD_474 line 314
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_474 line 315
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_474 line 316
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_474 line 317
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_474 line 318
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_474 line 319
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_474 line 326
  171. def OAI.SnakyPrototype.Certificate21.required_477 line 331
  172. def OAI.SnakyPrototype.Certificate21.envelope_477 line 332
  173. def OAI.SnakyPrototype.Certificate21.childrenC_477 line 333
  174. def OAI.SnakyPrototype.Certificate21.childrenD_477 line 334
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_477 line 335
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_477 line 336
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_477 line 337
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_477 line 338
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_477 line 339
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_477 line 346
  181. def OAI.SnakyPrototype.Certificate21.height_443_i6 line 351
  182. def OAI.SnakyPrototype.Certificate21.childrenH_443_i6 line 352
  183. theorem OAI.SnakyPrototype.Certificate21.height_exact_443_i6 line 353
  184. theorem OAI.SnakyPrototype.Certificate21.required_origin_443_i6 line 354
  185. theorem OAI.SnakyPrototype.Certificate21.required_exact_443_i6 line 356
  186. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_443_i6 line 360
  187. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_443_i6 line 362
  188. def OAI.SnakyPrototype.Certificate21.checked_443_i6 line 366
  189. def OAI.SnakyPrototype.Certificate21.height_443_i5 line 374
  190. def OAI.SnakyPrototype.Certificate21.childrenH_443_i5 line 375
  191. theorem OAI.SnakyPrototype.Certificate21.height_exact_443_i5 line 376
  192. theorem OAI.SnakyPrototype.Certificate21.required_origin_443_i5 line 377
  193. theorem OAI.SnakyPrototype.Certificate21.required_exact_443_i5 line 379
  194. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_443_i5 line 383
  195. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_443_i5 line 385
  196. def OAI.SnakyPrototype.Certificate21.checked_443_i5 line 389
  197. def OAI.SnakyPrototype.Certificate21.height_443_i4 line 397
  198. def OAI.SnakyPrototype.Certificate21.childrenH_443_i4 line 398
  199. theorem OAI.SnakyPrototype.Certificate21.height_exact_443_i4 line 399
  200. theorem OAI.SnakyPrototype.Certificate21.required_origin_443_i4 line 400
  201. theorem OAI.SnakyPrototype.Certificate21.required_exact_443_i4 line 402
  202. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_443_i4 line 406
  203. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_443_i4 line 408
  204. def OAI.SnakyPrototype.Certificate21.checked_443_i4 line 412
  205. def OAI.SnakyPrototype.Certificate21.height_443_i3 line 420
  206. def OAI.SnakyPrototype.Certificate21.childrenH_443_i3 line 421
  207. theorem OAI.SnakyPrototype.Certificate21.height_exact_443_i3 line 422
  208. theorem OAI.SnakyPrototype.Certificate21.required_origin_443_i3 line 423
  209. theorem OAI.SnakyPrototype.Certificate21.required_exact_443_i3 line 425
  210. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_443_i3 line 429
  211. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_443_i3 line 431
  212. def OAI.SnakyPrototype.Certificate21.checked_443_i3 line 435
  213. def OAI.SnakyPrototype.Certificate21.height_443_i2 line 443
  214. def OAI.SnakyPrototype.Certificate21.childrenH_443_i2 line 444
  215. theorem OAI.SnakyPrototype.Certificate21.height_exact_443_i2 line 445
  216. theorem OAI.SnakyPrototype.Certificate21.required_origin_443_i2 line 446
  217. theorem OAI.SnakyPrototype.Certificate21.required_exact_443_i2 line 448
  218. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_443_i2 line 452
  219. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_443_i2 line 454
  220. def OAI.SnakyPrototype.Certificate21.checked_443_i2 line 458
  221. def OAI.SnakyPrototype.Certificate21.height_443_i1 line 466
  222. def OAI.SnakyPrototype.Certificate21.childrenH_443_i1 line 467
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_443_i1 line 468
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_443_i1 line 469
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_443_i1 line 471
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_443_i1 line 475
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_443_i1 line 477
  228. def OAI.SnakyPrototype.Certificate21.checked_443_i1 line 481
  229. def OAI.SnakyPrototype.Certificate21.height_443_i0 line 489
  230. def OAI.SnakyPrototype.Certificate21.childrenH_443_i0 line 490
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_443_i0 line 491
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_443_i0 line 492
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_443_i0 line 494
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_443_i0 line 498
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_443_i0 line 500
  236. def OAI.SnakyPrototype.Certificate21.checked_443_i0 line 504
  237. def OAI.SnakyPrototype.Certificate21.height_443 line 512
  238. def OAI.SnakyPrototype.Certificate21.childrenH_443 line 513
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_443 line 514
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_443 line 515
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_443 line 517
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_443 line 521
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_443 line 523
  244. def OAI.SnakyPrototype.Certificate21.checked_443 line 527
  245. def OAI.SnakyPrototype.Certificate21.height_449 line 535
  246. def OAI.SnakyPrototype.Certificate21.childrenH_449 line 536
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_449 line 537
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_449 line 538
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_449 line 540
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_449 line 544
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_449 line 546
  252. def OAI.SnakyPrototype.Certificate21.checked_449 line 550
  253. def OAI.SnakyPrototype.Certificate21.height_450 line 558
  254. def OAI.SnakyPrototype.Certificate21.childrenH_450 line 559
  255. theorem OAI.SnakyPrototype.Certificate21.height_exact_450 line 560
  256. theorem OAI.SnakyPrototype.Certificate21.required_origin_450 line 561
  257. theorem OAI.SnakyPrototype.Certificate21.required_exact_450 line 563
  258. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_450 line 567
  259. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_450 line 569
  260. def OAI.SnakyPrototype.Certificate21.checked_450 line 573
  261. def OAI.SnakyPrototype.Certificate21.height_457 line 581
  262. def OAI.SnakyPrototype.Certificate21.childrenH_457 line 582
  263. theorem OAI.SnakyPrototype.Certificate21.height_exact_457 line 583
  264. theorem OAI.SnakyPrototype.Certificate21.required_origin_457 line 584
  265. theorem OAI.SnakyPrototype.Certificate21.required_exact_457 line 586
  266. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_457 line 590
  267. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_457 line 592
  268. def OAI.SnakyPrototype.Certificate21.checked_457 line 596
  269. def OAI.SnakyPrototype.Certificate21.height_458 line 604
  270. def OAI.SnakyPrototype.Certificate21.childrenH_458 line 605
  271. theorem OAI.SnakyPrototype.Certificate21.height_exact_458 line 606
  272. theorem OAI.SnakyPrototype.Certificate21.required_origin_458 line 607
  273. theorem OAI.SnakyPrototype.Certificate21.required_exact_458 line 609
  274. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_458 line 613
  275. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_458 line 615
  276. def OAI.SnakyPrototype.Certificate21.checked_458 line 619
  277. def OAI.SnakyPrototype.Certificate21.height_470_i0 line 627
  278. def OAI.SnakyPrototype.Certificate21.childrenH_470_i0 line 628
  279. theorem OAI.SnakyPrototype.Certificate21.height_exact_470_i0 line 629
  280. theorem OAI.SnakyPrototype.Certificate21.required_origin_470_i0 line 630
  281. theorem OAI.SnakyPrototype.Certificate21.required_exact_470_i0 line 632
  282. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_470_i0 line 636
  283. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_470_i0 line 638
  284. def OAI.SnakyPrototype.Certificate21.checked_470_i0 line 642
  285. def OAI.SnakyPrototype.Certificate21.height_470_i2 line 650
  286. def OAI.SnakyPrototype.Certificate21.childrenH_470_i2 line 651
  287. theorem OAI.SnakyPrototype.Certificate21.height_exact_470_i2 line 652
  288. theorem OAI.SnakyPrototype.Certificate21.required_origin_470_i2 line 653
  289. theorem OAI.SnakyPrototype.Certificate21.required_exact_470_i2 line 655
  290. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_470_i2 line 659
  291. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_470_i2 line 661
  292. def OAI.SnakyPrototype.Certificate21.checked_470_i2 line 665
  293. def OAI.SnakyPrototype.Certificate21.height_470_i1 line 673
  294. def OAI.SnakyPrototype.Certificate21.childrenH_470_i1 line 674
  295. theorem OAI.SnakyPrototype.Certificate21.height_exact_470_i1 line 675
  296. theorem OAI.SnakyPrototype.Certificate21.required_origin_470_i1 line 676
  297. theorem OAI.SnakyPrototype.Certificate21.required_exact_470_i1 line 678
  298. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_470_i1 line 682
  299. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_470_i1 line 684
  300. def OAI.SnakyPrototype.Certificate21.checked_470_i1 line 688
  301. def OAI.SnakyPrototype.Certificate21.height_470 line 696
  302. def OAI.SnakyPrototype.Certificate21.childrenH_470 line 697
  303. theorem OAI.SnakyPrototype.Certificate21.height_exact_470 line 698
  304. theorem OAI.SnakyPrototype.Certificate21.required_origin_470 line 699
  305. theorem OAI.SnakyPrototype.Certificate21.required_exact_470 line 701
  306. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_470 line 705
  307. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_470 line 707
  308. def OAI.SnakyPrototype.Certificate21.checked_470 line 711
  309. def OAI.SnakyPrototype.Certificate21.height_474 line 719
  310. def OAI.SnakyPrototype.Certificate21.childrenH_474 line 720
  311. theorem OAI.SnakyPrototype.Certificate21.height_exact_474 line 721
  312. theorem OAI.SnakyPrototype.Certificate21.required_origin_474 line 722
  313. theorem OAI.SnakyPrototype.Certificate21.required_exact_474 line 724
  314. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_474 line 728
  315. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_474 line 730
  316. def OAI.SnakyPrototype.Certificate21.checked_474 line 734
  317. def OAI.SnakyPrototype.Certificate21.height_477 line 742
  318. def OAI.SnakyPrototype.Certificate21.childrenH_477 line 743
  319. theorem OAI.SnakyPrototype.Certificate21.height_exact_477 line 744
  320. theorem OAI.SnakyPrototype.Certificate21.required_origin_477 line 745
  321. theorem OAI.SnakyPrototype.Certificate21.required_exact_477 line 747
  322. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_477 line 751
  323. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_477 line 753
  324. def OAI.SnakyPrototype.Certificate21.checked_477 line 757