OAI/GameTheory/SnakyTwentyOne/Cards/Height10Part01.lean

GitHub source file

414 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_399 line 26
  2. def OAI.SnakyPrototype.Certificate21.envelope_399 line 27
  3. def OAI.SnakyPrototype.Certificate21.childrenC_399 line 28
  4. def OAI.SnakyPrototype.Certificate21.childrenD_399 line 29
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_399 line 30
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_399 line 31
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_399 line 32
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_399 line 33
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_399 line 34
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_399 line 42
  11. def OAI.SnakyPrototype.Certificate21.required_401 line 47
  12. def OAI.SnakyPrototype.Certificate21.envelope_401 line 48
  13. def OAI.SnakyPrototype.Certificate21.childrenC_401 line 49
  14. def OAI.SnakyPrototype.Certificate21.childrenD_401 line 50
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_401 line 51
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_401 line 52
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_401 line 53
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_401 line 54
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_401 line 55
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_401 line 60
  21. def OAI.SnakyPrototype.Certificate21.required_408 line 65
  22. def OAI.SnakyPrototype.Certificate21.envelope_408 line 66
  23. def OAI.SnakyPrototype.Certificate21.childrenC_408 line 67
  24. def OAI.SnakyPrototype.Certificate21.childrenD_408 line 68
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_408 line 69
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_408 line 70
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_408 line 71
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_408 line 72
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_408 line 73
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_408 line 79
  31. def OAI.SnakyPrototype.Certificate21.required_409 line 84
  32. def OAI.SnakyPrototype.Certificate21.envelope_409 line 85
  33. def OAI.SnakyPrototype.Certificate21.childrenC_409 line 86
  34. def OAI.SnakyPrototype.Certificate21.childrenD_409 line 87
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_409 line 88
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_409 line 89
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_409 line 90
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_409 line 91
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_409 line 92
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_409 line 98
  41. def OAI.SnakyPrototype.Certificate21.required_410 line 103
  42. def OAI.SnakyPrototype.Certificate21.envelope_410 line 104
  43. def OAI.SnakyPrototype.Certificate21.childrenC_410 line 105
  44. def OAI.SnakyPrototype.Certificate21.childrenD_410 line 106
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_410 line 107
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_410 line 108
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_410 line 109
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_410 line 110
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_410 line 111
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_410 line 118
  51. def OAI.SnakyPrototype.Certificate21.required_411 line 123
  52. def OAI.SnakyPrototype.Certificate21.envelope_411 line 124
  53. def OAI.SnakyPrototype.Certificate21.childrenC_411 line 125
  54. def OAI.SnakyPrototype.Certificate21.childrenD_411 line 126
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_411 line 127
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_411 line 128
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_411 line 129
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_411 line 130
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_411 line 131
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_411 line 137
  61. def OAI.SnakyPrototype.Certificate21.required_444 line 142
  62. def OAI.SnakyPrototype.Certificate21.envelope_444 line 143
  63. def OAI.SnakyPrototype.Certificate21.childrenC_444 line 144
  64. def OAI.SnakyPrototype.Certificate21.childrenD_444 line 145
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_444 line 146
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_444 line 147
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_444 line 148
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_444 line 149
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_444 line 150
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_444 line 157
  71. def OAI.SnakyPrototype.Certificate21.required_459 line 162
  72. def OAI.SnakyPrototype.Certificate21.envelope_459 line 163
  73. def OAI.SnakyPrototype.Certificate21.childrenC_459 line 164
  74. def OAI.SnakyPrototype.Certificate21.childrenD_459 line 165
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_459 line 166
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_459 line 167
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_459 line 168
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_459 line 169
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_459 line 170
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_459 line 181
  81. def OAI.SnakyPrototype.Certificate21.required_460 line 186
  82. def OAI.SnakyPrototype.Certificate21.envelope_460 line 187
  83. def OAI.SnakyPrototype.Certificate21.childrenC_460 line 188
  84. def OAI.SnakyPrototype.Certificate21.childrenD_460 line 189
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_460 line 190
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_460 line 191
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_460 line 192
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_460 line 193
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_460 line 194
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_460 line 202
  91. def OAI.SnakyPrototype.Certificate21.required_461 line 207
  92. def OAI.SnakyPrototype.Certificate21.envelope_461 line 208
  93. def OAI.SnakyPrototype.Certificate21.childrenC_461 line 209
  94. def OAI.SnakyPrototype.Certificate21.childrenD_461 line 210
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_461 line 211
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_461 line 212
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_461 line 213
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_461 line 214
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_461 line 215
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_461 line 222
  101. def OAI.SnakyPrototype.Certificate21.required_475 line 227
  102. def OAI.SnakyPrototype.Certificate21.envelope_475 line 228
  103. def OAI.SnakyPrototype.Certificate21.childrenC_475 line 229
  104. def OAI.SnakyPrototype.Certificate21.childrenD_475 line 230
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_475 line 231
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_475 line 232
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_475 line 233
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_475 line 234
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_475 line 235
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_475 line 243
  111. def OAI.SnakyPrototype.Certificate21.required_476 line 248
  112. def OAI.SnakyPrototype.Certificate21.envelope_476 line 249
  113. def OAI.SnakyPrototype.Certificate21.childrenC_476 line 250
  114. def OAI.SnakyPrototype.Certificate21.childrenD_476 line 251
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_476 line 252
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_476 line 253
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_476 line 254
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_476 line 255
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_476 line 256
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_476 line 264
  121. def OAI.SnakyPrototype.Certificate21.required_479_i0 line 269
  122. def OAI.SnakyPrototype.Certificate21.envelope_479_i0 line 270
  123. def OAI.SnakyPrototype.Certificate21.childrenC_479_i0 line 271
  124. def OAI.SnakyPrototype.Certificate21.childrenD_479_i0 line 272
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_479_i0 line 273
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_479_i0 line 274
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_479_i0 line 275
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_479_i0 line 276
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_479_i0 line 277
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_479_i0 line 282
  131. def OAI.SnakyPrototype.Certificate21.required_479 line 287
  132. def OAI.SnakyPrototype.Certificate21.envelope_479 line 288
  133. def OAI.SnakyPrototype.Certificate21.childrenC_479 line 289
  134. def OAI.SnakyPrototype.Certificate21.childrenD_479 line 290
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_479 line 291
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_479 line 292
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_479 line 293
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_479 line 294
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_479 line 295
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_479 line 305
  141. def OAI.SnakyPrototype.Certificate21.required_480 line 310
  142. def OAI.SnakyPrototype.Certificate21.envelope_480 line 311
  143. def OAI.SnakyPrototype.Certificate21.childrenC_480 line 312
  144. def OAI.SnakyPrototype.Certificate21.childrenD_480 line 313
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_480 line 314
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_480 line 315
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_480 line 316
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_480 line 317
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_480 line 318
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_480 line 328
  151. def OAI.SnakyPrototype.Certificate21.required_481 line 333
  152. def OAI.SnakyPrototype.Certificate21.envelope_481 line 334
  153. def OAI.SnakyPrototype.Certificate21.childrenC_481 line 335
  154. def OAI.SnakyPrototype.Certificate21.childrenD_481 line 336
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_481 line 337
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_481 line 338
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_481 line 339
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_481 line 340
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_481 line 341
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_481 line 349
  161. def OAI.SnakyPrototype.Certificate21.required_483 line 354
  162. def OAI.SnakyPrototype.Certificate21.envelope_483 line 355
  163. def OAI.SnakyPrototype.Certificate21.childrenC_483 line 356
  164. def OAI.SnakyPrototype.Certificate21.childrenD_483 line 357
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_483 line 358
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_483 line 359
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_483 line 360
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_483 line 361
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_483 line 362
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_483 line 370
  171. def OAI.SnakyPrototype.Certificate21.required_491_i0 line 375
  172. def OAI.SnakyPrototype.Certificate21.envelope_491_i0 line 376
  173. def OAI.SnakyPrototype.Certificate21.childrenC_491_i0 line 377
  174. def OAI.SnakyPrototype.Certificate21.childrenD_491_i0 line 378
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_491_i0 line 379
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_491_i0 line 380
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_491_i0 line 381
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_491_i0 line 382
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_491_i0 line 383
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_491_i0 line 390
  181. def OAI.SnakyPrototype.Certificate21.required_491_i1 line 395
  182. def OAI.SnakyPrototype.Certificate21.envelope_491_i1 line 396
  183. def OAI.SnakyPrototype.Certificate21.childrenC_491_i1 line 397
  184. def OAI.SnakyPrototype.Certificate21.childrenD_491_i1 line 398
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_491_i1 line 399
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_491_i1 line 400
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_491_i1 line 401
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_491_i1 line 402
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_491_i1 line 403
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_491_i1 line 409
  191. def OAI.SnakyPrototype.Certificate21.required_491 line 414
  192. def OAI.SnakyPrototype.Certificate21.envelope_491 line 415
  193. def OAI.SnakyPrototype.Certificate21.childrenC_491 line 416
  194. def OAI.SnakyPrototype.Certificate21.childrenD_491 line 417
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_491 line 418
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_491 line 419
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_491 line 420
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_491 line 421
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_491 line 422
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_491 line 429
  201. def OAI.SnakyPrototype.Certificate21.required_508 line 434
  202. def OAI.SnakyPrototype.Certificate21.envelope_508 line 435
  203. def OAI.SnakyPrototype.Certificate21.childrenC_508 line 436
  204. def OAI.SnakyPrototype.Certificate21.childrenD_508 line 437
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_508 line 438
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_508 line 439
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_508 line 440
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_508 line 441
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_508 line 442
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_508 line 452
  211. def OAI.SnakyPrototype.Certificate21.required_509 line 457
  212. def OAI.SnakyPrototype.Certificate21.envelope_509 line 458
  213. def OAI.SnakyPrototype.Certificate21.childrenC_509 line 459
  214. def OAI.SnakyPrototype.Certificate21.childrenD_509 line 460
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_509 line 461
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_509 line 462
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_509 line 463
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_509 line 464
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_509 line 465
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_509 line 473
  221. def OAI.SnakyPrototype.Certificate21.required_520 line 478
  222. def OAI.SnakyPrototype.Certificate21.envelope_520 line 479
  223. def OAI.SnakyPrototype.Certificate21.childrenC_520 line 480
  224. def OAI.SnakyPrototype.Certificate21.childrenD_520 line 481
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_520 line 482
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_520 line 483
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_520 line 484
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_520 line 485
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_520 line 486
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_520 line 492
  231. def OAI.SnakyPrototype.Certificate21.height_399 line 497
  232. def OAI.SnakyPrototype.Certificate21.childrenH_399 line 498
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_399 line 499
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_399 line 500
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_399 line 502
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_399 line 506
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_399 line 508
  238. def OAI.SnakyPrototype.Certificate21.checked_399 line 512
  239. def OAI.SnakyPrototype.Certificate21.height_401 line 520
  240. def OAI.SnakyPrototype.Certificate21.childrenH_401 line 521
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_401 line 522
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_401 line 523
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_401 line 525
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_401 line 529
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_401 line 531
  246. def OAI.SnakyPrototype.Certificate21.checked_401 line 535
  247. def OAI.SnakyPrototype.Certificate21.height_408 line 543
  248. def OAI.SnakyPrototype.Certificate21.childrenH_408 line 544
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_408 line 545
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_408 line 546
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_408 line 548
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_408 line 552
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_408 line 554
  254. def OAI.SnakyPrototype.Certificate21.checked_408 line 558
  255. def OAI.SnakyPrototype.Certificate21.height_409 line 566
  256. def OAI.SnakyPrototype.Certificate21.childrenH_409 line 567
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_409 line 568
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_409 line 569
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_409 line 571
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_409 line 575
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_409 line 577
  262. def OAI.SnakyPrototype.Certificate21.checked_409 line 581
  263. def OAI.SnakyPrototype.Certificate21.height_410 line 589
  264. def OAI.SnakyPrototype.Certificate21.childrenH_410 line 590
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_410 line 591
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_410 line 592
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_410 line 594
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_410 line 598
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_410 line 600
  270. def OAI.SnakyPrototype.Certificate21.checked_410 line 604
  271. def OAI.SnakyPrototype.Certificate21.height_411 line 612
  272. def OAI.SnakyPrototype.Certificate21.childrenH_411 line 613
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_411 line 614
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_411 line 615
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_411 line 617
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_411 line 621
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_411 line 623
  278. def OAI.SnakyPrototype.Certificate21.checked_411 line 627
  279. def OAI.SnakyPrototype.Certificate21.height_444 line 635
  280. def OAI.SnakyPrototype.Certificate21.childrenH_444 line 636
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_444 line 637
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_444 line 638
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_444 line 640
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_444 line 644
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_444 line 646
  286. def OAI.SnakyPrototype.Certificate21.checked_444 line 650
  287. def OAI.SnakyPrototype.Certificate21.height_459 line 658
  288. def OAI.SnakyPrototype.Certificate21.childrenH_459 line 659
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_459 line 660
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_459 line 661
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_459 line 663
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_459 line 667
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_459 line 669
  294. def OAI.SnakyPrototype.Certificate21.checked_459 line 673
  295. def OAI.SnakyPrototype.Certificate21.height_460 line 681
  296. def OAI.SnakyPrototype.Certificate21.childrenH_460 line 682
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_460 line 683
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_460 line 684
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_460 line 686
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_460 line 690
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_460 line 692
  302. def OAI.SnakyPrototype.Certificate21.checked_460 line 696
  303. def OAI.SnakyPrototype.Certificate21.height_461 line 704
  304. def OAI.SnakyPrototype.Certificate21.childrenH_461 line 705
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_461 line 706
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_461 line 707
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_461 line 709
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_461 line 713
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_461 line 715
  310. def OAI.SnakyPrototype.Certificate21.checked_461 line 719
  311. def OAI.SnakyPrototype.Certificate21.height_475 line 727
  312. def OAI.SnakyPrototype.Certificate21.childrenH_475 line 728
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_475 line 729
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_475 line 730
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_475 line 732
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_475 line 736
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_475 line 738
  318. def OAI.SnakyPrototype.Certificate21.checked_475 line 742
  319. def OAI.SnakyPrototype.Certificate21.height_476 line 750
  320. def OAI.SnakyPrototype.Certificate21.childrenH_476 line 751
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_476 line 752
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_476 line 753
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_476 line 755
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_476 line 759
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_476 line 761
  326. def OAI.SnakyPrototype.Certificate21.checked_476 line 765
  327. def OAI.SnakyPrototype.Certificate21.height_479_i0 line 773
  328. def OAI.SnakyPrototype.Certificate21.childrenH_479_i0 line 774
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_479_i0 line 775
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_479_i0 line 776
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_479_i0 line 778
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_479_i0 line 782
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_479_i0 line 784
  334. def OAI.SnakyPrototype.Certificate21.checked_479_i0 line 788
  335. def OAI.SnakyPrototype.Certificate21.height_479 line 796
  336. def OAI.SnakyPrototype.Certificate21.childrenH_479 line 797
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_479 line 798
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_479 line 799
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_479 line 801
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_479 line 805
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_479 line 807
  342. def OAI.SnakyPrototype.Certificate21.checked_479 line 811
  343. def OAI.SnakyPrototype.Certificate21.height_480 line 819
  344. def OAI.SnakyPrototype.Certificate21.childrenH_480 line 820
  345. theorem OAI.SnakyPrototype.Certificate21.height_exact_480 line 821
  346. theorem OAI.SnakyPrototype.Certificate21.required_origin_480 line 822
  347. theorem OAI.SnakyPrototype.Certificate21.required_exact_480 line 824
  348. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_480 line 828
  349. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_480 line 830
  350. def OAI.SnakyPrototype.Certificate21.checked_480 line 834
  351. def OAI.SnakyPrototype.Certificate21.height_481 line 842
  352. def OAI.SnakyPrototype.Certificate21.childrenH_481 line 843
  353. theorem OAI.SnakyPrototype.Certificate21.height_exact_481 line 844
  354. theorem OAI.SnakyPrototype.Certificate21.required_origin_481 line 845
  355. theorem OAI.SnakyPrototype.Certificate21.required_exact_481 line 847
  356. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_481 line 851
  357. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_481 line 853
  358. def OAI.SnakyPrototype.Certificate21.checked_481 line 857
  359. def OAI.SnakyPrototype.Certificate21.height_483 line 865
  360. def OAI.SnakyPrototype.Certificate21.childrenH_483 line 866
  361. theorem OAI.SnakyPrototype.Certificate21.height_exact_483 line 867
  362. theorem OAI.SnakyPrototype.Certificate21.required_origin_483 line 868
  363. theorem OAI.SnakyPrototype.Certificate21.required_exact_483 line 870
  364. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_483 line 874
  365. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_483 line 876
  366. def OAI.SnakyPrototype.Certificate21.checked_483 line 880
  367. def OAI.SnakyPrototype.Certificate21.height_491_i0 line 888
  368. def OAI.SnakyPrototype.Certificate21.childrenH_491_i0 line 889
  369. theorem OAI.SnakyPrototype.Certificate21.height_exact_491_i0 line 890
  370. theorem OAI.SnakyPrototype.Certificate21.required_origin_491_i0 line 891
  371. theorem OAI.SnakyPrototype.Certificate21.required_exact_491_i0 line 893
  372. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_491_i0 line 897
  373. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_491_i0 line 899
  374. def OAI.SnakyPrototype.Certificate21.checked_491_i0 line 903
  375. def OAI.SnakyPrototype.Certificate21.height_491_i1 line 911
  376. def OAI.SnakyPrototype.Certificate21.childrenH_491_i1 line 912
  377. theorem OAI.SnakyPrototype.Certificate21.height_exact_491_i1 line 913
  378. theorem OAI.SnakyPrototype.Certificate21.required_origin_491_i1 line 914
  379. theorem OAI.SnakyPrototype.Certificate21.required_exact_491_i1 line 916
  380. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_491_i1 line 920
  381. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_491_i1 line 922
  382. def OAI.SnakyPrototype.Certificate21.checked_491_i1 line 926
  383. def OAI.SnakyPrototype.Certificate21.height_491 line 934
  384. def OAI.SnakyPrototype.Certificate21.childrenH_491 line 935
  385. theorem OAI.SnakyPrototype.Certificate21.height_exact_491 line 936
  386. theorem OAI.SnakyPrototype.Certificate21.required_origin_491 line 937
  387. theorem OAI.SnakyPrototype.Certificate21.required_exact_491 line 939
  388. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_491 line 943
  389. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_491 line 945
  390. def OAI.SnakyPrototype.Certificate21.checked_491 line 949
  391. def OAI.SnakyPrototype.Certificate21.height_508 line 957
  392. def OAI.SnakyPrototype.Certificate21.childrenH_508 line 958
  393. theorem OAI.SnakyPrototype.Certificate21.height_exact_508 line 959
  394. theorem OAI.SnakyPrototype.Certificate21.required_origin_508 line 960
  395. theorem OAI.SnakyPrototype.Certificate21.required_exact_508 line 962
  396. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_508 line 966
  397. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_508 line 968
  398. def OAI.SnakyPrototype.Certificate21.checked_508 line 972
  399. def OAI.SnakyPrototype.Certificate21.height_509 line 980
  400. def OAI.SnakyPrototype.Certificate21.childrenH_509 line 981
  401. theorem OAI.SnakyPrototype.Certificate21.height_exact_509 line 982
  402. theorem OAI.SnakyPrototype.Certificate21.required_origin_509 line 983
  403. theorem OAI.SnakyPrototype.Certificate21.required_exact_509 line 985
  404. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_509 line 989
  405. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_509 line 991
  406. def OAI.SnakyPrototype.Certificate21.checked_509 line 995
  407. def OAI.SnakyPrototype.Certificate21.height_520 line 1003
  408. def OAI.SnakyPrototype.Certificate21.childrenH_520 line 1004
  409. theorem OAI.SnakyPrototype.Certificate21.height_exact_520 line 1005
  410. theorem OAI.SnakyPrototype.Certificate21.required_origin_520 line 1006
  411. theorem OAI.SnakyPrototype.Certificate21.required_exact_520 line 1008
  412. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_520 line 1012
  413. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_520 line 1014
  414. def OAI.SnakyPrototype.Certificate21.checked_520 line 1018