OAI/GameTheory/SnakyTwentyOne/Cards/Height10Part05.lean

GitHub source file

378 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_594_i0 line 26
  2. def OAI.SnakyPrototype.Certificate21.envelope_594_i0 line 27
  3. def OAI.SnakyPrototype.Certificate21.childrenC_594_i0 line 28
  4. def OAI.SnakyPrototype.Certificate21.childrenD_594_i0 line 29
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_594_i0 line 30
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_594_i0 line 31
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_594_i0 line 32
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_594_i0 line 33
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_594_i0 line 34
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_594_i0 line 39
  11. def OAI.SnakyPrototype.Certificate21.required_594_i7 line 44
  12. def OAI.SnakyPrototype.Certificate21.envelope_594_i7 line 45
  13. def OAI.SnakyPrototype.Certificate21.childrenC_594_i7 line 46
  14. def OAI.SnakyPrototype.Certificate21.childrenD_594_i7 line 47
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_594_i7 line 48
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_594_i7 line 49
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_594_i7 line 50
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_594_i7 line 51
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_594_i7 line 52
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_594_i7 line 57
  21. def OAI.SnakyPrototype.Certificate21.required_594_i6 line 62
  22. def OAI.SnakyPrototype.Certificate21.envelope_594_i6 line 63
  23. def OAI.SnakyPrototype.Certificate21.childrenC_594_i6 line 64
  24. def OAI.SnakyPrototype.Certificate21.childrenD_594_i6 line 65
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_594_i6 line 66
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_594_i6 line 67
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_594_i6 line 68
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_594_i6 line 69
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_594_i6 line 70
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_594_i6 line 75
  31. def OAI.SnakyPrototype.Certificate21.required_594_i5 line 80
  32. def OAI.SnakyPrototype.Certificate21.envelope_594_i5 line 81
  33. def OAI.SnakyPrototype.Certificate21.childrenC_594_i5 line 82
  34. def OAI.SnakyPrototype.Certificate21.childrenD_594_i5 line 83
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_594_i5 line 84
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_594_i5 line 85
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_594_i5 line 86
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_594_i5 line 87
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_594_i5 line 88
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_594_i5 line 93
  41. def OAI.SnakyPrototype.Certificate21.required_594_i4 line 98
  42. def OAI.SnakyPrototype.Certificate21.envelope_594_i4 line 99
  43. def OAI.SnakyPrototype.Certificate21.childrenC_594_i4 line 100
  44. def OAI.SnakyPrototype.Certificate21.childrenD_594_i4 line 101
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_594_i4 line 102
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_594_i4 line 103
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_594_i4 line 104
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_594_i4 line 105
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_594_i4 line 106
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_594_i4 line 111
  51. def OAI.SnakyPrototype.Certificate21.required_594_i3 line 116
  52. def OAI.SnakyPrototype.Certificate21.envelope_594_i3 line 117
  53. def OAI.SnakyPrototype.Certificate21.childrenC_594_i3 line 118
  54. def OAI.SnakyPrototype.Certificate21.childrenD_594_i3 line 119
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_594_i3 line 120
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_594_i3 line 121
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_594_i3 line 122
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_594_i3 line 123
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_594_i3 line 124
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_594_i3 line 130
  61. def OAI.SnakyPrototype.Certificate21.required_594_i2 line 135
  62. def OAI.SnakyPrototype.Certificate21.envelope_594_i2 line 136
  63. def OAI.SnakyPrototype.Certificate21.childrenC_594_i2 line 137
  64. def OAI.SnakyPrototype.Certificate21.childrenD_594_i2 line 138
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_594_i2 line 139
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_594_i2 line 140
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_594_i2 line 141
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_594_i2 line 142
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_594_i2 line 143
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_594_i2 line 148
  71. def OAI.SnakyPrototype.Certificate21.required_594_i8 line 153
  72. def OAI.SnakyPrototype.Certificate21.envelope_594_i8 line 154
  73. def OAI.SnakyPrototype.Certificate21.childrenC_594_i8 line 155
  74. def OAI.SnakyPrototype.Certificate21.childrenD_594_i8 line 156
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_594_i8 line 157
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_594_i8 line 158
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_594_i8 line 159
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_594_i8 line 160
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_594_i8 line 161
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_594_i8 line 166
  81. def OAI.SnakyPrototype.Certificate21.required_594_i1 line 171
  82. def OAI.SnakyPrototype.Certificate21.envelope_594_i1 line 172
  83. def OAI.SnakyPrototype.Certificate21.childrenC_594_i1 line 173
  84. def OAI.SnakyPrototype.Certificate21.childrenD_594_i1 line 174
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_594_i1 line 175
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_594_i1 line 176
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_594_i1 line 177
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_594_i1 line 178
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_594_i1 line 179
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_594_i1 line 187
  91. def OAI.SnakyPrototype.Certificate21.required_594 line 192
  92. def OAI.SnakyPrototype.Certificate21.envelope_594 line 193
  93. def OAI.SnakyPrototype.Certificate21.childrenC_594 line 194
  94. def OAI.SnakyPrototype.Certificate21.childrenD_594 line 195
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_594 line 196
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_594 line 197
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_594 line 198
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_594 line 199
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_594 line 200
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_594 line 206
  101. def OAI.SnakyPrototype.Certificate21.required_608_i1 line 211
  102. def OAI.SnakyPrototype.Certificate21.envelope_608_i1 line 212
  103. def OAI.SnakyPrototype.Certificate21.childrenC_608_i1 line 213
  104. def OAI.SnakyPrototype.Certificate21.childrenD_608_i1 line 214
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_608_i1 line 215
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_608_i1 line 216
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_608_i1 line 217
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_608_i1 line 218
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_608_i1 line 219
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_608_i1 line 224
  111. def OAI.SnakyPrototype.Certificate21.required_608_i2 line 229
  112. def OAI.SnakyPrototype.Certificate21.envelope_608_i2 line 230
  113. def OAI.SnakyPrototype.Certificate21.childrenC_608_i2 line 231
  114. def OAI.SnakyPrototype.Certificate21.childrenD_608_i2 line 232
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_608_i2 line 233
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_608_i2 line 234
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_608_i2 line 235
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_608_i2 line 236
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_608_i2 line 237
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_608_i2 line 242
  121. def OAI.SnakyPrototype.Certificate21.required_608_i3 line 247
  122. def OAI.SnakyPrototype.Certificate21.envelope_608_i3 line 248
  123. def OAI.SnakyPrototype.Certificate21.childrenC_608_i3 line 249
  124. def OAI.SnakyPrototype.Certificate21.childrenD_608_i3 line 250
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_608_i3 line 251
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_608_i3 line 252
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_608_i3 line 253
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_608_i3 line 254
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_608_i3 line 255
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_608_i3 line 260
  131. def OAI.SnakyPrototype.Certificate21.required_608_i0 line 265
  132. def OAI.SnakyPrototype.Certificate21.envelope_608_i0 line 266
  133. def OAI.SnakyPrototype.Certificate21.childrenC_608_i0 line 267
  134. def OAI.SnakyPrototype.Certificate21.childrenD_608_i0 line 268
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_608_i0 line 269
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_608_i0 line 270
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_608_i0 line 271
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_608_i0 line 272
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_608_i0 line 273
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_608_i0 line 279
  141. def OAI.SnakyPrototype.Certificate21.required_608 line 284
  142. def OAI.SnakyPrototype.Certificate21.envelope_608 line 285
  143. def OAI.SnakyPrototype.Certificate21.childrenC_608 line 286
  144. def OAI.SnakyPrototype.Certificate21.childrenD_608 line 287
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_608 line 288
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_608 line 289
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_608 line 290
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_608 line 291
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_608 line 292
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_608 line 301
  151. def OAI.SnakyPrototype.Certificate21.required_616_i1 line 306
  152. def OAI.SnakyPrototype.Certificate21.envelope_616_i1 line 307
  153. def OAI.SnakyPrototype.Certificate21.childrenC_616_i1 line 308
  154. def OAI.SnakyPrototype.Certificate21.childrenD_616_i1 line 309
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_616_i1 line 310
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_616_i1 line 311
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_616_i1 line 312
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_616_i1 line 313
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_616_i1 line 314
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_616_i1 line 319
  161. def OAI.SnakyPrototype.Certificate21.required_616_i0 line 324
  162. def OAI.SnakyPrototype.Certificate21.envelope_616_i0 line 325
  163. def OAI.SnakyPrototype.Certificate21.childrenC_616_i0 line 326
  164. def OAI.SnakyPrototype.Certificate21.childrenD_616_i0 line 327
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_616_i0 line 328
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_616_i0 line 329
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_616_i0 line 330
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_616_i0 line 331
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_616_i0 line 332
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_616_i0 line 338
  171. def OAI.SnakyPrototype.Certificate21.required_616 line 343
  172. def OAI.SnakyPrototype.Certificate21.envelope_616 line 344
  173. def OAI.SnakyPrototype.Certificate21.childrenC_616 line 345
  174. def OAI.SnakyPrototype.Certificate21.childrenD_616 line 346
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_616 line 347
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_616 line 348
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_616 line 349
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_616 line 350
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_616 line 351
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_616 line 361
  181. def OAI.SnakyPrototype.Certificate21.required_631_i1 line 366
  182. def OAI.SnakyPrototype.Certificate21.envelope_631_i1 line 367
  183. def OAI.SnakyPrototype.Certificate21.childrenC_631_i1 line 368
  184. def OAI.SnakyPrototype.Certificate21.childrenD_631_i1 line 369
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_631_i1 line 370
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_631_i1 line 371
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_631_i1 line 372
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_631_i1 line 373
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_631_i1 line 374
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_631_i1 line 379
  191. def OAI.SnakyPrototype.Certificate21.required_631_i0 line 384
  192. def OAI.SnakyPrototype.Certificate21.envelope_631_i0 line 385
  193. def OAI.SnakyPrototype.Certificate21.childrenC_631_i0 line 386
  194. def OAI.SnakyPrototype.Certificate21.childrenD_631_i0 line 387
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_631_i0 line 388
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_631_i0 line 389
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_631_i0 line 390
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_631_i0 line 391
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_631_i0 line 392
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_631_i0 line 398
  201. def OAI.SnakyPrototype.Certificate21.required_631 line 403
  202. def OAI.SnakyPrototype.Certificate21.envelope_631 line 404
  203. def OAI.SnakyPrototype.Certificate21.childrenC_631 line 405
  204. def OAI.SnakyPrototype.Certificate21.childrenD_631 line 406
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_631 line 407
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_631 line 408
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_631 line 409
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_631 line 410
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_631 line 411
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_631 line 418
  211. def OAI.SnakyPrototype.Certificate21.height_594_i0 line 423
  212. def OAI.SnakyPrototype.Certificate21.childrenH_594_i0 line 424
  213. theorem OAI.SnakyPrototype.Certificate21.height_exact_594_i0 line 425
  214. theorem OAI.SnakyPrototype.Certificate21.required_origin_594_i0 line 426
  215. theorem OAI.SnakyPrototype.Certificate21.required_exact_594_i0 line 428
  216. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_594_i0 line 432
  217. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_594_i0 line 434
  218. def OAI.SnakyPrototype.Certificate21.checked_594_i0 line 438
  219. def OAI.SnakyPrototype.Certificate21.height_594_i7 line 446
  220. def OAI.SnakyPrototype.Certificate21.childrenH_594_i7 line 447
  221. theorem OAI.SnakyPrototype.Certificate21.height_exact_594_i7 line 448
  222. theorem OAI.SnakyPrototype.Certificate21.required_origin_594_i7 line 449
  223. theorem OAI.SnakyPrototype.Certificate21.required_exact_594_i7 line 451
  224. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_594_i7 line 455
  225. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_594_i7 line 457
  226. def OAI.SnakyPrototype.Certificate21.checked_594_i7 line 461
  227. def OAI.SnakyPrototype.Certificate21.height_594_i6 line 469
  228. def OAI.SnakyPrototype.Certificate21.childrenH_594_i6 line 470
  229. theorem OAI.SnakyPrototype.Certificate21.height_exact_594_i6 line 471
  230. theorem OAI.SnakyPrototype.Certificate21.required_origin_594_i6 line 472
  231. theorem OAI.SnakyPrototype.Certificate21.required_exact_594_i6 line 474
  232. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_594_i6 line 478
  233. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_594_i6 line 480
  234. def OAI.SnakyPrototype.Certificate21.checked_594_i6 line 484
  235. def OAI.SnakyPrototype.Certificate21.height_594_i5 line 492
  236. def OAI.SnakyPrototype.Certificate21.childrenH_594_i5 line 493
  237. theorem OAI.SnakyPrototype.Certificate21.height_exact_594_i5 line 494
  238. theorem OAI.SnakyPrototype.Certificate21.required_origin_594_i5 line 495
  239. theorem OAI.SnakyPrototype.Certificate21.required_exact_594_i5 line 497
  240. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_594_i5 line 501
  241. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_594_i5 line 503
  242. def OAI.SnakyPrototype.Certificate21.checked_594_i5 line 507
  243. def OAI.SnakyPrototype.Certificate21.height_594_i4 line 515
  244. def OAI.SnakyPrototype.Certificate21.childrenH_594_i4 line 516
  245. theorem OAI.SnakyPrototype.Certificate21.height_exact_594_i4 line 517
  246. theorem OAI.SnakyPrototype.Certificate21.required_origin_594_i4 line 518
  247. theorem OAI.SnakyPrototype.Certificate21.required_exact_594_i4 line 520
  248. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_594_i4 line 524
  249. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_594_i4 line 526
  250. def OAI.SnakyPrototype.Certificate21.checked_594_i4 line 530
  251. def OAI.SnakyPrototype.Certificate21.height_594_i3 line 538
  252. def OAI.SnakyPrototype.Certificate21.childrenH_594_i3 line 539
  253. theorem OAI.SnakyPrototype.Certificate21.height_exact_594_i3 line 540
  254. theorem OAI.SnakyPrototype.Certificate21.required_origin_594_i3 line 541
  255. theorem OAI.SnakyPrototype.Certificate21.required_exact_594_i3 line 543
  256. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_594_i3 line 547
  257. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_594_i3 line 549
  258. def OAI.SnakyPrototype.Certificate21.checked_594_i3 line 553
  259. def OAI.SnakyPrototype.Certificate21.height_594_i2 line 561
  260. def OAI.SnakyPrototype.Certificate21.childrenH_594_i2 line 562
  261. theorem OAI.SnakyPrototype.Certificate21.height_exact_594_i2 line 563
  262. theorem OAI.SnakyPrototype.Certificate21.required_origin_594_i2 line 564
  263. theorem OAI.SnakyPrototype.Certificate21.required_exact_594_i2 line 566
  264. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_594_i2 line 570
  265. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_594_i2 line 572
  266. def OAI.SnakyPrototype.Certificate21.checked_594_i2 line 576
  267. def OAI.SnakyPrototype.Certificate21.height_594_i8 line 584
  268. def OAI.SnakyPrototype.Certificate21.childrenH_594_i8 line 585
  269. theorem OAI.SnakyPrototype.Certificate21.height_exact_594_i8 line 586
  270. theorem OAI.SnakyPrototype.Certificate21.required_origin_594_i8 line 587
  271. theorem OAI.SnakyPrototype.Certificate21.required_exact_594_i8 line 589
  272. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_594_i8 line 593
  273. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_594_i8 line 595
  274. def OAI.SnakyPrototype.Certificate21.checked_594_i8 line 599
  275. def OAI.SnakyPrototype.Certificate21.height_594_i1 line 607
  276. def OAI.SnakyPrototype.Certificate21.childrenH_594_i1 line 608
  277. theorem OAI.SnakyPrototype.Certificate21.height_exact_594_i1 line 609
  278. theorem OAI.SnakyPrototype.Certificate21.required_origin_594_i1 line 610
  279. theorem OAI.SnakyPrototype.Certificate21.required_exact_594_i1 line 612
  280. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_594_i1 line 616
  281. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_594_i1 line 618
  282. def OAI.SnakyPrototype.Certificate21.checked_594_i1 line 622
  283. def OAI.SnakyPrototype.Certificate21.height_594 line 630
  284. def OAI.SnakyPrototype.Certificate21.childrenH_594 line 631
  285. theorem OAI.SnakyPrototype.Certificate21.height_exact_594 line 632
  286. theorem OAI.SnakyPrototype.Certificate21.required_origin_594 line 633
  287. theorem OAI.SnakyPrototype.Certificate21.required_exact_594 line 635
  288. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_594 line 639
  289. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_594 line 641
  290. def OAI.SnakyPrototype.Certificate21.checked_594 line 645
  291. def OAI.SnakyPrototype.Certificate21.height_608_i1 line 653
  292. def OAI.SnakyPrototype.Certificate21.childrenH_608_i1 line 654
  293. theorem OAI.SnakyPrototype.Certificate21.height_exact_608_i1 line 655
  294. theorem OAI.SnakyPrototype.Certificate21.required_origin_608_i1 line 656
  295. theorem OAI.SnakyPrototype.Certificate21.required_exact_608_i1 line 658
  296. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_608_i1 line 662
  297. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_608_i1 line 664
  298. def OAI.SnakyPrototype.Certificate21.checked_608_i1 line 668
  299. def OAI.SnakyPrototype.Certificate21.height_608_i2 line 676
  300. def OAI.SnakyPrototype.Certificate21.childrenH_608_i2 line 677
  301. theorem OAI.SnakyPrototype.Certificate21.height_exact_608_i2 line 678
  302. theorem OAI.SnakyPrototype.Certificate21.required_origin_608_i2 line 679
  303. theorem OAI.SnakyPrototype.Certificate21.required_exact_608_i2 line 681
  304. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_608_i2 line 685
  305. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_608_i2 line 687
  306. def OAI.SnakyPrototype.Certificate21.checked_608_i2 line 691
  307. def OAI.SnakyPrototype.Certificate21.height_608_i3 line 699
  308. def OAI.SnakyPrototype.Certificate21.childrenH_608_i3 line 700
  309. theorem OAI.SnakyPrototype.Certificate21.height_exact_608_i3 line 701
  310. theorem OAI.SnakyPrototype.Certificate21.required_origin_608_i3 line 702
  311. theorem OAI.SnakyPrototype.Certificate21.required_exact_608_i3 line 704
  312. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_608_i3 line 708
  313. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_608_i3 line 710
  314. def OAI.SnakyPrototype.Certificate21.checked_608_i3 line 714
  315. def OAI.SnakyPrototype.Certificate21.height_608_i0 line 722
  316. def OAI.SnakyPrototype.Certificate21.childrenH_608_i0 line 723
  317. theorem OAI.SnakyPrototype.Certificate21.height_exact_608_i0 line 724
  318. theorem OAI.SnakyPrototype.Certificate21.required_origin_608_i0 line 725
  319. theorem OAI.SnakyPrototype.Certificate21.required_exact_608_i0 line 727
  320. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_608_i0 line 731
  321. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_608_i0 line 733
  322. def OAI.SnakyPrototype.Certificate21.checked_608_i0 line 737
  323. def OAI.SnakyPrototype.Certificate21.height_608 line 745
  324. def OAI.SnakyPrototype.Certificate21.childrenH_608 line 746
  325. theorem OAI.SnakyPrototype.Certificate21.height_exact_608 line 747
  326. theorem OAI.SnakyPrototype.Certificate21.required_origin_608 line 748
  327. theorem OAI.SnakyPrototype.Certificate21.required_exact_608 line 750
  328. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_608 line 754
  329. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_608 line 756
  330. def OAI.SnakyPrototype.Certificate21.checked_608 line 760
  331. def OAI.SnakyPrototype.Certificate21.height_616_i1 line 768
  332. def OAI.SnakyPrototype.Certificate21.childrenH_616_i1 line 769
  333. theorem OAI.SnakyPrototype.Certificate21.height_exact_616_i1 line 770
  334. theorem OAI.SnakyPrototype.Certificate21.required_origin_616_i1 line 771
  335. theorem OAI.SnakyPrototype.Certificate21.required_exact_616_i1 line 773
  336. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_616_i1 line 777
  337. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_616_i1 line 779
  338. def OAI.SnakyPrototype.Certificate21.checked_616_i1 line 783
  339. def OAI.SnakyPrototype.Certificate21.height_616_i0 line 791
  340. def OAI.SnakyPrototype.Certificate21.childrenH_616_i0 line 792
  341. theorem OAI.SnakyPrototype.Certificate21.height_exact_616_i0 line 793
  342. theorem OAI.SnakyPrototype.Certificate21.required_origin_616_i0 line 794
  343. theorem OAI.SnakyPrototype.Certificate21.required_exact_616_i0 line 796
  344. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_616_i0 line 800
  345. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_616_i0 line 802
  346. def OAI.SnakyPrototype.Certificate21.checked_616_i0 line 806
  347. def OAI.SnakyPrototype.Certificate21.height_616 line 814
  348. def OAI.SnakyPrototype.Certificate21.childrenH_616 line 815
  349. theorem OAI.SnakyPrototype.Certificate21.height_exact_616 line 816
  350. theorem OAI.SnakyPrototype.Certificate21.required_origin_616 line 817
  351. theorem OAI.SnakyPrototype.Certificate21.required_exact_616 line 819
  352. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_616 line 823
  353. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_616 line 825
  354. def OAI.SnakyPrototype.Certificate21.checked_616 line 829
  355. def OAI.SnakyPrototype.Certificate21.height_631_i1 line 837
  356. def OAI.SnakyPrototype.Certificate21.childrenH_631_i1 line 838
  357. theorem OAI.SnakyPrototype.Certificate21.height_exact_631_i1 line 839
  358. theorem OAI.SnakyPrototype.Certificate21.required_origin_631_i1 line 840
  359. theorem OAI.SnakyPrototype.Certificate21.required_exact_631_i1 line 842
  360. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_631_i1 line 846
  361. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_631_i1 line 848
  362. def OAI.SnakyPrototype.Certificate21.checked_631_i1 line 852
  363. def OAI.SnakyPrototype.Certificate21.height_631_i0 line 860
  364. def OAI.SnakyPrototype.Certificate21.childrenH_631_i0 line 861
  365. theorem OAI.SnakyPrototype.Certificate21.height_exact_631_i0 line 862
  366. theorem OAI.SnakyPrototype.Certificate21.required_origin_631_i0 line 863
  367. theorem OAI.SnakyPrototype.Certificate21.required_exact_631_i0 line 865
  368. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_631_i0 line 869
  369. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_631_i0 line 871
  370. def OAI.SnakyPrototype.Certificate21.checked_631_i0 line 875
  371. def OAI.SnakyPrototype.Certificate21.height_631 line 883
  372. def OAI.SnakyPrototype.Certificate21.childrenH_631 line 884
  373. theorem OAI.SnakyPrototype.Certificate21.height_exact_631 line 885
  374. theorem OAI.SnakyPrototype.Certificate21.required_origin_631 line 886
  375. theorem OAI.SnakyPrototype.Certificate21.required_exact_631 line 888
  376. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_631 line 892
  377. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_631 line 894
  378. def OAI.SnakyPrototype.Certificate21.checked_631 line 898