OAI/GameTheory/SnakyTwentyOne/Cards/Height11Part05.lean

GitHub source file

414 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_639_i2 line 38
  2. def OAI.SnakyPrototype.Certificate21.envelope_639_i2 line 39
  3. def OAI.SnakyPrototype.Certificate21.childrenC_639_i2 line 40
  4. def OAI.SnakyPrototype.Certificate21.childrenD_639_i2 line 41
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_639_i2 line 42
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_639_i2 line 43
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_639_i2 line 44
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_639_i2 line 45
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_639_i2 line 46
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_639_i2 line 52
  11. def OAI.SnakyPrototype.Certificate21.required_639_i1 line 57
  12. def OAI.SnakyPrototype.Certificate21.envelope_639_i1 line 58
  13. def OAI.SnakyPrototype.Certificate21.childrenC_639_i1 line 59
  14. def OAI.SnakyPrototype.Certificate21.childrenD_639_i1 line 60
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_639_i1 line 61
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_639_i1 line 62
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_639_i1 line 63
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_639_i1 line 64
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_639_i1 line 65
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_639_i1 line 72
  21. def OAI.SnakyPrototype.Certificate21.required_639_i3 line 77
  22. def OAI.SnakyPrototype.Certificate21.envelope_639_i3 line 78
  23. def OAI.SnakyPrototype.Certificate21.childrenC_639_i3 line 79
  24. def OAI.SnakyPrototype.Certificate21.childrenD_639_i3 line 80
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_639_i3 line 81
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_639_i3 line 82
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_639_i3 line 83
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_639_i3 line 84
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_639_i3 line 85
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_639_i3 line 92
  31. def OAI.SnakyPrototype.Certificate21.required_639_i0 line 97
  32. def OAI.SnakyPrototype.Certificate21.envelope_639_i0 line 98
  33. def OAI.SnakyPrototype.Certificate21.childrenC_639_i0 line 99
  34. def OAI.SnakyPrototype.Certificate21.childrenD_639_i0 line 100
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_639_i0 line 101
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_639_i0 line 102
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_639_i0 line 103
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_639_i0 line 104
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_639_i0 line 105
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_639_i0 line 112
  41. def OAI.SnakyPrototype.Certificate21.required_639 line 117
  42. def OAI.SnakyPrototype.Certificate21.envelope_639 line 118
  43. def OAI.SnakyPrototype.Certificate21.childrenC_639 line 119
  44. def OAI.SnakyPrototype.Certificate21.childrenD_639 line 120
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_639 line 121
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_639 line 122
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_639 line 123
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_639 line 124
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_639 line 125
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_639 line 133
  51. def OAI.SnakyPrototype.Certificate21.required_646_i0 line 138
  52. def OAI.SnakyPrototype.Certificate21.envelope_646_i0 line 139
  53. def OAI.SnakyPrototype.Certificate21.childrenC_646_i0 line 140
  54. def OAI.SnakyPrototype.Certificate21.childrenD_646_i0 line 141
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_646_i0 line 142
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_646_i0 line 143
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_646_i0 line 144
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_646_i0 line 145
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_646_i0 line 146
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_646_i0 line 152
  61. def OAI.SnakyPrototype.Certificate21.required_646 line 157
  62. def OAI.SnakyPrototype.Certificate21.envelope_646 line 158
  63. def OAI.SnakyPrototype.Certificate21.childrenC_646 line 159
  64. def OAI.SnakyPrototype.Certificate21.childrenD_646 line 160
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_646 line 161
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_646 line 162
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_646 line 163
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_646 line 164
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_646 line 165
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_646 line 174
  71. def OAI.SnakyPrototype.Certificate21.required_653_i0 line 179
  72. def OAI.SnakyPrototype.Certificate21.envelope_653_i0 line 180
  73. def OAI.SnakyPrototype.Certificate21.childrenC_653_i0 line 181
  74. def OAI.SnakyPrototype.Certificate21.childrenD_653_i0 line 182
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_653_i0 line 183
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_653_i0 line 184
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_653_i0 line 185
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_653_i0 line 186
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_653_i0 line 187
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_653_i0 line 193
  81. def OAI.SnakyPrototype.Certificate21.required_653 line 198
  82. def OAI.SnakyPrototype.Certificate21.envelope_653 line 199
  83. def OAI.SnakyPrototype.Certificate21.childrenC_653 line 200
  84. def OAI.SnakyPrototype.Certificate21.childrenD_653 line 201
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_653 line 202
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_653 line 203
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_653 line 204
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_653 line 205
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_653 line 206
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_653 line 213
  91. def OAI.SnakyPrototype.Certificate21.required_660_i1 line 218
  92. def OAI.SnakyPrototype.Certificate21.envelope_660_i1 line 219
  93. def OAI.SnakyPrototype.Certificate21.childrenC_660_i1 line 220
  94. def OAI.SnakyPrototype.Certificate21.childrenD_660_i1 line 221
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_660_i1 line 222
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_660_i1 line 223
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_660_i1 line 224
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_660_i1 line 225
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_660_i1 line 226
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_660_i1 line 231
  101. def OAI.SnakyPrototype.Certificate21.required_660_i2 line 236
  102. def OAI.SnakyPrototype.Certificate21.envelope_660_i2 line 237
  103. def OAI.SnakyPrototype.Certificate21.childrenC_660_i2 line 238
  104. def OAI.SnakyPrototype.Certificate21.childrenD_660_i2 line 239
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_660_i2 line 240
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_660_i2 line 241
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_660_i2 line 242
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_660_i2 line 243
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_660_i2 line 244
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_660_i2 line 249
  111. def OAI.SnakyPrototype.Certificate21.required_660_i0 line 254
  112. def OAI.SnakyPrototype.Certificate21.envelope_660_i0 line 255
  113. def OAI.SnakyPrototype.Certificate21.childrenC_660_i0 line 256
  114. def OAI.SnakyPrototype.Certificate21.childrenD_660_i0 line 257
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_660_i0 line 258
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_660_i0 line 259
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_660_i0 line 260
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_660_i0 line 261
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_660_i0 line 262
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_660_i0 line 269
  121. def OAI.SnakyPrototype.Certificate21.required_660 line 274
  122. def OAI.SnakyPrototype.Certificate21.envelope_660 line 275
  123. def OAI.SnakyPrototype.Certificate21.childrenC_660 line 276
  124. def OAI.SnakyPrototype.Certificate21.childrenD_660 line 277
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_660 line 278
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_660 line 279
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_660 line 280
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_660 line 281
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_660 line 282
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_660 line 289
  131. def OAI.SnakyPrototype.Certificate21.required_663 line 294
  132. def OAI.SnakyPrototype.Certificate21.envelope_663 line 295
  133. def OAI.SnakyPrototype.Certificate21.childrenC_663 line 296
  134. def OAI.SnakyPrototype.Certificate21.childrenD_663 line 297
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_663 line 298
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_663 line 299
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_663 line 300
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_663 line 301
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_663 line 302
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_663 line 313
  141. def OAI.SnakyPrototype.Certificate21.required_664 line 318
  142. def OAI.SnakyPrototype.Certificate21.envelope_664 line 319
  143. def OAI.SnakyPrototype.Certificate21.childrenC_664 line 320
  144. def OAI.SnakyPrototype.Certificate21.childrenD_664 line 321
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_664 line 322
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_664 line 323
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_664 line 324
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_664 line 325
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_664 line 326
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_664 line 336
  151. def OAI.SnakyPrototype.Certificate21.required_676_i0 line 341
  152. def OAI.SnakyPrototype.Certificate21.envelope_676_i0 line 342
  153. def OAI.SnakyPrototype.Certificate21.childrenC_676_i0 line 343
  154. def OAI.SnakyPrototype.Certificate21.childrenD_676_i0 line 344
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_676_i0 line 345
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_676_i0 line 346
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_676_i0 line 347
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_676_i0 line 348
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_676_i0 line 349
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_676_i0 line 354
  161. def OAI.SnakyPrototype.Certificate21.required_676 line 359
  162. def OAI.SnakyPrototype.Certificate21.envelope_676 line 360
  163. def OAI.SnakyPrototype.Certificate21.childrenC_676 line 361
  164. def OAI.SnakyPrototype.Certificate21.childrenD_676 line 362
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_676 line 363
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_676 line 364
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_676 line 365
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_676 line 366
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_676 line 367
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_676 line 374
  171. def OAI.SnakyPrototype.Certificate21.required_685_i4 line 379
  172. def OAI.SnakyPrototype.Certificate21.envelope_685_i4 line 380
  173. def OAI.SnakyPrototype.Certificate21.childrenC_685_i4 line 381
  174. def OAI.SnakyPrototype.Certificate21.childrenD_685_i4 line 382
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_685_i4 line 383
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_685_i4 line 384
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_685_i4 line 385
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_685_i4 line 386
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_685_i4 line 387
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_685_i4 line 392
  181. def OAI.SnakyPrototype.Certificate21.required_685_i3 line 397
  182. def OAI.SnakyPrototype.Certificate21.envelope_685_i3 line 398
  183. def OAI.SnakyPrototype.Certificate21.childrenC_685_i3 line 399
  184. def OAI.SnakyPrototype.Certificate21.childrenD_685_i3 line 400
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_685_i3 line 401
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_685_i3 line 402
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_685_i3 line 403
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_685_i3 line 404
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_685_i3 line 405
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_685_i3 line 410
  191. def OAI.SnakyPrototype.Certificate21.required_685_i2 line 415
  192. def OAI.SnakyPrototype.Certificate21.envelope_685_i2 line 416
  193. def OAI.SnakyPrototype.Certificate21.childrenC_685_i2 line 417
  194. def OAI.SnakyPrototype.Certificate21.childrenD_685_i2 line 418
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_685_i2 line 419
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_685_i2 line 420
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_685_i2 line 421
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_685_i2 line 422
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_685_i2 line 423
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_685_i2 line 428
  201. def OAI.SnakyPrototype.Certificate21.required_685_i1 line 433
  202. def OAI.SnakyPrototype.Certificate21.envelope_685_i1 line 434
  203. def OAI.SnakyPrototype.Certificate21.childrenC_685_i1 line 435
  204. def OAI.SnakyPrototype.Certificate21.childrenD_685_i1 line 436
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_685_i1 line 437
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_685_i1 line 438
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_685_i1 line 439
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_685_i1 line 440
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_685_i1 line 441
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_685_i1 line 446
  211. def OAI.SnakyPrototype.Certificate21.required_685_i0 line 451
  212. def OAI.SnakyPrototype.Certificate21.envelope_685_i0 line 452
  213. def OAI.SnakyPrototype.Certificate21.childrenC_685_i0 line 453
  214. def OAI.SnakyPrototype.Certificate21.childrenD_685_i0 line 454
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_685_i0 line 455
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_685_i0 line 456
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_685_i0 line 457
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_685_i0 line 458
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_685_i0 line 459
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_685_i0 line 464
  221. def OAI.SnakyPrototype.Certificate21.required_685 line 469
  222. def OAI.SnakyPrototype.Certificate21.envelope_685 line 470
  223. def OAI.SnakyPrototype.Certificate21.childrenC_685 line 471
  224. def OAI.SnakyPrototype.Certificate21.childrenD_685 line 472
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_685 line 473
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_685 line 474
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_685 line 475
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_685 line 476
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_685 line 477
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_685 line 486
  231. def OAI.SnakyPrototype.Certificate21.height_639_i2 line 491
  232. def OAI.SnakyPrototype.Certificate21.childrenH_639_i2 line 492
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_639_i2 line 493
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_639_i2 line 494
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_639_i2 line 496
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_639_i2 line 500
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_639_i2 line 502
  238. def OAI.SnakyPrototype.Certificate21.checked_639_i2 line 506
  239. def OAI.SnakyPrototype.Certificate21.height_639_i1 line 514
  240. def OAI.SnakyPrototype.Certificate21.childrenH_639_i1 line 515
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_639_i1 line 516
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_639_i1 line 517
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_639_i1 line 519
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_639_i1 line 523
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_639_i1 line 525
  246. def OAI.SnakyPrototype.Certificate21.checked_639_i1 line 529
  247. def OAI.SnakyPrototype.Certificate21.height_639_i3 line 537
  248. def OAI.SnakyPrototype.Certificate21.childrenH_639_i3 line 538
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_639_i3 line 539
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_639_i3 line 540
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_639_i3 line 542
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_639_i3 line 546
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_639_i3 line 548
  254. def OAI.SnakyPrototype.Certificate21.checked_639_i3 line 552
  255. def OAI.SnakyPrototype.Certificate21.height_639_i0 line 560
  256. def OAI.SnakyPrototype.Certificate21.childrenH_639_i0 line 561
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_639_i0 line 562
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_639_i0 line 563
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_639_i0 line 565
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_639_i0 line 569
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_639_i0 line 571
  262. def OAI.SnakyPrototype.Certificate21.checked_639_i0 line 575
  263. def OAI.SnakyPrototype.Certificate21.height_639 line 583
  264. def OAI.SnakyPrototype.Certificate21.childrenH_639 line 584
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_639 line 585
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_639 line 586
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_639 line 588
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_639 line 592
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_639 line 594
  270. def OAI.SnakyPrototype.Certificate21.checked_639 line 598
  271. def OAI.SnakyPrototype.Certificate21.height_646_i0 line 606
  272. def OAI.SnakyPrototype.Certificate21.childrenH_646_i0 line 607
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_646_i0 line 608
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_646_i0 line 609
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_646_i0 line 611
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_646_i0 line 615
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_646_i0 line 617
  278. def OAI.SnakyPrototype.Certificate21.checked_646_i0 line 621
  279. def OAI.SnakyPrototype.Certificate21.height_646 line 629
  280. def OAI.SnakyPrototype.Certificate21.childrenH_646 line 630
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_646 line 631
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_646 line 632
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_646 line 634
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_646 line 638
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_646 line 640
  286. def OAI.SnakyPrototype.Certificate21.checked_646 line 644
  287. def OAI.SnakyPrototype.Certificate21.height_653_i0 line 652
  288. def OAI.SnakyPrototype.Certificate21.childrenH_653_i0 line 653
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_653_i0 line 654
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_653_i0 line 655
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_653_i0 line 657
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_653_i0 line 661
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_653_i0 line 663
  294. def OAI.SnakyPrototype.Certificate21.checked_653_i0 line 667
  295. def OAI.SnakyPrototype.Certificate21.height_653 line 675
  296. def OAI.SnakyPrototype.Certificate21.childrenH_653 line 676
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_653 line 677
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_653 line 678
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_653 line 680
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_653 line 684
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_653 line 686
  302. def OAI.SnakyPrototype.Certificate21.checked_653 line 690
  303. def OAI.SnakyPrototype.Certificate21.height_660_i1 line 698
  304. def OAI.SnakyPrototype.Certificate21.childrenH_660_i1 line 699
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_660_i1 line 700
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_660_i1 line 701
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_660_i1 line 703
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_660_i1 line 707
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_660_i1 line 709
  310. def OAI.SnakyPrototype.Certificate21.checked_660_i1 line 713
  311. def OAI.SnakyPrototype.Certificate21.height_660_i2 line 721
  312. def OAI.SnakyPrototype.Certificate21.childrenH_660_i2 line 722
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_660_i2 line 723
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_660_i2 line 724
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_660_i2 line 726
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_660_i2 line 730
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_660_i2 line 732
  318. def OAI.SnakyPrototype.Certificate21.checked_660_i2 line 736
  319. def OAI.SnakyPrototype.Certificate21.height_660_i0 line 744
  320. def OAI.SnakyPrototype.Certificate21.childrenH_660_i0 line 745
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_660_i0 line 746
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_660_i0 line 747
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_660_i0 line 749
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_660_i0 line 753
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_660_i0 line 755
  326. def OAI.SnakyPrototype.Certificate21.checked_660_i0 line 759
  327. def OAI.SnakyPrototype.Certificate21.height_660 line 767
  328. def OAI.SnakyPrototype.Certificate21.childrenH_660 line 768
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_660 line 769
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_660 line 770
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_660 line 772
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_660 line 776
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_660 line 778
  334. def OAI.SnakyPrototype.Certificate21.checked_660 line 782
  335. def OAI.SnakyPrototype.Certificate21.height_663 line 790
  336. def OAI.SnakyPrototype.Certificate21.childrenH_663 line 791
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_663 line 792
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_663 line 793
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_663 line 795
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_663 line 799
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_663 line 801
  342. def OAI.SnakyPrototype.Certificate21.checked_663 line 805
  343. def OAI.SnakyPrototype.Certificate21.height_664 line 813
  344. def OAI.SnakyPrototype.Certificate21.childrenH_664 line 814
  345. theorem OAI.SnakyPrototype.Certificate21.height_exact_664 line 815
  346. theorem OAI.SnakyPrototype.Certificate21.required_origin_664 line 816
  347. theorem OAI.SnakyPrototype.Certificate21.required_exact_664 line 818
  348. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_664 line 822
  349. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_664 line 824
  350. def OAI.SnakyPrototype.Certificate21.checked_664 line 828
  351. def OAI.SnakyPrototype.Certificate21.height_676_i0 line 836
  352. def OAI.SnakyPrototype.Certificate21.childrenH_676_i0 line 837
  353. theorem OAI.SnakyPrototype.Certificate21.height_exact_676_i0 line 838
  354. theorem OAI.SnakyPrototype.Certificate21.required_origin_676_i0 line 839
  355. theorem OAI.SnakyPrototype.Certificate21.required_exact_676_i0 line 841
  356. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_676_i0 line 845
  357. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_676_i0 line 847
  358. def OAI.SnakyPrototype.Certificate21.checked_676_i0 line 851
  359. def OAI.SnakyPrototype.Certificate21.height_676 line 859
  360. def OAI.SnakyPrototype.Certificate21.childrenH_676 line 860
  361. theorem OAI.SnakyPrototype.Certificate21.height_exact_676 line 861
  362. theorem OAI.SnakyPrototype.Certificate21.required_origin_676 line 862
  363. theorem OAI.SnakyPrototype.Certificate21.required_exact_676 line 864
  364. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_676 line 868
  365. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_676 line 870
  366. def OAI.SnakyPrototype.Certificate21.checked_676 line 874
  367. def OAI.SnakyPrototype.Certificate21.height_685_i4 line 882
  368. def OAI.SnakyPrototype.Certificate21.childrenH_685_i4 line 883
  369. theorem OAI.SnakyPrototype.Certificate21.height_exact_685_i4 line 884
  370. theorem OAI.SnakyPrototype.Certificate21.required_origin_685_i4 line 885
  371. theorem OAI.SnakyPrototype.Certificate21.required_exact_685_i4 line 887
  372. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_685_i4 line 891
  373. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_685_i4 line 893
  374. def OAI.SnakyPrototype.Certificate21.checked_685_i4 line 897
  375. def OAI.SnakyPrototype.Certificate21.height_685_i3 line 905
  376. def OAI.SnakyPrototype.Certificate21.childrenH_685_i3 line 906
  377. theorem OAI.SnakyPrototype.Certificate21.height_exact_685_i3 line 907
  378. theorem OAI.SnakyPrototype.Certificate21.required_origin_685_i3 line 908
  379. theorem OAI.SnakyPrototype.Certificate21.required_exact_685_i3 line 910
  380. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_685_i3 line 914
  381. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_685_i3 line 916
  382. def OAI.SnakyPrototype.Certificate21.checked_685_i3 line 920
  383. def OAI.SnakyPrototype.Certificate21.height_685_i2 line 928
  384. def OAI.SnakyPrototype.Certificate21.childrenH_685_i2 line 929
  385. theorem OAI.SnakyPrototype.Certificate21.height_exact_685_i2 line 930
  386. theorem OAI.SnakyPrototype.Certificate21.required_origin_685_i2 line 931
  387. theorem OAI.SnakyPrototype.Certificate21.required_exact_685_i2 line 933
  388. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_685_i2 line 937
  389. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_685_i2 line 939
  390. def OAI.SnakyPrototype.Certificate21.checked_685_i2 line 943
  391. def OAI.SnakyPrototype.Certificate21.height_685_i1 line 951
  392. def OAI.SnakyPrototype.Certificate21.childrenH_685_i1 line 952
  393. theorem OAI.SnakyPrototype.Certificate21.height_exact_685_i1 line 953
  394. theorem OAI.SnakyPrototype.Certificate21.required_origin_685_i1 line 954
  395. theorem OAI.SnakyPrototype.Certificate21.required_exact_685_i1 line 956
  396. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_685_i1 line 960
  397. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_685_i1 line 962
  398. def OAI.SnakyPrototype.Certificate21.checked_685_i1 line 966
  399. def OAI.SnakyPrototype.Certificate21.height_685_i0 line 974
  400. def OAI.SnakyPrototype.Certificate21.childrenH_685_i0 line 975
  401. theorem OAI.SnakyPrototype.Certificate21.height_exact_685_i0 line 976
  402. theorem OAI.SnakyPrototype.Certificate21.required_origin_685_i0 line 977
  403. theorem OAI.SnakyPrototype.Certificate21.required_exact_685_i0 line 979
  404. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_685_i0 line 983
  405. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_685_i0 line 985
  406. def OAI.SnakyPrototype.Certificate21.checked_685_i0 line 989
  407. def OAI.SnakyPrototype.Certificate21.height_685 line 997
  408. def OAI.SnakyPrototype.Certificate21.childrenH_685 line 998
  409. theorem OAI.SnakyPrototype.Certificate21.height_exact_685 line 999
  410. theorem OAI.SnakyPrototype.Certificate21.required_origin_685 line 1000
  411. theorem OAI.SnakyPrototype.Certificate21.required_exact_685 line 1002
  412. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_685 line 1006
  413. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_685 line 1008
  414. def OAI.SnakyPrototype.Certificate21.checked_685 line 1012