OAI/GameTheory/SnakyTwentyOne/Cards/Height09Part08.lean

GitHub source file

306 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_673_i0 line 24
  2. def OAI.SnakyPrototype.Certificate21.envelope_673_i0 line 25
  3. def OAI.SnakyPrototype.Certificate21.childrenC_673_i0 line 26
  4. def OAI.SnakyPrototype.Certificate21.childrenD_673_i0 line 27
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_673_i0 line 28
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_673_i0 line 29
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_673_i0 line 30
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_673_i0 line 31
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_673_i0 line 32
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_673_i0 line 37
  11. def OAI.SnakyPrototype.Certificate21.required_673_i3 line 42
  12. def OAI.SnakyPrototype.Certificate21.envelope_673_i3 line 43
  13. def OAI.SnakyPrototype.Certificate21.childrenC_673_i3 line 44
  14. def OAI.SnakyPrototype.Certificate21.childrenD_673_i3 line 45
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_673_i3 line 46
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_673_i3 line 47
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_673_i3 line 48
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_673_i3 line 49
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_673_i3 line 50
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_673_i3 line 55
  21. def OAI.SnakyPrototype.Certificate21.required_673_i2 line 60
  22. def OAI.SnakyPrototype.Certificate21.envelope_673_i2 line 61
  23. def OAI.SnakyPrototype.Certificate21.childrenC_673_i2 line 62
  24. def OAI.SnakyPrototype.Certificate21.childrenD_673_i2 line 63
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_673_i2 line 64
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_673_i2 line 65
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_673_i2 line 66
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_673_i2 line 67
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_673_i2 line 68
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_673_i2 line 73
  31. def OAI.SnakyPrototype.Certificate21.required_673_i1 line 78
  32. def OAI.SnakyPrototype.Certificate21.envelope_673_i1 line 79
  33. def OAI.SnakyPrototype.Certificate21.childrenC_673_i1 line 80
  34. def OAI.SnakyPrototype.Certificate21.childrenD_673_i1 line 81
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_673_i1 line 82
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_673_i1 line 83
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_673_i1 line 84
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_673_i1 line 85
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_673_i1 line 86
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_673_i1 line 91
  41. def OAI.SnakyPrototype.Certificate21.required_673_i4 line 96
  42. def OAI.SnakyPrototype.Certificate21.envelope_673_i4 line 97
  43. def OAI.SnakyPrototype.Certificate21.childrenC_673_i4 line 98
  44. def OAI.SnakyPrototype.Certificate21.childrenD_673_i4 line 99
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_673_i4 line 100
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_673_i4 line 101
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_673_i4 line 102
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_673_i4 line 103
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_673_i4 line 104
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_673_i4 line 112
  51. def OAI.SnakyPrototype.Certificate21.required_673_i6 line 117
  52. def OAI.SnakyPrototype.Certificate21.envelope_673_i6 line 118
  53. def OAI.SnakyPrototype.Certificate21.childrenC_673_i6 line 119
  54. def OAI.SnakyPrototype.Certificate21.childrenD_673_i6 line 120
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_673_i6 line 121
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_673_i6 line 122
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_673_i6 line 123
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_673_i6 line 124
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_673_i6 line 125
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_673_i6 line 130
  61. def OAI.SnakyPrototype.Certificate21.required_673_i5 line 135
  62. def OAI.SnakyPrototype.Certificate21.envelope_673_i5 line 136
  63. def OAI.SnakyPrototype.Certificate21.childrenC_673_i5 line 137
  64. def OAI.SnakyPrototype.Certificate21.childrenD_673_i5 line 138
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_673_i5 line 139
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_673_i5 line 140
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_673_i5 line 141
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_673_i5 line 142
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_673_i5 line 143
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_673_i5 line 148
  71. def OAI.SnakyPrototype.Certificate21.required_673_i9 line 153
  72. def OAI.SnakyPrototype.Certificate21.envelope_673_i9 line 154
  73. def OAI.SnakyPrototype.Certificate21.childrenC_673_i9 line 155
  74. def OAI.SnakyPrototype.Certificate21.childrenD_673_i9 line 156
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_673_i9 line 157
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_673_i9 line 158
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_673_i9 line 159
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_673_i9 line 160
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_673_i9 line 161
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_673_i9 line 167
  81. def OAI.SnakyPrototype.Certificate21.required_673_i10 line 172
  82. def OAI.SnakyPrototype.Certificate21.envelope_673_i10 line 173
  83. def OAI.SnakyPrototype.Certificate21.childrenC_673_i10 line 174
  84. def OAI.SnakyPrototype.Certificate21.childrenD_673_i10 line 175
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_673_i10 line 176
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_673_i10 line 177
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_673_i10 line 178
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_673_i10 line 179
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_673_i10 line 180
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_673_i10 line 185
  91. def OAI.SnakyPrototype.Certificate21.required_673_i8 line 190
  92. def OAI.SnakyPrototype.Certificate21.envelope_673_i8 line 191
  93. def OAI.SnakyPrototype.Certificate21.childrenC_673_i8 line 192
  94. def OAI.SnakyPrototype.Certificate21.childrenD_673_i8 line 193
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_673_i8 line 194
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_673_i8 line 195
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_673_i8 line 196
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_673_i8 line 197
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_673_i8 line 198
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_673_i8 line 206
  101. def OAI.SnakyPrototype.Certificate21.required_673_i7 line 211
  102. def OAI.SnakyPrototype.Certificate21.envelope_673_i7 line 212
  103. def OAI.SnakyPrototype.Certificate21.childrenC_673_i7 line 213
  104. def OAI.SnakyPrototype.Certificate21.childrenD_673_i7 line 214
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_673_i7 line 215
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_673_i7 line 216
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_673_i7 line 217
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_673_i7 line 218
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_673_i7 line 219
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_673_i7 line 224
  111. def OAI.SnakyPrototype.Certificate21.required_673 line 229
  112. def OAI.SnakyPrototype.Certificate21.envelope_673 line 230
  113. def OAI.SnakyPrototype.Certificate21.childrenC_673 line 231
  114. def OAI.SnakyPrototype.Certificate21.childrenD_673 line 232
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_673 line 233
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_673 line 234
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_673 line 235
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_673 line 236
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_673 line 237
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_673 line 245
  121. def OAI.SnakyPrototype.Certificate21.required_686_i0 line 250
  122. def OAI.SnakyPrototype.Certificate21.envelope_686_i0 line 251
  123. def OAI.SnakyPrototype.Certificate21.childrenC_686_i0 line 252
  124. def OAI.SnakyPrototype.Certificate21.childrenD_686_i0 line 253
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_686_i0 line 254
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_686_i0 line 255
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_686_i0 line 256
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_686_i0 line 257
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_686_i0 line 258
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_686_i0 line 264
  131. def OAI.SnakyPrototype.Certificate21.required_686_i1 line 269
  132. def OAI.SnakyPrototype.Certificate21.envelope_686_i1 line 270
  133. def OAI.SnakyPrototype.Certificate21.childrenC_686_i1 line 271
  134. def OAI.SnakyPrototype.Certificate21.childrenD_686_i1 line 272
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_686_i1 line 273
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_686_i1 line 274
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_686_i1 line 275
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_686_i1 line 276
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_686_i1 line 277
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_686_i1 line 283
  141. def OAI.SnakyPrototype.Certificate21.required_686 line 288
  142. def OAI.SnakyPrototype.Certificate21.envelope_686 line 289
  143. def OAI.SnakyPrototype.Certificate21.childrenC_686 line 290
  144. def OAI.SnakyPrototype.Certificate21.childrenD_686 line 291
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_686 line 292
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_686 line 293
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_686 line 294
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_686 line 295
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_686 line 296
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_686 line 306
  151. def OAI.SnakyPrototype.Certificate21.required_688_i0 line 311
  152. def OAI.SnakyPrototype.Certificate21.envelope_688_i0 line 312
  153. def OAI.SnakyPrototype.Certificate21.childrenC_688_i0 line 313
  154. def OAI.SnakyPrototype.Certificate21.childrenD_688_i0 line 314
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_688_i0 line 315
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_688_i0 line 316
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_688_i0 line 317
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_688_i0 line 318
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_688_i0 line 319
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_688_i0 line 327
  161. def OAI.SnakyPrototype.Certificate21.required_688 line 332
  162. def OAI.SnakyPrototype.Certificate21.envelope_688 line 333
  163. def OAI.SnakyPrototype.Certificate21.childrenC_688 line 334
  164. def OAI.SnakyPrototype.Certificate21.childrenD_688 line 335
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_688 line 336
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_688 line 337
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_688 line 338
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_688 line 339
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_688 line 340
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_688 line 345
  171. def OAI.SnakyPrototype.Certificate21.height_673_i0 line 350
  172. def OAI.SnakyPrototype.Certificate21.childrenH_673_i0 line 351
  173. theorem OAI.SnakyPrototype.Certificate21.height_exact_673_i0 line 352
  174. theorem OAI.SnakyPrototype.Certificate21.required_origin_673_i0 line 353
  175. theorem OAI.SnakyPrototype.Certificate21.required_exact_673_i0 line 355
  176. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_673_i0 line 359
  177. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_673_i0 line 361
  178. def OAI.SnakyPrototype.Certificate21.checked_673_i0 line 365
  179. def OAI.SnakyPrototype.Certificate21.height_673_i3 line 373
  180. def OAI.SnakyPrototype.Certificate21.childrenH_673_i3 line 374
  181. theorem OAI.SnakyPrototype.Certificate21.height_exact_673_i3 line 375
  182. theorem OAI.SnakyPrototype.Certificate21.required_origin_673_i3 line 376
  183. theorem OAI.SnakyPrototype.Certificate21.required_exact_673_i3 line 378
  184. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_673_i3 line 382
  185. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_673_i3 line 384
  186. def OAI.SnakyPrototype.Certificate21.checked_673_i3 line 388
  187. def OAI.SnakyPrototype.Certificate21.height_673_i2 line 396
  188. def OAI.SnakyPrototype.Certificate21.childrenH_673_i2 line 397
  189. theorem OAI.SnakyPrototype.Certificate21.height_exact_673_i2 line 398
  190. theorem OAI.SnakyPrototype.Certificate21.required_origin_673_i2 line 399
  191. theorem OAI.SnakyPrototype.Certificate21.required_exact_673_i2 line 401
  192. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_673_i2 line 405
  193. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_673_i2 line 407
  194. def OAI.SnakyPrototype.Certificate21.checked_673_i2 line 411
  195. def OAI.SnakyPrototype.Certificate21.height_673_i1 line 419
  196. def OAI.SnakyPrototype.Certificate21.childrenH_673_i1 line 420
  197. theorem OAI.SnakyPrototype.Certificate21.height_exact_673_i1 line 421
  198. theorem OAI.SnakyPrototype.Certificate21.required_origin_673_i1 line 422
  199. theorem OAI.SnakyPrototype.Certificate21.required_exact_673_i1 line 424
  200. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_673_i1 line 428
  201. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_673_i1 line 430
  202. def OAI.SnakyPrototype.Certificate21.checked_673_i1 line 434
  203. def OAI.SnakyPrototype.Certificate21.height_673_i4 line 442
  204. def OAI.SnakyPrototype.Certificate21.childrenH_673_i4 line 443
  205. theorem OAI.SnakyPrototype.Certificate21.height_exact_673_i4 line 444
  206. theorem OAI.SnakyPrototype.Certificate21.required_origin_673_i4 line 445
  207. theorem OAI.SnakyPrototype.Certificate21.required_exact_673_i4 line 447
  208. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_673_i4 line 451
  209. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_673_i4 line 453
  210. def OAI.SnakyPrototype.Certificate21.checked_673_i4 line 457
  211. def OAI.SnakyPrototype.Certificate21.height_673_i6 line 465
  212. def OAI.SnakyPrototype.Certificate21.childrenH_673_i6 line 466
  213. theorem OAI.SnakyPrototype.Certificate21.height_exact_673_i6 line 467
  214. theorem OAI.SnakyPrototype.Certificate21.required_origin_673_i6 line 468
  215. theorem OAI.SnakyPrototype.Certificate21.required_exact_673_i6 line 470
  216. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_673_i6 line 474
  217. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_673_i6 line 476
  218. def OAI.SnakyPrototype.Certificate21.checked_673_i6 line 480
  219. def OAI.SnakyPrototype.Certificate21.height_673_i5 line 488
  220. def OAI.SnakyPrototype.Certificate21.childrenH_673_i5 line 489
  221. theorem OAI.SnakyPrototype.Certificate21.height_exact_673_i5 line 490
  222. theorem OAI.SnakyPrototype.Certificate21.required_origin_673_i5 line 491
  223. theorem OAI.SnakyPrototype.Certificate21.required_exact_673_i5 line 493
  224. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_673_i5 line 497
  225. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_673_i5 line 499
  226. def OAI.SnakyPrototype.Certificate21.checked_673_i5 line 503
  227. def OAI.SnakyPrototype.Certificate21.height_673_i9 line 511
  228. def OAI.SnakyPrototype.Certificate21.childrenH_673_i9 line 512
  229. theorem OAI.SnakyPrototype.Certificate21.height_exact_673_i9 line 513
  230. theorem OAI.SnakyPrototype.Certificate21.required_origin_673_i9 line 514
  231. theorem OAI.SnakyPrototype.Certificate21.required_exact_673_i9 line 516
  232. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_673_i9 line 520
  233. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_673_i9 line 522
  234. def OAI.SnakyPrototype.Certificate21.checked_673_i9 line 526
  235. def OAI.SnakyPrototype.Certificate21.height_673_i10 line 534
  236. def OAI.SnakyPrototype.Certificate21.childrenH_673_i10 line 535
  237. theorem OAI.SnakyPrototype.Certificate21.height_exact_673_i10 line 536
  238. theorem OAI.SnakyPrototype.Certificate21.required_origin_673_i10 line 537
  239. theorem OAI.SnakyPrototype.Certificate21.required_exact_673_i10 line 539
  240. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_673_i10 line 543
  241. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_673_i10 line 545
  242. def OAI.SnakyPrototype.Certificate21.checked_673_i10 line 549
  243. def OAI.SnakyPrototype.Certificate21.height_673_i8 line 557
  244. def OAI.SnakyPrototype.Certificate21.childrenH_673_i8 line 558
  245. theorem OAI.SnakyPrototype.Certificate21.height_exact_673_i8 line 559
  246. theorem OAI.SnakyPrototype.Certificate21.required_origin_673_i8 line 560
  247. theorem OAI.SnakyPrototype.Certificate21.required_exact_673_i8 line 562
  248. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_673_i8 line 566
  249. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_673_i8 line 568
  250. def OAI.SnakyPrototype.Certificate21.checked_673_i8 line 572
  251. def OAI.SnakyPrototype.Certificate21.height_673_i7 line 580
  252. def OAI.SnakyPrototype.Certificate21.childrenH_673_i7 line 581
  253. theorem OAI.SnakyPrototype.Certificate21.height_exact_673_i7 line 582
  254. theorem OAI.SnakyPrototype.Certificate21.required_origin_673_i7 line 583
  255. theorem OAI.SnakyPrototype.Certificate21.required_exact_673_i7 line 585
  256. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_673_i7 line 589
  257. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_673_i7 line 591
  258. def OAI.SnakyPrototype.Certificate21.checked_673_i7 line 595
  259. def OAI.SnakyPrototype.Certificate21.height_673 line 603
  260. def OAI.SnakyPrototype.Certificate21.childrenH_673 line 604
  261. theorem OAI.SnakyPrototype.Certificate21.height_exact_673 line 605
  262. theorem OAI.SnakyPrototype.Certificate21.required_origin_673 line 606
  263. theorem OAI.SnakyPrototype.Certificate21.required_exact_673 line 608
  264. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_673 line 612
  265. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_673 line 614
  266. def OAI.SnakyPrototype.Certificate21.checked_673 line 618
  267. def OAI.SnakyPrototype.Certificate21.height_686_i0 line 626
  268. def OAI.SnakyPrototype.Certificate21.childrenH_686_i0 line 627
  269. theorem OAI.SnakyPrototype.Certificate21.height_exact_686_i0 line 628
  270. theorem OAI.SnakyPrototype.Certificate21.required_origin_686_i0 line 629
  271. theorem OAI.SnakyPrototype.Certificate21.required_exact_686_i0 line 631
  272. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_686_i0 line 635
  273. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_686_i0 line 637
  274. def OAI.SnakyPrototype.Certificate21.checked_686_i0 line 641
  275. def OAI.SnakyPrototype.Certificate21.height_686_i1 line 649
  276. def OAI.SnakyPrototype.Certificate21.childrenH_686_i1 line 650
  277. theorem OAI.SnakyPrototype.Certificate21.height_exact_686_i1 line 651
  278. theorem OAI.SnakyPrototype.Certificate21.required_origin_686_i1 line 652
  279. theorem OAI.SnakyPrototype.Certificate21.required_exact_686_i1 line 654
  280. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_686_i1 line 658
  281. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_686_i1 line 660
  282. def OAI.SnakyPrototype.Certificate21.checked_686_i1 line 664
  283. def OAI.SnakyPrototype.Certificate21.height_686 line 672
  284. def OAI.SnakyPrototype.Certificate21.childrenH_686 line 673
  285. theorem OAI.SnakyPrototype.Certificate21.height_exact_686 line 674
  286. theorem OAI.SnakyPrototype.Certificate21.required_origin_686 line 675
  287. theorem OAI.SnakyPrototype.Certificate21.required_exact_686 line 677
  288. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_686 line 681
  289. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_686 line 683
  290. def OAI.SnakyPrototype.Certificate21.checked_686 line 687
  291. def OAI.SnakyPrototype.Certificate21.height_688_i0 line 695
  292. def OAI.SnakyPrototype.Certificate21.childrenH_688_i0 line 696
  293. theorem OAI.SnakyPrototype.Certificate21.height_exact_688_i0 line 697
  294. theorem OAI.SnakyPrototype.Certificate21.required_origin_688_i0 line 698
  295. theorem OAI.SnakyPrototype.Certificate21.required_exact_688_i0 line 700
  296. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_688_i0 line 704
  297. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_688_i0 line 706
  298. def OAI.SnakyPrototype.Certificate21.checked_688_i0 line 710
  299. def OAI.SnakyPrototype.Certificate21.height_688 line 718
  300. def OAI.SnakyPrototype.Certificate21.childrenH_688 line 719
  301. theorem OAI.SnakyPrototype.Certificate21.height_exact_688 line 720
  302. theorem OAI.SnakyPrototype.Certificate21.required_origin_688 line 721
  303. theorem OAI.SnakyPrototype.Certificate21.required_exact_688 line 723
  304. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_688 line 727
  305. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_688 line 729
  306. def OAI.SnakyPrototype.Certificate21.checked_688 line 733