OAI/GameTheory/SnakyTwentyOne/Cards/Height06Part01.lean

GitHub source file

414 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_85 line 15
  2. def OAI.SnakyPrototype.Certificate21.envelope_85 line 16
  3. def OAI.SnakyPrototype.Certificate21.childrenC_85 line 17
  4. def OAI.SnakyPrototype.Certificate21.childrenD_85 line 18
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_85 line 19
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_85 line 20
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_85 line 21
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_85 line 22
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_85 line 23
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_85 line 29
  11. def OAI.SnakyPrototype.Certificate21.required_95 line 34
  12. def OAI.SnakyPrototype.Certificate21.envelope_95 line 35
  13. def OAI.SnakyPrototype.Certificate21.childrenC_95 line 36
  14. def OAI.SnakyPrototype.Certificate21.childrenD_95 line 37
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_95 line 38
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_95 line 39
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_95 line 40
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_95 line 41
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_95 line 42
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_95 line 49
  21. def OAI.SnakyPrototype.Certificate21.required_110 line 54
  22. def OAI.SnakyPrototype.Certificate21.envelope_110 line 55
  23. def OAI.SnakyPrototype.Certificate21.childrenC_110 line 56
  24. def OAI.SnakyPrototype.Certificate21.childrenD_110 line 57
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_110 line 58
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_110 line 59
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_110 line 60
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_110 line 61
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_110 line 62
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_110 line 69
  31. def OAI.SnakyPrototype.Certificate21.required_115 line 74
  32. def OAI.SnakyPrototype.Certificate21.envelope_115 line 75
  33. def OAI.SnakyPrototype.Certificate21.childrenC_115 line 76
  34. def OAI.SnakyPrototype.Certificate21.childrenD_115 line 77
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_115 line 78
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_115 line 79
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_115 line 80
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_115 line 81
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_115 line 82
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_115 line 87
  41. def OAI.SnakyPrototype.Certificate21.required_119 line 92
  42. def OAI.SnakyPrototype.Certificate21.envelope_119 line 93
  43. def OAI.SnakyPrototype.Certificate21.childrenC_119 line 94
  44. def OAI.SnakyPrototype.Certificate21.childrenD_119 line 95
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_119 line 96
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_119 line 97
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_119 line 98
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_119 line 99
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_119 line 100
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_119 line 105
  51. def OAI.SnakyPrototype.Certificate21.required_134 line 110
  52. def OAI.SnakyPrototype.Certificate21.envelope_134 line 111
  53. def OAI.SnakyPrototype.Certificate21.childrenC_134 line 112
  54. def OAI.SnakyPrototype.Certificate21.childrenD_134 line 113
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_134 line 114
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_134 line 115
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_134 line 116
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_134 line 117
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_134 line 118
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_134 line 124
  61. def OAI.SnakyPrototype.Certificate21.required_135 line 129
  62. def OAI.SnakyPrototype.Certificate21.envelope_135 line 130
  63. def OAI.SnakyPrototype.Certificate21.childrenC_135 line 131
  64. def OAI.SnakyPrototype.Certificate21.childrenD_135 line 132
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_135 line 133
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_135 line 134
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_135 line 135
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_135 line 136
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_135 line 137
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_135 line 143
  71. def OAI.SnakyPrototype.Certificate21.required_136 line 148
  72. def OAI.SnakyPrototype.Certificate21.envelope_136 line 149
  73. def OAI.SnakyPrototype.Certificate21.childrenC_136 line 150
  74. def OAI.SnakyPrototype.Certificate21.childrenD_136 line 151
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_136 line 152
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_136 line 153
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_136 line 154
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_136 line 155
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_136 line 156
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_136 line 162
  81. def OAI.SnakyPrototype.Certificate21.required_137 line 167
  82. def OAI.SnakyPrototype.Certificate21.envelope_137 line 168
  83. def OAI.SnakyPrototype.Certificate21.childrenC_137 line 169
  84. def OAI.SnakyPrototype.Certificate21.childrenD_137 line 170
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_137 line 171
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_137 line 172
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_137 line 173
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_137 line 174
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_137 line 175
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_137 line 181
  91. def OAI.SnakyPrototype.Certificate21.required_161 line 186
  92. def OAI.SnakyPrototype.Certificate21.envelope_161 line 187
  93. def OAI.SnakyPrototype.Certificate21.childrenC_161 line 188
  94. def OAI.SnakyPrototype.Certificate21.childrenD_161 line 189
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_161 line 190
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_161 line 191
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_161 line 192
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_161 line 193
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_161 line 194
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_161 line 199
  101. def OAI.SnakyPrototype.Certificate21.required_162 line 204
  102. def OAI.SnakyPrototype.Certificate21.envelope_162 line 205
  103. def OAI.SnakyPrototype.Certificate21.childrenC_162 line 206
  104. def OAI.SnakyPrototype.Certificate21.childrenD_162 line 207
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_162 line 208
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_162 line 209
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_162 line 210
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_162 line 211
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_162 line 212
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_162 line 217
  111. def OAI.SnakyPrototype.Certificate21.required_166 line 222
  112. def OAI.SnakyPrototype.Certificate21.envelope_166 line 223
  113. def OAI.SnakyPrototype.Certificate21.childrenC_166 line 224
  114. def OAI.SnakyPrototype.Certificate21.childrenD_166 line 225
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_166 line 226
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_166 line 227
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_166 line 228
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_166 line 229
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_166 line 230
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_166 line 237
  121. def OAI.SnakyPrototype.Certificate21.required_167 line 242
  122. def OAI.SnakyPrototype.Certificate21.envelope_167 line 243
  123. def OAI.SnakyPrototype.Certificate21.childrenC_167 line 244
  124. def OAI.SnakyPrototype.Certificate21.childrenD_167 line 245
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_167 line 246
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_167 line 247
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_167 line 248
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_167 line 249
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_167 line 250
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_167 line 255
  131. def OAI.SnakyPrototype.Certificate21.required_172 line 260
  132. def OAI.SnakyPrototype.Certificate21.envelope_172 line 261
  133. def OAI.SnakyPrototype.Certificate21.childrenC_172 line 262
  134. def OAI.SnakyPrototype.Certificate21.childrenD_172 line 263
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_172 line 264
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_172 line 265
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_172 line 266
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_172 line 267
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_172 line 268
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_172 line 273
  141. def OAI.SnakyPrototype.Certificate21.required_173 line 278
  142. def OAI.SnakyPrototype.Certificate21.envelope_173 line 279
  143. def OAI.SnakyPrototype.Certificate21.childrenC_173 line 280
  144. def OAI.SnakyPrototype.Certificate21.childrenD_173 line 281
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_173 line 282
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_173 line 283
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_173 line 284
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_173 line 285
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_173 line 286
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_173 line 291
  151. def OAI.SnakyPrototype.Certificate21.required_180 line 296
  152. def OAI.SnakyPrototype.Certificate21.envelope_180 line 297
  153. def OAI.SnakyPrototype.Certificate21.childrenC_180 line 298
  154. def OAI.SnakyPrototype.Certificate21.childrenD_180 line 299
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_180 line 300
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_180 line 301
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_180 line 302
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_180 line 303
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_180 line 304
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_180 line 310
  161. def OAI.SnakyPrototype.Certificate21.required_181 line 315
  162. def OAI.SnakyPrototype.Certificate21.envelope_181 line 316
  163. def OAI.SnakyPrototype.Certificate21.childrenC_181 line 317
  164. def OAI.SnakyPrototype.Certificate21.childrenD_181 line 318
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_181 line 319
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_181 line 320
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_181 line 321
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_181 line 322
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_181 line 323
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_181 line 329
  171. def OAI.SnakyPrototype.Certificate21.required_182 line 334
  172. def OAI.SnakyPrototype.Certificate21.envelope_182 line 335
  173. def OAI.SnakyPrototype.Certificate21.childrenC_182 line 336
  174. def OAI.SnakyPrototype.Certificate21.childrenD_182 line 337
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_182 line 338
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_182 line 339
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_182 line 340
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_182 line 341
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_182 line 342
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_182 line 348
  181. def OAI.SnakyPrototype.Certificate21.required_184 line 353
  182. def OAI.SnakyPrototype.Certificate21.envelope_184 line 354
  183. def OAI.SnakyPrototype.Certificate21.childrenC_184 line 355
  184. def OAI.SnakyPrototype.Certificate21.childrenD_184 line 356
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_184 line 357
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_184 line 358
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_184 line 359
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_184 line 360
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_184 line 361
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_184 line 366
  191. def OAI.SnakyPrototype.Certificate21.required_188 line 371
  192. def OAI.SnakyPrototype.Certificate21.envelope_188 line 372
  193. def OAI.SnakyPrototype.Certificate21.childrenC_188 line 373
  194. def OAI.SnakyPrototype.Certificate21.childrenD_188 line 374
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_188 line 375
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_188 line 376
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_188 line 377
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_188 line 378
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_188 line 379
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_188 line 387
  201. def OAI.SnakyPrototype.Certificate21.required_189 line 392
  202. def OAI.SnakyPrototype.Certificate21.envelope_189 line 393
  203. def OAI.SnakyPrototype.Certificate21.childrenC_189 line 394
  204. def OAI.SnakyPrototype.Certificate21.childrenD_189 line 395
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_189 line 396
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_189 line 397
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_189 line 398
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_189 line 399
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_189 line 400
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_189 line 408
  211. def OAI.SnakyPrototype.Certificate21.required_190 line 413
  212. def OAI.SnakyPrototype.Certificate21.envelope_190 line 414
  213. def OAI.SnakyPrototype.Certificate21.childrenC_190 line 415
  214. def OAI.SnakyPrototype.Certificate21.childrenD_190 line 416
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_190 line 417
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_190 line 418
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_190 line 419
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_190 line 420
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_190 line 421
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_190 line 429
  221. def OAI.SnakyPrototype.Certificate21.required_192 line 434
  222. def OAI.SnakyPrototype.Certificate21.envelope_192 line 435
  223. def OAI.SnakyPrototype.Certificate21.childrenC_192 line 436
  224. def OAI.SnakyPrototype.Certificate21.childrenD_192 line 437
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_192 line 438
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_192 line 439
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_192 line 440
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_192 line 441
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_192 line 442
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_192 line 450
  231. def OAI.SnakyPrototype.Certificate21.height_85 line 455
  232. def OAI.SnakyPrototype.Certificate21.childrenH_85 line 456
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_85 line 457
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_85 line 458
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_85 line 460
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_85 line 464
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_85 line 466
  238. def OAI.SnakyPrototype.Certificate21.checked_85 line 470
  239. def OAI.SnakyPrototype.Certificate21.height_95 line 478
  240. def OAI.SnakyPrototype.Certificate21.childrenH_95 line 479
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_95 line 480
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_95 line 481
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_95 line 483
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_95 line 487
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_95 line 489
  246. def OAI.SnakyPrototype.Certificate21.checked_95 line 493
  247. def OAI.SnakyPrototype.Certificate21.height_110 line 501
  248. def OAI.SnakyPrototype.Certificate21.childrenH_110 line 502
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_110 line 503
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_110 line 504
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_110 line 506
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_110 line 510
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_110 line 512
  254. def OAI.SnakyPrototype.Certificate21.checked_110 line 516
  255. def OAI.SnakyPrototype.Certificate21.height_115 line 524
  256. def OAI.SnakyPrototype.Certificate21.childrenH_115 line 525
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_115 line 526
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_115 line 527
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_115 line 529
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_115 line 533
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_115 line 535
  262. def OAI.SnakyPrototype.Certificate21.checked_115 line 539
  263. def OAI.SnakyPrototype.Certificate21.height_119 line 547
  264. def OAI.SnakyPrototype.Certificate21.childrenH_119 line 548
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_119 line 549
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_119 line 550
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_119 line 552
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_119 line 556
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_119 line 558
  270. def OAI.SnakyPrototype.Certificate21.checked_119 line 562
  271. def OAI.SnakyPrototype.Certificate21.height_134 line 570
  272. def OAI.SnakyPrototype.Certificate21.childrenH_134 line 571
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_134 line 572
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_134 line 573
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_134 line 575
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_134 line 579
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_134 line 581
  278. def OAI.SnakyPrototype.Certificate21.checked_134 line 585
  279. def OAI.SnakyPrototype.Certificate21.height_135 line 593
  280. def OAI.SnakyPrototype.Certificate21.childrenH_135 line 594
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_135 line 595
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_135 line 596
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_135 line 598
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_135 line 602
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_135 line 604
  286. def OAI.SnakyPrototype.Certificate21.checked_135 line 608
  287. def OAI.SnakyPrototype.Certificate21.height_136 line 616
  288. def OAI.SnakyPrototype.Certificate21.childrenH_136 line 617
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_136 line 618
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_136 line 619
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_136 line 621
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_136 line 625
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_136 line 627
  294. def OAI.SnakyPrototype.Certificate21.checked_136 line 631
  295. def OAI.SnakyPrototype.Certificate21.height_137 line 639
  296. def OAI.SnakyPrototype.Certificate21.childrenH_137 line 640
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_137 line 641
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_137 line 642
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_137 line 644
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_137 line 648
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_137 line 650
  302. def OAI.SnakyPrototype.Certificate21.checked_137 line 654
  303. def OAI.SnakyPrototype.Certificate21.height_161 line 662
  304. def OAI.SnakyPrototype.Certificate21.childrenH_161 line 663
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_161 line 664
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_161 line 665
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_161 line 667
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_161 line 671
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_161 line 673
  310. def OAI.SnakyPrototype.Certificate21.checked_161 line 677
  311. def OAI.SnakyPrototype.Certificate21.height_162 line 685
  312. def OAI.SnakyPrototype.Certificate21.childrenH_162 line 686
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_162 line 687
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_162 line 688
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_162 line 690
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_162 line 694
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_162 line 696
  318. def OAI.SnakyPrototype.Certificate21.checked_162 line 700
  319. def OAI.SnakyPrototype.Certificate21.height_166 line 708
  320. def OAI.SnakyPrototype.Certificate21.childrenH_166 line 709
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_166 line 710
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_166 line 711
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_166 line 713
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_166 line 717
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_166 line 719
  326. def OAI.SnakyPrototype.Certificate21.checked_166 line 723
  327. def OAI.SnakyPrototype.Certificate21.height_167 line 731
  328. def OAI.SnakyPrototype.Certificate21.childrenH_167 line 732
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_167 line 733
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_167 line 734
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_167 line 736
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_167 line 740
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_167 line 742
  334. def OAI.SnakyPrototype.Certificate21.checked_167 line 746
  335. def OAI.SnakyPrototype.Certificate21.height_172 line 754
  336. def OAI.SnakyPrototype.Certificate21.childrenH_172 line 755
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_172 line 756
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_172 line 757
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_172 line 759
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_172 line 763
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_172 line 765
  342. def OAI.SnakyPrototype.Certificate21.checked_172 line 769
  343. def OAI.SnakyPrototype.Certificate21.height_173 line 777
  344. def OAI.SnakyPrototype.Certificate21.childrenH_173 line 778
  345. theorem OAI.SnakyPrototype.Certificate21.height_exact_173 line 779
  346. theorem OAI.SnakyPrototype.Certificate21.required_origin_173 line 780
  347. theorem OAI.SnakyPrototype.Certificate21.required_exact_173 line 782
  348. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_173 line 786
  349. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_173 line 788
  350. def OAI.SnakyPrototype.Certificate21.checked_173 line 792
  351. def OAI.SnakyPrototype.Certificate21.height_180 line 800
  352. def OAI.SnakyPrototype.Certificate21.childrenH_180 line 801
  353. theorem OAI.SnakyPrototype.Certificate21.height_exact_180 line 802
  354. theorem OAI.SnakyPrototype.Certificate21.required_origin_180 line 803
  355. theorem OAI.SnakyPrototype.Certificate21.required_exact_180 line 805
  356. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_180 line 809
  357. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_180 line 811
  358. def OAI.SnakyPrototype.Certificate21.checked_180 line 815
  359. def OAI.SnakyPrototype.Certificate21.height_181 line 823
  360. def OAI.SnakyPrototype.Certificate21.childrenH_181 line 824
  361. theorem OAI.SnakyPrototype.Certificate21.height_exact_181 line 825
  362. theorem OAI.SnakyPrototype.Certificate21.required_origin_181 line 826
  363. theorem OAI.SnakyPrototype.Certificate21.required_exact_181 line 828
  364. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_181 line 832
  365. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_181 line 834
  366. def OAI.SnakyPrototype.Certificate21.checked_181 line 838
  367. def OAI.SnakyPrototype.Certificate21.height_182 line 846
  368. def OAI.SnakyPrototype.Certificate21.childrenH_182 line 847
  369. theorem OAI.SnakyPrototype.Certificate21.height_exact_182 line 848
  370. theorem OAI.SnakyPrototype.Certificate21.required_origin_182 line 849
  371. theorem OAI.SnakyPrototype.Certificate21.required_exact_182 line 851
  372. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_182 line 855
  373. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_182 line 857
  374. def OAI.SnakyPrototype.Certificate21.checked_182 line 861
  375. def OAI.SnakyPrototype.Certificate21.height_184 line 869
  376. def OAI.SnakyPrototype.Certificate21.childrenH_184 line 870
  377. theorem OAI.SnakyPrototype.Certificate21.height_exact_184 line 871
  378. theorem OAI.SnakyPrototype.Certificate21.required_origin_184 line 872
  379. theorem OAI.SnakyPrototype.Certificate21.required_exact_184 line 874
  380. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_184 line 878
  381. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_184 line 880
  382. def OAI.SnakyPrototype.Certificate21.checked_184 line 884
  383. def OAI.SnakyPrototype.Certificate21.height_188 line 892
  384. def OAI.SnakyPrototype.Certificate21.childrenH_188 line 893
  385. theorem OAI.SnakyPrototype.Certificate21.height_exact_188 line 894
  386. theorem OAI.SnakyPrototype.Certificate21.required_origin_188 line 895
  387. theorem OAI.SnakyPrototype.Certificate21.required_exact_188 line 897
  388. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_188 line 901
  389. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_188 line 903
  390. def OAI.SnakyPrototype.Certificate21.checked_188 line 907
  391. def OAI.SnakyPrototype.Certificate21.height_189 line 915
  392. def OAI.SnakyPrototype.Certificate21.childrenH_189 line 916
  393. theorem OAI.SnakyPrototype.Certificate21.height_exact_189 line 917
  394. theorem OAI.SnakyPrototype.Certificate21.required_origin_189 line 918
  395. theorem OAI.SnakyPrototype.Certificate21.required_exact_189 line 920
  396. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_189 line 924
  397. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_189 line 926
  398. def OAI.SnakyPrototype.Certificate21.checked_189 line 930
  399. def OAI.SnakyPrototype.Certificate21.height_190 line 938
  400. def OAI.SnakyPrototype.Certificate21.childrenH_190 line 939
  401. theorem OAI.SnakyPrototype.Certificate21.height_exact_190 line 940
  402. theorem OAI.SnakyPrototype.Certificate21.required_origin_190 line 941
  403. theorem OAI.SnakyPrototype.Certificate21.required_exact_190 line 943
  404. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_190 line 947
  405. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_190 line 949
  406. def OAI.SnakyPrototype.Certificate21.checked_190 line 953
  407. def OAI.SnakyPrototype.Certificate21.height_192 line 961
  408. def OAI.SnakyPrototype.Certificate21.childrenH_192 line 962
  409. theorem OAI.SnakyPrototype.Certificate21.height_exact_192 line 963
  410. theorem OAI.SnakyPrototype.Certificate21.required_origin_192 line 964
  411. theorem OAI.SnakyPrototype.Certificate21.required_exact_192 line 966
  412. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_192 line 970
  413. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_192 line 972
  414. def OAI.SnakyPrototype.Certificate21.checked_192 line 976