OAI/GameTheory/SnakyTwentyOne/Cards/Height06Part02.lean

GitHub source file

414 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_193 line 19
  2. def OAI.SnakyPrototype.Certificate21.envelope_193 line 20
  3. def OAI.SnakyPrototype.Certificate21.childrenC_193 line 21
  4. def OAI.SnakyPrototype.Certificate21.childrenD_193 line 22
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_193 line 23
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_193 line 24
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_193 line 25
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_193 line 26
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_193 line 27
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_193 line 33
  11. def OAI.SnakyPrototype.Certificate21.required_203 line 38
  12. def OAI.SnakyPrototype.Certificate21.envelope_203 line 39
  13. def OAI.SnakyPrototype.Certificate21.childrenC_203 line 40
  14. def OAI.SnakyPrototype.Certificate21.childrenD_203 line 41
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_203 line 42
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_203 line 43
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_203 line 44
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_203 line 45
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_203 line 46
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_203 line 51
  21. def OAI.SnakyPrototype.Certificate21.required_217 line 56
  22. def OAI.SnakyPrototype.Certificate21.envelope_217 line 57
  23. def OAI.SnakyPrototype.Certificate21.childrenC_217 line 58
  24. def OAI.SnakyPrototype.Certificate21.childrenD_217 line 59
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_217 line 60
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_217 line 61
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_217 line 62
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_217 line 63
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_217 line 64
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_217 line 70
  31. def OAI.SnakyPrototype.Certificate21.required_238 line 75
  32. def OAI.SnakyPrototype.Certificate21.envelope_238 line 76
  33. def OAI.SnakyPrototype.Certificate21.childrenC_238 line 77
  34. def OAI.SnakyPrototype.Certificate21.childrenD_238 line 78
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_238 line 79
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_238 line 80
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_238 line 81
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_238 line 82
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_238 line 83
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_238 line 88
  41. def OAI.SnakyPrototype.Certificate21.required_248 line 93
  42. def OAI.SnakyPrototype.Certificate21.envelope_248 line 94
  43. def OAI.SnakyPrototype.Certificate21.childrenC_248 line 95
  44. def OAI.SnakyPrototype.Certificate21.childrenD_248 line 96
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_248 line 97
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_248 line 98
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_248 line 99
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_248 line 100
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_248 line 101
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_248 line 107
  51. def OAI.SnakyPrototype.Certificate21.required_253 line 112
  52. def OAI.SnakyPrototype.Certificate21.envelope_253 line 113
  53. def OAI.SnakyPrototype.Certificate21.childrenC_253 line 114
  54. def OAI.SnakyPrototype.Certificate21.childrenD_253 line 115
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_253 line 116
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_253 line 117
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_253 line 118
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_253 line 119
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_253 line 120
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_253 line 126
  61. def OAI.SnakyPrototype.Certificate21.required_255 line 131
  62. def OAI.SnakyPrototype.Certificate21.envelope_255 line 132
  63. def OAI.SnakyPrototype.Certificate21.childrenC_255 line 133
  64. def OAI.SnakyPrototype.Certificate21.childrenD_255 line 134
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_255 line 135
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_255 line 136
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_255 line 137
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_255 line 138
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_255 line 139
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_255 line 144
  71. def OAI.SnakyPrototype.Certificate21.required_267 line 149
  72. def OAI.SnakyPrototype.Certificate21.envelope_267 line 150
  73. def OAI.SnakyPrototype.Certificate21.childrenC_267 line 151
  74. def OAI.SnakyPrototype.Certificate21.childrenD_267 line 152
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_267 line 153
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_267 line 154
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_267 line 155
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_267 line 156
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_267 line 157
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_267 line 165
  81. def OAI.SnakyPrototype.Certificate21.required_270 line 170
  82. def OAI.SnakyPrototype.Certificate21.envelope_270 line 171
  83. def OAI.SnakyPrototype.Certificate21.childrenC_270 line 172
  84. def OAI.SnakyPrototype.Certificate21.childrenD_270 line 173
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_270 line 174
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_270 line 175
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_270 line 176
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_270 line 177
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_270 line 178
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_270 line 185
  91. def OAI.SnakyPrototype.Certificate21.required_275 line 190
  92. def OAI.SnakyPrototype.Certificate21.envelope_275 line 191
  93. def OAI.SnakyPrototype.Certificate21.childrenC_275 line 192
  94. def OAI.SnakyPrototype.Certificate21.childrenD_275 line 193
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_275 line 194
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_275 line 195
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_275 line 196
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_275 line 197
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_275 line 198
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_275 line 204
  101. def OAI.SnakyPrototype.Certificate21.required_283 line 209
  102. def OAI.SnakyPrototype.Certificate21.envelope_283 line 210
  103. def OAI.SnakyPrototype.Certificate21.childrenC_283 line 211
  104. def OAI.SnakyPrototype.Certificate21.childrenD_283 line 212
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_283 line 213
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_283 line 214
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_283 line 215
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_283 line 216
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_283 line 217
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_283 line 222
  111. def OAI.SnakyPrototype.Certificate21.required_284 line 227
  112. def OAI.SnakyPrototype.Certificate21.envelope_284 line 228
  113. def OAI.SnakyPrototype.Certificate21.childrenC_284 line 229
  114. def OAI.SnakyPrototype.Certificate21.childrenD_284 line 230
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_284 line 231
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_284 line 232
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_284 line 233
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_284 line 234
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_284 line 235
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_284 line 242
  121. def OAI.SnakyPrototype.Certificate21.required_287 line 247
  122. def OAI.SnakyPrototype.Certificate21.envelope_287 line 248
  123. def OAI.SnakyPrototype.Certificate21.childrenC_287 line 249
  124. def OAI.SnakyPrototype.Certificate21.childrenD_287 line 250
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_287 line 251
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_287 line 252
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_287 line 253
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_287 line 254
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_287 line 255
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_287 line 260
  131. def OAI.SnakyPrototype.Certificate21.required_292 line 265
  132. def OAI.SnakyPrototype.Certificate21.envelope_292 line 266
  133. def OAI.SnakyPrototype.Certificate21.childrenC_292 line 267
  134. def OAI.SnakyPrototype.Certificate21.childrenD_292 line 268
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_292 line 269
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_292 line 270
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_292 line 271
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_292 line 272
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_292 line 273
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_292 line 279
  141. def OAI.SnakyPrototype.Certificate21.required_300 line 284
  142. def OAI.SnakyPrototype.Certificate21.envelope_300 line 285
  143. def OAI.SnakyPrototype.Certificate21.childrenC_300 line 286
  144. def OAI.SnakyPrototype.Certificate21.childrenD_300 line 287
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_300 line 288
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_300 line 289
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_300 line 290
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_300 line 291
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_300 line 292
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_300 line 299
  151. def OAI.SnakyPrototype.Certificate21.required_302 line 304
  152. def OAI.SnakyPrototype.Certificate21.envelope_302 line 305
  153. def OAI.SnakyPrototype.Certificate21.childrenC_302 line 306
  154. def OAI.SnakyPrototype.Certificate21.childrenD_302 line 307
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_302 line 308
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_302 line 309
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_302 line 310
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_302 line 311
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_302 line 312
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_302 line 317
  161. def OAI.SnakyPrototype.Certificate21.required_303 line 322
  162. def OAI.SnakyPrototype.Certificate21.envelope_303 line 323
  163. def OAI.SnakyPrototype.Certificate21.childrenC_303 line 324
  164. def OAI.SnakyPrototype.Certificate21.childrenD_303 line 325
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_303 line 326
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_303 line 327
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_303 line 328
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_303 line 329
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_303 line 330
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_303 line 335
  171. def OAI.SnakyPrototype.Certificate21.required_313 line 340
  172. def OAI.SnakyPrototype.Certificate21.envelope_313 line 341
  173. def OAI.SnakyPrototype.Certificate21.childrenC_313 line 342
  174. def OAI.SnakyPrototype.Certificate21.childrenD_313 line 343
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_313 line 344
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_313 line 345
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_313 line 346
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_313 line 347
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_313 line 348
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_313 line 353
  181. def OAI.SnakyPrototype.Certificate21.required_315 line 358
  182. def OAI.SnakyPrototype.Certificate21.envelope_315 line 359
  183. def OAI.SnakyPrototype.Certificate21.childrenC_315 line 360
  184. def OAI.SnakyPrototype.Certificate21.childrenD_315 line 361
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_315 line 362
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_315 line 363
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_315 line 364
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_315 line 365
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_315 line 366
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_315 line 371
  191. def OAI.SnakyPrototype.Certificate21.required_316 line 376
  192. def OAI.SnakyPrototype.Certificate21.envelope_316 line 377
  193. def OAI.SnakyPrototype.Certificate21.childrenC_316 line 378
  194. def OAI.SnakyPrototype.Certificate21.childrenD_316 line 379
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_316 line 380
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_316 line 381
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_316 line 382
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_316 line 383
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_316 line 384
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_316 line 389
  201. def OAI.SnakyPrototype.Certificate21.required_331_i1 line 394
  202. def OAI.SnakyPrototype.Certificate21.envelope_331_i1 line 395
  203. def OAI.SnakyPrototype.Certificate21.childrenC_331_i1 line 396
  204. def OAI.SnakyPrototype.Certificate21.childrenD_331_i1 line 397
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_331_i1 line 398
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_331_i1 line 399
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_331_i1 line 400
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_331_i1 line 401
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_331_i1 line 402
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_331_i1 line 407
  211. def OAI.SnakyPrototype.Certificate21.required_331_i0 line 412
  212. def OAI.SnakyPrototype.Certificate21.envelope_331_i0 line 413
  213. def OAI.SnakyPrototype.Certificate21.childrenC_331_i0 line 414
  214. def OAI.SnakyPrototype.Certificate21.childrenD_331_i0 line 415
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_331_i0 line 416
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_331_i0 line 417
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_331_i0 line 418
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_331_i0 line 419
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_331_i0 line 420
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_331_i0 line 425
  221. def OAI.SnakyPrototype.Certificate21.required_331 line 430
  222. def OAI.SnakyPrototype.Certificate21.envelope_331 line 431
  223. def OAI.SnakyPrototype.Certificate21.childrenC_331 line 432
  224. def OAI.SnakyPrototype.Certificate21.childrenD_331 line 433
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_331 line 434
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_331 line 435
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_331 line 436
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_331 line 437
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_331 line 438
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_331 line 443
  231. def OAI.SnakyPrototype.Certificate21.height_193 line 448
  232. def OAI.SnakyPrototype.Certificate21.childrenH_193 line 449
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_193 line 450
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_193 line 451
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_193 line 453
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_193 line 457
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_193 line 459
  238. def OAI.SnakyPrototype.Certificate21.checked_193 line 463
  239. def OAI.SnakyPrototype.Certificate21.height_203 line 471
  240. def OAI.SnakyPrototype.Certificate21.childrenH_203 line 472
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_203 line 473
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_203 line 474
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_203 line 476
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_203 line 480
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_203 line 482
  246. def OAI.SnakyPrototype.Certificate21.checked_203 line 486
  247. def OAI.SnakyPrototype.Certificate21.height_217 line 494
  248. def OAI.SnakyPrototype.Certificate21.childrenH_217 line 495
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_217 line 496
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_217 line 497
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_217 line 499
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_217 line 503
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_217 line 505
  254. def OAI.SnakyPrototype.Certificate21.checked_217 line 509
  255. def OAI.SnakyPrototype.Certificate21.height_238 line 517
  256. def OAI.SnakyPrototype.Certificate21.childrenH_238 line 518
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_238 line 519
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_238 line 520
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_238 line 522
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_238 line 526
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_238 line 528
  262. def OAI.SnakyPrototype.Certificate21.checked_238 line 532
  263. def OAI.SnakyPrototype.Certificate21.height_248 line 540
  264. def OAI.SnakyPrototype.Certificate21.childrenH_248 line 541
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_248 line 542
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_248 line 543
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_248 line 545
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_248 line 549
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_248 line 551
  270. def OAI.SnakyPrototype.Certificate21.checked_248 line 555
  271. def OAI.SnakyPrototype.Certificate21.height_253 line 563
  272. def OAI.SnakyPrototype.Certificate21.childrenH_253 line 564
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_253 line 565
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_253 line 566
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_253 line 568
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_253 line 572
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_253 line 574
  278. def OAI.SnakyPrototype.Certificate21.checked_253 line 578
  279. def OAI.SnakyPrototype.Certificate21.height_255 line 586
  280. def OAI.SnakyPrototype.Certificate21.childrenH_255 line 587
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_255 line 588
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_255 line 589
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_255 line 591
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_255 line 595
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_255 line 597
  286. def OAI.SnakyPrototype.Certificate21.checked_255 line 601
  287. def OAI.SnakyPrototype.Certificate21.height_267 line 609
  288. def OAI.SnakyPrototype.Certificate21.childrenH_267 line 610
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_267 line 611
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_267 line 612
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_267 line 614
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_267 line 618
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_267 line 620
  294. def OAI.SnakyPrototype.Certificate21.checked_267 line 624
  295. def OAI.SnakyPrototype.Certificate21.height_270 line 632
  296. def OAI.SnakyPrototype.Certificate21.childrenH_270 line 633
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_270 line 634
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_270 line 635
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_270 line 637
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_270 line 641
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_270 line 643
  302. def OAI.SnakyPrototype.Certificate21.checked_270 line 647
  303. def OAI.SnakyPrototype.Certificate21.height_275 line 655
  304. def OAI.SnakyPrototype.Certificate21.childrenH_275 line 656
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_275 line 657
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_275 line 658
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_275 line 660
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_275 line 664
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_275 line 666
  310. def OAI.SnakyPrototype.Certificate21.checked_275 line 670
  311. def OAI.SnakyPrototype.Certificate21.height_283 line 678
  312. def OAI.SnakyPrototype.Certificate21.childrenH_283 line 679
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_283 line 680
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_283 line 681
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_283 line 683
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_283 line 687
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_283 line 689
  318. def OAI.SnakyPrototype.Certificate21.checked_283 line 693
  319. def OAI.SnakyPrototype.Certificate21.height_284 line 701
  320. def OAI.SnakyPrototype.Certificate21.childrenH_284 line 702
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_284 line 703
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_284 line 704
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_284 line 706
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_284 line 710
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_284 line 712
  326. def OAI.SnakyPrototype.Certificate21.checked_284 line 716
  327. def OAI.SnakyPrototype.Certificate21.height_287 line 724
  328. def OAI.SnakyPrototype.Certificate21.childrenH_287 line 725
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_287 line 726
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_287 line 727
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_287 line 729
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_287 line 733
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_287 line 735
  334. def OAI.SnakyPrototype.Certificate21.checked_287 line 739
  335. def OAI.SnakyPrototype.Certificate21.height_292 line 747
  336. def OAI.SnakyPrototype.Certificate21.childrenH_292 line 748
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_292 line 749
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_292 line 750
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_292 line 752
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_292 line 756
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_292 line 758
  342. def OAI.SnakyPrototype.Certificate21.checked_292 line 762
  343. def OAI.SnakyPrototype.Certificate21.height_300 line 770
  344. def OAI.SnakyPrototype.Certificate21.childrenH_300 line 771
  345. theorem OAI.SnakyPrototype.Certificate21.height_exact_300 line 772
  346. theorem OAI.SnakyPrototype.Certificate21.required_origin_300 line 773
  347. theorem OAI.SnakyPrototype.Certificate21.required_exact_300 line 775
  348. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_300 line 779
  349. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_300 line 781
  350. def OAI.SnakyPrototype.Certificate21.checked_300 line 785
  351. def OAI.SnakyPrototype.Certificate21.height_302 line 793
  352. def OAI.SnakyPrototype.Certificate21.childrenH_302 line 794
  353. theorem OAI.SnakyPrototype.Certificate21.height_exact_302 line 795
  354. theorem OAI.SnakyPrototype.Certificate21.required_origin_302 line 796
  355. theorem OAI.SnakyPrototype.Certificate21.required_exact_302 line 798
  356. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_302 line 802
  357. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_302 line 804
  358. def OAI.SnakyPrototype.Certificate21.checked_302 line 808
  359. def OAI.SnakyPrototype.Certificate21.height_303 line 816
  360. def OAI.SnakyPrototype.Certificate21.childrenH_303 line 817
  361. theorem OAI.SnakyPrototype.Certificate21.height_exact_303 line 818
  362. theorem OAI.SnakyPrototype.Certificate21.required_origin_303 line 819
  363. theorem OAI.SnakyPrototype.Certificate21.required_exact_303 line 821
  364. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_303 line 825
  365. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_303 line 827
  366. def OAI.SnakyPrototype.Certificate21.checked_303 line 831
  367. def OAI.SnakyPrototype.Certificate21.height_313 line 839
  368. def OAI.SnakyPrototype.Certificate21.childrenH_313 line 840
  369. theorem OAI.SnakyPrototype.Certificate21.height_exact_313 line 841
  370. theorem OAI.SnakyPrototype.Certificate21.required_origin_313 line 842
  371. theorem OAI.SnakyPrototype.Certificate21.required_exact_313 line 844
  372. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_313 line 848
  373. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_313 line 850
  374. def OAI.SnakyPrototype.Certificate21.checked_313 line 854
  375. def OAI.SnakyPrototype.Certificate21.height_315 line 862
  376. def OAI.SnakyPrototype.Certificate21.childrenH_315 line 863
  377. theorem OAI.SnakyPrototype.Certificate21.height_exact_315 line 864
  378. theorem OAI.SnakyPrototype.Certificate21.required_origin_315 line 865
  379. theorem OAI.SnakyPrototype.Certificate21.required_exact_315 line 867
  380. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_315 line 871
  381. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_315 line 873
  382. def OAI.SnakyPrototype.Certificate21.checked_315 line 877
  383. def OAI.SnakyPrototype.Certificate21.height_316 line 885
  384. def OAI.SnakyPrototype.Certificate21.childrenH_316 line 886
  385. theorem OAI.SnakyPrototype.Certificate21.height_exact_316 line 887
  386. theorem OAI.SnakyPrototype.Certificate21.required_origin_316 line 888
  387. theorem OAI.SnakyPrototype.Certificate21.required_exact_316 line 890
  388. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_316 line 894
  389. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_316 line 896
  390. def OAI.SnakyPrototype.Certificate21.checked_316 line 900
  391. def OAI.SnakyPrototype.Certificate21.height_331_i1 line 908
  392. def OAI.SnakyPrototype.Certificate21.childrenH_331_i1 line 909
  393. theorem OAI.SnakyPrototype.Certificate21.height_exact_331_i1 line 910
  394. theorem OAI.SnakyPrototype.Certificate21.required_origin_331_i1 line 911
  395. theorem OAI.SnakyPrototype.Certificate21.required_exact_331_i1 line 913
  396. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_331_i1 line 917
  397. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_331_i1 line 919
  398. def OAI.SnakyPrototype.Certificate21.checked_331_i1 line 923
  399. def OAI.SnakyPrototype.Certificate21.height_331_i0 line 931
  400. def OAI.SnakyPrototype.Certificate21.childrenH_331_i0 line 932
  401. theorem OAI.SnakyPrototype.Certificate21.height_exact_331_i0 line 933
  402. theorem OAI.SnakyPrototype.Certificate21.required_origin_331_i0 line 934
  403. theorem OAI.SnakyPrototype.Certificate21.required_exact_331_i0 line 936
  404. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_331_i0 line 940
  405. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_331_i0 line 942
  406. def OAI.SnakyPrototype.Certificate21.checked_331_i0 line 946
  407. def OAI.SnakyPrototype.Certificate21.height_331 line 954
  408. def OAI.SnakyPrototype.Certificate21.childrenH_331 line 955
  409. theorem OAI.SnakyPrototype.Certificate21.height_exact_331 line 956
  410. theorem OAI.SnakyPrototype.Certificate21.required_origin_331 line 957
  411. theorem OAI.SnakyPrototype.Certificate21.required_exact_331 line 959
  412. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_331 line 963
  413. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_331 line 965
  414. def OAI.SnakyPrototype.Certificate21.checked_331 line 969