OAI/GameTheory/SnakyTwentyOne/Cards/Height02Part01.lean

GitHub source file

432 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_6 line 9
  2. def OAI.SnakyPrototype.Certificate21.envelope_6 line 10
  3. def OAI.SnakyPrototype.Certificate21.childrenC_6 line 11
  4. def OAI.SnakyPrototype.Certificate21.childrenD_6 line 12
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_6 line 13
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_6 line 14
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_6 line 15
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_6 line 16
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_6 line 17
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_6 line 22
  11. def OAI.SnakyPrototype.Certificate21.required_11 line 27
  12. def OAI.SnakyPrototype.Certificate21.envelope_11 line 28
  13. def OAI.SnakyPrototype.Certificate21.childrenC_11 line 29
  14. def OAI.SnakyPrototype.Certificate21.childrenD_11 line 30
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_11 line 31
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_11 line 32
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_11 line 33
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_11 line 34
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_11 line 35
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_11 line 40
  21. def OAI.SnakyPrototype.Certificate21.required_15 line 45
  22. def OAI.SnakyPrototype.Certificate21.envelope_15 line 46
  23. def OAI.SnakyPrototype.Certificate21.childrenC_15 line 47
  24. def OAI.SnakyPrototype.Certificate21.childrenD_15 line 48
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_15 line 49
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_15 line 50
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_15 line 51
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_15 line 52
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_15 line 53
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_15 line 58
  31. def OAI.SnakyPrototype.Certificate21.required_22 line 63
  32. def OAI.SnakyPrototype.Certificate21.envelope_22 line 64
  33. def OAI.SnakyPrototype.Certificate21.childrenC_22 line 65
  34. def OAI.SnakyPrototype.Certificate21.childrenD_22 line 66
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_22 line 67
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_22 line 68
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_22 line 69
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_22 line 70
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_22 line 71
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_22 line 76
  41. def OAI.SnakyPrototype.Certificate21.required_23 line 81
  42. def OAI.SnakyPrototype.Certificate21.envelope_23 line 82
  43. def OAI.SnakyPrototype.Certificate21.childrenC_23 line 83
  44. def OAI.SnakyPrototype.Certificate21.childrenD_23 line 84
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_23 line 85
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_23 line 86
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_23 line 87
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_23 line 88
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_23 line 89
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_23 line 94
  51. def OAI.SnakyPrototype.Certificate21.required_25 line 99
  52. def OAI.SnakyPrototype.Certificate21.envelope_25 line 100
  53. def OAI.SnakyPrototype.Certificate21.childrenC_25 line 101
  54. def OAI.SnakyPrototype.Certificate21.childrenD_25 line 102
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_25 line 103
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_25 line 104
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_25 line 105
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_25 line 106
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_25 line 107
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_25 line 112
  61. def OAI.SnakyPrototype.Certificate21.required_28 line 117
  62. def OAI.SnakyPrototype.Certificate21.envelope_28 line 118
  63. def OAI.SnakyPrototype.Certificate21.childrenC_28 line 119
  64. def OAI.SnakyPrototype.Certificate21.childrenD_28 line 120
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_28 line 121
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_28 line 122
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_28 line 123
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_28 line 124
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_28 line 125
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_28 line 130
  71. def OAI.SnakyPrototype.Certificate21.required_30 line 135
  72. def OAI.SnakyPrototype.Certificate21.envelope_30 line 136
  73. def OAI.SnakyPrototype.Certificate21.childrenC_30 line 137
  74. def OAI.SnakyPrototype.Certificate21.childrenD_30 line 138
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_30 line 139
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_30 line 140
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_30 line 141
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_30 line 142
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_30 line 143
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_30 line 148
  81. def OAI.SnakyPrototype.Certificate21.required_32 line 153
  82. def OAI.SnakyPrototype.Certificate21.envelope_32 line 154
  83. def OAI.SnakyPrototype.Certificate21.childrenC_32 line 155
  84. def OAI.SnakyPrototype.Certificate21.childrenD_32 line 156
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_32 line 157
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_32 line 158
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_32 line 159
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_32 line 160
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_32 line 161
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_32 line 166
  91. def OAI.SnakyPrototype.Certificate21.required_34 line 171
  92. def OAI.SnakyPrototype.Certificate21.envelope_34 line 172
  93. def OAI.SnakyPrototype.Certificate21.childrenC_34 line 173
  94. def OAI.SnakyPrototype.Certificate21.childrenD_34 line 174
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_34 line 175
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_34 line 176
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_34 line 177
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_34 line 178
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_34 line 179
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_34 line 184
  101. def OAI.SnakyPrototype.Certificate21.required_35 line 189
  102. def OAI.SnakyPrototype.Certificate21.envelope_35 line 190
  103. def OAI.SnakyPrototype.Certificate21.childrenC_35 line 191
  104. def OAI.SnakyPrototype.Certificate21.childrenD_35 line 192
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_35 line 193
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_35 line 194
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_35 line 195
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_35 line 196
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_35 line 197
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_35 line 202
  111. def OAI.SnakyPrototype.Certificate21.required_36 line 207
  112. def OAI.SnakyPrototype.Certificate21.envelope_36 line 208
  113. def OAI.SnakyPrototype.Certificate21.childrenC_36 line 209
  114. def OAI.SnakyPrototype.Certificate21.childrenD_36 line 210
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_36 line 211
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_36 line 212
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_36 line 213
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_36 line 214
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_36 line 215
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_36 line 220
  121. def OAI.SnakyPrototype.Certificate21.required_38 line 225
  122. def OAI.SnakyPrototype.Certificate21.envelope_38 line 226
  123. def OAI.SnakyPrototype.Certificate21.childrenC_38 line 227
  124. def OAI.SnakyPrototype.Certificate21.childrenD_38 line 228
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_38 line 229
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_38 line 230
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_38 line 231
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_38 line 232
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_38 line 233
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_38 line 238
  131. def OAI.SnakyPrototype.Certificate21.required_40 line 243
  132. def OAI.SnakyPrototype.Certificate21.envelope_40 line 244
  133. def OAI.SnakyPrototype.Certificate21.childrenC_40 line 245
  134. def OAI.SnakyPrototype.Certificate21.childrenD_40 line 246
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_40 line 247
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_40 line 248
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_40 line 249
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_40 line 250
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_40 line 251
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_40 line 256
  141. def OAI.SnakyPrototype.Certificate21.required_43 line 261
  142. def OAI.SnakyPrototype.Certificate21.envelope_43 line 262
  143. def OAI.SnakyPrototype.Certificate21.childrenC_43 line 263
  144. def OAI.SnakyPrototype.Certificate21.childrenD_43 line 264
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_43 line 265
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_43 line 266
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_43 line 267
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_43 line 268
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_43 line 269
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_43 line 274
  151. def OAI.SnakyPrototype.Certificate21.required_51 line 279
  152. def OAI.SnakyPrototype.Certificate21.envelope_51 line 280
  153. def OAI.SnakyPrototype.Certificate21.childrenC_51 line 281
  154. def OAI.SnakyPrototype.Certificate21.childrenD_51 line 282
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_51 line 283
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_51 line 284
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_51 line 285
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_51 line 286
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_51 line 287
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_51 line 292
  161. def OAI.SnakyPrototype.Certificate21.required_66 line 297
  162. def OAI.SnakyPrototype.Certificate21.envelope_66 line 298
  163. def OAI.SnakyPrototype.Certificate21.childrenC_66 line 299
  164. def OAI.SnakyPrototype.Certificate21.childrenD_66 line 300
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_66 line 301
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_66 line 302
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_66 line 303
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_66 line 304
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_66 line 305
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_66 line 310
  171. def OAI.SnakyPrototype.Certificate21.required_68 line 315
  172. def OAI.SnakyPrototype.Certificate21.envelope_68 line 316
  173. def OAI.SnakyPrototype.Certificate21.childrenC_68 line 317
  174. def OAI.SnakyPrototype.Certificate21.childrenD_68 line 318
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_68 line 319
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_68 line 320
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_68 line 321
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_68 line 322
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_68 line 323
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_68 line 328
  181. def OAI.SnakyPrototype.Certificate21.required_70 line 333
  182. def OAI.SnakyPrototype.Certificate21.envelope_70 line 334
  183. def OAI.SnakyPrototype.Certificate21.childrenC_70 line 335
  184. def OAI.SnakyPrototype.Certificate21.childrenD_70 line 336
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_70 line 337
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_70 line 338
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_70 line 339
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_70 line 340
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_70 line 341
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_70 line 346
  191. def OAI.SnakyPrototype.Certificate21.required_76 line 351
  192. def OAI.SnakyPrototype.Certificate21.envelope_76 line 352
  193. def OAI.SnakyPrototype.Certificate21.childrenC_76 line 353
  194. def OAI.SnakyPrototype.Certificate21.childrenD_76 line 354
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_76 line 355
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_76 line 356
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_76 line 357
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_76 line 358
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_76 line 359
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_76 line 364
  201. def OAI.SnakyPrototype.Certificate21.required_77 line 369
  202. def OAI.SnakyPrototype.Certificate21.envelope_77 line 370
  203. def OAI.SnakyPrototype.Certificate21.childrenC_77 line 371
  204. def OAI.SnakyPrototype.Certificate21.childrenD_77 line 372
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_77 line 373
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_77 line 374
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_77 line 375
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_77 line 376
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_77 line 377
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_77 line 382
  211. def OAI.SnakyPrototype.Certificate21.required_80 line 387
  212. def OAI.SnakyPrototype.Certificate21.envelope_80 line 388
  213. def OAI.SnakyPrototype.Certificate21.childrenC_80 line 389
  214. def OAI.SnakyPrototype.Certificate21.childrenD_80 line 390
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_80 line 391
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_80 line 392
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_80 line 393
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_80 line 394
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_80 line 395
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_80 line 400
  221. def OAI.SnakyPrototype.Certificate21.required_83 line 405
  222. def OAI.SnakyPrototype.Certificate21.envelope_83 line 406
  223. def OAI.SnakyPrototype.Certificate21.childrenC_83 line 407
  224. def OAI.SnakyPrototype.Certificate21.childrenD_83 line 408
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_83 line 409
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_83 line 410
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_83 line 411
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_83 line 412
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_83 line 413
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_83 line 418
  231. def OAI.SnakyPrototype.Certificate21.required_94 line 423
  232. def OAI.SnakyPrototype.Certificate21.envelope_94 line 424
  233. def OAI.SnakyPrototype.Certificate21.childrenC_94 line 425
  234. def OAI.SnakyPrototype.Certificate21.childrenD_94 line 426
  235. theorem OAI.SnakyPrototype.Certificate21.common_sub_94 line 427
  236. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_94 line 428
  237. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_94 line 429
  238. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_94 line 430
  239. theorem OAI.SnakyPrototype.Certificate21.children_work_94 line 431
  240. theorem OAI.SnakyPrototype.Certificate21.row_works_94 line 436
  241. def OAI.SnakyPrototype.Certificate21.height_6 line 441
  242. def OAI.SnakyPrototype.Certificate21.childrenH_6 line 442
  243. theorem OAI.SnakyPrototype.Certificate21.height_exact_6 line 443
  244. theorem OAI.SnakyPrototype.Certificate21.required_origin_6 line 444
  245. theorem OAI.SnakyPrototype.Certificate21.required_exact_6 line 446
  246. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_6 line 450
  247. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_6 line 452
  248. def OAI.SnakyPrototype.Certificate21.checked_6 line 456
  249. def OAI.SnakyPrototype.Certificate21.height_11 line 464
  250. def OAI.SnakyPrototype.Certificate21.childrenH_11 line 465
  251. theorem OAI.SnakyPrototype.Certificate21.height_exact_11 line 466
  252. theorem OAI.SnakyPrototype.Certificate21.required_origin_11 line 467
  253. theorem OAI.SnakyPrototype.Certificate21.required_exact_11 line 469
  254. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_11 line 473
  255. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_11 line 475
  256. def OAI.SnakyPrototype.Certificate21.checked_11 line 479
  257. def OAI.SnakyPrototype.Certificate21.height_15 line 487
  258. def OAI.SnakyPrototype.Certificate21.childrenH_15 line 488
  259. theorem OAI.SnakyPrototype.Certificate21.height_exact_15 line 489
  260. theorem OAI.SnakyPrototype.Certificate21.required_origin_15 line 490
  261. theorem OAI.SnakyPrototype.Certificate21.required_exact_15 line 492
  262. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_15 line 496
  263. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_15 line 498
  264. def OAI.SnakyPrototype.Certificate21.checked_15 line 502
  265. def OAI.SnakyPrototype.Certificate21.height_22 line 510
  266. def OAI.SnakyPrototype.Certificate21.childrenH_22 line 511
  267. theorem OAI.SnakyPrototype.Certificate21.height_exact_22 line 512
  268. theorem OAI.SnakyPrototype.Certificate21.required_origin_22 line 513
  269. theorem OAI.SnakyPrototype.Certificate21.required_exact_22 line 515
  270. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_22 line 519
  271. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_22 line 521
  272. def OAI.SnakyPrototype.Certificate21.checked_22 line 525
  273. def OAI.SnakyPrototype.Certificate21.height_23 line 533
  274. def OAI.SnakyPrototype.Certificate21.childrenH_23 line 534
  275. theorem OAI.SnakyPrototype.Certificate21.height_exact_23 line 535
  276. theorem OAI.SnakyPrototype.Certificate21.required_origin_23 line 536
  277. theorem OAI.SnakyPrototype.Certificate21.required_exact_23 line 538
  278. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_23 line 542
  279. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_23 line 544
  280. def OAI.SnakyPrototype.Certificate21.checked_23 line 548
  281. def OAI.SnakyPrototype.Certificate21.height_25 line 556
  282. def OAI.SnakyPrototype.Certificate21.childrenH_25 line 557
  283. theorem OAI.SnakyPrototype.Certificate21.height_exact_25 line 558
  284. theorem OAI.SnakyPrototype.Certificate21.required_origin_25 line 559
  285. theorem OAI.SnakyPrototype.Certificate21.required_exact_25 line 561
  286. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_25 line 565
  287. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_25 line 567
  288. def OAI.SnakyPrototype.Certificate21.checked_25 line 571
  289. def OAI.SnakyPrototype.Certificate21.height_28 line 579
  290. def OAI.SnakyPrototype.Certificate21.childrenH_28 line 580
  291. theorem OAI.SnakyPrototype.Certificate21.height_exact_28 line 581
  292. theorem OAI.SnakyPrototype.Certificate21.required_origin_28 line 582
  293. theorem OAI.SnakyPrototype.Certificate21.required_exact_28 line 584
  294. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_28 line 588
  295. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_28 line 590
  296. def OAI.SnakyPrototype.Certificate21.checked_28 line 594
  297. def OAI.SnakyPrototype.Certificate21.height_30 line 602
  298. def OAI.SnakyPrototype.Certificate21.childrenH_30 line 603
  299. theorem OAI.SnakyPrototype.Certificate21.height_exact_30 line 604
  300. theorem OAI.SnakyPrototype.Certificate21.required_origin_30 line 605
  301. theorem OAI.SnakyPrototype.Certificate21.required_exact_30 line 607
  302. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_30 line 611
  303. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_30 line 613
  304. def OAI.SnakyPrototype.Certificate21.checked_30 line 617
  305. def OAI.SnakyPrototype.Certificate21.height_32 line 625
  306. def OAI.SnakyPrototype.Certificate21.childrenH_32 line 626
  307. theorem OAI.SnakyPrototype.Certificate21.height_exact_32 line 627
  308. theorem OAI.SnakyPrototype.Certificate21.required_origin_32 line 628
  309. theorem OAI.SnakyPrototype.Certificate21.required_exact_32 line 630
  310. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_32 line 634
  311. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_32 line 636
  312. def OAI.SnakyPrototype.Certificate21.checked_32 line 640
  313. def OAI.SnakyPrototype.Certificate21.height_34 line 648
  314. def OAI.SnakyPrototype.Certificate21.childrenH_34 line 649
  315. theorem OAI.SnakyPrototype.Certificate21.height_exact_34 line 650
  316. theorem OAI.SnakyPrototype.Certificate21.required_origin_34 line 651
  317. theorem OAI.SnakyPrototype.Certificate21.required_exact_34 line 653
  318. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_34 line 657
  319. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_34 line 659
  320. def OAI.SnakyPrototype.Certificate21.checked_34 line 663
  321. def OAI.SnakyPrototype.Certificate21.height_35 line 671
  322. def OAI.SnakyPrototype.Certificate21.childrenH_35 line 672
  323. theorem OAI.SnakyPrototype.Certificate21.height_exact_35 line 673
  324. theorem OAI.SnakyPrototype.Certificate21.required_origin_35 line 674
  325. theorem OAI.SnakyPrototype.Certificate21.required_exact_35 line 676
  326. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_35 line 680
  327. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_35 line 682
  328. def OAI.SnakyPrototype.Certificate21.checked_35 line 686
  329. def OAI.SnakyPrototype.Certificate21.height_36 line 694
  330. def OAI.SnakyPrototype.Certificate21.childrenH_36 line 695
  331. theorem OAI.SnakyPrototype.Certificate21.height_exact_36 line 696
  332. theorem OAI.SnakyPrototype.Certificate21.required_origin_36 line 697
  333. theorem OAI.SnakyPrototype.Certificate21.required_exact_36 line 699
  334. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_36 line 703
  335. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_36 line 705
  336. def OAI.SnakyPrototype.Certificate21.checked_36 line 709
  337. def OAI.SnakyPrototype.Certificate21.height_38 line 717
  338. def OAI.SnakyPrototype.Certificate21.childrenH_38 line 718
  339. theorem OAI.SnakyPrototype.Certificate21.height_exact_38 line 719
  340. theorem OAI.SnakyPrototype.Certificate21.required_origin_38 line 720
  341. theorem OAI.SnakyPrototype.Certificate21.required_exact_38 line 722
  342. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_38 line 726
  343. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_38 line 728
  344. def OAI.SnakyPrototype.Certificate21.checked_38 line 732
  345. def OAI.SnakyPrototype.Certificate21.height_40 line 740
  346. def OAI.SnakyPrototype.Certificate21.childrenH_40 line 741
  347. theorem OAI.SnakyPrototype.Certificate21.height_exact_40 line 742
  348. theorem OAI.SnakyPrototype.Certificate21.required_origin_40 line 743
  349. theorem OAI.SnakyPrototype.Certificate21.required_exact_40 line 745
  350. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_40 line 749
  351. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_40 line 751
  352. def OAI.SnakyPrototype.Certificate21.checked_40 line 755
  353. def OAI.SnakyPrototype.Certificate21.height_43 line 763
  354. def OAI.SnakyPrototype.Certificate21.childrenH_43 line 764
  355. theorem OAI.SnakyPrototype.Certificate21.height_exact_43 line 765
  356. theorem OAI.SnakyPrototype.Certificate21.required_origin_43 line 766
  357. theorem OAI.SnakyPrototype.Certificate21.required_exact_43 line 768
  358. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_43 line 772
  359. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_43 line 774
  360. def OAI.SnakyPrototype.Certificate21.checked_43 line 778
  361. def OAI.SnakyPrototype.Certificate21.height_51 line 786
  362. def OAI.SnakyPrototype.Certificate21.childrenH_51 line 787
  363. theorem OAI.SnakyPrototype.Certificate21.height_exact_51 line 788
  364. theorem OAI.SnakyPrototype.Certificate21.required_origin_51 line 789
  365. theorem OAI.SnakyPrototype.Certificate21.required_exact_51 line 791
  366. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_51 line 795
  367. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_51 line 797
  368. def OAI.SnakyPrototype.Certificate21.checked_51 line 801
  369. def OAI.SnakyPrototype.Certificate21.height_66 line 809
  370. def OAI.SnakyPrototype.Certificate21.childrenH_66 line 810
  371. theorem OAI.SnakyPrototype.Certificate21.height_exact_66 line 811
  372. theorem OAI.SnakyPrototype.Certificate21.required_origin_66 line 812
  373. theorem OAI.SnakyPrototype.Certificate21.required_exact_66 line 814
  374. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_66 line 818
  375. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_66 line 820
  376. def OAI.SnakyPrototype.Certificate21.checked_66 line 824
  377. def OAI.SnakyPrototype.Certificate21.height_68 line 832
  378. def OAI.SnakyPrototype.Certificate21.childrenH_68 line 833
  379. theorem OAI.SnakyPrototype.Certificate21.height_exact_68 line 834
  380. theorem OAI.SnakyPrototype.Certificate21.required_origin_68 line 835
  381. theorem OAI.SnakyPrototype.Certificate21.required_exact_68 line 837
  382. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_68 line 841
  383. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_68 line 843
  384. def OAI.SnakyPrototype.Certificate21.checked_68 line 847
  385. def OAI.SnakyPrototype.Certificate21.height_70 line 855
  386. def OAI.SnakyPrototype.Certificate21.childrenH_70 line 856
  387. theorem OAI.SnakyPrototype.Certificate21.height_exact_70 line 857
  388. theorem OAI.SnakyPrototype.Certificate21.required_origin_70 line 858
  389. theorem OAI.SnakyPrototype.Certificate21.required_exact_70 line 860
  390. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_70 line 864
  391. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_70 line 866
  392. def OAI.SnakyPrototype.Certificate21.checked_70 line 870
  393. def OAI.SnakyPrototype.Certificate21.height_76 line 878
  394. def OAI.SnakyPrototype.Certificate21.childrenH_76 line 879
  395. theorem OAI.SnakyPrototype.Certificate21.height_exact_76 line 880
  396. theorem OAI.SnakyPrototype.Certificate21.required_origin_76 line 881
  397. theorem OAI.SnakyPrototype.Certificate21.required_exact_76 line 883
  398. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_76 line 887
  399. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_76 line 889
  400. def OAI.SnakyPrototype.Certificate21.checked_76 line 893
  401. def OAI.SnakyPrototype.Certificate21.height_77 line 901
  402. def OAI.SnakyPrototype.Certificate21.childrenH_77 line 902
  403. theorem OAI.SnakyPrototype.Certificate21.height_exact_77 line 903
  404. theorem OAI.SnakyPrototype.Certificate21.required_origin_77 line 904
  405. theorem OAI.SnakyPrototype.Certificate21.required_exact_77 line 906
  406. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_77 line 910
  407. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_77 line 912
  408. def OAI.SnakyPrototype.Certificate21.checked_77 line 916
  409. def OAI.SnakyPrototype.Certificate21.height_80 line 924
  410. def OAI.SnakyPrototype.Certificate21.childrenH_80 line 925
  411. theorem OAI.SnakyPrototype.Certificate21.height_exact_80 line 926
  412. theorem OAI.SnakyPrototype.Certificate21.required_origin_80 line 927
  413. theorem OAI.SnakyPrototype.Certificate21.required_exact_80 line 929
  414. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_80 line 933
  415. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_80 line 935
  416. def OAI.SnakyPrototype.Certificate21.checked_80 line 939
  417. def OAI.SnakyPrototype.Certificate21.height_83 line 947
  418. def OAI.SnakyPrototype.Certificate21.childrenH_83 line 948
  419. theorem OAI.SnakyPrototype.Certificate21.height_exact_83 line 949
  420. theorem OAI.SnakyPrototype.Certificate21.required_origin_83 line 950
  421. theorem OAI.SnakyPrototype.Certificate21.required_exact_83 line 952
  422. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_83 line 956
  423. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_83 line 958
  424. def OAI.SnakyPrototype.Certificate21.checked_83 line 962
  425. def OAI.SnakyPrototype.Certificate21.height_94 line 970
  426. def OAI.SnakyPrototype.Certificate21.childrenH_94 line 971
  427. theorem OAI.SnakyPrototype.Certificate21.height_exact_94 line 972
  428. theorem OAI.SnakyPrototype.Certificate21.required_origin_94 line 973
  429. theorem OAI.SnakyPrototype.Certificate21.required_exact_94 line 975
  430. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_94 line 979
  431. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_94 line 981
  432. def OAI.SnakyPrototype.Certificate21.checked_94 line 985