OAI/GameTheory/SnakyTwentyOne/Cards/Height13Part01.lean

GitHub source file

324 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_462 line 38
  2. def OAI.SnakyPrototype.Certificate21.envelope_462 line 39
  3. def OAI.SnakyPrototype.Certificate21.childrenC_462 line 40
  4. def OAI.SnakyPrototype.Certificate21.childrenD_462 line 41
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_462 line 42
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_462 line 43
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_462 line 44
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_462 line 45
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_462 line 46
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_462 line 56
  11. def OAI.SnakyPrototype.Certificate21.required_490 line 61
  12. def OAI.SnakyPrototype.Certificate21.envelope_490 line 62
  13. def OAI.SnakyPrototype.Certificate21.childrenC_490 line 63
  14. def OAI.SnakyPrototype.Certificate21.childrenD_490 line 64
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_490 line 65
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_490 line 66
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_490 line 67
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_490 line 68
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_490 line 69
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_490 line 78
  21. def OAI.SnakyPrototype.Certificate21.required_538_i0 line 83
  22. def OAI.SnakyPrototype.Certificate21.envelope_538_i0 line 84
  23. def OAI.SnakyPrototype.Certificate21.childrenC_538_i0 line 85
  24. def OAI.SnakyPrototype.Certificate21.childrenD_538_i0 line 86
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_538_i0 line 87
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_538_i0 line 88
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_538_i0 line 89
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_538_i0 line 90
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_538_i0 line 91
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_538_i0 line 100
  31. def OAI.SnakyPrototype.Certificate21.required_538_i1 line 105
  32. def OAI.SnakyPrototype.Certificate21.envelope_538_i1 line 106
  33. def OAI.SnakyPrototype.Certificate21.childrenC_538_i1 line 107
  34. def OAI.SnakyPrototype.Certificate21.childrenD_538_i1 line 108
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_538_i1 line 109
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_538_i1 line 110
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_538_i1 line 111
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_538_i1 line 112
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_538_i1 line 113
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_538_i1 line 118
  41. def OAI.SnakyPrototype.Certificate21.required_538_i3 line 123
  42. def OAI.SnakyPrototype.Certificate21.envelope_538_i3 line 124
  43. def OAI.SnakyPrototype.Certificate21.childrenC_538_i3 line 125
  44. def OAI.SnakyPrototype.Certificate21.childrenD_538_i3 line 126
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_538_i3 line 127
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_538_i3 line 128
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_538_i3 line 129
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_538_i3 line 130
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_538_i3 line 131
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_538_i3 line 137
  51. def OAI.SnakyPrototype.Certificate21.required_538_i4 line 142
  52. def OAI.SnakyPrototype.Certificate21.envelope_538_i4 line 143
  53. def OAI.SnakyPrototype.Certificate21.childrenC_538_i4 line 144
  54. def OAI.SnakyPrototype.Certificate21.childrenD_538_i4 line 145
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_538_i4 line 146
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_538_i4 line 147
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_538_i4 line 148
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_538_i4 line 149
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_538_i4 line 150
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_538_i4 line 155
  61. def OAI.SnakyPrototype.Certificate21.required_538_i5 line 160
  62. def OAI.SnakyPrototype.Certificate21.envelope_538_i5 line 161
  63. def OAI.SnakyPrototype.Certificate21.childrenC_538_i5 line 162
  64. def OAI.SnakyPrototype.Certificate21.childrenD_538_i5 line 163
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_538_i5 line 164
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_538_i5 line 165
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_538_i5 line 166
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_538_i5 line 167
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_538_i5 line 168
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_538_i5 line 173
  71. def OAI.SnakyPrototype.Certificate21.required_538_i2 line 178
  72. def OAI.SnakyPrototype.Certificate21.envelope_538_i2 line 179
  73. def OAI.SnakyPrototype.Certificate21.childrenC_538_i2 line 180
  74. def OAI.SnakyPrototype.Certificate21.childrenD_538_i2 line 181
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_538_i2 line 182
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_538_i2 line 183
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_538_i2 line 184
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_538_i2 line 185
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_538_i2 line 186
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_538_i2 line 193
  81. def OAI.SnakyPrototype.Certificate21.required_538_i6 line 198
  82. def OAI.SnakyPrototype.Certificate21.envelope_538_i6 line 199
  83. def OAI.SnakyPrototype.Certificate21.childrenC_538_i6 line 200
  84. def OAI.SnakyPrototype.Certificate21.childrenD_538_i6 line 201
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_538_i6 line 202
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_538_i6 line 203
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_538_i6 line 204
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_538_i6 line 205
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_538_i6 line 206
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_538_i6 line 211
  91. def OAI.SnakyPrototype.Certificate21.required_538_i7 line 216
  92. def OAI.SnakyPrototype.Certificate21.envelope_538_i7 line 217
  93. def OAI.SnakyPrototype.Certificate21.childrenC_538_i7 line 218
  94. def OAI.SnakyPrototype.Certificate21.childrenD_538_i7 line 219
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_538_i7 line 220
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_538_i7 line 221
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_538_i7 line 222
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_538_i7 line 223
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_538_i7 line 224
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_538_i7 line 234
  101. def OAI.SnakyPrototype.Certificate21.required_538_i8 line 239
  102. def OAI.SnakyPrototype.Certificate21.envelope_538_i8 line 240
  103. def OAI.SnakyPrototype.Certificate21.childrenC_538_i8 line 241
  104. def OAI.SnakyPrototype.Certificate21.childrenD_538_i8 line 242
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_538_i8 line 243
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_538_i8 line 244
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_538_i8 line 245
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_538_i8 line 246
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_538_i8 line 247
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_538_i8 line 252
  111. def OAI.SnakyPrototype.Certificate21.required_538_i9 line 257
  112. def OAI.SnakyPrototype.Certificate21.envelope_538_i9 line 258
  113. def OAI.SnakyPrototype.Certificate21.childrenC_538_i9 line 259
  114. def OAI.SnakyPrototype.Certificate21.childrenD_538_i9 line 260
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_538_i9 line 261
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_538_i9 line 262
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_538_i9 line 263
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_538_i9 line 264
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_538_i9 line 265
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_538_i9 line 270
  121. def OAI.SnakyPrototype.Certificate21.required_538 line 275
  122. def OAI.SnakyPrototype.Certificate21.envelope_538 line 276
  123. def OAI.SnakyPrototype.Certificate21.childrenC_538 line 277
  124. def OAI.SnakyPrototype.Certificate21.childrenD_538 line 278
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_538 line 279
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_538 line 280
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_538 line 281
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_538 line 282
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_538 line 283
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_538 line 296
  131. def OAI.SnakyPrototype.Certificate21.required_552_i1 line 301
  132. def OAI.SnakyPrototype.Certificate21.envelope_552_i1 line 302
  133. def OAI.SnakyPrototype.Certificate21.childrenC_552_i1 line 303
  134. def OAI.SnakyPrototype.Certificate21.childrenD_552_i1 line 304
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_552_i1 line 305
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_552_i1 line 306
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_552_i1 line 307
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_552_i1 line 308
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_552_i1 line 309
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_552_i1 line 314
  141. def OAI.SnakyPrototype.Certificate21.required_552_i0 line 319
  142. def OAI.SnakyPrototype.Certificate21.envelope_552_i0 line 320
  143. def OAI.SnakyPrototype.Certificate21.childrenC_552_i0 line 321
  144. def OAI.SnakyPrototype.Certificate21.childrenD_552_i0 line 322
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_552_i0 line 323
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_552_i0 line 324
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_552_i0 line 325
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_552_i0 line 326
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_552_i0 line 327
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_552_i0 line 335
  151. def OAI.SnakyPrototype.Certificate21.required_552 line 340
  152. def OAI.SnakyPrototype.Certificate21.envelope_552 line 341
  153. def OAI.SnakyPrototype.Certificate21.childrenC_552 line 342
  154. def OAI.SnakyPrototype.Certificate21.childrenD_552 line 343
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_552 line 344
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_552 line 345
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_552 line 346
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_552 line 347
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_552 line 348
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_552 line 357
  161. def OAI.SnakyPrototype.Certificate21.required_555_i0 line 362
  162. def OAI.SnakyPrototype.Certificate21.envelope_555_i0 line 363
  163. def OAI.SnakyPrototype.Certificate21.childrenC_555_i0 line 364
  164. def OAI.SnakyPrototype.Certificate21.childrenD_555_i0 line 365
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_555_i0 line 366
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_555_i0 line 367
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_555_i0 line 368
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_555_i0 line 369
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_555_i0 line 370
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_555_i0 line 376
  171. def OAI.SnakyPrototype.Certificate21.required_555 line 381
  172. def OAI.SnakyPrototype.Certificate21.envelope_555 line 382
  173. def OAI.SnakyPrototype.Certificate21.childrenC_555 line 383
  174. def OAI.SnakyPrototype.Certificate21.childrenD_555 line 384
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_555 line 385
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_555 line 386
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_555 line 387
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_555 line 388
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_555 line 389
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_555 line 399
  181. def OAI.SnakyPrototype.Certificate21.height_462 line 404
  182. def OAI.SnakyPrototype.Certificate21.childrenH_462 line 405
  183. theorem OAI.SnakyPrototype.Certificate21.height_exact_462 line 406
  184. theorem OAI.SnakyPrototype.Certificate21.required_origin_462 line 407
  185. theorem OAI.SnakyPrototype.Certificate21.required_exact_462 line 409
  186. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_462 line 413
  187. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_462 line 415
  188. def OAI.SnakyPrototype.Certificate21.checked_462 line 419
  189. def OAI.SnakyPrototype.Certificate21.height_490 line 427
  190. def OAI.SnakyPrototype.Certificate21.childrenH_490 line 428
  191. theorem OAI.SnakyPrototype.Certificate21.height_exact_490 line 429
  192. theorem OAI.SnakyPrototype.Certificate21.required_origin_490 line 430
  193. theorem OAI.SnakyPrototype.Certificate21.required_exact_490 line 432
  194. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_490 line 436
  195. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_490 line 438
  196. def OAI.SnakyPrototype.Certificate21.checked_490 line 442
  197. def OAI.SnakyPrototype.Certificate21.height_538_i0 line 450
  198. def OAI.SnakyPrototype.Certificate21.childrenH_538_i0 line 451
  199. theorem OAI.SnakyPrototype.Certificate21.height_exact_538_i0 line 452
  200. theorem OAI.SnakyPrototype.Certificate21.required_origin_538_i0 line 453
  201. theorem OAI.SnakyPrototype.Certificate21.required_exact_538_i0 line 455
  202. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_538_i0 line 459
  203. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_538_i0 line 461
  204. def OAI.SnakyPrototype.Certificate21.checked_538_i0 line 465
  205. def OAI.SnakyPrototype.Certificate21.height_538_i1 line 473
  206. def OAI.SnakyPrototype.Certificate21.childrenH_538_i1 line 474
  207. theorem OAI.SnakyPrototype.Certificate21.height_exact_538_i1 line 475
  208. theorem OAI.SnakyPrototype.Certificate21.required_origin_538_i1 line 476
  209. theorem OAI.SnakyPrototype.Certificate21.required_exact_538_i1 line 478
  210. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_538_i1 line 482
  211. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_538_i1 line 484
  212. def OAI.SnakyPrototype.Certificate21.checked_538_i1 line 488
  213. def OAI.SnakyPrototype.Certificate21.height_538_i3 line 496
  214. def OAI.SnakyPrototype.Certificate21.childrenH_538_i3 line 497
  215. theorem OAI.SnakyPrototype.Certificate21.height_exact_538_i3 line 498
  216. theorem OAI.SnakyPrototype.Certificate21.required_origin_538_i3 line 499
  217. theorem OAI.SnakyPrototype.Certificate21.required_exact_538_i3 line 501
  218. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_538_i3 line 505
  219. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_538_i3 line 507
  220. def OAI.SnakyPrototype.Certificate21.checked_538_i3 line 511
  221. def OAI.SnakyPrototype.Certificate21.height_538_i4 line 519
  222. def OAI.SnakyPrototype.Certificate21.childrenH_538_i4 line 520
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_538_i4 line 521
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_538_i4 line 522
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_538_i4 line 524
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_538_i4 line 528
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_538_i4 line 530
  228. def OAI.SnakyPrototype.Certificate21.checked_538_i4 line 534
  229. def OAI.SnakyPrototype.Certificate21.height_538_i5 line 542
  230. def OAI.SnakyPrototype.Certificate21.childrenH_538_i5 line 543
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_538_i5 line 544
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_538_i5 line 545
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_538_i5 line 547
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_538_i5 line 551
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_538_i5 line 553
  236. def OAI.SnakyPrototype.Certificate21.checked_538_i5 line 557
  237. def OAI.SnakyPrototype.Certificate21.height_538_i2 line 565
  238. def OAI.SnakyPrototype.Certificate21.childrenH_538_i2 line 566
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_538_i2 line 567
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_538_i2 line 568
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_538_i2 line 570
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_538_i2 line 574
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_538_i2 line 576
  244. def OAI.SnakyPrototype.Certificate21.checked_538_i2 line 580
  245. def OAI.SnakyPrototype.Certificate21.height_538_i6 line 588
  246. def OAI.SnakyPrototype.Certificate21.childrenH_538_i6 line 589
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_538_i6 line 590
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_538_i6 line 591
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_538_i6 line 593
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_538_i6 line 597
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_538_i6 line 599
  252. def OAI.SnakyPrototype.Certificate21.checked_538_i6 line 603
  253. def OAI.SnakyPrototype.Certificate21.height_538_i7 line 611
  254. def OAI.SnakyPrototype.Certificate21.childrenH_538_i7 line 612
  255. theorem OAI.SnakyPrototype.Certificate21.height_exact_538_i7 line 613
  256. theorem OAI.SnakyPrototype.Certificate21.required_origin_538_i7 line 614
  257. theorem OAI.SnakyPrototype.Certificate21.required_exact_538_i7 line 616
  258. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_538_i7 line 620
  259. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_538_i7 line 622
  260. def OAI.SnakyPrototype.Certificate21.checked_538_i7 line 626
  261. def OAI.SnakyPrototype.Certificate21.height_538_i8 line 634
  262. def OAI.SnakyPrototype.Certificate21.childrenH_538_i8 line 635
  263. theorem OAI.SnakyPrototype.Certificate21.height_exact_538_i8 line 636
  264. theorem OAI.SnakyPrototype.Certificate21.required_origin_538_i8 line 637
  265. theorem OAI.SnakyPrototype.Certificate21.required_exact_538_i8 line 639
  266. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_538_i8 line 643
  267. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_538_i8 line 645
  268. def OAI.SnakyPrototype.Certificate21.checked_538_i8 line 649
  269. def OAI.SnakyPrototype.Certificate21.height_538_i9 line 657
  270. def OAI.SnakyPrototype.Certificate21.childrenH_538_i9 line 658
  271. theorem OAI.SnakyPrototype.Certificate21.height_exact_538_i9 line 659
  272. theorem OAI.SnakyPrototype.Certificate21.required_origin_538_i9 line 660
  273. theorem OAI.SnakyPrototype.Certificate21.required_exact_538_i9 line 662
  274. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_538_i9 line 666
  275. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_538_i9 line 668
  276. def OAI.SnakyPrototype.Certificate21.checked_538_i9 line 672
  277. def OAI.SnakyPrototype.Certificate21.height_538 line 680
  278. def OAI.SnakyPrototype.Certificate21.childrenH_538 line 681
  279. theorem OAI.SnakyPrototype.Certificate21.height_exact_538 line 682
  280. theorem OAI.SnakyPrototype.Certificate21.required_origin_538 line 683
  281. theorem OAI.SnakyPrototype.Certificate21.required_exact_538 line 685
  282. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_538 line 689
  283. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_538 line 691
  284. def OAI.SnakyPrototype.Certificate21.checked_538 line 695
  285. def OAI.SnakyPrototype.Certificate21.height_552_i1 line 703
  286. def OAI.SnakyPrototype.Certificate21.childrenH_552_i1 line 704
  287. theorem OAI.SnakyPrototype.Certificate21.height_exact_552_i1 line 705
  288. theorem OAI.SnakyPrototype.Certificate21.required_origin_552_i1 line 706
  289. theorem OAI.SnakyPrototype.Certificate21.required_exact_552_i1 line 708
  290. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_552_i1 line 712
  291. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_552_i1 line 714
  292. def OAI.SnakyPrototype.Certificate21.checked_552_i1 line 718
  293. def OAI.SnakyPrototype.Certificate21.height_552_i0 line 726
  294. def OAI.SnakyPrototype.Certificate21.childrenH_552_i0 line 727
  295. theorem OAI.SnakyPrototype.Certificate21.height_exact_552_i0 line 728
  296. theorem OAI.SnakyPrototype.Certificate21.required_origin_552_i0 line 729
  297. theorem OAI.SnakyPrototype.Certificate21.required_exact_552_i0 line 731
  298. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_552_i0 line 735
  299. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_552_i0 line 737
  300. def OAI.SnakyPrototype.Certificate21.checked_552_i0 line 741
  301. def OAI.SnakyPrototype.Certificate21.height_552 line 749
  302. def OAI.SnakyPrototype.Certificate21.childrenH_552 line 750
  303. theorem OAI.SnakyPrototype.Certificate21.height_exact_552 line 751
  304. theorem OAI.SnakyPrototype.Certificate21.required_origin_552 line 752
  305. theorem OAI.SnakyPrototype.Certificate21.required_exact_552 line 754
  306. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_552 line 758
  307. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_552 line 760
  308. def OAI.SnakyPrototype.Certificate21.checked_552 line 764
  309. def OAI.SnakyPrototype.Certificate21.height_555_i0 line 772
  310. def OAI.SnakyPrototype.Certificate21.childrenH_555_i0 line 773
  311. theorem OAI.SnakyPrototype.Certificate21.height_exact_555_i0 line 774
  312. theorem OAI.SnakyPrototype.Certificate21.required_origin_555_i0 line 775
  313. theorem OAI.SnakyPrototype.Certificate21.required_exact_555_i0 line 777
  314. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_555_i0 line 781
  315. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_555_i0 line 783
  316. def OAI.SnakyPrototype.Certificate21.checked_555_i0 line 787
  317. def OAI.SnakyPrototype.Certificate21.height_555 line 795
  318. def OAI.SnakyPrototype.Certificate21.childrenH_555 line 796
  319. theorem OAI.SnakyPrototype.Certificate21.height_exact_555 line 797
  320. theorem OAI.SnakyPrototype.Certificate21.required_origin_555 line 798
  321. theorem OAI.SnakyPrototype.Certificate21.required_exact_555 line 800
  322. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_555 line 804
  323. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_555 line 806
  324. def OAI.SnakyPrototype.Certificate21.checked_555 line 810