OAI/GameTheory/SnakyTwentyOne/Cards/Height13Part04.lean

GitHub source file

288 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_650_i0 line 30
  2. def OAI.SnakyPrototype.Certificate21.envelope_650_i0 line 31
  3. def OAI.SnakyPrototype.Certificate21.childrenC_650_i0 line 32
  4. def OAI.SnakyPrototype.Certificate21.childrenD_650_i0 line 33
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_650_i0 line 34
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_650_i0 line 35
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_650_i0 line 36
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_650_i0 line 37
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_650_i0 line 38
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_650_i0 line 43
  11. def OAI.SnakyPrototype.Certificate21.required_650 line 48
  12. def OAI.SnakyPrototype.Certificate21.envelope_650 line 49
  13. def OAI.SnakyPrototype.Certificate21.childrenC_650 line 50
  14. def OAI.SnakyPrototype.Certificate21.childrenD_650 line 51
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_650 line 52
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_650 line 53
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_650 line 54
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_650 line 55
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_650 line 56
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_650 line 66
  21. def OAI.SnakyPrototype.Certificate21.required_657_i1 line 71
  22. def OAI.SnakyPrototype.Certificate21.envelope_657_i1 line 72
  23. def OAI.SnakyPrototype.Certificate21.childrenC_657_i1 line 73
  24. def OAI.SnakyPrototype.Certificate21.childrenD_657_i1 line 74
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_657_i1 line 75
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_657_i1 line 76
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_657_i1 line 77
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_657_i1 line 78
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_657_i1 line 79
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_657_i1 line 84
  31. def OAI.SnakyPrototype.Certificate21.required_657_i2 line 89
  32. def OAI.SnakyPrototype.Certificate21.envelope_657_i2 line 90
  33. def OAI.SnakyPrototype.Certificate21.childrenC_657_i2 line 91
  34. def OAI.SnakyPrototype.Certificate21.childrenD_657_i2 line 92
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_657_i2 line 93
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_657_i2 line 94
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_657_i2 line 95
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_657_i2 line 96
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_657_i2 line 97
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_657_i2 line 103
  41. def OAI.SnakyPrototype.Certificate21.required_657_i6 line 108
  42. def OAI.SnakyPrototype.Certificate21.envelope_657_i6 line 109
  43. def OAI.SnakyPrototype.Certificate21.childrenC_657_i6 line 110
  44. def OAI.SnakyPrototype.Certificate21.childrenD_657_i6 line 111
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_657_i6 line 112
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_657_i6 line 113
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_657_i6 line 114
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_657_i6 line 115
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_657_i6 line 116
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_657_i6 line 121
  51. def OAI.SnakyPrototype.Certificate21.required_657_i5 line 126
  52. def OAI.SnakyPrototype.Certificate21.envelope_657_i5 line 127
  53. def OAI.SnakyPrototype.Certificate21.childrenC_657_i5 line 128
  54. def OAI.SnakyPrototype.Certificate21.childrenD_657_i5 line 129
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_657_i5 line 130
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_657_i5 line 131
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_657_i5 line 132
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_657_i5 line 133
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_657_i5 line 134
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_657_i5 line 140
  61. def OAI.SnakyPrototype.Certificate21.required_657_i4 line 145
  62. def OAI.SnakyPrototype.Certificate21.envelope_657_i4 line 146
  63. def OAI.SnakyPrototype.Certificate21.childrenC_657_i4 line 147
  64. def OAI.SnakyPrototype.Certificate21.childrenD_657_i4 line 148
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_657_i4 line 149
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_657_i4 line 150
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_657_i4 line 151
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_657_i4 line 152
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_657_i4 line 153
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_657_i4 line 159
  71. def OAI.SnakyPrototype.Certificate21.required_657_i3 line 164
  72. def OAI.SnakyPrototype.Certificate21.envelope_657_i3 line 165
  73. def OAI.SnakyPrototype.Certificate21.childrenC_657_i3 line 166
  74. def OAI.SnakyPrototype.Certificate21.childrenD_657_i3 line 167
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_657_i3 line 168
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_657_i3 line 169
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_657_i3 line 170
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_657_i3 line 171
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_657_i3 line 172
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_657_i3 line 180
  81. def OAI.SnakyPrototype.Certificate21.required_657_i0 line 185
  82. def OAI.SnakyPrototype.Certificate21.envelope_657_i0 line 186
  83. def OAI.SnakyPrototype.Certificate21.childrenC_657_i0 line 187
  84. def OAI.SnakyPrototype.Certificate21.childrenD_657_i0 line 188
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_657_i0 line 189
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_657_i0 line 190
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_657_i0 line 191
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_657_i0 line 192
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_657_i0 line 193
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_657_i0 line 202
  91. def OAI.SnakyPrototype.Certificate21.required_657 line 207
  92. def OAI.SnakyPrototype.Certificate21.envelope_657 line 208
  93. def OAI.SnakyPrototype.Certificate21.childrenC_657 line 209
  94. def OAI.SnakyPrototype.Certificate21.childrenD_657 line 210
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_657 line 211
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_657 line 212
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_657 line 213
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_657 line 214
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_657 line 215
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_657 line 223
  101. def OAI.SnakyPrototype.Certificate21.required_665_i0 line 228
  102. def OAI.SnakyPrototype.Certificate21.envelope_665_i0 line 229
  103. def OAI.SnakyPrototype.Certificate21.childrenC_665_i0 line 230
  104. def OAI.SnakyPrototype.Certificate21.childrenD_665_i0 line 231
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_665_i0 line 232
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_665_i0 line 233
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_665_i0 line 234
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_665_i0 line 235
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_665_i0 line 236
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_665_i0 line 243
  111. def OAI.SnakyPrototype.Certificate21.required_665_i1 line 248
  112. def OAI.SnakyPrototype.Certificate21.envelope_665_i1 line 249
  113. def OAI.SnakyPrototype.Certificate21.childrenC_665_i1 line 250
  114. def OAI.SnakyPrototype.Certificate21.childrenD_665_i1 line 251
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_665_i1 line 252
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_665_i1 line 253
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_665_i1 line 254
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_665_i1 line 255
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_665_i1 line 256
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_665_i1 line 262
  121. def OAI.SnakyPrototype.Certificate21.required_665_i4 line 267
  122. def OAI.SnakyPrototype.Certificate21.envelope_665_i4 line 268
  123. def OAI.SnakyPrototype.Certificate21.childrenC_665_i4 line 269
  124. def OAI.SnakyPrototype.Certificate21.childrenD_665_i4 line 270
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_665_i4 line 271
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_665_i4 line 272
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_665_i4 line 273
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_665_i4 line 274
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_665_i4 line 275
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_665_i4 line 280
  131. def OAI.SnakyPrototype.Certificate21.required_665_i3 line 285
  132. def OAI.SnakyPrototype.Certificate21.envelope_665_i3 line 286
  133. def OAI.SnakyPrototype.Certificate21.childrenC_665_i3 line 287
  134. def OAI.SnakyPrototype.Certificate21.childrenD_665_i3 line 288
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_665_i3 line 289
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_665_i3 line 290
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_665_i3 line 291
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_665_i3 line 292
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_665_i3 line 293
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_665_i3 line 298
  141. def OAI.SnakyPrototype.Certificate21.required_665_i2 line 303
  142. def OAI.SnakyPrototype.Certificate21.envelope_665_i2 line 304
  143. def OAI.SnakyPrototype.Certificate21.childrenC_665_i2 line 305
  144. def OAI.SnakyPrototype.Certificate21.childrenD_665_i2 line 306
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_665_i2 line 307
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_665_i2 line 308
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_665_i2 line 309
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_665_i2 line 310
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_665_i2 line 311
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_665_i2 line 317
  151. def OAI.SnakyPrototype.Certificate21.required_665 line 322
  152. def OAI.SnakyPrototype.Certificate21.envelope_665 line 323
  153. def OAI.SnakyPrototype.Certificate21.childrenC_665 line 324
  154. def OAI.SnakyPrototype.Certificate21.childrenD_665 line 325
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_665 line 326
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_665 line 327
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_665 line 328
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_665 line 329
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_665 line 330
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_665 line 338
  161. def OAI.SnakyPrototype.Certificate21.height_650_i0 line 343
  162. def OAI.SnakyPrototype.Certificate21.childrenH_650_i0 line 344
  163. theorem OAI.SnakyPrototype.Certificate21.height_exact_650_i0 line 345
  164. theorem OAI.SnakyPrototype.Certificate21.required_origin_650_i0 line 346
  165. theorem OAI.SnakyPrototype.Certificate21.required_exact_650_i0 line 348
  166. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_650_i0 line 352
  167. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_650_i0 line 354
  168. def OAI.SnakyPrototype.Certificate21.checked_650_i0 line 358
  169. def OAI.SnakyPrototype.Certificate21.height_650 line 366
  170. def OAI.SnakyPrototype.Certificate21.childrenH_650 line 367
  171. theorem OAI.SnakyPrototype.Certificate21.height_exact_650 line 368
  172. theorem OAI.SnakyPrototype.Certificate21.required_origin_650 line 369
  173. theorem OAI.SnakyPrototype.Certificate21.required_exact_650 line 371
  174. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_650 line 375
  175. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_650 line 377
  176. def OAI.SnakyPrototype.Certificate21.checked_650 line 381
  177. def OAI.SnakyPrototype.Certificate21.height_657_i1 line 389
  178. def OAI.SnakyPrototype.Certificate21.childrenH_657_i1 line 390
  179. theorem OAI.SnakyPrototype.Certificate21.height_exact_657_i1 line 391
  180. theorem OAI.SnakyPrototype.Certificate21.required_origin_657_i1 line 392
  181. theorem OAI.SnakyPrototype.Certificate21.required_exact_657_i1 line 394
  182. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_657_i1 line 398
  183. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_657_i1 line 400
  184. def OAI.SnakyPrototype.Certificate21.checked_657_i1 line 404
  185. def OAI.SnakyPrototype.Certificate21.height_657_i2 line 412
  186. def OAI.SnakyPrototype.Certificate21.childrenH_657_i2 line 413
  187. theorem OAI.SnakyPrototype.Certificate21.height_exact_657_i2 line 414
  188. theorem OAI.SnakyPrototype.Certificate21.required_origin_657_i2 line 415
  189. theorem OAI.SnakyPrototype.Certificate21.required_exact_657_i2 line 417
  190. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_657_i2 line 421
  191. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_657_i2 line 423
  192. def OAI.SnakyPrototype.Certificate21.checked_657_i2 line 427
  193. def OAI.SnakyPrototype.Certificate21.height_657_i6 line 435
  194. def OAI.SnakyPrototype.Certificate21.childrenH_657_i6 line 436
  195. theorem OAI.SnakyPrototype.Certificate21.height_exact_657_i6 line 437
  196. theorem OAI.SnakyPrototype.Certificate21.required_origin_657_i6 line 438
  197. theorem OAI.SnakyPrototype.Certificate21.required_exact_657_i6 line 440
  198. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_657_i6 line 444
  199. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_657_i6 line 446
  200. def OAI.SnakyPrototype.Certificate21.checked_657_i6 line 450
  201. def OAI.SnakyPrototype.Certificate21.height_657_i5 line 458
  202. def OAI.SnakyPrototype.Certificate21.childrenH_657_i5 line 459
  203. theorem OAI.SnakyPrototype.Certificate21.height_exact_657_i5 line 460
  204. theorem OAI.SnakyPrototype.Certificate21.required_origin_657_i5 line 461
  205. theorem OAI.SnakyPrototype.Certificate21.required_exact_657_i5 line 463
  206. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_657_i5 line 467
  207. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_657_i5 line 469
  208. def OAI.SnakyPrototype.Certificate21.checked_657_i5 line 473
  209. def OAI.SnakyPrototype.Certificate21.height_657_i4 line 481
  210. def OAI.SnakyPrototype.Certificate21.childrenH_657_i4 line 482
  211. theorem OAI.SnakyPrototype.Certificate21.height_exact_657_i4 line 483
  212. theorem OAI.SnakyPrototype.Certificate21.required_origin_657_i4 line 484
  213. theorem OAI.SnakyPrototype.Certificate21.required_exact_657_i4 line 486
  214. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_657_i4 line 490
  215. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_657_i4 line 492
  216. def OAI.SnakyPrototype.Certificate21.checked_657_i4 line 496
  217. def OAI.SnakyPrototype.Certificate21.height_657_i3 line 504
  218. def OAI.SnakyPrototype.Certificate21.childrenH_657_i3 line 505
  219. theorem OAI.SnakyPrototype.Certificate21.height_exact_657_i3 line 506
  220. theorem OAI.SnakyPrototype.Certificate21.required_origin_657_i3 line 507
  221. theorem OAI.SnakyPrototype.Certificate21.required_exact_657_i3 line 509
  222. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_657_i3 line 513
  223. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_657_i3 line 515
  224. def OAI.SnakyPrototype.Certificate21.checked_657_i3 line 519
  225. def OAI.SnakyPrototype.Certificate21.height_657_i0 line 527
  226. def OAI.SnakyPrototype.Certificate21.childrenH_657_i0 line 528
  227. theorem OAI.SnakyPrototype.Certificate21.height_exact_657_i0 line 529
  228. theorem OAI.SnakyPrototype.Certificate21.required_origin_657_i0 line 530
  229. theorem OAI.SnakyPrototype.Certificate21.required_exact_657_i0 line 532
  230. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_657_i0 line 536
  231. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_657_i0 line 538
  232. def OAI.SnakyPrototype.Certificate21.checked_657_i0 line 542
  233. def OAI.SnakyPrototype.Certificate21.height_657 line 550
  234. def OAI.SnakyPrototype.Certificate21.childrenH_657 line 551
  235. theorem OAI.SnakyPrototype.Certificate21.height_exact_657 line 552
  236. theorem OAI.SnakyPrototype.Certificate21.required_origin_657 line 553
  237. theorem OAI.SnakyPrototype.Certificate21.required_exact_657 line 555
  238. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_657 line 559
  239. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_657 line 561
  240. def OAI.SnakyPrototype.Certificate21.checked_657 line 565
  241. def OAI.SnakyPrototype.Certificate21.height_665_i0 line 573
  242. def OAI.SnakyPrototype.Certificate21.childrenH_665_i0 line 574
  243. theorem OAI.SnakyPrototype.Certificate21.height_exact_665_i0 line 575
  244. theorem OAI.SnakyPrototype.Certificate21.required_origin_665_i0 line 576
  245. theorem OAI.SnakyPrototype.Certificate21.required_exact_665_i0 line 578
  246. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_665_i0 line 582
  247. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_665_i0 line 584
  248. def OAI.SnakyPrototype.Certificate21.checked_665_i0 line 588
  249. def OAI.SnakyPrototype.Certificate21.height_665_i1 line 596
  250. def OAI.SnakyPrototype.Certificate21.childrenH_665_i1 line 597
  251. theorem OAI.SnakyPrototype.Certificate21.height_exact_665_i1 line 598
  252. theorem OAI.SnakyPrototype.Certificate21.required_origin_665_i1 line 599
  253. theorem OAI.SnakyPrototype.Certificate21.required_exact_665_i1 line 601
  254. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_665_i1 line 605
  255. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_665_i1 line 607
  256. def OAI.SnakyPrototype.Certificate21.checked_665_i1 line 611
  257. def OAI.SnakyPrototype.Certificate21.height_665_i4 line 619
  258. def OAI.SnakyPrototype.Certificate21.childrenH_665_i4 line 620
  259. theorem OAI.SnakyPrototype.Certificate21.height_exact_665_i4 line 621
  260. theorem OAI.SnakyPrototype.Certificate21.required_origin_665_i4 line 622
  261. theorem OAI.SnakyPrototype.Certificate21.required_exact_665_i4 line 624
  262. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_665_i4 line 628
  263. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_665_i4 line 630
  264. def OAI.SnakyPrototype.Certificate21.checked_665_i4 line 634
  265. def OAI.SnakyPrototype.Certificate21.height_665_i3 line 642
  266. def OAI.SnakyPrototype.Certificate21.childrenH_665_i3 line 643
  267. theorem OAI.SnakyPrototype.Certificate21.height_exact_665_i3 line 644
  268. theorem OAI.SnakyPrototype.Certificate21.required_origin_665_i3 line 645
  269. theorem OAI.SnakyPrototype.Certificate21.required_exact_665_i3 line 647
  270. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_665_i3 line 651
  271. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_665_i3 line 653
  272. def OAI.SnakyPrototype.Certificate21.checked_665_i3 line 657
  273. def OAI.SnakyPrototype.Certificate21.height_665_i2 line 665
  274. def OAI.SnakyPrototype.Certificate21.childrenH_665_i2 line 666
  275. theorem OAI.SnakyPrototype.Certificate21.height_exact_665_i2 line 667
  276. theorem OAI.SnakyPrototype.Certificate21.required_origin_665_i2 line 668
  277. theorem OAI.SnakyPrototype.Certificate21.required_exact_665_i2 line 670
  278. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_665_i2 line 674
  279. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_665_i2 line 676
  280. def OAI.SnakyPrototype.Certificate21.checked_665_i2 line 680
  281. def OAI.SnakyPrototype.Certificate21.height_665 line 688
  282. def OAI.SnakyPrototype.Certificate21.childrenH_665 line 689
  283. theorem OAI.SnakyPrototype.Certificate21.height_exact_665 line 690
  284. theorem OAI.SnakyPrototype.Certificate21.required_origin_665 line 691
  285. theorem OAI.SnakyPrototype.Certificate21.required_exact_665 line 693
  286. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_665 line 697
  287. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_665 line 699
  288. def OAI.SnakyPrototype.Certificate21.checked_665 line 703