OAI/GameTheory/SnakyTwentyOne/Cards/Height12Part03.lean

GitHub source file

396 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_599_i6 line 29
  2. def OAI.SnakyPrototype.Certificate21.envelope_599_i6 line 30
  3. def OAI.SnakyPrototype.Certificate21.childrenC_599_i6 line 31
  4. def OAI.SnakyPrototype.Certificate21.childrenD_599_i6 line 32
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_599_i6 line 33
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_599_i6 line 34
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_599_i6 line 35
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_599_i6 line 36
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_599_i6 line 37
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_599_i6 line 42
  11. def OAI.SnakyPrototype.Certificate21.required_599_i8 line 47
  12. def OAI.SnakyPrototype.Certificate21.envelope_599_i8 line 48
  13. def OAI.SnakyPrototype.Certificate21.childrenC_599_i8 line 49
  14. def OAI.SnakyPrototype.Certificate21.childrenD_599_i8 line 50
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_599_i8 line 51
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_599_i8 line 52
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_599_i8 line 53
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_599_i8 line 54
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_599_i8 line 55
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_599_i8 line 60
  21. def OAI.SnakyPrototype.Certificate21.required_599_i7 line 65
  22. def OAI.SnakyPrototype.Certificate21.envelope_599_i7 line 66
  23. def OAI.SnakyPrototype.Certificate21.childrenC_599_i7 line 67
  24. def OAI.SnakyPrototype.Certificate21.childrenD_599_i7 line 68
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_599_i7 line 69
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_599_i7 line 70
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_599_i7 line 71
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_599_i7 line 72
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_599_i7 line 73
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_599_i7 line 79
  31. def OAI.SnakyPrototype.Certificate21.required_599_i5 line 84
  32. def OAI.SnakyPrototype.Certificate21.envelope_599_i5 line 85
  33. def OAI.SnakyPrototype.Certificate21.childrenC_599_i5 line 86
  34. def OAI.SnakyPrototype.Certificate21.childrenD_599_i5 line 87
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_599_i5 line 88
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_599_i5 line 89
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_599_i5 line 90
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_599_i5 line 91
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_599_i5 line 92
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_599_i5 line 100
  41. def OAI.SnakyPrototype.Certificate21.required_599_i4 line 105
  42. def OAI.SnakyPrototype.Certificate21.envelope_599_i4 line 106
  43. def OAI.SnakyPrototype.Certificate21.childrenC_599_i4 line 107
  44. def OAI.SnakyPrototype.Certificate21.childrenD_599_i4 line 108
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_599_i4 line 109
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_599_i4 line 110
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_599_i4 line 111
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_599_i4 line 112
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_599_i4 line 113
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_599_i4 line 118
  51. def OAI.SnakyPrototype.Certificate21.required_599_i3 line 123
  52. def OAI.SnakyPrototype.Certificate21.envelope_599_i3 line 124
  53. def OAI.SnakyPrototype.Certificate21.childrenC_599_i3 line 125
  54. def OAI.SnakyPrototype.Certificate21.childrenD_599_i3 line 126
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_599_i3 line 127
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_599_i3 line 128
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_599_i3 line 129
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_599_i3 line 130
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_599_i3 line 131
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_599_i3 line 136
  61. def OAI.SnakyPrototype.Certificate21.required_599_i2 line 141
  62. def OAI.SnakyPrototype.Certificate21.envelope_599_i2 line 142
  63. def OAI.SnakyPrototype.Certificate21.childrenC_599_i2 line 143
  64. def OAI.SnakyPrototype.Certificate21.childrenD_599_i2 line 144
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_599_i2 line 145
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_599_i2 line 146
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_599_i2 line 147
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_599_i2 line 148
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_599_i2 line 149
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_599_i2 line 155
  71. def OAI.SnakyPrototype.Certificate21.required_599_i1 line 160
  72. def OAI.SnakyPrototype.Certificate21.envelope_599_i1 line 161
  73. def OAI.SnakyPrototype.Certificate21.childrenC_599_i1 line 162
  74. def OAI.SnakyPrototype.Certificate21.childrenD_599_i1 line 163
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_599_i1 line 164
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_599_i1 line 165
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_599_i1 line 166
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_599_i1 line 167
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_599_i1 line 168
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_599_i1 line 176
  81. def OAI.SnakyPrototype.Certificate21.required_599_i0 line 181
  82. def OAI.SnakyPrototype.Certificate21.envelope_599_i0 line 182
  83. def OAI.SnakyPrototype.Certificate21.childrenC_599_i0 line 183
  84. def OAI.SnakyPrototype.Certificate21.childrenD_599_i0 line 184
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_599_i0 line 185
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_599_i0 line 186
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_599_i0 line 187
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_599_i0 line 188
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_599_i0 line 189
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_599_i0 line 194
  91. def OAI.SnakyPrototype.Certificate21.required_599 line 199
  92. def OAI.SnakyPrototype.Certificate21.envelope_599 line 200
  93. def OAI.SnakyPrototype.Certificate21.childrenC_599 line 201
  94. def OAI.SnakyPrototype.Certificate21.childrenD_599 line 202
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_599 line 203
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_599 line 204
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_599 line 205
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_599 line 206
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_599 line 207
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_599 line 214
  101. def OAI.SnakyPrototype.Certificate21.required_605_i0 line 219
  102. def OAI.SnakyPrototype.Certificate21.envelope_605_i0 line 220
  103. def OAI.SnakyPrototype.Certificate21.childrenC_605_i0 line 221
  104. def OAI.SnakyPrototype.Certificate21.childrenD_605_i0 line 222
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_605_i0 line 223
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_605_i0 line 224
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_605_i0 line 225
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_605_i0 line 226
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_605_i0 line 227
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_605_i0 line 233
  111. def OAI.SnakyPrototype.Certificate21.required_605 line 238
  112. def OAI.SnakyPrototype.Certificate21.envelope_605 line 239
  113. def OAI.SnakyPrototype.Certificate21.childrenC_605 line 240
  114. def OAI.SnakyPrototype.Certificate21.childrenD_605 line 241
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_605 line 242
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_605 line 243
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_605 line 244
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_605 line 245
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_605 line 246
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_605 line 254
  121. def OAI.SnakyPrototype.Certificate21.required_618_i2 line 259
  122. def OAI.SnakyPrototype.Certificate21.envelope_618_i2 line 260
  123. def OAI.SnakyPrototype.Certificate21.childrenC_618_i2 line 261
  124. def OAI.SnakyPrototype.Certificate21.childrenD_618_i2 line 262
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_618_i2 line 263
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_618_i2 line 264
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_618_i2 line 265
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_618_i2 line 266
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_618_i2 line 267
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_618_i2 line 272
  131. def OAI.SnakyPrototype.Certificate21.required_618_i1 line 277
  132. def OAI.SnakyPrototype.Certificate21.envelope_618_i1 line 278
  133. def OAI.SnakyPrototype.Certificate21.childrenC_618_i1 line 279
  134. def OAI.SnakyPrototype.Certificate21.childrenD_618_i1 line 280
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_618_i1 line 281
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_618_i1 line 282
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_618_i1 line 283
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_618_i1 line 284
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_618_i1 line 285
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_618_i1 line 290
  141. def OAI.SnakyPrototype.Certificate21.required_618_i0 line 295
  142. def OAI.SnakyPrototype.Certificate21.envelope_618_i0 line 296
  143. def OAI.SnakyPrototype.Certificate21.childrenC_618_i0 line 297
  144. def OAI.SnakyPrototype.Certificate21.childrenD_618_i0 line 298
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_618_i0 line 299
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_618_i0 line 300
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_618_i0 line 301
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_618_i0 line 302
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_618_i0 line 303
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_618_i0 line 310
  151. def OAI.SnakyPrototype.Certificate21.required_618_i3 line 315
  152. def OAI.SnakyPrototype.Certificate21.envelope_618_i3 line 316
  153. def OAI.SnakyPrototype.Certificate21.childrenC_618_i3 line 317
  154. def OAI.SnakyPrototype.Certificate21.childrenD_618_i3 line 318
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_618_i3 line 319
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_618_i3 line 320
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_618_i3 line 321
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_618_i3 line 322
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_618_i3 line 323
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_618_i3 line 330
  161. def OAI.SnakyPrototype.Certificate21.required_618_i4 line 335
  162. def OAI.SnakyPrototype.Certificate21.envelope_618_i4 line 336
  163. def OAI.SnakyPrototype.Certificate21.childrenC_618_i4 line 337
  164. def OAI.SnakyPrototype.Certificate21.childrenD_618_i4 line 338
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_618_i4 line 339
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_618_i4 line 340
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_618_i4 line 341
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_618_i4 line 342
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_618_i4 line 343
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_618_i4 line 350
  171. def OAI.SnakyPrototype.Certificate21.required_618_i5 line 355
  172. def OAI.SnakyPrototype.Certificate21.envelope_618_i5 line 356
  173. def OAI.SnakyPrototype.Certificate21.childrenC_618_i5 line 357
  174. def OAI.SnakyPrototype.Certificate21.childrenD_618_i5 line 358
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_618_i5 line 359
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_618_i5 line 360
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_618_i5 line 361
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_618_i5 line 362
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_618_i5 line 363
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_618_i5 line 369
  181. def OAI.SnakyPrototype.Certificate21.required_618_i8 line 374
  182. def OAI.SnakyPrototype.Certificate21.envelope_618_i8 line 375
  183. def OAI.SnakyPrototype.Certificate21.childrenC_618_i8 line 376
  184. def OAI.SnakyPrototype.Certificate21.childrenD_618_i8 line 377
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_618_i8 line 378
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_618_i8 line 379
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_618_i8 line 380
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_618_i8 line 381
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_618_i8 line 382
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_618_i8 line 387
  191. def OAI.SnakyPrototype.Certificate21.required_618_i7 line 392
  192. def OAI.SnakyPrototype.Certificate21.envelope_618_i7 line 393
  193. def OAI.SnakyPrototype.Certificate21.childrenC_618_i7 line 394
  194. def OAI.SnakyPrototype.Certificate21.childrenD_618_i7 line 395
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_618_i7 line 396
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_618_i7 line 397
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_618_i7 line 398
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_618_i7 line 399
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_618_i7 line 400
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_618_i7 line 405
  201. def OAI.SnakyPrototype.Certificate21.required_618_i6 line 410
  202. def OAI.SnakyPrototype.Certificate21.envelope_618_i6 line 411
  203. def OAI.SnakyPrototype.Certificate21.childrenC_618_i6 line 412
  204. def OAI.SnakyPrototype.Certificate21.childrenD_618_i6 line 413
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_618_i6 line 414
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_618_i6 line 415
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_618_i6 line 416
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_618_i6 line 417
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_618_i6 line 418
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_618_i6 line 425
  211. def OAI.SnakyPrototype.Certificate21.required_618 line 430
  212. def OAI.SnakyPrototype.Certificate21.envelope_618 line 431
  213. def OAI.SnakyPrototype.Certificate21.childrenC_618 line 432
  214. def OAI.SnakyPrototype.Certificate21.childrenD_618 line 433
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_618 line 434
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_618 line 435
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_618 line 436
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_618 line 437
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_618 line 438
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_618 line 450
  221. def OAI.SnakyPrototype.Certificate21.height_599_i6 line 455
  222. def OAI.SnakyPrototype.Certificate21.childrenH_599_i6 line 456
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_599_i6 line 457
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_599_i6 line 458
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_599_i6 line 460
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_599_i6 line 464
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_599_i6 line 466
  228. def OAI.SnakyPrototype.Certificate21.checked_599_i6 line 470
  229. def OAI.SnakyPrototype.Certificate21.height_599_i8 line 478
  230. def OAI.SnakyPrototype.Certificate21.childrenH_599_i8 line 479
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_599_i8 line 480
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_599_i8 line 481
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_599_i8 line 483
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_599_i8 line 487
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_599_i8 line 489
  236. def OAI.SnakyPrototype.Certificate21.checked_599_i8 line 493
  237. def OAI.SnakyPrototype.Certificate21.height_599_i7 line 501
  238. def OAI.SnakyPrototype.Certificate21.childrenH_599_i7 line 502
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_599_i7 line 503
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_599_i7 line 504
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_599_i7 line 506
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_599_i7 line 510
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_599_i7 line 512
  244. def OAI.SnakyPrototype.Certificate21.checked_599_i7 line 516
  245. def OAI.SnakyPrototype.Certificate21.height_599_i5 line 524
  246. def OAI.SnakyPrototype.Certificate21.childrenH_599_i5 line 525
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_599_i5 line 526
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_599_i5 line 527
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_599_i5 line 529
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_599_i5 line 533
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_599_i5 line 535
  252. def OAI.SnakyPrototype.Certificate21.checked_599_i5 line 539
  253. def OAI.SnakyPrototype.Certificate21.height_599_i4 line 547
  254. def OAI.SnakyPrototype.Certificate21.childrenH_599_i4 line 548
  255. theorem OAI.SnakyPrototype.Certificate21.height_exact_599_i4 line 549
  256. theorem OAI.SnakyPrototype.Certificate21.required_origin_599_i4 line 550
  257. theorem OAI.SnakyPrototype.Certificate21.required_exact_599_i4 line 552
  258. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_599_i4 line 556
  259. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_599_i4 line 558
  260. def OAI.SnakyPrototype.Certificate21.checked_599_i4 line 562
  261. def OAI.SnakyPrototype.Certificate21.height_599_i3 line 570
  262. def OAI.SnakyPrototype.Certificate21.childrenH_599_i3 line 571
  263. theorem OAI.SnakyPrototype.Certificate21.height_exact_599_i3 line 572
  264. theorem OAI.SnakyPrototype.Certificate21.required_origin_599_i3 line 573
  265. theorem OAI.SnakyPrototype.Certificate21.required_exact_599_i3 line 575
  266. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_599_i3 line 579
  267. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_599_i3 line 581
  268. def OAI.SnakyPrototype.Certificate21.checked_599_i3 line 585
  269. def OAI.SnakyPrototype.Certificate21.height_599_i2 line 593
  270. def OAI.SnakyPrototype.Certificate21.childrenH_599_i2 line 594
  271. theorem OAI.SnakyPrototype.Certificate21.height_exact_599_i2 line 595
  272. theorem OAI.SnakyPrototype.Certificate21.required_origin_599_i2 line 596
  273. theorem OAI.SnakyPrototype.Certificate21.required_exact_599_i2 line 598
  274. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_599_i2 line 602
  275. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_599_i2 line 604
  276. def OAI.SnakyPrototype.Certificate21.checked_599_i2 line 608
  277. def OAI.SnakyPrototype.Certificate21.height_599_i1 line 616
  278. def OAI.SnakyPrototype.Certificate21.childrenH_599_i1 line 617
  279. theorem OAI.SnakyPrototype.Certificate21.height_exact_599_i1 line 618
  280. theorem OAI.SnakyPrototype.Certificate21.required_origin_599_i1 line 619
  281. theorem OAI.SnakyPrototype.Certificate21.required_exact_599_i1 line 621
  282. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_599_i1 line 625
  283. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_599_i1 line 627
  284. def OAI.SnakyPrototype.Certificate21.checked_599_i1 line 631
  285. def OAI.SnakyPrototype.Certificate21.height_599_i0 line 639
  286. def OAI.SnakyPrototype.Certificate21.childrenH_599_i0 line 640
  287. theorem OAI.SnakyPrototype.Certificate21.height_exact_599_i0 line 641
  288. theorem OAI.SnakyPrototype.Certificate21.required_origin_599_i0 line 642
  289. theorem OAI.SnakyPrototype.Certificate21.required_exact_599_i0 line 644
  290. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_599_i0 line 648
  291. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_599_i0 line 650
  292. def OAI.SnakyPrototype.Certificate21.checked_599_i0 line 654
  293. def OAI.SnakyPrototype.Certificate21.height_599 line 662
  294. def OAI.SnakyPrototype.Certificate21.childrenH_599 line 663
  295. theorem OAI.SnakyPrototype.Certificate21.height_exact_599 line 664
  296. theorem OAI.SnakyPrototype.Certificate21.required_origin_599 line 665
  297. theorem OAI.SnakyPrototype.Certificate21.required_exact_599 line 667
  298. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_599 line 671
  299. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_599 line 673
  300. def OAI.SnakyPrototype.Certificate21.checked_599 line 677
  301. def OAI.SnakyPrototype.Certificate21.height_605_i0 line 685
  302. def OAI.SnakyPrototype.Certificate21.childrenH_605_i0 line 686
  303. theorem OAI.SnakyPrototype.Certificate21.height_exact_605_i0 line 687
  304. theorem OAI.SnakyPrototype.Certificate21.required_origin_605_i0 line 688
  305. theorem OAI.SnakyPrototype.Certificate21.required_exact_605_i0 line 690
  306. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_605_i0 line 694
  307. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_605_i0 line 696
  308. def OAI.SnakyPrototype.Certificate21.checked_605_i0 line 700
  309. def OAI.SnakyPrototype.Certificate21.height_605 line 708
  310. def OAI.SnakyPrototype.Certificate21.childrenH_605 line 709
  311. theorem OAI.SnakyPrototype.Certificate21.height_exact_605 line 710
  312. theorem OAI.SnakyPrototype.Certificate21.required_origin_605 line 711
  313. theorem OAI.SnakyPrototype.Certificate21.required_exact_605 line 713
  314. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_605 line 717
  315. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_605 line 719
  316. def OAI.SnakyPrototype.Certificate21.checked_605 line 723
  317. def OAI.SnakyPrototype.Certificate21.height_618_i2 line 731
  318. def OAI.SnakyPrototype.Certificate21.childrenH_618_i2 line 732
  319. theorem OAI.SnakyPrototype.Certificate21.height_exact_618_i2 line 733
  320. theorem OAI.SnakyPrototype.Certificate21.required_origin_618_i2 line 734
  321. theorem OAI.SnakyPrototype.Certificate21.required_exact_618_i2 line 736
  322. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_618_i2 line 740
  323. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_618_i2 line 742
  324. def OAI.SnakyPrototype.Certificate21.checked_618_i2 line 746
  325. def OAI.SnakyPrototype.Certificate21.height_618_i1 line 754
  326. def OAI.SnakyPrototype.Certificate21.childrenH_618_i1 line 755
  327. theorem OAI.SnakyPrototype.Certificate21.height_exact_618_i1 line 756
  328. theorem OAI.SnakyPrototype.Certificate21.required_origin_618_i1 line 757
  329. theorem OAI.SnakyPrototype.Certificate21.required_exact_618_i1 line 759
  330. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_618_i1 line 763
  331. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_618_i1 line 765
  332. def OAI.SnakyPrototype.Certificate21.checked_618_i1 line 769
  333. def OAI.SnakyPrototype.Certificate21.height_618_i0 line 777
  334. def OAI.SnakyPrototype.Certificate21.childrenH_618_i0 line 778
  335. theorem OAI.SnakyPrototype.Certificate21.height_exact_618_i0 line 779
  336. theorem OAI.SnakyPrototype.Certificate21.required_origin_618_i0 line 780
  337. theorem OAI.SnakyPrototype.Certificate21.required_exact_618_i0 line 782
  338. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_618_i0 line 786
  339. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_618_i0 line 788
  340. def OAI.SnakyPrototype.Certificate21.checked_618_i0 line 792
  341. def OAI.SnakyPrototype.Certificate21.height_618_i3 line 800
  342. def OAI.SnakyPrototype.Certificate21.childrenH_618_i3 line 801
  343. theorem OAI.SnakyPrototype.Certificate21.height_exact_618_i3 line 802
  344. theorem OAI.SnakyPrototype.Certificate21.required_origin_618_i3 line 803
  345. theorem OAI.SnakyPrototype.Certificate21.required_exact_618_i3 line 805
  346. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_618_i3 line 809
  347. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_618_i3 line 811
  348. def OAI.SnakyPrototype.Certificate21.checked_618_i3 line 815
  349. def OAI.SnakyPrototype.Certificate21.height_618_i4 line 823
  350. def OAI.SnakyPrototype.Certificate21.childrenH_618_i4 line 824
  351. theorem OAI.SnakyPrototype.Certificate21.height_exact_618_i4 line 825
  352. theorem OAI.SnakyPrototype.Certificate21.required_origin_618_i4 line 826
  353. theorem OAI.SnakyPrototype.Certificate21.required_exact_618_i4 line 828
  354. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_618_i4 line 832
  355. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_618_i4 line 834
  356. def OAI.SnakyPrototype.Certificate21.checked_618_i4 line 838
  357. def OAI.SnakyPrototype.Certificate21.height_618_i5 line 846
  358. def OAI.SnakyPrototype.Certificate21.childrenH_618_i5 line 847
  359. theorem OAI.SnakyPrototype.Certificate21.height_exact_618_i5 line 848
  360. theorem OAI.SnakyPrototype.Certificate21.required_origin_618_i5 line 849
  361. theorem OAI.SnakyPrototype.Certificate21.required_exact_618_i5 line 851
  362. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_618_i5 line 855
  363. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_618_i5 line 857
  364. def OAI.SnakyPrototype.Certificate21.checked_618_i5 line 861
  365. def OAI.SnakyPrototype.Certificate21.height_618_i8 line 869
  366. def OAI.SnakyPrototype.Certificate21.childrenH_618_i8 line 870
  367. theorem OAI.SnakyPrototype.Certificate21.height_exact_618_i8 line 871
  368. theorem OAI.SnakyPrototype.Certificate21.required_origin_618_i8 line 872
  369. theorem OAI.SnakyPrototype.Certificate21.required_exact_618_i8 line 874
  370. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_618_i8 line 878
  371. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_618_i8 line 880
  372. def OAI.SnakyPrototype.Certificate21.checked_618_i8 line 884
  373. def OAI.SnakyPrototype.Certificate21.height_618_i7 line 892
  374. def OAI.SnakyPrototype.Certificate21.childrenH_618_i7 line 893
  375. theorem OAI.SnakyPrototype.Certificate21.height_exact_618_i7 line 894
  376. theorem OAI.SnakyPrototype.Certificate21.required_origin_618_i7 line 895
  377. theorem OAI.SnakyPrototype.Certificate21.required_exact_618_i7 line 897
  378. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_618_i7 line 901
  379. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_618_i7 line 903
  380. def OAI.SnakyPrototype.Certificate21.checked_618_i7 line 907
  381. def OAI.SnakyPrototype.Certificate21.height_618_i6 line 915
  382. def OAI.SnakyPrototype.Certificate21.childrenH_618_i6 line 916
  383. theorem OAI.SnakyPrototype.Certificate21.height_exact_618_i6 line 917
  384. theorem OAI.SnakyPrototype.Certificate21.required_origin_618_i6 line 918
  385. theorem OAI.SnakyPrototype.Certificate21.required_exact_618_i6 line 920
  386. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_618_i6 line 924
  387. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_618_i6 line 926
  388. def OAI.SnakyPrototype.Certificate21.checked_618_i6 line 930
  389. def OAI.SnakyPrototype.Certificate21.height_618 line 938
  390. def OAI.SnakyPrototype.Certificate21.childrenH_618 line 939
  391. theorem OAI.SnakyPrototype.Certificate21.height_exact_618 line 940
  392. theorem OAI.SnakyPrototype.Certificate21.required_origin_618 line 941
  393. theorem OAI.SnakyPrototype.Certificate21.required_exact_618 line 943
  394. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_618 line 947
  395. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_618 line 949
  396. def OAI.SnakyPrototype.Certificate21.checked_618 line 953