OAI/GameTheory/SnakyTwentyOne/Cards/Height12Part05.lean

GitHub source file

306 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_715_i1 line 37
  2. def OAI.SnakyPrototype.Certificate21.envelope_715_i1 line 38
  3. def OAI.SnakyPrototype.Certificate21.childrenC_715_i1 line 39
  4. def OAI.SnakyPrototype.Certificate21.childrenD_715_i1 line 40
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_715_i1 line 41
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_715_i1 line 42
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_715_i1 line 43
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_715_i1 line 44
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_715_i1 line 45
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_715_i1 line 52
  11. def OAI.SnakyPrototype.Certificate21.required_715_i0 line 57
  12. def OAI.SnakyPrototype.Certificate21.envelope_715_i0 line 58
  13. def OAI.SnakyPrototype.Certificate21.childrenC_715_i0 line 59
  14. def OAI.SnakyPrototype.Certificate21.childrenD_715_i0 line 60
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_715_i0 line 61
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_715_i0 line 62
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_715_i0 line 63
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_715_i0 line 64
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_715_i0 line 65
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_715_i0 line 72
  21. def OAI.SnakyPrototype.Certificate21.required_715_i4 line 77
  22. def OAI.SnakyPrototype.Certificate21.envelope_715_i4 line 78
  23. def OAI.SnakyPrototype.Certificate21.childrenC_715_i4 line 79
  24. def OAI.SnakyPrototype.Certificate21.childrenD_715_i4 line 80
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_715_i4 line 81
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_715_i4 line 82
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_715_i4 line 83
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_715_i4 line 84
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_715_i4 line 85
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_715_i4 line 92
  31. def OAI.SnakyPrototype.Certificate21.required_715_i3 line 97
  32. def OAI.SnakyPrototype.Certificate21.envelope_715_i3 line 98
  33. def OAI.SnakyPrototype.Certificate21.childrenC_715_i3 line 99
  34. def OAI.SnakyPrototype.Certificate21.childrenD_715_i3 line 100
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_715_i3 line 101
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_715_i3 line 102
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_715_i3 line 103
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_715_i3 line 104
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_715_i3 line 105
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_715_i3 line 112
  41. def OAI.SnakyPrototype.Certificate21.required_715_i2 line 117
  42. def OAI.SnakyPrototype.Certificate21.envelope_715_i2 line 118
  43. def OAI.SnakyPrototype.Certificate21.childrenC_715_i2 line 119
  44. def OAI.SnakyPrototype.Certificate21.childrenD_715_i2 line 120
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_715_i2 line 121
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_715_i2 line 122
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_715_i2 line 123
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_715_i2 line 124
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_715_i2 line 125
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_715_i2 line 133
  51. def OAI.SnakyPrototype.Certificate21.required_715 line 138
  52. def OAI.SnakyPrototype.Certificate21.envelope_715 line 139
  53. def OAI.SnakyPrototype.Certificate21.childrenC_715 line 140
  54. def OAI.SnakyPrototype.Certificate21.childrenD_715 line 141
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_715 line 142
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_715 line 143
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_715 line 144
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_715 line 145
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_715 line 146
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_715 line 157
  61. def OAI.SnakyPrototype.Certificate21.required_717 line 162
  62. def OAI.SnakyPrototype.Certificate21.envelope_717 line 163
  63. def OAI.SnakyPrototype.Certificate21.childrenC_717 line 164
  64. def OAI.SnakyPrototype.Certificate21.childrenD_717 line 165
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_717 line 166
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_717 line 167
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_717 line 168
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_717 line 169
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_717 line 170
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_717 line 183
  71. def OAI.SnakyPrototype.Certificate21.required_723_i0 line 188
  72. def OAI.SnakyPrototype.Certificate21.envelope_723_i0 line 189
  73. def OAI.SnakyPrototype.Certificate21.childrenC_723_i0 line 190
  74. def OAI.SnakyPrototype.Certificate21.childrenD_723_i0 line 191
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_723_i0 line 192
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_723_i0 line 193
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_723_i0 line 194
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_723_i0 line 195
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_723_i0 line 196
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_723_i0 line 201
  81. def OAI.SnakyPrototype.Certificate21.required_723_i1 line 206
  82. def OAI.SnakyPrototype.Certificate21.envelope_723_i1 line 207
  83. def OAI.SnakyPrototype.Certificate21.childrenC_723_i1 line 208
  84. def OAI.SnakyPrototype.Certificate21.childrenD_723_i1 line 209
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_723_i1 line 210
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_723_i1 line 211
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_723_i1 line 212
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_723_i1 line 213
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_723_i1 line 214
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_723_i1 line 220
  91. def OAI.SnakyPrototype.Certificate21.required_723_i4 line 225
  92. def OAI.SnakyPrototype.Certificate21.envelope_723_i4 line 226
  93. def OAI.SnakyPrototype.Certificate21.childrenC_723_i4 line 227
  94. def OAI.SnakyPrototype.Certificate21.childrenD_723_i4 line 228
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_723_i4 line 229
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_723_i4 line 230
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_723_i4 line 231
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_723_i4 line 232
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_723_i4 line 233
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_723_i4 line 239
  101. def OAI.SnakyPrototype.Certificate21.required_723_i3 line 244
  102. def OAI.SnakyPrototype.Certificate21.envelope_723_i3 line 245
  103. def OAI.SnakyPrototype.Certificate21.childrenC_723_i3 line 246
  104. def OAI.SnakyPrototype.Certificate21.childrenD_723_i3 line 247
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_723_i3 line 248
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_723_i3 line 249
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_723_i3 line 250
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_723_i3 line 251
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_723_i3 line 252
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_723_i3 line 259
  111. def OAI.SnakyPrototype.Certificate21.required_723_i5 line 264
  112. def OAI.SnakyPrototype.Certificate21.envelope_723_i5 line 265
  113. def OAI.SnakyPrototype.Certificate21.childrenC_723_i5 line 266
  114. def OAI.SnakyPrototype.Certificate21.childrenD_723_i5 line 267
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_723_i5 line 268
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_723_i5 line 269
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_723_i5 line 270
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_723_i5 line 271
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_723_i5 line 272
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_723_i5 line 279
  121. def OAI.SnakyPrototype.Certificate21.required_723_i7 line 284
  122. def OAI.SnakyPrototype.Certificate21.envelope_723_i7 line 285
  123. def OAI.SnakyPrototype.Certificate21.childrenC_723_i7 line 286
  124. def OAI.SnakyPrototype.Certificate21.childrenD_723_i7 line 287
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_723_i7 line 288
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_723_i7 line 289
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_723_i7 line 290
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_723_i7 line 291
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_723_i7 line 292
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_723_i7 line 297
  131. def OAI.SnakyPrototype.Certificate21.required_723_i6 line 302
  132. def OAI.SnakyPrototype.Certificate21.envelope_723_i6 line 303
  133. def OAI.SnakyPrototype.Certificate21.childrenC_723_i6 line 304
  134. def OAI.SnakyPrototype.Certificate21.childrenD_723_i6 line 305
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_723_i6 line 306
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_723_i6 line 307
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_723_i6 line 308
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_723_i6 line 309
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_723_i6 line 310
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_723_i6 line 317
  141. def OAI.SnakyPrototype.Certificate21.required_723_i8 line 322
  142. def OAI.SnakyPrototype.Certificate21.envelope_723_i8 line 323
  143. def OAI.SnakyPrototype.Certificate21.childrenC_723_i8 line 324
  144. def OAI.SnakyPrototype.Certificate21.childrenD_723_i8 line 325
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_723_i8 line 326
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_723_i8 line 327
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_723_i8 line 328
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_723_i8 line 329
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_723_i8 line 330
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_723_i8 line 339
  151. def OAI.SnakyPrototype.Certificate21.required_723_i2 line 344
  152. def OAI.SnakyPrototype.Certificate21.envelope_723_i2 line 345
  153. def OAI.SnakyPrototype.Certificate21.childrenC_723_i2 line 346
  154. def OAI.SnakyPrototype.Certificate21.childrenD_723_i2 line 347
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_723_i2 line 348
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_723_i2 line 349
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_723_i2 line 350
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_723_i2 line 351
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_723_i2 line 352
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_723_i2 line 361
  161. def OAI.SnakyPrototype.Certificate21.required_723 line 366
  162. def OAI.SnakyPrototype.Certificate21.envelope_723 line 367
  163. def OAI.SnakyPrototype.Certificate21.childrenC_723 line 368
  164. def OAI.SnakyPrototype.Certificate21.childrenD_723 line 369
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_723 line 370
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_723 line 371
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_723 line 372
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_723 line 373
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_723 line 374
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_723 line 382
  171. def OAI.SnakyPrototype.Certificate21.height_715_i1 line 387
  172. def OAI.SnakyPrototype.Certificate21.childrenH_715_i1 line 388
  173. theorem OAI.SnakyPrototype.Certificate21.height_exact_715_i1 line 389
  174. theorem OAI.SnakyPrototype.Certificate21.required_origin_715_i1 line 390
  175. theorem OAI.SnakyPrototype.Certificate21.required_exact_715_i1 line 392
  176. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_715_i1 line 396
  177. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_715_i1 line 398
  178. def OAI.SnakyPrototype.Certificate21.checked_715_i1 line 402
  179. def OAI.SnakyPrototype.Certificate21.height_715_i0 line 410
  180. def OAI.SnakyPrototype.Certificate21.childrenH_715_i0 line 411
  181. theorem OAI.SnakyPrototype.Certificate21.height_exact_715_i0 line 412
  182. theorem OAI.SnakyPrototype.Certificate21.required_origin_715_i0 line 413
  183. theorem OAI.SnakyPrototype.Certificate21.required_exact_715_i0 line 415
  184. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_715_i0 line 419
  185. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_715_i0 line 421
  186. def OAI.SnakyPrototype.Certificate21.checked_715_i0 line 425
  187. def OAI.SnakyPrototype.Certificate21.height_715_i4 line 433
  188. def OAI.SnakyPrototype.Certificate21.childrenH_715_i4 line 434
  189. theorem OAI.SnakyPrototype.Certificate21.height_exact_715_i4 line 435
  190. theorem OAI.SnakyPrototype.Certificate21.required_origin_715_i4 line 436
  191. theorem OAI.SnakyPrototype.Certificate21.required_exact_715_i4 line 438
  192. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_715_i4 line 442
  193. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_715_i4 line 444
  194. def OAI.SnakyPrototype.Certificate21.checked_715_i4 line 448
  195. def OAI.SnakyPrototype.Certificate21.height_715_i3 line 456
  196. def OAI.SnakyPrototype.Certificate21.childrenH_715_i3 line 457
  197. theorem OAI.SnakyPrototype.Certificate21.height_exact_715_i3 line 458
  198. theorem OAI.SnakyPrototype.Certificate21.required_origin_715_i3 line 459
  199. theorem OAI.SnakyPrototype.Certificate21.required_exact_715_i3 line 461
  200. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_715_i3 line 465
  201. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_715_i3 line 467
  202. def OAI.SnakyPrototype.Certificate21.checked_715_i3 line 471
  203. def OAI.SnakyPrototype.Certificate21.height_715_i2 line 479
  204. def OAI.SnakyPrototype.Certificate21.childrenH_715_i2 line 480
  205. theorem OAI.SnakyPrototype.Certificate21.height_exact_715_i2 line 481
  206. theorem OAI.SnakyPrototype.Certificate21.required_origin_715_i2 line 482
  207. theorem OAI.SnakyPrototype.Certificate21.required_exact_715_i2 line 484
  208. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_715_i2 line 488
  209. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_715_i2 line 490
  210. def OAI.SnakyPrototype.Certificate21.checked_715_i2 line 494
  211. def OAI.SnakyPrototype.Certificate21.height_715 line 502
  212. def OAI.SnakyPrototype.Certificate21.childrenH_715 line 503
  213. theorem OAI.SnakyPrototype.Certificate21.height_exact_715 line 504
  214. theorem OAI.SnakyPrototype.Certificate21.required_origin_715 line 505
  215. theorem OAI.SnakyPrototype.Certificate21.required_exact_715 line 507
  216. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_715 line 511
  217. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_715 line 513
  218. def OAI.SnakyPrototype.Certificate21.checked_715 line 517
  219. def OAI.SnakyPrototype.Certificate21.height_717 line 525
  220. def OAI.SnakyPrototype.Certificate21.childrenH_717 line 526
  221. theorem OAI.SnakyPrototype.Certificate21.height_exact_717 line 527
  222. theorem OAI.SnakyPrototype.Certificate21.required_origin_717 line 528
  223. theorem OAI.SnakyPrototype.Certificate21.required_exact_717 line 530
  224. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_717 line 534
  225. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_717 line 536
  226. def OAI.SnakyPrototype.Certificate21.checked_717 line 540
  227. def OAI.SnakyPrototype.Certificate21.height_723_i0 line 548
  228. def OAI.SnakyPrototype.Certificate21.childrenH_723_i0 line 549
  229. theorem OAI.SnakyPrototype.Certificate21.height_exact_723_i0 line 550
  230. theorem OAI.SnakyPrototype.Certificate21.required_origin_723_i0 line 551
  231. theorem OAI.SnakyPrototype.Certificate21.required_exact_723_i0 line 553
  232. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_723_i0 line 557
  233. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_723_i0 line 559
  234. def OAI.SnakyPrototype.Certificate21.checked_723_i0 line 563
  235. def OAI.SnakyPrototype.Certificate21.height_723_i1 line 571
  236. def OAI.SnakyPrototype.Certificate21.childrenH_723_i1 line 572
  237. theorem OAI.SnakyPrototype.Certificate21.height_exact_723_i1 line 573
  238. theorem OAI.SnakyPrototype.Certificate21.required_origin_723_i1 line 574
  239. theorem OAI.SnakyPrototype.Certificate21.required_exact_723_i1 line 576
  240. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_723_i1 line 580
  241. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_723_i1 line 582
  242. def OAI.SnakyPrototype.Certificate21.checked_723_i1 line 586
  243. def OAI.SnakyPrototype.Certificate21.height_723_i4 line 594
  244. def OAI.SnakyPrototype.Certificate21.childrenH_723_i4 line 595
  245. theorem OAI.SnakyPrototype.Certificate21.height_exact_723_i4 line 596
  246. theorem OAI.SnakyPrototype.Certificate21.required_origin_723_i4 line 597
  247. theorem OAI.SnakyPrototype.Certificate21.required_exact_723_i4 line 599
  248. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_723_i4 line 603
  249. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_723_i4 line 605
  250. def OAI.SnakyPrototype.Certificate21.checked_723_i4 line 609
  251. def OAI.SnakyPrototype.Certificate21.height_723_i3 line 617
  252. def OAI.SnakyPrototype.Certificate21.childrenH_723_i3 line 618
  253. theorem OAI.SnakyPrototype.Certificate21.height_exact_723_i3 line 619
  254. theorem OAI.SnakyPrototype.Certificate21.required_origin_723_i3 line 620
  255. theorem OAI.SnakyPrototype.Certificate21.required_exact_723_i3 line 622
  256. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_723_i3 line 626
  257. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_723_i3 line 628
  258. def OAI.SnakyPrototype.Certificate21.checked_723_i3 line 632
  259. def OAI.SnakyPrototype.Certificate21.height_723_i5 line 640
  260. def OAI.SnakyPrototype.Certificate21.childrenH_723_i5 line 641
  261. theorem OAI.SnakyPrototype.Certificate21.height_exact_723_i5 line 642
  262. theorem OAI.SnakyPrototype.Certificate21.required_origin_723_i5 line 643
  263. theorem OAI.SnakyPrototype.Certificate21.required_exact_723_i5 line 645
  264. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_723_i5 line 649
  265. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_723_i5 line 651
  266. def OAI.SnakyPrototype.Certificate21.checked_723_i5 line 655
  267. def OAI.SnakyPrototype.Certificate21.height_723_i7 line 663
  268. def OAI.SnakyPrototype.Certificate21.childrenH_723_i7 line 664
  269. theorem OAI.SnakyPrototype.Certificate21.height_exact_723_i7 line 665
  270. theorem OAI.SnakyPrototype.Certificate21.required_origin_723_i7 line 666
  271. theorem OAI.SnakyPrototype.Certificate21.required_exact_723_i7 line 668
  272. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_723_i7 line 672
  273. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_723_i7 line 674
  274. def OAI.SnakyPrototype.Certificate21.checked_723_i7 line 678
  275. def OAI.SnakyPrototype.Certificate21.height_723_i6 line 686
  276. def OAI.SnakyPrototype.Certificate21.childrenH_723_i6 line 687
  277. theorem OAI.SnakyPrototype.Certificate21.height_exact_723_i6 line 688
  278. theorem OAI.SnakyPrototype.Certificate21.required_origin_723_i6 line 689
  279. theorem OAI.SnakyPrototype.Certificate21.required_exact_723_i6 line 691
  280. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_723_i6 line 695
  281. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_723_i6 line 697
  282. def OAI.SnakyPrototype.Certificate21.checked_723_i6 line 701
  283. def OAI.SnakyPrototype.Certificate21.height_723_i8 line 709
  284. def OAI.SnakyPrototype.Certificate21.childrenH_723_i8 line 710
  285. theorem OAI.SnakyPrototype.Certificate21.height_exact_723_i8 line 711
  286. theorem OAI.SnakyPrototype.Certificate21.required_origin_723_i8 line 712
  287. theorem OAI.SnakyPrototype.Certificate21.required_exact_723_i8 line 714
  288. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_723_i8 line 718
  289. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_723_i8 line 720
  290. def OAI.SnakyPrototype.Certificate21.checked_723_i8 line 724
  291. def OAI.SnakyPrototype.Certificate21.height_723_i2 line 732
  292. def OAI.SnakyPrototype.Certificate21.childrenH_723_i2 line 733
  293. theorem OAI.SnakyPrototype.Certificate21.height_exact_723_i2 line 734
  294. theorem OAI.SnakyPrototype.Certificate21.required_origin_723_i2 line 735
  295. theorem OAI.SnakyPrototype.Certificate21.required_exact_723_i2 line 737
  296. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_723_i2 line 741
  297. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_723_i2 line 743
  298. def OAI.SnakyPrototype.Certificate21.checked_723_i2 line 747
  299. def OAI.SnakyPrototype.Certificate21.height_723 line 755
  300. def OAI.SnakyPrototype.Certificate21.childrenH_723 line 756
  301. theorem OAI.SnakyPrototype.Certificate21.height_exact_723 line 757
  302. theorem OAI.SnakyPrototype.Certificate21.required_origin_723 line 758
  303. theorem OAI.SnakyPrototype.Certificate21.required_exact_723 line 760
  304. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_723 line 764
  305. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_723 line 766
  306. def OAI.SnakyPrototype.Certificate21.checked_723 line 770