OAI/GameTheory/SnakyTwentyOne/Cards/Height11Part03.lean

GitHub source file

324 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_596_i1 line 22
  2. def OAI.SnakyPrototype.Certificate21.envelope_596_i1 line 23
  3. def OAI.SnakyPrototype.Certificate21.childrenC_596_i1 line 24
  4. def OAI.SnakyPrototype.Certificate21.childrenD_596_i1 line 25
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_596_i1 line 26
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_596_i1 line 27
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_596_i1 line 28
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_596_i1 line 29
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_596_i1 line 30
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_596_i1 line 35
  11. def OAI.SnakyPrototype.Certificate21.required_596_i0 line 40
  12. def OAI.SnakyPrototype.Certificate21.envelope_596_i0 line 41
  13. def OAI.SnakyPrototype.Certificate21.childrenC_596_i0 line 42
  14. def OAI.SnakyPrototype.Certificate21.childrenD_596_i0 line 43
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_596_i0 line 44
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_596_i0 line 45
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_596_i0 line 46
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_596_i0 line 47
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_596_i0 line 48
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_596_i0 line 53
  21. def OAI.SnakyPrototype.Certificate21.required_596_i3 line 58
  22. def OAI.SnakyPrototype.Certificate21.envelope_596_i3 line 59
  23. def OAI.SnakyPrototype.Certificate21.childrenC_596_i3 line 60
  24. def OAI.SnakyPrototype.Certificate21.childrenD_596_i3 line 61
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_596_i3 line 62
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_596_i3 line 63
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_596_i3 line 64
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_596_i3 line 65
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_596_i3 line 66
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_596_i3 line 71
  31. def OAI.SnakyPrototype.Certificate21.required_596_i2 line 76
  32. def OAI.SnakyPrototype.Certificate21.envelope_596_i2 line 77
  33. def OAI.SnakyPrototype.Certificate21.childrenC_596_i2 line 78
  34. def OAI.SnakyPrototype.Certificate21.childrenD_596_i2 line 79
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_596_i2 line 80
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_596_i2 line 81
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_596_i2 line 82
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_596_i2 line 83
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_596_i2 line 84
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_596_i2 line 89
  41. def OAI.SnakyPrototype.Certificate21.required_596_i5 line 94
  42. def OAI.SnakyPrototype.Certificate21.envelope_596_i5 line 95
  43. def OAI.SnakyPrototype.Certificate21.childrenC_596_i5 line 96
  44. def OAI.SnakyPrototype.Certificate21.childrenD_596_i5 line 97
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_596_i5 line 98
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_596_i5 line 99
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_596_i5 line 100
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_596_i5 line 101
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_596_i5 line 102
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_596_i5 line 107
  51. def OAI.SnakyPrototype.Certificate21.required_596_i4 line 112
  52. def OAI.SnakyPrototype.Certificate21.envelope_596_i4 line 113
  53. def OAI.SnakyPrototype.Certificate21.childrenC_596_i4 line 114
  54. def OAI.SnakyPrototype.Certificate21.childrenD_596_i4 line 115
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_596_i4 line 116
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_596_i4 line 117
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_596_i4 line 118
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_596_i4 line 119
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_596_i4 line 120
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_596_i4 line 126
  61. def OAI.SnakyPrototype.Certificate21.required_596 line 131
  62. def OAI.SnakyPrototype.Certificate21.envelope_596 line 132
  63. def OAI.SnakyPrototype.Certificate21.childrenC_596 line 133
  64. def OAI.SnakyPrototype.Certificate21.childrenD_596 line 134
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_596 line 135
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_596 line 136
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_596 line 137
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_596 line 138
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_596 line 139
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_596 line 146
  71. def OAI.SnakyPrototype.Certificate21.required_601_i1 line 151
  72. def OAI.SnakyPrototype.Certificate21.envelope_601_i1 line 152
  73. def OAI.SnakyPrototype.Certificate21.childrenC_601_i1 line 153
  74. def OAI.SnakyPrototype.Certificate21.childrenD_601_i1 line 154
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_601_i1 line 155
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_601_i1 line 156
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_601_i1 line 157
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_601_i1 line 158
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_601_i1 line 159
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_601_i1 line 164
  81. def OAI.SnakyPrototype.Certificate21.required_601_i0 line 169
  82. def OAI.SnakyPrototype.Certificate21.envelope_601_i0 line 170
  83. def OAI.SnakyPrototype.Certificate21.childrenC_601_i0 line 171
  84. def OAI.SnakyPrototype.Certificate21.childrenD_601_i0 line 172
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_601_i0 line 173
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_601_i0 line 174
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_601_i0 line 175
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_601_i0 line 176
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_601_i0 line 177
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_601_i0 line 183
  91. def OAI.SnakyPrototype.Certificate21.required_601_i6 line 188
  92. def OAI.SnakyPrototype.Certificate21.envelope_601_i6 line 189
  93. def OAI.SnakyPrototype.Certificate21.childrenC_601_i6 line 190
  94. def OAI.SnakyPrototype.Certificate21.childrenD_601_i6 line 191
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_601_i6 line 192
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_601_i6 line 193
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_601_i6 line 194
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_601_i6 line 195
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_601_i6 line 196
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_601_i6 line 201
  101. def OAI.SnakyPrototype.Certificate21.required_601_i5 line 206
  102. def OAI.SnakyPrototype.Certificate21.envelope_601_i5 line 207
  103. def OAI.SnakyPrototype.Certificate21.childrenC_601_i5 line 208
  104. def OAI.SnakyPrototype.Certificate21.childrenD_601_i5 line 209
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_601_i5 line 210
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_601_i5 line 211
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_601_i5 line 212
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_601_i5 line 213
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_601_i5 line 214
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_601_i5 line 219
  111. def OAI.SnakyPrototype.Certificate21.required_601_i4 line 224
  112. def OAI.SnakyPrototype.Certificate21.envelope_601_i4 line 225
  113. def OAI.SnakyPrototype.Certificate21.childrenC_601_i4 line 226
  114. def OAI.SnakyPrototype.Certificate21.childrenD_601_i4 line 227
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_601_i4 line 228
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_601_i4 line 229
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_601_i4 line 230
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_601_i4 line 231
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_601_i4 line 232
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_601_i4 line 237
  121. def OAI.SnakyPrototype.Certificate21.required_601_i3 line 242
  122. def OAI.SnakyPrototype.Certificate21.envelope_601_i3 line 243
  123. def OAI.SnakyPrototype.Certificate21.childrenC_601_i3 line 244
  124. def OAI.SnakyPrototype.Certificate21.childrenD_601_i3 line 245
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_601_i3 line 246
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_601_i3 line 247
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_601_i3 line 248
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_601_i3 line 249
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_601_i3 line 250
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_601_i3 line 255
  131. def OAI.SnakyPrototype.Certificate21.required_601_i7 line 260
  132. def OAI.SnakyPrototype.Certificate21.envelope_601_i7 line 261
  133. def OAI.SnakyPrototype.Certificate21.childrenC_601_i7 line 262
  134. def OAI.SnakyPrototype.Certificate21.childrenD_601_i7 line 263
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_601_i7 line 264
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_601_i7 line 265
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_601_i7 line 266
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_601_i7 line 267
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_601_i7 line 268
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_601_i7 line 273
  141. def OAI.SnakyPrototype.Certificate21.required_601_i2 line 278
  142. def OAI.SnakyPrototype.Certificate21.envelope_601_i2 line 279
  143. def OAI.SnakyPrototype.Certificate21.childrenC_601_i2 line 280
  144. def OAI.SnakyPrototype.Certificate21.childrenD_601_i2 line 281
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_601_i2 line 282
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_601_i2 line 283
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_601_i2 line 284
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_601_i2 line 285
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_601_i2 line 286
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_601_i2 line 294
  151. def OAI.SnakyPrototype.Certificate21.required_601_i8 line 299
  152. def OAI.SnakyPrototype.Certificate21.envelope_601_i8 line 300
  153. def OAI.SnakyPrototype.Certificate21.childrenC_601_i8 line 301
  154. def OAI.SnakyPrototype.Certificate21.childrenD_601_i8 line 302
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_601_i8 line 303
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_601_i8 line 304
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_601_i8 line 305
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_601_i8 line 306
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_601_i8 line 307
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_601_i8 line 312
  161. def OAI.SnakyPrototype.Certificate21.required_601 line 317
  162. def OAI.SnakyPrototype.Certificate21.envelope_601 line 318
  163. def OAI.SnakyPrototype.Certificate21.childrenC_601 line 319
  164. def OAI.SnakyPrototype.Certificate21.childrenD_601 line 320
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_601 line 321
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_601 line 322
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_601 line 323
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_601 line 324
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_601 line 325
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_601 line 332
  171. def OAI.SnakyPrototype.Certificate21.required_613 line 337
  172. def OAI.SnakyPrototype.Certificate21.envelope_613 line 338
  173. def OAI.SnakyPrototype.Certificate21.childrenC_613 line 339
  174. def OAI.SnakyPrototype.Certificate21.childrenD_613 line 340
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_613 line 341
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_613 line 342
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_613 line 343
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_613 line 344
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_613 line 345
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_613 line 354
  181. def OAI.SnakyPrototype.Certificate21.height_596_i1 line 359
  182. def OAI.SnakyPrototype.Certificate21.childrenH_596_i1 line 360
  183. theorem OAI.SnakyPrototype.Certificate21.height_exact_596_i1 line 361
  184. theorem OAI.SnakyPrototype.Certificate21.required_origin_596_i1 line 362
  185. theorem OAI.SnakyPrototype.Certificate21.required_exact_596_i1 line 364
  186. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_596_i1 line 368
  187. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_596_i1 line 370
  188. def OAI.SnakyPrototype.Certificate21.checked_596_i1 line 374
  189. def OAI.SnakyPrototype.Certificate21.height_596_i0 line 382
  190. def OAI.SnakyPrototype.Certificate21.childrenH_596_i0 line 383
  191. theorem OAI.SnakyPrototype.Certificate21.height_exact_596_i0 line 384
  192. theorem OAI.SnakyPrototype.Certificate21.required_origin_596_i0 line 385
  193. theorem OAI.SnakyPrototype.Certificate21.required_exact_596_i0 line 387
  194. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_596_i0 line 391
  195. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_596_i0 line 393
  196. def OAI.SnakyPrototype.Certificate21.checked_596_i0 line 397
  197. def OAI.SnakyPrototype.Certificate21.height_596_i3 line 405
  198. def OAI.SnakyPrototype.Certificate21.childrenH_596_i3 line 406
  199. theorem OAI.SnakyPrototype.Certificate21.height_exact_596_i3 line 407
  200. theorem OAI.SnakyPrototype.Certificate21.required_origin_596_i3 line 408
  201. theorem OAI.SnakyPrototype.Certificate21.required_exact_596_i3 line 410
  202. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_596_i3 line 414
  203. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_596_i3 line 416
  204. def OAI.SnakyPrototype.Certificate21.checked_596_i3 line 420
  205. def OAI.SnakyPrototype.Certificate21.height_596_i2 line 428
  206. def OAI.SnakyPrototype.Certificate21.childrenH_596_i2 line 429
  207. theorem OAI.SnakyPrototype.Certificate21.height_exact_596_i2 line 430
  208. theorem OAI.SnakyPrototype.Certificate21.required_origin_596_i2 line 431
  209. theorem OAI.SnakyPrototype.Certificate21.required_exact_596_i2 line 433
  210. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_596_i2 line 437
  211. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_596_i2 line 439
  212. def OAI.SnakyPrototype.Certificate21.checked_596_i2 line 443
  213. def OAI.SnakyPrototype.Certificate21.height_596_i5 line 451
  214. def OAI.SnakyPrototype.Certificate21.childrenH_596_i5 line 452
  215. theorem OAI.SnakyPrototype.Certificate21.height_exact_596_i5 line 453
  216. theorem OAI.SnakyPrototype.Certificate21.required_origin_596_i5 line 454
  217. theorem OAI.SnakyPrototype.Certificate21.required_exact_596_i5 line 456
  218. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_596_i5 line 460
  219. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_596_i5 line 462
  220. def OAI.SnakyPrototype.Certificate21.checked_596_i5 line 466
  221. def OAI.SnakyPrototype.Certificate21.height_596_i4 line 474
  222. def OAI.SnakyPrototype.Certificate21.childrenH_596_i4 line 475
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_596_i4 line 476
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_596_i4 line 477
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_596_i4 line 479
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_596_i4 line 483
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_596_i4 line 485
  228. def OAI.SnakyPrototype.Certificate21.checked_596_i4 line 489
  229. def OAI.SnakyPrototype.Certificate21.height_596 line 497
  230. def OAI.SnakyPrototype.Certificate21.childrenH_596 line 498
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_596 line 499
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_596 line 500
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_596 line 502
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_596 line 506
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_596 line 508
  236. def OAI.SnakyPrototype.Certificate21.checked_596 line 512
  237. def OAI.SnakyPrototype.Certificate21.height_601_i1 line 520
  238. def OAI.SnakyPrototype.Certificate21.childrenH_601_i1 line 521
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_601_i1 line 522
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_601_i1 line 523
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_601_i1 line 525
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_601_i1 line 529
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_601_i1 line 531
  244. def OAI.SnakyPrototype.Certificate21.checked_601_i1 line 535
  245. def OAI.SnakyPrototype.Certificate21.height_601_i0 line 543
  246. def OAI.SnakyPrototype.Certificate21.childrenH_601_i0 line 544
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_601_i0 line 545
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_601_i0 line 546
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_601_i0 line 548
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_601_i0 line 552
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_601_i0 line 554
  252. def OAI.SnakyPrototype.Certificate21.checked_601_i0 line 558
  253. def OAI.SnakyPrototype.Certificate21.height_601_i6 line 566
  254. def OAI.SnakyPrototype.Certificate21.childrenH_601_i6 line 567
  255. theorem OAI.SnakyPrototype.Certificate21.height_exact_601_i6 line 568
  256. theorem OAI.SnakyPrototype.Certificate21.required_origin_601_i6 line 569
  257. theorem OAI.SnakyPrototype.Certificate21.required_exact_601_i6 line 571
  258. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_601_i6 line 575
  259. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_601_i6 line 577
  260. def OAI.SnakyPrototype.Certificate21.checked_601_i6 line 581
  261. def OAI.SnakyPrototype.Certificate21.height_601_i5 line 589
  262. def OAI.SnakyPrototype.Certificate21.childrenH_601_i5 line 590
  263. theorem OAI.SnakyPrototype.Certificate21.height_exact_601_i5 line 591
  264. theorem OAI.SnakyPrototype.Certificate21.required_origin_601_i5 line 592
  265. theorem OAI.SnakyPrototype.Certificate21.required_exact_601_i5 line 594
  266. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_601_i5 line 598
  267. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_601_i5 line 600
  268. def OAI.SnakyPrototype.Certificate21.checked_601_i5 line 604
  269. def OAI.SnakyPrototype.Certificate21.height_601_i4 line 612
  270. def OAI.SnakyPrototype.Certificate21.childrenH_601_i4 line 613
  271. theorem OAI.SnakyPrototype.Certificate21.height_exact_601_i4 line 614
  272. theorem OAI.SnakyPrototype.Certificate21.required_origin_601_i4 line 615
  273. theorem OAI.SnakyPrototype.Certificate21.required_exact_601_i4 line 617
  274. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_601_i4 line 621
  275. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_601_i4 line 623
  276. def OAI.SnakyPrototype.Certificate21.checked_601_i4 line 627
  277. def OAI.SnakyPrototype.Certificate21.height_601_i3 line 635
  278. def OAI.SnakyPrototype.Certificate21.childrenH_601_i3 line 636
  279. theorem OAI.SnakyPrototype.Certificate21.height_exact_601_i3 line 637
  280. theorem OAI.SnakyPrototype.Certificate21.required_origin_601_i3 line 638
  281. theorem OAI.SnakyPrototype.Certificate21.required_exact_601_i3 line 640
  282. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_601_i3 line 644
  283. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_601_i3 line 646
  284. def OAI.SnakyPrototype.Certificate21.checked_601_i3 line 650
  285. def OAI.SnakyPrototype.Certificate21.height_601_i7 line 658
  286. def OAI.SnakyPrototype.Certificate21.childrenH_601_i7 line 659
  287. theorem OAI.SnakyPrototype.Certificate21.height_exact_601_i7 line 660
  288. theorem OAI.SnakyPrototype.Certificate21.required_origin_601_i7 line 661
  289. theorem OAI.SnakyPrototype.Certificate21.required_exact_601_i7 line 663
  290. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_601_i7 line 667
  291. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_601_i7 line 669
  292. def OAI.SnakyPrototype.Certificate21.checked_601_i7 line 673
  293. def OAI.SnakyPrototype.Certificate21.height_601_i2 line 681
  294. def OAI.SnakyPrototype.Certificate21.childrenH_601_i2 line 682
  295. theorem OAI.SnakyPrototype.Certificate21.height_exact_601_i2 line 683
  296. theorem OAI.SnakyPrototype.Certificate21.required_origin_601_i2 line 684
  297. theorem OAI.SnakyPrototype.Certificate21.required_exact_601_i2 line 686
  298. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_601_i2 line 690
  299. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_601_i2 line 692
  300. def OAI.SnakyPrototype.Certificate21.checked_601_i2 line 696
  301. def OAI.SnakyPrototype.Certificate21.height_601_i8 line 704
  302. def OAI.SnakyPrototype.Certificate21.childrenH_601_i8 line 705
  303. theorem OAI.SnakyPrototype.Certificate21.height_exact_601_i8 line 706
  304. theorem OAI.SnakyPrototype.Certificate21.required_origin_601_i8 line 707
  305. theorem OAI.SnakyPrototype.Certificate21.required_exact_601_i8 line 709
  306. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_601_i8 line 713
  307. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_601_i8 line 715
  308. def OAI.SnakyPrototype.Certificate21.checked_601_i8 line 719
  309. def OAI.SnakyPrototype.Certificate21.height_601 line 727
  310. def OAI.SnakyPrototype.Certificate21.childrenH_601 line 728
  311. theorem OAI.SnakyPrototype.Certificate21.height_exact_601 line 729
  312. theorem OAI.SnakyPrototype.Certificate21.required_origin_601 line 730
  313. theorem OAI.SnakyPrototype.Certificate21.required_exact_601 line 732
  314. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_601 line 736
  315. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_601 line 738
  316. def OAI.SnakyPrototype.Certificate21.checked_601 line 742
  317. def OAI.SnakyPrototype.Certificate21.height_613 line 750
  318. def OAI.SnakyPrototype.Certificate21.childrenH_613 line 751
  319. theorem OAI.SnakyPrototype.Certificate21.height_exact_613 line 752
  320. theorem OAI.SnakyPrototype.Certificate21.required_origin_613 line 753
  321. theorem OAI.SnakyPrototype.Certificate21.required_exact_613 line 755
  322. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_613 line 759
  323. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_613 line 761
  324. def OAI.SnakyPrototype.Certificate21.checked_613 line 765