OAI/GameTheory/SnakyTwentyOne/Cards/Height11Part04.lean

GitHub source file

360 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_615_i5 line 33
  2. def OAI.SnakyPrototype.Certificate21.envelope_615_i5 line 34
  3. def OAI.SnakyPrototype.Certificate21.childrenC_615_i5 line 35
  4. def OAI.SnakyPrototype.Certificate21.childrenD_615_i5 line 36
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_615_i5 line 37
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_615_i5 line 38
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_615_i5 line 39
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_615_i5 line 40
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_615_i5 line 41
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_615_i5 line 47
  11. def OAI.SnakyPrototype.Certificate21.required_615_i4 line 52
  12. def OAI.SnakyPrototype.Certificate21.envelope_615_i4 line 53
  13. def OAI.SnakyPrototype.Certificate21.childrenC_615_i4 line 54
  14. def OAI.SnakyPrototype.Certificate21.childrenD_615_i4 line 55
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_615_i4 line 56
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_615_i4 line 57
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_615_i4 line 58
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_615_i4 line 59
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_615_i4 line 60
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_615_i4 line 65
  21. def OAI.SnakyPrototype.Certificate21.required_615_i3 line 70
  22. def OAI.SnakyPrototype.Certificate21.envelope_615_i3 line 71
  23. def OAI.SnakyPrototype.Certificate21.childrenC_615_i3 line 72
  24. def OAI.SnakyPrototype.Certificate21.childrenD_615_i3 line 73
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_615_i3 line 74
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_615_i3 line 75
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_615_i3 line 76
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_615_i3 line 77
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_615_i3 line 78
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_615_i3 line 83
  31. def OAI.SnakyPrototype.Certificate21.required_615_i2 line 88
  32. def OAI.SnakyPrototype.Certificate21.envelope_615_i2 line 89
  33. def OAI.SnakyPrototype.Certificate21.childrenC_615_i2 line 90
  34. def OAI.SnakyPrototype.Certificate21.childrenD_615_i2 line 91
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_615_i2 line 92
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_615_i2 line 93
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_615_i2 line 94
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_615_i2 line 95
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_615_i2 line 96
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_615_i2 line 102
  41. def OAI.SnakyPrototype.Certificate21.required_615_i1 line 107
  42. def OAI.SnakyPrototype.Certificate21.envelope_615_i1 line 108
  43. def OAI.SnakyPrototype.Certificate21.childrenC_615_i1 line 109
  44. def OAI.SnakyPrototype.Certificate21.childrenD_615_i1 line 110
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_615_i1 line 111
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_615_i1 line 112
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_615_i1 line 113
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_615_i1 line 114
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_615_i1 line 115
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_615_i1 line 121
  51. def OAI.SnakyPrototype.Certificate21.required_615_i0 line 126
  52. def OAI.SnakyPrototype.Certificate21.envelope_615_i0 line 127
  53. def OAI.SnakyPrototype.Certificate21.childrenC_615_i0 line 128
  54. def OAI.SnakyPrototype.Certificate21.childrenD_615_i0 line 129
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_615_i0 line 130
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_615_i0 line 131
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_615_i0 line 132
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_615_i0 line 133
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_615_i0 line 134
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_615_i0 line 144
  61. def OAI.SnakyPrototype.Certificate21.required_615 line 149
  62. def OAI.SnakyPrototype.Certificate21.envelope_615 line 150
  63. def OAI.SnakyPrototype.Certificate21.childrenC_615 line 151
  64. def OAI.SnakyPrototype.Certificate21.childrenD_615 line 152
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_615 line 153
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_615 line 154
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_615 line 155
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_615 line 156
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_615 line 157
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_615 line 163
  71. def OAI.SnakyPrototype.Certificate21.required_617 line 168
  72. def OAI.SnakyPrototype.Certificate21.envelope_617 line 169
  73. def OAI.SnakyPrototype.Certificate21.childrenC_617 line 170
  74. def OAI.SnakyPrototype.Certificate21.childrenD_617 line 171
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_617 line 172
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_617 line 173
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_617 line 174
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_617 line 175
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_617 line 176
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_617 line 183
  81. def OAI.SnakyPrototype.Certificate21.required_624_i1 line 188
  82. def OAI.SnakyPrototype.Certificate21.envelope_624_i1 line 189
  83. def OAI.SnakyPrototype.Certificate21.childrenC_624_i1 line 190
  84. def OAI.SnakyPrototype.Certificate21.childrenD_624_i1 line 191
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_624_i1 line 192
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_624_i1 line 193
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_624_i1 line 194
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_624_i1 line 195
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_624_i1 line 196
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_624_i1 line 201
  91. def OAI.SnakyPrototype.Certificate21.required_624_i0 line 206
  92. def OAI.SnakyPrototype.Certificate21.envelope_624_i0 line 207
  93. def OAI.SnakyPrototype.Certificate21.childrenC_624_i0 line 208
  94. def OAI.SnakyPrototype.Certificate21.childrenD_624_i0 line 209
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_624_i0 line 210
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_624_i0 line 211
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_624_i0 line 212
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_624_i0 line 213
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_624_i0 line 214
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_624_i0 line 221
  101. def OAI.SnakyPrototype.Certificate21.required_624 line 226
  102. def OAI.SnakyPrototype.Certificate21.envelope_624 line 227
  103. def OAI.SnakyPrototype.Certificate21.childrenC_624 line 228
  104. def OAI.SnakyPrototype.Certificate21.childrenD_624 line 229
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_624 line 230
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_624 line 231
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_624 line 232
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_624 line 233
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_624 line 234
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_624 line 240
  111. def OAI.SnakyPrototype.Certificate21.required_625_i2 line 245
  112. def OAI.SnakyPrototype.Certificate21.envelope_625_i2 line 246
  113. def OAI.SnakyPrototype.Certificate21.childrenC_625_i2 line 247
  114. def OAI.SnakyPrototype.Certificate21.childrenD_625_i2 line 248
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_625_i2 line 249
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_625_i2 line 250
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_625_i2 line 251
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_625_i2 line 252
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_625_i2 line 253
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_625_i2 line 258
  121. def OAI.SnakyPrototype.Certificate21.required_625_i1 line 263
  122. def OAI.SnakyPrototype.Certificate21.envelope_625_i1 line 264
  123. def OAI.SnakyPrototype.Certificate21.childrenC_625_i1 line 265
  124. def OAI.SnakyPrototype.Certificate21.childrenD_625_i1 line 266
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_625_i1 line 267
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_625_i1 line 268
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_625_i1 line 269
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_625_i1 line 270
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_625_i1 line 271
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_625_i1 line 277
  131. def OAI.SnakyPrototype.Certificate21.required_625_i0 line 282
  132. def OAI.SnakyPrototype.Certificate21.envelope_625_i0 line 283
  133. def OAI.SnakyPrototype.Certificate21.childrenC_625_i0 line 284
  134. def OAI.SnakyPrototype.Certificate21.childrenD_625_i0 line 285
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_625_i0 line 286
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_625_i0 line 287
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_625_i0 line 288
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_625_i0 line 289
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_625_i0 line 290
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_625_i0 line 297
  141. def OAI.SnakyPrototype.Certificate21.required_625 line 302
  142. def OAI.SnakyPrototype.Certificate21.envelope_625 line 303
  143. def OAI.SnakyPrototype.Certificate21.childrenC_625 line 304
  144. def OAI.SnakyPrototype.Certificate21.childrenD_625 line 305
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_625 line 306
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_625 line 307
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_625 line 308
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_625 line 309
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_625 line 310
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_625 line 318
  151. def OAI.SnakyPrototype.Certificate21.required_626_i1 line 323
  152. def OAI.SnakyPrototype.Certificate21.envelope_626_i1 line 324
  153. def OAI.SnakyPrototype.Certificate21.childrenC_626_i1 line 325
  154. def OAI.SnakyPrototype.Certificate21.childrenD_626_i1 line 326
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_626_i1 line 327
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_626_i1 line 328
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_626_i1 line 329
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_626_i1 line 330
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_626_i1 line 331
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_626_i1 line 336
  161. def OAI.SnakyPrototype.Certificate21.required_626_i0 line 341
  162. def OAI.SnakyPrototype.Certificate21.envelope_626_i0 line 342
  163. def OAI.SnakyPrototype.Certificate21.childrenC_626_i0 line 343
  164. def OAI.SnakyPrototype.Certificate21.childrenD_626_i0 line 344
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_626_i0 line 345
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_626_i0 line 346
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_626_i0 line 347
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_626_i0 line 348
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_626_i0 line 349
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_626_i0 line 355
  171. def OAI.SnakyPrototype.Certificate21.required_626_i3 line 360
  172. def OAI.SnakyPrototype.Certificate21.envelope_626_i3 line 361
  173. def OAI.SnakyPrototype.Certificate21.childrenC_626_i3 line 362
  174. def OAI.SnakyPrototype.Certificate21.childrenD_626_i3 line 363
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_626_i3 line 364
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_626_i3 line 365
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_626_i3 line 366
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_626_i3 line 367
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_626_i3 line 368
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_626_i3 line 373
  181. def OAI.SnakyPrototype.Certificate21.required_626_i2 line 378
  182. def OAI.SnakyPrototype.Certificate21.envelope_626_i2 line 379
  183. def OAI.SnakyPrototype.Certificate21.childrenC_626_i2 line 380
  184. def OAI.SnakyPrototype.Certificate21.childrenD_626_i2 line 381
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_626_i2 line 382
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_626_i2 line 383
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_626_i2 line 384
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_626_i2 line 385
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_626_i2 line 386
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_626_i2 line 392
  191. def OAI.SnakyPrototype.Certificate21.required_626 line 397
  192. def OAI.SnakyPrototype.Certificate21.envelope_626 line 398
  193. def OAI.SnakyPrototype.Certificate21.childrenC_626 line 399
  194. def OAI.SnakyPrototype.Certificate21.childrenD_626 line 400
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_626 line 401
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_626 line 402
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_626 line 403
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_626 line 404
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_626 line 405
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_626 line 413
  201. def OAI.SnakyPrototype.Certificate21.height_615_i5 line 418
  202. def OAI.SnakyPrototype.Certificate21.childrenH_615_i5 line 419
  203. theorem OAI.SnakyPrototype.Certificate21.height_exact_615_i5 line 420
  204. theorem OAI.SnakyPrototype.Certificate21.required_origin_615_i5 line 421
  205. theorem OAI.SnakyPrototype.Certificate21.required_exact_615_i5 line 423
  206. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_615_i5 line 427
  207. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_615_i5 line 429
  208. def OAI.SnakyPrototype.Certificate21.checked_615_i5 line 433
  209. def OAI.SnakyPrototype.Certificate21.height_615_i4 line 441
  210. def OAI.SnakyPrototype.Certificate21.childrenH_615_i4 line 442
  211. theorem OAI.SnakyPrototype.Certificate21.height_exact_615_i4 line 443
  212. theorem OAI.SnakyPrototype.Certificate21.required_origin_615_i4 line 444
  213. theorem OAI.SnakyPrototype.Certificate21.required_exact_615_i4 line 446
  214. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_615_i4 line 450
  215. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_615_i4 line 452
  216. def OAI.SnakyPrototype.Certificate21.checked_615_i4 line 456
  217. def OAI.SnakyPrototype.Certificate21.height_615_i3 line 464
  218. def OAI.SnakyPrototype.Certificate21.childrenH_615_i3 line 465
  219. theorem OAI.SnakyPrototype.Certificate21.height_exact_615_i3 line 466
  220. theorem OAI.SnakyPrototype.Certificate21.required_origin_615_i3 line 467
  221. theorem OAI.SnakyPrototype.Certificate21.required_exact_615_i3 line 469
  222. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_615_i3 line 473
  223. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_615_i3 line 475
  224. def OAI.SnakyPrototype.Certificate21.checked_615_i3 line 479
  225. def OAI.SnakyPrototype.Certificate21.height_615_i2 line 487
  226. def OAI.SnakyPrototype.Certificate21.childrenH_615_i2 line 488
  227. theorem OAI.SnakyPrototype.Certificate21.height_exact_615_i2 line 489
  228. theorem OAI.SnakyPrototype.Certificate21.required_origin_615_i2 line 490
  229. theorem OAI.SnakyPrototype.Certificate21.required_exact_615_i2 line 492
  230. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_615_i2 line 496
  231. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_615_i2 line 498
  232. def OAI.SnakyPrototype.Certificate21.checked_615_i2 line 502
  233. def OAI.SnakyPrototype.Certificate21.height_615_i1 line 510
  234. def OAI.SnakyPrototype.Certificate21.childrenH_615_i1 line 511
  235. theorem OAI.SnakyPrototype.Certificate21.height_exact_615_i1 line 512
  236. theorem OAI.SnakyPrototype.Certificate21.required_origin_615_i1 line 513
  237. theorem OAI.SnakyPrototype.Certificate21.required_exact_615_i1 line 515
  238. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_615_i1 line 519
  239. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_615_i1 line 521
  240. def OAI.SnakyPrototype.Certificate21.checked_615_i1 line 525
  241. def OAI.SnakyPrototype.Certificate21.height_615_i0 line 533
  242. def OAI.SnakyPrototype.Certificate21.childrenH_615_i0 line 534
  243. theorem OAI.SnakyPrototype.Certificate21.height_exact_615_i0 line 535
  244. theorem OAI.SnakyPrototype.Certificate21.required_origin_615_i0 line 536
  245. theorem OAI.SnakyPrototype.Certificate21.required_exact_615_i0 line 538
  246. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_615_i0 line 542
  247. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_615_i0 line 544
  248. def OAI.SnakyPrototype.Certificate21.checked_615_i0 line 548
  249. def OAI.SnakyPrototype.Certificate21.height_615 line 556
  250. def OAI.SnakyPrototype.Certificate21.childrenH_615 line 557
  251. theorem OAI.SnakyPrototype.Certificate21.height_exact_615 line 558
  252. theorem OAI.SnakyPrototype.Certificate21.required_origin_615 line 559
  253. theorem OAI.SnakyPrototype.Certificate21.required_exact_615 line 561
  254. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_615 line 565
  255. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_615 line 567
  256. def OAI.SnakyPrototype.Certificate21.checked_615 line 571
  257. def OAI.SnakyPrototype.Certificate21.height_617 line 579
  258. def OAI.SnakyPrototype.Certificate21.childrenH_617 line 580
  259. theorem OAI.SnakyPrototype.Certificate21.height_exact_617 line 581
  260. theorem OAI.SnakyPrototype.Certificate21.required_origin_617 line 582
  261. theorem OAI.SnakyPrototype.Certificate21.required_exact_617 line 584
  262. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_617 line 588
  263. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_617 line 590
  264. def OAI.SnakyPrototype.Certificate21.checked_617 line 594
  265. def OAI.SnakyPrototype.Certificate21.height_624_i1 line 602
  266. def OAI.SnakyPrototype.Certificate21.childrenH_624_i1 line 603
  267. theorem OAI.SnakyPrototype.Certificate21.height_exact_624_i1 line 604
  268. theorem OAI.SnakyPrototype.Certificate21.required_origin_624_i1 line 605
  269. theorem OAI.SnakyPrototype.Certificate21.required_exact_624_i1 line 607
  270. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_624_i1 line 611
  271. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_624_i1 line 613
  272. def OAI.SnakyPrototype.Certificate21.checked_624_i1 line 617
  273. def OAI.SnakyPrototype.Certificate21.height_624_i0 line 625
  274. def OAI.SnakyPrototype.Certificate21.childrenH_624_i0 line 626
  275. theorem OAI.SnakyPrototype.Certificate21.height_exact_624_i0 line 627
  276. theorem OAI.SnakyPrototype.Certificate21.required_origin_624_i0 line 628
  277. theorem OAI.SnakyPrototype.Certificate21.required_exact_624_i0 line 630
  278. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_624_i0 line 634
  279. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_624_i0 line 636
  280. def OAI.SnakyPrototype.Certificate21.checked_624_i0 line 640
  281. def OAI.SnakyPrototype.Certificate21.height_624 line 648
  282. def OAI.SnakyPrototype.Certificate21.childrenH_624 line 649
  283. theorem OAI.SnakyPrototype.Certificate21.height_exact_624 line 650
  284. theorem OAI.SnakyPrototype.Certificate21.required_origin_624 line 651
  285. theorem OAI.SnakyPrototype.Certificate21.required_exact_624 line 653
  286. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_624 line 657
  287. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_624 line 659
  288. def OAI.SnakyPrototype.Certificate21.checked_624 line 663
  289. def OAI.SnakyPrototype.Certificate21.height_625_i2 line 671
  290. def OAI.SnakyPrototype.Certificate21.childrenH_625_i2 line 672
  291. theorem OAI.SnakyPrototype.Certificate21.height_exact_625_i2 line 673
  292. theorem OAI.SnakyPrototype.Certificate21.required_origin_625_i2 line 674
  293. theorem OAI.SnakyPrototype.Certificate21.required_exact_625_i2 line 676
  294. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_625_i2 line 680
  295. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_625_i2 line 682
  296. def OAI.SnakyPrototype.Certificate21.checked_625_i2 line 686
  297. def OAI.SnakyPrototype.Certificate21.height_625_i1 line 694
  298. def OAI.SnakyPrototype.Certificate21.childrenH_625_i1 line 695
  299. theorem OAI.SnakyPrototype.Certificate21.height_exact_625_i1 line 696
  300. theorem OAI.SnakyPrototype.Certificate21.required_origin_625_i1 line 697
  301. theorem OAI.SnakyPrototype.Certificate21.required_exact_625_i1 line 699
  302. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_625_i1 line 703
  303. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_625_i1 line 705
  304. def OAI.SnakyPrototype.Certificate21.checked_625_i1 line 709
  305. def OAI.SnakyPrototype.Certificate21.height_625_i0 line 717
  306. def OAI.SnakyPrototype.Certificate21.childrenH_625_i0 line 718
  307. theorem OAI.SnakyPrototype.Certificate21.height_exact_625_i0 line 719
  308. theorem OAI.SnakyPrototype.Certificate21.required_origin_625_i0 line 720
  309. theorem OAI.SnakyPrototype.Certificate21.required_exact_625_i0 line 722
  310. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_625_i0 line 726
  311. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_625_i0 line 728
  312. def OAI.SnakyPrototype.Certificate21.checked_625_i0 line 732
  313. def OAI.SnakyPrototype.Certificate21.height_625 line 740
  314. def OAI.SnakyPrototype.Certificate21.childrenH_625 line 741
  315. theorem OAI.SnakyPrototype.Certificate21.height_exact_625 line 742
  316. theorem OAI.SnakyPrototype.Certificate21.required_origin_625 line 743
  317. theorem OAI.SnakyPrototype.Certificate21.required_exact_625 line 745
  318. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_625 line 749
  319. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_625 line 751
  320. def OAI.SnakyPrototype.Certificate21.checked_625 line 755
  321. def OAI.SnakyPrototype.Certificate21.height_626_i1 line 763
  322. def OAI.SnakyPrototype.Certificate21.childrenH_626_i1 line 764
  323. theorem OAI.SnakyPrototype.Certificate21.height_exact_626_i1 line 765
  324. theorem OAI.SnakyPrototype.Certificate21.required_origin_626_i1 line 766
  325. theorem OAI.SnakyPrototype.Certificate21.required_exact_626_i1 line 768
  326. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_626_i1 line 772
  327. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_626_i1 line 774
  328. def OAI.SnakyPrototype.Certificate21.checked_626_i1 line 778
  329. def OAI.SnakyPrototype.Certificate21.height_626_i0 line 786
  330. def OAI.SnakyPrototype.Certificate21.childrenH_626_i0 line 787
  331. theorem OAI.SnakyPrototype.Certificate21.height_exact_626_i0 line 788
  332. theorem OAI.SnakyPrototype.Certificate21.required_origin_626_i0 line 789
  333. theorem OAI.SnakyPrototype.Certificate21.required_exact_626_i0 line 791
  334. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_626_i0 line 795
  335. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_626_i0 line 797
  336. def OAI.SnakyPrototype.Certificate21.checked_626_i0 line 801
  337. def OAI.SnakyPrototype.Certificate21.height_626_i3 line 809
  338. def OAI.SnakyPrototype.Certificate21.childrenH_626_i3 line 810
  339. theorem OAI.SnakyPrototype.Certificate21.height_exact_626_i3 line 811
  340. theorem OAI.SnakyPrototype.Certificate21.required_origin_626_i3 line 812
  341. theorem OAI.SnakyPrototype.Certificate21.required_exact_626_i3 line 814
  342. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_626_i3 line 818
  343. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_626_i3 line 820
  344. def OAI.SnakyPrototype.Certificate21.checked_626_i3 line 824
  345. def OAI.SnakyPrototype.Certificate21.height_626_i2 line 832
  346. def OAI.SnakyPrototype.Certificate21.childrenH_626_i2 line 833
  347. theorem OAI.SnakyPrototype.Certificate21.height_exact_626_i2 line 834
  348. theorem OAI.SnakyPrototype.Certificate21.required_origin_626_i2 line 835
  349. theorem OAI.SnakyPrototype.Certificate21.required_exact_626_i2 line 837
  350. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_626_i2 line 841
  351. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_626_i2 line 843
  352. def OAI.SnakyPrototype.Certificate21.checked_626_i2 line 847
  353. def OAI.SnakyPrototype.Certificate21.height_626 line 855
  354. def OAI.SnakyPrototype.Certificate21.childrenH_626 line 856
  355. theorem OAI.SnakyPrototype.Certificate21.height_exact_626 line 857
  356. theorem OAI.SnakyPrototype.Certificate21.required_origin_626 line 858
  357. theorem OAI.SnakyPrototype.Certificate21.required_exact_626 line 860
  358. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_626 line 864
  359. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_626 line 866
  360. def OAI.SnakyPrototype.Certificate21.checked_626 line 870