OAI/GameTheory/SnakyTwentyOne/Cards/Height13Part05.lean

GitHub source file

324 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_675_i0 line 34
  2. def OAI.SnakyPrototype.Certificate21.envelope_675_i0 line 35
  3. def OAI.SnakyPrototype.Certificate21.childrenC_675_i0 line 36
  4. def OAI.SnakyPrototype.Certificate21.childrenD_675_i0 line 37
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_675_i0 line 38
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_675_i0 line 39
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_675_i0 line 40
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_675_i0 line 41
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_675_i0 line 42
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_675_i0 line 50
  11. def OAI.SnakyPrototype.Certificate21.required_675_i1 line 55
  12. def OAI.SnakyPrototype.Certificate21.envelope_675_i1 line 56
  13. def OAI.SnakyPrototype.Certificate21.childrenC_675_i1 line 57
  14. def OAI.SnakyPrototype.Certificate21.childrenD_675_i1 line 58
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_675_i1 line 59
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_675_i1 line 60
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_675_i1 line 61
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_675_i1 line 62
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_675_i1 line 63
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_675_i1 line 72
  21. def OAI.SnakyPrototype.Certificate21.required_675_i3 line 77
  22. def OAI.SnakyPrototype.Certificate21.envelope_675_i3 line 78
  23. def OAI.SnakyPrototype.Certificate21.childrenC_675_i3 line 79
  24. def OAI.SnakyPrototype.Certificate21.childrenD_675_i3 line 80
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_675_i3 line 81
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_675_i3 line 82
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_675_i3 line 83
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_675_i3 line 84
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_675_i3 line 85
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_675_i3 line 93
  31. def OAI.SnakyPrototype.Certificate21.required_675_i5 line 98
  32. def OAI.SnakyPrototype.Certificate21.envelope_675_i5 line 99
  33. def OAI.SnakyPrototype.Certificate21.childrenC_675_i5 line 100
  34. def OAI.SnakyPrototype.Certificate21.childrenD_675_i5 line 101
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_675_i5 line 102
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_675_i5 line 103
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_675_i5 line 104
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_675_i5 line 105
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_675_i5 line 106
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_675_i5 line 111
  41. def OAI.SnakyPrototype.Certificate21.required_675_i6 line 116
  42. def OAI.SnakyPrototype.Certificate21.envelope_675_i6 line 117
  43. def OAI.SnakyPrototype.Certificate21.childrenC_675_i6 line 118
  44. def OAI.SnakyPrototype.Certificate21.childrenD_675_i6 line 119
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_675_i6 line 120
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_675_i6 line 121
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_675_i6 line 122
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_675_i6 line 123
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_675_i6 line 124
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_675_i6 line 130
  51. def OAI.SnakyPrototype.Certificate21.required_675_i4 line 135
  52. def OAI.SnakyPrototype.Certificate21.envelope_675_i4 line 136
  53. def OAI.SnakyPrototype.Certificate21.childrenC_675_i4 line 137
  54. def OAI.SnakyPrototype.Certificate21.childrenD_675_i4 line 138
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_675_i4 line 139
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_675_i4 line 140
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_675_i4 line 141
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_675_i4 line 142
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_675_i4 line 143
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_675_i4 line 148
  61. def OAI.SnakyPrototype.Certificate21.required_675_i2 line 153
  62. def OAI.SnakyPrototype.Certificate21.envelope_675_i2 line 154
  63. def OAI.SnakyPrototype.Certificate21.childrenC_675_i2 line 155
  64. def OAI.SnakyPrototype.Certificate21.childrenD_675_i2 line 156
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_675_i2 line 157
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_675_i2 line 158
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_675_i2 line 159
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_675_i2 line 160
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_675_i2 line 161
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_675_i2 line 169
  71. def OAI.SnakyPrototype.Certificate21.required_675_i7 line 174
  72. def OAI.SnakyPrototype.Certificate21.envelope_675_i7 line 175
  73. def OAI.SnakyPrototype.Certificate21.childrenC_675_i7 line 176
  74. def OAI.SnakyPrototype.Certificate21.childrenD_675_i7 line 177
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_675_i7 line 178
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_675_i7 line 179
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_675_i7 line 180
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_675_i7 line 181
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_675_i7 line 182
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_675_i7 line 189
  81. def OAI.SnakyPrototype.Certificate21.required_675_i8 line 194
  82. def OAI.SnakyPrototype.Certificate21.envelope_675_i8 line 195
  83. def OAI.SnakyPrototype.Certificate21.childrenC_675_i8 line 196
  84. def OAI.SnakyPrototype.Certificate21.childrenD_675_i8 line 197
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_675_i8 line 198
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_675_i8 line 199
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_675_i8 line 200
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_675_i8 line 201
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_675_i8 line 202
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_675_i8 line 208
  91. def OAI.SnakyPrototype.Certificate21.required_675_i10 line 213
  92. def OAI.SnakyPrototype.Certificate21.envelope_675_i10 line 214
  93. def OAI.SnakyPrototype.Certificate21.childrenC_675_i10 line 215
  94. def OAI.SnakyPrototype.Certificate21.childrenD_675_i10 line 216
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_675_i10 line 217
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_675_i10 line 218
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_675_i10 line 219
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_675_i10 line 220
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_675_i10 line 221
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_675_i10 line 226
  101. def OAI.SnakyPrototype.Certificate21.required_675_i9 line 231
  102. def OAI.SnakyPrototype.Certificate21.envelope_675_i9 line 232
  103. def OAI.SnakyPrototype.Certificate21.childrenC_675_i9 line 233
  104. def OAI.SnakyPrototype.Certificate21.childrenD_675_i9 line 234
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_675_i9 line 235
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_675_i9 line 236
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_675_i9 line 237
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_675_i9 line 238
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_675_i9 line 239
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_675_i9 line 248
  111. def OAI.SnakyPrototype.Certificate21.required_675 line 253
  112. def OAI.SnakyPrototype.Certificate21.envelope_675 line 254
  113. def OAI.SnakyPrototype.Certificate21.childrenC_675 line 255
  114. def OAI.SnakyPrototype.Certificate21.childrenD_675 line 256
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_675 line 257
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_675 line 258
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_675 line 259
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_675 line 260
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_675 line 261
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_675 line 273
  121. def OAI.SnakyPrototype.Certificate21.required_690_i0 line 278
  122. def OAI.SnakyPrototype.Certificate21.envelope_690_i0 line 279
  123. def OAI.SnakyPrototype.Certificate21.childrenC_690_i0 line 280
  124. def OAI.SnakyPrototype.Certificate21.childrenD_690_i0 line 281
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_690_i0 line 282
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_690_i0 line 283
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_690_i0 line 284
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_690_i0 line 285
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_690_i0 line 286
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_690_i0 line 292
  131. def OAI.SnakyPrototype.Certificate21.required_690 line 297
  132. def OAI.SnakyPrototype.Certificate21.envelope_690 line 298
  133. def OAI.SnakyPrototype.Certificate21.childrenC_690 line 299
  134. def OAI.SnakyPrototype.Certificate21.childrenD_690 line 300
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_690 line 301
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_690 line 302
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_690 line 303
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_690 line 304
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_690 line 305
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_690 line 311
  141. def OAI.SnakyPrototype.Certificate21.required_692_i1 line 316
  142. def OAI.SnakyPrototype.Certificate21.envelope_692_i1 line 317
  143. def OAI.SnakyPrototype.Certificate21.childrenC_692_i1 line 318
  144. def OAI.SnakyPrototype.Certificate21.childrenD_692_i1 line 319
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_692_i1 line 320
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_692_i1 line 321
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_692_i1 line 322
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_692_i1 line 323
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_692_i1 line 324
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_692_i1 line 334
  151. def OAI.SnakyPrototype.Certificate21.required_692_i2 line 339
  152. def OAI.SnakyPrototype.Certificate21.envelope_692_i2 line 340
  153. def OAI.SnakyPrototype.Certificate21.childrenC_692_i2 line 341
  154. def OAI.SnakyPrototype.Certificate21.childrenD_692_i2 line 342
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_692_i2 line 343
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_692_i2 line 344
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_692_i2 line 345
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_692_i2 line 346
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_692_i2 line 347
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_692_i2 line 352
  161. def OAI.SnakyPrototype.Certificate21.required_692_i0 line 357
  162. def OAI.SnakyPrototype.Certificate21.envelope_692_i0 line 358
  163. def OAI.SnakyPrototype.Certificate21.childrenC_692_i0 line 359
  164. def OAI.SnakyPrototype.Certificate21.childrenD_692_i0 line 360
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_692_i0 line 361
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_692_i0 line 362
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_692_i0 line 363
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_692_i0 line 364
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_692_i0 line 365
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_692_i0 line 376
  171. def OAI.SnakyPrototype.Certificate21.required_692 line 381
  172. def OAI.SnakyPrototype.Certificate21.envelope_692 line 382
  173. def OAI.SnakyPrototype.Certificate21.childrenC_692 line 383
  174. def OAI.SnakyPrototype.Certificate21.childrenD_692 line 384
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_692 line 385
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_692 line 386
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_692 line 387
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_692 line 388
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_692 line 389
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_692 line 394
  181. def OAI.SnakyPrototype.Certificate21.height_675_i0 line 399
  182. def OAI.SnakyPrototype.Certificate21.childrenH_675_i0 line 400
  183. theorem OAI.SnakyPrototype.Certificate21.height_exact_675_i0 line 401
  184. theorem OAI.SnakyPrototype.Certificate21.required_origin_675_i0 line 402
  185. theorem OAI.SnakyPrototype.Certificate21.required_exact_675_i0 line 404
  186. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_675_i0 line 408
  187. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_675_i0 line 410
  188. def OAI.SnakyPrototype.Certificate21.checked_675_i0 line 414
  189. def OAI.SnakyPrototype.Certificate21.height_675_i1 line 422
  190. def OAI.SnakyPrototype.Certificate21.childrenH_675_i1 line 423
  191. theorem OAI.SnakyPrototype.Certificate21.height_exact_675_i1 line 424
  192. theorem OAI.SnakyPrototype.Certificate21.required_origin_675_i1 line 425
  193. theorem OAI.SnakyPrototype.Certificate21.required_exact_675_i1 line 427
  194. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_675_i1 line 431
  195. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_675_i1 line 433
  196. def OAI.SnakyPrototype.Certificate21.checked_675_i1 line 437
  197. def OAI.SnakyPrototype.Certificate21.height_675_i3 line 445
  198. def OAI.SnakyPrototype.Certificate21.childrenH_675_i3 line 446
  199. theorem OAI.SnakyPrototype.Certificate21.height_exact_675_i3 line 447
  200. theorem OAI.SnakyPrototype.Certificate21.required_origin_675_i3 line 448
  201. theorem OAI.SnakyPrototype.Certificate21.required_exact_675_i3 line 450
  202. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_675_i3 line 454
  203. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_675_i3 line 456
  204. def OAI.SnakyPrototype.Certificate21.checked_675_i3 line 460
  205. def OAI.SnakyPrototype.Certificate21.height_675_i5 line 468
  206. def OAI.SnakyPrototype.Certificate21.childrenH_675_i5 line 469
  207. theorem OAI.SnakyPrototype.Certificate21.height_exact_675_i5 line 470
  208. theorem OAI.SnakyPrototype.Certificate21.required_origin_675_i5 line 471
  209. theorem OAI.SnakyPrototype.Certificate21.required_exact_675_i5 line 473
  210. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_675_i5 line 477
  211. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_675_i5 line 479
  212. def OAI.SnakyPrototype.Certificate21.checked_675_i5 line 483
  213. def OAI.SnakyPrototype.Certificate21.height_675_i6 line 491
  214. def OAI.SnakyPrototype.Certificate21.childrenH_675_i6 line 492
  215. theorem OAI.SnakyPrototype.Certificate21.height_exact_675_i6 line 493
  216. theorem OAI.SnakyPrototype.Certificate21.required_origin_675_i6 line 494
  217. theorem OAI.SnakyPrototype.Certificate21.required_exact_675_i6 line 496
  218. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_675_i6 line 500
  219. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_675_i6 line 502
  220. def OAI.SnakyPrototype.Certificate21.checked_675_i6 line 506
  221. def OAI.SnakyPrototype.Certificate21.height_675_i4 line 514
  222. def OAI.SnakyPrototype.Certificate21.childrenH_675_i4 line 515
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_675_i4 line 516
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_675_i4 line 517
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_675_i4 line 519
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_675_i4 line 523
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_675_i4 line 525
  228. def OAI.SnakyPrototype.Certificate21.checked_675_i4 line 529
  229. def OAI.SnakyPrototype.Certificate21.height_675_i2 line 537
  230. def OAI.SnakyPrototype.Certificate21.childrenH_675_i2 line 538
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_675_i2 line 539
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_675_i2 line 540
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_675_i2 line 542
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_675_i2 line 546
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_675_i2 line 548
  236. def OAI.SnakyPrototype.Certificate21.checked_675_i2 line 552
  237. def OAI.SnakyPrototype.Certificate21.height_675_i7 line 560
  238. def OAI.SnakyPrototype.Certificate21.childrenH_675_i7 line 561
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_675_i7 line 562
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_675_i7 line 563
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_675_i7 line 565
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_675_i7 line 569
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_675_i7 line 571
  244. def OAI.SnakyPrototype.Certificate21.checked_675_i7 line 575
  245. def OAI.SnakyPrototype.Certificate21.height_675_i8 line 583
  246. def OAI.SnakyPrototype.Certificate21.childrenH_675_i8 line 584
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_675_i8 line 585
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_675_i8 line 586
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_675_i8 line 588
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_675_i8 line 592
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_675_i8 line 594
  252. def OAI.SnakyPrototype.Certificate21.checked_675_i8 line 598
  253. def OAI.SnakyPrototype.Certificate21.height_675_i10 line 606
  254. def OAI.SnakyPrototype.Certificate21.childrenH_675_i10 line 607
  255. theorem OAI.SnakyPrototype.Certificate21.height_exact_675_i10 line 608
  256. theorem OAI.SnakyPrototype.Certificate21.required_origin_675_i10 line 609
  257. theorem OAI.SnakyPrototype.Certificate21.required_exact_675_i10 line 611
  258. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_675_i10 line 615
  259. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_675_i10 line 617
  260. def OAI.SnakyPrototype.Certificate21.checked_675_i10 line 621
  261. def OAI.SnakyPrototype.Certificate21.height_675_i9 line 629
  262. def OAI.SnakyPrototype.Certificate21.childrenH_675_i9 line 630
  263. theorem OAI.SnakyPrototype.Certificate21.height_exact_675_i9 line 631
  264. theorem OAI.SnakyPrototype.Certificate21.required_origin_675_i9 line 632
  265. theorem OAI.SnakyPrototype.Certificate21.required_exact_675_i9 line 634
  266. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_675_i9 line 638
  267. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_675_i9 line 640
  268. def OAI.SnakyPrototype.Certificate21.checked_675_i9 line 644
  269. def OAI.SnakyPrototype.Certificate21.height_675 line 652
  270. def OAI.SnakyPrototype.Certificate21.childrenH_675 line 653
  271. theorem OAI.SnakyPrototype.Certificate21.height_exact_675 line 654
  272. theorem OAI.SnakyPrototype.Certificate21.required_origin_675 line 655
  273. theorem OAI.SnakyPrototype.Certificate21.required_exact_675 line 657
  274. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_675 line 661
  275. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_675 line 663
  276. def OAI.SnakyPrototype.Certificate21.checked_675 line 667
  277. def OAI.SnakyPrototype.Certificate21.height_690_i0 line 675
  278. def OAI.SnakyPrototype.Certificate21.childrenH_690_i0 line 676
  279. theorem OAI.SnakyPrototype.Certificate21.height_exact_690_i0 line 677
  280. theorem OAI.SnakyPrototype.Certificate21.required_origin_690_i0 line 678
  281. theorem OAI.SnakyPrototype.Certificate21.required_exact_690_i0 line 680
  282. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_690_i0 line 684
  283. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_690_i0 line 686
  284. def OAI.SnakyPrototype.Certificate21.checked_690_i0 line 690
  285. def OAI.SnakyPrototype.Certificate21.height_690 line 698
  286. def OAI.SnakyPrototype.Certificate21.childrenH_690 line 699
  287. theorem OAI.SnakyPrototype.Certificate21.height_exact_690 line 700
  288. theorem OAI.SnakyPrototype.Certificate21.required_origin_690 line 701
  289. theorem OAI.SnakyPrototype.Certificate21.required_exact_690 line 703
  290. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_690 line 707
  291. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_690 line 709
  292. def OAI.SnakyPrototype.Certificate21.checked_690 line 713
  293. def OAI.SnakyPrototype.Certificate21.height_692_i1 line 721
  294. def OAI.SnakyPrototype.Certificate21.childrenH_692_i1 line 722
  295. theorem OAI.SnakyPrototype.Certificate21.height_exact_692_i1 line 723
  296. theorem OAI.SnakyPrototype.Certificate21.required_origin_692_i1 line 724
  297. theorem OAI.SnakyPrototype.Certificate21.required_exact_692_i1 line 726
  298. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_692_i1 line 730
  299. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_692_i1 line 732
  300. def OAI.SnakyPrototype.Certificate21.checked_692_i1 line 736
  301. def OAI.SnakyPrototype.Certificate21.height_692_i2 line 744
  302. def OAI.SnakyPrototype.Certificate21.childrenH_692_i2 line 745
  303. theorem OAI.SnakyPrototype.Certificate21.height_exact_692_i2 line 746
  304. theorem OAI.SnakyPrototype.Certificate21.required_origin_692_i2 line 747
  305. theorem OAI.SnakyPrototype.Certificate21.required_exact_692_i2 line 749
  306. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_692_i2 line 753
  307. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_692_i2 line 755
  308. def OAI.SnakyPrototype.Certificate21.checked_692_i2 line 759
  309. def OAI.SnakyPrototype.Certificate21.height_692_i0 line 767
  310. def OAI.SnakyPrototype.Certificate21.childrenH_692_i0 line 768
  311. theorem OAI.SnakyPrototype.Certificate21.height_exact_692_i0 line 769
  312. theorem OAI.SnakyPrototype.Certificate21.required_origin_692_i0 line 770
  313. theorem OAI.SnakyPrototype.Certificate21.required_exact_692_i0 line 772
  314. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_692_i0 line 776
  315. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_692_i0 line 778
  316. def OAI.SnakyPrototype.Certificate21.checked_692_i0 line 782
  317. def OAI.SnakyPrototype.Certificate21.height_692 line 790
  318. def OAI.SnakyPrototype.Certificate21.childrenH_692 line 791
  319. theorem OAI.SnakyPrototype.Certificate21.height_exact_692 line 792
  320. theorem OAI.SnakyPrototype.Certificate21.required_origin_692 line 793
  321. theorem OAI.SnakyPrototype.Certificate21.required_exact_692 line 795
  322. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_692 line 799
  323. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_692 line 801
  324. def OAI.SnakyPrototype.Certificate21.checked_692 line 805