OAI/GameTheory/SnakyTwentyOne/Cards/Height08Part01.lean

GitHub source file

414 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_120 line 20
  2. def OAI.SnakyPrototype.Certificate21.envelope_120 line 21
  3. def OAI.SnakyPrototype.Certificate21.childrenC_120 line 22
  4. def OAI.SnakyPrototype.Certificate21.childrenD_120 line 23
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_120 line 24
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_120 line 25
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_120 line 26
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_120 line 27
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_120 line 28
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_120 line 34
  11. def OAI.SnakyPrototype.Certificate21.required_171 line 39
  12. def OAI.SnakyPrototype.Certificate21.envelope_171 line 40
  13. def OAI.SnakyPrototype.Certificate21.childrenC_171 line 41
  14. def OAI.SnakyPrototype.Certificate21.childrenD_171 line 42
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_171 line 43
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_171 line 44
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_171 line 45
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_171 line 46
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_171 line 47
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_171 line 53
  21. def OAI.SnakyPrototype.Certificate21.required_174 line 58
  22. def OAI.SnakyPrototype.Certificate21.envelope_174 line 59
  23. def OAI.SnakyPrototype.Certificate21.childrenC_174 line 60
  24. def OAI.SnakyPrototype.Certificate21.childrenD_174 line 61
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_174 line 62
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_174 line 63
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_174 line 64
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_174 line 65
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_174 line 66
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_174 line 75
  31. def OAI.SnakyPrototype.Certificate21.required_257 line 80
  32. def OAI.SnakyPrototype.Certificate21.envelope_257 line 81
  33. def OAI.SnakyPrototype.Certificate21.childrenC_257 line 82
  34. def OAI.SnakyPrototype.Certificate21.childrenD_257 line 83
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_257 line 84
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_257 line 85
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_257 line 86
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_257 line 87
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_257 line 88
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_257 line 94
  41. def OAI.SnakyPrototype.Certificate21.required_258 line 99
  42. def OAI.SnakyPrototype.Certificate21.envelope_258 line 100
  43. def OAI.SnakyPrototype.Certificate21.childrenC_258 line 101
  44. def OAI.SnakyPrototype.Certificate21.childrenD_258 line 102
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_258 line 103
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_258 line 104
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_258 line 105
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_258 line 106
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_258 line 107
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_258 line 114
  51. def OAI.SnakyPrototype.Certificate21.required_285 line 119
  52. def OAI.SnakyPrototype.Certificate21.envelope_285 line 120
  53. def OAI.SnakyPrototype.Certificate21.childrenC_285 line 121
  54. def OAI.SnakyPrototype.Certificate21.childrenD_285 line 122
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_285 line 123
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_285 line 124
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_285 line 125
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_285 line 126
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_285 line 127
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_285 line 133
  61. def OAI.SnakyPrototype.Certificate21.required_319 line 138
  62. def OAI.SnakyPrototype.Certificate21.envelope_319 line 139
  63. def OAI.SnakyPrototype.Certificate21.childrenC_319 line 140
  64. def OAI.SnakyPrototype.Certificate21.childrenD_319 line 141
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_319 line 142
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_319 line 143
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_319 line 144
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_319 line 145
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_319 line 146
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_319 line 151
  71. def OAI.SnakyPrototype.Certificate21.required_321 line 156
  72. def OAI.SnakyPrototype.Certificate21.envelope_321 line 157
  73. def OAI.SnakyPrototype.Certificate21.childrenC_321 line 158
  74. def OAI.SnakyPrototype.Certificate21.childrenD_321 line 159
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_321 line 160
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_321 line 161
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_321 line 162
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_321 line 163
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_321 line 164
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_321 line 169
  81. def OAI.SnakyPrototype.Certificate21.required_323 line 174
  82. def OAI.SnakyPrototype.Certificate21.envelope_323 line 175
  83. def OAI.SnakyPrototype.Certificate21.childrenC_323 line 176
  84. def OAI.SnakyPrototype.Certificate21.childrenD_323 line 177
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_323 line 178
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_323 line 179
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_323 line 180
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_323 line 181
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_323 line 182
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_323 line 187
  91. def OAI.SnakyPrototype.Certificate21.required_338 line 192
  92. def OAI.SnakyPrototype.Certificate21.envelope_338 line 193
  93. def OAI.SnakyPrototype.Certificate21.childrenC_338 line 194
  94. def OAI.SnakyPrototype.Certificate21.childrenD_338 line 195
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_338 line 196
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_338 line 197
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_338 line 198
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_338 line 199
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_338 line 200
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_338 line 206
  101. def OAI.SnakyPrototype.Certificate21.required_345 line 211
  102. def OAI.SnakyPrototype.Certificate21.envelope_345 line 212
  103. def OAI.SnakyPrototype.Certificate21.childrenC_345 line 213
  104. def OAI.SnakyPrototype.Certificate21.childrenD_345 line 214
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_345 line 215
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_345 line 216
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_345 line 217
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_345 line 218
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_345 line 219
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_345 line 225
  111. def OAI.SnakyPrototype.Certificate21.required_373 line 230
  112. def OAI.SnakyPrototype.Certificate21.envelope_373 line 231
  113. def OAI.SnakyPrototype.Certificate21.childrenC_373 line 232
  114. def OAI.SnakyPrototype.Certificate21.childrenD_373 line 233
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_373 line 234
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_373 line 235
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_373 line 236
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_373 line 237
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_373 line 238
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_373 line 243
  121. def OAI.SnakyPrototype.Certificate21.required_395_i0 line 248
  122. def OAI.SnakyPrototype.Certificate21.envelope_395_i0 line 249
  123. def OAI.SnakyPrototype.Certificate21.childrenC_395_i0 line 250
  124. def OAI.SnakyPrototype.Certificate21.childrenD_395_i0 line 251
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_395_i0 line 252
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_395_i0 line 253
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_395_i0 line 254
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_395_i0 line 255
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_395_i0 line 256
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_395_i0 line 261
  131. def OAI.SnakyPrototype.Certificate21.required_395 line 266
  132. def OAI.SnakyPrototype.Certificate21.envelope_395 line 267
  133. def OAI.SnakyPrototype.Certificate21.childrenC_395 line 268
  134. def OAI.SnakyPrototype.Certificate21.childrenD_395 line 269
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_395 line 270
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_395 line 271
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_395 line 272
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_395 line 273
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_395 line 274
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_395 line 279
  141. def OAI.SnakyPrototype.Certificate21.required_405 line 284
  142. def OAI.SnakyPrototype.Certificate21.envelope_405 line 285
  143. def OAI.SnakyPrototype.Certificate21.childrenC_405 line 286
  144. def OAI.SnakyPrototype.Certificate21.childrenD_405 line 287
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_405 line 288
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_405 line 289
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_405 line 290
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_405 line 291
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_405 line 292
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_405 line 297
  151. def OAI.SnakyPrototype.Certificate21.required_412_i0 line 302
  152. def OAI.SnakyPrototype.Certificate21.envelope_412_i0 line 303
  153. def OAI.SnakyPrototype.Certificate21.childrenC_412_i0 line 304
  154. def OAI.SnakyPrototype.Certificate21.childrenD_412_i0 line 305
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_412_i0 line 306
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_412_i0 line 307
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_412_i0 line 308
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_412_i0 line 309
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_412_i0 line 310
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_412_i0 line 315
  161. def OAI.SnakyPrototype.Certificate21.required_412 line 320
  162. def OAI.SnakyPrototype.Certificate21.envelope_412 line 321
  163. def OAI.SnakyPrototype.Certificate21.childrenC_412 line 322
  164. def OAI.SnakyPrototype.Certificate21.childrenD_412 line 323
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_412 line 324
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_412 line 325
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_412 line 326
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_412 line 327
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_412 line 328
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_412 line 333
  171. def OAI.SnakyPrototype.Certificate21.required_419 line 338
  172. def OAI.SnakyPrototype.Certificate21.envelope_419 line 339
  173. def OAI.SnakyPrototype.Certificate21.childrenC_419 line 340
  174. def OAI.SnakyPrototype.Certificate21.childrenD_419 line 341
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_419 line 342
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_419 line 343
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_419 line 344
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_419 line 345
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_419 line 346
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_419 line 351
  181. def OAI.SnakyPrototype.Certificate21.required_420 line 356
  182. def OAI.SnakyPrototype.Certificate21.envelope_420 line 357
  183. def OAI.SnakyPrototype.Certificate21.childrenC_420 line 358
  184. def OAI.SnakyPrototype.Certificate21.childrenD_420 line 359
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_420 line 360
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_420 line 361
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_420 line 362
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_420 line 363
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_420 line 364
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_420 line 369
  191. def OAI.SnakyPrototype.Certificate21.required_438 line 374
  192. def OAI.SnakyPrototype.Certificate21.envelope_438 line 375
  193. def OAI.SnakyPrototype.Certificate21.childrenC_438 line 376
  194. def OAI.SnakyPrototype.Certificate21.childrenD_438 line 377
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_438 line 378
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_438 line 379
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_438 line 380
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_438 line 381
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_438 line 382
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_438 line 388
  201. def OAI.SnakyPrototype.Certificate21.required_440_i0 line 393
  202. def OAI.SnakyPrototype.Certificate21.envelope_440_i0 line 394
  203. def OAI.SnakyPrototype.Certificate21.childrenC_440_i0 line 395
  204. def OAI.SnakyPrototype.Certificate21.childrenD_440_i0 line 396
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_440_i0 line 397
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_440_i0 line 398
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_440_i0 line 399
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_440_i0 line 400
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_440_i0 line 401
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_440_i0 line 406
  211. def OAI.SnakyPrototype.Certificate21.required_440 line 411
  212. def OAI.SnakyPrototype.Certificate21.envelope_440 line 412
  213. def OAI.SnakyPrototype.Certificate21.childrenC_440 line 413
  214. def OAI.SnakyPrototype.Certificate21.childrenD_440 line 414
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_440 line 415
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_440 line 416
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_440 line 417
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_440 line 418
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_440 line 419
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_440 line 424
  221. def OAI.SnakyPrototype.Certificate21.required_448 line 429
  222. def OAI.SnakyPrototype.Certificate21.envelope_448 line 430
  223. def OAI.SnakyPrototype.Certificate21.childrenC_448 line 431
  224. def OAI.SnakyPrototype.Certificate21.childrenD_448 line 432
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_448 line 433
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_448 line 434
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_448 line 435
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_448 line 436
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_448 line 437
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_448 line 442
  231. def OAI.SnakyPrototype.Certificate21.height_120 line 447
  232. def OAI.SnakyPrototype.Certificate21.childrenH_120 line 448
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_120 line 449
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_120 line 450
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_120 line 452
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_120 line 456
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_120 line 458
  238. def OAI.SnakyPrototype.Certificate21.checked_120 line 462
  239. def OAI.SnakyPrototype.Certificate21.height_171 line 470
  240. def OAI.SnakyPrototype.Certificate21.childrenH_171 line 471
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_171 line 472
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_171 line 473
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_171 line 475
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_171 line 479
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_171 line 481
  246. def OAI.SnakyPrototype.Certificate21.checked_171 line 485
  247. def OAI.SnakyPrototype.Certificate21.height_174 line 493
  248. def OAI.SnakyPrototype.Certificate21.childrenH_174 line 494
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_174 line 495
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_174 line 496
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_174 line 498
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_174 line 502
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_174 line 504
  254. def OAI.SnakyPrototype.Certificate21.checked_174 line 508
  255. def OAI.SnakyPrototype.Certificate21.height_257 line 516
  256. def OAI.SnakyPrototype.Certificate21.childrenH_257 line 517
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_257 line 518
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_257 line 519
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_257 line 521
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_257 line 525
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_257 line 527
  262. def OAI.SnakyPrototype.Certificate21.checked_257 line 531
  263. def OAI.SnakyPrototype.Certificate21.height_258 line 539
  264. def OAI.SnakyPrototype.Certificate21.childrenH_258 line 540
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_258 line 541
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_258 line 542
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_258 line 544
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_258 line 548
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_258 line 550
  270. def OAI.SnakyPrototype.Certificate21.checked_258 line 554
  271. def OAI.SnakyPrototype.Certificate21.height_285 line 562
  272. def OAI.SnakyPrototype.Certificate21.childrenH_285 line 563
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_285 line 564
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_285 line 565
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_285 line 567
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_285 line 571
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_285 line 573
  278. def OAI.SnakyPrototype.Certificate21.checked_285 line 577
  279. def OAI.SnakyPrototype.Certificate21.height_319 line 585
  280. def OAI.SnakyPrototype.Certificate21.childrenH_319 line 586
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_319 line 587
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_319 line 588
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_319 line 590
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_319 line 594
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_319 line 596
  286. def OAI.SnakyPrototype.Certificate21.checked_319 line 600
  287. def OAI.SnakyPrototype.Certificate21.height_321 line 608
  288. def OAI.SnakyPrototype.Certificate21.childrenH_321 line 609
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_321 line 610
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_321 line 611
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_321 line 613
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_321 line 617
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_321 line 619
  294. def OAI.SnakyPrototype.Certificate21.checked_321 line 623
  295. def OAI.SnakyPrototype.Certificate21.height_323 line 631
  296. def OAI.SnakyPrototype.Certificate21.childrenH_323 line 632
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_323 line 633
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_323 line 634
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_323 line 636
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_323 line 640
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_323 line 642
  302. def OAI.SnakyPrototype.Certificate21.checked_323 line 646
  303. def OAI.SnakyPrototype.Certificate21.height_338 line 654
  304. def OAI.SnakyPrototype.Certificate21.childrenH_338 line 655
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_338 line 656
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_338 line 657
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_338 line 659
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_338 line 663
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_338 line 665
  310. def OAI.SnakyPrototype.Certificate21.checked_338 line 669
  311. def OAI.SnakyPrototype.Certificate21.height_345 line 677
  312. def OAI.SnakyPrototype.Certificate21.childrenH_345 line 678
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_345 line 679
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_345 line 680
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_345 line 682
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_345 line 686
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_345 line 688
  318. def OAI.SnakyPrototype.Certificate21.checked_345 line 692
  319. def OAI.SnakyPrototype.Certificate21.height_373 line 700
  320. def OAI.SnakyPrototype.Certificate21.childrenH_373 line 701
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_373 line 702
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_373 line 703
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_373 line 705
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_373 line 709
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_373 line 711
  326. def OAI.SnakyPrototype.Certificate21.checked_373 line 715
  327. def OAI.SnakyPrototype.Certificate21.height_395_i0 line 723
  328. def OAI.SnakyPrototype.Certificate21.childrenH_395_i0 line 724
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_395_i0 line 725
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_395_i0 line 726
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_395_i0 line 728
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_395_i0 line 732
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_395_i0 line 734
  334. def OAI.SnakyPrototype.Certificate21.checked_395_i0 line 738
  335. def OAI.SnakyPrototype.Certificate21.height_395 line 746
  336. def OAI.SnakyPrototype.Certificate21.childrenH_395 line 747
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_395 line 748
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_395 line 749
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_395 line 751
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_395 line 755
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_395 line 757
  342. def OAI.SnakyPrototype.Certificate21.checked_395 line 761
  343. def OAI.SnakyPrototype.Certificate21.height_405 line 769
  344. def OAI.SnakyPrototype.Certificate21.childrenH_405 line 770
  345. theorem OAI.SnakyPrototype.Certificate21.height_exact_405 line 771
  346. theorem OAI.SnakyPrototype.Certificate21.required_origin_405 line 772
  347. theorem OAI.SnakyPrototype.Certificate21.required_exact_405 line 774
  348. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_405 line 778
  349. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_405 line 780
  350. def OAI.SnakyPrototype.Certificate21.checked_405 line 784
  351. def OAI.SnakyPrototype.Certificate21.height_412_i0 line 792
  352. def OAI.SnakyPrototype.Certificate21.childrenH_412_i0 line 793
  353. theorem OAI.SnakyPrototype.Certificate21.height_exact_412_i0 line 794
  354. theorem OAI.SnakyPrototype.Certificate21.required_origin_412_i0 line 795
  355. theorem OAI.SnakyPrototype.Certificate21.required_exact_412_i0 line 797
  356. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_412_i0 line 801
  357. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_412_i0 line 803
  358. def OAI.SnakyPrototype.Certificate21.checked_412_i0 line 807
  359. def OAI.SnakyPrototype.Certificate21.height_412 line 815
  360. def OAI.SnakyPrototype.Certificate21.childrenH_412 line 816
  361. theorem OAI.SnakyPrototype.Certificate21.height_exact_412 line 817
  362. theorem OAI.SnakyPrototype.Certificate21.required_origin_412 line 818
  363. theorem OAI.SnakyPrototype.Certificate21.required_exact_412 line 820
  364. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_412 line 824
  365. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_412 line 826
  366. def OAI.SnakyPrototype.Certificate21.checked_412 line 830
  367. def OAI.SnakyPrototype.Certificate21.height_419 line 838
  368. def OAI.SnakyPrototype.Certificate21.childrenH_419 line 839
  369. theorem OAI.SnakyPrototype.Certificate21.height_exact_419 line 840
  370. theorem OAI.SnakyPrototype.Certificate21.required_origin_419 line 841
  371. theorem OAI.SnakyPrototype.Certificate21.required_exact_419 line 843
  372. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_419 line 847
  373. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_419 line 849
  374. def OAI.SnakyPrototype.Certificate21.checked_419 line 853
  375. def OAI.SnakyPrototype.Certificate21.height_420 line 861
  376. def OAI.SnakyPrototype.Certificate21.childrenH_420 line 862
  377. theorem OAI.SnakyPrototype.Certificate21.height_exact_420 line 863
  378. theorem OAI.SnakyPrototype.Certificate21.required_origin_420 line 864
  379. theorem OAI.SnakyPrototype.Certificate21.required_exact_420 line 866
  380. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_420 line 870
  381. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_420 line 872
  382. def OAI.SnakyPrototype.Certificate21.checked_420 line 876
  383. def OAI.SnakyPrototype.Certificate21.height_438 line 884
  384. def OAI.SnakyPrototype.Certificate21.childrenH_438 line 885
  385. theorem OAI.SnakyPrototype.Certificate21.height_exact_438 line 886
  386. theorem OAI.SnakyPrototype.Certificate21.required_origin_438 line 887
  387. theorem OAI.SnakyPrototype.Certificate21.required_exact_438 line 889
  388. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_438 line 893
  389. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_438 line 895
  390. def OAI.SnakyPrototype.Certificate21.checked_438 line 899
  391. def OAI.SnakyPrototype.Certificate21.height_440_i0 line 907
  392. def OAI.SnakyPrototype.Certificate21.childrenH_440_i0 line 908
  393. theorem OAI.SnakyPrototype.Certificate21.height_exact_440_i0 line 909
  394. theorem OAI.SnakyPrototype.Certificate21.required_origin_440_i0 line 910
  395. theorem OAI.SnakyPrototype.Certificate21.required_exact_440_i0 line 912
  396. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_440_i0 line 916
  397. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_440_i0 line 918
  398. def OAI.SnakyPrototype.Certificate21.checked_440_i0 line 922
  399. def OAI.SnakyPrototype.Certificate21.height_440 line 930
  400. def OAI.SnakyPrototype.Certificate21.childrenH_440 line 931
  401. theorem OAI.SnakyPrototype.Certificate21.height_exact_440 line 932
  402. theorem OAI.SnakyPrototype.Certificate21.required_origin_440 line 933
  403. theorem OAI.SnakyPrototype.Certificate21.required_exact_440 line 935
  404. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_440 line 939
  405. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_440 line 941
  406. def OAI.SnakyPrototype.Certificate21.checked_440 line 945
  407. def OAI.SnakyPrototype.Certificate21.height_448 line 953
  408. def OAI.SnakyPrototype.Certificate21.childrenH_448 line 954
  409. theorem OAI.SnakyPrototype.Certificate21.height_exact_448 line 955
  410. theorem OAI.SnakyPrototype.Certificate21.required_origin_448 line 956
  411. theorem OAI.SnakyPrototype.Certificate21.required_exact_448 line 958
  412. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_448 line 962
  413. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_448 line 964
  414. def OAI.SnakyPrototype.Certificate21.checked_448 line 968