OAI/GameTheory/SnakyTwentyOne/Cards/Height10Part04.lean

GitHub source file

360 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_569_i2 line 27
  2. def OAI.SnakyPrototype.Certificate21.envelope_569_i2 line 28
  3. def OAI.SnakyPrototype.Certificate21.childrenC_569_i2 line 29
  4. def OAI.SnakyPrototype.Certificate21.childrenD_569_i2 line 30
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_569_i2 line 31
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_569_i2 line 32
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_569_i2 line 33
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_569_i2 line 34
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_569_i2 line 35
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_569_i2 line 40
  11. def OAI.SnakyPrototype.Certificate21.required_569_i1 line 45
  12. def OAI.SnakyPrototype.Certificate21.envelope_569_i1 line 46
  13. def OAI.SnakyPrototype.Certificate21.childrenC_569_i1 line 47
  14. def OAI.SnakyPrototype.Certificate21.childrenD_569_i1 line 48
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_569_i1 line 49
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_569_i1 line 50
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_569_i1 line 51
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_569_i1 line 52
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_569_i1 line 53
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_569_i1 line 58
  21. def OAI.SnakyPrototype.Certificate21.required_569_i3 line 63
  22. def OAI.SnakyPrototype.Certificate21.envelope_569_i3 line 64
  23. def OAI.SnakyPrototype.Certificate21.childrenC_569_i3 line 65
  24. def OAI.SnakyPrototype.Certificate21.childrenD_569_i3 line 66
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_569_i3 line 67
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_569_i3 line 68
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_569_i3 line 69
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_569_i3 line 70
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_569_i3 line 71
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_569_i3 line 76
  31. def OAI.SnakyPrototype.Certificate21.required_569_i0 line 81
  32. def OAI.SnakyPrototype.Certificate21.envelope_569_i0 line 82
  33. def OAI.SnakyPrototype.Certificate21.childrenC_569_i0 line 83
  34. def OAI.SnakyPrototype.Certificate21.childrenD_569_i0 line 84
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_569_i0 line 85
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_569_i0 line 86
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_569_i0 line 87
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_569_i0 line 88
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_569_i0 line 89
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_569_i0 line 95
  41. def OAI.SnakyPrototype.Certificate21.required_569_i4 line 100
  42. def OAI.SnakyPrototype.Certificate21.envelope_569_i4 line 101
  43. def OAI.SnakyPrototype.Certificate21.childrenC_569_i4 line 102
  44. def OAI.SnakyPrototype.Certificate21.childrenD_569_i4 line 103
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_569_i4 line 104
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_569_i4 line 105
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_569_i4 line 106
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_569_i4 line 107
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_569_i4 line 108
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_569_i4 line 113
  51. def OAI.SnakyPrototype.Certificate21.required_569_i6 line 118
  52. def OAI.SnakyPrototype.Certificate21.envelope_569_i6 line 119
  53. def OAI.SnakyPrototype.Certificate21.childrenC_569_i6 line 120
  54. def OAI.SnakyPrototype.Certificate21.childrenD_569_i6 line 121
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_569_i6 line 122
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_569_i6 line 123
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_569_i6 line 124
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_569_i6 line 125
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_569_i6 line 126
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_569_i6 line 131
  61. def OAI.SnakyPrototype.Certificate21.required_569_i7 line 136
  62. def OAI.SnakyPrototype.Certificate21.envelope_569_i7 line 137
  63. def OAI.SnakyPrototype.Certificate21.childrenC_569_i7 line 138
  64. def OAI.SnakyPrototype.Certificate21.childrenD_569_i7 line 139
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_569_i7 line 140
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_569_i7 line 141
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_569_i7 line 142
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_569_i7 line 143
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_569_i7 line 144
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_569_i7 line 149
  71. def OAI.SnakyPrototype.Certificate21.required_569_i5 line 154
  72. def OAI.SnakyPrototype.Certificate21.envelope_569_i5 line 155
  73. def OAI.SnakyPrototype.Certificate21.childrenC_569_i5 line 156
  74. def OAI.SnakyPrototype.Certificate21.childrenD_569_i5 line 157
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_569_i5 line 158
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_569_i5 line 159
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_569_i5 line 160
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_569_i5 line 161
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_569_i5 line 162
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_569_i5 line 168
  81. def OAI.SnakyPrototype.Certificate21.required_569 line 173
  82. def OAI.SnakyPrototype.Certificate21.envelope_569 line 174
  83. def OAI.SnakyPrototype.Certificate21.childrenC_569 line 175
  84. def OAI.SnakyPrototype.Certificate21.childrenD_569 line 176
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_569 line 177
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_569 line 178
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_569 line 179
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_569 line 180
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_569 line 181
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_569 line 190
  91. def OAI.SnakyPrototype.Certificate21.required_575_i0 line 195
  92. def OAI.SnakyPrototype.Certificate21.envelope_575_i0 line 196
  93. def OAI.SnakyPrototype.Certificate21.childrenC_575_i0 line 197
  94. def OAI.SnakyPrototype.Certificate21.childrenD_575_i0 line 198
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_575_i0 line 199
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_575_i0 line 200
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_575_i0 line 201
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_575_i0 line 202
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_575_i0 line 203
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_575_i0 line 208
  101. def OAI.SnakyPrototype.Certificate21.required_575_i2 line 213
  102. def OAI.SnakyPrototype.Certificate21.envelope_575_i2 line 214
  103. def OAI.SnakyPrototype.Certificate21.childrenC_575_i2 line 215
  104. def OAI.SnakyPrototype.Certificate21.childrenD_575_i2 line 216
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_575_i2 line 217
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_575_i2 line 218
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_575_i2 line 219
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_575_i2 line 220
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_575_i2 line 221
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_575_i2 line 226
  111. def OAI.SnakyPrototype.Certificate21.required_575_i1 line 231
  112. def OAI.SnakyPrototype.Certificate21.envelope_575_i1 line 232
  113. def OAI.SnakyPrototype.Certificate21.childrenC_575_i1 line 233
  114. def OAI.SnakyPrototype.Certificate21.childrenD_575_i1 line 234
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_575_i1 line 235
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_575_i1 line 236
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_575_i1 line 237
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_575_i1 line 238
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_575_i1 line 239
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_575_i1 line 244
  121. def OAI.SnakyPrototype.Certificate21.required_575_i3 line 249
  122. def OAI.SnakyPrototype.Certificate21.envelope_575_i3 line 250
  123. def OAI.SnakyPrototype.Certificate21.childrenC_575_i3 line 251
  124. def OAI.SnakyPrototype.Certificate21.childrenD_575_i3 line 252
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_575_i3 line 253
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_575_i3 line 254
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_575_i3 line 255
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_575_i3 line 256
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_575_i3 line 257
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_575_i3 line 262
  131. def OAI.SnakyPrototype.Certificate21.required_575 line 267
  132. def OAI.SnakyPrototype.Certificate21.envelope_575 line 268
  133. def OAI.SnakyPrototype.Certificate21.childrenC_575 line 269
  134. def OAI.SnakyPrototype.Certificate21.childrenD_575 line 270
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_575 line 271
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_575 line 272
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_575 line 273
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_575 line 274
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_575 line 275
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_575 line 283
  141. def OAI.SnakyPrototype.Certificate21.required_578 line 288
  142. def OAI.SnakyPrototype.Certificate21.envelope_578 line 289
  143. def OAI.SnakyPrototype.Certificate21.childrenC_578 line 290
  144. def OAI.SnakyPrototype.Certificate21.childrenD_578 line 291
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_578 line 292
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_578 line 293
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_578 line 294
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_578 line 295
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_578 line 296
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_578 line 303
  151. def OAI.SnakyPrototype.Certificate21.required_580 line 308
  152. def OAI.SnakyPrototype.Certificate21.envelope_580 line 309
  153. def OAI.SnakyPrototype.Certificate21.childrenC_580 line 310
  154. def OAI.SnakyPrototype.Certificate21.childrenD_580 line 311
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_580 line 312
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_580 line 313
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_580 line 314
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_580 line 315
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_580 line 316
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_580 line 323
  161. def OAI.SnakyPrototype.Certificate21.required_585_i2 line 328
  162. def OAI.SnakyPrototype.Certificate21.envelope_585_i2 line 329
  163. def OAI.SnakyPrototype.Certificate21.childrenC_585_i2 line 330
  164. def OAI.SnakyPrototype.Certificate21.childrenD_585_i2 line 331
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_585_i2 line 332
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_585_i2 line 333
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_585_i2 line 334
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_585_i2 line 335
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_585_i2 line 336
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_585_i2 line 341
  171. def OAI.SnakyPrototype.Certificate21.required_585_i1 line 346
  172. def OAI.SnakyPrototype.Certificate21.envelope_585_i1 line 347
  173. def OAI.SnakyPrototype.Certificate21.childrenC_585_i1 line 348
  174. def OAI.SnakyPrototype.Certificate21.childrenD_585_i1 line 349
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_585_i1 line 350
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_585_i1 line 351
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_585_i1 line 352
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_585_i1 line 353
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_585_i1 line 354
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_585_i1 line 359
  181. def OAI.SnakyPrototype.Certificate21.required_585_i0 line 364
  182. def OAI.SnakyPrototype.Certificate21.envelope_585_i0 line 365
  183. def OAI.SnakyPrototype.Certificate21.childrenC_585_i0 line 366
  184. def OAI.SnakyPrototype.Certificate21.childrenD_585_i0 line 367
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_585_i0 line 368
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_585_i0 line 369
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_585_i0 line 370
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_585_i0 line 371
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_585_i0 line 372
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_585_i0 line 377
  191. def OAI.SnakyPrototype.Certificate21.required_585 line 382
  192. def OAI.SnakyPrototype.Certificate21.envelope_585 line 383
  193. def OAI.SnakyPrototype.Certificate21.childrenC_585 line 384
  194. def OAI.SnakyPrototype.Certificate21.childrenD_585 line 385
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_585 line 386
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_585 line 387
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_585 line 388
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_585 line 389
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_585 line 390
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_585 line 395
  201. def OAI.SnakyPrototype.Certificate21.height_569_i2 line 400
  202. def OAI.SnakyPrototype.Certificate21.childrenH_569_i2 line 401
  203. theorem OAI.SnakyPrototype.Certificate21.height_exact_569_i2 line 402
  204. theorem OAI.SnakyPrototype.Certificate21.required_origin_569_i2 line 403
  205. theorem OAI.SnakyPrototype.Certificate21.required_exact_569_i2 line 405
  206. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_569_i2 line 409
  207. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_569_i2 line 411
  208. def OAI.SnakyPrototype.Certificate21.checked_569_i2 line 415
  209. def OAI.SnakyPrototype.Certificate21.height_569_i1 line 423
  210. def OAI.SnakyPrototype.Certificate21.childrenH_569_i1 line 424
  211. theorem OAI.SnakyPrototype.Certificate21.height_exact_569_i1 line 425
  212. theorem OAI.SnakyPrototype.Certificate21.required_origin_569_i1 line 426
  213. theorem OAI.SnakyPrototype.Certificate21.required_exact_569_i1 line 428
  214. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_569_i1 line 432
  215. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_569_i1 line 434
  216. def OAI.SnakyPrototype.Certificate21.checked_569_i1 line 438
  217. def OAI.SnakyPrototype.Certificate21.height_569_i3 line 446
  218. def OAI.SnakyPrototype.Certificate21.childrenH_569_i3 line 447
  219. theorem OAI.SnakyPrototype.Certificate21.height_exact_569_i3 line 448
  220. theorem OAI.SnakyPrototype.Certificate21.required_origin_569_i3 line 449
  221. theorem OAI.SnakyPrototype.Certificate21.required_exact_569_i3 line 451
  222. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_569_i3 line 455
  223. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_569_i3 line 457
  224. def OAI.SnakyPrototype.Certificate21.checked_569_i3 line 461
  225. def OAI.SnakyPrototype.Certificate21.height_569_i0 line 469
  226. def OAI.SnakyPrototype.Certificate21.childrenH_569_i0 line 470
  227. theorem OAI.SnakyPrototype.Certificate21.height_exact_569_i0 line 471
  228. theorem OAI.SnakyPrototype.Certificate21.required_origin_569_i0 line 472
  229. theorem OAI.SnakyPrototype.Certificate21.required_exact_569_i0 line 474
  230. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_569_i0 line 478
  231. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_569_i0 line 480
  232. def OAI.SnakyPrototype.Certificate21.checked_569_i0 line 484
  233. def OAI.SnakyPrototype.Certificate21.height_569_i4 line 492
  234. def OAI.SnakyPrototype.Certificate21.childrenH_569_i4 line 493
  235. theorem OAI.SnakyPrototype.Certificate21.height_exact_569_i4 line 494
  236. theorem OAI.SnakyPrototype.Certificate21.required_origin_569_i4 line 495
  237. theorem OAI.SnakyPrototype.Certificate21.required_exact_569_i4 line 497
  238. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_569_i4 line 501
  239. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_569_i4 line 503
  240. def OAI.SnakyPrototype.Certificate21.checked_569_i4 line 507
  241. def OAI.SnakyPrototype.Certificate21.height_569_i6 line 515
  242. def OAI.SnakyPrototype.Certificate21.childrenH_569_i6 line 516
  243. theorem OAI.SnakyPrototype.Certificate21.height_exact_569_i6 line 517
  244. theorem OAI.SnakyPrototype.Certificate21.required_origin_569_i6 line 518
  245. theorem OAI.SnakyPrototype.Certificate21.required_exact_569_i6 line 520
  246. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_569_i6 line 524
  247. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_569_i6 line 526
  248. def OAI.SnakyPrototype.Certificate21.checked_569_i6 line 530
  249. def OAI.SnakyPrototype.Certificate21.height_569_i7 line 538
  250. def OAI.SnakyPrototype.Certificate21.childrenH_569_i7 line 539
  251. theorem OAI.SnakyPrototype.Certificate21.height_exact_569_i7 line 540
  252. theorem OAI.SnakyPrototype.Certificate21.required_origin_569_i7 line 541
  253. theorem OAI.SnakyPrototype.Certificate21.required_exact_569_i7 line 543
  254. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_569_i7 line 547
  255. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_569_i7 line 549
  256. def OAI.SnakyPrototype.Certificate21.checked_569_i7 line 553
  257. def OAI.SnakyPrototype.Certificate21.height_569_i5 line 561
  258. def OAI.SnakyPrototype.Certificate21.childrenH_569_i5 line 562
  259. theorem OAI.SnakyPrototype.Certificate21.height_exact_569_i5 line 563
  260. theorem OAI.SnakyPrototype.Certificate21.required_origin_569_i5 line 564
  261. theorem OAI.SnakyPrototype.Certificate21.required_exact_569_i5 line 566
  262. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_569_i5 line 570
  263. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_569_i5 line 572
  264. def OAI.SnakyPrototype.Certificate21.checked_569_i5 line 576
  265. def OAI.SnakyPrototype.Certificate21.height_569 line 584
  266. def OAI.SnakyPrototype.Certificate21.childrenH_569 line 585
  267. theorem OAI.SnakyPrototype.Certificate21.height_exact_569 line 586
  268. theorem OAI.SnakyPrototype.Certificate21.required_origin_569 line 587
  269. theorem OAI.SnakyPrototype.Certificate21.required_exact_569 line 589
  270. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_569 line 593
  271. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_569 line 595
  272. def OAI.SnakyPrototype.Certificate21.checked_569 line 599
  273. def OAI.SnakyPrototype.Certificate21.height_575_i0 line 607
  274. def OAI.SnakyPrototype.Certificate21.childrenH_575_i0 line 608
  275. theorem OAI.SnakyPrototype.Certificate21.height_exact_575_i0 line 609
  276. theorem OAI.SnakyPrototype.Certificate21.required_origin_575_i0 line 610
  277. theorem OAI.SnakyPrototype.Certificate21.required_exact_575_i0 line 612
  278. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_575_i0 line 616
  279. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_575_i0 line 618
  280. def OAI.SnakyPrototype.Certificate21.checked_575_i0 line 622
  281. def OAI.SnakyPrototype.Certificate21.height_575_i2 line 630
  282. def OAI.SnakyPrototype.Certificate21.childrenH_575_i2 line 631
  283. theorem OAI.SnakyPrototype.Certificate21.height_exact_575_i2 line 632
  284. theorem OAI.SnakyPrototype.Certificate21.required_origin_575_i2 line 633
  285. theorem OAI.SnakyPrototype.Certificate21.required_exact_575_i2 line 635
  286. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_575_i2 line 639
  287. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_575_i2 line 641
  288. def OAI.SnakyPrototype.Certificate21.checked_575_i2 line 645
  289. def OAI.SnakyPrototype.Certificate21.height_575_i1 line 653
  290. def OAI.SnakyPrototype.Certificate21.childrenH_575_i1 line 654
  291. theorem OAI.SnakyPrototype.Certificate21.height_exact_575_i1 line 655
  292. theorem OAI.SnakyPrototype.Certificate21.required_origin_575_i1 line 656
  293. theorem OAI.SnakyPrototype.Certificate21.required_exact_575_i1 line 658
  294. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_575_i1 line 662
  295. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_575_i1 line 664
  296. def OAI.SnakyPrototype.Certificate21.checked_575_i1 line 668
  297. def OAI.SnakyPrototype.Certificate21.height_575_i3 line 676
  298. def OAI.SnakyPrototype.Certificate21.childrenH_575_i3 line 677
  299. theorem OAI.SnakyPrototype.Certificate21.height_exact_575_i3 line 678
  300. theorem OAI.SnakyPrototype.Certificate21.required_origin_575_i3 line 679
  301. theorem OAI.SnakyPrototype.Certificate21.required_exact_575_i3 line 681
  302. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_575_i3 line 685
  303. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_575_i3 line 687
  304. def OAI.SnakyPrototype.Certificate21.checked_575_i3 line 691
  305. def OAI.SnakyPrototype.Certificate21.height_575 line 699
  306. def OAI.SnakyPrototype.Certificate21.childrenH_575 line 700
  307. theorem OAI.SnakyPrototype.Certificate21.height_exact_575 line 701
  308. theorem OAI.SnakyPrototype.Certificate21.required_origin_575 line 702
  309. theorem OAI.SnakyPrototype.Certificate21.required_exact_575 line 704
  310. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_575 line 708
  311. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_575 line 710
  312. def OAI.SnakyPrototype.Certificate21.checked_575 line 714
  313. def OAI.SnakyPrototype.Certificate21.height_578 line 722
  314. def OAI.SnakyPrototype.Certificate21.childrenH_578 line 723
  315. theorem OAI.SnakyPrototype.Certificate21.height_exact_578 line 724
  316. theorem OAI.SnakyPrototype.Certificate21.required_origin_578 line 725
  317. theorem OAI.SnakyPrototype.Certificate21.required_exact_578 line 727
  318. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_578 line 731
  319. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_578 line 733
  320. def OAI.SnakyPrototype.Certificate21.checked_578 line 737
  321. def OAI.SnakyPrototype.Certificate21.height_580 line 745
  322. def OAI.SnakyPrototype.Certificate21.childrenH_580 line 746
  323. theorem OAI.SnakyPrototype.Certificate21.height_exact_580 line 747
  324. theorem OAI.SnakyPrototype.Certificate21.required_origin_580 line 748
  325. theorem OAI.SnakyPrototype.Certificate21.required_exact_580 line 750
  326. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_580 line 754
  327. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_580 line 756
  328. def OAI.SnakyPrototype.Certificate21.checked_580 line 760
  329. def OAI.SnakyPrototype.Certificate21.height_585_i2 line 768
  330. def OAI.SnakyPrototype.Certificate21.childrenH_585_i2 line 769
  331. theorem OAI.SnakyPrototype.Certificate21.height_exact_585_i2 line 770
  332. theorem OAI.SnakyPrototype.Certificate21.required_origin_585_i2 line 771
  333. theorem OAI.SnakyPrototype.Certificate21.required_exact_585_i2 line 773
  334. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_585_i2 line 777
  335. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_585_i2 line 779
  336. def OAI.SnakyPrototype.Certificate21.checked_585_i2 line 783
  337. def OAI.SnakyPrototype.Certificate21.height_585_i1 line 791
  338. def OAI.SnakyPrototype.Certificate21.childrenH_585_i1 line 792
  339. theorem OAI.SnakyPrototype.Certificate21.height_exact_585_i1 line 793
  340. theorem OAI.SnakyPrototype.Certificate21.required_origin_585_i1 line 794
  341. theorem OAI.SnakyPrototype.Certificate21.required_exact_585_i1 line 796
  342. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_585_i1 line 800
  343. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_585_i1 line 802
  344. def OAI.SnakyPrototype.Certificate21.checked_585_i1 line 806
  345. def OAI.SnakyPrototype.Certificate21.height_585_i0 line 814
  346. def OAI.SnakyPrototype.Certificate21.childrenH_585_i0 line 815
  347. theorem OAI.SnakyPrototype.Certificate21.height_exact_585_i0 line 816
  348. theorem OAI.SnakyPrototype.Certificate21.required_origin_585_i0 line 817
  349. theorem OAI.SnakyPrototype.Certificate21.required_exact_585_i0 line 819
  350. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_585_i0 line 823
  351. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_585_i0 line 825
  352. def OAI.SnakyPrototype.Certificate21.checked_585_i0 line 829
  353. def OAI.SnakyPrototype.Certificate21.height_585 line 837
  354. def OAI.SnakyPrototype.Certificate21.childrenH_585 line 838
  355. theorem OAI.SnakyPrototype.Certificate21.height_exact_585 line 839
  356. theorem OAI.SnakyPrototype.Certificate21.required_origin_585 line 840
  357. theorem OAI.SnakyPrototype.Certificate21.required_exact_585 line 842
  358. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_585 line 846
  359. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_585 line 848
  360. def OAI.SnakyPrototype.Certificate21.checked_585 line 852