OAI/GameTheory/SnakyTwentyOne/Cards/Height13Part06.lean

GitHub source file

324 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_695_i6 line 31
  2. def OAI.SnakyPrototype.Certificate21.envelope_695_i6 line 32
  3. def OAI.SnakyPrototype.Certificate21.childrenC_695_i6 line 33
  4. def OAI.SnakyPrototype.Certificate21.childrenD_695_i6 line 34
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_695_i6 line 35
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_695_i6 line 36
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_695_i6 line 37
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_695_i6 line 38
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_695_i6 line 39
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_695_i6 line 45
  11. def OAI.SnakyPrototype.Certificate21.required_695_i7 line 50
  12. def OAI.SnakyPrototype.Certificate21.envelope_695_i7 line 51
  13. def OAI.SnakyPrototype.Certificate21.childrenC_695_i7 line 52
  14. def OAI.SnakyPrototype.Certificate21.childrenD_695_i7 line 53
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_695_i7 line 54
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_695_i7 line 55
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_695_i7 line 56
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_695_i7 line 57
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_695_i7 line 58
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_695_i7 line 64
  21. def OAI.SnakyPrototype.Certificate21.required_695_i5 line 69
  22. def OAI.SnakyPrototype.Certificate21.envelope_695_i5 line 70
  23. def OAI.SnakyPrototype.Certificate21.childrenC_695_i5 line 71
  24. def OAI.SnakyPrototype.Certificate21.childrenD_695_i5 line 72
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_695_i5 line 73
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_695_i5 line 74
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_695_i5 line 75
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_695_i5 line 76
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_695_i5 line 77
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_695_i5 line 84
  31. def OAI.SnakyPrototype.Certificate21.required_695_i4 line 89
  32. def OAI.SnakyPrototype.Certificate21.envelope_695_i4 line 90
  33. def OAI.SnakyPrototype.Certificate21.childrenC_695_i4 line 91
  34. def OAI.SnakyPrototype.Certificate21.childrenD_695_i4 line 92
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_695_i4 line 93
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_695_i4 line 94
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_695_i4 line 95
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_695_i4 line 96
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_695_i4 line 97
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_695_i4 line 102
  41. def OAI.SnakyPrototype.Certificate21.required_695_i3 line 107
  42. def OAI.SnakyPrototype.Certificate21.envelope_695_i3 line 108
  43. def OAI.SnakyPrototype.Certificate21.childrenC_695_i3 line 109
  44. def OAI.SnakyPrototype.Certificate21.childrenD_695_i3 line 110
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_695_i3 line 111
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_695_i3 line 112
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_695_i3 line 113
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_695_i3 line 114
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_695_i3 line 115
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_695_i3 line 120
  51. def OAI.SnakyPrototype.Certificate21.required_695_i2 line 125
  52. def OAI.SnakyPrototype.Certificate21.envelope_695_i2 line 126
  53. def OAI.SnakyPrototype.Certificate21.childrenC_695_i2 line 127
  54. def OAI.SnakyPrototype.Certificate21.childrenD_695_i2 line 128
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_695_i2 line 129
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_695_i2 line 130
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_695_i2 line 131
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_695_i2 line 132
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_695_i2 line 133
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_695_i2 line 138
  61. def OAI.SnakyPrototype.Certificate21.required_695_i1 line 143
  62. def OAI.SnakyPrototype.Certificate21.envelope_695_i1 line 144
  63. def OAI.SnakyPrototype.Certificate21.childrenC_695_i1 line 145
  64. def OAI.SnakyPrototype.Certificate21.childrenD_695_i1 line 146
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_695_i1 line 147
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_695_i1 line 148
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_695_i1 line 149
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_695_i1 line 150
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_695_i1 line 151
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_695_i1 line 160
  71. def OAI.SnakyPrototype.Certificate21.required_695_i0 line 165
  72. def OAI.SnakyPrototype.Certificate21.envelope_695_i0 line 166
  73. def OAI.SnakyPrototype.Certificate21.childrenC_695_i0 line 167
  74. def OAI.SnakyPrototype.Certificate21.childrenD_695_i0 line 168
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_695_i0 line 169
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_695_i0 line 170
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_695_i0 line 171
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_695_i0 line 172
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_695_i0 line 173
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_695_i0 line 180
  81. def OAI.SnakyPrototype.Certificate21.required_695 line 185
  82. def OAI.SnakyPrototype.Certificate21.envelope_695 line 186
  83. def OAI.SnakyPrototype.Certificate21.childrenC_695 line 187
  84. def OAI.SnakyPrototype.Certificate21.childrenD_695 line 188
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_695 line 189
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_695 line 190
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_695 line 191
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_695 line 192
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_695 line 193
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_695 line 201
  91. def OAI.SnakyPrototype.Certificate21.required_696_i1 line 206
  92. def OAI.SnakyPrototype.Certificate21.envelope_696_i1 line 207
  93. def OAI.SnakyPrototype.Certificate21.childrenC_696_i1 line 208
  94. def OAI.SnakyPrototype.Certificate21.childrenD_696_i1 line 209
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_696_i1 line 210
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_696_i1 line 211
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_696_i1 line 212
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_696_i1 line 213
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_696_i1 line 214
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_696_i1 line 219
  101. def OAI.SnakyPrototype.Certificate21.required_696_i0 line 224
  102. def OAI.SnakyPrototype.Certificate21.envelope_696_i0 line 225
  103. def OAI.SnakyPrototype.Certificate21.childrenC_696_i0 line 226
  104. def OAI.SnakyPrototype.Certificate21.childrenD_696_i0 line 227
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_696_i0 line 228
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_696_i0 line 229
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_696_i0 line 230
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_696_i0 line 231
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_696_i0 line 232
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_696_i0 line 239
  111. def OAI.SnakyPrototype.Certificate21.required_696 line 244
  112. def OAI.SnakyPrototype.Certificate21.envelope_696 line 245
  113. def OAI.SnakyPrototype.Certificate21.childrenC_696 line 246
  114. def OAI.SnakyPrototype.Certificate21.childrenD_696 line 247
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_696 line 248
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_696 line 249
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_696 line 250
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_696 line 251
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_696 line 252
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_696 line 261
  121. def OAI.SnakyPrototype.Certificate21.required_709_i2 line 266
  122. def OAI.SnakyPrototype.Certificate21.envelope_709_i2 line 267
  123. def OAI.SnakyPrototype.Certificate21.childrenC_709_i2 line 268
  124. def OAI.SnakyPrototype.Certificate21.childrenD_709_i2 line 269
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_709_i2 line 270
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_709_i2 line 271
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_709_i2 line 272
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_709_i2 line 273
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_709_i2 line 274
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_709_i2 line 280
  131. def OAI.SnakyPrototype.Certificate21.required_709_i1 line 285
  132. def OAI.SnakyPrototype.Certificate21.envelope_709_i1 line 286
  133. def OAI.SnakyPrototype.Certificate21.childrenC_709_i1 line 287
  134. def OAI.SnakyPrototype.Certificate21.childrenD_709_i1 line 288
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_709_i1 line 289
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_709_i1 line 290
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_709_i1 line 291
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_709_i1 line 292
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_709_i1 line 293
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_709_i1 line 299
  141. def OAI.SnakyPrototype.Certificate21.required_709_i4 line 304
  142. def OAI.SnakyPrototype.Certificate21.envelope_709_i4 line 305
  143. def OAI.SnakyPrototype.Certificate21.childrenC_709_i4 line 306
  144. def OAI.SnakyPrototype.Certificate21.childrenD_709_i4 line 307
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_709_i4 line 308
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_709_i4 line 309
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_709_i4 line 310
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_709_i4 line 311
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_709_i4 line 312
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_709_i4 line 317
  151. def OAI.SnakyPrototype.Certificate21.required_709_i3 line 322
  152. def OAI.SnakyPrototype.Certificate21.envelope_709_i3 line 323
  153. def OAI.SnakyPrototype.Certificate21.childrenC_709_i3 line 324
  154. def OAI.SnakyPrototype.Certificate21.childrenD_709_i3 line 325
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_709_i3 line 326
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_709_i3 line 327
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_709_i3 line 328
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_709_i3 line 329
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_709_i3 line 330
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_709_i3 line 336
  161. def OAI.SnakyPrototype.Certificate21.required_709_i0 line 341
  162. def OAI.SnakyPrototype.Certificate21.envelope_709_i0 line 342
  163. def OAI.SnakyPrototype.Certificate21.childrenC_709_i0 line 343
  164. def OAI.SnakyPrototype.Certificate21.childrenD_709_i0 line 344
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_709_i0 line 345
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_709_i0 line 346
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_709_i0 line 347
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_709_i0 line 348
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_709_i0 line 349
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_709_i0 line 359
  171. def OAI.SnakyPrototype.Certificate21.required_709 line 364
  172. def OAI.SnakyPrototype.Certificate21.envelope_709 line 365
  173. def OAI.SnakyPrototype.Certificate21.childrenC_709 line 366
  174. def OAI.SnakyPrototype.Certificate21.childrenD_709 line 367
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_709 line 368
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_709 line 369
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_709 line 370
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_709 line 371
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_709 line 372
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_709 line 379
  181. def OAI.SnakyPrototype.Certificate21.height_695_i6 line 384
  182. def OAI.SnakyPrototype.Certificate21.childrenH_695_i6 line 385
  183. theorem OAI.SnakyPrototype.Certificate21.height_exact_695_i6 line 386
  184. theorem OAI.SnakyPrototype.Certificate21.required_origin_695_i6 line 387
  185. theorem OAI.SnakyPrototype.Certificate21.required_exact_695_i6 line 389
  186. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_695_i6 line 393
  187. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_695_i6 line 395
  188. def OAI.SnakyPrototype.Certificate21.checked_695_i6 line 399
  189. def OAI.SnakyPrototype.Certificate21.height_695_i7 line 407
  190. def OAI.SnakyPrototype.Certificate21.childrenH_695_i7 line 408
  191. theorem OAI.SnakyPrototype.Certificate21.height_exact_695_i7 line 409
  192. theorem OAI.SnakyPrototype.Certificate21.required_origin_695_i7 line 410
  193. theorem OAI.SnakyPrototype.Certificate21.required_exact_695_i7 line 412
  194. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_695_i7 line 416
  195. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_695_i7 line 418
  196. def OAI.SnakyPrototype.Certificate21.checked_695_i7 line 422
  197. def OAI.SnakyPrototype.Certificate21.height_695_i5 line 430
  198. def OAI.SnakyPrototype.Certificate21.childrenH_695_i5 line 431
  199. theorem OAI.SnakyPrototype.Certificate21.height_exact_695_i5 line 432
  200. theorem OAI.SnakyPrototype.Certificate21.required_origin_695_i5 line 433
  201. theorem OAI.SnakyPrototype.Certificate21.required_exact_695_i5 line 435
  202. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_695_i5 line 439
  203. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_695_i5 line 441
  204. def OAI.SnakyPrototype.Certificate21.checked_695_i5 line 445
  205. def OAI.SnakyPrototype.Certificate21.height_695_i4 line 453
  206. def OAI.SnakyPrototype.Certificate21.childrenH_695_i4 line 454
  207. theorem OAI.SnakyPrototype.Certificate21.height_exact_695_i4 line 455
  208. theorem OAI.SnakyPrototype.Certificate21.required_origin_695_i4 line 456
  209. theorem OAI.SnakyPrototype.Certificate21.required_exact_695_i4 line 458
  210. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_695_i4 line 462
  211. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_695_i4 line 464
  212. def OAI.SnakyPrototype.Certificate21.checked_695_i4 line 468
  213. def OAI.SnakyPrototype.Certificate21.height_695_i3 line 476
  214. def OAI.SnakyPrototype.Certificate21.childrenH_695_i3 line 477
  215. theorem OAI.SnakyPrototype.Certificate21.height_exact_695_i3 line 478
  216. theorem OAI.SnakyPrototype.Certificate21.required_origin_695_i3 line 479
  217. theorem OAI.SnakyPrototype.Certificate21.required_exact_695_i3 line 481
  218. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_695_i3 line 485
  219. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_695_i3 line 487
  220. def OAI.SnakyPrototype.Certificate21.checked_695_i3 line 491
  221. def OAI.SnakyPrototype.Certificate21.height_695_i2 line 499
  222. def OAI.SnakyPrototype.Certificate21.childrenH_695_i2 line 500
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_695_i2 line 501
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_695_i2 line 502
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_695_i2 line 504
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_695_i2 line 508
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_695_i2 line 510
  228. def OAI.SnakyPrototype.Certificate21.checked_695_i2 line 514
  229. def OAI.SnakyPrototype.Certificate21.height_695_i1 line 522
  230. def OAI.SnakyPrototype.Certificate21.childrenH_695_i1 line 523
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_695_i1 line 524
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_695_i1 line 525
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_695_i1 line 527
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_695_i1 line 531
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_695_i1 line 533
  236. def OAI.SnakyPrototype.Certificate21.checked_695_i1 line 537
  237. def OAI.SnakyPrototype.Certificate21.height_695_i0 line 545
  238. def OAI.SnakyPrototype.Certificate21.childrenH_695_i0 line 546
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_695_i0 line 547
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_695_i0 line 548
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_695_i0 line 550
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_695_i0 line 554
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_695_i0 line 556
  244. def OAI.SnakyPrototype.Certificate21.checked_695_i0 line 560
  245. def OAI.SnakyPrototype.Certificate21.height_695 line 568
  246. def OAI.SnakyPrototype.Certificate21.childrenH_695 line 569
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_695 line 570
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_695 line 571
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_695 line 573
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_695 line 577
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_695 line 579
  252. def OAI.SnakyPrototype.Certificate21.checked_695 line 583
  253. def OAI.SnakyPrototype.Certificate21.height_696_i1 line 591
  254. def OAI.SnakyPrototype.Certificate21.childrenH_696_i1 line 592
  255. theorem OAI.SnakyPrototype.Certificate21.height_exact_696_i1 line 593
  256. theorem OAI.SnakyPrototype.Certificate21.required_origin_696_i1 line 594
  257. theorem OAI.SnakyPrototype.Certificate21.required_exact_696_i1 line 596
  258. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_696_i1 line 600
  259. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_696_i1 line 602
  260. def OAI.SnakyPrototype.Certificate21.checked_696_i1 line 606
  261. def OAI.SnakyPrototype.Certificate21.height_696_i0 line 614
  262. def OAI.SnakyPrototype.Certificate21.childrenH_696_i0 line 615
  263. theorem OAI.SnakyPrototype.Certificate21.height_exact_696_i0 line 616
  264. theorem OAI.SnakyPrototype.Certificate21.required_origin_696_i0 line 617
  265. theorem OAI.SnakyPrototype.Certificate21.required_exact_696_i0 line 619
  266. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_696_i0 line 623
  267. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_696_i0 line 625
  268. def OAI.SnakyPrototype.Certificate21.checked_696_i0 line 629
  269. def OAI.SnakyPrototype.Certificate21.height_696 line 637
  270. def OAI.SnakyPrototype.Certificate21.childrenH_696 line 638
  271. theorem OAI.SnakyPrototype.Certificate21.height_exact_696 line 639
  272. theorem OAI.SnakyPrototype.Certificate21.required_origin_696 line 640
  273. theorem OAI.SnakyPrototype.Certificate21.required_exact_696 line 642
  274. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_696 line 646
  275. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_696 line 648
  276. def OAI.SnakyPrototype.Certificate21.checked_696 line 652
  277. def OAI.SnakyPrototype.Certificate21.height_709_i2 line 660
  278. def OAI.SnakyPrototype.Certificate21.childrenH_709_i2 line 661
  279. theorem OAI.SnakyPrototype.Certificate21.height_exact_709_i2 line 662
  280. theorem OAI.SnakyPrototype.Certificate21.required_origin_709_i2 line 663
  281. theorem OAI.SnakyPrototype.Certificate21.required_exact_709_i2 line 665
  282. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_709_i2 line 669
  283. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_709_i2 line 671
  284. def OAI.SnakyPrototype.Certificate21.checked_709_i2 line 675
  285. def OAI.SnakyPrototype.Certificate21.height_709_i1 line 683
  286. def OAI.SnakyPrototype.Certificate21.childrenH_709_i1 line 684
  287. theorem OAI.SnakyPrototype.Certificate21.height_exact_709_i1 line 685
  288. theorem OAI.SnakyPrototype.Certificate21.required_origin_709_i1 line 686
  289. theorem OAI.SnakyPrototype.Certificate21.required_exact_709_i1 line 688
  290. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_709_i1 line 692
  291. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_709_i1 line 694
  292. def OAI.SnakyPrototype.Certificate21.checked_709_i1 line 698
  293. def OAI.SnakyPrototype.Certificate21.height_709_i4 line 706
  294. def OAI.SnakyPrototype.Certificate21.childrenH_709_i4 line 707
  295. theorem OAI.SnakyPrototype.Certificate21.height_exact_709_i4 line 708
  296. theorem OAI.SnakyPrototype.Certificate21.required_origin_709_i4 line 709
  297. theorem OAI.SnakyPrototype.Certificate21.required_exact_709_i4 line 711
  298. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_709_i4 line 715
  299. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_709_i4 line 717
  300. def OAI.SnakyPrototype.Certificate21.checked_709_i4 line 721
  301. def OAI.SnakyPrototype.Certificate21.height_709_i3 line 729
  302. def OAI.SnakyPrototype.Certificate21.childrenH_709_i3 line 730
  303. theorem OAI.SnakyPrototype.Certificate21.height_exact_709_i3 line 731
  304. theorem OAI.SnakyPrototype.Certificate21.required_origin_709_i3 line 732
  305. theorem OAI.SnakyPrototype.Certificate21.required_exact_709_i3 line 734
  306. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_709_i3 line 738
  307. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_709_i3 line 740
  308. def OAI.SnakyPrototype.Certificate21.checked_709_i3 line 744
  309. def OAI.SnakyPrototype.Certificate21.height_709_i0 line 752
  310. def OAI.SnakyPrototype.Certificate21.childrenH_709_i0 line 753
  311. theorem OAI.SnakyPrototype.Certificate21.height_exact_709_i0 line 754
  312. theorem OAI.SnakyPrototype.Certificate21.required_origin_709_i0 line 755
  313. theorem OAI.SnakyPrototype.Certificate21.required_exact_709_i0 line 757
  314. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_709_i0 line 761
  315. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_709_i0 line 763
  316. def OAI.SnakyPrototype.Certificate21.checked_709_i0 line 767
  317. def OAI.SnakyPrototype.Certificate21.height_709 line 775
  318. def OAI.SnakyPrototype.Certificate21.childrenH_709 line 776
  319. theorem OAI.SnakyPrototype.Certificate21.height_exact_709 line 777
  320. theorem OAI.SnakyPrototype.Certificate21.required_origin_709 line 778
  321. theorem OAI.SnakyPrototype.Certificate21.required_exact_709 line 780
  322. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_709 line 784
  323. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_709 line 786
  324. def OAI.SnakyPrototype.Certificate21.checked_709 line 790