OAI/GameTheory/SnakyTwentyOne/Cards/Height16Part01.lean

GitHub source file

378 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_602_i1 line 37
  2. def OAI.SnakyPrototype.Certificate21.envelope_602_i1 line 38
  3. def OAI.SnakyPrototype.Certificate21.childrenC_602_i1 line 39
  4. def OAI.SnakyPrototype.Certificate21.childrenD_602_i1 line 40
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_602_i1 line 41
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_602_i1 line 42
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_602_i1 line 43
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_602_i1 line 44
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_602_i1 line 45
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_602_i1 line 50
  11. def OAI.SnakyPrototype.Certificate21.required_602_i0 line 55
  12. def OAI.SnakyPrototype.Certificate21.envelope_602_i0 line 56
  13. def OAI.SnakyPrototype.Certificate21.childrenC_602_i0 line 57
  14. def OAI.SnakyPrototype.Certificate21.childrenD_602_i0 line 58
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_602_i0 line 59
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_602_i0 line 60
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_602_i0 line 61
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_602_i0 line 62
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_602_i0 line 63
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_602_i0 line 70
  21. def OAI.SnakyPrototype.Certificate21.required_602_i3 line 75
  22. def OAI.SnakyPrototype.Certificate21.envelope_602_i3 line 76
  23. def OAI.SnakyPrototype.Certificate21.childrenC_602_i3 line 77
  24. def OAI.SnakyPrototype.Certificate21.childrenD_602_i3 line 78
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_602_i3 line 79
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_602_i3 line 80
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_602_i3 line 81
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_602_i3 line 82
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_602_i3 line 83
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_602_i3 line 88
  31. def OAI.SnakyPrototype.Certificate21.required_602_i2 line 93
  32. def OAI.SnakyPrototype.Certificate21.envelope_602_i2 line 94
  33. def OAI.SnakyPrototype.Certificate21.childrenC_602_i2 line 95
  34. def OAI.SnakyPrototype.Certificate21.childrenD_602_i2 line 96
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_602_i2 line 97
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_602_i2 line 98
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_602_i2 line 99
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_602_i2 line 100
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_602_i2 line 101
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_602_i2 line 108
  41. def OAI.SnakyPrototype.Certificate21.required_602_i6 line 113
  42. def OAI.SnakyPrototype.Certificate21.envelope_602_i6 line 114
  43. def OAI.SnakyPrototype.Certificate21.childrenC_602_i6 line 115
  44. def OAI.SnakyPrototype.Certificate21.childrenD_602_i6 line 116
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_602_i6 line 117
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_602_i6 line 118
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_602_i6 line 119
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_602_i6 line 120
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_602_i6 line 121
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_602_i6 line 126
  51. def OAI.SnakyPrototype.Certificate21.required_602_i7 line 131
  52. def OAI.SnakyPrototype.Certificate21.envelope_602_i7 line 132
  53. def OAI.SnakyPrototype.Certificate21.childrenC_602_i7 line 133
  54. def OAI.SnakyPrototype.Certificate21.childrenD_602_i7 line 134
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_602_i7 line 135
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_602_i7 line 136
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_602_i7 line 137
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_602_i7 line 138
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_602_i7 line 139
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_602_i7 line 144
  61. def OAI.SnakyPrototype.Certificate21.required_602_i8 line 149
  62. def OAI.SnakyPrototype.Certificate21.envelope_602_i8 line 150
  63. def OAI.SnakyPrototype.Certificate21.childrenC_602_i8 line 151
  64. def OAI.SnakyPrototype.Certificate21.childrenD_602_i8 line 152
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_602_i8 line 153
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_602_i8 line 154
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_602_i8 line 155
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_602_i8 line 156
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_602_i8 line 157
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_602_i8 line 162
  71. def OAI.SnakyPrototype.Certificate21.required_602_i5 line 167
  72. def OAI.SnakyPrototype.Certificate21.envelope_602_i5 line 168
  73. def OAI.SnakyPrototype.Certificate21.childrenC_602_i5 line 169
  74. def OAI.SnakyPrototype.Certificate21.childrenD_602_i5 line 170
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_602_i5 line 171
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_602_i5 line 172
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_602_i5 line 173
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_602_i5 line 174
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_602_i5 line 175
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_602_i5 line 182
  81. def OAI.SnakyPrototype.Certificate21.required_602_i4 line 187
  82. def OAI.SnakyPrototype.Certificate21.envelope_602_i4 line 188
  83. def OAI.SnakyPrototype.Certificate21.childrenC_602_i4 line 189
  84. def OAI.SnakyPrototype.Certificate21.childrenD_602_i4 line 190
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_602_i4 line 191
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_602_i4 line 192
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_602_i4 line 193
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_602_i4 line 194
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_602_i4 line 195
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_602_i4 line 202
  91. def OAI.SnakyPrototype.Certificate21.required_602 line 207
  92. def OAI.SnakyPrototype.Certificate21.envelope_602 line 208
  93. def OAI.SnakyPrototype.Certificate21.childrenC_602 line 209
  94. def OAI.SnakyPrototype.Certificate21.childrenD_602 line 210
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_602 line 211
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_602 line 212
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_602 line 213
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_602 line 214
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_602 line 215
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_602 line 230
  101. def OAI.SnakyPrototype.Certificate21.required_627_i0 line 235
  102. def OAI.SnakyPrototype.Certificate21.envelope_627_i0 line 236
  103. def OAI.SnakyPrototype.Certificate21.childrenC_627_i0 line 237
  104. def OAI.SnakyPrototype.Certificate21.childrenD_627_i0 line 238
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_627_i0 line 239
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_627_i0 line 240
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_627_i0 line 241
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_627_i0 line 242
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_627_i0 line 243
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_627_i0 line 248
  111. def OAI.SnakyPrototype.Certificate21.required_627_i3 line 253
  112. def OAI.SnakyPrototype.Certificate21.envelope_627_i3 line 254
  113. def OAI.SnakyPrototype.Certificate21.childrenC_627_i3 line 255
  114. def OAI.SnakyPrototype.Certificate21.childrenD_627_i3 line 256
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_627_i3 line 257
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_627_i3 line 258
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_627_i3 line 259
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_627_i3 line 260
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_627_i3 line 261
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_627_i3 line 266
  121. def OAI.SnakyPrototype.Certificate21.required_627_i2 line 271
  122. def OAI.SnakyPrototype.Certificate21.envelope_627_i2 line 272
  123. def OAI.SnakyPrototype.Certificate21.childrenC_627_i2 line 273
  124. def OAI.SnakyPrototype.Certificate21.childrenD_627_i2 line 274
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_627_i2 line 275
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_627_i2 line 276
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_627_i2 line 277
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_627_i2 line 278
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_627_i2 line 279
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_627_i2 line 284
  131. def OAI.SnakyPrototype.Certificate21.required_627_i5 line 289
  132. def OAI.SnakyPrototype.Certificate21.envelope_627_i5 line 290
  133. def OAI.SnakyPrototype.Certificate21.childrenC_627_i5 line 291
  134. def OAI.SnakyPrototype.Certificate21.childrenD_627_i5 line 292
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_627_i5 line 293
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_627_i5 line 294
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_627_i5 line 295
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_627_i5 line 296
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_627_i5 line 297
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_627_i5 line 302
  141. def OAI.SnakyPrototype.Certificate21.required_627_i4 line 307
  142. def OAI.SnakyPrototype.Certificate21.envelope_627_i4 line 308
  143. def OAI.SnakyPrototype.Certificate21.childrenC_627_i4 line 309
  144. def OAI.SnakyPrototype.Certificate21.childrenD_627_i4 line 310
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_627_i4 line 311
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_627_i4 line 312
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_627_i4 line 313
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_627_i4 line 314
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_627_i4 line 315
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_627_i4 line 320
  151. def OAI.SnakyPrototype.Certificate21.required_627_i6 line 325
  152. def OAI.SnakyPrototype.Certificate21.envelope_627_i6 line 326
  153. def OAI.SnakyPrototype.Certificate21.childrenC_627_i6 line 327
  154. def OAI.SnakyPrototype.Certificate21.childrenD_627_i6 line 328
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_627_i6 line 329
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_627_i6 line 330
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_627_i6 line 331
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_627_i6 line 332
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_627_i6 line 333
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_627_i6 line 342
  161. def OAI.SnakyPrototype.Certificate21.required_627_i8 line 347
  162. def OAI.SnakyPrototype.Certificate21.envelope_627_i8 line 348
  163. def OAI.SnakyPrototype.Certificate21.childrenC_627_i8 line 349
  164. def OAI.SnakyPrototype.Certificate21.childrenD_627_i8 line 350
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_627_i8 line 351
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_627_i8 line 352
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_627_i8 line 353
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_627_i8 line 354
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_627_i8 line 355
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_627_i8 line 360
  171. def OAI.SnakyPrototype.Certificate21.required_627_i7 line 365
  172. def OAI.SnakyPrototype.Certificate21.envelope_627_i7 line 366
  173. def OAI.SnakyPrototype.Certificate21.childrenC_627_i7 line 367
  174. def OAI.SnakyPrototype.Certificate21.childrenD_627_i7 line 368
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_627_i7 line 369
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_627_i7 line 370
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_627_i7 line 371
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_627_i7 line 372
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_627_i7 line 373
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_627_i7 line 378
  181. def OAI.SnakyPrototype.Certificate21.required_627_i9 line 383
  182. def OAI.SnakyPrototype.Certificate21.envelope_627_i9 line 384
  183. def OAI.SnakyPrototype.Certificate21.childrenC_627_i9 line 385
  184. def OAI.SnakyPrototype.Certificate21.childrenD_627_i9 line 386
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_627_i9 line 387
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_627_i9 line 388
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_627_i9 line 389
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_627_i9 line 390
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_627_i9 line 391
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_627_i9 line 398
  191. def OAI.SnakyPrototype.Certificate21.required_627_i1 line 403
  192. def OAI.SnakyPrototype.Certificate21.envelope_627_i1 line 404
  193. def OAI.SnakyPrototype.Certificate21.childrenC_627_i1 line 405
  194. def OAI.SnakyPrototype.Certificate21.childrenD_627_i1 line 406
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_627_i1 line 407
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_627_i1 line 408
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_627_i1 line 409
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_627_i1 line 410
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_627_i1 line 411
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_627_i1 line 420
  201. def OAI.SnakyPrototype.Certificate21.required_627 line 425
  202. def OAI.SnakyPrototype.Certificate21.envelope_627 line 426
  203. def OAI.SnakyPrototype.Certificate21.childrenC_627 line 427
  204. def OAI.SnakyPrototype.Certificate21.childrenD_627 line 428
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_627 line 429
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_627 line 430
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_627 line 431
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_627 line 432
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_627 line 433
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_627 line 440
  211. def OAI.SnakyPrototype.Certificate21.height_602_i1 line 445
  212. def OAI.SnakyPrototype.Certificate21.childrenH_602_i1 line 446
  213. theorem OAI.SnakyPrototype.Certificate21.height_exact_602_i1 line 447
  214. theorem OAI.SnakyPrototype.Certificate21.required_origin_602_i1 line 448
  215. theorem OAI.SnakyPrototype.Certificate21.required_exact_602_i1 line 450
  216. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_602_i1 line 454
  217. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_602_i1 line 456
  218. def OAI.SnakyPrototype.Certificate21.checked_602_i1 line 460
  219. def OAI.SnakyPrototype.Certificate21.height_602_i0 line 468
  220. def OAI.SnakyPrototype.Certificate21.childrenH_602_i0 line 469
  221. theorem OAI.SnakyPrototype.Certificate21.height_exact_602_i0 line 470
  222. theorem OAI.SnakyPrototype.Certificate21.required_origin_602_i0 line 471
  223. theorem OAI.SnakyPrototype.Certificate21.required_exact_602_i0 line 473
  224. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_602_i0 line 477
  225. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_602_i0 line 479
  226. def OAI.SnakyPrototype.Certificate21.checked_602_i0 line 483
  227. def OAI.SnakyPrototype.Certificate21.height_602_i3 line 491
  228. def OAI.SnakyPrototype.Certificate21.childrenH_602_i3 line 492
  229. theorem OAI.SnakyPrototype.Certificate21.height_exact_602_i3 line 493
  230. theorem OAI.SnakyPrototype.Certificate21.required_origin_602_i3 line 494
  231. theorem OAI.SnakyPrototype.Certificate21.required_exact_602_i3 line 496
  232. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_602_i3 line 500
  233. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_602_i3 line 502
  234. def OAI.SnakyPrototype.Certificate21.checked_602_i3 line 506
  235. def OAI.SnakyPrototype.Certificate21.height_602_i2 line 514
  236. def OAI.SnakyPrototype.Certificate21.childrenH_602_i2 line 515
  237. theorem OAI.SnakyPrototype.Certificate21.height_exact_602_i2 line 516
  238. theorem OAI.SnakyPrototype.Certificate21.required_origin_602_i2 line 517
  239. theorem OAI.SnakyPrototype.Certificate21.required_exact_602_i2 line 519
  240. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_602_i2 line 523
  241. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_602_i2 line 525
  242. def OAI.SnakyPrototype.Certificate21.checked_602_i2 line 529
  243. def OAI.SnakyPrototype.Certificate21.height_602_i6 line 537
  244. def OAI.SnakyPrototype.Certificate21.childrenH_602_i6 line 538
  245. theorem OAI.SnakyPrototype.Certificate21.height_exact_602_i6 line 539
  246. theorem OAI.SnakyPrototype.Certificate21.required_origin_602_i6 line 540
  247. theorem OAI.SnakyPrototype.Certificate21.required_exact_602_i6 line 542
  248. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_602_i6 line 546
  249. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_602_i6 line 548
  250. def OAI.SnakyPrototype.Certificate21.checked_602_i6 line 552
  251. def OAI.SnakyPrototype.Certificate21.height_602_i7 line 560
  252. def OAI.SnakyPrototype.Certificate21.childrenH_602_i7 line 561
  253. theorem OAI.SnakyPrototype.Certificate21.height_exact_602_i7 line 562
  254. theorem OAI.SnakyPrototype.Certificate21.required_origin_602_i7 line 563
  255. theorem OAI.SnakyPrototype.Certificate21.required_exact_602_i7 line 565
  256. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_602_i7 line 569
  257. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_602_i7 line 571
  258. def OAI.SnakyPrototype.Certificate21.checked_602_i7 line 575
  259. def OAI.SnakyPrototype.Certificate21.height_602_i8 line 583
  260. def OAI.SnakyPrototype.Certificate21.childrenH_602_i8 line 584
  261. theorem OAI.SnakyPrototype.Certificate21.height_exact_602_i8 line 585
  262. theorem OAI.SnakyPrototype.Certificate21.required_origin_602_i8 line 586
  263. theorem OAI.SnakyPrototype.Certificate21.required_exact_602_i8 line 588
  264. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_602_i8 line 592
  265. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_602_i8 line 594
  266. def OAI.SnakyPrototype.Certificate21.checked_602_i8 line 598
  267. def OAI.SnakyPrototype.Certificate21.height_602_i5 line 606
  268. def OAI.SnakyPrototype.Certificate21.childrenH_602_i5 line 607
  269. theorem OAI.SnakyPrototype.Certificate21.height_exact_602_i5 line 608
  270. theorem OAI.SnakyPrototype.Certificate21.required_origin_602_i5 line 609
  271. theorem OAI.SnakyPrototype.Certificate21.required_exact_602_i5 line 611
  272. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_602_i5 line 615
  273. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_602_i5 line 617
  274. def OAI.SnakyPrototype.Certificate21.checked_602_i5 line 621
  275. def OAI.SnakyPrototype.Certificate21.height_602_i4 line 629
  276. def OAI.SnakyPrototype.Certificate21.childrenH_602_i4 line 630
  277. theorem OAI.SnakyPrototype.Certificate21.height_exact_602_i4 line 631
  278. theorem OAI.SnakyPrototype.Certificate21.required_origin_602_i4 line 632
  279. theorem OAI.SnakyPrototype.Certificate21.required_exact_602_i4 line 634
  280. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_602_i4 line 638
  281. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_602_i4 line 640
  282. def OAI.SnakyPrototype.Certificate21.checked_602_i4 line 644
  283. def OAI.SnakyPrototype.Certificate21.height_602 line 652
  284. def OAI.SnakyPrototype.Certificate21.childrenH_602 line 653
  285. theorem OAI.SnakyPrototype.Certificate21.height_exact_602 line 654
  286. theorem OAI.SnakyPrototype.Certificate21.required_origin_602 line 655
  287. theorem OAI.SnakyPrototype.Certificate21.required_exact_602 line 657
  288. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_602 line 661
  289. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_602 line 663
  290. def OAI.SnakyPrototype.Certificate21.checked_602 line 667
  291. def OAI.SnakyPrototype.Certificate21.height_627_i0 line 675
  292. def OAI.SnakyPrototype.Certificate21.childrenH_627_i0 line 676
  293. theorem OAI.SnakyPrototype.Certificate21.height_exact_627_i0 line 677
  294. theorem OAI.SnakyPrototype.Certificate21.required_origin_627_i0 line 678
  295. theorem OAI.SnakyPrototype.Certificate21.required_exact_627_i0 line 680
  296. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_627_i0 line 684
  297. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_627_i0 line 686
  298. def OAI.SnakyPrototype.Certificate21.checked_627_i0 line 690
  299. def OAI.SnakyPrototype.Certificate21.height_627_i3 line 698
  300. def OAI.SnakyPrototype.Certificate21.childrenH_627_i3 line 699
  301. theorem OAI.SnakyPrototype.Certificate21.height_exact_627_i3 line 700
  302. theorem OAI.SnakyPrototype.Certificate21.required_origin_627_i3 line 701
  303. theorem OAI.SnakyPrototype.Certificate21.required_exact_627_i3 line 703
  304. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_627_i3 line 707
  305. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_627_i3 line 709
  306. def OAI.SnakyPrototype.Certificate21.checked_627_i3 line 713
  307. def OAI.SnakyPrototype.Certificate21.height_627_i2 line 721
  308. def OAI.SnakyPrototype.Certificate21.childrenH_627_i2 line 722
  309. theorem OAI.SnakyPrototype.Certificate21.height_exact_627_i2 line 723
  310. theorem OAI.SnakyPrototype.Certificate21.required_origin_627_i2 line 724
  311. theorem OAI.SnakyPrototype.Certificate21.required_exact_627_i2 line 726
  312. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_627_i2 line 730
  313. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_627_i2 line 732
  314. def OAI.SnakyPrototype.Certificate21.checked_627_i2 line 736
  315. def OAI.SnakyPrototype.Certificate21.height_627_i5 line 744
  316. def OAI.SnakyPrototype.Certificate21.childrenH_627_i5 line 745
  317. theorem OAI.SnakyPrototype.Certificate21.height_exact_627_i5 line 746
  318. theorem OAI.SnakyPrototype.Certificate21.required_origin_627_i5 line 747
  319. theorem OAI.SnakyPrototype.Certificate21.required_exact_627_i5 line 749
  320. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_627_i5 line 753
  321. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_627_i5 line 755
  322. def OAI.SnakyPrototype.Certificate21.checked_627_i5 line 759
  323. def OAI.SnakyPrototype.Certificate21.height_627_i4 line 767
  324. def OAI.SnakyPrototype.Certificate21.childrenH_627_i4 line 768
  325. theorem OAI.SnakyPrototype.Certificate21.height_exact_627_i4 line 769
  326. theorem OAI.SnakyPrototype.Certificate21.required_origin_627_i4 line 770
  327. theorem OAI.SnakyPrototype.Certificate21.required_exact_627_i4 line 772
  328. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_627_i4 line 776
  329. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_627_i4 line 778
  330. def OAI.SnakyPrototype.Certificate21.checked_627_i4 line 782
  331. def OAI.SnakyPrototype.Certificate21.height_627_i6 line 790
  332. def OAI.SnakyPrototype.Certificate21.childrenH_627_i6 line 791
  333. theorem OAI.SnakyPrototype.Certificate21.height_exact_627_i6 line 792
  334. theorem OAI.SnakyPrototype.Certificate21.required_origin_627_i6 line 793
  335. theorem OAI.SnakyPrototype.Certificate21.required_exact_627_i6 line 795
  336. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_627_i6 line 799
  337. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_627_i6 line 801
  338. def OAI.SnakyPrototype.Certificate21.checked_627_i6 line 805
  339. def OAI.SnakyPrototype.Certificate21.height_627_i8 line 813
  340. def OAI.SnakyPrototype.Certificate21.childrenH_627_i8 line 814
  341. theorem OAI.SnakyPrototype.Certificate21.height_exact_627_i8 line 815
  342. theorem OAI.SnakyPrototype.Certificate21.required_origin_627_i8 line 816
  343. theorem OAI.SnakyPrototype.Certificate21.required_exact_627_i8 line 818
  344. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_627_i8 line 822
  345. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_627_i8 line 824
  346. def OAI.SnakyPrototype.Certificate21.checked_627_i8 line 828
  347. def OAI.SnakyPrototype.Certificate21.height_627_i7 line 836
  348. def OAI.SnakyPrototype.Certificate21.childrenH_627_i7 line 837
  349. theorem OAI.SnakyPrototype.Certificate21.height_exact_627_i7 line 838
  350. theorem OAI.SnakyPrototype.Certificate21.required_origin_627_i7 line 839
  351. theorem OAI.SnakyPrototype.Certificate21.required_exact_627_i7 line 841
  352. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_627_i7 line 845
  353. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_627_i7 line 847
  354. def OAI.SnakyPrototype.Certificate21.checked_627_i7 line 851
  355. def OAI.SnakyPrototype.Certificate21.height_627_i9 line 859
  356. def OAI.SnakyPrototype.Certificate21.childrenH_627_i9 line 860
  357. theorem OAI.SnakyPrototype.Certificate21.height_exact_627_i9 line 861
  358. theorem OAI.SnakyPrototype.Certificate21.required_origin_627_i9 line 862
  359. theorem OAI.SnakyPrototype.Certificate21.required_exact_627_i9 line 864
  360. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_627_i9 line 868
  361. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_627_i9 line 870
  362. def OAI.SnakyPrototype.Certificate21.checked_627_i9 line 874
  363. def OAI.SnakyPrototype.Certificate21.height_627_i1 line 882
  364. def OAI.SnakyPrototype.Certificate21.childrenH_627_i1 line 883
  365. theorem OAI.SnakyPrototype.Certificate21.height_exact_627_i1 line 884
  366. theorem OAI.SnakyPrototype.Certificate21.required_origin_627_i1 line 885
  367. theorem OAI.SnakyPrototype.Certificate21.required_exact_627_i1 line 887
  368. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_627_i1 line 891
  369. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_627_i1 line 893
  370. def OAI.SnakyPrototype.Certificate21.checked_627_i1 line 897
  371. def OAI.SnakyPrototype.Certificate21.height_627 line 905
  372. def OAI.SnakyPrototype.Certificate21.childrenH_627 line 906
  373. theorem OAI.SnakyPrototype.Certificate21.height_exact_627 line 907
  374. theorem OAI.SnakyPrototype.Certificate21.required_origin_627 line 908
  375. theorem OAI.SnakyPrototype.Certificate21.required_exact_627 line 910
  376. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_627 line 914
  377. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_627 line 916
  378. def OAI.SnakyPrototype.Certificate21.checked_627 line 920