OAI/GameTheory/SnakyTwentyOne/Cards/Height05Part01.lean

GitHub source file

432 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_19 line 15
  2. def OAI.SnakyPrototype.Certificate21.envelope_19 line 16
  3. def OAI.SnakyPrototype.Certificate21.childrenC_19 line 17
  4. def OAI.SnakyPrototype.Certificate21.childrenD_19 line 18
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_19 line 19
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_19 line 20
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_19 line 21
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_19 line 22
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_19 line 23
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_19 line 28
  11. def OAI.SnakyPrototype.Certificate21.required_47 line 33
  12. def OAI.SnakyPrototype.Certificate21.envelope_47 line 34
  13. def OAI.SnakyPrototype.Certificate21.childrenC_47 line 35
  14. def OAI.SnakyPrototype.Certificate21.childrenD_47 line 36
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_47 line 37
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_47 line 38
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_47 line 39
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_47 line 40
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_47 line 41
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_47 line 47
  21. def OAI.SnakyPrototype.Certificate21.required_59 line 52
  22. def OAI.SnakyPrototype.Certificate21.envelope_59 line 53
  23. def OAI.SnakyPrototype.Certificate21.childrenC_59 line 54
  24. def OAI.SnakyPrototype.Certificate21.childrenD_59 line 55
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_59 line 56
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_59 line 57
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_59 line 58
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_59 line 59
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_59 line 60
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_59 line 66
  31. def OAI.SnakyPrototype.Certificate21.required_71 line 71
  32. def OAI.SnakyPrototype.Certificate21.envelope_71 line 72
  33. def OAI.SnakyPrototype.Certificate21.childrenC_71 line 73
  34. def OAI.SnakyPrototype.Certificate21.childrenD_71 line 74
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_71 line 75
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_71 line 76
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_71 line 77
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_71 line 78
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_71 line 79
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_71 line 84
  41. def OAI.SnakyPrototype.Certificate21.required_72 line 89
  42. def OAI.SnakyPrototype.Certificate21.envelope_72 line 90
  43. def OAI.SnakyPrototype.Certificate21.childrenC_72 line 91
  44. def OAI.SnakyPrototype.Certificate21.childrenD_72 line 92
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_72 line 93
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_72 line 94
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_72 line 95
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_72 line 96
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_72 line 97
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_72 line 103
  51. def OAI.SnakyPrototype.Certificate21.required_81 line 108
  52. def OAI.SnakyPrototype.Certificate21.envelope_81 line 109
  53. def OAI.SnakyPrototype.Certificate21.childrenC_81 line 110
  54. def OAI.SnakyPrototype.Certificate21.childrenD_81 line 111
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_81 line 112
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_81 line 113
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_81 line 114
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_81 line 115
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_81 line 116
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_81 line 121
  61. def OAI.SnakyPrototype.Certificate21.required_84 line 126
  62. def OAI.SnakyPrototype.Certificate21.envelope_84 line 127
  63. def OAI.SnakyPrototype.Certificate21.childrenC_84 line 128
  64. def OAI.SnakyPrototype.Certificate21.childrenD_84 line 129
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_84 line 130
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_84 line 131
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_84 line 132
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_84 line 133
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_84 line 134
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_84 line 139
  71. def OAI.SnakyPrototype.Certificate21.required_100 line 144
  72. def OAI.SnakyPrototype.Certificate21.envelope_100 line 145
  73. def OAI.SnakyPrototype.Certificate21.childrenC_100 line 146
  74. def OAI.SnakyPrototype.Certificate21.childrenD_100 line 147
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_100 line 148
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_100 line 149
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_100 line 150
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_100 line 151
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_100 line 152
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_100 line 157
  81. def OAI.SnakyPrototype.Certificate21.required_104 line 162
  82. def OAI.SnakyPrototype.Certificate21.envelope_104 line 163
  83. def OAI.SnakyPrototype.Certificate21.childrenC_104 line 164
  84. def OAI.SnakyPrototype.Certificate21.childrenD_104 line 165
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_104 line 166
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_104 line 167
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_104 line 168
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_104 line 169
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_104 line 170
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_104 line 177
  91. def OAI.SnakyPrototype.Certificate21.required_107 line 182
  92. def OAI.SnakyPrototype.Certificate21.envelope_107 line 183
  93. def OAI.SnakyPrototype.Certificate21.childrenC_107 line 184
  94. def OAI.SnakyPrototype.Certificate21.childrenD_107 line 185
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_107 line 186
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_107 line 187
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_107 line 188
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_107 line 189
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_107 line 190
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_107 line 195
  101. def OAI.SnakyPrototype.Certificate21.required_111 line 200
  102. def OAI.SnakyPrototype.Certificate21.envelope_111 line 201
  103. def OAI.SnakyPrototype.Certificate21.childrenC_111 line 202
  104. def OAI.SnakyPrototype.Certificate21.childrenD_111 line 203
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_111 line 204
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_111 line 205
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_111 line 206
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_111 line 207
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_111 line 208
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_111 line 213
  111. def OAI.SnakyPrototype.Certificate21.required_114 line 218
  112. def OAI.SnakyPrototype.Certificate21.envelope_114 line 219
  113. def OAI.SnakyPrototype.Certificate21.childrenC_114 line 220
  114. def OAI.SnakyPrototype.Certificate21.childrenD_114 line 221
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_114 line 222
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_114 line 223
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_114 line 224
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_114 line 225
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_114 line 226
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_114 line 231
  121. def OAI.SnakyPrototype.Certificate21.required_122 line 236
  122. def OAI.SnakyPrototype.Certificate21.envelope_122 line 237
  123. def OAI.SnakyPrototype.Certificate21.childrenC_122 line 238
  124. def OAI.SnakyPrototype.Certificate21.childrenD_122 line 239
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_122 line 240
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_122 line 241
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_122 line 242
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_122 line 243
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_122 line 244
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_122 line 249
  131. def OAI.SnakyPrototype.Certificate21.required_133 line 254
  132. def OAI.SnakyPrototype.Certificate21.envelope_133 line 255
  133. def OAI.SnakyPrototype.Certificate21.childrenC_133 line 256
  134. def OAI.SnakyPrototype.Certificate21.childrenD_133 line 257
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_133 line 258
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_133 line 259
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_133 line 260
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_133 line 261
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_133 line 262
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_133 line 267
  141. def OAI.SnakyPrototype.Certificate21.required_142 line 272
  142. def OAI.SnakyPrototype.Certificate21.envelope_142 line 273
  143. def OAI.SnakyPrototype.Certificate21.childrenC_142 line 274
  144. def OAI.SnakyPrototype.Certificate21.childrenD_142 line 275
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_142 line 276
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_142 line 277
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_142 line 278
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_142 line 279
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_142 line 280
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_142 line 285
  151. def OAI.SnakyPrototype.Certificate21.required_144 line 290
  152. def OAI.SnakyPrototype.Certificate21.envelope_144 line 291
  153. def OAI.SnakyPrototype.Certificate21.childrenC_144 line 292
  154. def OAI.SnakyPrototype.Certificate21.childrenD_144 line 293
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_144 line 294
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_144 line 295
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_144 line 296
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_144 line 297
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_144 line 298
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_144 line 304
  161. def OAI.SnakyPrototype.Certificate21.required_145 line 309
  162. def OAI.SnakyPrototype.Certificate21.envelope_145 line 310
  163. def OAI.SnakyPrototype.Certificate21.childrenC_145 line 311
  164. def OAI.SnakyPrototype.Certificate21.childrenD_145 line 312
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_145 line 313
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_145 line 314
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_145 line 315
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_145 line 316
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_145 line 317
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_145 line 322
  171. def OAI.SnakyPrototype.Certificate21.required_147 line 327
  172. def OAI.SnakyPrototype.Certificate21.envelope_147 line 328
  173. def OAI.SnakyPrototype.Certificate21.childrenC_147 line 329
  174. def OAI.SnakyPrototype.Certificate21.childrenD_147 line 330
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_147 line 331
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_147 line 332
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_147 line 333
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_147 line 334
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_147 line 335
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_147 line 340
  181. def OAI.SnakyPrototype.Certificate21.required_152 line 345
  182. def OAI.SnakyPrototype.Certificate21.envelope_152 line 346
  183. def OAI.SnakyPrototype.Certificate21.childrenC_152 line 347
  184. def OAI.SnakyPrototype.Certificate21.childrenD_152 line 348
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_152 line 349
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_152 line 350
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_152 line 351
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_152 line 352
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_152 line 353
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_152 line 358
  191. def OAI.SnakyPrototype.Certificate21.required_155 line 363
  192. def OAI.SnakyPrototype.Certificate21.envelope_155 line 364
  193. def OAI.SnakyPrototype.Certificate21.childrenC_155 line 365
  194. def OAI.SnakyPrototype.Certificate21.childrenD_155 line 366
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_155 line 367
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_155 line 368
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_155 line 369
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_155 line 370
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_155 line 371
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_155 line 377
  201. def OAI.SnakyPrototype.Certificate21.required_164 line 382
  202. def OAI.SnakyPrototype.Certificate21.envelope_164 line 383
  203. def OAI.SnakyPrototype.Certificate21.childrenC_164 line 384
  204. def OAI.SnakyPrototype.Certificate21.childrenD_164 line 385
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_164 line 386
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_164 line 387
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_164 line 388
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_164 line 389
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_164 line 390
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_164 line 395
  211. def OAI.SnakyPrototype.Certificate21.required_175 line 400
  212. def OAI.SnakyPrototype.Certificate21.envelope_175 line 401
  213. def OAI.SnakyPrototype.Certificate21.childrenC_175 line 402
  214. def OAI.SnakyPrototype.Certificate21.childrenD_175 line 403
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_175 line 404
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_175 line 405
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_175 line 406
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_175 line 407
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_175 line 408
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_175 line 414
  221. def OAI.SnakyPrototype.Certificate21.required_176 line 419
  222. def OAI.SnakyPrototype.Certificate21.envelope_176 line 420
  223. def OAI.SnakyPrototype.Certificate21.childrenC_176 line 421
  224. def OAI.SnakyPrototype.Certificate21.childrenD_176 line 422
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_176 line 423
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_176 line 424
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_176 line 425
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_176 line 426
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_176 line 427
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_176 line 432
  231. def OAI.SnakyPrototype.Certificate21.required_179 line 437
  232. def OAI.SnakyPrototype.Certificate21.envelope_179 line 438
  233. def OAI.SnakyPrototype.Certificate21.childrenC_179 line 439
  234. def OAI.SnakyPrototype.Certificate21.childrenD_179 line 440
  235. theorem OAI.SnakyPrototype.Certificate21.common_sub_179 line 441
  236. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_179 line 442
  237. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_179 line 443
  238. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_179 line 444
  239. theorem OAI.SnakyPrototype.Certificate21.children_work_179 line 445
  240. theorem OAI.SnakyPrototype.Certificate21.row_works_179 line 450
  241. def OAI.SnakyPrototype.Certificate21.height_19 line 455
  242. def OAI.SnakyPrototype.Certificate21.childrenH_19 line 456
  243. theorem OAI.SnakyPrototype.Certificate21.height_exact_19 line 457
  244. theorem OAI.SnakyPrototype.Certificate21.required_origin_19 line 458
  245. theorem OAI.SnakyPrototype.Certificate21.required_exact_19 line 460
  246. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_19 line 464
  247. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_19 line 466
  248. def OAI.SnakyPrototype.Certificate21.checked_19 line 470
  249. def OAI.SnakyPrototype.Certificate21.height_47 line 478
  250. def OAI.SnakyPrototype.Certificate21.childrenH_47 line 479
  251. theorem OAI.SnakyPrototype.Certificate21.height_exact_47 line 480
  252. theorem OAI.SnakyPrototype.Certificate21.required_origin_47 line 481
  253. theorem OAI.SnakyPrototype.Certificate21.required_exact_47 line 483
  254. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_47 line 487
  255. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_47 line 489
  256. def OAI.SnakyPrototype.Certificate21.checked_47 line 493
  257. def OAI.SnakyPrototype.Certificate21.height_59 line 501
  258. def OAI.SnakyPrototype.Certificate21.childrenH_59 line 502
  259. theorem OAI.SnakyPrototype.Certificate21.height_exact_59 line 503
  260. theorem OAI.SnakyPrototype.Certificate21.required_origin_59 line 504
  261. theorem OAI.SnakyPrototype.Certificate21.required_exact_59 line 506
  262. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_59 line 510
  263. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_59 line 512
  264. def OAI.SnakyPrototype.Certificate21.checked_59 line 516
  265. def OAI.SnakyPrototype.Certificate21.height_71 line 524
  266. def OAI.SnakyPrototype.Certificate21.childrenH_71 line 525
  267. theorem OAI.SnakyPrototype.Certificate21.height_exact_71 line 526
  268. theorem OAI.SnakyPrototype.Certificate21.required_origin_71 line 527
  269. theorem OAI.SnakyPrototype.Certificate21.required_exact_71 line 529
  270. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_71 line 533
  271. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_71 line 535
  272. def OAI.SnakyPrototype.Certificate21.checked_71 line 539
  273. def OAI.SnakyPrototype.Certificate21.height_72 line 547
  274. def OAI.SnakyPrototype.Certificate21.childrenH_72 line 548
  275. theorem OAI.SnakyPrototype.Certificate21.height_exact_72 line 549
  276. theorem OAI.SnakyPrototype.Certificate21.required_origin_72 line 550
  277. theorem OAI.SnakyPrototype.Certificate21.required_exact_72 line 552
  278. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_72 line 556
  279. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_72 line 558
  280. def OAI.SnakyPrototype.Certificate21.checked_72 line 562
  281. def OAI.SnakyPrototype.Certificate21.height_81 line 570
  282. def OAI.SnakyPrototype.Certificate21.childrenH_81 line 571
  283. theorem OAI.SnakyPrototype.Certificate21.height_exact_81 line 572
  284. theorem OAI.SnakyPrototype.Certificate21.required_origin_81 line 573
  285. theorem OAI.SnakyPrototype.Certificate21.required_exact_81 line 575
  286. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_81 line 579
  287. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_81 line 581
  288. def OAI.SnakyPrototype.Certificate21.checked_81 line 585
  289. def OAI.SnakyPrototype.Certificate21.height_84 line 593
  290. def OAI.SnakyPrototype.Certificate21.childrenH_84 line 594
  291. theorem OAI.SnakyPrototype.Certificate21.height_exact_84 line 595
  292. theorem OAI.SnakyPrototype.Certificate21.required_origin_84 line 596
  293. theorem OAI.SnakyPrototype.Certificate21.required_exact_84 line 598
  294. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_84 line 602
  295. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_84 line 604
  296. def OAI.SnakyPrototype.Certificate21.checked_84 line 608
  297. def OAI.SnakyPrototype.Certificate21.height_100 line 616
  298. def OAI.SnakyPrototype.Certificate21.childrenH_100 line 617
  299. theorem OAI.SnakyPrototype.Certificate21.height_exact_100 line 618
  300. theorem OAI.SnakyPrototype.Certificate21.required_origin_100 line 619
  301. theorem OAI.SnakyPrototype.Certificate21.required_exact_100 line 621
  302. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_100 line 625
  303. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_100 line 627
  304. def OAI.SnakyPrototype.Certificate21.checked_100 line 631
  305. def OAI.SnakyPrototype.Certificate21.height_104 line 639
  306. def OAI.SnakyPrototype.Certificate21.childrenH_104 line 640
  307. theorem OAI.SnakyPrototype.Certificate21.height_exact_104 line 641
  308. theorem OAI.SnakyPrototype.Certificate21.required_origin_104 line 642
  309. theorem OAI.SnakyPrototype.Certificate21.required_exact_104 line 644
  310. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_104 line 648
  311. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_104 line 650
  312. def OAI.SnakyPrototype.Certificate21.checked_104 line 654
  313. def OAI.SnakyPrototype.Certificate21.height_107 line 662
  314. def OAI.SnakyPrototype.Certificate21.childrenH_107 line 663
  315. theorem OAI.SnakyPrototype.Certificate21.height_exact_107 line 664
  316. theorem OAI.SnakyPrototype.Certificate21.required_origin_107 line 665
  317. theorem OAI.SnakyPrototype.Certificate21.required_exact_107 line 667
  318. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_107 line 671
  319. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_107 line 673
  320. def OAI.SnakyPrototype.Certificate21.checked_107 line 677
  321. def OAI.SnakyPrototype.Certificate21.height_111 line 685
  322. def OAI.SnakyPrototype.Certificate21.childrenH_111 line 686
  323. theorem OAI.SnakyPrototype.Certificate21.height_exact_111 line 687
  324. theorem OAI.SnakyPrototype.Certificate21.required_origin_111 line 688
  325. theorem OAI.SnakyPrototype.Certificate21.required_exact_111 line 690
  326. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_111 line 694
  327. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_111 line 696
  328. def OAI.SnakyPrototype.Certificate21.checked_111 line 700
  329. def OAI.SnakyPrototype.Certificate21.height_114 line 708
  330. def OAI.SnakyPrototype.Certificate21.childrenH_114 line 709
  331. theorem OAI.SnakyPrototype.Certificate21.height_exact_114 line 710
  332. theorem OAI.SnakyPrototype.Certificate21.required_origin_114 line 711
  333. theorem OAI.SnakyPrototype.Certificate21.required_exact_114 line 713
  334. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_114 line 717
  335. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_114 line 719
  336. def OAI.SnakyPrototype.Certificate21.checked_114 line 723
  337. def OAI.SnakyPrototype.Certificate21.height_122 line 731
  338. def OAI.SnakyPrototype.Certificate21.childrenH_122 line 732
  339. theorem OAI.SnakyPrototype.Certificate21.height_exact_122 line 733
  340. theorem OAI.SnakyPrototype.Certificate21.required_origin_122 line 734
  341. theorem OAI.SnakyPrototype.Certificate21.required_exact_122 line 736
  342. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_122 line 740
  343. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_122 line 742
  344. def OAI.SnakyPrototype.Certificate21.checked_122 line 746
  345. def OAI.SnakyPrototype.Certificate21.height_133 line 754
  346. def OAI.SnakyPrototype.Certificate21.childrenH_133 line 755
  347. theorem OAI.SnakyPrototype.Certificate21.height_exact_133 line 756
  348. theorem OAI.SnakyPrototype.Certificate21.required_origin_133 line 757
  349. theorem OAI.SnakyPrototype.Certificate21.required_exact_133 line 759
  350. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_133 line 763
  351. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_133 line 765
  352. def OAI.SnakyPrototype.Certificate21.checked_133 line 769
  353. def OAI.SnakyPrototype.Certificate21.height_142 line 777
  354. def OAI.SnakyPrototype.Certificate21.childrenH_142 line 778
  355. theorem OAI.SnakyPrototype.Certificate21.height_exact_142 line 779
  356. theorem OAI.SnakyPrototype.Certificate21.required_origin_142 line 780
  357. theorem OAI.SnakyPrototype.Certificate21.required_exact_142 line 782
  358. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_142 line 786
  359. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_142 line 788
  360. def OAI.SnakyPrototype.Certificate21.checked_142 line 792
  361. def OAI.SnakyPrototype.Certificate21.height_144 line 800
  362. def OAI.SnakyPrototype.Certificate21.childrenH_144 line 801
  363. theorem OAI.SnakyPrototype.Certificate21.height_exact_144 line 802
  364. theorem OAI.SnakyPrototype.Certificate21.required_origin_144 line 803
  365. theorem OAI.SnakyPrototype.Certificate21.required_exact_144 line 805
  366. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_144 line 809
  367. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_144 line 811
  368. def OAI.SnakyPrototype.Certificate21.checked_144 line 815
  369. def OAI.SnakyPrototype.Certificate21.height_145 line 823
  370. def OAI.SnakyPrototype.Certificate21.childrenH_145 line 824
  371. theorem OAI.SnakyPrototype.Certificate21.height_exact_145 line 825
  372. theorem OAI.SnakyPrototype.Certificate21.required_origin_145 line 826
  373. theorem OAI.SnakyPrototype.Certificate21.required_exact_145 line 828
  374. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_145 line 832
  375. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_145 line 834
  376. def OAI.SnakyPrototype.Certificate21.checked_145 line 838
  377. def OAI.SnakyPrototype.Certificate21.height_147 line 846
  378. def OAI.SnakyPrototype.Certificate21.childrenH_147 line 847
  379. theorem OAI.SnakyPrototype.Certificate21.height_exact_147 line 848
  380. theorem OAI.SnakyPrototype.Certificate21.required_origin_147 line 849
  381. theorem OAI.SnakyPrototype.Certificate21.required_exact_147 line 851
  382. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_147 line 855
  383. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_147 line 857
  384. def OAI.SnakyPrototype.Certificate21.checked_147 line 861
  385. def OAI.SnakyPrototype.Certificate21.height_152 line 869
  386. def OAI.SnakyPrototype.Certificate21.childrenH_152 line 870
  387. theorem OAI.SnakyPrototype.Certificate21.height_exact_152 line 871
  388. theorem OAI.SnakyPrototype.Certificate21.required_origin_152 line 872
  389. theorem OAI.SnakyPrototype.Certificate21.required_exact_152 line 874
  390. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_152 line 878
  391. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_152 line 880
  392. def OAI.SnakyPrototype.Certificate21.checked_152 line 884
  393. def OAI.SnakyPrototype.Certificate21.height_155 line 892
  394. def OAI.SnakyPrototype.Certificate21.childrenH_155 line 893
  395. theorem OAI.SnakyPrototype.Certificate21.height_exact_155 line 894
  396. theorem OAI.SnakyPrototype.Certificate21.required_origin_155 line 895
  397. theorem OAI.SnakyPrototype.Certificate21.required_exact_155 line 897
  398. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_155 line 901
  399. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_155 line 903
  400. def OAI.SnakyPrototype.Certificate21.checked_155 line 907
  401. def OAI.SnakyPrototype.Certificate21.height_164 line 915
  402. def OAI.SnakyPrototype.Certificate21.childrenH_164 line 916
  403. theorem OAI.SnakyPrototype.Certificate21.height_exact_164 line 917
  404. theorem OAI.SnakyPrototype.Certificate21.required_origin_164 line 918
  405. theorem OAI.SnakyPrototype.Certificate21.required_exact_164 line 920
  406. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_164 line 924
  407. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_164 line 926
  408. def OAI.SnakyPrototype.Certificate21.checked_164 line 930
  409. def OAI.SnakyPrototype.Certificate21.height_175 line 938
  410. def OAI.SnakyPrototype.Certificate21.childrenH_175 line 939
  411. theorem OAI.SnakyPrototype.Certificate21.height_exact_175 line 940
  412. theorem OAI.SnakyPrototype.Certificate21.required_origin_175 line 941
  413. theorem OAI.SnakyPrototype.Certificate21.required_exact_175 line 943
  414. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_175 line 947
  415. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_175 line 949
  416. def OAI.SnakyPrototype.Certificate21.checked_175 line 953
  417. def OAI.SnakyPrototype.Certificate21.height_176 line 961
  418. def OAI.SnakyPrototype.Certificate21.childrenH_176 line 962
  419. theorem OAI.SnakyPrototype.Certificate21.height_exact_176 line 963
  420. theorem OAI.SnakyPrototype.Certificate21.required_origin_176 line 964
  421. theorem OAI.SnakyPrototype.Certificate21.required_exact_176 line 966
  422. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_176 line 970
  423. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_176 line 972
  424. def OAI.SnakyPrototype.Certificate21.checked_176 line 976
  425. def OAI.SnakyPrototype.Certificate21.height_179 line 984
  426. def OAI.SnakyPrototype.Certificate21.childrenH_179 line 985
  427. theorem OAI.SnakyPrototype.Certificate21.height_exact_179 line 986
  428. theorem OAI.SnakyPrototype.Certificate21.required_origin_179 line 987
  429. theorem OAI.SnakyPrototype.Certificate21.required_exact_179 line 989
  430. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_179 line 993
  431. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_179 line 995
  432. def OAI.SnakyPrototype.Certificate21.checked_179 line 999