OAI/GameTheory/SnakyTwentyOne/Cards/Height12Part04.lean

GitHub source file

360 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_632_i2 line 31
  2. def OAI.SnakyPrototype.Certificate21.envelope_632_i2 line 32
  3. def OAI.SnakyPrototype.Certificate21.childrenC_632_i2 line 33
  4. def OAI.SnakyPrototype.Certificate21.childrenD_632_i2 line 34
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_632_i2 line 35
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_632_i2 line 36
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_632_i2 line 37
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_632_i2 line 38
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_632_i2 line 39
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_632_i2 line 44
  11. def OAI.SnakyPrototype.Certificate21.required_632_i1 line 49
  12. def OAI.SnakyPrototype.Certificate21.envelope_632_i1 line 50
  13. def OAI.SnakyPrototype.Certificate21.childrenC_632_i1 line 51
  14. def OAI.SnakyPrototype.Certificate21.childrenD_632_i1 line 52
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_632_i1 line 53
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_632_i1 line 54
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_632_i1 line 55
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_632_i1 line 56
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_632_i1 line 57
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_632_i1 line 64
  21. def OAI.SnakyPrototype.Certificate21.required_632_i0 line 69
  22. def OAI.SnakyPrototype.Certificate21.envelope_632_i0 line 70
  23. def OAI.SnakyPrototype.Certificate21.childrenC_632_i0 line 71
  24. def OAI.SnakyPrototype.Certificate21.childrenD_632_i0 line 72
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_632_i0 line 73
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_632_i0 line 74
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_632_i0 line 75
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_632_i0 line 76
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_632_i0 line 77
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_632_i0 line 84
  31. def OAI.SnakyPrototype.Certificate21.required_632 line 89
  32. def OAI.SnakyPrototype.Certificate21.envelope_632 line 90
  33. def OAI.SnakyPrototype.Certificate21.childrenC_632 line 91
  34. def OAI.SnakyPrototype.Certificate21.childrenD_632 line 92
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_632 line 93
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_632 line 94
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_632 line 95
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_632 line 96
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_632 line 97
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_632 line 105
  41. def OAI.SnakyPrototype.Certificate21.required_635_i0 line 110
  42. def OAI.SnakyPrototype.Certificate21.envelope_635_i0 line 111
  43. def OAI.SnakyPrototype.Certificate21.childrenC_635_i0 line 112
  44. def OAI.SnakyPrototype.Certificate21.childrenD_635_i0 line 113
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_635_i0 line 114
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_635_i0 line 115
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_635_i0 line 116
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_635_i0 line 117
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_635_i0 line 118
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_635_i0 line 124
  51. def OAI.SnakyPrototype.Certificate21.required_635 line 129
  52. def OAI.SnakyPrototype.Certificate21.envelope_635 line 130
  53. def OAI.SnakyPrototype.Certificate21.childrenC_635 line 131
  54. def OAI.SnakyPrototype.Certificate21.childrenD_635 line 132
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_635 line 133
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_635 line 134
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_635 line 135
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_635 line 136
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_635 line 137
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_635 line 145
  61. def OAI.SnakyPrototype.Certificate21.required_649_i7 line 150
  62. def OAI.SnakyPrototype.Certificate21.envelope_649_i7 line 151
  63. def OAI.SnakyPrototype.Certificate21.childrenC_649_i7 line 152
  64. def OAI.SnakyPrototype.Certificate21.childrenD_649_i7 line 153
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_649_i7 line 154
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_649_i7 line 155
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_649_i7 line 156
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_649_i7 line 157
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_649_i7 line 158
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_649_i7 line 163
  71. def OAI.SnakyPrototype.Certificate21.required_649_i6 line 168
  72. def OAI.SnakyPrototype.Certificate21.envelope_649_i6 line 169
  73. def OAI.SnakyPrototype.Certificate21.childrenC_649_i6 line 170
  74. def OAI.SnakyPrototype.Certificate21.childrenD_649_i6 line 171
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_649_i6 line 172
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_649_i6 line 173
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_649_i6 line 174
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_649_i6 line 175
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_649_i6 line 176
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_649_i6 line 181
  81. def OAI.SnakyPrototype.Certificate21.required_649_i5 line 186
  82. def OAI.SnakyPrototype.Certificate21.envelope_649_i5 line 187
  83. def OAI.SnakyPrototype.Certificate21.childrenC_649_i5 line 188
  84. def OAI.SnakyPrototype.Certificate21.childrenD_649_i5 line 189
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_649_i5 line 190
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_649_i5 line 191
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_649_i5 line 192
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_649_i5 line 193
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_649_i5 line 194
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_649_i5 line 199
  91. def OAI.SnakyPrototype.Certificate21.required_649_i4 line 204
  92. def OAI.SnakyPrototype.Certificate21.envelope_649_i4 line 205
  93. def OAI.SnakyPrototype.Certificate21.childrenC_649_i4 line 206
  94. def OAI.SnakyPrototype.Certificate21.childrenD_649_i4 line 207
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_649_i4 line 208
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_649_i4 line 209
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_649_i4 line 210
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_649_i4 line 211
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_649_i4 line 212
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_649_i4 line 217
  101. def OAI.SnakyPrototype.Certificate21.required_649_i3 line 222
  102. def OAI.SnakyPrototype.Certificate21.envelope_649_i3 line 223
  103. def OAI.SnakyPrototype.Certificate21.childrenC_649_i3 line 224
  104. def OAI.SnakyPrototype.Certificate21.childrenD_649_i3 line 225
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_649_i3 line 226
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_649_i3 line 227
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_649_i3 line 228
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_649_i3 line 229
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_649_i3 line 230
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_649_i3 line 235
  111. def OAI.SnakyPrototype.Certificate21.required_649_i2 line 240
  112. def OAI.SnakyPrototype.Certificate21.envelope_649_i2 line 241
  113. def OAI.SnakyPrototype.Certificate21.childrenC_649_i2 line 242
  114. def OAI.SnakyPrototype.Certificate21.childrenD_649_i2 line 243
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_649_i2 line 244
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_649_i2 line 245
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_649_i2 line 246
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_649_i2 line 247
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_649_i2 line 248
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_649_i2 line 253
  121. def OAI.SnakyPrototype.Certificate21.required_649_i1 line 258
  122. def OAI.SnakyPrototype.Certificate21.envelope_649_i1 line 259
  123. def OAI.SnakyPrototype.Certificate21.childrenC_649_i1 line 260
  124. def OAI.SnakyPrototype.Certificate21.childrenD_649_i1 line 261
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_649_i1 line 262
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_649_i1 line 263
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_649_i1 line 264
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_649_i1 line 265
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_649_i1 line 266
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_649_i1 line 273
  131. def OAI.SnakyPrototype.Certificate21.required_649_i0 line 278
  132. def OAI.SnakyPrototype.Certificate21.envelope_649_i0 line 279
  133. def OAI.SnakyPrototype.Certificate21.childrenC_649_i0 line 280
  134. def OAI.SnakyPrototype.Certificate21.childrenD_649_i0 line 281
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_649_i0 line 282
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_649_i0 line 283
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_649_i0 line 284
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_649_i0 line 285
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_649_i0 line 286
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_649_i0 line 293
  141. def OAI.SnakyPrototype.Certificate21.required_649 line 298
  142. def OAI.SnakyPrototype.Certificate21.envelope_649 line 299
  143. def OAI.SnakyPrototype.Certificate21.childrenC_649 line 300
  144. def OAI.SnakyPrototype.Certificate21.childrenD_649 line 301
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_649 line 302
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_649 line 303
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_649 line 304
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_649 line 305
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_649 line 306
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_649 line 312
  151. def OAI.SnakyPrototype.Certificate21.required_654_i1 line 317
  152. def OAI.SnakyPrototype.Certificate21.envelope_654_i1 line 318
  153. def OAI.SnakyPrototype.Certificate21.childrenC_654_i1 line 319
  154. def OAI.SnakyPrototype.Certificate21.childrenD_654_i1 line 320
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_654_i1 line 321
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_654_i1 line 322
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_654_i1 line 323
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_654_i1 line 324
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_654_i1 line 325
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_654_i1 line 330
  161. def OAI.SnakyPrototype.Certificate21.required_654_i0 line 335
  162. def OAI.SnakyPrototype.Certificate21.envelope_654_i0 line 336
  163. def OAI.SnakyPrototype.Certificate21.childrenC_654_i0 line 337
  164. def OAI.SnakyPrototype.Certificate21.childrenD_654_i0 line 338
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_654_i0 line 339
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_654_i0 line 340
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_654_i0 line 341
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_654_i0 line 342
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_654_i0 line 343
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_654_i0 line 350
  171. def OAI.SnakyPrototype.Certificate21.required_654 line 355
  172. def OAI.SnakyPrototype.Certificate21.envelope_654 line 356
  173. def OAI.SnakyPrototype.Certificate21.childrenC_654 line 357
  174. def OAI.SnakyPrototype.Certificate21.childrenD_654 line 358
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_654 line 359
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_654 line 360
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_654 line 361
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_654 line 362
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_654 line 363
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_654 line 374
  181. def OAI.SnakyPrototype.Certificate21.required_677 line 379
  182. def OAI.SnakyPrototype.Certificate21.envelope_677 line 380
  183. def OAI.SnakyPrototype.Certificate21.childrenC_677 line 381
  184. def OAI.SnakyPrototype.Certificate21.childrenD_677 line 382
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_677 line 383
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_677 line 384
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_677 line 385
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_677 line 386
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_677 line 387
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_677 line 395
  191. def OAI.SnakyPrototype.Certificate21.required_687 line 400
  192. def OAI.SnakyPrototype.Certificate21.envelope_687 line 401
  193. def OAI.SnakyPrototype.Certificate21.childrenC_687 line 402
  194. def OAI.SnakyPrototype.Certificate21.childrenD_687 line 403
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_687 line 404
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_687 line 405
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_687 line 406
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_687 line 407
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_687 line 408
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_687 line 415
  201. def OAI.SnakyPrototype.Certificate21.height_632_i2 line 420
  202. def OAI.SnakyPrototype.Certificate21.childrenH_632_i2 line 421
  203. theorem OAI.SnakyPrototype.Certificate21.height_exact_632_i2 line 422
  204. theorem OAI.SnakyPrototype.Certificate21.required_origin_632_i2 line 423
  205. theorem OAI.SnakyPrototype.Certificate21.required_exact_632_i2 line 425
  206. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_632_i2 line 429
  207. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_632_i2 line 431
  208. def OAI.SnakyPrototype.Certificate21.checked_632_i2 line 435
  209. def OAI.SnakyPrototype.Certificate21.height_632_i1 line 443
  210. def OAI.SnakyPrototype.Certificate21.childrenH_632_i1 line 444
  211. theorem OAI.SnakyPrototype.Certificate21.height_exact_632_i1 line 445
  212. theorem OAI.SnakyPrototype.Certificate21.required_origin_632_i1 line 446
  213. theorem OAI.SnakyPrototype.Certificate21.required_exact_632_i1 line 448
  214. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_632_i1 line 452
  215. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_632_i1 line 454
  216. def OAI.SnakyPrototype.Certificate21.checked_632_i1 line 458
  217. def OAI.SnakyPrototype.Certificate21.height_632_i0 line 466
  218. def OAI.SnakyPrototype.Certificate21.childrenH_632_i0 line 467
  219. theorem OAI.SnakyPrototype.Certificate21.height_exact_632_i0 line 468
  220. theorem OAI.SnakyPrototype.Certificate21.required_origin_632_i0 line 469
  221. theorem OAI.SnakyPrototype.Certificate21.required_exact_632_i0 line 471
  222. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_632_i0 line 475
  223. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_632_i0 line 477
  224. def OAI.SnakyPrototype.Certificate21.checked_632_i0 line 481
  225. def OAI.SnakyPrototype.Certificate21.height_632 line 489
  226. def OAI.SnakyPrototype.Certificate21.childrenH_632 line 490
  227. theorem OAI.SnakyPrototype.Certificate21.height_exact_632 line 491
  228. theorem OAI.SnakyPrototype.Certificate21.required_origin_632 line 492
  229. theorem OAI.SnakyPrototype.Certificate21.required_exact_632 line 494
  230. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_632 line 498
  231. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_632 line 500
  232. def OAI.SnakyPrototype.Certificate21.checked_632 line 504
  233. def OAI.SnakyPrototype.Certificate21.height_635_i0 line 512
  234. def OAI.SnakyPrototype.Certificate21.childrenH_635_i0 line 513
  235. theorem OAI.SnakyPrototype.Certificate21.height_exact_635_i0 line 514
  236. theorem OAI.SnakyPrototype.Certificate21.required_origin_635_i0 line 515
  237. theorem OAI.SnakyPrototype.Certificate21.required_exact_635_i0 line 517
  238. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_635_i0 line 521
  239. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_635_i0 line 523
  240. def OAI.SnakyPrototype.Certificate21.checked_635_i0 line 527
  241. def OAI.SnakyPrototype.Certificate21.height_635 line 535
  242. def OAI.SnakyPrototype.Certificate21.childrenH_635 line 536
  243. theorem OAI.SnakyPrototype.Certificate21.height_exact_635 line 537
  244. theorem OAI.SnakyPrototype.Certificate21.required_origin_635 line 538
  245. theorem OAI.SnakyPrototype.Certificate21.required_exact_635 line 540
  246. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_635 line 544
  247. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_635 line 546
  248. def OAI.SnakyPrototype.Certificate21.checked_635 line 550
  249. def OAI.SnakyPrototype.Certificate21.height_649_i7 line 558
  250. def OAI.SnakyPrototype.Certificate21.childrenH_649_i7 line 559
  251. theorem OAI.SnakyPrototype.Certificate21.height_exact_649_i7 line 560
  252. theorem OAI.SnakyPrototype.Certificate21.required_origin_649_i7 line 561
  253. theorem OAI.SnakyPrototype.Certificate21.required_exact_649_i7 line 563
  254. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_649_i7 line 567
  255. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_649_i7 line 569
  256. def OAI.SnakyPrototype.Certificate21.checked_649_i7 line 573
  257. def OAI.SnakyPrototype.Certificate21.height_649_i6 line 581
  258. def OAI.SnakyPrototype.Certificate21.childrenH_649_i6 line 582
  259. theorem OAI.SnakyPrototype.Certificate21.height_exact_649_i6 line 583
  260. theorem OAI.SnakyPrototype.Certificate21.required_origin_649_i6 line 584
  261. theorem OAI.SnakyPrototype.Certificate21.required_exact_649_i6 line 586
  262. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_649_i6 line 590
  263. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_649_i6 line 592
  264. def OAI.SnakyPrototype.Certificate21.checked_649_i6 line 596
  265. def OAI.SnakyPrototype.Certificate21.height_649_i5 line 604
  266. def OAI.SnakyPrototype.Certificate21.childrenH_649_i5 line 605
  267. theorem OAI.SnakyPrototype.Certificate21.height_exact_649_i5 line 606
  268. theorem OAI.SnakyPrototype.Certificate21.required_origin_649_i5 line 607
  269. theorem OAI.SnakyPrototype.Certificate21.required_exact_649_i5 line 609
  270. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_649_i5 line 613
  271. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_649_i5 line 615
  272. def OAI.SnakyPrototype.Certificate21.checked_649_i5 line 619
  273. def OAI.SnakyPrototype.Certificate21.height_649_i4 line 627
  274. def OAI.SnakyPrototype.Certificate21.childrenH_649_i4 line 628
  275. theorem OAI.SnakyPrototype.Certificate21.height_exact_649_i4 line 629
  276. theorem OAI.SnakyPrototype.Certificate21.required_origin_649_i4 line 630
  277. theorem OAI.SnakyPrototype.Certificate21.required_exact_649_i4 line 632
  278. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_649_i4 line 636
  279. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_649_i4 line 638
  280. def OAI.SnakyPrototype.Certificate21.checked_649_i4 line 642
  281. def OAI.SnakyPrototype.Certificate21.height_649_i3 line 650
  282. def OAI.SnakyPrototype.Certificate21.childrenH_649_i3 line 651
  283. theorem OAI.SnakyPrototype.Certificate21.height_exact_649_i3 line 652
  284. theorem OAI.SnakyPrototype.Certificate21.required_origin_649_i3 line 653
  285. theorem OAI.SnakyPrototype.Certificate21.required_exact_649_i3 line 655
  286. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_649_i3 line 659
  287. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_649_i3 line 661
  288. def OAI.SnakyPrototype.Certificate21.checked_649_i3 line 665
  289. def OAI.SnakyPrototype.Certificate21.height_649_i2 line 673
  290. def OAI.SnakyPrototype.Certificate21.childrenH_649_i2 line 674
  291. theorem OAI.SnakyPrototype.Certificate21.height_exact_649_i2 line 675
  292. theorem OAI.SnakyPrototype.Certificate21.required_origin_649_i2 line 676
  293. theorem OAI.SnakyPrototype.Certificate21.required_exact_649_i2 line 678
  294. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_649_i2 line 682
  295. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_649_i2 line 684
  296. def OAI.SnakyPrototype.Certificate21.checked_649_i2 line 688
  297. def OAI.SnakyPrototype.Certificate21.height_649_i1 line 696
  298. def OAI.SnakyPrototype.Certificate21.childrenH_649_i1 line 697
  299. theorem OAI.SnakyPrototype.Certificate21.height_exact_649_i1 line 698
  300. theorem OAI.SnakyPrototype.Certificate21.required_origin_649_i1 line 699
  301. theorem OAI.SnakyPrototype.Certificate21.required_exact_649_i1 line 701
  302. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_649_i1 line 705
  303. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_649_i1 line 707
  304. def OAI.SnakyPrototype.Certificate21.checked_649_i1 line 711
  305. def OAI.SnakyPrototype.Certificate21.height_649_i0 line 719
  306. def OAI.SnakyPrototype.Certificate21.childrenH_649_i0 line 720
  307. theorem OAI.SnakyPrototype.Certificate21.height_exact_649_i0 line 721
  308. theorem OAI.SnakyPrototype.Certificate21.required_origin_649_i0 line 722
  309. theorem OAI.SnakyPrototype.Certificate21.required_exact_649_i0 line 724
  310. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_649_i0 line 728
  311. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_649_i0 line 730
  312. def OAI.SnakyPrototype.Certificate21.checked_649_i0 line 734
  313. def OAI.SnakyPrototype.Certificate21.height_649 line 742
  314. def OAI.SnakyPrototype.Certificate21.childrenH_649 line 743
  315. theorem OAI.SnakyPrototype.Certificate21.height_exact_649 line 744
  316. theorem OAI.SnakyPrototype.Certificate21.required_origin_649 line 745
  317. theorem OAI.SnakyPrototype.Certificate21.required_exact_649 line 747
  318. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_649 line 751
  319. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_649 line 753
  320. def OAI.SnakyPrototype.Certificate21.checked_649 line 757
  321. def OAI.SnakyPrototype.Certificate21.height_654_i1 line 765
  322. def OAI.SnakyPrototype.Certificate21.childrenH_654_i1 line 766
  323. theorem OAI.SnakyPrototype.Certificate21.height_exact_654_i1 line 767
  324. theorem OAI.SnakyPrototype.Certificate21.required_origin_654_i1 line 768
  325. theorem OAI.SnakyPrototype.Certificate21.required_exact_654_i1 line 770
  326. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_654_i1 line 774
  327. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_654_i1 line 776
  328. def OAI.SnakyPrototype.Certificate21.checked_654_i1 line 780
  329. def OAI.SnakyPrototype.Certificate21.height_654_i0 line 788
  330. def OAI.SnakyPrototype.Certificate21.childrenH_654_i0 line 789
  331. theorem OAI.SnakyPrototype.Certificate21.height_exact_654_i0 line 790
  332. theorem OAI.SnakyPrototype.Certificate21.required_origin_654_i0 line 791
  333. theorem OAI.SnakyPrototype.Certificate21.required_exact_654_i0 line 793
  334. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_654_i0 line 797
  335. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_654_i0 line 799
  336. def OAI.SnakyPrototype.Certificate21.checked_654_i0 line 803
  337. def OAI.SnakyPrototype.Certificate21.height_654 line 811
  338. def OAI.SnakyPrototype.Certificate21.childrenH_654 line 812
  339. theorem OAI.SnakyPrototype.Certificate21.height_exact_654 line 813
  340. theorem OAI.SnakyPrototype.Certificate21.required_origin_654 line 814
  341. theorem OAI.SnakyPrototype.Certificate21.required_exact_654 line 816
  342. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_654 line 820
  343. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_654 line 822
  344. def OAI.SnakyPrototype.Certificate21.checked_654 line 826
  345. def OAI.SnakyPrototype.Certificate21.height_677 line 834
  346. def OAI.SnakyPrototype.Certificate21.childrenH_677 line 835
  347. theorem OAI.SnakyPrototype.Certificate21.height_exact_677 line 836
  348. theorem OAI.SnakyPrototype.Certificate21.required_origin_677 line 837
  349. theorem OAI.SnakyPrototype.Certificate21.required_exact_677 line 839
  350. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_677 line 843
  351. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_677 line 845
  352. def OAI.SnakyPrototype.Certificate21.checked_677 line 849
  353. def OAI.SnakyPrototype.Certificate21.height_687 line 857
  354. def OAI.SnakyPrototype.Certificate21.childrenH_687 line 858
  355. theorem OAI.SnakyPrototype.Certificate21.height_exact_687 line 859
  356. theorem OAI.SnakyPrototype.Certificate21.required_origin_687 line 860
  357. theorem OAI.SnakyPrototype.Certificate21.required_exact_687 line 862
  358. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_687 line 866
  359. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_687 line 868
  360. def OAI.SnakyPrototype.Certificate21.checked_687 line 872