OAI/GameTheory/SnakyTwentyOne/Cards/Height10Part03.lean

GitHub source file

414 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_546_i4 line 26
  2. def OAI.SnakyPrototype.Certificate21.envelope_546_i4 line 27
  3. def OAI.SnakyPrototype.Certificate21.childrenC_546_i4 line 28
  4. def OAI.SnakyPrototype.Certificate21.childrenD_546_i4 line 29
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_546_i4 line 30
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_546_i4 line 31
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_546_i4 line 32
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_546_i4 line 33
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_546_i4 line 34
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_546_i4 line 40
  11. def OAI.SnakyPrototype.Certificate21.required_546_i3 line 45
  12. def OAI.SnakyPrototype.Certificate21.envelope_546_i3 line 46
  13. def OAI.SnakyPrototype.Certificate21.childrenC_546_i3 line 47
  14. def OAI.SnakyPrototype.Certificate21.childrenD_546_i3 line 48
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_546_i3 line 49
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_546_i3 line 50
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_546_i3 line 51
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_546_i3 line 52
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_546_i3 line 53
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_546_i3 line 58
  21. def OAI.SnakyPrototype.Certificate21.required_546_i2 line 63
  22. def OAI.SnakyPrototype.Certificate21.envelope_546_i2 line 64
  23. def OAI.SnakyPrototype.Certificate21.childrenC_546_i2 line 65
  24. def OAI.SnakyPrototype.Certificate21.childrenD_546_i2 line 66
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_546_i2 line 67
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_546_i2 line 68
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_546_i2 line 69
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_546_i2 line 70
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_546_i2 line 71
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_546_i2 line 76
  31. def OAI.SnakyPrototype.Certificate21.required_546_i1 line 81
  32. def OAI.SnakyPrototype.Certificate21.envelope_546_i1 line 82
  33. def OAI.SnakyPrototype.Certificate21.childrenC_546_i1 line 83
  34. def OAI.SnakyPrototype.Certificate21.childrenD_546_i1 line 84
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_546_i1 line 85
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_546_i1 line 86
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_546_i1 line 87
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_546_i1 line 88
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_546_i1 line 89
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_546_i1 line 94
  41. def OAI.SnakyPrototype.Certificate21.required_546_i0 line 99
  42. def OAI.SnakyPrototype.Certificate21.envelope_546_i0 line 100
  43. def OAI.SnakyPrototype.Certificate21.childrenC_546_i0 line 101
  44. def OAI.SnakyPrototype.Certificate21.childrenD_546_i0 line 102
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_546_i0 line 103
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_546_i0 line 104
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_546_i0 line 105
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_546_i0 line 106
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_546_i0 line 107
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_546_i0 line 114
  51. def OAI.SnakyPrototype.Certificate21.required_546 line 119
  52. def OAI.SnakyPrototype.Certificate21.envelope_546 line 120
  53. def OAI.SnakyPrototype.Certificate21.childrenC_546 line 121
  54. def OAI.SnakyPrototype.Certificate21.childrenD_546 line 122
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_546 line 123
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_546 line 124
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_546 line 125
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_546 line 126
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_546 line 127
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_546 line 134
  61. def OAI.SnakyPrototype.Certificate21.required_556_i0 line 139
  62. def OAI.SnakyPrototype.Certificate21.envelope_556_i0 line 140
  63. def OAI.SnakyPrototype.Certificate21.childrenC_556_i0 line 141
  64. def OAI.SnakyPrototype.Certificate21.childrenD_556_i0 line 142
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_556_i0 line 143
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_556_i0 line 144
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_556_i0 line 145
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_556_i0 line 146
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_556_i0 line 147
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_556_i0 line 155
  71. def OAI.SnakyPrototype.Certificate21.required_556 line 160
  72. def OAI.SnakyPrototype.Certificate21.envelope_556 line 161
  73. def OAI.SnakyPrototype.Certificate21.childrenC_556 line 162
  74. def OAI.SnakyPrototype.Certificate21.childrenD_556 line 163
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_556 line 164
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_556 line 165
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_556 line 166
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_556 line 167
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_556 line 168
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_556 line 173
  81. def OAI.SnakyPrototype.Certificate21.required_560_i4 line 178
  82. def OAI.SnakyPrototype.Certificate21.envelope_560_i4 line 179
  83. def OAI.SnakyPrototype.Certificate21.childrenC_560_i4 line 180
  84. def OAI.SnakyPrototype.Certificate21.childrenD_560_i4 line 181
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_560_i4 line 182
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_560_i4 line 183
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_560_i4 line 184
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_560_i4 line 185
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_560_i4 line 186
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_560_i4 line 191
  91. def OAI.SnakyPrototype.Certificate21.required_560_i3 line 196
  92. def OAI.SnakyPrototype.Certificate21.envelope_560_i3 line 197
  93. def OAI.SnakyPrototype.Certificate21.childrenC_560_i3 line 198
  94. def OAI.SnakyPrototype.Certificate21.childrenD_560_i3 line 199
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_560_i3 line 200
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_560_i3 line 201
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_560_i3 line 202
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_560_i3 line 203
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_560_i3 line 204
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_560_i3 line 210
  101. def OAI.SnakyPrototype.Certificate21.required_560_i2 line 215
  102. def OAI.SnakyPrototype.Certificate21.envelope_560_i2 line 216
  103. def OAI.SnakyPrototype.Certificate21.childrenC_560_i2 line 217
  104. def OAI.SnakyPrototype.Certificate21.childrenD_560_i2 line 218
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_560_i2 line 219
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_560_i2 line 220
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_560_i2 line 221
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_560_i2 line 222
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_560_i2 line 223
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_560_i2 line 228
  111. def OAI.SnakyPrototype.Certificate21.required_560_i1 line 233
  112. def OAI.SnakyPrototype.Certificate21.envelope_560_i1 line 234
  113. def OAI.SnakyPrototype.Certificate21.childrenC_560_i1 line 235
  114. def OAI.SnakyPrototype.Certificate21.childrenD_560_i1 line 236
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_560_i1 line 237
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_560_i1 line 238
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_560_i1 line 239
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_560_i1 line 240
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_560_i1 line 241
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_560_i1 line 246
  121. def OAI.SnakyPrototype.Certificate21.required_560_i0 line 251
  122. def OAI.SnakyPrototype.Certificate21.envelope_560_i0 line 252
  123. def OAI.SnakyPrototype.Certificate21.childrenC_560_i0 line 253
  124. def OAI.SnakyPrototype.Certificate21.childrenD_560_i0 line 254
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_560_i0 line 255
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_560_i0 line 256
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_560_i0 line 257
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_560_i0 line 258
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_560_i0 line 259
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_560_i0 line 264
  131. def OAI.SnakyPrototype.Certificate21.required_560_i5 line 269
  132. def OAI.SnakyPrototype.Certificate21.envelope_560_i5 line 270
  133. def OAI.SnakyPrototype.Certificate21.childrenC_560_i5 line 271
  134. def OAI.SnakyPrototype.Certificate21.childrenD_560_i5 line 272
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_560_i5 line 273
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_560_i5 line 274
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_560_i5 line 275
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_560_i5 line 276
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_560_i5 line 277
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_560_i5 line 283
  141. def OAI.SnakyPrototype.Certificate21.required_560 line 288
  142. def OAI.SnakyPrototype.Certificate21.envelope_560 line 289
  143. def OAI.SnakyPrototype.Certificate21.childrenC_560 line 290
  144. def OAI.SnakyPrototype.Certificate21.childrenD_560 line 291
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_560 line 292
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_560 line 293
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_560 line 294
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_560 line 295
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_560 line 296
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_560 line 307
  151. def OAI.SnakyPrototype.Certificate21.required_563_i2 line 312
  152. def OAI.SnakyPrototype.Certificate21.envelope_563_i2 line 313
  153. def OAI.SnakyPrototype.Certificate21.childrenC_563_i2 line 314
  154. def OAI.SnakyPrototype.Certificate21.childrenD_563_i2 line 315
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_563_i2 line 316
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_563_i2 line 317
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_563_i2 line 318
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_563_i2 line 319
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_563_i2 line 320
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_563_i2 line 325
  161. def OAI.SnakyPrototype.Certificate21.required_563_i1 line 330
  162. def OAI.SnakyPrototype.Certificate21.envelope_563_i1 line 331
  163. def OAI.SnakyPrototype.Certificate21.childrenC_563_i1 line 332
  164. def OAI.SnakyPrototype.Certificate21.childrenD_563_i1 line 333
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_563_i1 line 334
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_563_i1 line 335
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_563_i1 line 336
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_563_i1 line 337
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_563_i1 line 338
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_563_i1 line 343
  171. def OAI.SnakyPrototype.Certificate21.required_563_i6 line 348
  172. def OAI.SnakyPrototype.Certificate21.envelope_563_i6 line 349
  173. def OAI.SnakyPrototype.Certificate21.childrenC_563_i6 line 350
  174. def OAI.SnakyPrototype.Certificate21.childrenD_563_i6 line 351
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_563_i6 line 352
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_563_i6 line 353
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_563_i6 line 354
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_563_i6 line 355
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_563_i6 line 356
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_563_i6 line 361
  181. def OAI.SnakyPrototype.Certificate21.required_563_i5 line 366
  182. def OAI.SnakyPrototype.Certificate21.envelope_563_i5 line 367
  183. def OAI.SnakyPrototype.Certificate21.childrenC_563_i5 line 368
  184. def OAI.SnakyPrototype.Certificate21.childrenD_563_i5 line 369
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_563_i5 line 370
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_563_i5 line 371
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_563_i5 line 372
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_563_i5 line 373
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_563_i5 line 374
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_563_i5 line 379
  191. def OAI.SnakyPrototype.Certificate21.required_563_i4 line 384
  192. def OAI.SnakyPrototype.Certificate21.envelope_563_i4 line 385
  193. def OAI.SnakyPrototype.Certificate21.childrenC_563_i4 line 386
  194. def OAI.SnakyPrototype.Certificate21.childrenD_563_i4 line 387
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_563_i4 line 388
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_563_i4 line 389
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_563_i4 line 390
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_563_i4 line 391
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_563_i4 line 392
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_563_i4 line 397
  201. def OAI.SnakyPrototype.Certificate21.required_563_i3 line 402
  202. def OAI.SnakyPrototype.Certificate21.envelope_563_i3 line 403
  203. def OAI.SnakyPrototype.Certificate21.childrenC_563_i3 line 404
  204. def OAI.SnakyPrototype.Certificate21.childrenD_563_i3 line 405
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_563_i3 line 406
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_563_i3 line 407
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_563_i3 line 408
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_563_i3 line 409
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_563_i3 line 410
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_563_i3 line 415
  211. def OAI.SnakyPrototype.Certificate21.required_563_i0 line 420
  212. def OAI.SnakyPrototype.Certificate21.envelope_563_i0 line 421
  213. def OAI.SnakyPrototype.Certificate21.childrenC_563_i0 line 422
  214. def OAI.SnakyPrototype.Certificate21.childrenD_563_i0 line 423
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_563_i0 line 424
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_563_i0 line 425
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_563_i0 line 426
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_563_i0 line 427
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_563_i0 line 428
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_563_i0 line 434
  221. def OAI.SnakyPrototype.Certificate21.required_563 line 439
  222. def OAI.SnakyPrototype.Certificate21.envelope_563 line 440
  223. def OAI.SnakyPrototype.Certificate21.childrenC_563 line 441
  224. def OAI.SnakyPrototype.Certificate21.childrenD_563 line 442
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_563 line 443
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_563 line 444
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_563 line 445
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_563 line 446
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_563 line 447
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_563 line 458
  231. def OAI.SnakyPrototype.Certificate21.height_546_i4 line 463
  232. def OAI.SnakyPrototype.Certificate21.childrenH_546_i4 line 464
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_546_i4 line 465
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_546_i4 line 466
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_546_i4 line 468
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_546_i4 line 472
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_546_i4 line 474
  238. def OAI.SnakyPrototype.Certificate21.checked_546_i4 line 478
  239. def OAI.SnakyPrototype.Certificate21.height_546_i3 line 486
  240. def OAI.SnakyPrototype.Certificate21.childrenH_546_i3 line 487
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_546_i3 line 488
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_546_i3 line 489
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_546_i3 line 491
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_546_i3 line 495
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_546_i3 line 497
  246. def OAI.SnakyPrototype.Certificate21.checked_546_i3 line 501
  247. def OAI.SnakyPrototype.Certificate21.height_546_i2 line 509
  248. def OAI.SnakyPrototype.Certificate21.childrenH_546_i2 line 510
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_546_i2 line 511
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_546_i2 line 512
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_546_i2 line 514
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_546_i2 line 518
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_546_i2 line 520
  254. def OAI.SnakyPrototype.Certificate21.checked_546_i2 line 524
  255. def OAI.SnakyPrototype.Certificate21.height_546_i1 line 532
  256. def OAI.SnakyPrototype.Certificate21.childrenH_546_i1 line 533
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_546_i1 line 534
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_546_i1 line 535
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_546_i1 line 537
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_546_i1 line 541
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_546_i1 line 543
  262. def OAI.SnakyPrototype.Certificate21.checked_546_i1 line 547
  263. def OAI.SnakyPrototype.Certificate21.height_546_i0 line 555
  264. def OAI.SnakyPrototype.Certificate21.childrenH_546_i0 line 556
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_546_i0 line 557
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_546_i0 line 558
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_546_i0 line 560
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_546_i0 line 564
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_546_i0 line 566
  270. def OAI.SnakyPrototype.Certificate21.checked_546_i0 line 570
  271. def OAI.SnakyPrototype.Certificate21.height_546 line 578
  272. def OAI.SnakyPrototype.Certificate21.childrenH_546 line 579
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_546 line 580
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_546 line 581
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_546 line 583
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_546 line 587
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_546 line 589
  278. def OAI.SnakyPrototype.Certificate21.checked_546 line 593
  279. def OAI.SnakyPrototype.Certificate21.height_556_i0 line 601
  280. def OAI.SnakyPrototype.Certificate21.childrenH_556_i0 line 602
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_556_i0 line 603
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_556_i0 line 604
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_556_i0 line 606
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_556_i0 line 610
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_556_i0 line 612
  286. def OAI.SnakyPrototype.Certificate21.checked_556_i0 line 616
  287. def OAI.SnakyPrototype.Certificate21.height_556 line 624
  288. def OAI.SnakyPrototype.Certificate21.childrenH_556 line 625
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_556 line 626
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_556 line 627
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_556 line 629
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_556 line 633
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_556 line 635
  294. def OAI.SnakyPrototype.Certificate21.checked_556 line 639
  295. def OAI.SnakyPrototype.Certificate21.height_560_i4 line 647
  296. def OAI.SnakyPrototype.Certificate21.childrenH_560_i4 line 648
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_560_i4 line 649
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_560_i4 line 650
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_560_i4 line 652
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_560_i4 line 656
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_560_i4 line 658
  302. def OAI.SnakyPrototype.Certificate21.checked_560_i4 line 662
  303. def OAI.SnakyPrototype.Certificate21.height_560_i3 line 670
  304. def OAI.SnakyPrototype.Certificate21.childrenH_560_i3 line 671
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_560_i3 line 672
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_560_i3 line 673
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_560_i3 line 675
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_560_i3 line 679
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_560_i3 line 681
  310. def OAI.SnakyPrototype.Certificate21.checked_560_i3 line 685
  311. def OAI.SnakyPrototype.Certificate21.height_560_i2 line 693
  312. def OAI.SnakyPrototype.Certificate21.childrenH_560_i2 line 694
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_560_i2 line 695
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_560_i2 line 696
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_560_i2 line 698
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_560_i2 line 702
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_560_i2 line 704
  318. def OAI.SnakyPrototype.Certificate21.checked_560_i2 line 708
  319. def OAI.SnakyPrototype.Certificate21.height_560_i1 line 716
  320. def OAI.SnakyPrototype.Certificate21.childrenH_560_i1 line 717
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_560_i1 line 718
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_560_i1 line 719
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_560_i1 line 721
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_560_i1 line 725
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_560_i1 line 727
  326. def OAI.SnakyPrototype.Certificate21.checked_560_i1 line 731
  327. def OAI.SnakyPrototype.Certificate21.height_560_i0 line 739
  328. def OAI.SnakyPrototype.Certificate21.childrenH_560_i0 line 740
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_560_i0 line 741
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_560_i0 line 742
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_560_i0 line 744
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_560_i0 line 748
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_560_i0 line 750
  334. def OAI.SnakyPrototype.Certificate21.checked_560_i0 line 754
  335. def OAI.SnakyPrototype.Certificate21.height_560_i5 line 762
  336. def OAI.SnakyPrototype.Certificate21.childrenH_560_i5 line 763
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_560_i5 line 764
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_560_i5 line 765
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_560_i5 line 767
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_560_i5 line 771
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_560_i5 line 773
  342. def OAI.SnakyPrototype.Certificate21.checked_560_i5 line 777
  343. def OAI.SnakyPrototype.Certificate21.height_560 line 785
  344. def OAI.SnakyPrototype.Certificate21.childrenH_560 line 786
  345. theorem OAI.SnakyPrototype.Certificate21.height_exact_560 line 787
  346. theorem OAI.SnakyPrototype.Certificate21.required_origin_560 line 788
  347. theorem OAI.SnakyPrototype.Certificate21.required_exact_560 line 790
  348. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_560 line 794
  349. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_560 line 796
  350. def OAI.SnakyPrototype.Certificate21.checked_560 line 800
  351. def OAI.SnakyPrototype.Certificate21.height_563_i2 line 808
  352. def OAI.SnakyPrototype.Certificate21.childrenH_563_i2 line 809
  353. theorem OAI.SnakyPrototype.Certificate21.height_exact_563_i2 line 810
  354. theorem OAI.SnakyPrototype.Certificate21.required_origin_563_i2 line 811
  355. theorem OAI.SnakyPrototype.Certificate21.required_exact_563_i2 line 813
  356. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_563_i2 line 817
  357. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_563_i2 line 819
  358. def OAI.SnakyPrototype.Certificate21.checked_563_i2 line 823
  359. def OAI.SnakyPrototype.Certificate21.height_563_i1 line 831
  360. def OAI.SnakyPrototype.Certificate21.childrenH_563_i1 line 832
  361. theorem OAI.SnakyPrototype.Certificate21.height_exact_563_i1 line 833
  362. theorem OAI.SnakyPrototype.Certificate21.required_origin_563_i1 line 834
  363. theorem OAI.SnakyPrototype.Certificate21.required_exact_563_i1 line 836
  364. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_563_i1 line 840
  365. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_563_i1 line 842
  366. def OAI.SnakyPrototype.Certificate21.checked_563_i1 line 846
  367. def OAI.SnakyPrototype.Certificate21.height_563_i6 line 854
  368. def OAI.SnakyPrototype.Certificate21.childrenH_563_i6 line 855
  369. theorem OAI.SnakyPrototype.Certificate21.height_exact_563_i6 line 856
  370. theorem OAI.SnakyPrototype.Certificate21.required_origin_563_i6 line 857
  371. theorem OAI.SnakyPrototype.Certificate21.required_exact_563_i6 line 859
  372. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_563_i6 line 863
  373. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_563_i6 line 865
  374. def OAI.SnakyPrototype.Certificate21.checked_563_i6 line 869
  375. def OAI.SnakyPrototype.Certificate21.height_563_i5 line 877
  376. def OAI.SnakyPrototype.Certificate21.childrenH_563_i5 line 878
  377. theorem OAI.SnakyPrototype.Certificate21.height_exact_563_i5 line 879
  378. theorem OAI.SnakyPrototype.Certificate21.required_origin_563_i5 line 880
  379. theorem OAI.SnakyPrototype.Certificate21.required_exact_563_i5 line 882
  380. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_563_i5 line 886
  381. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_563_i5 line 888
  382. def OAI.SnakyPrototype.Certificate21.checked_563_i5 line 892
  383. def OAI.SnakyPrototype.Certificate21.height_563_i4 line 900
  384. def OAI.SnakyPrototype.Certificate21.childrenH_563_i4 line 901
  385. theorem OAI.SnakyPrototype.Certificate21.height_exact_563_i4 line 902
  386. theorem OAI.SnakyPrototype.Certificate21.required_origin_563_i4 line 903
  387. theorem OAI.SnakyPrototype.Certificate21.required_exact_563_i4 line 905
  388. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_563_i4 line 909
  389. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_563_i4 line 911
  390. def OAI.SnakyPrototype.Certificate21.checked_563_i4 line 915
  391. def OAI.SnakyPrototype.Certificate21.height_563_i3 line 923
  392. def OAI.SnakyPrototype.Certificate21.childrenH_563_i3 line 924
  393. theorem OAI.SnakyPrototype.Certificate21.height_exact_563_i3 line 925
  394. theorem OAI.SnakyPrototype.Certificate21.required_origin_563_i3 line 926
  395. theorem OAI.SnakyPrototype.Certificate21.required_exact_563_i3 line 928
  396. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_563_i3 line 932
  397. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_563_i3 line 934
  398. def OAI.SnakyPrototype.Certificate21.checked_563_i3 line 938
  399. def OAI.SnakyPrototype.Certificate21.height_563_i0 line 946
  400. def OAI.SnakyPrototype.Certificate21.childrenH_563_i0 line 947
  401. theorem OAI.SnakyPrototype.Certificate21.height_exact_563_i0 line 948
  402. theorem OAI.SnakyPrototype.Certificate21.required_origin_563_i0 line 949
  403. theorem OAI.SnakyPrototype.Certificate21.required_exact_563_i0 line 951
  404. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_563_i0 line 955
  405. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_563_i0 line 957
  406. def OAI.SnakyPrototype.Certificate21.checked_563_i0 line 961
  407. def OAI.SnakyPrototype.Certificate21.height_563 line 969
  408. def OAI.SnakyPrototype.Certificate21.childrenH_563 line 970
  409. theorem OAI.SnakyPrototype.Certificate21.height_exact_563 line 971
  410. theorem OAI.SnakyPrototype.Certificate21.required_origin_563 line 972
  411. theorem OAI.SnakyPrototype.Certificate21.required_exact_563 line 974
  412. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_563 line 978
  413. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_563 line 980
  414. def OAI.SnakyPrototype.Certificate21.checked_563 line 984