OAI/GameTheory/SnakyTwentyOne/Cards/Height11Part02.lean

GitHub source file

378 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_517_i0 line 34
  2. def OAI.SnakyPrototype.Certificate21.envelope_517_i0 line 35
  3. def OAI.SnakyPrototype.Certificate21.childrenC_517_i0 line 36
  4. def OAI.SnakyPrototype.Certificate21.childrenD_517_i0 line 37
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_517_i0 line 38
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_517_i0 line 39
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_517_i0 line 40
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_517_i0 line 41
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_517_i0 line 42
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_517_i0 line 47
  11. def OAI.SnakyPrototype.Certificate21.required_517_i2 line 52
  12. def OAI.SnakyPrototype.Certificate21.envelope_517_i2 line 53
  13. def OAI.SnakyPrototype.Certificate21.childrenC_517_i2 line 54
  14. def OAI.SnakyPrototype.Certificate21.childrenD_517_i2 line 55
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_517_i2 line 56
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_517_i2 line 57
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_517_i2 line 58
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_517_i2 line 59
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_517_i2 line 60
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_517_i2 line 68
  21. def OAI.SnakyPrototype.Certificate21.required_517_i1 line 73
  22. def OAI.SnakyPrototype.Certificate21.envelope_517_i1 line 74
  23. def OAI.SnakyPrototype.Certificate21.childrenC_517_i1 line 75
  24. def OAI.SnakyPrototype.Certificate21.childrenD_517_i1 line 76
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_517_i1 line 77
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_517_i1 line 78
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_517_i1 line 79
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_517_i1 line 80
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_517_i1 line 81
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_517_i1 line 88
  31. def OAI.SnakyPrototype.Certificate21.required_517_i4 line 93
  32. def OAI.SnakyPrototype.Certificate21.envelope_517_i4 line 94
  33. def OAI.SnakyPrototype.Certificate21.childrenC_517_i4 line 95
  34. def OAI.SnakyPrototype.Certificate21.childrenD_517_i4 line 96
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_517_i4 line 97
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_517_i4 line 98
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_517_i4 line 99
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_517_i4 line 100
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_517_i4 line 101
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_517_i4 line 108
  41. def OAI.SnakyPrototype.Certificate21.required_517_i3 line 113
  42. def OAI.SnakyPrototype.Certificate21.envelope_517_i3 line 114
  43. def OAI.SnakyPrototype.Certificate21.childrenC_517_i3 line 115
  44. def OAI.SnakyPrototype.Certificate21.childrenD_517_i3 line 116
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_517_i3 line 117
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_517_i3 line 118
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_517_i3 line 119
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_517_i3 line 120
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_517_i3 line 121
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_517_i3 line 128
  51. def OAI.SnakyPrototype.Certificate21.required_517 line 133
  52. def OAI.SnakyPrototype.Certificate21.envelope_517 line 134
  53. def OAI.SnakyPrototype.Certificate21.childrenC_517 line 135
  54. def OAI.SnakyPrototype.Certificate21.childrenD_517 line 136
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_517 line 137
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_517 line 138
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_517 line 139
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_517 line 140
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_517 line 141
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_517 line 148
  61. def OAI.SnakyPrototype.Certificate21.required_527_i0 line 153
  62. def OAI.SnakyPrototype.Certificate21.envelope_527_i0 line 154
  63. def OAI.SnakyPrototype.Certificate21.childrenC_527_i0 line 155
  64. def OAI.SnakyPrototype.Certificate21.childrenD_527_i0 line 156
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_527_i0 line 157
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_527_i0 line 158
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_527_i0 line 159
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_527_i0 line 160
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_527_i0 line 161
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_527_i0 line 166
  71. def OAI.SnakyPrototype.Certificate21.required_527_i2 line 171
  72. def OAI.SnakyPrototype.Certificate21.envelope_527_i2 line 172
  73. def OAI.SnakyPrototype.Certificate21.childrenC_527_i2 line 173
  74. def OAI.SnakyPrototype.Certificate21.childrenD_527_i2 line 174
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_527_i2 line 175
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_527_i2 line 176
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_527_i2 line 177
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_527_i2 line 178
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_527_i2 line 179
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_527_i2 line 188
  81. def OAI.SnakyPrototype.Certificate21.required_527_i1 line 193
  82. def OAI.SnakyPrototype.Certificate21.envelope_527_i1 line 194
  83. def OAI.SnakyPrototype.Certificate21.childrenC_527_i1 line 195
  84. def OAI.SnakyPrototype.Certificate21.childrenD_527_i1 line 196
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_527_i1 line 197
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_527_i1 line 198
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_527_i1 line 199
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_527_i1 line 200
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_527_i1 line 201
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_527_i1 line 207
  91. def OAI.SnakyPrototype.Certificate21.required_527 line 212
  92. def OAI.SnakyPrototype.Certificate21.envelope_527 line 213
  93. def OAI.SnakyPrototype.Certificate21.childrenC_527 line 214
  94. def OAI.SnakyPrototype.Certificate21.childrenD_527 line 215
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_527 line 216
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_527 line 217
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_527 line 218
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_527 line 219
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_527 line 220
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_527 line 227
  101. def OAI.SnakyPrototype.Certificate21.required_550 line 232
  102. def OAI.SnakyPrototype.Certificate21.envelope_550 line 233
  103. def OAI.SnakyPrototype.Certificate21.childrenC_550 line 234
  104. def OAI.SnakyPrototype.Certificate21.childrenD_550 line 235
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_550 line 236
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_550 line 237
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_550 line 238
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_550 line 239
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_550 line 240
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_550 line 248
  111. def OAI.SnakyPrototype.Certificate21.required_567_i4 line 253
  112. def OAI.SnakyPrototype.Certificate21.envelope_567_i4 line 254
  113. def OAI.SnakyPrototype.Certificate21.childrenC_567_i4 line 255
  114. def OAI.SnakyPrototype.Certificate21.childrenD_567_i4 line 256
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_567_i4 line 257
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_567_i4 line 258
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_567_i4 line 259
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_567_i4 line 260
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_567_i4 line 261
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_567_i4 line 266
  121. def OAI.SnakyPrototype.Certificate21.required_567_i3 line 271
  122. def OAI.SnakyPrototype.Certificate21.envelope_567_i3 line 272
  123. def OAI.SnakyPrototype.Certificate21.childrenC_567_i3 line 273
  124. def OAI.SnakyPrototype.Certificate21.childrenD_567_i3 line 274
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_567_i3 line 275
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_567_i3 line 276
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_567_i3 line 277
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_567_i3 line 278
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_567_i3 line 279
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_567_i3 line 285
  131. def OAI.SnakyPrototype.Certificate21.required_567_i2 line 290
  132. def OAI.SnakyPrototype.Certificate21.envelope_567_i2 line 291
  133. def OAI.SnakyPrototype.Certificate21.childrenC_567_i2 line 292
  134. def OAI.SnakyPrototype.Certificate21.childrenD_567_i2 line 293
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_567_i2 line 294
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_567_i2 line 295
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_567_i2 line 296
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_567_i2 line 297
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_567_i2 line 298
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_567_i2 line 303
  141. def OAI.SnakyPrototype.Certificate21.required_567_i1 line 308
  142. def OAI.SnakyPrototype.Certificate21.envelope_567_i1 line 309
  143. def OAI.SnakyPrototype.Certificate21.childrenC_567_i1 line 310
  144. def OAI.SnakyPrototype.Certificate21.childrenD_567_i1 line 311
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_567_i1 line 312
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_567_i1 line 313
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_567_i1 line 314
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_567_i1 line 315
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_567_i1 line 316
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_567_i1 line 322
  151. def OAI.SnakyPrototype.Certificate21.required_567_i0 line 327
  152. def OAI.SnakyPrototype.Certificate21.envelope_567_i0 line 328
  153. def OAI.SnakyPrototype.Certificate21.childrenC_567_i0 line 329
  154. def OAI.SnakyPrototype.Certificate21.childrenD_567_i0 line 330
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_567_i0 line 331
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_567_i0 line 332
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_567_i0 line 333
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_567_i0 line 334
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_567_i0 line 335
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_567_i0 line 345
  161. def OAI.SnakyPrototype.Certificate21.required_567 line 350
  162. def OAI.SnakyPrototype.Certificate21.envelope_567 line 351
  163. def OAI.SnakyPrototype.Certificate21.childrenC_567 line 352
  164. def OAI.SnakyPrototype.Certificate21.childrenD_567 line 353
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_567 line 354
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_567 line 355
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_567 line 356
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_567 line 357
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_567 line 358
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_567 line 366
  171. def OAI.SnakyPrototype.Certificate21.required_579 line 371
  172. def OAI.SnakyPrototype.Certificate21.envelope_579 line 372
  173. def OAI.SnakyPrototype.Certificate21.childrenC_579 line 373
  174. def OAI.SnakyPrototype.Certificate21.childrenD_579 line 374
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_579 line 375
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_579 line 376
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_579 line 377
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_579 line 378
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_579 line 379
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_579 line 391
  181. def OAI.SnakyPrototype.Certificate21.required_581 line 396
  182. def OAI.SnakyPrototype.Certificate21.envelope_581 line 397
  183. def OAI.SnakyPrototype.Certificate21.childrenC_581 line 398
  184. def OAI.SnakyPrototype.Certificate21.childrenD_581 line 399
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_581 line 400
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_581 line 401
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_581 line 402
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_581 line 403
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_581 line 404
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_581 line 413
  191. def OAI.SnakyPrototype.Certificate21.required_586 line 418
  192. def OAI.SnakyPrototype.Certificate21.envelope_586 line 419
  193. def OAI.SnakyPrototype.Certificate21.childrenC_586 line 420
  194. def OAI.SnakyPrototype.Certificate21.childrenD_586 line 421
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_586 line 422
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_586 line 423
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_586 line 424
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_586 line 425
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_586 line 426
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_586 line 432
  201. def OAI.SnakyPrototype.Certificate21.required_589 line 437
  202. def OAI.SnakyPrototype.Certificate21.envelope_589 line 438
  203. def OAI.SnakyPrototype.Certificate21.childrenC_589 line 439
  204. def OAI.SnakyPrototype.Certificate21.childrenD_589 line 440
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_589 line 441
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_589 line 442
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_589 line 443
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_589 line 444
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_589 line 445
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_589 line 452
  211. def OAI.SnakyPrototype.Certificate21.height_517_i0 line 457
  212. def OAI.SnakyPrototype.Certificate21.childrenH_517_i0 line 458
  213. theorem OAI.SnakyPrototype.Certificate21.height_exact_517_i0 line 459
  214. theorem OAI.SnakyPrototype.Certificate21.required_origin_517_i0 line 460
  215. theorem OAI.SnakyPrototype.Certificate21.required_exact_517_i0 line 462
  216. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_517_i0 line 466
  217. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_517_i0 line 468
  218. def OAI.SnakyPrototype.Certificate21.checked_517_i0 line 472
  219. def OAI.SnakyPrototype.Certificate21.height_517_i2 line 480
  220. def OAI.SnakyPrototype.Certificate21.childrenH_517_i2 line 481
  221. theorem OAI.SnakyPrototype.Certificate21.height_exact_517_i2 line 482
  222. theorem OAI.SnakyPrototype.Certificate21.required_origin_517_i2 line 483
  223. theorem OAI.SnakyPrototype.Certificate21.required_exact_517_i2 line 485
  224. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_517_i2 line 489
  225. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_517_i2 line 491
  226. def OAI.SnakyPrototype.Certificate21.checked_517_i2 line 495
  227. def OAI.SnakyPrototype.Certificate21.height_517_i1 line 503
  228. def OAI.SnakyPrototype.Certificate21.childrenH_517_i1 line 504
  229. theorem OAI.SnakyPrototype.Certificate21.height_exact_517_i1 line 505
  230. theorem OAI.SnakyPrototype.Certificate21.required_origin_517_i1 line 506
  231. theorem OAI.SnakyPrototype.Certificate21.required_exact_517_i1 line 508
  232. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_517_i1 line 512
  233. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_517_i1 line 514
  234. def OAI.SnakyPrototype.Certificate21.checked_517_i1 line 518
  235. def OAI.SnakyPrototype.Certificate21.height_517_i4 line 526
  236. def OAI.SnakyPrototype.Certificate21.childrenH_517_i4 line 527
  237. theorem OAI.SnakyPrototype.Certificate21.height_exact_517_i4 line 528
  238. theorem OAI.SnakyPrototype.Certificate21.required_origin_517_i4 line 529
  239. theorem OAI.SnakyPrototype.Certificate21.required_exact_517_i4 line 531
  240. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_517_i4 line 535
  241. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_517_i4 line 537
  242. def OAI.SnakyPrototype.Certificate21.checked_517_i4 line 541
  243. def OAI.SnakyPrototype.Certificate21.height_517_i3 line 549
  244. def OAI.SnakyPrototype.Certificate21.childrenH_517_i3 line 550
  245. theorem OAI.SnakyPrototype.Certificate21.height_exact_517_i3 line 551
  246. theorem OAI.SnakyPrototype.Certificate21.required_origin_517_i3 line 552
  247. theorem OAI.SnakyPrototype.Certificate21.required_exact_517_i3 line 554
  248. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_517_i3 line 558
  249. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_517_i3 line 560
  250. def OAI.SnakyPrototype.Certificate21.checked_517_i3 line 564
  251. def OAI.SnakyPrototype.Certificate21.height_517 line 572
  252. def OAI.SnakyPrototype.Certificate21.childrenH_517 line 573
  253. theorem OAI.SnakyPrototype.Certificate21.height_exact_517 line 574
  254. theorem OAI.SnakyPrototype.Certificate21.required_origin_517 line 575
  255. theorem OAI.SnakyPrototype.Certificate21.required_exact_517 line 577
  256. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_517 line 581
  257. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_517 line 583
  258. def OAI.SnakyPrototype.Certificate21.checked_517 line 587
  259. def OAI.SnakyPrototype.Certificate21.height_527_i0 line 595
  260. def OAI.SnakyPrototype.Certificate21.childrenH_527_i0 line 596
  261. theorem OAI.SnakyPrototype.Certificate21.height_exact_527_i0 line 597
  262. theorem OAI.SnakyPrototype.Certificate21.required_origin_527_i0 line 598
  263. theorem OAI.SnakyPrototype.Certificate21.required_exact_527_i0 line 600
  264. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_527_i0 line 604
  265. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_527_i0 line 606
  266. def OAI.SnakyPrototype.Certificate21.checked_527_i0 line 610
  267. def OAI.SnakyPrototype.Certificate21.height_527_i2 line 618
  268. def OAI.SnakyPrototype.Certificate21.childrenH_527_i2 line 619
  269. theorem OAI.SnakyPrototype.Certificate21.height_exact_527_i2 line 620
  270. theorem OAI.SnakyPrototype.Certificate21.required_origin_527_i2 line 621
  271. theorem OAI.SnakyPrototype.Certificate21.required_exact_527_i2 line 623
  272. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_527_i2 line 627
  273. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_527_i2 line 629
  274. def OAI.SnakyPrototype.Certificate21.checked_527_i2 line 633
  275. def OAI.SnakyPrototype.Certificate21.height_527_i1 line 641
  276. def OAI.SnakyPrototype.Certificate21.childrenH_527_i1 line 642
  277. theorem OAI.SnakyPrototype.Certificate21.height_exact_527_i1 line 643
  278. theorem OAI.SnakyPrototype.Certificate21.required_origin_527_i1 line 644
  279. theorem OAI.SnakyPrototype.Certificate21.required_exact_527_i1 line 646
  280. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_527_i1 line 650
  281. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_527_i1 line 652
  282. def OAI.SnakyPrototype.Certificate21.checked_527_i1 line 656
  283. def OAI.SnakyPrototype.Certificate21.height_527 line 664
  284. def OAI.SnakyPrototype.Certificate21.childrenH_527 line 665
  285. theorem OAI.SnakyPrototype.Certificate21.height_exact_527 line 666
  286. theorem OAI.SnakyPrototype.Certificate21.required_origin_527 line 667
  287. theorem OAI.SnakyPrototype.Certificate21.required_exact_527 line 669
  288. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_527 line 673
  289. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_527 line 675
  290. def OAI.SnakyPrototype.Certificate21.checked_527 line 679
  291. def OAI.SnakyPrototype.Certificate21.height_550 line 687
  292. def OAI.SnakyPrototype.Certificate21.childrenH_550 line 688
  293. theorem OAI.SnakyPrototype.Certificate21.height_exact_550 line 689
  294. theorem OAI.SnakyPrototype.Certificate21.required_origin_550 line 690
  295. theorem OAI.SnakyPrototype.Certificate21.required_exact_550 line 692
  296. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_550 line 696
  297. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_550 line 698
  298. def OAI.SnakyPrototype.Certificate21.checked_550 line 702
  299. def OAI.SnakyPrototype.Certificate21.height_567_i4 line 710
  300. def OAI.SnakyPrototype.Certificate21.childrenH_567_i4 line 711
  301. theorem OAI.SnakyPrototype.Certificate21.height_exact_567_i4 line 712
  302. theorem OAI.SnakyPrototype.Certificate21.required_origin_567_i4 line 713
  303. theorem OAI.SnakyPrototype.Certificate21.required_exact_567_i4 line 715
  304. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_567_i4 line 719
  305. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_567_i4 line 721
  306. def OAI.SnakyPrototype.Certificate21.checked_567_i4 line 725
  307. def OAI.SnakyPrototype.Certificate21.height_567_i3 line 733
  308. def OAI.SnakyPrototype.Certificate21.childrenH_567_i3 line 734
  309. theorem OAI.SnakyPrototype.Certificate21.height_exact_567_i3 line 735
  310. theorem OAI.SnakyPrototype.Certificate21.required_origin_567_i3 line 736
  311. theorem OAI.SnakyPrototype.Certificate21.required_exact_567_i3 line 738
  312. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_567_i3 line 742
  313. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_567_i3 line 744
  314. def OAI.SnakyPrototype.Certificate21.checked_567_i3 line 748
  315. def OAI.SnakyPrototype.Certificate21.height_567_i2 line 756
  316. def OAI.SnakyPrototype.Certificate21.childrenH_567_i2 line 757
  317. theorem OAI.SnakyPrototype.Certificate21.height_exact_567_i2 line 758
  318. theorem OAI.SnakyPrototype.Certificate21.required_origin_567_i2 line 759
  319. theorem OAI.SnakyPrototype.Certificate21.required_exact_567_i2 line 761
  320. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_567_i2 line 765
  321. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_567_i2 line 767
  322. def OAI.SnakyPrototype.Certificate21.checked_567_i2 line 771
  323. def OAI.SnakyPrototype.Certificate21.height_567_i1 line 779
  324. def OAI.SnakyPrototype.Certificate21.childrenH_567_i1 line 780
  325. theorem OAI.SnakyPrototype.Certificate21.height_exact_567_i1 line 781
  326. theorem OAI.SnakyPrototype.Certificate21.required_origin_567_i1 line 782
  327. theorem OAI.SnakyPrototype.Certificate21.required_exact_567_i1 line 784
  328. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_567_i1 line 788
  329. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_567_i1 line 790
  330. def OAI.SnakyPrototype.Certificate21.checked_567_i1 line 794
  331. def OAI.SnakyPrototype.Certificate21.height_567_i0 line 802
  332. def OAI.SnakyPrototype.Certificate21.childrenH_567_i0 line 803
  333. theorem OAI.SnakyPrototype.Certificate21.height_exact_567_i0 line 804
  334. theorem OAI.SnakyPrototype.Certificate21.required_origin_567_i0 line 805
  335. theorem OAI.SnakyPrototype.Certificate21.required_exact_567_i0 line 807
  336. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_567_i0 line 811
  337. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_567_i0 line 813
  338. def OAI.SnakyPrototype.Certificate21.checked_567_i0 line 817
  339. def OAI.SnakyPrototype.Certificate21.height_567 line 825
  340. def OAI.SnakyPrototype.Certificate21.childrenH_567 line 826
  341. theorem OAI.SnakyPrototype.Certificate21.height_exact_567 line 827
  342. theorem OAI.SnakyPrototype.Certificate21.required_origin_567 line 828
  343. theorem OAI.SnakyPrototype.Certificate21.required_exact_567 line 830
  344. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_567 line 834
  345. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_567 line 836
  346. def OAI.SnakyPrototype.Certificate21.checked_567 line 840
  347. def OAI.SnakyPrototype.Certificate21.height_579 line 848
  348. def OAI.SnakyPrototype.Certificate21.childrenH_579 line 849
  349. theorem OAI.SnakyPrototype.Certificate21.height_exact_579 line 850
  350. theorem OAI.SnakyPrototype.Certificate21.required_origin_579 line 851
  351. theorem OAI.SnakyPrototype.Certificate21.required_exact_579 line 853
  352. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_579 line 857
  353. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_579 line 859
  354. def OAI.SnakyPrototype.Certificate21.checked_579 line 863
  355. def OAI.SnakyPrototype.Certificate21.height_581 line 871
  356. def OAI.SnakyPrototype.Certificate21.childrenH_581 line 872
  357. theorem OAI.SnakyPrototype.Certificate21.height_exact_581 line 873
  358. theorem OAI.SnakyPrototype.Certificate21.required_origin_581 line 874
  359. theorem OAI.SnakyPrototype.Certificate21.required_exact_581 line 876
  360. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_581 line 880
  361. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_581 line 882
  362. def OAI.SnakyPrototype.Certificate21.checked_581 line 886
  363. def OAI.SnakyPrototype.Certificate21.height_586 line 894
  364. def OAI.SnakyPrototype.Certificate21.childrenH_586 line 895
  365. theorem OAI.SnakyPrototype.Certificate21.height_exact_586 line 896
  366. theorem OAI.SnakyPrototype.Certificate21.required_origin_586 line 897
  367. theorem OAI.SnakyPrototype.Certificate21.required_exact_586 line 899
  368. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_586 line 903
  369. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_586 line 905
  370. def OAI.SnakyPrototype.Certificate21.checked_586 line 909
  371. def OAI.SnakyPrototype.Certificate21.height_589 line 917
  372. def OAI.SnakyPrototype.Certificate21.childrenH_589 line 918
  373. theorem OAI.SnakyPrototype.Certificate21.height_exact_589 line 919
  374. theorem OAI.SnakyPrototype.Certificate21.required_origin_589 line 920
  375. theorem OAI.SnakyPrototype.Certificate21.required_exact_589 line 922
  376. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_589 line 926
  377. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_589 line 928
  378. def OAI.SnakyPrototype.Certificate21.checked_589 line 932