OAI/GameTheory/SnakyTwentyOne/Cards/Height07Part04.lean

GitHub source file

432 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_511_i1 line 19
  2. def OAI.SnakyPrototype.Certificate21.envelope_511_i1 line 20
  3. def OAI.SnakyPrototype.Certificate21.childrenC_511_i1 line 21
  4. def OAI.SnakyPrototype.Certificate21.childrenD_511_i1 line 22
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_511_i1 line 23
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_511_i1 line 24
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_511_i1 line 25
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_511_i1 line 26
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_511_i1 line 27
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_511_i1 line 32
  11. def OAI.SnakyPrototype.Certificate21.required_511_i3 line 37
  12. def OAI.SnakyPrototype.Certificate21.envelope_511_i3 line 38
  13. def OAI.SnakyPrototype.Certificate21.childrenC_511_i3 line 39
  14. def OAI.SnakyPrototype.Certificate21.childrenD_511_i3 line 40
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_511_i3 line 41
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_511_i3 line 42
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_511_i3 line 43
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_511_i3 line 44
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_511_i3 line 45
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_511_i3 line 51
  21. def OAI.SnakyPrototype.Certificate21.required_511_i2 line 56
  22. def OAI.SnakyPrototype.Certificate21.envelope_511_i2 line 57
  23. def OAI.SnakyPrototype.Certificate21.childrenC_511_i2 line 58
  24. def OAI.SnakyPrototype.Certificate21.childrenD_511_i2 line 59
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_511_i2 line 60
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_511_i2 line 61
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_511_i2 line 62
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_511_i2 line 63
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_511_i2 line 64
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_511_i2 line 69
  31. def OAI.SnakyPrototype.Certificate21.required_511_i0 line 74
  32. def OAI.SnakyPrototype.Certificate21.envelope_511_i0 line 75
  33. def OAI.SnakyPrototype.Certificate21.childrenC_511_i0 line 76
  34. def OAI.SnakyPrototype.Certificate21.childrenD_511_i0 line 77
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_511_i0 line 78
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_511_i0 line 79
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_511_i0 line 80
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_511_i0 line 81
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_511_i0 line 82
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_511_i0 line 90
  41. def OAI.SnakyPrototype.Certificate21.required_511 line 95
  42. def OAI.SnakyPrototype.Certificate21.envelope_511 line 96
  43. def OAI.SnakyPrototype.Certificate21.childrenC_511 line 97
  44. def OAI.SnakyPrototype.Certificate21.childrenD_511 line 98
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_511 line 99
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_511 line 100
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_511 line 101
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_511 line 102
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_511 line 103
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_511 line 108
  51. def OAI.SnakyPrototype.Certificate21.required_522_i0 line 113
  52. def OAI.SnakyPrototype.Certificate21.envelope_522_i0 line 114
  53. def OAI.SnakyPrototype.Certificate21.childrenC_522_i0 line 115
  54. def OAI.SnakyPrototype.Certificate21.childrenD_522_i0 line 116
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_522_i0 line 117
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_522_i0 line 118
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_522_i0 line 119
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_522_i0 line 120
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_522_i0 line 121
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_522_i0 line 126
  61. def OAI.SnakyPrototype.Certificate21.required_522 line 131
  62. def OAI.SnakyPrototype.Certificate21.envelope_522 line 132
  63. def OAI.SnakyPrototype.Certificate21.childrenC_522 line 133
  64. def OAI.SnakyPrototype.Certificate21.childrenD_522 line 134
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_522 line 135
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_522 line 136
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_522 line 137
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_522 line 138
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_522 line 139
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_522 line 145
  71. def OAI.SnakyPrototype.Certificate21.required_526 line 150
  72. def OAI.SnakyPrototype.Certificate21.envelope_526 line 151
  73. def OAI.SnakyPrototype.Certificate21.childrenC_526 line 152
  74. def OAI.SnakyPrototype.Certificate21.childrenD_526 line 153
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_526 line 154
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_526 line 155
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_526 line 156
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_526 line 157
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_526 line 158
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_526 line 163
  81. def OAI.SnakyPrototype.Certificate21.required_542_i3 line 168
  82. def OAI.SnakyPrototype.Certificate21.envelope_542_i3 line 169
  83. def OAI.SnakyPrototype.Certificate21.childrenC_542_i3 line 170
  84. def OAI.SnakyPrototype.Certificate21.childrenD_542_i3 line 171
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_542_i3 line 172
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_542_i3 line 173
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_542_i3 line 174
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_542_i3 line 175
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_542_i3 line 176
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_542_i3 line 181
  91. def OAI.SnakyPrototype.Certificate21.required_542_i2 line 186
  92. def OAI.SnakyPrototype.Certificate21.envelope_542_i2 line 187
  93. def OAI.SnakyPrototype.Certificate21.childrenC_542_i2 line 188
  94. def OAI.SnakyPrototype.Certificate21.childrenD_542_i2 line 189
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_542_i2 line 190
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_542_i2 line 191
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_542_i2 line 192
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_542_i2 line 193
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_542_i2 line 194
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_542_i2 line 199
  101. def OAI.SnakyPrototype.Certificate21.required_542_i1 line 204
  102. def OAI.SnakyPrototype.Certificate21.envelope_542_i1 line 205
  103. def OAI.SnakyPrototype.Certificate21.childrenC_542_i1 line 206
  104. def OAI.SnakyPrototype.Certificate21.childrenD_542_i1 line 207
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_542_i1 line 208
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_542_i1 line 209
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_542_i1 line 210
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_542_i1 line 211
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_542_i1 line 212
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_542_i1 line 217
  111. def OAI.SnakyPrototype.Certificate21.required_542_i0 line 222
  112. def OAI.SnakyPrototype.Certificate21.envelope_542_i0 line 223
  113. def OAI.SnakyPrototype.Certificate21.childrenC_542_i0 line 224
  114. def OAI.SnakyPrototype.Certificate21.childrenD_542_i0 line 225
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_542_i0 line 226
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_542_i0 line 227
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_542_i0 line 228
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_542_i0 line 229
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_542_i0 line 230
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_542_i0 line 235
  121. def OAI.SnakyPrototype.Certificate21.required_542 line 240
  122. def OAI.SnakyPrototype.Certificate21.envelope_542 line 241
  123. def OAI.SnakyPrototype.Certificate21.childrenC_542 line 242
  124. def OAI.SnakyPrototype.Certificate21.childrenD_542 line 243
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_542 line 244
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_542 line 245
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_542 line 246
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_542 line 247
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_542 line 248
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_542 line 253
  131. def OAI.SnakyPrototype.Certificate21.required_554_i0 line 258
  132. def OAI.SnakyPrototype.Certificate21.envelope_554_i0 line 259
  133. def OAI.SnakyPrototype.Certificate21.childrenC_554_i0 line 260
  134. def OAI.SnakyPrototype.Certificate21.childrenD_554_i0 line 261
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_554_i0 line 262
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_554_i0 line 263
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_554_i0 line 264
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_554_i0 line 265
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_554_i0 line 266
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_554_i0 line 271
  141. def OAI.SnakyPrototype.Certificate21.required_554 line 276
  142. def OAI.SnakyPrototype.Certificate21.envelope_554 line 277
  143. def OAI.SnakyPrototype.Certificate21.childrenC_554 line 278
  144. def OAI.SnakyPrototype.Certificate21.childrenD_554 line 279
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_554 line 280
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_554 line 281
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_554 line 282
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_554 line 283
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_554 line 284
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_554 line 289
  151. def OAI.SnakyPrototype.Certificate21.required_565_i0 line 294
  152. def OAI.SnakyPrototype.Certificate21.envelope_565_i0 line 295
  153. def OAI.SnakyPrototype.Certificate21.childrenC_565_i0 line 296
  154. def OAI.SnakyPrototype.Certificate21.childrenD_565_i0 line 297
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_565_i0 line 298
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_565_i0 line 299
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_565_i0 line 300
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_565_i0 line 301
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_565_i0 line 302
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_565_i0 line 307
  161. def OAI.SnakyPrototype.Certificate21.required_565_i1 line 312
  162. def OAI.SnakyPrototype.Certificate21.envelope_565_i1 line 313
  163. def OAI.SnakyPrototype.Certificate21.childrenC_565_i1 line 314
  164. def OAI.SnakyPrototype.Certificate21.childrenD_565_i1 line 315
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_565_i1 line 316
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_565_i1 line 317
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_565_i1 line 318
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_565_i1 line 319
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_565_i1 line 320
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_565_i1 line 325
  171. def OAI.SnakyPrototype.Certificate21.required_565 line 330
  172. def OAI.SnakyPrototype.Certificate21.envelope_565 line 331
  173. def OAI.SnakyPrototype.Certificate21.childrenC_565 line 332
  174. def OAI.SnakyPrototype.Certificate21.childrenD_565 line 333
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_565 line 334
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_565 line 335
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_565 line 336
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_565 line 337
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_565 line 338
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_565 line 344
  181. def OAI.SnakyPrototype.Certificate21.required_576_i2 line 349
  182. def OAI.SnakyPrototype.Certificate21.envelope_576_i2 line 350
  183. def OAI.SnakyPrototype.Certificate21.childrenC_576_i2 line 351
  184. def OAI.SnakyPrototype.Certificate21.childrenD_576_i2 line 352
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_576_i2 line 353
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_576_i2 line 354
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_576_i2 line 355
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_576_i2 line 356
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_576_i2 line 357
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_576_i2 line 362
  191. def OAI.SnakyPrototype.Certificate21.required_576_i3 line 367
  192. def OAI.SnakyPrototype.Certificate21.envelope_576_i3 line 368
  193. def OAI.SnakyPrototype.Certificate21.childrenC_576_i3 line 369
  194. def OAI.SnakyPrototype.Certificate21.childrenD_576_i3 line 370
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_576_i3 line 371
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_576_i3 line 372
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_576_i3 line 373
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_576_i3 line 374
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_576_i3 line 375
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_576_i3 line 380
  201. def OAI.SnakyPrototype.Certificate21.required_576_i1 line 385
  202. def OAI.SnakyPrototype.Certificate21.envelope_576_i1 line 386
  203. def OAI.SnakyPrototype.Certificate21.childrenC_576_i1 line 387
  204. def OAI.SnakyPrototype.Certificate21.childrenD_576_i1 line 388
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_576_i1 line 389
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_576_i1 line 390
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_576_i1 line 391
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_576_i1 line 392
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_576_i1 line 393
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_576_i1 line 398
  211. def OAI.SnakyPrototype.Certificate21.required_576_i4 line 403
  212. def OAI.SnakyPrototype.Certificate21.envelope_576_i4 line 404
  213. def OAI.SnakyPrototype.Certificate21.childrenC_576_i4 line 405
  214. def OAI.SnakyPrototype.Certificate21.childrenD_576_i4 line 406
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_576_i4 line 407
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_576_i4 line 408
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_576_i4 line 409
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_576_i4 line 410
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_576_i4 line 411
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_576_i4 line 416
  221. def OAI.SnakyPrototype.Certificate21.required_576_i0 line 421
  222. def OAI.SnakyPrototype.Certificate21.envelope_576_i0 line 422
  223. def OAI.SnakyPrototype.Certificate21.childrenC_576_i0 line 423
  224. def OAI.SnakyPrototype.Certificate21.childrenD_576_i0 line 424
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_576_i0 line 425
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_576_i0 line 426
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_576_i0 line 427
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_576_i0 line 428
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_576_i0 line 429
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_576_i0 line 436
  231. def OAI.SnakyPrototype.Certificate21.required_576 line 441
  232. def OAI.SnakyPrototype.Certificate21.envelope_576 line 442
  233. def OAI.SnakyPrototype.Certificate21.childrenC_576 line 443
  234. def OAI.SnakyPrototype.Certificate21.childrenD_576 line 444
  235. theorem OAI.SnakyPrototype.Certificate21.common_sub_576 line 445
  236. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_576 line 446
  237. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_576 line 447
  238. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_576 line 448
  239. theorem OAI.SnakyPrototype.Certificate21.children_work_576 line 449
  240. theorem OAI.SnakyPrototype.Certificate21.row_works_576 line 454
  241. def OAI.SnakyPrototype.Certificate21.height_511_i1 line 459
  242. def OAI.SnakyPrototype.Certificate21.childrenH_511_i1 line 460
  243. theorem OAI.SnakyPrototype.Certificate21.height_exact_511_i1 line 461
  244. theorem OAI.SnakyPrototype.Certificate21.required_origin_511_i1 line 462
  245. theorem OAI.SnakyPrototype.Certificate21.required_exact_511_i1 line 464
  246. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_511_i1 line 468
  247. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_511_i1 line 470
  248. def OAI.SnakyPrototype.Certificate21.checked_511_i1 line 474
  249. def OAI.SnakyPrototype.Certificate21.height_511_i3 line 482
  250. def OAI.SnakyPrototype.Certificate21.childrenH_511_i3 line 483
  251. theorem OAI.SnakyPrototype.Certificate21.height_exact_511_i3 line 484
  252. theorem OAI.SnakyPrototype.Certificate21.required_origin_511_i3 line 485
  253. theorem OAI.SnakyPrototype.Certificate21.required_exact_511_i3 line 487
  254. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_511_i3 line 491
  255. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_511_i3 line 493
  256. def OAI.SnakyPrototype.Certificate21.checked_511_i3 line 497
  257. def OAI.SnakyPrototype.Certificate21.height_511_i2 line 505
  258. def OAI.SnakyPrototype.Certificate21.childrenH_511_i2 line 506
  259. theorem OAI.SnakyPrototype.Certificate21.height_exact_511_i2 line 507
  260. theorem OAI.SnakyPrototype.Certificate21.required_origin_511_i2 line 508
  261. theorem OAI.SnakyPrototype.Certificate21.required_exact_511_i2 line 510
  262. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_511_i2 line 514
  263. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_511_i2 line 516
  264. def OAI.SnakyPrototype.Certificate21.checked_511_i2 line 520
  265. def OAI.SnakyPrototype.Certificate21.height_511_i0 line 528
  266. def OAI.SnakyPrototype.Certificate21.childrenH_511_i0 line 529
  267. theorem OAI.SnakyPrototype.Certificate21.height_exact_511_i0 line 530
  268. theorem OAI.SnakyPrototype.Certificate21.required_origin_511_i0 line 531
  269. theorem OAI.SnakyPrototype.Certificate21.required_exact_511_i0 line 533
  270. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_511_i0 line 537
  271. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_511_i0 line 539
  272. def OAI.SnakyPrototype.Certificate21.checked_511_i0 line 543
  273. def OAI.SnakyPrototype.Certificate21.height_511 line 551
  274. def OAI.SnakyPrototype.Certificate21.childrenH_511 line 552
  275. theorem OAI.SnakyPrototype.Certificate21.height_exact_511 line 553
  276. theorem OAI.SnakyPrototype.Certificate21.required_origin_511 line 554
  277. theorem OAI.SnakyPrototype.Certificate21.required_exact_511 line 556
  278. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_511 line 560
  279. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_511 line 562
  280. def OAI.SnakyPrototype.Certificate21.checked_511 line 566
  281. def OAI.SnakyPrototype.Certificate21.height_522_i0 line 574
  282. def OAI.SnakyPrototype.Certificate21.childrenH_522_i0 line 575
  283. theorem OAI.SnakyPrototype.Certificate21.height_exact_522_i0 line 576
  284. theorem OAI.SnakyPrototype.Certificate21.required_origin_522_i0 line 577
  285. theorem OAI.SnakyPrototype.Certificate21.required_exact_522_i0 line 579
  286. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_522_i0 line 583
  287. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_522_i0 line 585
  288. def OAI.SnakyPrototype.Certificate21.checked_522_i0 line 589
  289. def OAI.SnakyPrototype.Certificate21.height_522 line 597
  290. def OAI.SnakyPrototype.Certificate21.childrenH_522 line 598
  291. theorem OAI.SnakyPrototype.Certificate21.height_exact_522 line 599
  292. theorem OAI.SnakyPrototype.Certificate21.required_origin_522 line 600
  293. theorem OAI.SnakyPrototype.Certificate21.required_exact_522 line 602
  294. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_522 line 606
  295. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_522 line 608
  296. def OAI.SnakyPrototype.Certificate21.checked_522 line 612
  297. def OAI.SnakyPrototype.Certificate21.height_526 line 620
  298. def OAI.SnakyPrototype.Certificate21.childrenH_526 line 621
  299. theorem OAI.SnakyPrototype.Certificate21.height_exact_526 line 622
  300. theorem OAI.SnakyPrototype.Certificate21.required_origin_526 line 623
  301. theorem OAI.SnakyPrototype.Certificate21.required_exact_526 line 625
  302. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_526 line 629
  303. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_526 line 631
  304. def OAI.SnakyPrototype.Certificate21.checked_526 line 635
  305. def OAI.SnakyPrototype.Certificate21.height_542_i3 line 643
  306. def OAI.SnakyPrototype.Certificate21.childrenH_542_i3 line 644
  307. theorem OAI.SnakyPrototype.Certificate21.height_exact_542_i3 line 645
  308. theorem OAI.SnakyPrototype.Certificate21.required_origin_542_i3 line 646
  309. theorem OAI.SnakyPrototype.Certificate21.required_exact_542_i3 line 648
  310. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_542_i3 line 652
  311. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_542_i3 line 654
  312. def OAI.SnakyPrototype.Certificate21.checked_542_i3 line 658
  313. def OAI.SnakyPrototype.Certificate21.height_542_i2 line 666
  314. def OAI.SnakyPrototype.Certificate21.childrenH_542_i2 line 667
  315. theorem OAI.SnakyPrototype.Certificate21.height_exact_542_i2 line 668
  316. theorem OAI.SnakyPrototype.Certificate21.required_origin_542_i2 line 669
  317. theorem OAI.SnakyPrototype.Certificate21.required_exact_542_i2 line 671
  318. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_542_i2 line 675
  319. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_542_i2 line 677
  320. def OAI.SnakyPrototype.Certificate21.checked_542_i2 line 681
  321. def OAI.SnakyPrototype.Certificate21.height_542_i1 line 689
  322. def OAI.SnakyPrototype.Certificate21.childrenH_542_i1 line 690
  323. theorem OAI.SnakyPrototype.Certificate21.height_exact_542_i1 line 691
  324. theorem OAI.SnakyPrototype.Certificate21.required_origin_542_i1 line 692
  325. theorem OAI.SnakyPrototype.Certificate21.required_exact_542_i1 line 694
  326. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_542_i1 line 698
  327. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_542_i1 line 700
  328. def OAI.SnakyPrototype.Certificate21.checked_542_i1 line 704
  329. def OAI.SnakyPrototype.Certificate21.height_542_i0 line 712
  330. def OAI.SnakyPrototype.Certificate21.childrenH_542_i0 line 713
  331. theorem OAI.SnakyPrototype.Certificate21.height_exact_542_i0 line 714
  332. theorem OAI.SnakyPrototype.Certificate21.required_origin_542_i0 line 715
  333. theorem OAI.SnakyPrototype.Certificate21.required_exact_542_i0 line 717
  334. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_542_i0 line 721
  335. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_542_i0 line 723
  336. def OAI.SnakyPrototype.Certificate21.checked_542_i0 line 727
  337. def OAI.SnakyPrototype.Certificate21.height_542 line 735
  338. def OAI.SnakyPrototype.Certificate21.childrenH_542 line 736
  339. theorem OAI.SnakyPrototype.Certificate21.height_exact_542 line 737
  340. theorem OAI.SnakyPrototype.Certificate21.required_origin_542 line 738
  341. theorem OAI.SnakyPrototype.Certificate21.required_exact_542 line 740
  342. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_542 line 744
  343. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_542 line 746
  344. def OAI.SnakyPrototype.Certificate21.checked_542 line 750
  345. def OAI.SnakyPrototype.Certificate21.height_554_i0 line 758
  346. def OAI.SnakyPrototype.Certificate21.childrenH_554_i0 line 759
  347. theorem OAI.SnakyPrototype.Certificate21.height_exact_554_i0 line 760
  348. theorem OAI.SnakyPrototype.Certificate21.required_origin_554_i0 line 761
  349. theorem OAI.SnakyPrototype.Certificate21.required_exact_554_i0 line 763
  350. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_554_i0 line 767
  351. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_554_i0 line 769
  352. def OAI.SnakyPrototype.Certificate21.checked_554_i0 line 773
  353. def OAI.SnakyPrototype.Certificate21.height_554 line 781
  354. def OAI.SnakyPrototype.Certificate21.childrenH_554 line 782
  355. theorem OAI.SnakyPrototype.Certificate21.height_exact_554 line 783
  356. theorem OAI.SnakyPrototype.Certificate21.required_origin_554 line 784
  357. theorem OAI.SnakyPrototype.Certificate21.required_exact_554 line 786
  358. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_554 line 790
  359. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_554 line 792
  360. def OAI.SnakyPrototype.Certificate21.checked_554 line 796
  361. def OAI.SnakyPrototype.Certificate21.height_565_i0 line 804
  362. def OAI.SnakyPrototype.Certificate21.childrenH_565_i0 line 805
  363. theorem OAI.SnakyPrototype.Certificate21.height_exact_565_i0 line 806
  364. theorem OAI.SnakyPrototype.Certificate21.required_origin_565_i0 line 807
  365. theorem OAI.SnakyPrototype.Certificate21.required_exact_565_i0 line 809
  366. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_565_i0 line 813
  367. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_565_i0 line 815
  368. def OAI.SnakyPrototype.Certificate21.checked_565_i0 line 819
  369. def OAI.SnakyPrototype.Certificate21.height_565_i1 line 827
  370. def OAI.SnakyPrototype.Certificate21.childrenH_565_i1 line 828
  371. theorem OAI.SnakyPrototype.Certificate21.height_exact_565_i1 line 829
  372. theorem OAI.SnakyPrototype.Certificate21.required_origin_565_i1 line 830
  373. theorem OAI.SnakyPrototype.Certificate21.required_exact_565_i1 line 832
  374. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_565_i1 line 836
  375. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_565_i1 line 838
  376. def OAI.SnakyPrototype.Certificate21.checked_565_i1 line 842
  377. def OAI.SnakyPrototype.Certificate21.height_565 line 850
  378. def OAI.SnakyPrototype.Certificate21.childrenH_565 line 851
  379. theorem OAI.SnakyPrototype.Certificate21.height_exact_565 line 852
  380. theorem OAI.SnakyPrototype.Certificate21.required_origin_565 line 853
  381. theorem OAI.SnakyPrototype.Certificate21.required_exact_565 line 855
  382. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_565 line 859
  383. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_565 line 861
  384. def OAI.SnakyPrototype.Certificate21.checked_565 line 865
  385. def OAI.SnakyPrototype.Certificate21.height_576_i2 line 873
  386. def OAI.SnakyPrototype.Certificate21.childrenH_576_i2 line 874
  387. theorem OAI.SnakyPrototype.Certificate21.height_exact_576_i2 line 875
  388. theorem OAI.SnakyPrototype.Certificate21.required_origin_576_i2 line 876
  389. theorem OAI.SnakyPrototype.Certificate21.required_exact_576_i2 line 878
  390. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_576_i2 line 882
  391. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_576_i2 line 884
  392. def OAI.SnakyPrototype.Certificate21.checked_576_i2 line 888
  393. def OAI.SnakyPrototype.Certificate21.height_576_i3 line 896
  394. def OAI.SnakyPrototype.Certificate21.childrenH_576_i3 line 897
  395. theorem OAI.SnakyPrototype.Certificate21.height_exact_576_i3 line 898
  396. theorem OAI.SnakyPrototype.Certificate21.required_origin_576_i3 line 899
  397. theorem OAI.SnakyPrototype.Certificate21.required_exact_576_i3 line 901
  398. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_576_i3 line 905
  399. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_576_i3 line 907
  400. def OAI.SnakyPrototype.Certificate21.checked_576_i3 line 911
  401. def OAI.SnakyPrototype.Certificate21.height_576_i1 line 919
  402. def OAI.SnakyPrototype.Certificate21.childrenH_576_i1 line 920
  403. theorem OAI.SnakyPrototype.Certificate21.height_exact_576_i1 line 921
  404. theorem OAI.SnakyPrototype.Certificate21.required_origin_576_i1 line 922
  405. theorem OAI.SnakyPrototype.Certificate21.required_exact_576_i1 line 924
  406. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_576_i1 line 928
  407. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_576_i1 line 930
  408. def OAI.SnakyPrototype.Certificate21.checked_576_i1 line 934
  409. def OAI.SnakyPrototype.Certificate21.height_576_i4 line 942
  410. def OAI.SnakyPrototype.Certificate21.childrenH_576_i4 line 943
  411. theorem OAI.SnakyPrototype.Certificate21.height_exact_576_i4 line 944
  412. theorem OAI.SnakyPrototype.Certificate21.required_origin_576_i4 line 945
  413. theorem OAI.SnakyPrototype.Certificate21.required_exact_576_i4 line 947
  414. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_576_i4 line 951
  415. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_576_i4 line 953
  416. def OAI.SnakyPrototype.Certificate21.checked_576_i4 line 957
  417. def OAI.SnakyPrototype.Certificate21.height_576_i0 line 965
  418. def OAI.SnakyPrototype.Certificate21.childrenH_576_i0 line 966
  419. theorem OAI.SnakyPrototype.Certificate21.height_exact_576_i0 line 967
  420. theorem OAI.SnakyPrototype.Certificate21.required_origin_576_i0 line 968
  421. theorem OAI.SnakyPrototype.Certificate21.required_exact_576_i0 line 970
  422. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_576_i0 line 974
  423. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_576_i0 line 976
  424. def OAI.SnakyPrototype.Certificate21.checked_576_i0 line 980
  425. def OAI.SnakyPrototype.Certificate21.height_576 line 988
  426. def OAI.SnakyPrototype.Certificate21.childrenH_576 line 989
  427. theorem OAI.SnakyPrototype.Certificate21.height_exact_576 line 990
  428. theorem OAI.SnakyPrototype.Certificate21.required_origin_576 line 991
  429. theorem OAI.SnakyPrototype.Certificate21.required_exact_576 line 993
  430. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_576 line 997
  431. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_576 line 999
  432. def OAI.SnakyPrototype.Certificate21.checked_576 line 1003