OAI/GameTheory/SnakyTwentyOne/Cards/Height11Part01.lean

GitHub source file

342 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_427_i6 line 25
  2. def OAI.SnakyPrototype.Certificate21.envelope_427_i6 line 26
  3. def OAI.SnakyPrototype.Certificate21.childrenC_427_i6 line 27
  4. def OAI.SnakyPrototype.Certificate21.childrenD_427_i6 line 28
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_427_i6 line 29
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_427_i6 line 30
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_427_i6 line 31
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_427_i6 line 32
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_427_i6 line 33
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_427_i6 line 38
  11. def OAI.SnakyPrototype.Certificate21.required_427_i5 line 43
  12. def OAI.SnakyPrototype.Certificate21.envelope_427_i5 line 44
  13. def OAI.SnakyPrototype.Certificate21.childrenC_427_i5 line 45
  14. def OAI.SnakyPrototype.Certificate21.childrenD_427_i5 line 46
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_427_i5 line 47
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_427_i5 line 48
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_427_i5 line 49
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_427_i5 line 50
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_427_i5 line 51
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_427_i5 line 56
  21. def OAI.SnakyPrototype.Certificate21.required_427_i4 line 61
  22. def OAI.SnakyPrototype.Certificate21.envelope_427_i4 line 62
  23. def OAI.SnakyPrototype.Certificate21.childrenC_427_i4 line 63
  24. def OAI.SnakyPrototype.Certificate21.childrenD_427_i4 line 64
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_427_i4 line 65
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_427_i4 line 66
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_427_i4 line 67
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_427_i4 line 68
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_427_i4 line 69
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_427_i4 line 74
  31. def OAI.SnakyPrototype.Certificate21.required_427_i9 line 79
  32. def OAI.SnakyPrototype.Certificate21.envelope_427_i9 line 80
  33. def OAI.SnakyPrototype.Certificate21.childrenC_427_i9 line 81
  34. def OAI.SnakyPrototype.Certificate21.childrenD_427_i9 line 82
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_427_i9 line 83
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_427_i9 line 84
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_427_i9 line 85
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_427_i9 line 86
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_427_i9 line 87
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_427_i9 line 92
  41. def OAI.SnakyPrototype.Certificate21.required_427_i8 line 97
  42. def OAI.SnakyPrototype.Certificate21.envelope_427_i8 line 98
  43. def OAI.SnakyPrototype.Certificate21.childrenC_427_i8 line 99
  44. def OAI.SnakyPrototype.Certificate21.childrenD_427_i8 line 100
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_427_i8 line 101
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_427_i8 line 102
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_427_i8 line 103
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_427_i8 line 104
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_427_i8 line 105
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_427_i8 line 110
  51. def OAI.SnakyPrototype.Certificate21.required_427_i7 line 115
  52. def OAI.SnakyPrototype.Certificate21.envelope_427_i7 line 116
  53. def OAI.SnakyPrototype.Certificate21.childrenC_427_i7 line 117
  54. def OAI.SnakyPrototype.Certificate21.childrenD_427_i7 line 118
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_427_i7 line 119
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_427_i7 line 120
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_427_i7 line 121
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_427_i7 line 122
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_427_i7 line 123
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_427_i7 line 128
  61. def OAI.SnakyPrototype.Certificate21.required_427_i3 line 133
  62. def OAI.SnakyPrototype.Certificate21.envelope_427_i3 line 134
  63. def OAI.SnakyPrototype.Certificate21.childrenC_427_i3 line 135
  64. def OAI.SnakyPrototype.Certificate21.childrenD_427_i3 line 136
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_427_i3 line 137
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_427_i3 line 138
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_427_i3 line 139
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_427_i3 line 140
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_427_i3 line 141
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_427_i3 line 148
  71. def OAI.SnakyPrototype.Certificate21.required_427_i2 line 153
  72. def OAI.SnakyPrototype.Certificate21.envelope_427_i2 line 154
  73. def OAI.SnakyPrototype.Certificate21.childrenC_427_i2 line 155
  74. def OAI.SnakyPrototype.Certificate21.childrenD_427_i2 line 156
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_427_i2 line 157
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_427_i2 line 158
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_427_i2 line 159
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_427_i2 line 160
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_427_i2 line 161
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_427_i2 line 166
  81. def OAI.SnakyPrototype.Certificate21.required_427_i1 line 171
  82. def OAI.SnakyPrototype.Certificate21.envelope_427_i1 line 172
  83. def OAI.SnakyPrototype.Certificate21.childrenC_427_i1 line 173
  84. def OAI.SnakyPrototype.Certificate21.childrenD_427_i1 line 174
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_427_i1 line 175
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_427_i1 line 176
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_427_i1 line 177
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_427_i1 line 178
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_427_i1 line 179
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_427_i1 line 184
  91. def OAI.SnakyPrototype.Certificate21.required_427_i0 line 189
  92. def OAI.SnakyPrototype.Certificate21.envelope_427_i0 line 190
  93. def OAI.SnakyPrototype.Certificate21.childrenC_427_i0 line 191
  94. def OAI.SnakyPrototype.Certificate21.childrenD_427_i0 line 192
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_427_i0 line 193
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_427_i0 line 194
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_427_i0 line 195
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_427_i0 line 196
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_427_i0 line 197
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_427_i0 line 202
  101. def OAI.SnakyPrototype.Certificate21.required_427 line 207
  102. def OAI.SnakyPrototype.Certificate21.envelope_427 line 208
  103. def OAI.SnakyPrototype.Certificate21.childrenC_427 line 209
  104. def OAI.SnakyPrototype.Certificate21.childrenD_427 line 210
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_427 line 211
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_427 line 212
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_427 line 213
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_427 line 214
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_427 line 215
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_427 line 220
  111. def OAI.SnakyPrototype.Certificate21.required_463_i0 line 225
  112. def OAI.SnakyPrototype.Certificate21.envelope_463_i0 line 226
  113. def OAI.SnakyPrototype.Certificate21.childrenC_463_i0 line 227
  114. def OAI.SnakyPrototype.Certificate21.childrenD_463_i0 line 228
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_463_i0 line 229
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_463_i0 line 230
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_463_i0 line 231
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_463_i0 line 232
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_463_i0 line 233
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_463_i0 line 238
  121. def OAI.SnakyPrototype.Certificate21.required_463 line 243
  122. def OAI.SnakyPrototype.Certificate21.envelope_463 line 244
  123. def OAI.SnakyPrototype.Certificate21.childrenC_463 line 245
  124. def OAI.SnakyPrototype.Certificate21.childrenD_463 line 246
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_463 line 247
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_463 line 248
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_463 line 249
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_463 line 250
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_463 line 251
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_463 line 259
  131. def OAI.SnakyPrototype.Certificate21.required_467 line 264
  132. def OAI.SnakyPrototype.Certificate21.envelope_467 line 265
  133. def OAI.SnakyPrototype.Certificate21.childrenC_467 line 266
  134. def OAI.SnakyPrototype.Certificate21.childrenD_467 line 267
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_467 line 268
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_467 line 269
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_467 line 270
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_467 line 271
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_467 line 272
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_467 line 279
  141. def OAI.SnakyPrototype.Certificate21.required_468_i1 line 284
  142. def OAI.SnakyPrototype.Certificate21.envelope_468_i1 line 285
  143. def OAI.SnakyPrototype.Certificate21.childrenC_468_i1 line 286
  144. def OAI.SnakyPrototype.Certificate21.childrenD_468_i1 line 287
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_468_i1 line 288
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_468_i1 line 289
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_468_i1 line 290
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_468_i1 line 291
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_468_i1 line 292
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_468_i1 line 299
  151. def OAI.SnakyPrototype.Certificate21.required_468_i3 line 304
  152. def OAI.SnakyPrototype.Certificate21.envelope_468_i3 line 305
  153. def OAI.SnakyPrototype.Certificate21.childrenC_468_i3 line 306
  154. def OAI.SnakyPrototype.Certificate21.childrenD_468_i3 line 307
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_468_i3 line 308
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_468_i3 line 309
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_468_i3 line 310
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_468_i3 line 311
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_468_i3 line 312
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_468_i3 line 320
  161. def OAI.SnakyPrototype.Certificate21.required_468_i2 line 325
  162. def OAI.SnakyPrototype.Certificate21.envelope_468_i2 line 326
  163. def OAI.SnakyPrototype.Certificate21.childrenC_468_i2 line 327
  164. def OAI.SnakyPrototype.Certificate21.childrenD_468_i2 line 328
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_468_i2 line 329
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_468_i2 line 330
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_468_i2 line 331
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_468_i2 line 332
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_468_i2 line 333
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_468_i2 line 340
  171. def OAI.SnakyPrototype.Certificate21.required_468_i0 line 345
  172. def OAI.SnakyPrototype.Certificate21.envelope_468_i0 line 346
  173. def OAI.SnakyPrototype.Certificate21.childrenC_468_i0 line 347
  174. def OAI.SnakyPrototype.Certificate21.childrenD_468_i0 line 348
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_468_i0 line 349
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_468_i0 line 350
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_468_i0 line 351
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_468_i0 line 352
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_468_i0 line 353
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_468_i0 line 359
  181. def OAI.SnakyPrototype.Certificate21.required_468 line 364
  182. def OAI.SnakyPrototype.Certificate21.envelope_468 line 365
  183. def OAI.SnakyPrototype.Certificate21.childrenC_468 line 366
  184. def OAI.SnakyPrototype.Certificate21.childrenD_468 line 367
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_468 line 368
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_468 line 369
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_468 line 370
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_468 line 371
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_468 line 372
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_468 line 379
  191. def OAI.SnakyPrototype.Certificate21.height_427_i6 line 384
  192. def OAI.SnakyPrototype.Certificate21.childrenH_427_i6 line 385
  193. theorem OAI.SnakyPrototype.Certificate21.height_exact_427_i6 line 386
  194. theorem OAI.SnakyPrototype.Certificate21.required_origin_427_i6 line 387
  195. theorem OAI.SnakyPrototype.Certificate21.required_exact_427_i6 line 389
  196. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_427_i6 line 393
  197. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_427_i6 line 395
  198. def OAI.SnakyPrototype.Certificate21.checked_427_i6 line 399
  199. def OAI.SnakyPrototype.Certificate21.height_427_i5 line 407
  200. def OAI.SnakyPrototype.Certificate21.childrenH_427_i5 line 408
  201. theorem OAI.SnakyPrototype.Certificate21.height_exact_427_i5 line 409
  202. theorem OAI.SnakyPrototype.Certificate21.required_origin_427_i5 line 410
  203. theorem OAI.SnakyPrototype.Certificate21.required_exact_427_i5 line 412
  204. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_427_i5 line 416
  205. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_427_i5 line 418
  206. def OAI.SnakyPrototype.Certificate21.checked_427_i5 line 422
  207. def OAI.SnakyPrototype.Certificate21.height_427_i4 line 430
  208. def OAI.SnakyPrototype.Certificate21.childrenH_427_i4 line 431
  209. theorem OAI.SnakyPrototype.Certificate21.height_exact_427_i4 line 432
  210. theorem OAI.SnakyPrototype.Certificate21.required_origin_427_i4 line 433
  211. theorem OAI.SnakyPrototype.Certificate21.required_exact_427_i4 line 435
  212. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_427_i4 line 439
  213. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_427_i4 line 441
  214. def OAI.SnakyPrototype.Certificate21.checked_427_i4 line 445
  215. def OAI.SnakyPrototype.Certificate21.height_427_i9 line 453
  216. def OAI.SnakyPrototype.Certificate21.childrenH_427_i9 line 454
  217. theorem OAI.SnakyPrototype.Certificate21.height_exact_427_i9 line 455
  218. theorem OAI.SnakyPrototype.Certificate21.required_origin_427_i9 line 456
  219. theorem OAI.SnakyPrototype.Certificate21.required_exact_427_i9 line 458
  220. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_427_i9 line 462
  221. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_427_i9 line 464
  222. def OAI.SnakyPrototype.Certificate21.checked_427_i9 line 468
  223. def OAI.SnakyPrototype.Certificate21.height_427_i8 line 476
  224. def OAI.SnakyPrototype.Certificate21.childrenH_427_i8 line 477
  225. theorem OAI.SnakyPrototype.Certificate21.height_exact_427_i8 line 478
  226. theorem OAI.SnakyPrototype.Certificate21.required_origin_427_i8 line 479
  227. theorem OAI.SnakyPrototype.Certificate21.required_exact_427_i8 line 481
  228. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_427_i8 line 485
  229. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_427_i8 line 487
  230. def OAI.SnakyPrototype.Certificate21.checked_427_i8 line 491
  231. def OAI.SnakyPrototype.Certificate21.height_427_i7 line 499
  232. def OAI.SnakyPrototype.Certificate21.childrenH_427_i7 line 500
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_427_i7 line 501
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_427_i7 line 502
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_427_i7 line 504
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_427_i7 line 508
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_427_i7 line 510
  238. def OAI.SnakyPrototype.Certificate21.checked_427_i7 line 514
  239. def OAI.SnakyPrototype.Certificate21.height_427_i3 line 522
  240. def OAI.SnakyPrototype.Certificate21.childrenH_427_i3 line 523
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_427_i3 line 524
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_427_i3 line 525
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_427_i3 line 527
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_427_i3 line 531
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_427_i3 line 533
  246. def OAI.SnakyPrototype.Certificate21.checked_427_i3 line 537
  247. def OAI.SnakyPrototype.Certificate21.height_427_i2 line 545
  248. def OAI.SnakyPrototype.Certificate21.childrenH_427_i2 line 546
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_427_i2 line 547
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_427_i2 line 548
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_427_i2 line 550
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_427_i2 line 554
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_427_i2 line 556
  254. def OAI.SnakyPrototype.Certificate21.checked_427_i2 line 560
  255. def OAI.SnakyPrototype.Certificate21.height_427_i1 line 568
  256. def OAI.SnakyPrototype.Certificate21.childrenH_427_i1 line 569
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_427_i1 line 570
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_427_i1 line 571
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_427_i1 line 573
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_427_i1 line 577
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_427_i1 line 579
  262. def OAI.SnakyPrototype.Certificate21.checked_427_i1 line 583
  263. def OAI.SnakyPrototype.Certificate21.height_427_i0 line 591
  264. def OAI.SnakyPrototype.Certificate21.childrenH_427_i0 line 592
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_427_i0 line 593
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_427_i0 line 594
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_427_i0 line 596
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_427_i0 line 600
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_427_i0 line 602
  270. def OAI.SnakyPrototype.Certificate21.checked_427_i0 line 606
  271. def OAI.SnakyPrototype.Certificate21.height_427 line 614
  272. def OAI.SnakyPrototype.Certificate21.childrenH_427 line 615
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_427 line 616
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_427 line 617
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_427 line 619
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_427 line 623
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_427 line 625
  278. def OAI.SnakyPrototype.Certificate21.checked_427 line 629
  279. def OAI.SnakyPrototype.Certificate21.height_463_i0 line 637
  280. def OAI.SnakyPrototype.Certificate21.childrenH_463_i0 line 638
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_463_i0 line 639
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_463_i0 line 640
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_463_i0 line 642
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_463_i0 line 646
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_463_i0 line 648
  286. def OAI.SnakyPrototype.Certificate21.checked_463_i0 line 652
  287. def OAI.SnakyPrototype.Certificate21.height_463 line 660
  288. def OAI.SnakyPrototype.Certificate21.childrenH_463 line 661
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_463 line 662
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_463 line 663
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_463 line 665
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_463 line 669
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_463 line 671
  294. def OAI.SnakyPrototype.Certificate21.checked_463 line 675
  295. def OAI.SnakyPrototype.Certificate21.height_467 line 683
  296. def OAI.SnakyPrototype.Certificate21.childrenH_467 line 684
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_467 line 685
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_467 line 686
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_467 line 688
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_467 line 692
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_467 line 694
  302. def OAI.SnakyPrototype.Certificate21.checked_467 line 698
  303. def OAI.SnakyPrototype.Certificate21.height_468_i1 line 706
  304. def OAI.SnakyPrototype.Certificate21.childrenH_468_i1 line 707
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_468_i1 line 708
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_468_i1 line 709
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_468_i1 line 711
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_468_i1 line 715
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_468_i1 line 717
  310. def OAI.SnakyPrototype.Certificate21.checked_468_i1 line 721
  311. def OAI.SnakyPrototype.Certificate21.height_468_i3 line 729
  312. def OAI.SnakyPrototype.Certificate21.childrenH_468_i3 line 730
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_468_i3 line 731
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_468_i3 line 732
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_468_i3 line 734
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_468_i3 line 738
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_468_i3 line 740
  318. def OAI.SnakyPrototype.Certificate21.checked_468_i3 line 744
  319. def OAI.SnakyPrototype.Certificate21.height_468_i2 line 752
  320. def OAI.SnakyPrototype.Certificate21.childrenH_468_i2 line 753
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_468_i2 line 754
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_468_i2 line 755
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_468_i2 line 757
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_468_i2 line 761
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_468_i2 line 763
  326. def OAI.SnakyPrototype.Certificate21.checked_468_i2 line 767
  327. def OAI.SnakyPrototype.Certificate21.height_468_i0 line 775
  328. def OAI.SnakyPrototype.Certificate21.childrenH_468_i0 line 776
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_468_i0 line 777
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_468_i0 line 778
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_468_i0 line 780
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_468_i0 line 784
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_468_i0 line 786
  334. def OAI.SnakyPrototype.Certificate21.checked_468_i0 line 790
  335. def OAI.SnakyPrototype.Certificate21.height_468 line 798
  336. def OAI.SnakyPrototype.Certificate21.childrenH_468 line 799
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_468 line 800
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_468 line 801
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_468 line 803
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_468 line 807
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_468 line 809
  342. def OAI.SnakyPrototype.Certificate21.checked_468 line 813