OAI/GameTheory/SnakyTwentyOne/Cards/Height07Part01.lean

GitHub source file

414 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_116 line 20
  2. def OAI.SnakyPrototype.Certificate21.envelope_116 line 21
  3. def OAI.SnakyPrototype.Certificate21.childrenC_116 line 22
  4. def OAI.SnakyPrototype.Certificate21.childrenD_116 line 23
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_116 line 24
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_116 line 25
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_116 line 26
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_116 line 27
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_116 line 28
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_116 line 34
  11. def OAI.SnakyPrototype.Certificate21.required_117 line 39
  12. def OAI.SnakyPrototype.Certificate21.envelope_117 line 40
  13. def OAI.SnakyPrototype.Certificate21.childrenC_117 line 41
  14. def OAI.SnakyPrototype.Certificate21.childrenD_117 line 42
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_117 line 43
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_117 line 44
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_117 line 45
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_117 line 46
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_117 line 47
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_117 line 53
  21. def OAI.SnakyPrototype.Certificate21.required_118 line 58
  22. def OAI.SnakyPrototype.Certificate21.envelope_118 line 59
  23. def OAI.SnakyPrototype.Certificate21.childrenC_118 line 60
  24. def OAI.SnakyPrototype.Certificate21.childrenD_118 line 61
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_118 line 62
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_118 line 63
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_118 line 64
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_118 line 65
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_118 line 66
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_118 line 72
  31. def OAI.SnakyPrototype.Certificate21.required_204 line 77
  32. def OAI.SnakyPrototype.Certificate21.envelope_204 line 78
  33. def OAI.SnakyPrototype.Certificate21.childrenC_204 line 79
  34. def OAI.SnakyPrototype.Certificate21.childrenD_204 line 80
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_204 line 81
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_204 line 82
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_204 line 83
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_204 line 84
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_204 line 85
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_204 line 90
  41. def OAI.SnakyPrototype.Certificate21.required_256 line 95
  42. def OAI.SnakyPrototype.Certificate21.envelope_256 line 96
  43. def OAI.SnakyPrototype.Certificate21.childrenC_256 line 97
  44. def OAI.SnakyPrototype.Certificate21.childrenD_256 line 98
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_256 line 99
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_256 line 100
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_256 line 101
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_256 line 102
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_256 line 103
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_256 line 108
  51. def OAI.SnakyPrototype.Certificate21.required_276 line 113
  52. def OAI.SnakyPrototype.Certificate21.envelope_276 line 114
  53. def OAI.SnakyPrototype.Certificate21.childrenC_276 line 115
  54. def OAI.SnakyPrototype.Certificate21.childrenD_276 line 116
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_276 line 117
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_276 line 118
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_276 line 119
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_276 line 120
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_276 line 121
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_276 line 128
  61. def OAI.SnakyPrototype.Certificate21.required_286 line 133
  62. def OAI.SnakyPrototype.Certificate21.envelope_286 line 134
  63. def OAI.SnakyPrototype.Certificate21.childrenC_286 line 135
  64. def OAI.SnakyPrototype.Certificate21.childrenD_286 line 136
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_286 line 137
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_286 line 138
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_286 line 139
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_286 line 140
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_286 line 141
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_286 line 146
  71. def OAI.SnakyPrototype.Certificate21.required_290 line 151
  72. def OAI.SnakyPrototype.Certificate21.envelope_290 line 152
  73. def OAI.SnakyPrototype.Certificate21.childrenC_290 line 153
  74. def OAI.SnakyPrototype.Certificate21.childrenD_290 line 154
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_290 line 155
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_290 line 156
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_290 line 157
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_290 line 158
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_290 line 159
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_290 line 164
  81. def OAI.SnakyPrototype.Certificate21.required_295 line 169
  82. def OAI.SnakyPrototype.Certificate21.envelope_295 line 170
  83. def OAI.SnakyPrototype.Certificate21.childrenC_295 line 171
  84. def OAI.SnakyPrototype.Certificate21.childrenD_295 line 172
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_295 line 173
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_295 line 174
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_295 line 175
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_295 line 176
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_295 line 177
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_295 line 182
  91. def OAI.SnakyPrototype.Certificate21.required_297 line 187
  92. def OAI.SnakyPrototype.Certificate21.envelope_297 line 188
  93. def OAI.SnakyPrototype.Certificate21.childrenC_297 line 189
  94. def OAI.SnakyPrototype.Certificate21.childrenD_297 line 190
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_297 line 191
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_297 line 192
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_297 line 193
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_297 line 194
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_297 line 195
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_297 line 201
  101. def OAI.SnakyPrototype.Certificate21.required_298 line 206
  102. def OAI.SnakyPrototype.Certificate21.envelope_298 line 207
  103. def OAI.SnakyPrototype.Certificate21.childrenC_298 line 208
  104. def OAI.SnakyPrototype.Certificate21.childrenD_298 line 209
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_298 line 210
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_298 line 211
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_298 line 212
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_298 line 213
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_298 line 214
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_298 line 220
  111. def OAI.SnakyPrototype.Certificate21.required_309 line 225
  112. def OAI.SnakyPrototype.Certificate21.envelope_309 line 226
  113. def OAI.SnakyPrototype.Certificate21.childrenC_309 line 227
  114. def OAI.SnakyPrototype.Certificate21.childrenD_309 line 228
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_309 line 229
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_309 line 230
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_309 line 231
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_309 line 232
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_309 line 233
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_309 line 239
  121. def OAI.SnakyPrototype.Certificate21.required_317 line 244
  122. def OAI.SnakyPrototype.Certificate21.envelope_317 line 245
  123. def OAI.SnakyPrototype.Certificate21.childrenC_317 line 246
  124. def OAI.SnakyPrototype.Certificate21.childrenD_317 line 247
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_317 line 248
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_317 line 249
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_317 line 250
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_317 line 251
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_317 line 252
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_317 line 258
  131. def OAI.SnakyPrototype.Certificate21.required_318 line 263
  132. def OAI.SnakyPrototype.Certificate21.envelope_318 line 264
  133. def OAI.SnakyPrototype.Certificate21.childrenC_318 line 265
  134. def OAI.SnakyPrototype.Certificate21.childrenD_318 line 266
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_318 line 267
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_318 line 268
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_318 line 269
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_318 line 270
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_318 line 271
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_318 line 278
  141. def OAI.SnakyPrototype.Certificate21.required_320 line 283
  142. def OAI.SnakyPrototype.Certificate21.envelope_320 line 284
  143. def OAI.SnakyPrototype.Certificate21.childrenC_320 line 285
  144. def OAI.SnakyPrototype.Certificate21.childrenD_320 line 286
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_320 line 287
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_320 line 288
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_320 line 289
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_320 line 290
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_320 line 291
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_320 line 296
  151. def OAI.SnakyPrototype.Certificate21.required_324 line 301
  152. def OAI.SnakyPrototype.Certificate21.envelope_324 line 302
  153. def OAI.SnakyPrototype.Certificate21.childrenC_324 line 303
  154. def OAI.SnakyPrototype.Certificate21.childrenD_324 line 304
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_324 line 305
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_324 line 306
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_324 line 307
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_324 line 308
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_324 line 309
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_324 line 316
  161. def OAI.SnakyPrototype.Certificate21.required_329 line 321
  162. def OAI.SnakyPrototype.Certificate21.envelope_329 line 322
  163. def OAI.SnakyPrototype.Certificate21.childrenC_329 line 323
  164. def OAI.SnakyPrototype.Certificate21.childrenD_329 line 324
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_329 line 325
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_329 line 326
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_329 line 327
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_329 line 328
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_329 line 329
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_329 line 336
  171. def OAI.SnakyPrototype.Certificate21.required_332 line 341
  172. def OAI.SnakyPrototype.Certificate21.envelope_332 line 342
  173. def OAI.SnakyPrototype.Certificate21.childrenC_332 line 343
  174. def OAI.SnakyPrototype.Certificate21.childrenD_332 line 344
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_332 line 345
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_332 line 346
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_332 line 347
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_332 line 348
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_332 line 349
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_332 line 355
  181. def OAI.SnakyPrototype.Certificate21.required_337 line 360
  182. def OAI.SnakyPrototype.Certificate21.envelope_337 line 361
  183. def OAI.SnakyPrototype.Certificate21.childrenC_337 line 362
  184. def OAI.SnakyPrototype.Certificate21.childrenD_337 line 363
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_337 line 364
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_337 line 365
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_337 line 366
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_337 line 367
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_337 line 368
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_337 line 374
  191. def OAI.SnakyPrototype.Certificate21.required_339 line 379
  192. def OAI.SnakyPrototype.Certificate21.envelope_339 line 380
  193. def OAI.SnakyPrototype.Certificate21.childrenC_339 line 381
  194. def OAI.SnakyPrototype.Certificate21.childrenD_339 line 382
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_339 line 383
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_339 line 384
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_339 line 385
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_339 line 386
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_339 line 387
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_339 line 392
  201. def OAI.SnakyPrototype.Certificate21.required_341 line 397
  202. def OAI.SnakyPrototype.Certificate21.envelope_341 line 398
  203. def OAI.SnakyPrototype.Certificate21.childrenC_341 line 399
  204. def OAI.SnakyPrototype.Certificate21.childrenD_341 line 400
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_341 line 401
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_341 line 402
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_341 line 403
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_341 line 404
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_341 line 405
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_341 line 411
  211. def OAI.SnakyPrototype.Certificate21.required_344 line 416
  212. def OAI.SnakyPrototype.Certificate21.envelope_344 line 417
  213. def OAI.SnakyPrototype.Certificate21.childrenC_344 line 418
  214. def OAI.SnakyPrototype.Certificate21.childrenD_344 line 419
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_344 line 420
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_344 line 421
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_344 line 422
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_344 line 423
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_344 line 424
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_344 line 429
  221. def OAI.SnakyPrototype.Certificate21.required_353 line 434
  222. def OAI.SnakyPrototype.Certificate21.envelope_353 line 435
  223. def OAI.SnakyPrototype.Certificate21.childrenC_353 line 436
  224. def OAI.SnakyPrototype.Certificate21.childrenD_353 line 437
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_353 line 438
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_353 line 439
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_353 line 440
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_353 line 441
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_353 line 442
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_353 line 447
  231. def OAI.SnakyPrototype.Certificate21.height_116 line 452
  232. def OAI.SnakyPrototype.Certificate21.childrenH_116 line 453
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_116 line 454
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_116 line 455
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_116 line 457
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_116 line 461
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_116 line 463
  238. def OAI.SnakyPrototype.Certificate21.checked_116 line 467
  239. def OAI.SnakyPrototype.Certificate21.height_117 line 475
  240. def OAI.SnakyPrototype.Certificate21.childrenH_117 line 476
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_117 line 477
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_117 line 478
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_117 line 480
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_117 line 484
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_117 line 486
  246. def OAI.SnakyPrototype.Certificate21.checked_117 line 490
  247. def OAI.SnakyPrototype.Certificate21.height_118 line 498
  248. def OAI.SnakyPrototype.Certificate21.childrenH_118 line 499
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_118 line 500
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_118 line 501
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_118 line 503
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_118 line 507
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_118 line 509
  254. def OAI.SnakyPrototype.Certificate21.checked_118 line 513
  255. def OAI.SnakyPrototype.Certificate21.height_204 line 521
  256. def OAI.SnakyPrototype.Certificate21.childrenH_204 line 522
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_204 line 523
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_204 line 524
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_204 line 526
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_204 line 530
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_204 line 532
  262. def OAI.SnakyPrototype.Certificate21.checked_204 line 536
  263. def OAI.SnakyPrototype.Certificate21.height_256 line 544
  264. def OAI.SnakyPrototype.Certificate21.childrenH_256 line 545
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_256 line 546
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_256 line 547
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_256 line 549
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_256 line 553
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_256 line 555
  270. def OAI.SnakyPrototype.Certificate21.checked_256 line 559
  271. def OAI.SnakyPrototype.Certificate21.height_276 line 567
  272. def OAI.SnakyPrototype.Certificate21.childrenH_276 line 568
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_276 line 569
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_276 line 570
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_276 line 572
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_276 line 576
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_276 line 578
  278. def OAI.SnakyPrototype.Certificate21.checked_276 line 582
  279. def OAI.SnakyPrototype.Certificate21.height_286 line 590
  280. def OAI.SnakyPrototype.Certificate21.childrenH_286 line 591
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_286 line 592
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_286 line 593
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_286 line 595
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_286 line 599
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_286 line 601
  286. def OAI.SnakyPrototype.Certificate21.checked_286 line 605
  287. def OAI.SnakyPrototype.Certificate21.height_290 line 613
  288. def OAI.SnakyPrototype.Certificate21.childrenH_290 line 614
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_290 line 615
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_290 line 616
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_290 line 618
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_290 line 622
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_290 line 624
  294. def OAI.SnakyPrototype.Certificate21.checked_290 line 628
  295. def OAI.SnakyPrototype.Certificate21.height_295 line 636
  296. def OAI.SnakyPrototype.Certificate21.childrenH_295 line 637
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_295 line 638
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_295 line 639
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_295 line 641
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_295 line 645
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_295 line 647
  302. def OAI.SnakyPrototype.Certificate21.checked_295 line 651
  303. def OAI.SnakyPrototype.Certificate21.height_297 line 659
  304. def OAI.SnakyPrototype.Certificate21.childrenH_297 line 660
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_297 line 661
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_297 line 662
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_297 line 664
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_297 line 668
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_297 line 670
  310. def OAI.SnakyPrototype.Certificate21.checked_297 line 674
  311. def OAI.SnakyPrototype.Certificate21.height_298 line 682
  312. def OAI.SnakyPrototype.Certificate21.childrenH_298 line 683
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_298 line 684
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_298 line 685
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_298 line 687
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_298 line 691
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_298 line 693
  318. def OAI.SnakyPrototype.Certificate21.checked_298 line 697
  319. def OAI.SnakyPrototype.Certificate21.height_309 line 705
  320. def OAI.SnakyPrototype.Certificate21.childrenH_309 line 706
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_309 line 707
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_309 line 708
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_309 line 710
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_309 line 714
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_309 line 716
  326. def OAI.SnakyPrototype.Certificate21.checked_309 line 720
  327. def OAI.SnakyPrototype.Certificate21.height_317 line 728
  328. def OAI.SnakyPrototype.Certificate21.childrenH_317 line 729
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_317 line 730
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_317 line 731
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_317 line 733
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_317 line 737
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_317 line 739
  334. def OAI.SnakyPrototype.Certificate21.checked_317 line 743
  335. def OAI.SnakyPrototype.Certificate21.height_318 line 751
  336. def OAI.SnakyPrototype.Certificate21.childrenH_318 line 752
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_318 line 753
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_318 line 754
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_318 line 756
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_318 line 760
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_318 line 762
  342. def OAI.SnakyPrototype.Certificate21.checked_318 line 766
  343. def OAI.SnakyPrototype.Certificate21.height_320 line 774
  344. def OAI.SnakyPrototype.Certificate21.childrenH_320 line 775
  345. theorem OAI.SnakyPrototype.Certificate21.height_exact_320 line 776
  346. theorem OAI.SnakyPrototype.Certificate21.required_origin_320 line 777
  347. theorem OAI.SnakyPrototype.Certificate21.required_exact_320 line 779
  348. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_320 line 783
  349. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_320 line 785
  350. def OAI.SnakyPrototype.Certificate21.checked_320 line 789
  351. def OAI.SnakyPrototype.Certificate21.height_324 line 797
  352. def OAI.SnakyPrototype.Certificate21.childrenH_324 line 798
  353. theorem OAI.SnakyPrototype.Certificate21.height_exact_324 line 799
  354. theorem OAI.SnakyPrototype.Certificate21.required_origin_324 line 800
  355. theorem OAI.SnakyPrototype.Certificate21.required_exact_324 line 802
  356. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_324 line 806
  357. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_324 line 808
  358. def OAI.SnakyPrototype.Certificate21.checked_324 line 812
  359. def OAI.SnakyPrototype.Certificate21.height_329 line 820
  360. def OAI.SnakyPrototype.Certificate21.childrenH_329 line 821
  361. theorem OAI.SnakyPrototype.Certificate21.height_exact_329 line 822
  362. theorem OAI.SnakyPrototype.Certificate21.required_origin_329 line 823
  363. theorem OAI.SnakyPrototype.Certificate21.required_exact_329 line 825
  364. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_329 line 829
  365. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_329 line 831
  366. def OAI.SnakyPrototype.Certificate21.checked_329 line 835
  367. def OAI.SnakyPrototype.Certificate21.height_332 line 843
  368. def OAI.SnakyPrototype.Certificate21.childrenH_332 line 844
  369. theorem OAI.SnakyPrototype.Certificate21.height_exact_332 line 845
  370. theorem OAI.SnakyPrototype.Certificate21.required_origin_332 line 846
  371. theorem OAI.SnakyPrototype.Certificate21.required_exact_332 line 848
  372. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_332 line 852
  373. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_332 line 854
  374. def OAI.SnakyPrototype.Certificate21.checked_332 line 858
  375. def OAI.SnakyPrototype.Certificate21.height_337 line 866
  376. def OAI.SnakyPrototype.Certificate21.childrenH_337 line 867
  377. theorem OAI.SnakyPrototype.Certificate21.height_exact_337 line 868
  378. theorem OAI.SnakyPrototype.Certificate21.required_origin_337 line 869
  379. theorem OAI.SnakyPrototype.Certificate21.required_exact_337 line 871
  380. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_337 line 875
  381. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_337 line 877
  382. def OAI.SnakyPrototype.Certificate21.checked_337 line 881
  383. def OAI.SnakyPrototype.Certificate21.height_339 line 889
  384. def OAI.SnakyPrototype.Certificate21.childrenH_339 line 890
  385. theorem OAI.SnakyPrototype.Certificate21.height_exact_339 line 891
  386. theorem OAI.SnakyPrototype.Certificate21.required_origin_339 line 892
  387. theorem OAI.SnakyPrototype.Certificate21.required_exact_339 line 894
  388. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_339 line 898
  389. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_339 line 900
  390. def OAI.SnakyPrototype.Certificate21.checked_339 line 904
  391. def OAI.SnakyPrototype.Certificate21.height_341 line 912
  392. def OAI.SnakyPrototype.Certificate21.childrenH_341 line 913
  393. theorem OAI.SnakyPrototype.Certificate21.height_exact_341 line 914
  394. theorem OAI.SnakyPrototype.Certificate21.required_origin_341 line 915
  395. theorem OAI.SnakyPrototype.Certificate21.required_exact_341 line 917
  396. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_341 line 921
  397. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_341 line 923
  398. def OAI.SnakyPrototype.Certificate21.checked_341 line 927
  399. def OAI.SnakyPrototype.Certificate21.height_344 line 935
  400. def OAI.SnakyPrototype.Certificate21.childrenH_344 line 936
  401. theorem OAI.SnakyPrototype.Certificate21.height_exact_344 line 937
  402. theorem OAI.SnakyPrototype.Certificate21.required_origin_344 line 938
  403. theorem OAI.SnakyPrototype.Certificate21.required_exact_344 line 940
  404. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_344 line 944
  405. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_344 line 946
  406. def OAI.SnakyPrototype.Certificate21.checked_344 line 950
  407. def OAI.SnakyPrototype.Certificate21.height_353 line 958
  408. def OAI.SnakyPrototype.Certificate21.childrenH_353 line 959
  409. theorem OAI.SnakyPrototype.Certificate21.height_exact_353 line 960
  410. theorem OAI.SnakyPrototype.Certificate21.required_origin_353 line 961
  411. theorem OAI.SnakyPrototype.Certificate21.required_exact_353 line 963
  412. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_353 line 967
  413. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_353 line 969
  414. def OAI.SnakyPrototype.Certificate21.checked_353 line 973