OAI/GameTheory/SnakyTwentyOne/Cards/Height03Part03.lean

GitHub source file

396 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_221 line 11
  2. def OAI.SnakyPrototype.Certificate21.envelope_221 line 12
  3. def OAI.SnakyPrototype.Certificate21.childrenC_221 line 13
  4. def OAI.SnakyPrototype.Certificate21.childrenD_221 line 14
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_221 line 15
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_221 line 16
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_221 line 17
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_221 line 18
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_221 line 19
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_221 line 24
  11. def OAI.SnakyPrototype.Certificate21.required_222 line 29
  12. def OAI.SnakyPrototype.Certificate21.envelope_222 line 30
  13. def OAI.SnakyPrototype.Certificate21.childrenC_222 line 31
  14. def OAI.SnakyPrototype.Certificate21.childrenD_222 line 32
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_222 line 33
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_222 line 34
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_222 line 35
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_222 line 36
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_222 line 37
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_222 line 42
  21. def OAI.SnakyPrototype.Certificate21.required_223 line 47
  22. def OAI.SnakyPrototype.Certificate21.envelope_223 line 48
  23. def OAI.SnakyPrototype.Certificate21.childrenC_223 line 49
  24. def OAI.SnakyPrototype.Certificate21.childrenD_223 line 50
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_223 line 51
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_223 line 52
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_223 line 53
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_223 line 54
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_223 line 55
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_223 line 60
  31. def OAI.SnakyPrototype.Certificate21.required_226 line 65
  32. def OAI.SnakyPrototype.Certificate21.envelope_226 line 66
  33. def OAI.SnakyPrototype.Certificate21.childrenC_226 line 67
  34. def OAI.SnakyPrototype.Certificate21.childrenD_226 line 68
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_226 line 69
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_226 line 70
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_226 line 71
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_226 line 72
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_226 line 73
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_226 line 78
  41. def OAI.SnakyPrototype.Certificate21.required_236 line 83
  42. def OAI.SnakyPrototype.Certificate21.envelope_236 line 84
  43. def OAI.SnakyPrototype.Certificate21.childrenC_236 line 85
  44. def OAI.SnakyPrototype.Certificate21.childrenD_236 line 86
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_236 line 87
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_236 line 88
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_236 line 89
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_236 line 90
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_236 line 91
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_236 line 96
  51. def OAI.SnakyPrototype.Certificate21.required_239 line 101
  52. def OAI.SnakyPrototype.Certificate21.envelope_239 line 102
  53. def OAI.SnakyPrototype.Certificate21.childrenC_239 line 103
  54. def OAI.SnakyPrototype.Certificate21.childrenD_239 line 104
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_239 line 105
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_239 line 106
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_239 line 107
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_239 line 108
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_239 line 109
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_239 line 114
  61. def OAI.SnakyPrototype.Certificate21.required_245 line 119
  62. def OAI.SnakyPrototype.Certificate21.envelope_245 line 120
  63. def OAI.SnakyPrototype.Certificate21.childrenC_245 line 121
  64. def OAI.SnakyPrototype.Certificate21.childrenD_245 line 122
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_245 line 123
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_245 line 124
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_245 line 125
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_245 line 126
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_245 line 127
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_245 line 132
  71. def OAI.SnakyPrototype.Certificate21.required_246 line 137
  72. def OAI.SnakyPrototype.Certificate21.envelope_246 line 138
  73. def OAI.SnakyPrototype.Certificate21.childrenC_246 line 139
  74. def OAI.SnakyPrototype.Certificate21.childrenD_246 line 140
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_246 line 141
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_246 line 142
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_246 line 143
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_246 line 144
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_246 line 145
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_246 line 150
  81. def OAI.SnakyPrototype.Certificate21.required_247 line 155
  82. def OAI.SnakyPrototype.Certificate21.envelope_247 line 156
  83. def OAI.SnakyPrototype.Certificate21.childrenC_247 line 157
  84. def OAI.SnakyPrototype.Certificate21.childrenD_247 line 158
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_247 line 159
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_247 line 160
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_247 line 161
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_247 line 162
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_247 line 163
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_247 line 168
  91. def OAI.SnakyPrototype.Certificate21.required_251 line 173
  92. def OAI.SnakyPrototype.Certificate21.envelope_251 line 174
  93. def OAI.SnakyPrototype.Certificate21.childrenC_251 line 175
  94. def OAI.SnakyPrototype.Certificate21.childrenD_251 line 176
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_251 line 177
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_251 line 178
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_251 line 179
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_251 line 180
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_251 line 181
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_251 line 186
  101. def OAI.SnakyPrototype.Certificate21.required_261 line 191
  102. def OAI.SnakyPrototype.Certificate21.envelope_261 line 192
  103. def OAI.SnakyPrototype.Certificate21.childrenC_261 line 193
  104. def OAI.SnakyPrototype.Certificate21.childrenD_261 line 194
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_261 line 195
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_261 line 196
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_261 line 197
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_261 line 198
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_261 line 199
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_261 line 204
  111. def OAI.SnakyPrototype.Certificate21.required_262 line 209
  112. def OAI.SnakyPrototype.Certificate21.envelope_262 line 210
  113. def OAI.SnakyPrototype.Certificate21.childrenC_262 line 211
  114. def OAI.SnakyPrototype.Certificate21.childrenD_262 line 212
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_262 line 213
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_262 line 214
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_262 line 215
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_262 line 216
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_262 line 217
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_262 line 222
  121. def OAI.SnakyPrototype.Certificate21.required_280 line 227
  122. def OAI.SnakyPrototype.Certificate21.envelope_280 line 228
  123. def OAI.SnakyPrototype.Certificate21.childrenC_280 line 229
  124. def OAI.SnakyPrototype.Certificate21.childrenD_280 line 230
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_280 line 231
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_280 line 232
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_280 line 233
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_280 line 234
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_280 line 235
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_280 line 240
  131. def OAI.SnakyPrototype.Certificate21.required_310 line 245
  132. def OAI.SnakyPrototype.Certificate21.envelope_310 line 246
  133. def OAI.SnakyPrototype.Certificate21.childrenC_310 line 247
  134. def OAI.SnakyPrototype.Certificate21.childrenD_310 line 248
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_310 line 249
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_310 line 250
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_310 line 251
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_310 line 252
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_310 line 253
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_310 line 258
  141. def OAI.SnakyPrototype.Certificate21.required_333_i0 line 263
  142. def OAI.SnakyPrototype.Certificate21.envelope_333_i0 line 264
  143. def OAI.SnakyPrototype.Certificate21.childrenC_333_i0 line 265
  144. def OAI.SnakyPrototype.Certificate21.childrenD_333_i0 line 266
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_333_i0 line 267
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_333_i0 line 268
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_333_i0 line 269
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_333_i0 line 270
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_333_i0 line 271
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_333_i0 line 276
  151. def OAI.SnakyPrototype.Certificate21.required_333 line 281
  152. def OAI.SnakyPrototype.Certificate21.envelope_333 line 282
  153. def OAI.SnakyPrototype.Certificate21.childrenC_333 line 283
  154. def OAI.SnakyPrototype.Certificate21.childrenD_333 line 284
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_333 line 285
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_333 line 286
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_333 line 287
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_333 line 288
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_333 line 289
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_333 line 294
  161. def OAI.SnakyPrototype.Certificate21.required_350_i0 line 299
  162. def OAI.SnakyPrototype.Certificate21.envelope_350_i0 line 300
  163. def OAI.SnakyPrototype.Certificate21.childrenC_350_i0 line 301
  164. def OAI.SnakyPrototype.Certificate21.childrenD_350_i0 line 302
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_350_i0 line 303
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_350_i0 line 304
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_350_i0 line 305
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_350_i0 line 306
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_350_i0 line 307
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_350_i0 line 312
  171. def OAI.SnakyPrototype.Certificate21.required_350 line 317
  172. def OAI.SnakyPrototype.Certificate21.envelope_350 line 318
  173. def OAI.SnakyPrototype.Certificate21.childrenC_350 line 319
  174. def OAI.SnakyPrototype.Certificate21.childrenD_350 line 320
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_350 line 321
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_350 line 322
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_350 line 323
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_350 line 324
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_350 line 325
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_350 line 330
  181. def OAI.SnakyPrototype.Certificate21.required_374_i0 line 335
  182. def OAI.SnakyPrototype.Certificate21.envelope_374_i0 line 336
  183. def OAI.SnakyPrototype.Certificate21.childrenC_374_i0 line 337
  184. def OAI.SnakyPrototype.Certificate21.childrenD_374_i0 line 338
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_374_i0 line 339
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_374_i0 line 340
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_374_i0 line 341
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_374_i0 line 342
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_374_i0 line 343
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_374_i0 line 348
  191. def OAI.SnakyPrototype.Certificate21.required_374 line 353
  192. def OAI.SnakyPrototype.Certificate21.envelope_374 line 354
  193. def OAI.SnakyPrototype.Certificate21.childrenC_374 line 355
  194. def OAI.SnakyPrototype.Certificate21.childrenD_374 line 356
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_374 line 357
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_374 line 358
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_374 line 359
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_374 line 360
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_374 line 361
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_374 line 366
  201. def OAI.SnakyPrototype.Certificate21.required_402_i0 line 371
  202. def OAI.SnakyPrototype.Certificate21.envelope_402_i0 line 372
  203. def OAI.SnakyPrototype.Certificate21.childrenC_402_i0 line 373
  204. def OAI.SnakyPrototype.Certificate21.childrenD_402_i0 line 374
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_402_i0 line 375
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_402_i0 line 376
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_402_i0 line 377
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_402_i0 line 378
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_402_i0 line 379
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_402_i0 line 384
  211. def OAI.SnakyPrototype.Certificate21.required_402 line 389
  212. def OAI.SnakyPrototype.Certificate21.envelope_402 line 390
  213. def OAI.SnakyPrototype.Certificate21.childrenC_402 line 391
  214. def OAI.SnakyPrototype.Certificate21.childrenD_402 line 392
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_402 line 393
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_402 line 394
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_402 line 395
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_402 line 396
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_402 line 397
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_402 line 402
  221. def OAI.SnakyPrototype.Certificate21.height_221 line 407
  222. def OAI.SnakyPrototype.Certificate21.childrenH_221 line 408
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_221 line 409
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_221 line 410
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_221 line 412
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_221 line 416
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_221 line 418
  228. def OAI.SnakyPrototype.Certificate21.checked_221 line 422
  229. def OAI.SnakyPrototype.Certificate21.height_222 line 430
  230. def OAI.SnakyPrototype.Certificate21.childrenH_222 line 431
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_222 line 432
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_222 line 433
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_222 line 435
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_222 line 439
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_222 line 441
  236. def OAI.SnakyPrototype.Certificate21.checked_222 line 445
  237. def OAI.SnakyPrototype.Certificate21.height_223 line 453
  238. def OAI.SnakyPrototype.Certificate21.childrenH_223 line 454
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_223 line 455
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_223 line 456
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_223 line 458
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_223 line 462
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_223 line 464
  244. def OAI.SnakyPrototype.Certificate21.checked_223 line 468
  245. def OAI.SnakyPrototype.Certificate21.height_226 line 476
  246. def OAI.SnakyPrototype.Certificate21.childrenH_226 line 477
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_226 line 478
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_226 line 479
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_226 line 481
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_226 line 485
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_226 line 487
  252. def OAI.SnakyPrototype.Certificate21.checked_226 line 491
  253. def OAI.SnakyPrototype.Certificate21.height_236 line 499
  254. def OAI.SnakyPrototype.Certificate21.childrenH_236 line 500
  255. theorem OAI.SnakyPrototype.Certificate21.height_exact_236 line 501
  256. theorem OAI.SnakyPrototype.Certificate21.required_origin_236 line 502
  257. theorem OAI.SnakyPrototype.Certificate21.required_exact_236 line 504
  258. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_236 line 508
  259. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_236 line 510
  260. def OAI.SnakyPrototype.Certificate21.checked_236 line 514
  261. def OAI.SnakyPrototype.Certificate21.height_239 line 522
  262. def OAI.SnakyPrototype.Certificate21.childrenH_239 line 523
  263. theorem OAI.SnakyPrototype.Certificate21.height_exact_239 line 524
  264. theorem OAI.SnakyPrototype.Certificate21.required_origin_239 line 525
  265. theorem OAI.SnakyPrototype.Certificate21.required_exact_239 line 527
  266. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_239 line 531
  267. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_239 line 533
  268. def OAI.SnakyPrototype.Certificate21.checked_239 line 537
  269. def OAI.SnakyPrototype.Certificate21.height_245 line 545
  270. def OAI.SnakyPrototype.Certificate21.childrenH_245 line 546
  271. theorem OAI.SnakyPrototype.Certificate21.height_exact_245 line 547
  272. theorem OAI.SnakyPrototype.Certificate21.required_origin_245 line 548
  273. theorem OAI.SnakyPrototype.Certificate21.required_exact_245 line 550
  274. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_245 line 554
  275. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_245 line 556
  276. def OAI.SnakyPrototype.Certificate21.checked_245 line 560
  277. def OAI.SnakyPrototype.Certificate21.height_246 line 568
  278. def OAI.SnakyPrototype.Certificate21.childrenH_246 line 569
  279. theorem OAI.SnakyPrototype.Certificate21.height_exact_246 line 570
  280. theorem OAI.SnakyPrototype.Certificate21.required_origin_246 line 571
  281. theorem OAI.SnakyPrototype.Certificate21.required_exact_246 line 573
  282. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_246 line 577
  283. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_246 line 579
  284. def OAI.SnakyPrototype.Certificate21.checked_246 line 583
  285. def OAI.SnakyPrototype.Certificate21.height_247 line 591
  286. def OAI.SnakyPrototype.Certificate21.childrenH_247 line 592
  287. theorem OAI.SnakyPrototype.Certificate21.height_exact_247 line 593
  288. theorem OAI.SnakyPrototype.Certificate21.required_origin_247 line 594
  289. theorem OAI.SnakyPrototype.Certificate21.required_exact_247 line 596
  290. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_247 line 600
  291. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_247 line 602
  292. def OAI.SnakyPrototype.Certificate21.checked_247 line 606
  293. def OAI.SnakyPrototype.Certificate21.height_251 line 614
  294. def OAI.SnakyPrototype.Certificate21.childrenH_251 line 615
  295. theorem OAI.SnakyPrototype.Certificate21.height_exact_251 line 616
  296. theorem OAI.SnakyPrototype.Certificate21.required_origin_251 line 617
  297. theorem OAI.SnakyPrototype.Certificate21.required_exact_251 line 619
  298. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_251 line 623
  299. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_251 line 625
  300. def OAI.SnakyPrototype.Certificate21.checked_251 line 629
  301. def OAI.SnakyPrototype.Certificate21.height_261 line 637
  302. def OAI.SnakyPrototype.Certificate21.childrenH_261 line 638
  303. theorem OAI.SnakyPrototype.Certificate21.height_exact_261 line 639
  304. theorem OAI.SnakyPrototype.Certificate21.required_origin_261 line 640
  305. theorem OAI.SnakyPrototype.Certificate21.required_exact_261 line 642
  306. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_261 line 646
  307. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_261 line 648
  308. def OAI.SnakyPrototype.Certificate21.checked_261 line 652
  309. def OAI.SnakyPrototype.Certificate21.height_262 line 660
  310. def OAI.SnakyPrototype.Certificate21.childrenH_262 line 661
  311. theorem OAI.SnakyPrototype.Certificate21.height_exact_262 line 662
  312. theorem OAI.SnakyPrototype.Certificate21.required_origin_262 line 663
  313. theorem OAI.SnakyPrototype.Certificate21.required_exact_262 line 665
  314. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_262 line 669
  315. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_262 line 671
  316. def OAI.SnakyPrototype.Certificate21.checked_262 line 675
  317. def OAI.SnakyPrototype.Certificate21.height_280 line 683
  318. def OAI.SnakyPrototype.Certificate21.childrenH_280 line 684
  319. theorem OAI.SnakyPrototype.Certificate21.height_exact_280 line 685
  320. theorem OAI.SnakyPrototype.Certificate21.required_origin_280 line 686
  321. theorem OAI.SnakyPrototype.Certificate21.required_exact_280 line 688
  322. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_280 line 692
  323. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_280 line 694
  324. def OAI.SnakyPrototype.Certificate21.checked_280 line 698
  325. def OAI.SnakyPrototype.Certificate21.height_310 line 706
  326. def OAI.SnakyPrototype.Certificate21.childrenH_310 line 707
  327. theorem OAI.SnakyPrototype.Certificate21.height_exact_310 line 708
  328. theorem OAI.SnakyPrototype.Certificate21.required_origin_310 line 709
  329. theorem OAI.SnakyPrototype.Certificate21.required_exact_310 line 711
  330. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_310 line 715
  331. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_310 line 717
  332. def OAI.SnakyPrototype.Certificate21.checked_310 line 721
  333. def OAI.SnakyPrototype.Certificate21.height_333_i0 line 729
  334. def OAI.SnakyPrototype.Certificate21.childrenH_333_i0 line 730
  335. theorem OAI.SnakyPrototype.Certificate21.height_exact_333_i0 line 731
  336. theorem OAI.SnakyPrototype.Certificate21.required_origin_333_i0 line 732
  337. theorem OAI.SnakyPrototype.Certificate21.required_exact_333_i0 line 734
  338. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_333_i0 line 738
  339. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_333_i0 line 740
  340. def OAI.SnakyPrototype.Certificate21.checked_333_i0 line 744
  341. def OAI.SnakyPrototype.Certificate21.height_333 line 752
  342. def OAI.SnakyPrototype.Certificate21.childrenH_333 line 753
  343. theorem OAI.SnakyPrototype.Certificate21.height_exact_333 line 754
  344. theorem OAI.SnakyPrototype.Certificate21.required_origin_333 line 755
  345. theorem OAI.SnakyPrototype.Certificate21.required_exact_333 line 757
  346. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_333 line 761
  347. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_333 line 763
  348. def OAI.SnakyPrototype.Certificate21.checked_333 line 767
  349. def OAI.SnakyPrototype.Certificate21.height_350_i0 line 775
  350. def OAI.SnakyPrototype.Certificate21.childrenH_350_i0 line 776
  351. theorem OAI.SnakyPrototype.Certificate21.height_exact_350_i0 line 777
  352. theorem OAI.SnakyPrototype.Certificate21.required_origin_350_i0 line 778
  353. theorem OAI.SnakyPrototype.Certificate21.required_exact_350_i0 line 780
  354. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_350_i0 line 784
  355. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_350_i0 line 786
  356. def OAI.SnakyPrototype.Certificate21.checked_350_i0 line 790
  357. def OAI.SnakyPrototype.Certificate21.height_350 line 798
  358. def OAI.SnakyPrototype.Certificate21.childrenH_350 line 799
  359. theorem OAI.SnakyPrototype.Certificate21.height_exact_350 line 800
  360. theorem OAI.SnakyPrototype.Certificate21.required_origin_350 line 801
  361. theorem OAI.SnakyPrototype.Certificate21.required_exact_350 line 803
  362. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_350 line 807
  363. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_350 line 809
  364. def OAI.SnakyPrototype.Certificate21.checked_350 line 813
  365. def OAI.SnakyPrototype.Certificate21.height_374_i0 line 821
  366. def OAI.SnakyPrototype.Certificate21.childrenH_374_i0 line 822
  367. theorem OAI.SnakyPrototype.Certificate21.height_exact_374_i0 line 823
  368. theorem OAI.SnakyPrototype.Certificate21.required_origin_374_i0 line 824
  369. theorem OAI.SnakyPrototype.Certificate21.required_exact_374_i0 line 826
  370. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_374_i0 line 830
  371. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_374_i0 line 832
  372. def OAI.SnakyPrototype.Certificate21.checked_374_i0 line 836
  373. def OAI.SnakyPrototype.Certificate21.height_374 line 844
  374. def OAI.SnakyPrototype.Certificate21.childrenH_374 line 845
  375. theorem OAI.SnakyPrototype.Certificate21.height_exact_374 line 846
  376. theorem OAI.SnakyPrototype.Certificate21.required_origin_374 line 847
  377. theorem OAI.SnakyPrototype.Certificate21.required_exact_374 line 849
  378. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_374 line 853
  379. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_374 line 855
  380. def OAI.SnakyPrototype.Certificate21.checked_374 line 859
  381. def OAI.SnakyPrototype.Certificate21.height_402_i0 line 867
  382. def OAI.SnakyPrototype.Certificate21.childrenH_402_i0 line 868
  383. theorem OAI.SnakyPrototype.Certificate21.height_exact_402_i0 line 869
  384. theorem OAI.SnakyPrototype.Certificate21.required_origin_402_i0 line 870
  385. theorem OAI.SnakyPrototype.Certificate21.required_exact_402_i0 line 872
  386. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_402_i0 line 876
  387. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_402_i0 line 878
  388. def OAI.SnakyPrototype.Certificate21.checked_402_i0 line 882
  389. def OAI.SnakyPrototype.Certificate21.height_402 line 890
  390. def OAI.SnakyPrototype.Certificate21.childrenH_402 line 891
  391. theorem OAI.SnakyPrototype.Certificate21.height_exact_402 line 892
  392. theorem OAI.SnakyPrototype.Certificate21.required_origin_402 line 893
  393. theorem OAI.SnakyPrototype.Certificate21.required_exact_402 line 895
  394. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_402 line 899
  395. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_402 line 901
  396. def OAI.SnakyPrototype.Certificate21.checked_402 line 905