OAI/GameTheory/SnakyTwentyOne/Cards/Height05Part02.lean

GitHub source file

432 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_183 line 14
  2. def OAI.SnakyPrototype.Certificate21.envelope_183 line 15
  3. def OAI.SnakyPrototype.Certificate21.childrenC_183 line 16
  4. def OAI.SnakyPrototype.Certificate21.childrenD_183 line 17
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_183 line 18
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_183 line 19
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_183 line 20
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_183 line 21
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_183 line 22
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_183 line 27
  11. def OAI.SnakyPrototype.Certificate21.required_186 line 32
  12. def OAI.SnakyPrototype.Certificate21.envelope_186 line 33
  13. def OAI.SnakyPrototype.Certificate21.childrenC_186 line 34
  14. def OAI.SnakyPrototype.Certificate21.childrenD_186 line 35
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_186 line 36
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_186 line 37
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_186 line 38
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_186 line 39
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_186 line 40
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_186 line 45
  21. def OAI.SnakyPrototype.Certificate21.required_187 line 50
  22. def OAI.SnakyPrototype.Certificate21.envelope_187 line 51
  23. def OAI.SnakyPrototype.Certificate21.childrenC_187 line 52
  24. def OAI.SnakyPrototype.Certificate21.childrenD_187 line 53
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_187 line 54
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_187 line 55
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_187 line 56
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_187 line 57
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_187 line 58
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_187 line 64
  31. def OAI.SnakyPrototype.Certificate21.required_191 line 69
  32. def OAI.SnakyPrototype.Certificate21.envelope_191 line 70
  33. def OAI.SnakyPrototype.Certificate21.childrenC_191 line 71
  34. def OAI.SnakyPrototype.Certificate21.childrenD_191 line 72
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_191 line 73
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_191 line 74
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_191 line 75
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_191 line 76
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_191 line 77
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_191 line 82
  41. def OAI.SnakyPrototype.Certificate21.required_197 line 87
  42. def OAI.SnakyPrototype.Certificate21.envelope_197 line 88
  43. def OAI.SnakyPrototype.Certificate21.childrenC_197 line 89
  44. def OAI.SnakyPrototype.Certificate21.childrenD_197 line 90
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_197 line 91
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_197 line 92
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_197 line 93
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_197 line 94
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_197 line 95
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_197 line 102
  51. def OAI.SnakyPrototype.Certificate21.required_202 line 107
  52. def OAI.SnakyPrototype.Certificate21.envelope_202 line 108
  53. def OAI.SnakyPrototype.Certificate21.childrenC_202 line 109
  54. def OAI.SnakyPrototype.Certificate21.childrenD_202 line 110
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_202 line 111
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_202 line 112
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_202 line 113
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_202 line 114
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_202 line 115
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_202 line 120
  61. def OAI.SnakyPrototype.Certificate21.required_211 line 125
  62. def OAI.SnakyPrototype.Certificate21.envelope_211 line 126
  63. def OAI.SnakyPrototype.Certificate21.childrenC_211 line 127
  64. def OAI.SnakyPrototype.Certificate21.childrenD_211 line 128
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_211 line 129
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_211 line 130
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_211 line 131
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_211 line 132
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_211 line 133
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_211 line 139
  71. def OAI.SnakyPrototype.Certificate21.required_214 line 144
  72. def OAI.SnakyPrototype.Certificate21.envelope_214 line 145
  73. def OAI.SnakyPrototype.Certificate21.childrenC_214 line 146
  74. def OAI.SnakyPrototype.Certificate21.childrenD_214 line 147
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_214 line 148
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_214 line 149
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_214 line 150
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_214 line 151
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_214 line 152
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_214 line 157
  81. def OAI.SnakyPrototype.Certificate21.required_225 line 162
  82. def OAI.SnakyPrototype.Certificate21.envelope_225 line 163
  83. def OAI.SnakyPrototype.Certificate21.childrenC_225 line 164
  84. def OAI.SnakyPrototype.Certificate21.childrenD_225 line 165
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_225 line 166
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_225 line 167
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_225 line 168
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_225 line 169
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_225 line 170
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_225 line 175
  91. def OAI.SnakyPrototype.Certificate21.required_228 line 180
  92. def OAI.SnakyPrototype.Certificate21.envelope_228 line 181
  93. def OAI.SnakyPrototype.Certificate21.childrenC_228 line 182
  94. def OAI.SnakyPrototype.Certificate21.childrenD_228 line 183
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_228 line 184
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_228 line 185
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_228 line 186
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_228 line 187
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_228 line 188
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_228 line 193
  101. def OAI.SnakyPrototype.Certificate21.required_230 line 198
  102. def OAI.SnakyPrototype.Certificate21.envelope_230 line 199
  103. def OAI.SnakyPrototype.Certificate21.childrenC_230 line 200
  104. def OAI.SnakyPrototype.Certificate21.childrenD_230 line 201
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_230 line 202
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_230 line 203
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_230 line 204
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_230 line 205
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_230 line 206
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_230 line 212
  111. def OAI.SnakyPrototype.Certificate21.required_231 line 217
  112. def OAI.SnakyPrototype.Certificate21.envelope_231 line 218
  113. def OAI.SnakyPrototype.Certificate21.childrenC_231 line 219
  114. def OAI.SnakyPrototype.Certificate21.childrenD_231 line 220
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_231 line 221
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_231 line 222
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_231 line 223
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_231 line 224
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_231 line 225
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_231 line 230
  121. def OAI.SnakyPrototype.Certificate21.required_232 line 235
  122. def OAI.SnakyPrototype.Certificate21.envelope_232 line 236
  123. def OAI.SnakyPrototype.Certificate21.childrenC_232 line 237
  124. def OAI.SnakyPrototype.Certificate21.childrenD_232 line 238
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_232 line 239
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_232 line 240
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_232 line 241
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_232 line 242
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_232 line 243
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_232 line 248
  131. def OAI.SnakyPrototype.Certificate21.required_233 line 253
  132. def OAI.SnakyPrototype.Certificate21.envelope_233 line 254
  133. def OAI.SnakyPrototype.Certificate21.childrenC_233 line 255
  134. def OAI.SnakyPrototype.Certificate21.childrenD_233 line 256
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_233 line 257
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_233 line 258
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_233 line 259
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_233 line 260
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_233 line 261
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_233 line 266
  141. def OAI.SnakyPrototype.Certificate21.required_234 line 271
  142. def OAI.SnakyPrototype.Certificate21.envelope_234 line 272
  143. def OAI.SnakyPrototype.Certificate21.childrenC_234 line 273
  144. def OAI.SnakyPrototype.Certificate21.childrenD_234 line 274
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_234 line 275
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_234 line 276
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_234 line 277
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_234 line 278
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_234 line 279
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_234 line 284
  151. def OAI.SnakyPrototype.Certificate21.required_237 line 289
  152. def OAI.SnakyPrototype.Certificate21.envelope_237 line 290
  153. def OAI.SnakyPrototype.Certificate21.childrenC_237 line 291
  154. def OAI.SnakyPrototype.Certificate21.childrenD_237 line 292
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_237 line 293
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_237 line 294
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_237 line 295
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_237 line 296
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_237 line 297
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_237 line 302
  161. def OAI.SnakyPrototype.Certificate21.required_241 line 307
  162. def OAI.SnakyPrototype.Certificate21.envelope_241 line 308
  163. def OAI.SnakyPrototype.Certificate21.childrenC_241 line 309
  164. def OAI.SnakyPrototype.Certificate21.childrenD_241 line 310
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_241 line 311
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_241 line 312
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_241 line 313
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_241 line 314
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_241 line 315
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_241 line 320
  171. def OAI.SnakyPrototype.Certificate21.required_243 line 325
  172. def OAI.SnakyPrototype.Certificate21.envelope_243 line 326
  173. def OAI.SnakyPrototype.Certificate21.childrenC_243 line 327
  174. def OAI.SnakyPrototype.Certificate21.childrenD_243 line 328
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_243 line 329
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_243 line 330
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_243 line 331
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_243 line 332
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_243 line 333
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_243 line 338
  181. def OAI.SnakyPrototype.Certificate21.required_249 line 343
  182. def OAI.SnakyPrototype.Certificate21.envelope_249 line 344
  183. def OAI.SnakyPrototype.Certificate21.childrenC_249 line 345
  184. def OAI.SnakyPrototype.Certificate21.childrenD_249 line 346
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_249 line 347
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_249 line 348
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_249 line 349
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_249 line 350
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_249 line 351
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_249 line 356
  191. def OAI.SnakyPrototype.Certificate21.required_250 line 361
  192. def OAI.SnakyPrototype.Certificate21.envelope_250 line 362
  193. def OAI.SnakyPrototype.Certificate21.childrenC_250 line 363
  194. def OAI.SnakyPrototype.Certificate21.childrenD_250 line 364
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_250 line 365
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_250 line 366
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_250 line 367
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_250 line 368
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_250 line 369
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_250 line 374
  201. def OAI.SnakyPrototype.Certificate21.required_252 line 379
  202. def OAI.SnakyPrototype.Certificate21.envelope_252 line 380
  203. def OAI.SnakyPrototype.Certificate21.childrenC_252 line 381
  204. def OAI.SnakyPrototype.Certificate21.childrenD_252 line 382
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_252 line 383
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_252 line 384
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_252 line 385
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_252 line 386
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_252 line 387
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_252 line 393
  211. def OAI.SnakyPrototype.Certificate21.required_254 line 398
  212. def OAI.SnakyPrototype.Certificate21.envelope_254 line 399
  213. def OAI.SnakyPrototype.Certificate21.childrenC_254 line 400
  214. def OAI.SnakyPrototype.Certificate21.childrenD_254 line 401
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_254 line 402
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_254 line 403
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_254 line 404
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_254 line 405
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_254 line 406
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_254 line 412
  221. def OAI.SnakyPrototype.Certificate21.required_260 line 417
  222. def OAI.SnakyPrototype.Certificate21.envelope_260 line 418
  223. def OAI.SnakyPrototype.Certificate21.childrenC_260 line 419
  224. def OAI.SnakyPrototype.Certificate21.childrenD_260 line 420
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_260 line 421
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_260 line 422
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_260 line 423
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_260 line 424
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_260 line 425
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_260 line 430
  231. def OAI.SnakyPrototype.Certificate21.required_265 line 435
  232. def OAI.SnakyPrototype.Certificate21.envelope_265 line 436
  233. def OAI.SnakyPrototype.Certificate21.childrenC_265 line 437
  234. def OAI.SnakyPrototype.Certificate21.childrenD_265 line 438
  235. theorem OAI.SnakyPrototype.Certificate21.common_sub_265 line 439
  236. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_265 line 440
  237. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_265 line 441
  238. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_265 line 442
  239. theorem OAI.SnakyPrototype.Certificate21.children_work_265 line 443
  240. theorem OAI.SnakyPrototype.Certificate21.row_works_265 line 448
  241. def OAI.SnakyPrototype.Certificate21.height_183 line 453
  242. def OAI.SnakyPrototype.Certificate21.childrenH_183 line 454
  243. theorem OAI.SnakyPrototype.Certificate21.height_exact_183 line 455
  244. theorem OAI.SnakyPrototype.Certificate21.required_origin_183 line 456
  245. theorem OAI.SnakyPrototype.Certificate21.required_exact_183 line 458
  246. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_183 line 462
  247. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_183 line 464
  248. def OAI.SnakyPrototype.Certificate21.checked_183 line 468
  249. def OAI.SnakyPrototype.Certificate21.height_186 line 476
  250. def OAI.SnakyPrototype.Certificate21.childrenH_186 line 477
  251. theorem OAI.SnakyPrototype.Certificate21.height_exact_186 line 478
  252. theorem OAI.SnakyPrototype.Certificate21.required_origin_186 line 479
  253. theorem OAI.SnakyPrototype.Certificate21.required_exact_186 line 481
  254. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_186 line 485
  255. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_186 line 487
  256. def OAI.SnakyPrototype.Certificate21.checked_186 line 491
  257. def OAI.SnakyPrototype.Certificate21.height_187 line 499
  258. def OAI.SnakyPrototype.Certificate21.childrenH_187 line 500
  259. theorem OAI.SnakyPrototype.Certificate21.height_exact_187 line 501
  260. theorem OAI.SnakyPrototype.Certificate21.required_origin_187 line 502
  261. theorem OAI.SnakyPrototype.Certificate21.required_exact_187 line 504
  262. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_187 line 508
  263. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_187 line 510
  264. def OAI.SnakyPrototype.Certificate21.checked_187 line 514
  265. def OAI.SnakyPrototype.Certificate21.height_191 line 522
  266. def OAI.SnakyPrototype.Certificate21.childrenH_191 line 523
  267. theorem OAI.SnakyPrototype.Certificate21.height_exact_191 line 524
  268. theorem OAI.SnakyPrototype.Certificate21.required_origin_191 line 525
  269. theorem OAI.SnakyPrototype.Certificate21.required_exact_191 line 527
  270. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_191 line 531
  271. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_191 line 533
  272. def OAI.SnakyPrototype.Certificate21.checked_191 line 537
  273. def OAI.SnakyPrototype.Certificate21.height_197 line 545
  274. def OAI.SnakyPrototype.Certificate21.childrenH_197 line 546
  275. theorem OAI.SnakyPrototype.Certificate21.height_exact_197 line 547
  276. theorem OAI.SnakyPrototype.Certificate21.required_origin_197 line 548
  277. theorem OAI.SnakyPrototype.Certificate21.required_exact_197 line 550
  278. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_197 line 554
  279. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_197 line 556
  280. def OAI.SnakyPrototype.Certificate21.checked_197 line 560
  281. def OAI.SnakyPrototype.Certificate21.height_202 line 568
  282. def OAI.SnakyPrototype.Certificate21.childrenH_202 line 569
  283. theorem OAI.SnakyPrototype.Certificate21.height_exact_202 line 570
  284. theorem OAI.SnakyPrototype.Certificate21.required_origin_202 line 571
  285. theorem OAI.SnakyPrototype.Certificate21.required_exact_202 line 573
  286. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_202 line 577
  287. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_202 line 579
  288. def OAI.SnakyPrototype.Certificate21.checked_202 line 583
  289. def OAI.SnakyPrototype.Certificate21.height_211 line 591
  290. def OAI.SnakyPrototype.Certificate21.childrenH_211 line 592
  291. theorem OAI.SnakyPrototype.Certificate21.height_exact_211 line 593
  292. theorem OAI.SnakyPrototype.Certificate21.required_origin_211 line 594
  293. theorem OAI.SnakyPrototype.Certificate21.required_exact_211 line 596
  294. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_211 line 600
  295. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_211 line 602
  296. def OAI.SnakyPrototype.Certificate21.checked_211 line 606
  297. def OAI.SnakyPrototype.Certificate21.height_214 line 614
  298. def OAI.SnakyPrototype.Certificate21.childrenH_214 line 615
  299. theorem OAI.SnakyPrototype.Certificate21.height_exact_214 line 616
  300. theorem OAI.SnakyPrototype.Certificate21.required_origin_214 line 617
  301. theorem OAI.SnakyPrototype.Certificate21.required_exact_214 line 619
  302. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_214 line 623
  303. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_214 line 625
  304. def OAI.SnakyPrototype.Certificate21.checked_214 line 629
  305. def OAI.SnakyPrototype.Certificate21.height_225 line 637
  306. def OAI.SnakyPrototype.Certificate21.childrenH_225 line 638
  307. theorem OAI.SnakyPrototype.Certificate21.height_exact_225 line 639
  308. theorem OAI.SnakyPrototype.Certificate21.required_origin_225 line 640
  309. theorem OAI.SnakyPrototype.Certificate21.required_exact_225 line 642
  310. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_225 line 646
  311. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_225 line 648
  312. def OAI.SnakyPrototype.Certificate21.checked_225 line 652
  313. def OAI.SnakyPrototype.Certificate21.height_228 line 660
  314. def OAI.SnakyPrototype.Certificate21.childrenH_228 line 661
  315. theorem OAI.SnakyPrototype.Certificate21.height_exact_228 line 662
  316. theorem OAI.SnakyPrototype.Certificate21.required_origin_228 line 663
  317. theorem OAI.SnakyPrototype.Certificate21.required_exact_228 line 665
  318. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_228 line 669
  319. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_228 line 671
  320. def OAI.SnakyPrototype.Certificate21.checked_228 line 675
  321. def OAI.SnakyPrototype.Certificate21.height_230 line 683
  322. def OAI.SnakyPrototype.Certificate21.childrenH_230 line 684
  323. theorem OAI.SnakyPrototype.Certificate21.height_exact_230 line 685
  324. theorem OAI.SnakyPrototype.Certificate21.required_origin_230 line 686
  325. theorem OAI.SnakyPrototype.Certificate21.required_exact_230 line 688
  326. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_230 line 692
  327. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_230 line 694
  328. def OAI.SnakyPrototype.Certificate21.checked_230 line 698
  329. def OAI.SnakyPrototype.Certificate21.height_231 line 706
  330. def OAI.SnakyPrototype.Certificate21.childrenH_231 line 707
  331. theorem OAI.SnakyPrototype.Certificate21.height_exact_231 line 708
  332. theorem OAI.SnakyPrototype.Certificate21.required_origin_231 line 709
  333. theorem OAI.SnakyPrototype.Certificate21.required_exact_231 line 711
  334. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_231 line 715
  335. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_231 line 717
  336. def OAI.SnakyPrototype.Certificate21.checked_231 line 721
  337. def OAI.SnakyPrototype.Certificate21.height_232 line 729
  338. def OAI.SnakyPrototype.Certificate21.childrenH_232 line 730
  339. theorem OAI.SnakyPrototype.Certificate21.height_exact_232 line 731
  340. theorem OAI.SnakyPrototype.Certificate21.required_origin_232 line 732
  341. theorem OAI.SnakyPrototype.Certificate21.required_exact_232 line 734
  342. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_232 line 738
  343. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_232 line 740
  344. def OAI.SnakyPrototype.Certificate21.checked_232 line 744
  345. def OAI.SnakyPrototype.Certificate21.height_233 line 752
  346. def OAI.SnakyPrototype.Certificate21.childrenH_233 line 753
  347. theorem OAI.SnakyPrototype.Certificate21.height_exact_233 line 754
  348. theorem OAI.SnakyPrototype.Certificate21.required_origin_233 line 755
  349. theorem OAI.SnakyPrototype.Certificate21.required_exact_233 line 757
  350. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_233 line 761
  351. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_233 line 763
  352. def OAI.SnakyPrototype.Certificate21.checked_233 line 767
  353. def OAI.SnakyPrototype.Certificate21.height_234 line 775
  354. def OAI.SnakyPrototype.Certificate21.childrenH_234 line 776
  355. theorem OAI.SnakyPrototype.Certificate21.height_exact_234 line 777
  356. theorem OAI.SnakyPrototype.Certificate21.required_origin_234 line 778
  357. theorem OAI.SnakyPrototype.Certificate21.required_exact_234 line 780
  358. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_234 line 784
  359. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_234 line 786
  360. def OAI.SnakyPrototype.Certificate21.checked_234 line 790
  361. def OAI.SnakyPrototype.Certificate21.height_237 line 798
  362. def OAI.SnakyPrototype.Certificate21.childrenH_237 line 799
  363. theorem OAI.SnakyPrototype.Certificate21.height_exact_237 line 800
  364. theorem OAI.SnakyPrototype.Certificate21.required_origin_237 line 801
  365. theorem OAI.SnakyPrototype.Certificate21.required_exact_237 line 803
  366. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_237 line 807
  367. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_237 line 809
  368. def OAI.SnakyPrototype.Certificate21.checked_237 line 813
  369. def OAI.SnakyPrototype.Certificate21.height_241 line 821
  370. def OAI.SnakyPrototype.Certificate21.childrenH_241 line 822
  371. theorem OAI.SnakyPrototype.Certificate21.height_exact_241 line 823
  372. theorem OAI.SnakyPrototype.Certificate21.required_origin_241 line 824
  373. theorem OAI.SnakyPrototype.Certificate21.required_exact_241 line 826
  374. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_241 line 830
  375. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_241 line 832
  376. def OAI.SnakyPrototype.Certificate21.checked_241 line 836
  377. def OAI.SnakyPrototype.Certificate21.height_243 line 844
  378. def OAI.SnakyPrototype.Certificate21.childrenH_243 line 845
  379. theorem OAI.SnakyPrototype.Certificate21.height_exact_243 line 846
  380. theorem OAI.SnakyPrototype.Certificate21.required_origin_243 line 847
  381. theorem OAI.SnakyPrototype.Certificate21.required_exact_243 line 849
  382. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_243 line 853
  383. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_243 line 855
  384. def OAI.SnakyPrototype.Certificate21.checked_243 line 859
  385. def OAI.SnakyPrototype.Certificate21.height_249 line 867
  386. def OAI.SnakyPrototype.Certificate21.childrenH_249 line 868
  387. theorem OAI.SnakyPrototype.Certificate21.height_exact_249 line 869
  388. theorem OAI.SnakyPrototype.Certificate21.required_origin_249 line 870
  389. theorem OAI.SnakyPrototype.Certificate21.required_exact_249 line 872
  390. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_249 line 876
  391. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_249 line 878
  392. def OAI.SnakyPrototype.Certificate21.checked_249 line 882
  393. def OAI.SnakyPrototype.Certificate21.height_250 line 890
  394. def OAI.SnakyPrototype.Certificate21.childrenH_250 line 891
  395. theorem OAI.SnakyPrototype.Certificate21.height_exact_250 line 892
  396. theorem OAI.SnakyPrototype.Certificate21.required_origin_250 line 893
  397. theorem OAI.SnakyPrototype.Certificate21.required_exact_250 line 895
  398. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_250 line 899
  399. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_250 line 901
  400. def OAI.SnakyPrototype.Certificate21.checked_250 line 905
  401. def OAI.SnakyPrototype.Certificate21.height_252 line 913
  402. def OAI.SnakyPrototype.Certificate21.childrenH_252 line 914
  403. theorem OAI.SnakyPrototype.Certificate21.height_exact_252 line 915
  404. theorem OAI.SnakyPrototype.Certificate21.required_origin_252 line 916
  405. theorem OAI.SnakyPrototype.Certificate21.required_exact_252 line 918
  406. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_252 line 922
  407. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_252 line 924
  408. def OAI.SnakyPrototype.Certificate21.checked_252 line 928
  409. def OAI.SnakyPrototype.Certificate21.height_254 line 936
  410. def OAI.SnakyPrototype.Certificate21.childrenH_254 line 937
  411. theorem OAI.SnakyPrototype.Certificate21.height_exact_254 line 938
  412. theorem OAI.SnakyPrototype.Certificate21.required_origin_254 line 939
  413. theorem OAI.SnakyPrototype.Certificate21.required_exact_254 line 941
  414. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_254 line 945
  415. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_254 line 947
  416. def OAI.SnakyPrototype.Certificate21.checked_254 line 951
  417. def OAI.SnakyPrototype.Certificate21.height_260 line 959
  418. def OAI.SnakyPrototype.Certificate21.childrenH_260 line 960
  419. theorem OAI.SnakyPrototype.Certificate21.height_exact_260 line 961
  420. theorem OAI.SnakyPrototype.Certificate21.required_origin_260 line 962
  421. theorem OAI.SnakyPrototype.Certificate21.required_exact_260 line 964
  422. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_260 line 968
  423. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_260 line 970
  424. def OAI.SnakyPrototype.Certificate21.checked_260 line 974
  425. def OAI.SnakyPrototype.Certificate21.height_265 line 982
  426. def OAI.SnakyPrototype.Certificate21.childrenH_265 line 983
  427. theorem OAI.SnakyPrototype.Certificate21.height_exact_265 line 984
  428. theorem OAI.SnakyPrototype.Certificate21.required_origin_265 line 985
  429. theorem OAI.SnakyPrototype.Certificate21.required_exact_265 line 987
  430. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_265 line 991
  431. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_265 line 993
  432. def OAI.SnakyPrototype.Certificate21.checked_265 line 997