OAI/GameTheory/SnakyTwentyOne/Cards/Height15Part03.lean

GitHub source file

378 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_698 line 44
  2. def OAI.SnakyPrototype.Certificate21.envelope_698 line 45
  3. def OAI.SnakyPrototype.Certificate21.childrenC_698 line 46
  4. def OAI.SnakyPrototype.Certificate21.childrenD_698 line 47
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_698 line 48
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_698 line 49
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_698 line 50
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_698 line 51
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_698 line 52
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_698 line 63
  11. def OAI.SnakyPrototype.Certificate21.required_699_i3 line 68
  12. def OAI.SnakyPrototype.Certificate21.envelope_699_i3 line 69
  13. def OAI.SnakyPrototype.Certificate21.childrenC_699_i3 line 70
  14. def OAI.SnakyPrototype.Certificate21.childrenD_699_i3 line 71
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_699_i3 line 72
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_699_i3 line 73
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_699_i3 line 74
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_699_i3 line 75
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_699_i3 line 76
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_699_i3 line 81
  21. def OAI.SnakyPrototype.Certificate21.required_699_i2 line 86
  22. def OAI.SnakyPrototype.Certificate21.envelope_699_i2 line 87
  23. def OAI.SnakyPrototype.Certificate21.childrenC_699_i2 line 88
  24. def OAI.SnakyPrototype.Certificate21.childrenD_699_i2 line 89
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_699_i2 line 90
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_699_i2 line 91
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_699_i2 line 92
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_699_i2 line 93
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_699_i2 line 94
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_699_i2 line 100
  31. def OAI.SnakyPrototype.Certificate21.required_699_i1 line 105
  32. def OAI.SnakyPrototype.Certificate21.envelope_699_i1 line 106
  33. def OAI.SnakyPrototype.Certificate21.childrenC_699_i1 line 107
  34. def OAI.SnakyPrototype.Certificate21.childrenD_699_i1 line 108
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_699_i1 line 109
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_699_i1 line 110
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_699_i1 line 111
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_699_i1 line 112
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_699_i1 line 113
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_699_i1 line 119
  41. def OAI.SnakyPrototype.Certificate21.required_699_i0 line 124
  42. def OAI.SnakyPrototype.Certificate21.envelope_699_i0 line 125
  43. def OAI.SnakyPrototype.Certificate21.childrenC_699_i0 line 126
  44. def OAI.SnakyPrototype.Certificate21.childrenD_699_i0 line 127
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_699_i0 line 128
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_699_i0 line 129
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_699_i0 line 130
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_699_i0 line 131
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_699_i0 line 132
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_699_i0 line 139
  51. def OAI.SnakyPrototype.Certificate21.required_699_i6 line 144
  52. def OAI.SnakyPrototype.Certificate21.envelope_699_i6 line 145
  53. def OAI.SnakyPrototype.Certificate21.childrenC_699_i6 line 146
  54. def OAI.SnakyPrototype.Certificate21.childrenD_699_i6 line 147
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_699_i6 line 148
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_699_i6 line 149
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_699_i6 line 150
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_699_i6 line 151
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_699_i6 line 152
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_699_i6 line 157
  61. def OAI.SnakyPrototype.Certificate21.required_699_i5 line 162
  62. def OAI.SnakyPrototype.Certificate21.envelope_699_i5 line 163
  63. def OAI.SnakyPrototype.Certificate21.childrenC_699_i5 line 164
  64. def OAI.SnakyPrototype.Certificate21.childrenD_699_i5 line 165
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_699_i5 line 166
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_699_i5 line 167
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_699_i5 line 168
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_699_i5 line 169
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_699_i5 line 170
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_699_i5 line 177
  71. def OAI.SnakyPrototype.Certificate21.required_699_i4 line 182
  72. def OAI.SnakyPrototype.Certificate21.envelope_699_i4 line 183
  73. def OAI.SnakyPrototype.Certificate21.childrenC_699_i4 line 184
  74. def OAI.SnakyPrototype.Certificate21.childrenD_699_i4 line 185
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_699_i4 line 186
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_699_i4 line 187
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_699_i4 line 188
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_699_i4 line 189
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_699_i4 line 190
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_699_i4 line 198
  81. def OAI.SnakyPrototype.Certificate21.required_699 line 203
  82. def OAI.SnakyPrototype.Certificate21.envelope_699 line 204
  83. def OAI.SnakyPrototype.Certificate21.childrenC_699 line 205
  84. def OAI.SnakyPrototype.Certificate21.childrenD_699 line 206
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_699 line 207
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_699 line 208
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_699 line 209
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_699 line 210
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_699 line 211
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_699 line 219
  91. def OAI.SnakyPrototype.Certificate21.required_712_i1 line 224
  92. def OAI.SnakyPrototype.Certificate21.envelope_712_i1 line 225
  93. def OAI.SnakyPrototype.Certificate21.childrenC_712_i1 line 226
  94. def OAI.SnakyPrototype.Certificate21.childrenD_712_i1 line 227
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_712_i1 line 228
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_712_i1 line 229
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_712_i1 line 230
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_712_i1 line 231
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_712_i1 line 232
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_712_i1 line 238
  101. def OAI.SnakyPrototype.Certificate21.required_712_i0 line 243
  102. def OAI.SnakyPrototype.Certificate21.envelope_712_i0 line 244
  103. def OAI.SnakyPrototype.Certificate21.childrenC_712_i0 line 245
  104. def OAI.SnakyPrototype.Certificate21.childrenD_712_i0 line 246
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_712_i0 line 247
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_712_i0 line 248
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_712_i0 line 249
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_712_i0 line 250
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_712_i0 line 251
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_712_i0 line 260
  111. def OAI.SnakyPrototype.Certificate21.required_712 line 265
  112. def OAI.SnakyPrototype.Certificate21.envelope_712 line 266
  113. def OAI.SnakyPrototype.Certificate21.childrenC_712 line 267
  114. def OAI.SnakyPrototype.Certificate21.childrenD_712 line 268
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_712 line 269
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_712 line 270
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_712 line 271
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_712 line 272
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_712 line 273
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_712 line 289
  121. def OAI.SnakyPrototype.Certificate21.required_713 line 294
  122. def OAI.SnakyPrototype.Certificate21.envelope_713 line 295
  123. def OAI.SnakyPrototype.Certificate21.childrenC_713 line 296
  124. def OAI.SnakyPrototype.Certificate21.childrenD_713 line 297
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_713 line 298
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_713 line 299
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_713 line 300
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_713 line 301
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_713 line 302
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_713 line 316
  131. def OAI.SnakyPrototype.Certificate21.required_718_i0 line 321
  132. def OAI.SnakyPrototype.Certificate21.envelope_718_i0 line 322
  133. def OAI.SnakyPrototype.Certificate21.childrenC_718_i0 line 323
  134. def OAI.SnakyPrototype.Certificate21.childrenD_718_i0 line 324
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_718_i0 line 325
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_718_i0 line 326
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_718_i0 line 327
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_718_i0 line 328
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_718_i0 line 329
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_718_i0 line 336
  141. def OAI.SnakyPrototype.Certificate21.required_718_i1 line 341
  142. def OAI.SnakyPrototype.Certificate21.envelope_718_i1 line 342
  143. def OAI.SnakyPrototype.Certificate21.childrenC_718_i1 line 343
  144. def OAI.SnakyPrototype.Certificate21.childrenD_718_i1 line 344
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_718_i1 line 345
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_718_i1 line 346
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_718_i1 line 347
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_718_i1 line 348
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_718_i1 line 349
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_718_i1 line 357
  151. def OAI.SnakyPrototype.Certificate21.required_718_i3 line 362
  152. def OAI.SnakyPrototype.Certificate21.envelope_718_i3 line 363
  153. def OAI.SnakyPrototype.Certificate21.childrenC_718_i3 line 364
  154. def OAI.SnakyPrototype.Certificate21.childrenD_718_i3 line 365
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_718_i3 line 366
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_718_i3 line 367
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_718_i3 line 368
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_718_i3 line 369
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_718_i3 line 370
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_718_i3 line 377
  161. def OAI.SnakyPrototype.Certificate21.required_718_i5 line 382
  162. def OAI.SnakyPrototype.Certificate21.envelope_718_i5 line 383
  163. def OAI.SnakyPrototype.Certificate21.childrenC_718_i5 line 384
  164. def OAI.SnakyPrototype.Certificate21.childrenD_718_i5 line 385
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_718_i5 line 386
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_718_i5 line 387
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_718_i5 line 388
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_718_i5 line 389
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_718_i5 line 390
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_718_i5 line 395
  171. def OAI.SnakyPrototype.Certificate21.required_718_i4 line 400
  172. def OAI.SnakyPrototype.Certificate21.envelope_718_i4 line 401
  173. def OAI.SnakyPrototype.Certificate21.childrenC_718_i4 line 402
  174. def OAI.SnakyPrototype.Certificate21.childrenD_718_i4 line 403
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_718_i4 line 404
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_718_i4 line 405
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_718_i4 line 406
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_718_i4 line 407
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_718_i4 line 408
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_718_i4 line 416
  181. def OAI.SnakyPrototype.Certificate21.required_718_i6 line 421
  182. def OAI.SnakyPrototype.Certificate21.envelope_718_i6 line 422
  183. def OAI.SnakyPrototype.Certificate21.childrenC_718_i6 line 423
  184. def OAI.SnakyPrototype.Certificate21.childrenD_718_i6 line 424
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_718_i6 line 425
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_718_i6 line 426
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_718_i6 line 427
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_718_i6 line 428
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_718_i6 line 429
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_718_i6 line 435
  191. def OAI.SnakyPrototype.Certificate21.required_718_i2 line 440
  192. def OAI.SnakyPrototype.Certificate21.envelope_718_i2 line 441
  193. def OAI.SnakyPrototype.Certificate21.childrenC_718_i2 line 442
  194. def OAI.SnakyPrototype.Certificate21.childrenD_718_i2 line 443
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_718_i2 line 444
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_718_i2 line 445
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_718_i2 line 446
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_718_i2 line 447
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_718_i2 line 448
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_718_i2 line 457
  201. def OAI.SnakyPrototype.Certificate21.required_718 line 462
  202. def OAI.SnakyPrototype.Certificate21.envelope_718 line 463
  203. def OAI.SnakyPrototype.Certificate21.childrenC_718 line 464
  204. def OAI.SnakyPrototype.Certificate21.childrenD_718 line 465
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_718 line 466
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_718 line 467
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_718 line 468
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_718 line 469
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_718 line 470
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_718 line 483
  211. def OAI.SnakyPrototype.Certificate21.height_698 line 488
  212. def OAI.SnakyPrototype.Certificate21.childrenH_698 line 489
  213. theorem OAI.SnakyPrototype.Certificate21.height_exact_698 line 490
  214. theorem OAI.SnakyPrototype.Certificate21.required_origin_698 line 491
  215. theorem OAI.SnakyPrototype.Certificate21.required_exact_698 line 493
  216. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_698 line 497
  217. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_698 line 499
  218. def OAI.SnakyPrototype.Certificate21.checked_698 line 503
  219. def OAI.SnakyPrototype.Certificate21.height_699_i3 line 511
  220. def OAI.SnakyPrototype.Certificate21.childrenH_699_i3 line 512
  221. theorem OAI.SnakyPrototype.Certificate21.height_exact_699_i3 line 513
  222. theorem OAI.SnakyPrototype.Certificate21.required_origin_699_i3 line 514
  223. theorem OAI.SnakyPrototype.Certificate21.required_exact_699_i3 line 516
  224. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_699_i3 line 520
  225. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_699_i3 line 522
  226. def OAI.SnakyPrototype.Certificate21.checked_699_i3 line 526
  227. def OAI.SnakyPrototype.Certificate21.height_699_i2 line 534
  228. def OAI.SnakyPrototype.Certificate21.childrenH_699_i2 line 535
  229. theorem OAI.SnakyPrototype.Certificate21.height_exact_699_i2 line 536
  230. theorem OAI.SnakyPrototype.Certificate21.required_origin_699_i2 line 537
  231. theorem OAI.SnakyPrototype.Certificate21.required_exact_699_i2 line 539
  232. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_699_i2 line 543
  233. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_699_i2 line 545
  234. def OAI.SnakyPrototype.Certificate21.checked_699_i2 line 549
  235. def OAI.SnakyPrototype.Certificate21.height_699_i1 line 557
  236. def OAI.SnakyPrototype.Certificate21.childrenH_699_i1 line 558
  237. theorem OAI.SnakyPrototype.Certificate21.height_exact_699_i1 line 559
  238. theorem OAI.SnakyPrototype.Certificate21.required_origin_699_i1 line 560
  239. theorem OAI.SnakyPrototype.Certificate21.required_exact_699_i1 line 562
  240. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_699_i1 line 566
  241. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_699_i1 line 568
  242. def OAI.SnakyPrototype.Certificate21.checked_699_i1 line 572
  243. def OAI.SnakyPrototype.Certificate21.height_699_i0 line 580
  244. def OAI.SnakyPrototype.Certificate21.childrenH_699_i0 line 581
  245. theorem OAI.SnakyPrototype.Certificate21.height_exact_699_i0 line 582
  246. theorem OAI.SnakyPrototype.Certificate21.required_origin_699_i0 line 583
  247. theorem OAI.SnakyPrototype.Certificate21.required_exact_699_i0 line 585
  248. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_699_i0 line 589
  249. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_699_i0 line 591
  250. def OAI.SnakyPrototype.Certificate21.checked_699_i0 line 595
  251. def OAI.SnakyPrototype.Certificate21.height_699_i6 line 603
  252. def OAI.SnakyPrototype.Certificate21.childrenH_699_i6 line 604
  253. theorem OAI.SnakyPrototype.Certificate21.height_exact_699_i6 line 605
  254. theorem OAI.SnakyPrototype.Certificate21.required_origin_699_i6 line 606
  255. theorem OAI.SnakyPrototype.Certificate21.required_exact_699_i6 line 608
  256. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_699_i6 line 612
  257. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_699_i6 line 614
  258. def OAI.SnakyPrototype.Certificate21.checked_699_i6 line 618
  259. def OAI.SnakyPrototype.Certificate21.height_699_i5 line 626
  260. def OAI.SnakyPrototype.Certificate21.childrenH_699_i5 line 627
  261. theorem OAI.SnakyPrototype.Certificate21.height_exact_699_i5 line 628
  262. theorem OAI.SnakyPrototype.Certificate21.required_origin_699_i5 line 629
  263. theorem OAI.SnakyPrototype.Certificate21.required_exact_699_i5 line 631
  264. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_699_i5 line 635
  265. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_699_i5 line 637
  266. def OAI.SnakyPrototype.Certificate21.checked_699_i5 line 641
  267. def OAI.SnakyPrototype.Certificate21.height_699_i4 line 649
  268. def OAI.SnakyPrototype.Certificate21.childrenH_699_i4 line 650
  269. theorem OAI.SnakyPrototype.Certificate21.height_exact_699_i4 line 651
  270. theorem OAI.SnakyPrototype.Certificate21.required_origin_699_i4 line 652
  271. theorem OAI.SnakyPrototype.Certificate21.required_exact_699_i4 line 654
  272. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_699_i4 line 658
  273. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_699_i4 line 660
  274. def OAI.SnakyPrototype.Certificate21.checked_699_i4 line 664
  275. def OAI.SnakyPrototype.Certificate21.height_699 line 672
  276. def OAI.SnakyPrototype.Certificate21.childrenH_699 line 673
  277. theorem OAI.SnakyPrototype.Certificate21.height_exact_699 line 674
  278. theorem OAI.SnakyPrototype.Certificate21.required_origin_699 line 675
  279. theorem OAI.SnakyPrototype.Certificate21.required_exact_699 line 677
  280. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_699 line 681
  281. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_699 line 683
  282. def OAI.SnakyPrototype.Certificate21.checked_699 line 687
  283. def OAI.SnakyPrototype.Certificate21.height_712_i1 line 695
  284. def OAI.SnakyPrototype.Certificate21.childrenH_712_i1 line 696
  285. theorem OAI.SnakyPrototype.Certificate21.height_exact_712_i1 line 697
  286. theorem OAI.SnakyPrototype.Certificate21.required_origin_712_i1 line 698
  287. theorem OAI.SnakyPrototype.Certificate21.required_exact_712_i1 line 700
  288. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_712_i1 line 704
  289. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_712_i1 line 706
  290. def OAI.SnakyPrototype.Certificate21.checked_712_i1 line 710
  291. def OAI.SnakyPrototype.Certificate21.height_712_i0 line 718
  292. def OAI.SnakyPrototype.Certificate21.childrenH_712_i0 line 719
  293. theorem OAI.SnakyPrototype.Certificate21.height_exact_712_i0 line 720
  294. theorem OAI.SnakyPrototype.Certificate21.required_origin_712_i0 line 721
  295. theorem OAI.SnakyPrototype.Certificate21.required_exact_712_i0 line 723
  296. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_712_i0 line 727
  297. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_712_i0 line 729
  298. def OAI.SnakyPrototype.Certificate21.checked_712_i0 line 733
  299. def OAI.SnakyPrototype.Certificate21.height_712 line 741
  300. def OAI.SnakyPrototype.Certificate21.childrenH_712 line 742
  301. theorem OAI.SnakyPrototype.Certificate21.height_exact_712 line 743
  302. theorem OAI.SnakyPrototype.Certificate21.required_origin_712 line 744
  303. theorem OAI.SnakyPrototype.Certificate21.required_exact_712 line 746
  304. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_712 line 750
  305. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_712 line 752
  306. def OAI.SnakyPrototype.Certificate21.checked_712 line 756
  307. def OAI.SnakyPrototype.Certificate21.height_713 line 764
  308. def OAI.SnakyPrototype.Certificate21.childrenH_713 line 765
  309. theorem OAI.SnakyPrototype.Certificate21.height_exact_713 line 766
  310. theorem OAI.SnakyPrototype.Certificate21.required_origin_713 line 767
  311. theorem OAI.SnakyPrototype.Certificate21.required_exact_713 line 769
  312. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_713 line 773
  313. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_713 line 775
  314. def OAI.SnakyPrototype.Certificate21.checked_713 line 779
  315. def OAI.SnakyPrototype.Certificate21.height_718_i0 line 787
  316. def OAI.SnakyPrototype.Certificate21.childrenH_718_i0 line 788
  317. theorem OAI.SnakyPrototype.Certificate21.height_exact_718_i0 line 789
  318. theorem OAI.SnakyPrototype.Certificate21.required_origin_718_i0 line 790
  319. theorem OAI.SnakyPrototype.Certificate21.required_exact_718_i0 line 792
  320. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_718_i0 line 796
  321. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_718_i0 line 798
  322. def OAI.SnakyPrototype.Certificate21.checked_718_i0 line 802
  323. def OAI.SnakyPrototype.Certificate21.height_718_i1 line 810
  324. def OAI.SnakyPrototype.Certificate21.childrenH_718_i1 line 811
  325. theorem OAI.SnakyPrototype.Certificate21.height_exact_718_i1 line 812
  326. theorem OAI.SnakyPrototype.Certificate21.required_origin_718_i1 line 813
  327. theorem OAI.SnakyPrototype.Certificate21.required_exact_718_i1 line 815
  328. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_718_i1 line 819
  329. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_718_i1 line 821
  330. def OAI.SnakyPrototype.Certificate21.checked_718_i1 line 825
  331. def OAI.SnakyPrototype.Certificate21.height_718_i3 line 833
  332. def OAI.SnakyPrototype.Certificate21.childrenH_718_i3 line 834
  333. theorem OAI.SnakyPrototype.Certificate21.height_exact_718_i3 line 835
  334. theorem OAI.SnakyPrototype.Certificate21.required_origin_718_i3 line 836
  335. theorem OAI.SnakyPrototype.Certificate21.required_exact_718_i3 line 838
  336. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_718_i3 line 842
  337. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_718_i3 line 844
  338. def OAI.SnakyPrototype.Certificate21.checked_718_i3 line 848
  339. def OAI.SnakyPrototype.Certificate21.height_718_i5 line 856
  340. def OAI.SnakyPrototype.Certificate21.childrenH_718_i5 line 857
  341. theorem OAI.SnakyPrototype.Certificate21.height_exact_718_i5 line 858
  342. theorem OAI.SnakyPrototype.Certificate21.required_origin_718_i5 line 859
  343. theorem OAI.SnakyPrototype.Certificate21.required_exact_718_i5 line 861
  344. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_718_i5 line 865
  345. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_718_i5 line 867
  346. def OAI.SnakyPrototype.Certificate21.checked_718_i5 line 871
  347. def OAI.SnakyPrototype.Certificate21.height_718_i4 line 879
  348. def OAI.SnakyPrototype.Certificate21.childrenH_718_i4 line 880
  349. theorem OAI.SnakyPrototype.Certificate21.height_exact_718_i4 line 881
  350. theorem OAI.SnakyPrototype.Certificate21.required_origin_718_i4 line 882
  351. theorem OAI.SnakyPrototype.Certificate21.required_exact_718_i4 line 884
  352. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_718_i4 line 888
  353. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_718_i4 line 890
  354. def OAI.SnakyPrototype.Certificate21.checked_718_i4 line 894
  355. def OAI.SnakyPrototype.Certificate21.height_718_i6 line 902
  356. def OAI.SnakyPrototype.Certificate21.childrenH_718_i6 line 903
  357. theorem OAI.SnakyPrototype.Certificate21.height_exact_718_i6 line 904
  358. theorem OAI.SnakyPrototype.Certificate21.required_origin_718_i6 line 905
  359. theorem OAI.SnakyPrototype.Certificate21.required_exact_718_i6 line 907
  360. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_718_i6 line 911
  361. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_718_i6 line 913
  362. def OAI.SnakyPrototype.Certificate21.checked_718_i6 line 917
  363. def OAI.SnakyPrototype.Certificate21.height_718_i2 line 925
  364. def OAI.SnakyPrototype.Certificate21.childrenH_718_i2 line 926
  365. theorem OAI.SnakyPrototype.Certificate21.height_exact_718_i2 line 927
  366. theorem OAI.SnakyPrototype.Certificate21.required_origin_718_i2 line 928
  367. theorem OAI.SnakyPrototype.Certificate21.required_exact_718_i2 line 930
  368. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_718_i2 line 934
  369. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_718_i2 line 936
  370. def OAI.SnakyPrototype.Certificate21.checked_718_i2 line 940
  371. def OAI.SnakyPrototype.Certificate21.height_718 line 948
  372. def OAI.SnakyPrototype.Certificate21.childrenH_718 line 949
  373. theorem OAI.SnakyPrototype.Certificate21.height_exact_718 line 950
  374. theorem OAI.SnakyPrototype.Certificate21.required_origin_718 line 951
  375. theorem OAI.SnakyPrototype.Certificate21.required_exact_718 line 953
  376. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_718 line 957
  377. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_718 line 959
  378. def OAI.SnakyPrototype.Certificate21.checked_718 line 963