OAI/GameTheory/SnakyTwentyOne/Cards/Height04Part03.lean

GitHub source file

432 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_149 line 13
  2. def OAI.SnakyPrototype.Certificate21.envelope_149 line 14
  3. def OAI.SnakyPrototype.Certificate21.childrenC_149 line 15
  4. def OAI.SnakyPrototype.Certificate21.childrenD_149 line 16
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_149 line 17
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_149 line 18
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_149 line 19
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_149 line 20
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_149 line 21
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_149 line 26
  11. def OAI.SnakyPrototype.Certificate21.required_150 line 31
  12. def OAI.SnakyPrototype.Certificate21.envelope_150 line 32
  13. def OAI.SnakyPrototype.Certificate21.childrenC_150 line 33
  14. def OAI.SnakyPrototype.Certificate21.childrenD_150 line 34
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_150 line 35
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_150 line 36
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_150 line 37
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_150 line 38
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_150 line 39
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_150 line 44
  21. def OAI.SnakyPrototype.Certificate21.required_151 line 49
  22. def OAI.SnakyPrototype.Certificate21.envelope_151 line 50
  23. def OAI.SnakyPrototype.Certificate21.childrenC_151 line 51
  24. def OAI.SnakyPrototype.Certificate21.childrenD_151 line 52
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_151 line 53
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_151 line 54
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_151 line 55
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_151 line 56
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_151 line 57
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_151 line 62
  31. def OAI.SnakyPrototype.Certificate21.required_165 line 67
  32. def OAI.SnakyPrototype.Certificate21.envelope_165 line 68
  33. def OAI.SnakyPrototype.Certificate21.childrenC_165 line 69
  34. def OAI.SnakyPrototype.Certificate21.childrenD_165 line 70
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_165 line 71
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_165 line 72
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_165 line 73
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_165 line 74
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_165 line 75
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_165 line 80
  41. def OAI.SnakyPrototype.Certificate21.required_168 line 85
  42. def OAI.SnakyPrototype.Certificate21.envelope_168 line 86
  43. def OAI.SnakyPrototype.Certificate21.childrenC_168 line 87
  44. def OAI.SnakyPrototype.Certificate21.childrenD_168 line 88
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_168 line 89
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_168 line 90
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_168 line 91
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_168 line 92
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_168 line 93
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_168 line 98
  51. def OAI.SnakyPrototype.Certificate21.required_178 line 103
  52. def OAI.SnakyPrototype.Certificate21.envelope_178 line 104
  53. def OAI.SnakyPrototype.Certificate21.childrenC_178 line 105
  54. def OAI.SnakyPrototype.Certificate21.childrenD_178 line 106
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_178 line 107
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_178 line 108
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_178 line 109
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_178 line 110
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_178 line 111
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_178 line 116
  61. def OAI.SnakyPrototype.Certificate21.required_185 line 121
  62. def OAI.SnakyPrototype.Certificate21.envelope_185 line 122
  63. def OAI.SnakyPrototype.Certificate21.childrenC_185 line 123
  64. def OAI.SnakyPrototype.Certificate21.childrenD_185 line 124
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_185 line 125
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_185 line 126
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_185 line 127
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_185 line 128
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_185 line 129
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_185 line 134
  71. def OAI.SnakyPrototype.Certificate21.required_194 line 139
  72. def OAI.SnakyPrototype.Certificate21.envelope_194 line 140
  73. def OAI.SnakyPrototype.Certificate21.childrenC_194 line 141
  74. def OAI.SnakyPrototype.Certificate21.childrenD_194 line 142
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_194 line 143
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_194 line 144
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_194 line 145
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_194 line 146
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_194 line 147
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_194 line 152
  81. def OAI.SnakyPrototype.Certificate21.required_195 line 157
  82. def OAI.SnakyPrototype.Certificate21.envelope_195 line 158
  83. def OAI.SnakyPrototype.Certificate21.childrenC_195 line 159
  84. def OAI.SnakyPrototype.Certificate21.childrenD_195 line 160
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_195 line 161
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_195 line 162
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_195 line 163
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_195 line 164
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_195 line 165
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_195 line 170
  91. def OAI.SnakyPrototype.Certificate21.required_196 line 175
  92. def OAI.SnakyPrototype.Certificate21.envelope_196 line 176
  93. def OAI.SnakyPrototype.Certificate21.childrenC_196 line 177
  94. def OAI.SnakyPrototype.Certificate21.childrenD_196 line 178
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_196 line 179
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_196 line 180
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_196 line 181
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_196 line 182
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_196 line 183
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_196 line 188
  101. def OAI.SnakyPrototype.Certificate21.required_199 line 193
  102. def OAI.SnakyPrototype.Certificate21.envelope_199 line 194
  103. def OAI.SnakyPrototype.Certificate21.childrenC_199 line 195
  104. def OAI.SnakyPrototype.Certificate21.childrenD_199 line 196
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_199 line 197
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_199 line 198
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_199 line 199
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_199 line 200
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_199 line 201
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_199 line 206
  111. def OAI.SnakyPrototype.Certificate21.required_206 line 211
  112. def OAI.SnakyPrototype.Certificate21.envelope_206 line 212
  113. def OAI.SnakyPrototype.Certificate21.childrenC_206 line 213
  114. def OAI.SnakyPrototype.Certificate21.childrenD_206 line 214
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_206 line 215
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_206 line 216
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_206 line 217
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_206 line 218
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_206 line 219
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_206 line 224
  121. def OAI.SnakyPrototype.Certificate21.required_208 line 229
  122. def OAI.SnakyPrototype.Certificate21.envelope_208 line 230
  123. def OAI.SnakyPrototype.Certificate21.childrenC_208 line 231
  124. def OAI.SnakyPrototype.Certificate21.childrenD_208 line 232
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_208 line 233
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_208 line 234
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_208 line 235
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_208 line 236
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_208 line 237
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_208 line 242
  131. def OAI.SnakyPrototype.Certificate21.required_213 line 247
  132. def OAI.SnakyPrototype.Certificate21.envelope_213 line 248
  133. def OAI.SnakyPrototype.Certificate21.childrenC_213 line 249
  134. def OAI.SnakyPrototype.Certificate21.childrenD_213 line 250
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_213 line 251
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_213 line 252
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_213 line 253
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_213 line 254
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_213 line 255
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_213 line 261
  141. def OAI.SnakyPrototype.Certificate21.required_216 line 266
  142. def OAI.SnakyPrototype.Certificate21.envelope_216 line 267
  143. def OAI.SnakyPrototype.Certificate21.childrenC_216 line 268
  144. def OAI.SnakyPrototype.Certificate21.childrenD_216 line 269
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_216 line 270
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_216 line 271
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_216 line 272
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_216 line 273
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_216 line 274
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_216 line 279
  151. def OAI.SnakyPrototype.Certificate21.required_227 line 284
  152. def OAI.SnakyPrototype.Certificate21.envelope_227 line 285
  153. def OAI.SnakyPrototype.Certificate21.childrenC_227 line 286
  154. def OAI.SnakyPrototype.Certificate21.childrenD_227 line 287
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_227 line 288
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_227 line 289
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_227 line 290
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_227 line 291
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_227 line 292
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_227 line 297
  161. def OAI.SnakyPrototype.Certificate21.required_229 line 302
  162. def OAI.SnakyPrototype.Certificate21.envelope_229 line 303
  163. def OAI.SnakyPrototype.Certificate21.childrenC_229 line 304
  164. def OAI.SnakyPrototype.Certificate21.childrenD_229 line 305
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_229 line 306
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_229 line 307
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_229 line 308
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_229 line 309
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_229 line 310
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_229 line 315
  171. def OAI.SnakyPrototype.Certificate21.required_235 line 320
  172. def OAI.SnakyPrototype.Certificate21.envelope_235 line 321
  173. def OAI.SnakyPrototype.Certificate21.childrenC_235 line 322
  174. def OAI.SnakyPrototype.Certificate21.childrenD_235 line 323
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_235 line 324
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_235 line 325
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_235 line 326
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_235 line 327
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_235 line 328
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_235 line 333
  181. def OAI.SnakyPrototype.Certificate21.required_240 line 338
  182. def OAI.SnakyPrototype.Certificate21.envelope_240 line 339
  183. def OAI.SnakyPrototype.Certificate21.childrenC_240 line 340
  184. def OAI.SnakyPrototype.Certificate21.childrenD_240 line 341
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_240 line 342
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_240 line 343
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_240 line 344
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_240 line 345
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_240 line 346
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_240 line 351
  191. def OAI.SnakyPrototype.Certificate21.required_242 line 356
  192. def OAI.SnakyPrototype.Certificate21.envelope_242 line 357
  193. def OAI.SnakyPrototype.Certificate21.childrenC_242 line 358
  194. def OAI.SnakyPrototype.Certificate21.childrenD_242 line 359
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_242 line 360
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_242 line 361
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_242 line 362
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_242 line 363
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_242 line 364
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_242 line 369
  201. def OAI.SnakyPrototype.Certificate21.required_259 line 374
  202. def OAI.SnakyPrototype.Certificate21.envelope_259 line 375
  203. def OAI.SnakyPrototype.Certificate21.childrenC_259 line 376
  204. def OAI.SnakyPrototype.Certificate21.childrenD_259 line 377
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_259 line 378
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_259 line 379
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_259 line 380
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_259 line 381
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_259 line 382
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_259 line 387
  211. def OAI.SnakyPrototype.Certificate21.required_263 line 392
  212. def OAI.SnakyPrototype.Certificate21.envelope_263 line 393
  213. def OAI.SnakyPrototype.Certificate21.childrenC_263 line 394
  214. def OAI.SnakyPrototype.Certificate21.childrenD_263 line 395
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_263 line 396
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_263 line 397
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_263 line 398
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_263 line 399
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_263 line 400
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_263 line 406
  221. def OAI.SnakyPrototype.Certificate21.required_264 line 411
  222. def OAI.SnakyPrototype.Certificate21.envelope_264 line 412
  223. def OAI.SnakyPrototype.Certificate21.childrenC_264 line 413
  224. def OAI.SnakyPrototype.Certificate21.childrenD_264 line 414
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_264 line 415
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_264 line 416
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_264 line 417
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_264 line 418
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_264 line 419
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_264 line 424
  231. def OAI.SnakyPrototype.Certificate21.required_266 line 429
  232. def OAI.SnakyPrototype.Certificate21.envelope_266 line 430
  233. def OAI.SnakyPrototype.Certificate21.childrenC_266 line 431
  234. def OAI.SnakyPrototype.Certificate21.childrenD_266 line 432
  235. theorem OAI.SnakyPrototype.Certificate21.common_sub_266 line 433
  236. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_266 line 434
  237. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_266 line 435
  238. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_266 line 436
  239. theorem OAI.SnakyPrototype.Certificate21.children_work_266 line 437
  240. theorem OAI.SnakyPrototype.Certificate21.row_works_266 line 443
  241. def OAI.SnakyPrototype.Certificate21.height_149 line 448
  242. def OAI.SnakyPrototype.Certificate21.childrenH_149 line 449
  243. theorem OAI.SnakyPrototype.Certificate21.height_exact_149 line 450
  244. theorem OAI.SnakyPrototype.Certificate21.required_origin_149 line 451
  245. theorem OAI.SnakyPrototype.Certificate21.required_exact_149 line 453
  246. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_149 line 457
  247. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_149 line 459
  248. def OAI.SnakyPrototype.Certificate21.checked_149 line 463
  249. def OAI.SnakyPrototype.Certificate21.height_150 line 471
  250. def OAI.SnakyPrototype.Certificate21.childrenH_150 line 472
  251. theorem OAI.SnakyPrototype.Certificate21.height_exact_150 line 473
  252. theorem OAI.SnakyPrototype.Certificate21.required_origin_150 line 474
  253. theorem OAI.SnakyPrototype.Certificate21.required_exact_150 line 476
  254. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_150 line 480
  255. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_150 line 482
  256. def OAI.SnakyPrototype.Certificate21.checked_150 line 486
  257. def OAI.SnakyPrototype.Certificate21.height_151 line 494
  258. def OAI.SnakyPrototype.Certificate21.childrenH_151 line 495
  259. theorem OAI.SnakyPrototype.Certificate21.height_exact_151 line 496
  260. theorem OAI.SnakyPrototype.Certificate21.required_origin_151 line 497
  261. theorem OAI.SnakyPrototype.Certificate21.required_exact_151 line 499
  262. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_151 line 503
  263. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_151 line 505
  264. def OAI.SnakyPrototype.Certificate21.checked_151 line 509
  265. def OAI.SnakyPrototype.Certificate21.height_165 line 517
  266. def OAI.SnakyPrototype.Certificate21.childrenH_165 line 518
  267. theorem OAI.SnakyPrototype.Certificate21.height_exact_165 line 519
  268. theorem OAI.SnakyPrototype.Certificate21.required_origin_165 line 520
  269. theorem OAI.SnakyPrototype.Certificate21.required_exact_165 line 522
  270. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_165 line 526
  271. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_165 line 528
  272. def OAI.SnakyPrototype.Certificate21.checked_165 line 532
  273. def OAI.SnakyPrototype.Certificate21.height_168 line 540
  274. def OAI.SnakyPrototype.Certificate21.childrenH_168 line 541
  275. theorem OAI.SnakyPrototype.Certificate21.height_exact_168 line 542
  276. theorem OAI.SnakyPrototype.Certificate21.required_origin_168 line 543
  277. theorem OAI.SnakyPrototype.Certificate21.required_exact_168 line 545
  278. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_168 line 549
  279. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_168 line 551
  280. def OAI.SnakyPrototype.Certificate21.checked_168 line 555
  281. def OAI.SnakyPrototype.Certificate21.height_178 line 563
  282. def OAI.SnakyPrototype.Certificate21.childrenH_178 line 564
  283. theorem OAI.SnakyPrototype.Certificate21.height_exact_178 line 565
  284. theorem OAI.SnakyPrototype.Certificate21.required_origin_178 line 566
  285. theorem OAI.SnakyPrototype.Certificate21.required_exact_178 line 568
  286. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_178 line 572
  287. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_178 line 574
  288. def OAI.SnakyPrototype.Certificate21.checked_178 line 578
  289. def OAI.SnakyPrototype.Certificate21.height_185 line 586
  290. def OAI.SnakyPrototype.Certificate21.childrenH_185 line 587
  291. theorem OAI.SnakyPrototype.Certificate21.height_exact_185 line 588
  292. theorem OAI.SnakyPrototype.Certificate21.required_origin_185 line 589
  293. theorem OAI.SnakyPrototype.Certificate21.required_exact_185 line 591
  294. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_185 line 595
  295. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_185 line 597
  296. def OAI.SnakyPrototype.Certificate21.checked_185 line 601
  297. def OAI.SnakyPrototype.Certificate21.height_194 line 609
  298. def OAI.SnakyPrototype.Certificate21.childrenH_194 line 610
  299. theorem OAI.SnakyPrototype.Certificate21.height_exact_194 line 611
  300. theorem OAI.SnakyPrototype.Certificate21.required_origin_194 line 612
  301. theorem OAI.SnakyPrototype.Certificate21.required_exact_194 line 614
  302. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_194 line 618
  303. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_194 line 620
  304. def OAI.SnakyPrototype.Certificate21.checked_194 line 624
  305. def OAI.SnakyPrototype.Certificate21.height_195 line 632
  306. def OAI.SnakyPrototype.Certificate21.childrenH_195 line 633
  307. theorem OAI.SnakyPrototype.Certificate21.height_exact_195 line 634
  308. theorem OAI.SnakyPrototype.Certificate21.required_origin_195 line 635
  309. theorem OAI.SnakyPrototype.Certificate21.required_exact_195 line 637
  310. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_195 line 641
  311. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_195 line 643
  312. def OAI.SnakyPrototype.Certificate21.checked_195 line 647
  313. def OAI.SnakyPrototype.Certificate21.height_196 line 655
  314. def OAI.SnakyPrototype.Certificate21.childrenH_196 line 656
  315. theorem OAI.SnakyPrototype.Certificate21.height_exact_196 line 657
  316. theorem OAI.SnakyPrototype.Certificate21.required_origin_196 line 658
  317. theorem OAI.SnakyPrototype.Certificate21.required_exact_196 line 660
  318. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_196 line 664
  319. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_196 line 666
  320. def OAI.SnakyPrototype.Certificate21.checked_196 line 670
  321. def OAI.SnakyPrototype.Certificate21.height_199 line 678
  322. def OAI.SnakyPrototype.Certificate21.childrenH_199 line 679
  323. theorem OAI.SnakyPrototype.Certificate21.height_exact_199 line 680
  324. theorem OAI.SnakyPrototype.Certificate21.required_origin_199 line 681
  325. theorem OAI.SnakyPrototype.Certificate21.required_exact_199 line 683
  326. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_199 line 687
  327. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_199 line 689
  328. def OAI.SnakyPrototype.Certificate21.checked_199 line 693
  329. def OAI.SnakyPrototype.Certificate21.height_206 line 701
  330. def OAI.SnakyPrototype.Certificate21.childrenH_206 line 702
  331. theorem OAI.SnakyPrototype.Certificate21.height_exact_206 line 703
  332. theorem OAI.SnakyPrototype.Certificate21.required_origin_206 line 704
  333. theorem OAI.SnakyPrototype.Certificate21.required_exact_206 line 706
  334. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_206 line 710
  335. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_206 line 712
  336. def OAI.SnakyPrototype.Certificate21.checked_206 line 716
  337. def OAI.SnakyPrototype.Certificate21.height_208 line 724
  338. def OAI.SnakyPrototype.Certificate21.childrenH_208 line 725
  339. theorem OAI.SnakyPrototype.Certificate21.height_exact_208 line 726
  340. theorem OAI.SnakyPrototype.Certificate21.required_origin_208 line 727
  341. theorem OAI.SnakyPrototype.Certificate21.required_exact_208 line 729
  342. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_208 line 733
  343. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_208 line 735
  344. def OAI.SnakyPrototype.Certificate21.checked_208 line 739
  345. def OAI.SnakyPrototype.Certificate21.height_213 line 747
  346. def OAI.SnakyPrototype.Certificate21.childrenH_213 line 748
  347. theorem OAI.SnakyPrototype.Certificate21.height_exact_213 line 749
  348. theorem OAI.SnakyPrototype.Certificate21.required_origin_213 line 750
  349. theorem OAI.SnakyPrototype.Certificate21.required_exact_213 line 752
  350. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_213 line 756
  351. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_213 line 758
  352. def OAI.SnakyPrototype.Certificate21.checked_213 line 762
  353. def OAI.SnakyPrototype.Certificate21.height_216 line 770
  354. def OAI.SnakyPrototype.Certificate21.childrenH_216 line 771
  355. theorem OAI.SnakyPrototype.Certificate21.height_exact_216 line 772
  356. theorem OAI.SnakyPrototype.Certificate21.required_origin_216 line 773
  357. theorem OAI.SnakyPrototype.Certificate21.required_exact_216 line 775
  358. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_216 line 779
  359. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_216 line 781
  360. def OAI.SnakyPrototype.Certificate21.checked_216 line 785
  361. def OAI.SnakyPrototype.Certificate21.height_227 line 793
  362. def OAI.SnakyPrototype.Certificate21.childrenH_227 line 794
  363. theorem OAI.SnakyPrototype.Certificate21.height_exact_227 line 795
  364. theorem OAI.SnakyPrototype.Certificate21.required_origin_227 line 796
  365. theorem OAI.SnakyPrototype.Certificate21.required_exact_227 line 798
  366. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_227 line 802
  367. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_227 line 804
  368. def OAI.SnakyPrototype.Certificate21.checked_227 line 808
  369. def OAI.SnakyPrototype.Certificate21.height_229 line 816
  370. def OAI.SnakyPrototype.Certificate21.childrenH_229 line 817
  371. theorem OAI.SnakyPrototype.Certificate21.height_exact_229 line 818
  372. theorem OAI.SnakyPrototype.Certificate21.required_origin_229 line 819
  373. theorem OAI.SnakyPrototype.Certificate21.required_exact_229 line 821
  374. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_229 line 825
  375. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_229 line 827
  376. def OAI.SnakyPrototype.Certificate21.checked_229 line 831
  377. def OAI.SnakyPrototype.Certificate21.height_235 line 839
  378. def OAI.SnakyPrototype.Certificate21.childrenH_235 line 840
  379. theorem OAI.SnakyPrototype.Certificate21.height_exact_235 line 841
  380. theorem OAI.SnakyPrototype.Certificate21.required_origin_235 line 842
  381. theorem OAI.SnakyPrototype.Certificate21.required_exact_235 line 844
  382. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_235 line 848
  383. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_235 line 850
  384. def OAI.SnakyPrototype.Certificate21.checked_235 line 854
  385. def OAI.SnakyPrototype.Certificate21.height_240 line 862
  386. def OAI.SnakyPrototype.Certificate21.childrenH_240 line 863
  387. theorem OAI.SnakyPrototype.Certificate21.height_exact_240 line 864
  388. theorem OAI.SnakyPrototype.Certificate21.required_origin_240 line 865
  389. theorem OAI.SnakyPrototype.Certificate21.required_exact_240 line 867
  390. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_240 line 871
  391. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_240 line 873
  392. def OAI.SnakyPrototype.Certificate21.checked_240 line 877
  393. def OAI.SnakyPrototype.Certificate21.height_242 line 885
  394. def OAI.SnakyPrototype.Certificate21.childrenH_242 line 886
  395. theorem OAI.SnakyPrototype.Certificate21.height_exact_242 line 887
  396. theorem OAI.SnakyPrototype.Certificate21.required_origin_242 line 888
  397. theorem OAI.SnakyPrototype.Certificate21.required_exact_242 line 890
  398. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_242 line 894
  399. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_242 line 896
  400. def OAI.SnakyPrototype.Certificate21.checked_242 line 900
  401. def OAI.SnakyPrototype.Certificate21.height_259 line 908
  402. def OAI.SnakyPrototype.Certificate21.childrenH_259 line 909
  403. theorem OAI.SnakyPrototype.Certificate21.height_exact_259 line 910
  404. theorem OAI.SnakyPrototype.Certificate21.required_origin_259 line 911
  405. theorem OAI.SnakyPrototype.Certificate21.required_exact_259 line 913
  406. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_259 line 917
  407. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_259 line 919
  408. def OAI.SnakyPrototype.Certificate21.checked_259 line 923
  409. def OAI.SnakyPrototype.Certificate21.height_263 line 931
  410. def OAI.SnakyPrototype.Certificate21.childrenH_263 line 932
  411. theorem OAI.SnakyPrototype.Certificate21.height_exact_263 line 933
  412. theorem OAI.SnakyPrototype.Certificate21.required_origin_263 line 934
  413. theorem OAI.SnakyPrototype.Certificate21.required_exact_263 line 936
  414. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_263 line 940
  415. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_263 line 942
  416. def OAI.SnakyPrototype.Certificate21.checked_263 line 946
  417. def OAI.SnakyPrototype.Certificate21.height_264 line 954
  418. def OAI.SnakyPrototype.Certificate21.childrenH_264 line 955
  419. theorem OAI.SnakyPrototype.Certificate21.height_exact_264 line 956
  420. theorem OAI.SnakyPrototype.Certificate21.required_origin_264 line 957
  421. theorem OAI.SnakyPrototype.Certificate21.required_exact_264 line 959
  422. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_264 line 963
  423. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_264 line 965
  424. def OAI.SnakyPrototype.Certificate21.checked_264 line 969
  425. def OAI.SnakyPrototype.Certificate21.height_266 line 977
  426. def OAI.SnakyPrototype.Certificate21.childrenH_266 line 978
  427. theorem OAI.SnakyPrototype.Certificate21.height_exact_266 line 979
  428. theorem OAI.SnakyPrototype.Certificate21.required_origin_266 line 980
  429. theorem OAI.SnakyPrototype.Certificate21.required_exact_266 line 982
  430. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_266 line 986
  431. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_266 line 988
  432. def OAI.SnakyPrototype.Certificate21.checked_266 line 992