OAI/GameTheory/SnakyTwentyOne/Cards/Height18Part01.lean

GitHub source file

342 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_684_i1 line 43
  2. def OAI.SnakyPrototype.Certificate21.envelope_684_i1 line 44
  3. def OAI.SnakyPrototype.Certificate21.childrenC_684_i1 line 45
  4. def OAI.SnakyPrototype.Certificate21.childrenD_684_i1 line 46
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_684_i1 line 47
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_684_i1 line 48
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_684_i1 line 49
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_684_i1 line 50
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_684_i1 line 51
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_684_i1 line 60
  11. def OAI.SnakyPrototype.Certificate21.required_684_i0 line 65
  12. def OAI.SnakyPrototype.Certificate21.envelope_684_i0 line 66
  13. def OAI.SnakyPrototype.Certificate21.childrenC_684_i0 line 67
  14. def OAI.SnakyPrototype.Certificate21.childrenD_684_i0 line 68
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_684_i0 line 69
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_684_i0 line 70
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_684_i0 line 71
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_684_i0 line 72
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_684_i0 line 73
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_684_i0 line 82
  21. def OAI.SnakyPrototype.Certificate21.required_684_i2 line 87
  22. def OAI.SnakyPrototype.Certificate21.envelope_684_i2 line 88
  23. def OAI.SnakyPrototype.Certificate21.childrenC_684_i2 line 89
  24. def OAI.SnakyPrototype.Certificate21.childrenD_684_i2 line 90
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_684_i2 line 91
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_684_i2 line 92
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_684_i2 line 93
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_684_i2 line 94
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_684_i2 line 95
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_684_i2 line 104
  31. def OAI.SnakyPrototype.Certificate21.required_684_i3 line 109
  32. def OAI.SnakyPrototype.Certificate21.envelope_684_i3 line 110
  33. def OAI.SnakyPrototype.Certificate21.childrenC_684_i3 line 111
  34. def OAI.SnakyPrototype.Certificate21.childrenD_684_i3 line 112
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_684_i3 line 113
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_684_i3 line 114
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_684_i3 line 115
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_684_i3 line 116
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_684_i3 line 117
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_684_i3 line 133
  41. def OAI.SnakyPrototype.Certificate21.required_684_i5 line 138
  42. def OAI.SnakyPrototype.Certificate21.envelope_684_i5 line 139
  43. def OAI.SnakyPrototype.Certificate21.childrenC_684_i5 line 140
  44. def OAI.SnakyPrototype.Certificate21.childrenD_684_i5 line 141
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_684_i5 line 142
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_684_i5 line 143
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_684_i5 line 144
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_684_i5 line 145
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_684_i5 line 146
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_684_i5 line 151
  51. def OAI.SnakyPrototype.Certificate21.required_684_i4 line 156
  52. def OAI.SnakyPrototype.Certificate21.envelope_684_i4 line 157
  53. def OAI.SnakyPrototype.Certificate21.childrenC_684_i4 line 158
  54. def OAI.SnakyPrototype.Certificate21.childrenD_684_i4 line 159
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_684_i4 line 160
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_684_i4 line 161
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_684_i4 line 162
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_684_i4 line 163
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_684_i4 line 164
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_684_i4 line 172
  61. def OAI.SnakyPrototype.Certificate21.required_684 line 177
  62. def OAI.SnakyPrototype.Certificate21.envelope_684 line 178
  63. def OAI.SnakyPrototype.Certificate21.childrenC_684 line 179
  64. def OAI.SnakyPrototype.Certificate21.childrenD_684 line 180
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_684 line 181
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_684 line 182
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_684 line 183
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_684 line 184
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_684 line 185
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_684 line 203
  71. def OAI.SnakyPrototype.Certificate21.required_691_i0 line 208
  72. def OAI.SnakyPrototype.Certificate21.envelope_691_i0 line 209
  73. def OAI.SnakyPrototype.Certificate21.childrenC_691_i0 line 210
  74. def OAI.SnakyPrototype.Certificate21.childrenD_691_i0 line 211
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_691_i0 line 212
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_691_i0 line 213
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_691_i0 line 214
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_691_i0 line 215
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_691_i0 line 216
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_691_i0 line 222
  81. def OAI.SnakyPrototype.Certificate21.required_691_i5 line 227
  82. def OAI.SnakyPrototype.Certificate21.envelope_691_i5 line 228
  83. def OAI.SnakyPrototype.Certificate21.childrenC_691_i5 line 229
  84. def OAI.SnakyPrototype.Certificate21.childrenD_691_i5 line 230
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_691_i5 line 231
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_691_i5 line 232
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_691_i5 line 233
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_691_i5 line 234
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_691_i5 line 235
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_691_i5 line 240
  91. def OAI.SnakyPrototype.Certificate21.required_691_i4 line 245
  92. def OAI.SnakyPrototype.Certificate21.envelope_691_i4 line 246
  93. def OAI.SnakyPrototype.Certificate21.childrenC_691_i4 line 247
  94. def OAI.SnakyPrototype.Certificate21.childrenD_691_i4 line 248
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_691_i4 line 249
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_691_i4 line 250
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_691_i4 line 251
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_691_i4 line 252
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_691_i4 line 253
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_691_i4 line 260
  101. def OAI.SnakyPrototype.Certificate21.required_691_i3 line 265
  102. def OAI.SnakyPrototype.Certificate21.envelope_691_i3 line 266
  103. def OAI.SnakyPrototype.Certificate21.childrenC_691_i3 line 267
  104. def OAI.SnakyPrototype.Certificate21.childrenD_691_i3 line 268
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_691_i3 line 269
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_691_i3 line 270
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_691_i3 line 271
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_691_i3 line 272
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_691_i3 line 273
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_691_i3 line 279
  111. def OAI.SnakyPrototype.Certificate21.required_691_i2 line 284
  112. def OAI.SnakyPrototype.Certificate21.envelope_691_i2 line 285
  113. def OAI.SnakyPrototype.Certificate21.childrenC_691_i2 line 286
  114. def OAI.SnakyPrototype.Certificate21.childrenD_691_i2 line 287
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_691_i2 line 288
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_691_i2 line 289
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_691_i2 line 290
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_691_i2 line 291
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_691_i2 line 292
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_691_i2 line 297
  121. def OAI.SnakyPrototype.Certificate21.required_691_i1 line 302
  122. def OAI.SnakyPrototype.Certificate21.envelope_691_i1 line 303
  123. def OAI.SnakyPrototype.Certificate21.childrenC_691_i1 line 304
  124. def OAI.SnakyPrototype.Certificate21.childrenD_691_i1 line 305
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_691_i1 line 306
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_691_i1 line 307
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_691_i1 line 308
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_691_i1 line 309
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_691_i1 line 310
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_691_i1 line 315
  131. def OAI.SnakyPrototype.Certificate21.required_691_i10 line 320
  132. def OAI.SnakyPrototype.Certificate21.envelope_691_i10 line 321
  133. def OAI.SnakyPrototype.Certificate21.childrenC_691_i10 line 322
  134. def OAI.SnakyPrototype.Certificate21.childrenD_691_i10 line 323
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_691_i10 line 324
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_691_i10 line 325
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_691_i10 line 326
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_691_i10 line 327
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_691_i10 line 328
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_691_i10 line 333
  141. def OAI.SnakyPrototype.Certificate21.required_691_i9 line 338
  142. def OAI.SnakyPrototype.Certificate21.envelope_691_i9 line 339
  143. def OAI.SnakyPrototype.Certificate21.childrenC_691_i9 line 340
  144. def OAI.SnakyPrototype.Certificate21.childrenD_691_i9 line 341
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_691_i9 line 342
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_691_i9 line 343
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_691_i9 line 344
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_691_i9 line 345
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_691_i9 line 346
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_691_i9 line 352
  151. def OAI.SnakyPrototype.Certificate21.required_691_i8 line 357
  152. def OAI.SnakyPrototype.Certificate21.envelope_691_i8 line 358
  153. def OAI.SnakyPrototype.Certificate21.childrenC_691_i8 line 359
  154. def OAI.SnakyPrototype.Certificate21.childrenD_691_i8 line 360
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_691_i8 line 361
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_691_i8 line 362
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_691_i8 line 363
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_691_i8 line 364
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_691_i8 line 365
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_691_i8 line 371
  161. def OAI.SnakyPrototype.Certificate21.required_691_i7 line 376
  162. def OAI.SnakyPrototype.Certificate21.envelope_691_i7 line 377
  163. def OAI.SnakyPrototype.Certificate21.childrenC_691_i7 line 378
  164. def OAI.SnakyPrototype.Certificate21.childrenD_691_i7 line 379
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_691_i7 line 380
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_691_i7 line 381
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_691_i7 line 382
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_691_i7 line 383
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_691_i7 line 384
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_691_i7 line 390
  171. def OAI.SnakyPrototype.Certificate21.required_691_i6 line 395
  172. def OAI.SnakyPrototype.Certificate21.envelope_691_i6 line 396
  173. def OAI.SnakyPrototype.Certificate21.childrenC_691_i6 line 397
  174. def OAI.SnakyPrototype.Certificate21.childrenD_691_i6 line 398
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_691_i6 line 399
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_691_i6 line 400
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_691_i6 line 401
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_691_i6 line 402
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_691_i6 line 403
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_691_i6 line 410
  181. def OAI.SnakyPrototype.Certificate21.required_691 line 415
  182. def OAI.SnakyPrototype.Certificate21.envelope_691 line 416
  183. def OAI.SnakyPrototype.Certificate21.childrenC_691 line 417
  184. def OAI.SnakyPrototype.Certificate21.childrenD_691 line 418
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_691 line 419
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_691 line 420
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_691 line 421
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_691 line 422
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_691 line 423
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_691 line 430
  191. def OAI.SnakyPrototype.Certificate21.height_684_i1 line 435
  192. def OAI.SnakyPrototype.Certificate21.childrenH_684_i1 line 436
  193. theorem OAI.SnakyPrototype.Certificate21.height_exact_684_i1 line 437
  194. theorem OAI.SnakyPrototype.Certificate21.required_origin_684_i1 line 438
  195. theorem OAI.SnakyPrototype.Certificate21.required_exact_684_i1 line 440
  196. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_684_i1 line 444
  197. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_684_i1 line 446
  198. def OAI.SnakyPrototype.Certificate21.checked_684_i1 line 450
  199. def OAI.SnakyPrototype.Certificate21.height_684_i0 line 458
  200. def OAI.SnakyPrototype.Certificate21.childrenH_684_i0 line 459
  201. theorem OAI.SnakyPrototype.Certificate21.height_exact_684_i0 line 460
  202. theorem OAI.SnakyPrototype.Certificate21.required_origin_684_i0 line 461
  203. theorem OAI.SnakyPrototype.Certificate21.required_exact_684_i0 line 463
  204. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_684_i0 line 467
  205. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_684_i0 line 469
  206. def OAI.SnakyPrototype.Certificate21.checked_684_i0 line 473
  207. def OAI.SnakyPrototype.Certificate21.height_684_i2 line 481
  208. def OAI.SnakyPrototype.Certificate21.childrenH_684_i2 line 482
  209. theorem OAI.SnakyPrototype.Certificate21.height_exact_684_i2 line 483
  210. theorem OAI.SnakyPrototype.Certificate21.required_origin_684_i2 line 484
  211. theorem OAI.SnakyPrototype.Certificate21.required_exact_684_i2 line 486
  212. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_684_i2 line 490
  213. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_684_i2 line 492
  214. def OAI.SnakyPrototype.Certificate21.checked_684_i2 line 496
  215. def OAI.SnakyPrototype.Certificate21.height_684_i3 line 504
  216. def OAI.SnakyPrototype.Certificate21.childrenH_684_i3 line 505
  217. theorem OAI.SnakyPrototype.Certificate21.height_exact_684_i3 line 506
  218. theorem OAI.SnakyPrototype.Certificate21.required_origin_684_i3 line 507
  219. theorem OAI.SnakyPrototype.Certificate21.required_exact_684_i3 line 509
  220. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_684_i3 line 513
  221. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_684_i3 line 515
  222. def OAI.SnakyPrototype.Certificate21.checked_684_i3 line 519
  223. def OAI.SnakyPrototype.Certificate21.height_684_i5 line 527
  224. def OAI.SnakyPrototype.Certificate21.childrenH_684_i5 line 528
  225. theorem OAI.SnakyPrototype.Certificate21.height_exact_684_i5 line 529
  226. theorem OAI.SnakyPrototype.Certificate21.required_origin_684_i5 line 530
  227. theorem OAI.SnakyPrototype.Certificate21.required_exact_684_i5 line 532
  228. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_684_i5 line 536
  229. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_684_i5 line 538
  230. def OAI.SnakyPrototype.Certificate21.checked_684_i5 line 542
  231. def OAI.SnakyPrototype.Certificate21.height_684_i4 line 550
  232. def OAI.SnakyPrototype.Certificate21.childrenH_684_i4 line 551
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_684_i4 line 552
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_684_i4 line 553
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_684_i4 line 555
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_684_i4 line 559
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_684_i4 line 561
  238. def OAI.SnakyPrototype.Certificate21.checked_684_i4 line 565
  239. def OAI.SnakyPrototype.Certificate21.height_684 line 573
  240. def OAI.SnakyPrototype.Certificate21.childrenH_684 line 574
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_684 line 575
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_684 line 576
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_684 line 578
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_684 line 582
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_684 line 584
  246. def OAI.SnakyPrototype.Certificate21.checked_684 line 588
  247. def OAI.SnakyPrototype.Certificate21.height_691_i0 line 596
  248. def OAI.SnakyPrototype.Certificate21.childrenH_691_i0 line 597
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_691_i0 line 598
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_691_i0 line 599
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_691_i0 line 601
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_691_i0 line 605
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_691_i0 line 607
  254. def OAI.SnakyPrototype.Certificate21.checked_691_i0 line 611
  255. def OAI.SnakyPrototype.Certificate21.height_691_i5 line 619
  256. def OAI.SnakyPrototype.Certificate21.childrenH_691_i5 line 620
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_691_i5 line 621
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_691_i5 line 622
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_691_i5 line 624
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_691_i5 line 628
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_691_i5 line 630
  262. def OAI.SnakyPrototype.Certificate21.checked_691_i5 line 634
  263. def OAI.SnakyPrototype.Certificate21.height_691_i4 line 642
  264. def OAI.SnakyPrototype.Certificate21.childrenH_691_i4 line 643
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_691_i4 line 644
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_691_i4 line 645
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_691_i4 line 647
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_691_i4 line 651
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_691_i4 line 653
  270. def OAI.SnakyPrototype.Certificate21.checked_691_i4 line 657
  271. def OAI.SnakyPrototype.Certificate21.height_691_i3 line 665
  272. def OAI.SnakyPrototype.Certificate21.childrenH_691_i3 line 666
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_691_i3 line 667
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_691_i3 line 668
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_691_i3 line 670
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_691_i3 line 674
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_691_i3 line 676
  278. def OAI.SnakyPrototype.Certificate21.checked_691_i3 line 680
  279. def OAI.SnakyPrototype.Certificate21.height_691_i2 line 688
  280. def OAI.SnakyPrototype.Certificate21.childrenH_691_i2 line 689
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_691_i2 line 690
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_691_i2 line 691
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_691_i2 line 693
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_691_i2 line 697
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_691_i2 line 699
  286. def OAI.SnakyPrototype.Certificate21.checked_691_i2 line 703
  287. def OAI.SnakyPrototype.Certificate21.height_691_i1 line 711
  288. def OAI.SnakyPrototype.Certificate21.childrenH_691_i1 line 712
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_691_i1 line 713
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_691_i1 line 714
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_691_i1 line 716
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_691_i1 line 720
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_691_i1 line 722
  294. def OAI.SnakyPrototype.Certificate21.checked_691_i1 line 726
  295. def OAI.SnakyPrototype.Certificate21.height_691_i10 line 734
  296. def OAI.SnakyPrototype.Certificate21.childrenH_691_i10 line 735
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_691_i10 line 736
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_691_i10 line 737
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_691_i10 line 739
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_691_i10 line 743
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_691_i10 line 745
  302. def OAI.SnakyPrototype.Certificate21.checked_691_i10 line 749
  303. def OAI.SnakyPrototype.Certificate21.height_691_i9 line 757
  304. def OAI.SnakyPrototype.Certificate21.childrenH_691_i9 line 758
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_691_i9 line 759
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_691_i9 line 760
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_691_i9 line 762
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_691_i9 line 766
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_691_i9 line 768
  310. def OAI.SnakyPrototype.Certificate21.checked_691_i9 line 772
  311. def OAI.SnakyPrototype.Certificate21.height_691_i8 line 780
  312. def OAI.SnakyPrototype.Certificate21.childrenH_691_i8 line 781
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_691_i8 line 782
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_691_i8 line 783
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_691_i8 line 785
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_691_i8 line 789
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_691_i8 line 791
  318. def OAI.SnakyPrototype.Certificate21.checked_691_i8 line 795
  319. def OAI.SnakyPrototype.Certificate21.height_691_i7 line 803
  320. def OAI.SnakyPrototype.Certificate21.childrenH_691_i7 line 804
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_691_i7 line 805
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_691_i7 line 806
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_691_i7 line 808
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_691_i7 line 812
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_691_i7 line 814
  326. def OAI.SnakyPrototype.Certificate21.checked_691_i7 line 818
  327. def OAI.SnakyPrototype.Certificate21.height_691_i6 line 826
  328. def OAI.SnakyPrototype.Certificate21.childrenH_691_i6 line 827
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_691_i6 line 828
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_691_i6 line 829
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_691_i6 line 831
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_691_i6 line 835
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_691_i6 line 837
  334. def OAI.SnakyPrototype.Certificate21.checked_691_i6 line 841
  335. def OAI.SnakyPrototype.Certificate21.height_691 line 849
  336. def OAI.SnakyPrototype.Certificate21.childrenH_691 line 850
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_691 line 851
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_691 line 852
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_691 line 854
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_691 line 858
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_691 line 860
  342. def OAI.SnakyPrototype.Certificate21.checked_691 line 864