OAI/GameTheory/SnakyTwentyOne/Cards/Height14Part01.lean

GitHub source file

414 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_553_i3 line 25
  2. def OAI.SnakyPrototype.Certificate21.envelope_553_i3 line 26
  3. def OAI.SnakyPrototype.Certificate21.childrenC_553_i3 line 27
  4. def OAI.SnakyPrototype.Certificate21.childrenD_553_i3 line 28
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_553_i3 line 29
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_553_i3 line 30
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_553_i3 line 31
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_553_i3 line 32
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_553_i3 line 33
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_553_i3 line 38
  11. def OAI.SnakyPrototype.Certificate21.required_553_i2 line 43
  12. def OAI.SnakyPrototype.Certificate21.envelope_553_i2 line 44
  13. def OAI.SnakyPrototype.Certificate21.childrenC_553_i2 line 45
  14. def OAI.SnakyPrototype.Certificate21.childrenD_553_i2 line 46
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_553_i2 line 47
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_553_i2 line 48
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_553_i2 line 49
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_553_i2 line 50
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_553_i2 line 51
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_553_i2 line 58
  21. def OAI.SnakyPrototype.Certificate21.required_553_i1 line 63
  22. def OAI.SnakyPrototype.Certificate21.envelope_553_i1 line 64
  23. def OAI.SnakyPrototype.Certificate21.childrenC_553_i1 line 65
  24. def OAI.SnakyPrototype.Certificate21.childrenD_553_i1 line 66
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_553_i1 line 67
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_553_i1 line 68
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_553_i1 line 69
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_553_i1 line 70
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_553_i1 line 71
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_553_i1 line 76
  31. def OAI.SnakyPrototype.Certificate21.required_553_i6 line 81
  32. def OAI.SnakyPrototype.Certificate21.envelope_553_i6 line 82
  33. def OAI.SnakyPrototype.Certificate21.childrenC_553_i6 line 83
  34. def OAI.SnakyPrototype.Certificate21.childrenD_553_i6 line 84
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_553_i6 line 85
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_553_i6 line 86
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_553_i6 line 87
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_553_i6 line 88
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_553_i6 line 89
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_553_i6 line 94
  41. def OAI.SnakyPrototype.Certificate21.required_553_i5 line 99
  42. def OAI.SnakyPrototype.Certificate21.envelope_553_i5 line 100
  43. def OAI.SnakyPrototype.Certificate21.childrenC_553_i5 line 101
  44. def OAI.SnakyPrototype.Certificate21.childrenD_553_i5 line 102
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_553_i5 line 103
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_553_i5 line 104
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_553_i5 line 105
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_553_i5 line 106
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_553_i5 line 107
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_553_i5 line 113
  51. def OAI.SnakyPrototype.Certificate21.required_553_i4 line 118
  52. def OAI.SnakyPrototype.Certificate21.envelope_553_i4 line 119
  53. def OAI.SnakyPrototype.Certificate21.childrenC_553_i4 line 120
  54. def OAI.SnakyPrototype.Certificate21.childrenD_553_i4 line 121
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_553_i4 line 122
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_553_i4 line 123
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_553_i4 line 124
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_553_i4 line 125
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_553_i4 line 126
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_553_i4 line 131
  61. def OAI.SnakyPrototype.Certificate21.required_553_i8 line 136
  62. def OAI.SnakyPrototype.Certificate21.envelope_553_i8 line 137
  63. def OAI.SnakyPrototype.Certificate21.childrenC_553_i8 line 138
  64. def OAI.SnakyPrototype.Certificate21.childrenD_553_i8 line 139
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_553_i8 line 140
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_553_i8 line 141
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_553_i8 line 142
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_553_i8 line 143
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_553_i8 line 144
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_553_i8 line 149
  71. def OAI.SnakyPrototype.Certificate21.required_553_i7 line 154
  72. def OAI.SnakyPrototype.Certificate21.envelope_553_i7 line 155
  73. def OAI.SnakyPrototype.Certificate21.childrenC_553_i7 line 156
  74. def OAI.SnakyPrototype.Certificate21.childrenD_553_i7 line 157
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_553_i7 line 158
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_553_i7 line 159
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_553_i7 line 160
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_553_i7 line 161
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_553_i7 line 162
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_553_i7 line 167
  81. def OAI.SnakyPrototype.Certificate21.required_553_i0 line 172
  82. def OAI.SnakyPrototype.Certificate21.envelope_553_i0 line 173
  83. def OAI.SnakyPrototype.Certificate21.childrenC_553_i0 line 174
  84. def OAI.SnakyPrototype.Certificate21.childrenD_553_i0 line 175
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_553_i0 line 176
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_553_i0 line 177
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_553_i0 line 178
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_553_i0 line 179
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_553_i0 line 180
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_553_i0 line 187
  91. def OAI.SnakyPrototype.Certificate21.required_553 line 192
  92. def OAI.SnakyPrototype.Certificate21.envelope_553 line 193
  93. def OAI.SnakyPrototype.Certificate21.childrenC_553 line 194
  94. def OAI.SnakyPrototype.Certificate21.childrenD_553 line 195
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_553 line 196
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_553 line 197
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_553 line 198
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_553 line 199
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_553 line 200
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_553 line 208
  101. def OAI.SnakyPrototype.Certificate21.required_557_i0 line 213
  102. def OAI.SnakyPrototype.Certificate21.envelope_557_i0 line 214
  103. def OAI.SnakyPrototype.Certificate21.childrenC_557_i0 line 215
  104. def OAI.SnakyPrototype.Certificate21.childrenD_557_i0 line 216
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_557_i0 line 217
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_557_i0 line 218
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_557_i0 line 219
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_557_i0 line 220
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_557_i0 line 221
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_557_i0 line 227
  111. def OAI.SnakyPrototype.Certificate21.required_557_i4 line 232
  112. def OAI.SnakyPrototype.Certificate21.envelope_557_i4 line 233
  113. def OAI.SnakyPrototype.Certificate21.childrenC_557_i4 line 234
  114. def OAI.SnakyPrototype.Certificate21.childrenD_557_i4 line 235
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_557_i4 line 236
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_557_i4 line 237
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_557_i4 line 238
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_557_i4 line 239
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_557_i4 line 240
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_557_i4 line 245
  121. def OAI.SnakyPrototype.Certificate21.required_557_i6 line 250
  122. def OAI.SnakyPrototype.Certificate21.envelope_557_i6 line 251
  123. def OAI.SnakyPrototype.Certificate21.childrenC_557_i6 line 252
  124. def OAI.SnakyPrototype.Certificate21.childrenD_557_i6 line 253
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_557_i6 line 254
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_557_i6 line 255
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_557_i6 line 256
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_557_i6 line 257
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_557_i6 line 258
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_557_i6 line 263
  131. def OAI.SnakyPrototype.Certificate21.required_557_i5 line 268
  132. def OAI.SnakyPrototype.Certificate21.envelope_557_i5 line 269
  133. def OAI.SnakyPrototype.Certificate21.childrenC_557_i5 line 270
  134. def OAI.SnakyPrototype.Certificate21.childrenD_557_i5 line 271
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_557_i5 line 272
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_557_i5 line 273
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_557_i5 line 274
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_557_i5 line 275
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_557_i5 line 276
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_557_i5 line 282
  141. def OAI.SnakyPrototype.Certificate21.required_557_i3 line 287
  142. def OAI.SnakyPrototype.Certificate21.envelope_557_i3 line 288
  143. def OAI.SnakyPrototype.Certificate21.childrenC_557_i3 line 289
  144. def OAI.SnakyPrototype.Certificate21.childrenD_557_i3 line 290
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_557_i3 line 291
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_557_i3 line 292
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_557_i3 line 293
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_557_i3 line 294
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_557_i3 line 295
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_557_i3 line 300
  151. def OAI.SnakyPrototype.Certificate21.required_557_i2 line 305
  152. def OAI.SnakyPrototype.Certificate21.envelope_557_i2 line 306
  153. def OAI.SnakyPrototype.Certificate21.childrenC_557_i2 line 307
  154. def OAI.SnakyPrototype.Certificate21.childrenD_557_i2 line 308
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_557_i2 line 309
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_557_i2 line 310
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_557_i2 line 311
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_557_i2 line 312
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_557_i2 line 313
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_557_i2 line 319
  161. def OAI.SnakyPrototype.Certificate21.required_557_i1 line 324
  162. def OAI.SnakyPrototype.Certificate21.envelope_557_i1 line 325
  163. def OAI.SnakyPrototype.Certificate21.childrenC_557_i1 line 326
  164. def OAI.SnakyPrototype.Certificate21.childrenD_557_i1 line 327
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_557_i1 line 328
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_557_i1 line 329
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_557_i1 line 330
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_557_i1 line 331
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_557_i1 line 332
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_557_i1 line 337
  171. def OAI.SnakyPrototype.Certificate21.required_557 line 342
  172. def OAI.SnakyPrototype.Certificate21.envelope_557 line 343
  173. def OAI.SnakyPrototype.Certificate21.childrenC_557 line 344
  174. def OAI.SnakyPrototype.Certificate21.childrenD_557 line 345
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_557 line 346
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_557 line 347
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_557 line 348
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_557 line 349
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_557 line 350
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_557 line 360
  181. def OAI.SnakyPrototype.Certificate21.required_582_i1 line 365
  182. def OAI.SnakyPrototype.Certificate21.envelope_582_i1 line 366
  183. def OAI.SnakyPrototype.Certificate21.childrenC_582_i1 line 367
  184. def OAI.SnakyPrototype.Certificate21.childrenD_582_i1 line 368
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_582_i1 line 369
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_582_i1 line 370
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_582_i1 line 371
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_582_i1 line 372
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_582_i1 line 373
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_582_i1 line 378
  191. def OAI.SnakyPrototype.Certificate21.required_582_i0 line 383
  192. def OAI.SnakyPrototype.Certificate21.envelope_582_i0 line 384
  193. def OAI.SnakyPrototype.Certificate21.childrenC_582_i0 line 385
  194. def OAI.SnakyPrototype.Certificate21.childrenD_582_i0 line 386
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_582_i0 line 387
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_582_i0 line 388
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_582_i0 line 389
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_582_i0 line 390
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_582_i0 line 391
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_582_i0 line 396
  201. def OAI.SnakyPrototype.Certificate21.required_582_i2 line 401
  202. def OAI.SnakyPrototype.Certificate21.envelope_582_i2 line 402
  203. def OAI.SnakyPrototype.Certificate21.childrenC_582_i2 line 403
  204. def OAI.SnakyPrototype.Certificate21.childrenD_582_i2 line 404
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_582_i2 line 405
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_582_i2 line 406
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_582_i2 line 407
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_582_i2 line 408
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_582_i2 line 409
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_582_i2 line 416
  211. def OAI.SnakyPrototype.Certificate21.required_582_i3 line 421
  212. def OAI.SnakyPrototype.Certificate21.envelope_582_i3 line 422
  213. def OAI.SnakyPrototype.Certificate21.childrenC_582_i3 line 423
  214. def OAI.SnakyPrototype.Certificate21.childrenD_582_i3 line 424
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_582_i3 line 425
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_582_i3 line 426
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_582_i3 line 427
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_582_i3 line 428
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_582_i3 line 429
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_582_i3 line 434
  221. def OAI.SnakyPrototype.Certificate21.required_582 line 439
  222. def OAI.SnakyPrototype.Certificate21.envelope_582 line 440
  223. def OAI.SnakyPrototype.Certificate21.childrenC_582 line 441
  224. def OAI.SnakyPrototype.Certificate21.childrenD_582 line 442
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_582 line 443
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_582 line 444
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_582 line 445
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_582 line 446
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_582 line 447
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_582 line 456
  231. def OAI.SnakyPrototype.Certificate21.height_553_i3 line 461
  232. def OAI.SnakyPrototype.Certificate21.childrenH_553_i3 line 462
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_553_i3 line 463
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_553_i3 line 464
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_553_i3 line 466
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_553_i3 line 470
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_553_i3 line 472
  238. def OAI.SnakyPrototype.Certificate21.checked_553_i3 line 476
  239. def OAI.SnakyPrototype.Certificate21.height_553_i2 line 484
  240. def OAI.SnakyPrototype.Certificate21.childrenH_553_i2 line 485
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_553_i2 line 486
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_553_i2 line 487
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_553_i2 line 489
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_553_i2 line 493
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_553_i2 line 495
  246. def OAI.SnakyPrototype.Certificate21.checked_553_i2 line 499
  247. def OAI.SnakyPrototype.Certificate21.height_553_i1 line 507
  248. def OAI.SnakyPrototype.Certificate21.childrenH_553_i1 line 508
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_553_i1 line 509
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_553_i1 line 510
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_553_i1 line 512
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_553_i1 line 516
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_553_i1 line 518
  254. def OAI.SnakyPrototype.Certificate21.checked_553_i1 line 522
  255. def OAI.SnakyPrototype.Certificate21.height_553_i6 line 530
  256. def OAI.SnakyPrototype.Certificate21.childrenH_553_i6 line 531
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_553_i6 line 532
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_553_i6 line 533
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_553_i6 line 535
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_553_i6 line 539
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_553_i6 line 541
  262. def OAI.SnakyPrototype.Certificate21.checked_553_i6 line 545
  263. def OAI.SnakyPrototype.Certificate21.height_553_i5 line 553
  264. def OAI.SnakyPrototype.Certificate21.childrenH_553_i5 line 554
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_553_i5 line 555
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_553_i5 line 556
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_553_i5 line 558
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_553_i5 line 562
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_553_i5 line 564
  270. def OAI.SnakyPrototype.Certificate21.checked_553_i5 line 568
  271. def OAI.SnakyPrototype.Certificate21.height_553_i4 line 576
  272. def OAI.SnakyPrototype.Certificate21.childrenH_553_i4 line 577
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_553_i4 line 578
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_553_i4 line 579
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_553_i4 line 581
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_553_i4 line 585
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_553_i4 line 587
  278. def OAI.SnakyPrototype.Certificate21.checked_553_i4 line 591
  279. def OAI.SnakyPrototype.Certificate21.height_553_i8 line 599
  280. def OAI.SnakyPrototype.Certificate21.childrenH_553_i8 line 600
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_553_i8 line 601
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_553_i8 line 602
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_553_i8 line 604
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_553_i8 line 608
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_553_i8 line 610
  286. def OAI.SnakyPrototype.Certificate21.checked_553_i8 line 614
  287. def OAI.SnakyPrototype.Certificate21.height_553_i7 line 622
  288. def OAI.SnakyPrototype.Certificate21.childrenH_553_i7 line 623
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_553_i7 line 624
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_553_i7 line 625
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_553_i7 line 627
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_553_i7 line 631
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_553_i7 line 633
  294. def OAI.SnakyPrototype.Certificate21.checked_553_i7 line 637
  295. def OAI.SnakyPrototype.Certificate21.height_553_i0 line 645
  296. def OAI.SnakyPrototype.Certificate21.childrenH_553_i0 line 646
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_553_i0 line 647
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_553_i0 line 648
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_553_i0 line 650
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_553_i0 line 654
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_553_i0 line 656
  302. def OAI.SnakyPrototype.Certificate21.checked_553_i0 line 660
  303. def OAI.SnakyPrototype.Certificate21.height_553 line 668
  304. def OAI.SnakyPrototype.Certificate21.childrenH_553 line 669
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_553 line 670
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_553 line 671
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_553 line 673
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_553 line 677
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_553 line 679
  310. def OAI.SnakyPrototype.Certificate21.checked_553 line 683
  311. def OAI.SnakyPrototype.Certificate21.height_557_i0 line 691
  312. def OAI.SnakyPrototype.Certificate21.childrenH_557_i0 line 692
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_557_i0 line 693
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_557_i0 line 694
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_557_i0 line 696
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_557_i0 line 700
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_557_i0 line 702
  318. def OAI.SnakyPrototype.Certificate21.checked_557_i0 line 706
  319. def OAI.SnakyPrototype.Certificate21.height_557_i4 line 714
  320. def OAI.SnakyPrototype.Certificate21.childrenH_557_i4 line 715
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_557_i4 line 716
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_557_i4 line 717
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_557_i4 line 719
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_557_i4 line 723
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_557_i4 line 725
  326. def OAI.SnakyPrototype.Certificate21.checked_557_i4 line 729
  327. def OAI.SnakyPrototype.Certificate21.height_557_i6 line 737
  328. def OAI.SnakyPrototype.Certificate21.childrenH_557_i6 line 738
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_557_i6 line 739
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_557_i6 line 740
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_557_i6 line 742
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_557_i6 line 746
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_557_i6 line 748
  334. def OAI.SnakyPrototype.Certificate21.checked_557_i6 line 752
  335. def OAI.SnakyPrototype.Certificate21.height_557_i5 line 760
  336. def OAI.SnakyPrototype.Certificate21.childrenH_557_i5 line 761
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_557_i5 line 762
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_557_i5 line 763
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_557_i5 line 765
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_557_i5 line 769
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_557_i5 line 771
  342. def OAI.SnakyPrototype.Certificate21.checked_557_i5 line 775
  343. def OAI.SnakyPrototype.Certificate21.height_557_i3 line 783
  344. def OAI.SnakyPrototype.Certificate21.childrenH_557_i3 line 784
  345. theorem OAI.SnakyPrototype.Certificate21.height_exact_557_i3 line 785
  346. theorem OAI.SnakyPrototype.Certificate21.required_origin_557_i3 line 786
  347. theorem OAI.SnakyPrototype.Certificate21.required_exact_557_i3 line 788
  348. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_557_i3 line 792
  349. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_557_i3 line 794
  350. def OAI.SnakyPrototype.Certificate21.checked_557_i3 line 798
  351. def OAI.SnakyPrototype.Certificate21.height_557_i2 line 806
  352. def OAI.SnakyPrototype.Certificate21.childrenH_557_i2 line 807
  353. theorem OAI.SnakyPrototype.Certificate21.height_exact_557_i2 line 808
  354. theorem OAI.SnakyPrototype.Certificate21.required_origin_557_i2 line 809
  355. theorem OAI.SnakyPrototype.Certificate21.required_exact_557_i2 line 811
  356. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_557_i2 line 815
  357. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_557_i2 line 817
  358. def OAI.SnakyPrototype.Certificate21.checked_557_i2 line 821
  359. def OAI.SnakyPrototype.Certificate21.height_557_i1 line 829
  360. def OAI.SnakyPrototype.Certificate21.childrenH_557_i1 line 830
  361. theorem OAI.SnakyPrototype.Certificate21.height_exact_557_i1 line 831
  362. theorem OAI.SnakyPrototype.Certificate21.required_origin_557_i1 line 832
  363. theorem OAI.SnakyPrototype.Certificate21.required_exact_557_i1 line 834
  364. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_557_i1 line 838
  365. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_557_i1 line 840
  366. def OAI.SnakyPrototype.Certificate21.checked_557_i1 line 844
  367. def OAI.SnakyPrototype.Certificate21.height_557 line 852
  368. def OAI.SnakyPrototype.Certificate21.childrenH_557 line 853
  369. theorem OAI.SnakyPrototype.Certificate21.height_exact_557 line 854
  370. theorem OAI.SnakyPrototype.Certificate21.required_origin_557 line 855
  371. theorem OAI.SnakyPrototype.Certificate21.required_exact_557 line 857
  372. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_557 line 861
  373. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_557 line 863
  374. def OAI.SnakyPrototype.Certificate21.checked_557 line 867
  375. def OAI.SnakyPrototype.Certificate21.height_582_i1 line 875
  376. def OAI.SnakyPrototype.Certificate21.childrenH_582_i1 line 876
  377. theorem OAI.SnakyPrototype.Certificate21.height_exact_582_i1 line 877
  378. theorem OAI.SnakyPrototype.Certificate21.required_origin_582_i1 line 878
  379. theorem OAI.SnakyPrototype.Certificate21.required_exact_582_i1 line 880
  380. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_582_i1 line 884
  381. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_582_i1 line 886
  382. def OAI.SnakyPrototype.Certificate21.checked_582_i1 line 890
  383. def OAI.SnakyPrototype.Certificate21.height_582_i0 line 898
  384. def OAI.SnakyPrototype.Certificate21.childrenH_582_i0 line 899
  385. theorem OAI.SnakyPrototype.Certificate21.height_exact_582_i0 line 900
  386. theorem OAI.SnakyPrototype.Certificate21.required_origin_582_i0 line 901
  387. theorem OAI.SnakyPrototype.Certificate21.required_exact_582_i0 line 903
  388. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_582_i0 line 907
  389. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_582_i0 line 909
  390. def OAI.SnakyPrototype.Certificate21.checked_582_i0 line 913
  391. def OAI.SnakyPrototype.Certificate21.height_582_i2 line 921
  392. def OAI.SnakyPrototype.Certificate21.childrenH_582_i2 line 922
  393. theorem OAI.SnakyPrototype.Certificate21.height_exact_582_i2 line 923
  394. theorem OAI.SnakyPrototype.Certificate21.required_origin_582_i2 line 924
  395. theorem OAI.SnakyPrototype.Certificate21.required_exact_582_i2 line 926
  396. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_582_i2 line 930
  397. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_582_i2 line 932
  398. def OAI.SnakyPrototype.Certificate21.checked_582_i2 line 936
  399. def OAI.SnakyPrototype.Certificate21.height_582_i3 line 944
  400. def OAI.SnakyPrototype.Certificate21.childrenH_582_i3 line 945
  401. theorem OAI.SnakyPrototype.Certificate21.height_exact_582_i3 line 946
  402. theorem OAI.SnakyPrototype.Certificate21.required_origin_582_i3 line 947
  403. theorem OAI.SnakyPrototype.Certificate21.required_exact_582_i3 line 949
  404. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_582_i3 line 953
  405. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_582_i3 line 955
  406. def OAI.SnakyPrototype.Certificate21.checked_582_i3 line 959
  407. def OAI.SnakyPrototype.Certificate21.height_582 line 967
  408. def OAI.SnakyPrototype.Certificate21.childrenH_582 line 968
  409. theorem OAI.SnakyPrototype.Certificate21.height_exact_582 line 969
  410. theorem OAI.SnakyPrototype.Certificate21.required_origin_582 line 970
  411. theorem OAI.SnakyPrototype.Certificate21.required_exact_582 line 972
  412. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_582 line 976
  413. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_582 line 978
  414. def OAI.SnakyPrototype.Certificate21.checked_582 line 982