OAI/GameTheory/SnakyTwentyOne/Cards/Height08Part03.lean

GitHub source file

396 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_518_i1 line 27
  2. def OAI.SnakyPrototype.Certificate21.envelope_518_i1 line 28
  3. def OAI.SnakyPrototype.Certificate21.childrenC_518_i1 line 29
  4. def OAI.SnakyPrototype.Certificate21.childrenD_518_i1 line 30
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_518_i1 line 31
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_518_i1 line 32
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_518_i1 line 33
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_518_i1 line 34
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_518_i1 line 35
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_518_i1 line 41
  11. def OAI.SnakyPrototype.Certificate21.required_518_i0 line 46
  12. def OAI.SnakyPrototype.Certificate21.envelope_518_i0 line 47
  13. def OAI.SnakyPrototype.Certificate21.childrenC_518_i0 line 48
  14. def OAI.SnakyPrototype.Certificate21.childrenD_518_i0 line 49
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_518_i0 line 50
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_518_i0 line 51
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_518_i0 line 52
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_518_i0 line 53
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_518_i0 line 54
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_518_i0 line 59
  21. def OAI.SnakyPrototype.Certificate21.required_518 line 64
  22. def OAI.SnakyPrototype.Certificate21.envelope_518 line 65
  23. def OAI.SnakyPrototype.Certificate21.childrenC_518 line 66
  24. def OAI.SnakyPrototype.Certificate21.childrenD_518 line 67
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_518 line 68
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_518 line 69
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_518 line 70
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_518 line 71
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_518 line 72
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_518 line 79
  31. def OAI.SnakyPrototype.Certificate21.required_523 line 84
  32. def OAI.SnakyPrototype.Certificate21.envelope_523 line 85
  33. def OAI.SnakyPrototype.Certificate21.childrenC_523 line 86
  34. def OAI.SnakyPrototype.Certificate21.childrenD_523 line 87
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_523 line 88
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_523 line 89
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_523 line 90
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_523 line 91
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_523 line 92
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_523 line 100
  41. def OAI.SnakyPrototype.Certificate21.required_524 line 105
  42. def OAI.SnakyPrototype.Certificate21.envelope_524 line 106
  43. def OAI.SnakyPrototype.Certificate21.childrenC_524 line 107
  44. def OAI.SnakyPrototype.Certificate21.childrenD_524 line 108
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_524 line 109
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_524 line 110
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_524 line 111
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_524 line 112
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_524 line 113
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_524 line 120
  51. def OAI.SnakyPrototype.Certificate21.required_530_i2 line 125
  52. def OAI.SnakyPrototype.Certificate21.envelope_530_i2 line 126
  53. def OAI.SnakyPrototype.Certificate21.childrenC_530_i2 line 127
  54. def OAI.SnakyPrototype.Certificate21.childrenD_530_i2 line 128
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_530_i2 line 129
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_530_i2 line 130
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_530_i2 line 131
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_530_i2 line 132
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_530_i2 line 133
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_530_i2 line 138
  61. def OAI.SnakyPrototype.Certificate21.required_530_i1 line 143
  62. def OAI.SnakyPrototype.Certificate21.envelope_530_i1 line 144
  63. def OAI.SnakyPrototype.Certificate21.childrenC_530_i1 line 145
  64. def OAI.SnakyPrototype.Certificate21.childrenD_530_i1 line 146
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_530_i1 line 147
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_530_i1 line 148
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_530_i1 line 149
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_530_i1 line 150
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_530_i1 line 151
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_530_i1 line 156
  71. def OAI.SnakyPrototype.Certificate21.required_530_i0 line 161
  72. def OAI.SnakyPrototype.Certificate21.envelope_530_i0 line 162
  73. def OAI.SnakyPrototype.Certificate21.childrenC_530_i0 line 163
  74. def OAI.SnakyPrototype.Certificate21.childrenD_530_i0 line 164
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_530_i0 line 165
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_530_i0 line 166
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_530_i0 line 167
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_530_i0 line 168
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_530_i0 line 169
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_530_i0 line 174
  81. def OAI.SnakyPrototype.Certificate21.required_530 line 179
  82. def OAI.SnakyPrototype.Certificate21.envelope_530 line 180
  83. def OAI.SnakyPrototype.Certificate21.childrenC_530 line 181
  84. def OAI.SnakyPrototype.Certificate21.childrenD_530 line 182
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_530 line 183
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_530 line 184
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_530 line 185
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_530 line 186
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_530 line 187
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_530 line 194
  91. def OAI.SnakyPrototype.Certificate21.required_532_i0 line 199
  92. def OAI.SnakyPrototype.Certificate21.envelope_532_i0 line 200
  93. def OAI.SnakyPrototype.Certificate21.childrenC_532_i0 line 201
  94. def OAI.SnakyPrototype.Certificate21.childrenD_532_i0 line 202
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_532_i0 line 203
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_532_i0 line 204
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_532_i0 line 205
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_532_i0 line 206
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_532_i0 line 207
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_532_i0 line 214
  101. def OAI.SnakyPrototype.Certificate21.required_532 line 219
  102. def OAI.SnakyPrototype.Certificate21.envelope_532 line 220
  103. def OAI.SnakyPrototype.Certificate21.childrenC_532 line 221
  104. def OAI.SnakyPrototype.Certificate21.childrenD_532 line 222
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_532 line 223
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_532 line 224
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_532 line 225
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_532 line 226
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_532 line 227
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_532 line 234
  111. def OAI.SnakyPrototype.Certificate21.required_533_i0 line 239
  112. def OAI.SnakyPrototype.Certificate21.envelope_533_i0 line 240
  113. def OAI.SnakyPrototype.Certificate21.childrenC_533_i0 line 241
  114. def OAI.SnakyPrototype.Certificate21.childrenD_533_i0 line 242
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_533_i0 line 243
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_533_i0 line 244
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_533_i0 line 245
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_533_i0 line 246
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_533_i0 line 247
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_533_i0 line 253
  121. def OAI.SnakyPrototype.Certificate21.required_533 line 258
  122. def OAI.SnakyPrototype.Certificate21.envelope_533 line 259
  123. def OAI.SnakyPrototype.Certificate21.childrenC_533 line 260
  124. def OAI.SnakyPrototype.Certificate21.childrenD_533 line 261
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_533 line 262
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_533 line 263
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_533 line 264
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_533 line 265
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_533 line 266
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_533 line 272
  131. def OAI.SnakyPrototype.Certificate21.required_534_i1 line 277
  132. def OAI.SnakyPrototype.Certificate21.envelope_534_i1 line 278
  133. def OAI.SnakyPrototype.Certificate21.childrenC_534_i1 line 279
  134. def OAI.SnakyPrototype.Certificate21.childrenD_534_i1 line 280
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_534_i1 line 281
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_534_i1 line 282
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_534_i1 line 283
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_534_i1 line 284
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_534_i1 line 285
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_534_i1 line 290
  141. def OAI.SnakyPrototype.Certificate21.required_534_i2 line 295
  142. def OAI.SnakyPrototype.Certificate21.envelope_534_i2 line 296
  143. def OAI.SnakyPrototype.Certificate21.childrenC_534_i2 line 297
  144. def OAI.SnakyPrototype.Certificate21.childrenD_534_i2 line 298
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_534_i2 line 299
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_534_i2 line 300
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_534_i2 line 301
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_534_i2 line 302
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_534_i2 line 303
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_534_i2 line 308
  151. def OAI.SnakyPrototype.Certificate21.required_534_i0 line 313
  152. def OAI.SnakyPrototype.Certificate21.envelope_534_i0 line 314
  153. def OAI.SnakyPrototype.Certificate21.childrenC_534_i0 line 315
  154. def OAI.SnakyPrototype.Certificate21.childrenD_534_i0 line 316
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_534_i0 line 317
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_534_i0 line 318
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_534_i0 line 319
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_534_i0 line 320
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_534_i0 line 321
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_534_i0 line 327
  161. def OAI.SnakyPrototype.Certificate21.required_534 line 332
  162. def OAI.SnakyPrototype.Certificate21.envelope_534 line 333
  163. def OAI.SnakyPrototype.Certificate21.childrenC_534 line 334
  164. def OAI.SnakyPrototype.Certificate21.childrenD_534 line 335
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_534 line 336
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_534 line 337
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_534 line 338
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_534 line 339
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_534 line 340
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_534 line 347
  171. def OAI.SnakyPrototype.Certificate21.required_547_i0 line 352
  172. def OAI.SnakyPrototype.Certificate21.envelope_547_i0 line 353
  173. def OAI.SnakyPrototype.Certificate21.childrenC_547_i0 line 354
  174. def OAI.SnakyPrototype.Certificate21.childrenD_547_i0 line 355
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_547_i0 line 356
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_547_i0 line 357
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_547_i0 line 358
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_547_i0 line 359
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_547_i0 line 360
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_547_i0 line 365
  181. def OAI.SnakyPrototype.Certificate21.required_547_i1 line 370
  182. def OAI.SnakyPrototype.Certificate21.envelope_547_i1 line 371
  183. def OAI.SnakyPrototype.Certificate21.childrenC_547_i1 line 372
  184. def OAI.SnakyPrototype.Certificate21.childrenD_547_i1 line 373
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_547_i1 line 374
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_547_i1 line 375
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_547_i1 line 376
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_547_i1 line 377
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_547_i1 line 378
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_547_i1 line 383
  191. def OAI.SnakyPrototype.Certificate21.required_547 line 388
  192. def OAI.SnakyPrototype.Certificate21.envelope_547 line 389
  193. def OAI.SnakyPrototype.Certificate21.childrenC_547 line 390
  194. def OAI.SnakyPrototype.Certificate21.childrenD_547 line 391
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_547 line 392
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_547 line 393
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_547 line 394
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_547 line 395
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_547 line 396
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_547 line 403
  201. def OAI.SnakyPrototype.Certificate21.required_558_i0 line 408
  202. def OAI.SnakyPrototype.Certificate21.envelope_558_i0 line 409
  203. def OAI.SnakyPrototype.Certificate21.childrenC_558_i0 line 410
  204. def OAI.SnakyPrototype.Certificate21.childrenD_558_i0 line 411
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_558_i0 line 412
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_558_i0 line 413
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_558_i0 line 414
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_558_i0 line 415
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_558_i0 line 416
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_558_i0 line 421
  211. def OAI.SnakyPrototype.Certificate21.required_558 line 426
  212. def OAI.SnakyPrototype.Certificate21.envelope_558 line 427
  213. def OAI.SnakyPrototype.Certificate21.childrenC_558 line 428
  214. def OAI.SnakyPrototype.Certificate21.childrenD_558 line 429
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_558 line 430
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_558 line 431
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_558 line 432
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_558 line 433
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_558 line 434
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_558 line 441
  221. def OAI.SnakyPrototype.Certificate21.height_518_i1 line 446
  222. def OAI.SnakyPrototype.Certificate21.childrenH_518_i1 line 447
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_518_i1 line 448
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_518_i1 line 449
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_518_i1 line 451
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_518_i1 line 455
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_518_i1 line 457
  228. def OAI.SnakyPrototype.Certificate21.checked_518_i1 line 461
  229. def OAI.SnakyPrototype.Certificate21.height_518_i0 line 469
  230. def OAI.SnakyPrototype.Certificate21.childrenH_518_i0 line 470
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_518_i0 line 471
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_518_i0 line 472
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_518_i0 line 474
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_518_i0 line 478
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_518_i0 line 480
  236. def OAI.SnakyPrototype.Certificate21.checked_518_i0 line 484
  237. def OAI.SnakyPrototype.Certificate21.height_518 line 492
  238. def OAI.SnakyPrototype.Certificate21.childrenH_518 line 493
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_518 line 494
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_518 line 495
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_518 line 497
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_518 line 501
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_518 line 503
  244. def OAI.SnakyPrototype.Certificate21.checked_518 line 507
  245. def OAI.SnakyPrototype.Certificate21.height_523 line 515
  246. def OAI.SnakyPrototype.Certificate21.childrenH_523 line 516
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_523 line 517
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_523 line 518
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_523 line 520
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_523 line 524
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_523 line 526
  252. def OAI.SnakyPrototype.Certificate21.checked_523 line 530
  253. def OAI.SnakyPrototype.Certificate21.height_524 line 538
  254. def OAI.SnakyPrototype.Certificate21.childrenH_524 line 539
  255. theorem OAI.SnakyPrototype.Certificate21.height_exact_524 line 540
  256. theorem OAI.SnakyPrototype.Certificate21.required_origin_524 line 541
  257. theorem OAI.SnakyPrototype.Certificate21.required_exact_524 line 543
  258. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_524 line 547
  259. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_524 line 549
  260. def OAI.SnakyPrototype.Certificate21.checked_524 line 553
  261. def OAI.SnakyPrototype.Certificate21.height_530_i2 line 561
  262. def OAI.SnakyPrototype.Certificate21.childrenH_530_i2 line 562
  263. theorem OAI.SnakyPrototype.Certificate21.height_exact_530_i2 line 563
  264. theorem OAI.SnakyPrototype.Certificate21.required_origin_530_i2 line 564
  265. theorem OAI.SnakyPrototype.Certificate21.required_exact_530_i2 line 566
  266. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_530_i2 line 570
  267. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_530_i2 line 572
  268. def OAI.SnakyPrototype.Certificate21.checked_530_i2 line 576
  269. def OAI.SnakyPrototype.Certificate21.height_530_i1 line 584
  270. def OAI.SnakyPrototype.Certificate21.childrenH_530_i1 line 585
  271. theorem OAI.SnakyPrototype.Certificate21.height_exact_530_i1 line 586
  272. theorem OAI.SnakyPrototype.Certificate21.required_origin_530_i1 line 587
  273. theorem OAI.SnakyPrototype.Certificate21.required_exact_530_i1 line 589
  274. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_530_i1 line 593
  275. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_530_i1 line 595
  276. def OAI.SnakyPrototype.Certificate21.checked_530_i1 line 599
  277. def OAI.SnakyPrototype.Certificate21.height_530_i0 line 607
  278. def OAI.SnakyPrototype.Certificate21.childrenH_530_i0 line 608
  279. theorem OAI.SnakyPrototype.Certificate21.height_exact_530_i0 line 609
  280. theorem OAI.SnakyPrototype.Certificate21.required_origin_530_i0 line 610
  281. theorem OAI.SnakyPrototype.Certificate21.required_exact_530_i0 line 612
  282. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_530_i0 line 616
  283. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_530_i0 line 618
  284. def OAI.SnakyPrototype.Certificate21.checked_530_i0 line 622
  285. def OAI.SnakyPrototype.Certificate21.height_530 line 630
  286. def OAI.SnakyPrototype.Certificate21.childrenH_530 line 631
  287. theorem OAI.SnakyPrototype.Certificate21.height_exact_530 line 632
  288. theorem OAI.SnakyPrototype.Certificate21.required_origin_530 line 633
  289. theorem OAI.SnakyPrototype.Certificate21.required_exact_530 line 635
  290. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_530 line 639
  291. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_530 line 641
  292. def OAI.SnakyPrototype.Certificate21.checked_530 line 645
  293. def OAI.SnakyPrototype.Certificate21.height_532_i0 line 653
  294. def OAI.SnakyPrototype.Certificate21.childrenH_532_i0 line 654
  295. theorem OAI.SnakyPrototype.Certificate21.height_exact_532_i0 line 655
  296. theorem OAI.SnakyPrototype.Certificate21.required_origin_532_i0 line 656
  297. theorem OAI.SnakyPrototype.Certificate21.required_exact_532_i0 line 658
  298. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_532_i0 line 662
  299. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_532_i0 line 664
  300. def OAI.SnakyPrototype.Certificate21.checked_532_i0 line 668
  301. def OAI.SnakyPrototype.Certificate21.height_532 line 676
  302. def OAI.SnakyPrototype.Certificate21.childrenH_532 line 677
  303. theorem OAI.SnakyPrototype.Certificate21.height_exact_532 line 678
  304. theorem OAI.SnakyPrototype.Certificate21.required_origin_532 line 679
  305. theorem OAI.SnakyPrototype.Certificate21.required_exact_532 line 681
  306. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_532 line 685
  307. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_532 line 687
  308. def OAI.SnakyPrototype.Certificate21.checked_532 line 691
  309. def OAI.SnakyPrototype.Certificate21.height_533_i0 line 699
  310. def OAI.SnakyPrototype.Certificate21.childrenH_533_i0 line 700
  311. theorem OAI.SnakyPrototype.Certificate21.height_exact_533_i0 line 701
  312. theorem OAI.SnakyPrototype.Certificate21.required_origin_533_i0 line 702
  313. theorem OAI.SnakyPrototype.Certificate21.required_exact_533_i0 line 704
  314. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_533_i0 line 708
  315. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_533_i0 line 710
  316. def OAI.SnakyPrototype.Certificate21.checked_533_i0 line 714
  317. def OAI.SnakyPrototype.Certificate21.height_533 line 722
  318. def OAI.SnakyPrototype.Certificate21.childrenH_533 line 723
  319. theorem OAI.SnakyPrototype.Certificate21.height_exact_533 line 724
  320. theorem OAI.SnakyPrototype.Certificate21.required_origin_533 line 725
  321. theorem OAI.SnakyPrototype.Certificate21.required_exact_533 line 727
  322. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_533 line 731
  323. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_533 line 733
  324. def OAI.SnakyPrototype.Certificate21.checked_533 line 737
  325. def OAI.SnakyPrototype.Certificate21.height_534_i1 line 745
  326. def OAI.SnakyPrototype.Certificate21.childrenH_534_i1 line 746
  327. theorem OAI.SnakyPrototype.Certificate21.height_exact_534_i1 line 747
  328. theorem OAI.SnakyPrototype.Certificate21.required_origin_534_i1 line 748
  329. theorem OAI.SnakyPrototype.Certificate21.required_exact_534_i1 line 750
  330. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_534_i1 line 754
  331. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_534_i1 line 756
  332. def OAI.SnakyPrototype.Certificate21.checked_534_i1 line 760
  333. def OAI.SnakyPrototype.Certificate21.height_534_i2 line 768
  334. def OAI.SnakyPrototype.Certificate21.childrenH_534_i2 line 769
  335. theorem OAI.SnakyPrototype.Certificate21.height_exact_534_i2 line 770
  336. theorem OAI.SnakyPrototype.Certificate21.required_origin_534_i2 line 771
  337. theorem OAI.SnakyPrototype.Certificate21.required_exact_534_i2 line 773
  338. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_534_i2 line 777
  339. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_534_i2 line 779
  340. def OAI.SnakyPrototype.Certificate21.checked_534_i2 line 783
  341. def OAI.SnakyPrototype.Certificate21.height_534_i0 line 791
  342. def OAI.SnakyPrototype.Certificate21.childrenH_534_i0 line 792
  343. theorem OAI.SnakyPrototype.Certificate21.height_exact_534_i0 line 793
  344. theorem OAI.SnakyPrototype.Certificate21.required_origin_534_i0 line 794
  345. theorem OAI.SnakyPrototype.Certificate21.required_exact_534_i0 line 796
  346. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_534_i0 line 800
  347. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_534_i0 line 802
  348. def OAI.SnakyPrototype.Certificate21.checked_534_i0 line 806
  349. def OAI.SnakyPrototype.Certificate21.height_534 line 814
  350. def OAI.SnakyPrototype.Certificate21.childrenH_534 line 815
  351. theorem OAI.SnakyPrototype.Certificate21.height_exact_534 line 816
  352. theorem OAI.SnakyPrototype.Certificate21.required_origin_534 line 817
  353. theorem OAI.SnakyPrototype.Certificate21.required_exact_534 line 819
  354. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_534 line 823
  355. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_534 line 825
  356. def OAI.SnakyPrototype.Certificate21.checked_534 line 829
  357. def OAI.SnakyPrototype.Certificate21.height_547_i0 line 837
  358. def OAI.SnakyPrototype.Certificate21.childrenH_547_i0 line 838
  359. theorem OAI.SnakyPrototype.Certificate21.height_exact_547_i0 line 839
  360. theorem OAI.SnakyPrototype.Certificate21.required_origin_547_i0 line 840
  361. theorem OAI.SnakyPrototype.Certificate21.required_exact_547_i0 line 842
  362. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_547_i0 line 846
  363. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_547_i0 line 848
  364. def OAI.SnakyPrototype.Certificate21.checked_547_i0 line 852
  365. def OAI.SnakyPrototype.Certificate21.height_547_i1 line 860
  366. def OAI.SnakyPrototype.Certificate21.childrenH_547_i1 line 861
  367. theorem OAI.SnakyPrototype.Certificate21.height_exact_547_i1 line 862
  368. theorem OAI.SnakyPrototype.Certificate21.required_origin_547_i1 line 863
  369. theorem OAI.SnakyPrototype.Certificate21.required_exact_547_i1 line 865
  370. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_547_i1 line 869
  371. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_547_i1 line 871
  372. def OAI.SnakyPrototype.Certificate21.checked_547_i1 line 875
  373. def OAI.SnakyPrototype.Certificate21.height_547 line 883
  374. def OAI.SnakyPrototype.Certificate21.childrenH_547 line 884
  375. theorem OAI.SnakyPrototype.Certificate21.height_exact_547 line 885
  376. theorem OAI.SnakyPrototype.Certificate21.required_origin_547 line 886
  377. theorem OAI.SnakyPrototype.Certificate21.required_exact_547 line 888
  378. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_547 line 892
  379. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_547 line 894
  380. def OAI.SnakyPrototype.Certificate21.checked_547 line 898
  381. def OAI.SnakyPrototype.Certificate21.height_558_i0 line 906
  382. def OAI.SnakyPrototype.Certificate21.childrenH_558_i0 line 907
  383. theorem OAI.SnakyPrototype.Certificate21.height_exact_558_i0 line 908
  384. theorem OAI.SnakyPrototype.Certificate21.required_origin_558_i0 line 909
  385. theorem OAI.SnakyPrototype.Certificate21.required_exact_558_i0 line 911
  386. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_558_i0 line 915
  387. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_558_i0 line 917
  388. def OAI.SnakyPrototype.Certificate21.checked_558_i0 line 921
  389. def OAI.SnakyPrototype.Certificate21.height_558 line 929
  390. def OAI.SnakyPrototype.Certificate21.childrenH_558 line 930
  391. theorem OAI.SnakyPrototype.Certificate21.height_exact_558 line 931
  392. theorem OAI.SnakyPrototype.Certificate21.required_origin_558 line 932
  393. theorem OAI.SnakyPrototype.Certificate21.required_exact_558 line 934
  394. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_558 line 938
  395. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_558 line 940
  396. def OAI.SnakyPrototype.Certificate21.checked_558 line 944