OAI/GameTheory/SnakyTwentyOne/Cards/Height06Part04.lean

GitHub source file

360 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_378_i0 line 20
  2. def OAI.SnakyPrototype.Certificate21.envelope_378_i0 line 21
  3. def OAI.SnakyPrototype.Certificate21.childrenC_378_i0 line 22
  4. def OAI.SnakyPrototype.Certificate21.childrenD_378_i0 line 23
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_378_i0 line 24
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_378_i0 line 25
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_378_i0 line 26
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_378_i0 line 27
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_378_i0 line 28
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_378_i0 line 33
  11. def OAI.SnakyPrototype.Certificate21.required_378 line 38
  12. def OAI.SnakyPrototype.Certificate21.envelope_378 line 39
  13. def OAI.SnakyPrototype.Certificate21.childrenC_378 line 40
  14. def OAI.SnakyPrototype.Certificate21.childrenD_378 line 41
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_378 line 42
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_378 line 43
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_378 line 44
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_378 line 45
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_378 line 46
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_378 line 51
  21. def OAI.SnakyPrototype.Certificate21.required_384 line 56
  22. def OAI.SnakyPrototype.Certificate21.envelope_384 line 57
  23. def OAI.SnakyPrototype.Certificate21.childrenC_384 line 58
  24. def OAI.SnakyPrototype.Certificate21.childrenD_384 line 59
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_384 line 60
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_384 line 61
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_384 line 62
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_384 line 63
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_384 line 64
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_384 line 69
  31. def OAI.SnakyPrototype.Certificate21.required_387 line 74
  32. def OAI.SnakyPrototype.Certificate21.envelope_387 line 75
  33. def OAI.SnakyPrototype.Certificate21.childrenC_387 line 76
  34. def OAI.SnakyPrototype.Certificate21.childrenD_387 line 77
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_387 line 78
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_387 line 79
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_387 line 80
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_387 line 81
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_387 line 82
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_387 line 88
  41. def OAI.SnakyPrototype.Certificate21.required_390 line 93
  42. def OAI.SnakyPrototype.Certificate21.envelope_390 line 94
  43. def OAI.SnakyPrototype.Certificate21.childrenC_390 line 95
  44. def OAI.SnakyPrototype.Certificate21.childrenD_390 line 96
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_390 line 97
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_390 line 98
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_390 line 99
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_390 line 100
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_390 line 101
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_390 line 107
  51. def OAI.SnakyPrototype.Certificate21.required_392 line 112
  52. def OAI.SnakyPrototype.Certificate21.envelope_392 line 113
  53. def OAI.SnakyPrototype.Certificate21.childrenC_392 line 114
  54. def OAI.SnakyPrototype.Certificate21.childrenD_392 line 115
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_392 line 116
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_392 line 117
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_392 line 118
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_392 line 119
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_392 line 120
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_392 line 125
  61. def OAI.SnakyPrototype.Certificate21.required_393 line 130
  62. def OAI.SnakyPrototype.Certificate21.envelope_393 line 131
  63. def OAI.SnakyPrototype.Certificate21.childrenC_393 line 132
  64. def OAI.SnakyPrototype.Certificate21.childrenD_393 line 133
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_393 line 134
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_393 line 135
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_393 line 136
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_393 line 137
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_393 line 138
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_393 line 144
  71. def OAI.SnakyPrototype.Certificate21.required_403_i0 line 149
  72. def OAI.SnakyPrototype.Certificate21.envelope_403_i0 line 150
  73. def OAI.SnakyPrototype.Certificate21.childrenC_403_i0 line 151
  74. def OAI.SnakyPrototype.Certificate21.childrenD_403_i0 line 152
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_403_i0 line 153
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_403_i0 line 154
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_403_i0 line 155
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_403_i0 line 156
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_403_i0 line 157
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_403_i0 line 162
  81. def OAI.SnakyPrototype.Certificate21.required_403 line 167
  82. def OAI.SnakyPrototype.Certificate21.envelope_403 line 168
  83. def OAI.SnakyPrototype.Certificate21.childrenC_403 line 169
  84. def OAI.SnakyPrototype.Certificate21.childrenD_403 line 170
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_403 line 171
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_403 line 172
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_403 line 173
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_403 line 174
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_403 line 175
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_403 line 180
  91. def OAI.SnakyPrototype.Certificate21.required_414 line 185
  92. def OAI.SnakyPrototype.Certificate21.envelope_414 line 186
  93. def OAI.SnakyPrototype.Certificate21.childrenC_414 line 187
  94. def OAI.SnakyPrototype.Certificate21.childrenD_414 line 188
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_414 line 189
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_414 line 190
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_414 line 191
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_414 line 192
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_414 line 193
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_414 line 198
  101. def OAI.SnakyPrototype.Certificate21.required_417 line 203
  102. def OAI.SnakyPrototype.Certificate21.envelope_417 line 204
  103. def OAI.SnakyPrototype.Certificate21.childrenC_417 line 205
  104. def OAI.SnakyPrototype.Certificate21.childrenD_417 line 206
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_417 line 207
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_417 line 208
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_417 line 209
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_417 line 210
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_417 line 211
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_417 line 216
  111. def OAI.SnakyPrototype.Certificate21.required_423_i0 line 221
  112. def OAI.SnakyPrototype.Certificate21.envelope_423_i0 line 222
  113. def OAI.SnakyPrototype.Certificate21.childrenC_423_i0 line 223
  114. def OAI.SnakyPrototype.Certificate21.childrenD_423_i0 line 224
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_423_i0 line 225
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_423_i0 line 226
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_423_i0 line 227
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_423_i0 line 228
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_423_i0 line 229
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_423_i0 line 234
  121. def OAI.SnakyPrototype.Certificate21.required_423 line 239
  122. def OAI.SnakyPrototype.Certificate21.envelope_423 line 240
  123. def OAI.SnakyPrototype.Certificate21.childrenC_423 line 241
  124. def OAI.SnakyPrototype.Certificate21.childrenD_423 line 242
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_423 line 243
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_423 line 244
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_423 line 245
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_423 line 246
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_423 line 247
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_423 line 252
  131. def OAI.SnakyPrototype.Certificate21.required_429_i0 line 257
  132. def OAI.SnakyPrototype.Certificate21.envelope_429_i0 line 258
  133. def OAI.SnakyPrototype.Certificate21.childrenC_429_i0 line 259
  134. def OAI.SnakyPrototype.Certificate21.childrenD_429_i0 line 260
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_429_i0 line 261
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_429_i0 line 262
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_429_i0 line 263
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_429_i0 line 264
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_429_i0 line 265
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_429_i0 line 270
  141. def OAI.SnakyPrototype.Certificate21.required_429 line 275
  142. def OAI.SnakyPrototype.Certificate21.envelope_429 line 276
  143. def OAI.SnakyPrototype.Certificate21.childrenC_429 line 277
  144. def OAI.SnakyPrototype.Certificate21.childrenD_429 line 278
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_429 line 279
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_429 line 280
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_429 line 281
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_429 line 282
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_429 line 283
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_429 line 290
  151. def OAI.SnakyPrototype.Certificate21.required_435_i1 line 295
  152. def OAI.SnakyPrototype.Certificate21.envelope_435_i1 line 296
  153. def OAI.SnakyPrototype.Certificate21.childrenC_435_i1 line 297
  154. def OAI.SnakyPrototype.Certificate21.childrenD_435_i1 line 298
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_435_i1 line 299
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_435_i1 line 300
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_435_i1 line 301
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_435_i1 line 302
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_435_i1 line 303
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_435_i1 line 308
  161. def OAI.SnakyPrototype.Certificate21.required_435_i3 line 313
  162. def OAI.SnakyPrototype.Certificate21.envelope_435_i3 line 314
  163. def OAI.SnakyPrototype.Certificate21.childrenC_435_i3 line 315
  164. def OAI.SnakyPrototype.Certificate21.childrenD_435_i3 line 316
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_435_i3 line 317
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_435_i3 line 318
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_435_i3 line 319
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_435_i3 line 320
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_435_i3 line 321
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_435_i3 line 326
  171. def OAI.SnakyPrototype.Certificate21.required_435_i2 line 331
  172. def OAI.SnakyPrototype.Certificate21.envelope_435_i2 line 332
  173. def OAI.SnakyPrototype.Certificate21.childrenC_435_i2 line 333
  174. def OAI.SnakyPrototype.Certificate21.childrenD_435_i2 line 334
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_435_i2 line 335
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_435_i2 line 336
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_435_i2 line 337
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_435_i2 line 338
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_435_i2 line 339
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_435_i2 line 345
  181. def OAI.SnakyPrototype.Certificate21.required_435_i0 line 350
  182. def OAI.SnakyPrototype.Certificate21.envelope_435_i0 line 351
  183. def OAI.SnakyPrototype.Certificate21.childrenC_435_i0 line 352
  184. def OAI.SnakyPrototype.Certificate21.childrenD_435_i0 line 353
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_435_i0 line 354
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_435_i0 line 355
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_435_i0 line 356
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_435_i0 line 357
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_435_i0 line 358
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_435_i0 line 365
  191. def OAI.SnakyPrototype.Certificate21.required_435 line 370
  192. def OAI.SnakyPrototype.Certificate21.envelope_435 line 371
  193. def OAI.SnakyPrototype.Certificate21.childrenC_435 line 372
  194. def OAI.SnakyPrototype.Certificate21.childrenD_435 line 373
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_435 line 374
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_435 line 375
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_435 line 376
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_435 line 377
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_435 line 378
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_435 line 385
  201. def OAI.SnakyPrototype.Certificate21.height_378_i0 line 390
  202. def OAI.SnakyPrototype.Certificate21.childrenH_378_i0 line 391
  203. theorem OAI.SnakyPrototype.Certificate21.height_exact_378_i0 line 392
  204. theorem OAI.SnakyPrototype.Certificate21.required_origin_378_i0 line 393
  205. theorem OAI.SnakyPrototype.Certificate21.required_exact_378_i0 line 395
  206. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_378_i0 line 399
  207. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_378_i0 line 401
  208. def OAI.SnakyPrototype.Certificate21.checked_378_i0 line 405
  209. def OAI.SnakyPrototype.Certificate21.height_378 line 413
  210. def OAI.SnakyPrototype.Certificate21.childrenH_378 line 414
  211. theorem OAI.SnakyPrototype.Certificate21.height_exact_378 line 415
  212. theorem OAI.SnakyPrototype.Certificate21.required_origin_378 line 416
  213. theorem OAI.SnakyPrototype.Certificate21.required_exact_378 line 418
  214. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_378 line 422
  215. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_378 line 424
  216. def OAI.SnakyPrototype.Certificate21.checked_378 line 428
  217. def OAI.SnakyPrototype.Certificate21.height_384 line 436
  218. def OAI.SnakyPrototype.Certificate21.childrenH_384 line 437
  219. theorem OAI.SnakyPrototype.Certificate21.height_exact_384 line 438
  220. theorem OAI.SnakyPrototype.Certificate21.required_origin_384 line 439
  221. theorem OAI.SnakyPrototype.Certificate21.required_exact_384 line 441
  222. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_384 line 445
  223. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_384 line 447
  224. def OAI.SnakyPrototype.Certificate21.checked_384 line 451
  225. def OAI.SnakyPrototype.Certificate21.height_387 line 459
  226. def OAI.SnakyPrototype.Certificate21.childrenH_387 line 460
  227. theorem OAI.SnakyPrototype.Certificate21.height_exact_387 line 461
  228. theorem OAI.SnakyPrototype.Certificate21.required_origin_387 line 462
  229. theorem OAI.SnakyPrototype.Certificate21.required_exact_387 line 464
  230. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_387 line 468
  231. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_387 line 470
  232. def OAI.SnakyPrototype.Certificate21.checked_387 line 474
  233. def OAI.SnakyPrototype.Certificate21.height_390 line 482
  234. def OAI.SnakyPrototype.Certificate21.childrenH_390 line 483
  235. theorem OAI.SnakyPrototype.Certificate21.height_exact_390 line 484
  236. theorem OAI.SnakyPrototype.Certificate21.required_origin_390 line 485
  237. theorem OAI.SnakyPrototype.Certificate21.required_exact_390 line 487
  238. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_390 line 491
  239. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_390 line 493
  240. def OAI.SnakyPrototype.Certificate21.checked_390 line 497
  241. def OAI.SnakyPrototype.Certificate21.height_392 line 505
  242. def OAI.SnakyPrototype.Certificate21.childrenH_392 line 506
  243. theorem OAI.SnakyPrototype.Certificate21.height_exact_392 line 507
  244. theorem OAI.SnakyPrototype.Certificate21.required_origin_392 line 508
  245. theorem OAI.SnakyPrototype.Certificate21.required_exact_392 line 510
  246. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_392 line 514
  247. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_392 line 516
  248. def OAI.SnakyPrototype.Certificate21.checked_392 line 520
  249. def OAI.SnakyPrototype.Certificate21.height_393 line 528
  250. def OAI.SnakyPrototype.Certificate21.childrenH_393 line 529
  251. theorem OAI.SnakyPrototype.Certificate21.height_exact_393 line 530
  252. theorem OAI.SnakyPrototype.Certificate21.required_origin_393 line 531
  253. theorem OAI.SnakyPrototype.Certificate21.required_exact_393 line 533
  254. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_393 line 537
  255. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_393 line 539
  256. def OAI.SnakyPrototype.Certificate21.checked_393 line 543
  257. def OAI.SnakyPrototype.Certificate21.height_403_i0 line 551
  258. def OAI.SnakyPrototype.Certificate21.childrenH_403_i0 line 552
  259. theorem OAI.SnakyPrototype.Certificate21.height_exact_403_i0 line 553
  260. theorem OAI.SnakyPrototype.Certificate21.required_origin_403_i0 line 554
  261. theorem OAI.SnakyPrototype.Certificate21.required_exact_403_i0 line 556
  262. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_403_i0 line 560
  263. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_403_i0 line 562
  264. def OAI.SnakyPrototype.Certificate21.checked_403_i0 line 566
  265. def OAI.SnakyPrototype.Certificate21.height_403 line 574
  266. def OAI.SnakyPrototype.Certificate21.childrenH_403 line 575
  267. theorem OAI.SnakyPrototype.Certificate21.height_exact_403 line 576
  268. theorem OAI.SnakyPrototype.Certificate21.required_origin_403 line 577
  269. theorem OAI.SnakyPrototype.Certificate21.required_exact_403 line 579
  270. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_403 line 583
  271. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_403 line 585
  272. def OAI.SnakyPrototype.Certificate21.checked_403 line 589
  273. def OAI.SnakyPrototype.Certificate21.height_414 line 597
  274. def OAI.SnakyPrototype.Certificate21.childrenH_414 line 598
  275. theorem OAI.SnakyPrototype.Certificate21.height_exact_414 line 599
  276. theorem OAI.SnakyPrototype.Certificate21.required_origin_414 line 600
  277. theorem OAI.SnakyPrototype.Certificate21.required_exact_414 line 602
  278. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_414 line 606
  279. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_414 line 608
  280. def OAI.SnakyPrototype.Certificate21.checked_414 line 612
  281. def OAI.SnakyPrototype.Certificate21.height_417 line 620
  282. def OAI.SnakyPrototype.Certificate21.childrenH_417 line 621
  283. theorem OAI.SnakyPrototype.Certificate21.height_exact_417 line 622
  284. theorem OAI.SnakyPrototype.Certificate21.required_origin_417 line 623
  285. theorem OAI.SnakyPrototype.Certificate21.required_exact_417 line 625
  286. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_417 line 629
  287. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_417 line 631
  288. def OAI.SnakyPrototype.Certificate21.checked_417 line 635
  289. def OAI.SnakyPrototype.Certificate21.height_423_i0 line 643
  290. def OAI.SnakyPrototype.Certificate21.childrenH_423_i0 line 644
  291. theorem OAI.SnakyPrototype.Certificate21.height_exact_423_i0 line 645
  292. theorem OAI.SnakyPrototype.Certificate21.required_origin_423_i0 line 646
  293. theorem OAI.SnakyPrototype.Certificate21.required_exact_423_i0 line 648
  294. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_423_i0 line 652
  295. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_423_i0 line 654
  296. def OAI.SnakyPrototype.Certificate21.checked_423_i0 line 658
  297. def OAI.SnakyPrototype.Certificate21.height_423 line 666
  298. def OAI.SnakyPrototype.Certificate21.childrenH_423 line 667
  299. theorem OAI.SnakyPrototype.Certificate21.height_exact_423 line 668
  300. theorem OAI.SnakyPrototype.Certificate21.required_origin_423 line 669
  301. theorem OAI.SnakyPrototype.Certificate21.required_exact_423 line 671
  302. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_423 line 675
  303. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_423 line 677
  304. def OAI.SnakyPrototype.Certificate21.checked_423 line 681
  305. def OAI.SnakyPrototype.Certificate21.height_429_i0 line 689
  306. def OAI.SnakyPrototype.Certificate21.childrenH_429_i0 line 690
  307. theorem OAI.SnakyPrototype.Certificate21.height_exact_429_i0 line 691
  308. theorem OAI.SnakyPrototype.Certificate21.required_origin_429_i0 line 692
  309. theorem OAI.SnakyPrototype.Certificate21.required_exact_429_i0 line 694
  310. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_429_i0 line 698
  311. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_429_i0 line 700
  312. def OAI.SnakyPrototype.Certificate21.checked_429_i0 line 704
  313. def OAI.SnakyPrototype.Certificate21.height_429 line 712
  314. def OAI.SnakyPrototype.Certificate21.childrenH_429 line 713
  315. theorem OAI.SnakyPrototype.Certificate21.height_exact_429 line 714
  316. theorem OAI.SnakyPrototype.Certificate21.required_origin_429 line 715
  317. theorem OAI.SnakyPrototype.Certificate21.required_exact_429 line 717
  318. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_429 line 721
  319. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_429 line 723
  320. def OAI.SnakyPrototype.Certificate21.checked_429 line 727
  321. def OAI.SnakyPrototype.Certificate21.height_435_i1 line 735
  322. def OAI.SnakyPrototype.Certificate21.childrenH_435_i1 line 736
  323. theorem OAI.SnakyPrototype.Certificate21.height_exact_435_i1 line 737
  324. theorem OAI.SnakyPrototype.Certificate21.required_origin_435_i1 line 738
  325. theorem OAI.SnakyPrototype.Certificate21.required_exact_435_i1 line 740
  326. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_435_i1 line 744
  327. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_435_i1 line 746
  328. def OAI.SnakyPrototype.Certificate21.checked_435_i1 line 750
  329. def OAI.SnakyPrototype.Certificate21.height_435_i3 line 758
  330. def OAI.SnakyPrototype.Certificate21.childrenH_435_i3 line 759
  331. theorem OAI.SnakyPrototype.Certificate21.height_exact_435_i3 line 760
  332. theorem OAI.SnakyPrototype.Certificate21.required_origin_435_i3 line 761
  333. theorem OAI.SnakyPrototype.Certificate21.required_exact_435_i3 line 763
  334. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_435_i3 line 767
  335. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_435_i3 line 769
  336. def OAI.SnakyPrototype.Certificate21.checked_435_i3 line 773
  337. def OAI.SnakyPrototype.Certificate21.height_435_i2 line 781
  338. def OAI.SnakyPrototype.Certificate21.childrenH_435_i2 line 782
  339. theorem OAI.SnakyPrototype.Certificate21.height_exact_435_i2 line 783
  340. theorem OAI.SnakyPrototype.Certificate21.required_origin_435_i2 line 784
  341. theorem OAI.SnakyPrototype.Certificate21.required_exact_435_i2 line 786
  342. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_435_i2 line 790
  343. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_435_i2 line 792
  344. def OAI.SnakyPrototype.Certificate21.checked_435_i2 line 796
  345. def OAI.SnakyPrototype.Certificate21.height_435_i0 line 804
  346. def OAI.SnakyPrototype.Certificate21.childrenH_435_i0 line 805
  347. theorem OAI.SnakyPrototype.Certificate21.height_exact_435_i0 line 806
  348. theorem OAI.SnakyPrototype.Certificate21.required_origin_435_i0 line 807
  349. theorem OAI.SnakyPrototype.Certificate21.required_exact_435_i0 line 809
  350. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_435_i0 line 813
  351. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_435_i0 line 815
  352. def OAI.SnakyPrototype.Certificate21.checked_435_i0 line 819
  353. def OAI.SnakyPrototype.Certificate21.height_435 line 827
  354. def OAI.SnakyPrototype.Certificate21.childrenH_435 line 828
  355. theorem OAI.SnakyPrototype.Certificate21.height_exact_435 line 829
  356. theorem OAI.SnakyPrototype.Certificate21.required_origin_435 line 830
  357. theorem OAI.SnakyPrototype.Certificate21.required_exact_435 line 832
  358. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_435 line 836
  359. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_435 line 838
  360. def OAI.SnakyPrototype.Certificate21.checked_435 line 842