OAI/GameTheory/SnakyTwentyOne/Cards/Height04Part01.lean

GitHub source file

432 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_10 line 11
  2. def OAI.SnakyPrototype.Certificate21.envelope_10 line 12
  3. def OAI.SnakyPrototype.Certificate21.childrenC_10 line 13
  4. def OAI.SnakyPrototype.Certificate21.childrenD_10 line 14
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_10 line 15
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_10 line 16
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_10 line 17
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_10 line 18
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_10 line 19
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_10 line 24
  11. def OAI.SnakyPrototype.Certificate21.required_12 line 29
  12. def OAI.SnakyPrototype.Certificate21.envelope_12 line 30
  13. def OAI.SnakyPrototype.Certificate21.childrenC_12 line 31
  14. def OAI.SnakyPrototype.Certificate21.childrenD_12 line 32
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_12 line 33
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_12 line 34
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_12 line 35
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_12 line 36
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_12 line 37
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_12 line 43
  21. def OAI.SnakyPrototype.Certificate21.required_13 line 48
  22. def OAI.SnakyPrototype.Certificate21.envelope_13 line 49
  23. def OAI.SnakyPrototype.Certificate21.childrenC_13 line 50
  24. def OAI.SnakyPrototype.Certificate21.childrenD_13 line 51
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_13 line 52
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_13 line 53
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_13 line 54
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_13 line 55
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_13 line 56
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_13 line 62
  31. def OAI.SnakyPrototype.Certificate21.required_14 line 67
  32. def OAI.SnakyPrototype.Certificate21.envelope_14 line 68
  33. def OAI.SnakyPrototype.Certificate21.childrenC_14 line 69
  34. def OAI.SnakyPrototype.Certificate21.childrenD_14 line 70
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_14 line 71
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_14 line 72
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_14 line 73
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_14 line 74
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_14 line 75
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_14 line 81
  41. def OAI.SnakyPrototype.Certificate21.required_17 line 86
  42. def OAI.SnakyPrototype.Certificate21.envelope_17 line 87
  43. def OAI.SnakyPrototype.Certificate21.childrenC_17 line 88
  44. def OAI.SnakyPrototype.Certificate21.childrenD_17 line 89
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_17 line 90
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_17 line 91
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_17 line 92
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_17 line 93
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_17 line 94
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_17 line 99
  51. def OAI.SnakyPrototype.Certificate21.required_18 line 104
  52. def OAI.SnakyPrototype.Certificate21.envelope_18 line 105
  53. def OAI.SnakyPrototype.Certificate21.childrenC_18 line 106
  54. def OAI.SnakyPrototype.Certificate21.childrenD_18 line 107
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_18 line 108
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_18 line 109
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_18 line 110
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_18 line 111
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_18 line 112
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_18 line 117
  61. def OAI.SnakyPrototype.Certificate21.required_26 line 122
  62. def OAI.SnakyPrototype.Certificate21.envelope_26 line 123
  63. def OAI.SnakyPrototype.Certificate21.childrenC_26 line 124
  64. def OAI.SnakyPrototype.Certificate21.childrenD_26 line 125
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_26 line 126
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_26 line 127
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_26 line 128
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_26 line 129
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_26 line 130
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_26 line 135
  71. def OAI.SnakyPrototype.Certificate21.required_27 line 140
  72. def OAI.SnakyPrototype.Certificate21.envelope_27 line 141
  73. def OAI.SnakyPrototype.Certificate21.childrenC_27 line 142
  74. def OAI.SnakyPrototype.Certificate21.childrenD_27 line 143
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_27 line 144
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_27 line 145
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_27 line 146
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_27 line 147
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_27 line 148
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_27 line 153
  81. def OAI.SnakyPrototype.Certificate21.required_31 line 158
  82. def OAI.SnakyPrototype.Certificate21.envelope_31 line 159
  83. def OAI.SnakyPrototype.Certificate21.childrenC_31 line 160
  84. def OAI.SnakyPrototype.Certificate21.childrenD_31 line 161
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_31 line 162
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_31 line 163
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_31 line 164
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_31 line 165
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_31 line 166
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_31 line 171
  91. def OAI.SnakyPrototype.Certificate21.required_33 line 176
  92. def OAI.SnakyPrototype.Certificate21.envelope_33 line 177
  93. def OAI.SnakyPrototype.Certificate21.childrenC_33 line 178
  94. def OAI.SnakyPrototype.Certificate21.childrenD_33 line 179
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_33 line 180
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_33 line 181
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_33 line 182
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_33 line 183
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_33 line 184
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_33 line 190
  101. def OAI.SnakyPrototype.Certificate21.required_39 line 195
  102. def OAI.SnakyPrototype.Certificate21.envelope_39 line 196
  103. def OAI.SnakyPrototype.Certificate21.childrenC_39 line 197
  104. def OAI.SnakyPrototype.Certificate21.childrenD_39 line 198
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_39 line 199
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_39 line 200
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_39 line 201
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_39 line 202
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_39 line 203
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_39 line 208
  111. def OAI.SnakyPrototype.Certificate21.required_41 line 213
  112. def OAI.SnakyPrototype.Certificate21.envelope_41 line 214
  113. def OAI.SnakyPrototype.Certificate21.childrenC_41 line 215
  114. def OAI.SnakyPrototype.Certificate21.childrenD_41 line 216
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_41 line 217
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_41 line 218
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_41 line 219
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_41 line 220
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_41 line 221
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_41 line 226
  121. def OAI.SnakyPrototype.Certificate21.required_42 line 231
  122. def OAI.SnakyPrototype.Certificate21.envelope_42 line 232
  123. def OAI.SnakyPrototype.Certificate21.childrenC_42 line 233
  124. def OAI.SnakyPrototype.Certificate21.childrenD_42 line 234
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_42 line 235
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_42 line 236
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_42 line 237
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_42 line 238
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_42 line 239
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_42 line 244
  131. def OAI.SnakyPrototype.Certificate21.required_46 line 249
  132. def OAI.SnakyPrototype.Certificate21.envelope_46 line 250
  133. def OAI.SnakyPrototype.Certificate21.childrenC_46 line 251
  134. def OAI.SnakyPrototype.Certificate21.childrenD_46 line 252
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_46 line 253
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_46 line 254
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_46 line 255
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_46 line 256
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_46 line 257
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_46 line 262
  141. def OAI.SnakyPrototype.Certificate21.required_48 line 267
  142. def OAI.SnakyPrototype.Certificate21.envelope_48 line 268
  143. def OAI.SnakyPrototype.Certificate21.childrenC_48 line 269
  144. def OAI.SnakyPrototype.Certificate21.childrenD_48 line 270
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_48 line 271
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_48 line 272
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_48 line 273
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_48 line 274
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_48 line 275
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_48 line 280
  151. def OAI.SnakyPrototype.Certificate21.required_49 line 285
  152. def OAI.SnakyPrototype.Certificate21.envelope_49 line 286
  153. def OAI.SnakyPrototype.Certificate21.childrenC_49 line 287
  154. def OAI.SnakyPrototype.Certificate21.childrenD_49 line 288
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_49 line 289
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_49 line 290
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_49 line 291
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_49 line 292
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_49 line 293
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_49 line 298
  161. def OAI.SnakyPrototype.Certificate21.required_50 line 303
  162. def OAI.SnakyPrototype.Certificate21.envelope_50 line 304
  163. def OAI.SnakyPrototype.Certificate21.childrenC_50 line 305
  164. def OAI.SnakyPrototype.Certificate21.childrenD_50 line 306
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_50 line 307
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_50 line 308
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_50 line 309
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_50 line 310
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_50 line 311
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_50 line 316
  171. def OAI.SnakyPrototype.Certificate21.required_55 line 321
  172. def OAI.SnakyPrototype.Certificate21.envelope_55 line 322
  173. def OAI.SnakyPrototype.Certificate21.childrenC_55 line 323
  174. def OAI.SnakyPrototype.Certificate21.childrenD_55 line 324
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_55 line 325
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_55 line 326
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_55 line 327
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_55 line 328
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_55 line 329
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_55 line 334
  181. def OAI.SnakyPrototype.Certificate21.required_56 line 339
  182. def OAI.SnakyPrototype.Certificate21.envelope_56 line 340
  183. def OAI.SnakyPrototype.Certificate21.childrenC_56 line 341
  184. def OAI.SnakyPrototype.Certificate21.childrenD_56 line 342
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_56 line 343
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_56 line 344
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_56 line 345
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_56 line 346
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_56 line 347
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_56 line 352
  191. def OAI.SnakyPrototype.Certificate21.required_57 line 357
  192. def OAI.SnakyPrototype.Certificate21.envelope_57 line 358
  193. def OAI.SnakyPrototype.Certificate21.childrenC_57 line 359
  194. def OAI.SnakyPrototype.Certificate21.childrenD_57 line 360
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_57 line 361
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_57 line 362
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_57 line 363
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_57 line 364
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_57 line 365
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_57 line 370
  201. def OAI.SnakyPrototype.Certificate21.required_58 line 375
  202. def OAI.SnakyPrototype.Certificate21.envelope_58 line 376
  203. def OAI.SnakyPrototype.Certificate21.childrenC_58 line 377
  204. def OAI.SnakyPrototype.Certificate21.childrenD_58 line 378
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_58 line 379
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_58 line 380
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_58 line 381
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_58 line 382
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_58 line 383
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_58 line 388
  211. def OAI.SnakyPrototype.Certificate21.required_60 line 393
  212. def OAI.SnakyPrototype.Certificate21.envelope_60 line 394
  213. def OAI.SnakyPrototype.Certificate21.childrenC_60 line 395
  214. def OAI.SnakyPrototype.Certificate21.childrenD_60 line 396
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_60 line 397
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_60 line 398
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_60 line 399
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_60 line 400
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_60 line 401
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_60 line 406
  221. def OAI.SnakyPrototype.Certificate21.required_63 line 411
  222. def OAI.SnakyPrototype.Certificate21.envelope_63 line 412
  223. def OAI.SnakyPrototype.Certificate21.childrenC_63 line 413
  224. def OAI.SnakyPrototype.Certificate21.childrenD_63 line 414
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_63 line 415
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_63 line 416
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_63 line 417
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_63 line 418
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_63 line 419
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_63 line 425
  231. def OAI.SnakyPrototype.Certificate21.required_65 line 430
  232. def OAI.SnakyPrototype.Certificate21.envelope_65 line 431
  233. def OAI.SnakyPrototype.Certificate21.childrenC_65 line 432
  234. def OAI.SnakyPrototype.Certificate21.childrenD_65 line 433
  235. theorem OAI.SnakyPrototype.Certificate21.common_sub_65 line 434
  236. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_65 line 435
  237. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_65 line 436
  238. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_65 line 437
  239. theorem OAI.SnakyPrototype.Certificate21.children_work_65 line 438
  240. theorem OAI.SnakyPrototype.Certificate21.row_works_65 line 443
  241. def OAI.SnakyPrototype.Certificate21.height_10 line 448
  242. def OAI.SnakyPrototype.Certificate21.childrenH_10 line 449
  243. theorem OAI.SnakyPrototype.Certificate21.height_exact_10 line 450
  244. theorem OAI.SnakyPrototype.Certificate21.required_origin_10 line 451
  245. theorem OAI.SnakyPrototype.Certificate21.required_exact_10 line 453
  246. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_10 line 457
  247. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_10 line 459
  248. def OAI.SnakyPrototype.Certificate21.checked_10 line 463
  249. def OAI.SnakyPrototype.Certificate21.height_12 line 471
  250. def OAI.SnakyPrototype.Certificate21.childrenH_12 line 472
  251. theorem OAI.SnakyPrototype.Certificate21.height_exact_12 line 473
  252. theorem OAI.SnakyPrototype.Certificate21.required_origin_12 line 474
  253. theorem OAI.SnakyPrototype.Certificate21.required_exact_12 line 476
  254. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_12 line 480
  255. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_12 line 482
  256. def OAI.SnakyPrototype.Certificate21.checked_12 line 486
  257. def OAI.SnakyPrototype.Certificate21.height_13 line 494
  258. def OAI.SnakyPrototype.Certificate21.childrenH_13 line 495
  259. theorem OAI.SnakyPrototype.Certificate21.height_exact_13 line 496
  260. theorem OAI.SnakyPrototype.Certificate21.required_origin_13 line 497
  261. theorem OAI.SnakyPrototype.Certificate21.required_exact_13 line 499
  262. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_13 line 503
  263. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_13 line 505
  264. def OAI.SnakyPrototype.Certificate21.checked_13 line 509
  265. def OAI.SnakyPrototype.Certificate21.height_14 line 517
  266. def OAI.SnakyPrototype.Certificate21.childrenH_14 line 518
  267. theorem OAI.SnakyPrototype.Certificate21.height_exact_14 line 519
  268. theorem OAI.SnakyPrototype.Certificate21.required_origin_14 line 520
  269. theorem OAI.SnakyPrototype.Certificate21.required_exact_14 line 522
  270. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_14 line 526
  271. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_14 line 528
  272. def OAI.SnakyPrototype.Certificate21.checked_14 line 532
  273. def OAI.SnakyPrototype.Certificate21.height_17 line 540
  274. def OAI.SnakyPrototype.Certificate21.childrenH_17 line 541
  275. theorem OAI.SnakyPrototype.Certificate21.height_exact_17 line 542
  276. theorem OAI.SnakyPrototype.Certificate21.required_origin_17 line 543
  277. theorem OAI.SnakyPrototype.Certificate21.required_exact_17 line 545
  278. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_17 line 549
  279. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_17 line 551
  280. def OAI.SnakyPrototype.Certificate21.checked_17 line 555
  281. def OAI.SnakyPrototype.Certificate21.height_18 line 563
  282. def OAI.SnakyPrototype.Certificate21.childrenH_18 line 564
  283. theorem OAI.SnakyPrototype.Certificate21.height_exact_18 line 565
  284. theorem OAI.SnakyPrototype.Certificate21.required_origin_18 line 566
  285. theorem OAI.SnakyPrototype.Certificate21.required_exact_18 line 568
  286. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_18 line 572
  287. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_18 line 574
  288. def OAI.SnakyPrototype.Certificate21.checked_18 line 578
  289. def OAI.SnakyPrototype.Certificate21.height_26 line 586
  290. def OAI.SnakyPrototype.Certificate21.childrenH_26 line 587
  291. theorem OAI.SnakyPrototype.Certificate21.height_exact_26 line 588
  292. theorem OAI.SnakyPrototype.Certificate21.required_origin_26 line 589
  293. theorem OAI.SnakyPrototype.Certificate21.required_exact_26 line 591
  294. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_26 line 595
  295. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_26 line 597
  296. def OAI.SnakyPrototype.Certificate21.checked_26 line 601
  297. def OAI.SnakyPrototype.Certificate21.height_27 line 609
  298. def OAI.SnakyPrototype.Certificate21.childrenH_27 line 610
  299. theorem OAI.SnakyPrototype.Certificate21.height_exact_27 line 611
  300. theorem OAI.SnakyPrototype.Certificate21.required_origin_27 line 612
  301. theorem OAI.SnakyPrototype.Certificate21.required_exact_27 line 614
  302. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_27 line 618
  303. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_27 line 620
  304. def OAI.SnakyPrototype.Certificate21.checked_27 line 624
  305. def OAI.SnakyPrototype.Certificate21.height_31 line 632
  306. def OAI.SnakyPrototype.Certificate21.childrenH_31 line 633
  307. theorem OAI.SnakyPrototype.Certificate21.height_exact_31 line 634
  308. theorem OAI.SnakyPrototype.Certificate21.required_origin_31 line 635
  309. theorem OAI.SnakyPrototype.Certificate21.required_exact_31 line 637
  310. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_31 line 641
  311. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_31 line 643
  312. def OAI.SnakyPrototype.Certificate21.checked_31 line 647
  313. def OAI.SnakyPrototype.Certificate21.height_33 line 655
  314. def OAI.SnakyPrototype.Certificate21.childrenH_33 line 656
  315. theorem OAI.SnakyPrototype.Certificate21.height_exact_33 line 657
  316. theorem OAI.SnakyPrototype.Certificate21.required_origin_33 line 658
  317. theorem OAI.SnakyPrototype.Certificate21.required_exact_33 line 660
  318. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_33 line 664
  319. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_33 line 666
  320. def OAI.SnakyPrototype.Certificate21.checked_33 line 670
  321. def OAI.SnakyPrototype.Certificate21.height_39 line 678
  322. def OAI.SnakyPrototype.Certificate21.childrenH_39 line 679
  323. theorem OAI.SnakyPrototype.Certificate21.height_exact_39 line 680
  324. theorem OAI.SnakyPrototype.Certificate21.required_origin_39 line 681
  325. theorem OAI.SnakyPrototype.Certificate21.required_exact_39 line 683
  326. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_39 line 687
  327. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_39 line 689
  328. def OAI.SnakyPrototype.Certificate21.checked_39 line 693
  329. def OAI.SnakyPrototype.Certificate21.height_41 line 701
  330. def OAI.SnakyPrototype.Certificate21.childrenH_41 line 702
  331. theorem OAI.SnakyPrototype.Certificate21.height_exact_41 line 703
  332. theorem OAI.SnakyPrototype.Certificate21.required_origin_41 line 704
  333. theorem OAI.SnakyPrototype.Certificate21.required_exact_41 line 706
  334. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_41 line 710
  335. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_41 line 712
  336. def OAI.SnakyPrototype.Certificate21.checked_41 line 716
  337. def OAI.SnakyPrototype.Certificate21.height_42 line 724
  338. def OAI.SnakyPrototype.Certificate21.childrenH_42 line 725
  339. theorem OAI.SnakyPrototype.Certificate21.height_exact_42 line 726
  340. theorem OAI.SnakyPrototype.Certificate21.required_origin_42 line 727
  341. theorem OAI.SnakyPrototype.Certificate21.required_exact_42 line 729
  342. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_42 line 733
  343. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_42 line 735
  344. def OAI.SnakyPrototype.Certificate21.checked_42 line 739
  345. def OAI.SnakyPrototype.Certificate21.height_46 line 747
  346. def OAI.SnakyPrototype.Certificate21.childrenH_46 line 748
  347. theorem OAI.SnakyPrototype.Certificate21.height_exact_46 line 749
  348. theorem OAI.SnakyPrototype.Certificate21.required_origin_46 line 750
  349. theorem OAI.SnakyPrototype.Certificate21.required_exact_46 line 752
  350. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_46 line 756
  351. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_46 line 758
  352. def OAI.SnakyPrototype.Certificate21.checked_46 line 762
  353. def OAI.SnakyPrototype.Certificate21.height_48 line 770
  354. def OAI.SnakyPrototype.Certificate21.childrenH_48 line 771
  355. theorem OAI.SnakyPrototype.Certificate21.height_exact_48 line 772
  356. theorem OAI.SnakyPrototype.Certificate21.required_origin_48 line 773
  357. theorem OAI.SnakyPrototype.Certificate21.required_exact_48 line 775
  358. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_48 line 779
  359. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_48 line 781
  360. def OAI.SnakyPrototype.Certificate21.checked_48 line 785
  361. def OAI.SnakyPrototype.Certificate21.height_49 line 793
  362. def OAI.SnakyPrototype.Certificate21.childrenH_49 line 794
  363. theorem OAI.SnakyPrototype.Certificate21.height_exact_49 line 795
  364. theorem OAI.SnakyPrototype.Certificate21.required_origin_49 line 796
  365. theorem OAI.SnakyPrototype.Certificate21.required_exact_49 line 798
  366. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_49 line 802
  367. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_49 line 804
  368. def OAI.SnakyPrototype.Certificate21.checked_49 line 808
  369. def OAI.SnakyPrototype.Certificate21.height_50 line 816
  370. def OAI.SnakyPrototype.Certificate21.childrenH_50 line 817
  371. theorem OAI.SnakyPrototype.Certificate21.height_exact_50 line 818
  372. theorem OAI.SnakyPrototype.Certificate21.required_origin_50 line 819
  373. theorem OAI.SnakyPrototype.Certificate21.required_exact_50 line 821
  374. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_50 line 825
  375. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_50 line 827
  376. def OAI.SnakyPrototype.Certificate21.checked_50 line 831
  377. def OAI.SnakyPrototype.Certificate21.height_55 line 839
  378. def OAI.SnakyPrototype.Certificate21.childrenH_55 line 840
  379. theorem OAI.SnakyPrototype.Certificate21.height_exact_55 line 841
  380. theorem OAI.SnakyPrototype.Certificate21.required_origin_55 line 842
  381. theorem OAI.SnakyPrototype.Certificate21.required_exact_55 line 844
  382. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_55 line 848
  383. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_55 line 850
  384. def OAI.SnakyPrototype.Certificate21.checked_55 line 854
  385. def OAI.SnakyPrototype.Certificate21.height_56 line 862
  386. def OAI.SnakyPrototype.Certificate21.childrenH_56 line 863
  387. theorem OAI.SnakyPrototype.Certificate21.height_exact_56 line 864
  388. theorem OAI.SnakyPrototype.Certificate21.required_origin_56 line 865
  389. theorem OAI.SnakyPrototype.Certificate21.required_exact_56 line 867
  390. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_56 line 871
  391. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_56 line 873
  392. def OAI.SnakyPrototype.Certificate21.checked_56 line 877
  393. def OAI.SnakyPrototype.Certificate21.height_57 line 885
  394. def OAI.SnakyPrototype.Certificate21.childrenH_57 line 886
  395. theorem OAI.SnakyPrototype.Certificate21.height_exact_57 line 887
  396. theorem OAI.SnakyPrototype.Certificate21.required_origin_57 line 888
  397. theorem OAI.SnakyPrototype.Certificate21.required_exact_57 line 890
  398. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_57 line 894
  399. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_57 line 896
  400. def OAI.SnakyPrototype.Certificate21.checked_57 line 900
  401. def OAI.SnakyPrototype.Certificate21.height_58 line 908
  402. def OAI.SnakyPrototype.Certificate21.childrenH_58 line 909
  403. theorem OAI.SnakyPrototype.Certificate21.height_exact_58 line 910
  404. theorem OAI.SnakyPrototype.Certificate21.required_origin_58 line 911
  405. theorem OAI.SnakyPrototype.Certificate21.required_exact_58 line 913
  406. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_58 line 917
  407. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_58 line 919
  408. def OAI.SnakyPrototype.Certificate21.checked_58 line 923
  409. def OAI.SnakyPrototype.Certificate21.height_60 line 931
  410. def OAI.SnakyPrototype.Certificate21.childrenH_60 line 932
  411. theorem OAI.SnakyPrototype.Certificate21.height_exact_60 line 933
  412. theorem OAI.SnakyPrototype.Certificate21.required_origin_60 line 934
  413. theorem OAI.SnakyPrototype.Certificate21.required_exact_60 line 936
  414. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_60 line 940
  415. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_60 line 942
  416. def OAI.SnakyPrototype.Certificate21.checked_60 line 946
  417. def OAI.SnakyPrototype.Certificate21.height_63 line 954
  418. def OAI.SnakyPrototype.Certificate21.childrenH_63 line 955
  419. theorem OAI.SnakyPrototype.Certificate21.height_exact_63 line 956
  420. theorem OAI.SnakyPrototype.Certificate21.required_origin_63 line 957
  421. theorem OAI.SnakyPrototype.Certificate21.required_exact_63 line 959
  422. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_63 line 963
  423. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_63 line 965
  424. def OAI.SnakyPrototype.Certificate21.checked_63 line 969
  425. def OAI.SnakyPrototype.Certificate21.height_65 line 977
  426. def OAI.SnakyPrototype.Certificate21.childrenH_65 line 978
  427. theorem OAI.SnakyPrototype.Certificate21.height_exact_65 line 979
  428. theorem OAI.SnakyPrototype.Certificate21.required_origin_65 line 980
  429. theorem OAI.SnakyPrototype.Certificate21.required_exact_65 line 982
  430. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_65 line 986
  431. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_65 line 988
  432. def OAI.SnakyPrototype.Certificate21.checked_65 line 992