OAI/GameTheory/SnakyTwentyOne/Cards/Height03Part01.lean

GitHub source file

432 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_7 line 10
  2. def OAI.SnakyPrototype.Certificate21.envelope_7 line 11
  3. def OAI.SnakyPrototype.Certificate21.childrenC_7 line 12
  4. def OAI.SnakyPrototype.Certificate21.childrenD_7 line 13
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_7 line 14
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_7 line 15
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_7 line 16
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_7 line 17
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_7 line 18
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_7 line 23
  11. def OAI.SnakyPrototype.Certificate21.required_8 line 28
  12. def OAI.SnakyPrototype.Certificate21.envelope_8 line 29
  13. def OAI.SnakyPrototype.Certificate21.childrenC_8 line 30
  14. def OAI.SnakyPrototype.Certificate21.childrenD_8 line 31
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_8 line 32
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_8 line 33
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_8 line 34
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_8 line 35
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_8 line 36
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_8 line 41
  21. def OAI.SnakyPrototype.Certificate21.required_9 line 46
  22. def OAI.SnakyPrototype.Certificate21.envelope_9 line 47
  23. def OAI.SnakyPrototype.Certificate21.childrenC_9 line 48
  24. def OAI.SnakyPrototype.Certificate21.childrenD_9 line 49
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_9 line 50
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_9 line 51
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_9 line 52
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_9 line 53
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_9 line 54
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_9 line 59
  31. def OAI.SnakyPrototype.Certificate21.required_16 line 64
  32. def OAI.SnakyPrototype.Certificate21.envelope_16 line 65
  33. def OAI.SnakyPrototype.Certificate21.childrenC_16 line 66
  34. def OAI.SnakyPrototype.Certificate21.childrenD_16 line 67
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_16 line 68
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_16 line 69
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_16 line 70
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_16 line 71
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_16 line 72
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_16 line 77
  41. def OAI.SnakyPrototype.Certificate21.required_20 line 82
  42. def OAI.SnakyPrototype.Certificate21.envelope_20 line 83
  43. def OAI.SnakyPrototype.Certificate21.childrenC_20 line 84
  44. def OAI.SnakyPrototype.Certificate21.childrenD_20 line 85
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_20 line 86
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_20 line 87
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_20 line 88
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_20 line 89
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_20 line 90
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_20 line 95
  51. def OAI.SnakyPrototype.Certificate21.required_21 line 100
  52. def OAI.SnakyPrototype.Certificate21.envelope_21 line 101
  53. def OAI.SnakyPrototype.Certificate21.childrenC_21 line 102
  54. def OAI.SnakyPrototype.Certificate21.childrenD_21 line 103
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_21 line 104
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_21 line 105
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_21 line 106
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_21 line 107
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_21 line 108
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_21 line 113
  61. def OAI.SnakyPrototype.Certificate21.required_24 line 118
  62. def OAI.SnakyPrototype.Certificate21.envelope_24 line 119
  63. def OAI.SnakyPrototype.Certificate21.childrenC_24 line 120
  64. def OAI.SnakyPrototype.Certificate21.childrenD_24 line 121
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_24 line 122
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_24 line 123
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_24 line 124
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_24 line 125
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_24 line 126
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_24 line 131
  71. def OAI.SnakyPrototype.Certificate21.required_29 line 136
  72. def OAI.SnakyPrototype.Certificate21.envelope_29 line 137
  73. def OAI.SnakyPrototype.Certificate21.childrenC_29 line 138
  74. def OAI.SnakyPrototype.Certificate21.childrenD_29 line 139
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_29 line 140
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_29 line 141
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_29 line 142
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_29 line 143
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_29 line 144
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_29 line 149
  81. def OAI.SnakyPrototype.Certificate21.required_37 line 154
  82. def OAI.SnakyPrototype.Certificate21.envelope_37 line 155
  83. def OAI.SnakyPrototype.Certificate21.childrenC_37 line 156
  84. def OAI.SnakyPrototype.Certificate21.childrenD_37 line 157
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_37 line 158
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_37 line 159
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_37 line 160
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_37 line 161
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_37 line 162
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_37 line 167
  91. def OAI.SnakyPrototype.Certificate21.required_44 line 172
  92. def OAI.SnakyPrototype.Certificate21.envelope_44 line 173
  93. def OAI.SnakyPrototype.Certificate21.childrenC_44 line 174
  94. def OAI.SnakyPrototype.Certificate21.childrenD_44 line 175
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_44 line 176
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_44 line 177
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_44 line 178
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_44 line 179
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_44 line 180
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_44 line 185
  101. def OAI.SnakyPrototype.Certificate21.required_45 line 190
  102. def OAI.SnakyPrototype.Certificate21.envelope_45 line 191
  103. def OAI.SnakyPrototype.Certificate21.childrenC_45 line 192
  104. def OAI.SnakyPrototype.Certificate21.childrenD_45 line 193
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_45 line 194
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_45 line 195
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_45 line 196
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_45 line 197
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_45 line 198
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_45 line 203
  111. def OAI.SnakyPrototype.Certificate21.required_52 line 208
  112. def OAI.SnakyPrototype.Certificate21.envelope_52 line 209
  113. def OAI.SnakyPrototype.Certificate21.childrenC_52 line 210
  114. def OAI.SnakyPrototype.Certificate21.childrenD_52 line 211
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_52 line 212
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_52 line 213
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_52 line 214
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_52 line 215
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_52 line 216
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_52 line 221
  121. def OAI.SnakyPrototype.Certificate21.required_53 line 226
  122. def OAI.SnakyPrototype.Certificate21.envelope_53 line 227
  123. def OAI.SnakyPrototype.Certificate21.childrenC_53 line 228
  124. def OAI.SnakyPrototype.Certificate21.childrenD_53 line 229
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_53 line 230
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_53 line 231
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_53 line 232
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_53 line 233
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_53 line 234
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_53 line 239
  131. def OAI.SnakyPrototype.Certificate21.required_54 line 244
  132. def OAI.SnakyPrototype.Certificate21.envelope_54 line 245
  133. def OAI.SnakyPrototype.Certificate21.childrenC_54 line 246
  134. def OAI.SnakyPrototype.Certificate21.childrenD_54 line 247
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_54 line 248
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_54 line 249
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_54 line 250
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_54 line 251
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_54 line 252
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_54 line 257
  141. def OAI.SnakyPrototype.Certificate21.required_61 line 262
  142. def OAI.SnakyPrototype.Certificate21.envelope_61 line 263
  143. def OAI.SnakyPrototype.Certificate21.childrenC_61 line 264
  144. def OAI.SnakyPrototype.Certificate21.childrenD_61 line 265
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_61 line 266
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_61 line 267
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_61 line 268
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_61 line 269
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_61 line 270
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_61 line 275
  151. def OAI.SnakyPrototype.Certificate21.required_62 line 280
  152. def OAI.SnakyPrototype.Certificate21.envelope_62 line 281
  153. def OAI.SnakyPrototype.Certificate21.childrenC_62 line 282
  154. def OAI.SnakyPrototype.Certificate21.childrenD_62 line 283
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_62 line 284
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_62 line 285
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_62 line 286
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_62 line 287
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_62 line 288
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_62 line 293
  161. def OAI.SnakyPrototype.Certificate21.required_64 line 298
  162. def OAI.SnakyPrototype.Certificate21.envelope_64 line 299
  163. def OAI.SnakyPrototype.Certificate21.childrenC_64 line 300
  164. def OAI.SnakyPrototype.Certificate21.childrenD_64 line 301
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_64 line 302
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_64 line 303
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_64 line 304
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_64 line 305
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_64 line 306
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_64 line 311
  171. def OAI.SnakyPrototype.Certificate21.required_69 line 316
  172. def OAI.SnakyPrototype.Certificate21.envelope_69 line 317
  173. def OAI.SnakyPrototype.Certificate21.childrenC_69 line 318
  174. def OAI.SnakyPrototype.Certificate21.childrenD_69 line 319
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_69 line 320
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_69 line 321
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_69 line 322
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_69 line 323
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_69 line 324
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_69 line 329
  181. def OAI.SnakyPrototype.Certificate21.required_74 line 334
  182. def OAI.SnakyPrototype.Certificate21.envelope_74 line 335
  183. def OAI.SnakyPrototype.Certificate21.childrenC_74 line 336
  184. def OAI.SnakyPrototype.Certificate21.childrenD_74 line 337
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_74 line 338
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_74 line 339
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_74 line 340
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_74 line 341
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_74 line 342
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_74 line 349
  191. def OAI.SnakyPrototype.Certificate21.required_78 line 354
  192. def OAI.SnakyPrototype.Certificate21.envelope_78 line 355
  193. def OAI.SnakyPrototype.Certificate21.childrenC_78 line 356
  194. def OAI.SnakyPrototype.Certificate21.childrenD_78 line 357
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_78 line 358
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_78 line 359
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_78 line 360
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_78 line 361
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_78 line 362
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_78 line 367
  201. def OAI.SnakyPrototype.Certificate21.required_87 line 372
  202. def OAI.SnakyPrototype.Certificate21.envelope_87 line 373
  203. def OAI.SnakyPrototype.Certificate21.childrenC_87 line 374
  204. def OAI.SnakyPrototype.Certificate21.childrenD_87 line 375
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_87 line 376
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_87 line 377
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_87 line 378
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_87 line 379
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_87 line 380
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_87 line 385
  211. def OAI.SnakyPrototype.Certificate21.required_101 line 390
  212. def OAI.SnakyPrototype.Certificate21.envelope_101 line 391
  213. def OAI.SnakyPrototype.Certificate21.childrenC_101 line 392
  214. def OAI.SnakyPrototype.Certificate21.childrenD_101 line 393
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_101 line 394
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_101 line 395
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_101 line 396
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_101 line 397
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_101 line 398
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_101 line 403
  221. def OAI.SnakyPrototype.Certificate21.required_103 line 408
  222. def OAI.SnakyPrototype.Certificate21.envelope_103 line 409
  223. def OAI.SnakyPrototype.Certificate21.childrenC_103 line 410
  224. def OAI.SnakyPrototype.Certificate21.childrenD_103 line 411
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_103 line 412
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_103 line 413
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_103 line 414
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_103 line 415
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_103 line 416
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_103 line 421
  231. def OAI.SnakyPrototype.Certificate21.required_105 line 426
  232. def OAI.SnakyPrototype.Certificate21.envelope_105 line 427
  233. def OAI.SnakyPrototype.Certificate21.childrenC_105 line 428
  234. def OAI.SnakyPrototype.Certificate21.childrenD_105 line 429
  235. theorem OAI.SnakyPrototype.Certificate21.common_sub_105 line 430
  236. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_105 line 431
  237. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_105 line 432
  238. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_105 line 433
  239. theorem OAI.SnakyPrototype.Certificate21.children_work_105 line 434
  240. theorem OAI.SnakyPrototype.Certificate21.row_works_105 line 439
  241. def OAI.SnakyPrototype.Certificate21.height_7 line 444
  242. def OAI.SnakyPrototype.Certificate21.childrenH_7 line 445
  243. theorem OAI.SnakyPrototype.Certificate21.height_exact_7 line 446
  244. theorem OAI.SnakyPrototype.Certificate21.required_origin_7 line 447
  245. theorem OAI.SnakyPrototype.Certificate21.required_exact_7 line 449
  246. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_7 line 453
  247. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_7 line 455
  248. def OAI.SnakyPrototype.Certificate21.checked_7 line 459
  249. def OAI.SnakyPrototype.Certificate21.height_8 line 467
  250. def OAI.SnakyPrototype.Certificate21.childrenH_8 line 468
  251. theorem OAI.SnakyPrototype.Certificate21.height_exact_8 line 469
  252. theorem OAI.SnakyPrototype.Certificate21.required_origin_8 line 470
  253. theorem OAI.SnakyPrototype.Certificate21.required_exact_8 line 472
  254. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_8 line 476
  255. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_8 line 478
  256. def OAI.SnakyPrototype.Certificate21.checked_8 line 482
  257. def OAI.SnakyPrototype.Certificate21.height_9 line 490
  258. def OAI.SnakyPrototype.Certificate21.childrenH_9 line 491
  259. theorem OAI.SnakyPrototype.Certificate21.height_exact_9 line 492
  260. theorem OAI.SnakyPrototype.Certificate21.required_origin_9 line 493
  261. theorem OAI.SnakyPrototype.Certificate21.required_exact_9 line 495
  262. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_9 line 499
  263. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_9 line 501
  264. def OAI.SnakyPrototype.Certificate21.checked_9 line 505
  265. def OAI.SnakyPrototype.Certificate21.height_16 line 513
  266. def OAI.SnakyPrototype.Certificate21.childrenH_16 line 514
  267. theorem OAI.SnakyPrototype.Certificate21.height_exact_16 line 515
  268. theorem OAI.SnakyPrototype.Certificate21.required_origin_16 line 516
  269. theorem OAI.SnakyPrototype.Certificate21.required_exact_16 line 518
  270. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_16 line 522
  271. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_16 line 524
  272. def OAI.SnakyPrototype.Certificate21.checked_16 line 528
  273. def OAI.SnakyPrototype.Certificate21.height_20 line 536
  274. def OAI.SnakyPrototype.Certificate21.childrenH_20 line 537
  275. theorem OAI.SnakyPrototype.Certificate21.height_exact_20 line 538
  276. theorem OAI.SnakyPrototype.Certificate21.required_origin_20 line 539
  277. theorem OAI.SnakyPrototype.Certificate21.required_exact_20 line 541
  278. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_20 line 545
  279. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_20 line 547
  280. def OAI.SnakyPrototype.Certificate21.checked_20 line 551
  281. def OAI.SnakyPrototype.Certificate21.height_21 line 559
  282. def OAI.SnakyPrototype.Certificate21.childrenH_21 line 560
  283. theorem OAI.SnakyPrototype.Certificate21.height_exact_21 line 561
  284. theorem OAI.SnakyPrototype.Certificate21.required_origin_21 line 562
  285. theorem OAI.SnakyPrototype.Certificate21.required_exact_21 line 564
  286. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_21 line 568
  287. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_21 line 570
  288. def OAI.SnakyPrototype.Certificate21.checked_21 line 574
  289. def OAI.SnakyPrototype.Certificate21.height_24 line 582
  290. def OAI.SnakyPrototype.Certificate21.childrenH_24 line 583
  291. theorem OAI.SnakyPrototype.Certificate21.height_exact_24 line 584
  292. theorem OAI.SnakyPrototype.Certificate21.required_origin_24 line 585
  293. theorem OAI.SnakyPrototype.Certificate21.required_exact_24 line 587
  294. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_24 line 591
  295. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_24 line 593
  296. def OAI.SnakyPrototype.Certificate21.checked_24 line 597
  297. def OAI.SnakyPrototype.Certificate21.height_29 line 605
  298. def OAI.SnakyPrototype.Certificate21.childrenH_29 line 606
  299. theorem OAI.SnakyPrototype.Certificate21.height_exact_29 line 607
  300. theorem OAI.SnakyPrototype.Certificate21.required_origin_29 line 608
  301. theorem OAI.SnakyPrototype.Certificate21.required_exact_29 line 610
  302. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_29 line 614
  303. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_29 line 616
  304. def OAI.SnakyPrototype.Certificate21.checked_29 line 620
  305. def OAI.SnakyPrototype.Certificate21.height_37 line 628
  306. def OAI.SnakyPrototype.Certificate21.childrenH_37 line 629
  307. theorem OAI.SnakyPrototype.Certificate21.height_exact_37 line 630
  308. theorem OAI.SnakyPrototype.Certificate21.required_origin_37 line 631
  309. theorem OAI.SnakyPrototype.Certificate21.required_exact_37 line 633
  310. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_37 line 637
  311. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_37 line 639
  312. def OAI.SnakyPrototype.Certificate21.checked_37 line 643
  313. def OAI.SnakyPrototype.Certificate21.height_44 line 651
  314. def OAI.SnakyPrototype.Certificate21.childrenH_44 line 652
  315. theorem OAI.SnakyPrototype.Certificate21.height_exact_44 line 653
  316. theorem OAI.SnakyPrototype.Certificate21.required_origin_44 line 654
  317. theorem OAI.SnakyPrototype.Certificate21.required_exact_44 line 656
  318. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_44 line 660
  319. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_44 line 662
  320. def OAI.SnakyPrototype.Certificate21.checked_44 line 666
  321. def OAI.SnakyPrototype.Certificate21.height_45 line 674
  322. def OAI.SnakyPrototype.Certificate21.childrenH_45 line 675
  323. theorem OAI.SnakyPrototype.Certificate21.height_exact_45 line 676
  324. theorem OAI.SnakyPrototype.Certificate21.required_origin_45 line 677
  325. theorem OAI.SnakyPrototype.Certificate21.required_exact_45 line 679
  326. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_45 line 683
  327. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_45 line 685
  328. def OAI.SnakyPrototype.Certificate21.checked_45 line 689
  329. def OAI.SnakyPrototype.Certificate21.height_52 line 697
  330. def OAI.SnakyPrototype.Certificate21.childrenH_52 line 698
  331. theorem OAI.SnakyPrototype.Certificate21.height_exact_52 line 699
  332. theorem OAI.SnakyPrototype.Certificate21.required_origin_52 line 700
  333. theorem OAI.SnakyPrototype.Certificate21.required_exact_52 line 702
  334. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_52 line 706
  335. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_52 line 708
  336. def OAI.SnakyPrototype.Certificate21.checked_52 line 712
  337. def OAI.SnakyPrototype.Certificate21.height_53 line 720
  338. def OAI.SnakyPrototype.Certificate21.childrenH_53 line 721
  339. theorem OAI.SnakyPrototype.Certificate21.height_exact_53 line 722
  340. theorem OAI.SnakyPrototype.Certificate21.required_origin_53 line 723
  341. theorem OAI.SnakyPrototype.Certificate21.required_exact_53 line 725
  342. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_53 line 729
  343. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_53 line 731
  344. def OAI.SnakyPrototype.Certificate21.checked_53 line 735
  345. def OAI.SnakyPrototype.Certificate21.height_54 line 743
  346. def OAI.SnakyPrototype.Certificate21.childrenH_54 line 744
  347. theorem OAI.SnakyPrototype.Certificate21.height_exact_54 line 745
  348. theorem OAI.SnakyPrototype.Certificate21.required_origin_54 line 746
  349. theorem OAI.SnakyPrototype.Certificate21.required_exact_54 line 748
  350. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_54 line 752
  351. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_54 line 754
  352. def OAI.SnakyPrototype.Certificate21.checked_54 line 758
  353. def OAI.SnakyPrototype.Certificate21.height_61 line 766
  354. def OAI.SnakyPrototype.Certificate21.childrenH_61 line 767
  355. theorem OAI.SnakyPrototype.Certificate21.height_exact_61 line 768
  356. theorem OAI.SnakyPrototype.Certificate21.required_origin_61 line 769
  357. theorem OAI.SnakyPrototype.Certificate21.required_exact_61 line 771
  358. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_61 line 775
  359. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_61 line 777
  360. def OAI.SnakyPrototype.Certificate21.checked_61 line 781
  361. def OAI.SnakyPrototype.Certificate21.height_62 line 789
  362. def OAI.SnakyPrototype.Certificate21.childrenH_62 line 790
  363. theorem OAI.SnakyPrototype.Certificate21.height_exact_62 line 791
  364. theorem OAI.SnakyPrototype.Certificate21.required_origin_62 line 792
  365. theorem OAI.SnakyPrototype.Certificate21.required_exact_62 line 794
  366. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_62 line 798
  367. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_62 line 800
  368. def OAI.SnakyPrototype.Certificate21.checked_62 line 804
  369. def OAI.SnakyPrototype.Certificate21.height_64 line 812
  370. def OAI.SnakyPrototype.Certificate21.childrenH_64 line 813
  371. theorem OAI.SnakyPrototype.Certificate21.height_exact_64 line 814
  372. theorem OAI.SnakyPrototype.Certificate21.required_origin_64 line 815
  373. theorem OAI.SnakyPrototype.Certificate21.required_exact_64 line 817
  374. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_64 line 821
  375. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_64 line 823
  376. def OAI.SnakyPrototype.Certificate21.checked_64 line 827
  377. def OAI.SnakyPrototype.Certificate21.height_69 line 835
  378. def OAI.SnakyPrototype.Certificate21.childrenH_69 line 836
  379. theorem OAI.SnakyPrototype.Certificate21.height_exact_69 line 837
  380. theorem OAI.SnakyPrototype.Certificate21.required_origin_69 line 838
  381. theorem OAI.SnakyPrototype.Certificate21.required_exact_69 line 840
  382. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_69 line 844
  383. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_69 line 846
  384. def OAI.SnakyPrototype.Certificate21.checked_69 line 850
  385. def OAI.SnakyPrototype.Certificate21.height_74 line 858
  386. def OAI.SnakyPrototype.Certificate21.childrenH_74 line 859
  387. theorem OAI.SnakyPrototype.Certificate21.height_exact_74 line 860
  388. theorem OAI.SnakyPrototype.Certificate21.required_origin_74 line 861
  389. theorem OAI.SnakyPrototype.Certificate21.required_exact_74 line 863
  390. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_74 line 867
  391. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_74 line 869
  392. def OAI.SnakyPrototype.Certificate21.checked_74 line 873
  393. def OAI.SnakyPrototype.Certificate21.height_78 line 881
  394. def OAI.SnakyPrototype.Certificate21.childrenH_78 line 882
  395. theorem OAI.SnakyPrototype.Certificate21.height_exact_78 line 883
  396. theorem OAI.SnakyPrototype.Certificate21.required_origin_78 line 884
  397. theorem OAI.SnakyPrototype.Certificate21.required_exact_78 line 886
  398. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_78 line 890
  399. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_78 line 892
  400. def OAI.SnakyPrototype.Certificate21.checked_78 line 896
  401. def OAI.SnakyPrototype.Certificate21.height_87 line 904
  402. def OAI.SnakyPrototype.Certificate21.childrenH_87 line 905
  403. theorem OAI.SnakyPrototype.Certificate21.height_exact_87 line 906
  404. theorem OAI.SnakyPrototype.Certificate21.required_origin_87 line 907
  405. theorem OAI.SnakyPrototype.Certificate21.required_exact_87 line 909
  406. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_87 line 913
  407. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_87 line 915
  408. def OAI.SnakyPrototype.Certificate21.checked_87 line 919
  409. def OAI.SnakyPrototype.Certificate21.height_101 line 927
  410. def OAI.SnakyPrototype.Certificate21.childrenH_101 line 928
  411. theorem OAI.SnakyPrototype.Certificate21.height_exact_101 line 929
  412. theorem OAI.SnakyPrototype.Certificate21.required_origin_101 line 930
  413. theorem OAI.SnakyPrototype.Certificate21.required_exact_101 line 932
  414. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_101 line 936
  415. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_101 line 938
  416. def OAI.SnakyPrototype.Certificate21.checked_101 line 942
  417. def OAI.SnakyPrototype.Certificate21.height_103 line 950
  418. def OAI.SnakyPrototype.Certificate21.childrenH_103 line 951
  419. theorem OAI.SnakyPrototype.Certificate21.height_exact_103 line 952
  420. theorem OAI.SnakyPrototype.Certificate21.required_origin_103 line 953
  421. theorem OAI.SnakyPrototype.Certificate21.required_exact_103 line 955
  422. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_103 line 959
  423. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_103 line 961
  424. def OAI.SnakyPrototype.Certificate21.checked_103 line 965
  425. def OAI.SnakyPrototype.Certificate21.height_105 line 973
  426. def OAI.SnakyPrototype.Certificate21.childrenH_105 line 974
  427. theorem OAI.SnakyPrototype.Certificate21.height_exact_105 line 975
  428. theorem OAI.SnakyPrototype.Certificate21.required_origin_105 line 976
  429. theorem OAI.SnakyPrototype.Certificate21.required_exact_105 line 978
  430. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_105 line 982
  431. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_105 line 984
  432. def OAI.SnakyPrototype.Certificate21.checked_105 line 988