OAI/GameTheory/SnakyTwentyOne/Cards/Height03Part02.lean

GitHub source file

432 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_108 line 11
  2. def OAI.SnakyPrototype.Certificate21.envelope_108 line 12
  3. def OAI.SnakyPrototype.Certificate21.childrenC_108 line 13
  4. def OAI.SnakyPrototype.Certificate21.childrenD_108 line 14
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_108 line 15
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_108 line 16
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_108 line 17
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_108 line 18
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_108 line 19
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_108 line 24
  11. def OAI.SnakyPrototype.Certificate21.required_113 line 29
  12. def OAI.SnakyPrototype.Certificate21.envelope_113 line 30
  13. def OAI.SnakyPrototype.Certificate21.childrenC_113 line 31
  14. def OAI.SnakyPrototype.Certificate21.childrenD_113 line 32
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_113 line 33
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_113 line 34
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_113 line 35
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_113 line 36
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_113 line 37
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_113 line 42
  21. def OAI.SnakyPrototype.Certificate21.required_124 line 47
  22. def OAI.SnakyPrototype.Certificate21.envelope_124 line 48
  23. def OAI.SnakyPrototype.Certificate21.childrenC_124 line 49
  24. def OAI.SnakyPrototype.Certificate21.childrenD_124 line 50
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_124 line 51
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_124 line 52
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_124 line 53
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_124 line 54
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_124 line 55
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_124 line 60
  31. def OAI.SnakyPrototype.Certificate21.required_126 line 65
  32. def OAI.SnakyPrototype.Certificate21.envelope_126 line 66
  33. def OAI.SnakyPrototype.Certificate21.childrenC_126 line 67
  34. def OAI.SnakyPrototype.Certificate21.childrenD_126 line 68
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_126 line 69
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_126 line 70
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_126 line 71
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_126 line 72
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_126 line 73
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_126 line 78
  41. def OAI.SnakyPrototype.Certificate21.required_130 line 83
  42. def OAI.SnakyPrototype.Certificate21.envelope_130 line 84
  43. def OAI.SnakyPrototype.Certificate21.childrenC_130 line 85
  44. def OAI.SnakyPrototype.Certificate21.childrenD_130 line 86
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_130 line 87
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_130 line 88
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_130 line 89
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_130 line 90
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_130 line 91
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_130 line 96
  51. def OAI.SnakyPrototype.Certificate21.required_131 line 101
  52. def OAI.SnakyPrototype.Certificate21.envelope_131 line 102
  53. def OAI.SnakyPrototype.Certificate21.childrenC_131 line 103
  54. def OAI.SnakyPrototype.Certificate21.childrenD_131 line 104
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_131 line 105
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_131 line 106
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_131 line 107
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_131 line 108
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_131 line 109
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_131 line 114
  61. def OAI.SnakyPrototype.Certificate21.required_139 line 119
  62. def OAI.SnakyPrototype.Certificate21.envelope_139 line 120
  63. def OAI.SnakyPrototype.Certificate21.childrenC_139 line 121
  64. def OAI.SnakyPrototype.Certificate21.childrenD_139 line 122
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_139 line 123
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_139 line 124
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_139 line 125
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_139 line 126
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_139 line 127
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_139 line 132
  71. def OAI.SnakyPrototype.Certificate21.required_140 line 137
  72. def OAI.SnakyPrototype.Certificate21.envelope_140 line 138
  73. def OAI.SnakyPrototype.Certificate21.childrenC_140 line 139
  74. def OAI.SnakyPrototype.Certificate21.childrenD_140 line 140
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_140 line 141
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_140 line 142
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_140 line 143
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_140 line 144
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_140 line 145
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_140 line 150
  81. def OAI.SnakyPrototype.Certificate21.required_143 line 155
  82. def OAI.SnakyPrototype.Certificate21.envelope_143 line 156
  83. def OAI.SnakyPrototype.Certificate21.childrenC_143 line 157
  84. def OAI.SnakyPrototype.Certificate21.childrenD_143 line 158
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_143 line 159
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_143 line 160
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_143 line 161
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_143 line 162
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_143 line 163
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_143 line 168
  91. def OAI.SnakyPrototype.Certificate21.required_157 line 173
  92. def OAI.SnakyPrototype.Certificate21.envelope_157 line 174
  93. def OAI.SnakyPrototype.Certificate21.childrenC_157 line 175
  94. def OAI.SnakyPrototype.Certificate21.childrenD_157 line 176
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_157 line 177
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_157 line 178
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_157 line 179
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_157 line 180
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_157 line 181
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_157 line 186
  101. def OAI.SnakyPrototype.Certificate21.required_158 line 191
  102. def OAI.SnakyPrototype.Certificate21.envelope_158 line 192
  103. def OAI.SnakyPrototype.Certificate21.childrenC_158 line 193
  104. def OAI.SnakyPrototype.Certificate21.childrenD_158 line 194
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_158 line 195
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_158 line 196
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_158 line 197
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_158 line 198
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_158 line 199
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_158 line 204
  111. def OAI.SnakyPrototype.Certificate21.required_159 line 209
  112. def OAI.SnakyPrototype.Certificate21.envelope_159 line 210
  113. def OAI.SnakyPrototype.Certificate21.childrenC_159 line 211
  114. def OAI.SnakyPrototype.Certificate21.childrenD_159 line 212
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_159 line 213
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_159 line 214
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_159 line 215
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_159 line 216
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_159 line 217
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_159 line 222
  121. def OAI.SnakyPrototype.Certificate21.required_160 line 227
  122. def OAI.SnakyPrototype.Certificate21.envelope_160 line 228
  123. def OAI.SnakyPrototype.Certificate21.childrenC_160 line 229
  124. def OAI.SnakyPrototype.Certificate21.childrenD_160 line 230
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_160 line 231
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_160 line 232
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_160 line 233
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_160 line 234
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_160 line 235
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_160 line 240
  131. def OAI.SnakyPrototype.Certificate21.required_163 line 245
  132. def OAI.SnakyPrototype.Certificate21.envelope_163 line 246
  133. def OAI.SnakyPrototype.Certificate21.childrenC_163 line 247
  134. def OAI.SnakyPrototype.Certificate21.childrenD_163 line 248
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_163 line 249
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_163 line 250
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_163 line 251
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_163 line 252
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_163 line 253
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_163 line 258
  141. def OAI.SnakyPrototype.Certificate21.required_177 line 263
  142. def OAI.SnakyPrototype.Certificate21.envelope_177 line 264
  143. def OAI.SnakyPrototype.Certificate21.childrenC_177 line 265
  144. def OAI.SnakyPrototype.Certificate21.childrenD_177 line 266
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_177 line 267
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_177 line 268
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_177 line 269
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_177 line 270
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_177 line 271
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_177 line 276
  151. def OAI.SnakyPrototype.Certificate21.required_198 line 281
  152. def OAI.SnakyPrototype.Certificate21.envelope_198 line 282
  153. def OAI.SnakyPrototype.Certificate21.childrenC_198 line 283
  154. def OAI.SnakyPrototype.Certificate21.childrenD_198 line 284
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_198 line 285
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_198 line 286
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_198 line 287
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_198 line 288
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_198 line 289
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_198 line 294
  161. def OAI.SnakyPrototype.Certificate21.required_201 line 299
  162. def OAI.SnakyPrototype.Certificate21.envelope_201 line 300
  163. def OAI.SnakyPrototype.Certificate21.childrenC_201 line 301
  164. def OAI.SnakyPrototype.Certificate21.childrenD_201 line 302
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_201 line 303
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_201 line 304
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_201 line 305
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_201 line 306
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_201 line 307
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_201 line 312
  171. def OAI.SnakyPrototype.Certificate21.required_205 line 317
  172. def OAI.SnakyPrototype.Certificate21.envelope_205 line 318
  173. def OAI.SnakyPrototype.Certificate21.childrenC_205 line 319
  174. def OAI.SnakyPrototype.Certificate21.childrenD_205 line 320
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_205 line 321
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_205 line 322
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_205 line 323
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_205 line 324
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_205 line 325
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_205 line 330
  181. def OAI.SnakyPrototype.Certificate21.required_207 line 335
  182. def OAI.SnakyPrototype.Certificate21.envelope_207 line 336
  183. def OAI.SnakyPrototype.Certificate21.childrenC_207 line 337
  184. def OAI.SnakyPrototype.Certificate21.childrenD_207 line 338
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_207 line 339
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_207 line 340
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_207 line 341
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_207 line 342
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_207 line 343
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_207 line 348
  191. def OAI.SnakyPrototype.Certificate21.required_209 line 353
  192. def OAI.SnakyPrototype.Certificate21.envelope_209 line 354
  193. def OAI.SnakyPrototype.Certificate21.childrenC_209 line 355
  194. def OAI.SnakyPrototype.Certificate21.childrenD_209 line 356
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_209 line 357
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_209 line 358
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_209 line 359
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_209 line 360
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_209 line 361
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_209 line 366
  201. def OAI.SnakyPrototype.Certificate21.required_212 line 371
  202. def OAI.SnakyPrototype.Certificate21.envelope_212 line 372
  203. def OAI.SnakyPrototype.Certificate21.childrenC_212 line 373
  204. def OAI.SnakyPrototype.Certificate21.childrenD_212 line 374
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_212 line 375
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_212 line 376
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_212 line 377
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_212 line 378
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_212 line 379
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_212 line 384
  211. def OAI.SnakyPrototype.Certificate21.required_215 line 389
  212. def OAI.SnakyPrototype.Certificate21.envelope_215 line 390
  213. def OAI.SnakyPrototype.Certificate21.childrenC_215 line 391
  214. def OAI.SnakyPrototype.Certificate21.childrenD_215 line 392
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_215 line 393
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_215 line 394
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_215 line 395
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_215 line 396
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_215 line 397
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_215 line 402
  221. def OAI.SnakyPrototype.Certificate21.required_218 line 407
  222. def OAI.SnakyPrototype.Certificate21.envelope_218 line 408
  223. def OAI.SnakyPrototype.Certificate21.childrenC_218 line 409
  224. def OAI.SnakyPrototype.Certificate21.childrenD_218 line 410
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_218 line 411
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_218 line 412
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_218 line 413
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_218 line 414
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_218 line 415
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_218 line 420
  231. def OAI.SnakyPrototype.Certificate21.required_219 line 425
  232. def OAI.SnakyPrototype.Certificate21.envelope_219 line 426
  233. def OAI.SnakyPrototype.Certificate21.childrenC_219 line 427
  234. def OAI.SnakyPrototype.Certificate21.childrenD_219 line 428
  235. theorem OAI.SnakyPrototype.Certificate21.common_sub_219 line 429
  236. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_219 line 430
  237. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_219 line 431
  238. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_219 line 432
  239. theorem OAI.SnakyPrototype.Certificate21.children_work_219 line 433
  240. theorem OAI.SnakyPrototype.Certificate21.row_works_219 line 438
  241. def OAI.SnakyPrototype.Certificate21.height_108 line 443
  242. def OAI.SnakyPrototype.Certificate21.childrenH_108 line 444
  243. theorem OAI.SnakyPrototype.Certificate21.height_exact_108 line 445
  244. theorem OAI.SnakyPrototype.Certificate21.required_origin_108 line 446
  245. theorem OAI.SnakyPrototype.Certificate21.required_exact_108 line 448
  246. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_108 line 452
  247. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_108 line 454
  248. def OAI.SnakyPrototype.Certificate21.checked_108 line 458
  249. def OAI.SnakyPrototype.Certificate21.height_113 line 466
  250. def OAI.SnakyPrototype.Certificate21.childrenH_113 line 467
  251. theorem OAI.SnakyPrototype.Certificate21.height_exact_113 line 468
  252. theorem OAI.SnakyPrototype.Certificate21.required_origin_113 line 469
  253. theorem OAI.SnakyPrototype.Certificate21.required_exact_113 line 471
  254. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_113 line 475
  255. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_113 line 477
  256. def OAI.SnakyPrototype.Certificate21.checked_113 line 481
  257. def OAI.SnakyPrototype.Certificate21.height_124 line 489
  258. def OAI.SnakyPrototype.Certificate21.childrenH_124 line 490
  259. theorem OAI.SnakyPrototype.Certificate21.height_exact_124 line 491
  260. theorem OAI.SnakyPrototype.Certificate21.required_origin_124 line 492
  261. theorem OAI.SnakyPrototype.Certificate21.required_exact_124 line 494
  262. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_124 line 498
  263. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_124 line 500
  264. def OAI.SnakyPrototype.Certificate21.checked_124 line 504
  265. def OAI.SnakyPrototype.Certificate21.height_126 line 512
  266. def OAI.SnakyPrototype.Certificate21.childrenH_126 line 513
  267. theorem OAI.SnakyPrototype.Certificate21.height_exact_126 line 514
  268. theorem OAI.SnakyPrototype.Certificate21.required_origin_126 line 515
  269. theorem OAI.SnakyPrototype.Certificate21.required_exact_126 line 517
  270. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_126 line 521
  271. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_126 line 523
  272. def OAI.SnakyPrototype.Certificate21.checked_126 line 527
  273. def OAI.SnakyPrototype.Certificate21.height_130 line 535
  274. def OAI.SnakyPrototype.Certificate21.childrenH_130 line 536
  275. theorem OAI.SnakyPrototype.Certificate21.height_exact_130 line 537
  276. theorem OAI.SnakyPrototype.Certificate21.required_origin_130 line 538
  277. theorem OAI.SnakyPrototype.Certificate21.required_exact_130 line 540
  278. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_130 line 544
  279. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_130 line 546
  280. def OAI.SnakyPrototype.Certificate21.checked_130 line 550
  281. def OAI.SnakyPrototype.Certificate21.height_131 line 558
  282. def OAI.SnakyPrototype.Certificate21.childrenH_131 line 559
  283. theorem OAI.SnakyPrototype.Certificate21.height_exact_131 line 560
  284. theorem OAI.SnakyPrototype.Certificate21.required_origin_131 line 561
  285. theorem OAI.SnakyPrototype.Certificate21.required_exact_131 line 563
  286. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_131 line 567
  287. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_131 line 569
  288. def OAI.SnakyPrototype.Certificate21.checked_131 line 573
  289. def OAI.SnakyPrototype.Certificate21.height_139 line 581
  290. def OAI.SnakyPrototype.Certificate21.childrenH_139 line 582
  291. theorem OAI.SnakyPrototype.Certificate21.height_exact_139 line 583
  292. theorem OAI.SnakyPrototype.Certificate21.required_origin_139 line 584
  293. theorem OAI.SnakyPrototype.Certificate21.required_exact_139 line 586
  294. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_139 line 590
  295. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_139 line 592
  296. def OAI.SnakyPrototype.Certificate21.checked_139 line 596
  297. def OAI.SnakyPrototype.Certificate21.height_140 line 604
  298. def OAI.SnakyPrototype.Certificate21.childrenH_140 line 605
  299. theorem OAI.SnakyPrototype.Certificate21.height_exact_140 line 606
  300. theorem OAI.SnakyPrototype.Certificate21.required_origin_140 line 607
  301. theorem OAI.SnakyPrototype.Certificate21.required_exact_140 line 609
  302. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_140 line 613
  303. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_140 line 615
  304. def OAI.SnakyPrototype.Certificate21.checked_140 line 619
  305. def OAI.SnakyPrototype.Certificate21.height_143 line 627
  306. def OAI.SnakyPrototype.Certificate21.childrenH_143 line 628
  307. theorem OAI.SnakyPrototype.Certificate21.height_exact_143 line 629
  308. theorem OAI.SnakyPrototype.Certificate21.required_origin_143 line 630
  309. theorem OAI.SnakyPrototype.Certificate21.required_exact_143 line 632
  310. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_143 line 636
  311. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_143 line 638
  312. def OAI.SnakyPrototype.Certificate21.checked_143 line 642
  313. def OAI.SnakyPrototype.Certificate21.height_157 line 650
  314. def OAI.SnakyPrototype.Certificate21.childrenH_157 line 651
  315. theorem OAI.SnakyPrototype.Certificate21.height_exact_157 line 652
  316. theorem OAI.SnakyPrototype.Certificate21.required_origin_157 line 653
  317. theorem OAI.SnakyPrototype.Certificate21.required_exact_157 line 655
  318. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_157 line 659
  319. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_157 line 661
  320. def OAI.SnakyPrototype.Certificate21.checked_157 line 665
  321. def OAI.SnakyPrototype.Certificate21.height_158 line 673
  322. def OAI.SnakyPrototype.Certificate21.childrenH_158 line 674
  323. theorem OAI.SnakyPrototype.Certificate21.height_exact_158 line 675
  324. theorem OAI.SnakyPrototype.Certificate21.required_origin_158 line 676
  325. theorem OAI.SnakyPrototype.Certificate21.required_exact_158 line 678
  326. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_158 line 682
  327. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_158 line 684
  328. def OAI.SnakyPrototype.Certificate21.checked_158 line 688
  329. def OAI.SnakyPrototype.Certificate21.height_159 line 696
  330. def OAI.SnakyPrototype.Certificate21.childrenH_159 line 697
  331. theorem OAI.SnakyPrototype.Certificate21.height_exact_159 line 698
  332. theorem OAI.SnakyPrototype.Certificate21.required_origin_159 line 699
  333. theorem OAI.SnakyPrototype.Certificate21.required_exact_159 line 701
  334. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_159 line 705
  335. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_159 line 707
  336. def OAI.SnakyPrototype.Certificate21.checked_159 line 711
  337. def OAI.SnakyPrototype.Certificate21.height_160 line 719
  338. def OAI.SnakyPrototype.Certificate21.childrenH_160 line 720
  339. theorem OAI.SnakyPrototype.Certificate21.height_exact_160 line 721
  340. theorem OAI.SnakyPrototype.Certificate21.required_origin_160 line 722
  341. theorem OAI.SnakyPrototype.Certificate21.required_exact_160 line 724
  342. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_160 line 728
  343. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_160 line 730
  344. def OAI.SnakyPrototype.Certificate21.checked_160 line 734
  345. def OAI.SnakyPrototype.Certificate21.height_163 line 742
  346. def OAI.SnakyPrototype.Certificate21.childrenH_163 line 743
  347. theorem OAI.SnakyPrototype.Certificate21.height_exact_163 line 744
  348. theorem OAI.SnakyPrototype.Certificate21.required_origin_163 line 745
  349. theorem OAI.SnakyPrototype.Certificate21.required_exact_163 line 747
  350. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_163 line 751
  351. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_163 line 753
  352. def OAI.SnakyPrototype.Certificate21.checked_163 line 757
  353. def OAI.SnakyPrototype.Certificate21.height_177 line 765
  354. def OAI.SnakyPrototype.Certificate21.childrenH_177 line 766
  355. theorem OAI.SnakyPrototype.Certificate21.height_exact_177 line 767
  356. theorem OAI.SnakyPrototype.Certificate21.required_origin_177 line 768
  357. theorem OAI.SnakyPrototype.Certificate21.required_exact_177 line 770
  358. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_177 line 774
  359. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_177 line 776
  360. def OAI.SnakyPrototype.Certificate21.checked_177 line 780
  361. def OAI.SnakyPrototype.Certificate21.height_198 line 788
  362. def OAI.SnakyPrototype.Certificate21.childrenH_198 line 789
  363. theorem OAI.SnakyPrototype.Certificate21.height_exact_198 line 790
  364. theorem OAI.SnakyPrototype.Certificate21.required_origin_198 line 791
  365. theorem OAI.SnakyPrototype.Certificate21.required_exact_198 line 793
  366. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_198 line 797
  367. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_198 line 799
  368. def OAI.SnakyPrototype.Certificate21.checked_198 line 803
  369. def OAI.SnakyPrototype.Certificate21.height_201 line 811
  370. def OAI.SnakyPrototype.Certificate21.childrenH_201 line 812
  371. theorem OAI.SnakyPrototype.Certificate21.height_exact_201 line 813
  372. theorem OAI.SnakyPrototype.Certificate21.required_origin_201 line 814
  373. theorem OAI.SnakyPrototype.Certificate21.required_exact_201 line 816
  374. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_201 line 820
  375. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_201 line 822
  376. def OAI.SnakyPrototype.Certificate21.checked_201 line 826
  377. def OAI.SnakyPrototype.Certificate21.height_205 line 834
  378. def OAI.SnakyPrototype.Certificate21.childrenH_205 line 835
  379. theorem OAI.SnakyPrototype.Certificate21.height_exact_205 line 836
  380. theorem OAI.SnakyPrototype.Certificate21.required_origin_205 line 837
  381. theorem OAI.SnakyPrototype.Certificate21.required_exact_205 line 839
  382. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_205 line 843
  383. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_205 line 845
  384. def OAI.SnakyPrototype.Certificate21.checked_205 line 849
  385. def OAI.SnakyPrototype.Certificate21.height_207 line 857
  386. def OAI.SnakyPrototype.Certificate21.childrenH_207 line 858
  387. theorem OAI.SnakyPrototype.Certificate21.height_exact_207 line 859
  388. theorem OAI.SnakyPrototype.Certificate21.required_origin_207 line 860
  389. theorem OAI.SnakyPrototype.Certificate21.required_exact_207 line 862
  390. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_207 line 866
  391. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_207 line 868
  392. def OAI.SnakyPrototype.Certificate21.checked_207 line 872
  393. def OAI.SnakyPrototype.Certificate21.height_209 line 880
  394. def OAI.SnakyPrototype.Certificate21.childrenH_209 line 881
  395. theorem OAI.SnakyPrototype.Certificate21.height_exact_209 line 882
  396. theorem OAI.SnakyPrototype.Certificate21.required_origin_209 line 883
  397. theorem OAI.SnakyPrototype.Certificate21.required_exact_209 line 885
  398. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_209 line 889
  399. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_209 line 891
  400. def OAI.SnakyPrototype.Certificate21.checked_209 line 895
  401. def OAI.SnakyPrototype.Certificate21.height_212 line 903
  402. def OAI.SnakyPrototype.Certificate21.childrenH_212 line 904
  403. theorem OAI.SnakyPrototype.Certificate21.height_exact_212 line 905
  404. theorem OAI.SnakyPrototype.Certificate21.required_origin_212 line 906
  405. theorem OAI.SnakyPrototype.Certificate21.required_exact_212 line 908
  406. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_212 line 912
  407. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_212 line 914
  408. def OAI.SnakyPrototype.Certificate21.checked_212 line 918
  409. def OAI.SnakyPrototype.Certificate21.height_215 line 926
  410. def OAI.SnakyPrototype.Certificate21.childrenH_215 line 927
  411. theorem OAI.SnakyPrototype.Certificate21.height_exact_215 line 928
  412. theorem OAI.SnakyPrototype.Certificate21.required_origin_215 line 929
  413. theorem OAI.SnakyPrototype.Certificate21.required_exact_215 line 931
  414. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_215 line 935
  415. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_215 line 937
  416. def OAI.SnakyPrototype.Certificate21.checked_215 line 941
  417. def OAI.SnakyPrototype.Certificate21.height_218 line 949
  418. def OAI.SnakyPrototype.Certificate21.childrenH_218 line 950
  419. theorem OAI.SnakyPrototype.Certificate21.height_exact_218 line 951
  420. theorem OAI.SnakyPrototype.Certificate21.required_origin_218 line 952
  421. theorem OAI.SnakyPrototype.Certificate21.required_exact_218 line 954
  422. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_218 line 958
  423. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_218 line 960
  424. def OAI.SnakyPrototype.Certificate21.checked_218 line 964
  425. def OAI.SnakyPrototype.Certificate21.height_219 line 972
  426. def OAI.SnakyPrototype.Certificate21.childrenH_219 line 973
  427. theorem OAI.SnakyPrototype.Certificate21.height_exact_219 line 974
  428. theorem OAI.SnakyPrototype.Certificate21.required_origin_219 line 975
  429. theorem OAI.SnakyPrototype.Certificate21.required_exact_219 line 977
  430. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_219 line 981
  431. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_219 line 983
  432. def OAI.SnakyPrototype.Certificate21.checked_219 line 987