OAI/GameTheory/SnakyTwentyOne/Cards/Height07Part05.lean

GitHub source file

414 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_593_i0 line 23
  2. def OAI.SnakyPrototype.Certificate21.envelope_593_i0 line 24
  3. def OAI.SnakyPrototype.Certificate21.childrenC_593_i0 line 25
  4. def OAI.SnakyPrototype.Certificate21.childrenD_593_i0 line 26
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_593_i0 line 27
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_593_i0 line 28
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_593_i0 line 29
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_593_i0 line 30
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_593_i0 line 31
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_593_i0 line 38
  11. def OAI.SnakyPrototype.Certificate21.required_593 line 43
  12. def OAI.SnakyPrototype.Certificate21.envelope_593 line 44
  13. def OAI.SnakyPrototype.Certificate21.childrenC_593 line 45
  14. def OAI.SnakyPrototype.Certificate21.childrenD_593 line 46
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_593 line 47
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_593 line 48
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_593 line 49
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_593 line 50
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_593 line 51
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_593 line 56
  21. def OAI.SnakyPrototype.Certificate21.required_610 line 61
  22. def OAI.SnakyPrototype.Certificate21.envelope_610 line 62
  23. def OAI.SnakyPrototype.Certificate21.childrenC_610 line 63
  24. def OAI.SnakyPrototype.Certificate21.childrenD_610 line 64
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_610 line 65
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_610 line 66
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_610 line 67
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_610 line 68
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_610 line 69
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_610 line 76
  31. def OAI.SnakyPrototype.Certificate21.required_620_i0 line 81
  32. def OAI.SnakyPrototype.Certificate21.envelope_620_i0 line 82
  33. def OAI.SnakyPrototype.Certificate21.childrenC_620_i0 line 83
  34. def OAI.SnakyPrototype.Certificate21.childrenD_620_i0 line 84
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_620_i0 line 85
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_620_i0 line 86
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_620_i0 line 87
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_620_i0 line 88
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_620_i0 line 89
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_620_i0 line 95
  41. def OAI.SnakyPrototype.Certificate21.required_620 line 100
  42. def OAI.SnakyPrototype.Certificate21.envelope_620 line 101
  43. def OAI.SnakyPrototype.Certificate21.childrenC_620 line 102
  44. def OAI.SnakyPrototype.Certificate21.childrenD_620 line 103
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_620 line 104
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_620 line 105
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_620 line 106
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_620 line 107
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_620 line 108
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_620 line 116
  51. def OAI.SnakyPrototype.Certificate21.required_621_i0 line 121
  52. def OAI.SnakyPrototype.Certificate21.envelope_621_i0 line 122
  53. def OAI.SnakyPrototype.Certificate21.childrenC_621_i0 line 123
  54. def OAI.SnakyPrototype.Certificate21.childrenD_621_i0 line 124
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_621_i0 line 125
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_621_i0 line 126
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_621_i0 line 127
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_621_i0 line 128
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_621_i0 line 129
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_621_i0 line 135
  61. def OAI.SnakyPrototype.Certificate21.required_621_i1 line 140
  62. def OAI.SnakyPrototype.Certificate21.envelope_621_i1 line 141
  63. def OAI.SnakyPrototype.Certificate21.childrenC_621_i1 line 142
  64. def OAI.SnakyPrototype.Certificate21.childrenD_621_i1 line 143
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_621_i1 line 144
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_621_i1 line 145
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_621_i1 line 146
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_621_i1 line 147
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_621_i1 line 148
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_621_i1 line 153
  71. def OAI.SnakyPrototype.Certificate21.required_621 line 158
  72. def OAI.SnakyPrototype.Certificate21.envelope_621 line 159
  73. def OAI.SnakyPrototype.Certificate21.childrenC_621 line 160
  74. def OAI.SnakyPrototype.Certificate21.childrenD_621 line 161
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_621 line 162
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_621 line 163
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_621 line 164
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_621 line 165
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_621 line 166
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_621 line 175
  81. def OAI.SnakyPrototype.Certificate21.required_628_i0 line 180
  82. def OAI.SnakyPrototype.Certificate21.envelope_628_i0 line 181
  83. def OAI.SnakyPrototype.Certificate21.childrenC_628_i0 line 182
  84. def OAI.SnakyPrototype.Certificate21.childrenD_628_i0 line 183
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_628_i0 line 184
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_628_i0 line 185
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_628_i0 line 186
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_628_i0 line 187
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_628_i0 line 188
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_628_i0 line 193
  91. def OAI.SnakyPrototype.Certificate21.required_628_i1 line 198
  92. def OAI.SnakyPrototype.Certificate21.envelope_628_i1 line 199
  93. def OAI.SnakyPrototype.Certificate21.childrenC_628_i1 line 200
  94. def OAI.SnakyPrototype.Certificate21.childrenD_628_i1 line 201
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_628_i1 line 202
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_628_i1 line 203
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_628_i1 line 204
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_628_i1 line 205
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_628_i1 line 206
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_628_i1 line 211
  101. def OAI.SnakyPrototype.Certificate21.required_628_i2 line 216
  102. def OAI.SnakyPrototype.Certificate21.envelope_628_i2 line 217
  103. def OAI.SnakyPrototype.Certificate21.childrenC_628_i2 line 218
  104. def OAI.SnakyPrototype.Certificate21.childrenD_628_i2 line 219
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_628_i2 line 220
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_628_i2 line 221
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_628_i2 line 222
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_628_i2 line 223
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_628_i2 line 224
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_628_i2 line 229
  111. def OAI.SnakyPrototype.Certificate21.required_628 line 234
  112. def OAI.SnakyPrototype.Certificate21.envelope_628 line 235
  113. def OAI.SnakyPrototype.Certificate21.childrenC_628 line 236
  114. def OAI.SnakyPrototype.Certificate21.childrenD_628 line 237
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_628 line 238
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_628 line 239
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_628 line 240
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_628 line 241
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_628 line 242
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_628 line 250
  121. def OAI.SnakyPrototype.Certificate21.required_633_i1 line 255
  122. def OAI.SnakyPrototype.Certificate21.envelope_633_i1 line 256
  123. def OAI.SnakyPrototype.Certificate21.childrenC_633_i1 line 257
  124. def OAI.SnakyPrototype.Certificate21.childrenD_633_i1 line 258
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_633_i1 line 259
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_633_i1 line 260
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_633_i1 line 261
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_633_i1 line 262
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_633_i1 line 263
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_633_i1 line 268
  131. def OAI.SnakyPrototype.Certificate21.required_633_i0 line 273
  132. def OAI.SnakyPrototype.Certificate21.envelope_633_i0 line 274
  133. def OAI.SnakyPrototype.Certificate21.childrenC_633_i0 line 275
  134. def OAI.SnakyPrototype.Certificate21.childrenD_633_i0 line 276
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_633_i0 line 277
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_633_i0 line 278
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_633_i0 line 279
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_633_i0 line 280
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_633_i0 line 281
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_633_i0 line 288
  141. def OAI.SnakyPrototype.Certificate21.required_633 line 293
  142. def OAI.SnakyPrototype.Certificate21.envelope_633 line 294
  143. def OAI.SnakyPrototype.Certificate21.childrenC_633 line 295
  144. def OAI.SnakyPrototype.Certificate21.childrenD_633 line 296
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_633 line 297
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_633 line 298
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_633 line 299
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_633 line 300
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_633 line 301
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_633 line 307
  151. def OAI.SnakyPrototype.Certificate21.required_637_i2 line 312
  152. def OAI.SnakyPrototype.Certificate21.envelope_637_i2 line 313
  153. def OAI.SnakyPrototype.Certificate21.childrenC_637_i2 line 314
  154. def OAI.SnakyPrototype.Certificate21.childrenD_637_i2 line 315
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_637_i2 line 316
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_637_i2 line 317
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_637_i2 line 318
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_637_i2 line 319
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_637_i2 line 320
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_637_i2 line 325
  161. def OAI.SnakyPrototype.Certificate21.required_637_i1 line 330
  162. def OAI.SnakyPrototype.Certificate21.envelope_637_i1 line 331
  163. def OAI.SnakyPrototype.Certificate21.childrenC_637_i1 line 332
  164. def OAI.SnakyPrototype.Certificate21.childrenD_637_i1 line 333
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_637_i1 line 334
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_637_i1 line 335
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_637_i1 line 336
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_637_i1 line 337
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_637_i1 line 338
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_637_i1 line 343
  171. def OAI.SnakyPrototype.Certificate21.required_637_i0 line 348
  172. def OAI.SnakyPrototype.Certificate21.envelope_637_i0 line 349
  173. def OAI.SnakyPrototype.Certificate21.childrenC_637_i0 line 350
  174. def OAI.SnakyPrototype.Certificate21.childrenD_637_i0 line 351
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_637_i0 line 352
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_637_i0 line 353
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_637_i0 line 354
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_637_i0 line 355
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_637_i0 line 356
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_637_i0 line 361
  181. def OAI.SnakyPrototype.Certificate21.required_637 line 366
  182. def OAI.SnakyPrototype.Certificate21.envelope_637 line 367
  183. def OAI.SnakyPrototype.Certificate21.childrenC_637 line 368
  184. def OAI.SnakyPrototype.Certificate21.childrenD_637 line 369
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_637 line 370
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_637 line 371
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_637 line 372
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_637 line 373
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_637 line 374
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_637 line 381
  191. def OAI.SnakyPrototype.Certificate21.required_671_i0 line 386
  192. def OAI.SnakyPrototype.Certificate21.envelope_671_i0 line 387
  193. def OAI.SnakyPrototype.Certificate21.childrenC_671_i0 line 388
  194. def OAI.SnakyPrototype.Certificate21.childrenD_671_i0 line 389
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_671_i0 line 390
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_671_i0 line 391
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_671_i0 line 392
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_671_i0 line 393
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_671_i0 line 394
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_671_i0 line 399
  201. def OAI.SnakyPrototype.Certificate21.required_671 line 404
  202. def OAI.SnakyPrototype.Certificate21.envelope_671 line 405
  203. def OAI.SnakyPrototype.Certificate21.childrenC_671 line 406
  204. def OAI.SnakyPrototype.Certificate21.childrenD_671 line 407
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_671 line 408
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_671 line 409
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_671 line 410
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_671 line 411
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_671 line 412
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_671 line 419
  211. def OAI.SnakyPrototype.Certificate21.required_680_i0 line 424
  212. def OAI.SnakyPrototype.Certificate21.envelope_680_i0 line 425
  213. def OAI.SnakyPrototype.Certificate21.childrenC_680_i0 line 426
  214. def OAI.SnakyPrototype.Certificate21.childrenD_680_i0 line 427
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_680_i0 line 428
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_680_i0 line 429
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_680_i0 line 430
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_680_i0 line 431
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_680_i0 line 432
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_680_i0 line 437
  221. def OAI.SnakyPrototype.Certificate21.required_680 line 442
  222. def OAI.SnakyPrototype.Certificate21.envelope_680 line 443
  223. def OAI.SnakyPrototype.Certificate21.childrenC_680 line 444
  224. def OAI.SnakyPrototype.Certificate21.childrenD_680 line 445
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_680 line 446
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_680 line 447
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_680 line 448
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_680 line 449
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_680 line 450
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_680 line 455
  231. def OAI.SnakyPrototype.Certificate21.height_593_i0 line 460
  232. def OAI.SnakyPrototype.Certificate21.childrenH_593_i0 line 461
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_593_i0 line 462
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_593_i0 line 463
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_593_i0 line 465
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_593_i0 line 469
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_593_i0 line 471
  238. def OAI.SnakyPrototype.Certificate21.checked_593_i0 line 475
  239. def OAI.SnakyPrototype.Certificate21.height_593 line 483
  240. def OAI.SnakyPrototype.Certificate21.childrenH_593 line 484
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_593 line 485
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_593 line 486
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_593 line 488
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_593 line 492
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_593 line 494
  246. def OAI.SnakyPrototype.Certificate21.checked_593 line 498
  247. def OAI.SnakyPrototype.Certificate21.height_610 line 506
  248. def OAI.SnakyPrototype.Certificate21.childrenH_610 line 507
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_610 line 508
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_610 line 509
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_610 line 511
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_610 line 515
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_610 line 517
  254. def OAI.SnakyPrototype.Certificate21.checked_610 line 521
  255. def OAI.SnakyPrototype.Certificate21.height_620_i0 line 529
  256. def OAI.SnakyPrototype.Certificate21.childrenH_620_i0 line 530
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_620_i0 line 531
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_620_i0 line 532
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_620_i0 line 534
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_620_i0 line 538
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_620_i0 line 540
  262. def OAI.SnakyPrototype.Certificate21.checked_620_i0 line 544
  263. def OAI.SnakyPrototype.Certificate21.height_620 line 552
  264. def OAI.SnakyPrototype.Certificate21.childrenH_620 line 553
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_620 line 554
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_620 line 555
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_620 line 557
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_620 line 561
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_620 line 563
  270. def OAI.SnakyPrototype.Certificate21.checked_620 line 567
  271. def OAI.SnakyPrototype.Certificate21.height_621_i0 line 575
  272. def OAI.SnakyPrototype.Certificate21.childrenH_621_i0 line 576
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_621_i0 line 577
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_621_i0 line 578
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_621_i0 line 580
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_621_i0 line 584
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_621_i0 line 586
  278. def OAI.SnakyPrototype.Certificate21.checked_621_i0 line 590
  279. def OAI.SnakyPrototype.Certificate21.height_621_i1 line 598
  280. def OAI.SnakyPrototype.Certificate21.childrenH_621_i1 line 599
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_621_i1 line 600
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_621_i1 line 601
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_621_i1 line 603
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_621_i1 line 607
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_621_i1 line 609
  286. def OAI.SnakyPrototype.Certificate21.checked_621_i1 line 613
  287. def OAI.SnakyPrototype.Certificate21.height_621 line 621
  288. def OAI.SnakyPrototype.Certificate21.childrenH_621 line 622
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_621 line 623
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_621 line 624
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_621 line 626
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_621 line 630
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_621 line 632
  294. def OAI.SnakyPrototype.Certificate21.checked_621 line 636
  295. def OAI.SnakyPrototype.Certificate21.height_628_i0 line 644
  296. def OAI.SnakyPrototype.Certificate21.childrenH_628_i0 line 645
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_628_i0 line 646
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_628_i0 line 647
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_628_i0 line 649
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_628_i0 line 653
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_628_i0 line 655
  302. def OAI.SnakyPrototype.Certificate21.checked_628_i0 line 659
  303. def OAI.SnakyPrototype.Certificate21.height_628_i1 line 667
  304. def OAI.SnakyPrototype.Certificate21.childrenH_628_i1 line 668
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_628_i1 line 669
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_628_i1 line 670
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_628_i1 line 672
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_628_i1 line 676
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_628_i1 line 678
  310. def OAI.SnakyPrototype.Certificate21.checked_628_i1 line 682
  311. def OAI.SnakyPrototype.Certificate21.height_628_i2 line 690
  312. def OAI.SnakyPrototype.Certificate21.childrenH_628_i2 line 691
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_628_i2 line 692
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_628_i2 line 693
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_628_i2 line 695
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_628_i2 line 699
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_628_i2 line 701
  318. def OAI.SnakyPrototype.Certificate21.checked_628_i2 line 705
  319. def OAI.SnakyPrototype.Certificate21.height_628 line 713
  320. def OAI.SnakyPrototype.Certificate21.childrenH_628 line 714
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_628 line 715
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_628 line 716
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_628 line 718
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_628 line 722
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_628 line 724
  326. def OAI.SnakyPrototype.Certificate21.checked_628 line 728
  327. def OAI.SnakyPrototype.Certificate21.height_633_i1 line 736
  328. def OAI.SnakyPrototype.Certificate21.childrenH_633_i1 line 737
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_633_i1 line 738
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_633_i1 line 739
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_633_i1 line 741
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_633_i1 line 745
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_633_i1 line 747
  334. def OAI.SnakyPrototype.Certificate21.checked_633_i1 line 751
  335. def OAI.SnakyPrototype.Certificate21.height_633_i0 line 759
  336. def OAI.SnakyPrototype.Certificate21.childrenH_633_i0 line 760
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_633_i0 line 761
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_633_i0 line 762
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_633_i0 line 764
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_633_i0 line 768
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_633_i0 line 770
  342. def OAI.SnakyPrototype.Certificate21.checked_633_i0 line 774
  343. def OAI.SnakyPrototype.Certificate21.height_633 line 782
  344. def OAI.SnakyPrototype.Certificate21.childrenH_633 line 783
  345. theorem OAI.SnakyPrototype.Certificate21.height_exact_633 line 784
  346. theorem OAI.SnakyPrototype.Certificate21.required_origin_633 line 785
  347. theorem OAI.SnakyPrototype.Certificate21.required_exact_633 line 787
  348. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_633 line 791
  349. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_633 line 793
  350. def OAI.SnakyPrototype.Certificate21.checked_633 line 797
  351. def OAI.SnakyPrototype.Certificate21.height_637_i2 line 805
  352. def OAI.SnakyPrototype.Certificate21.childrenH_637_i2 line 806
  353. theorem OAI.SnakyPrototype.Certificate21.height_exact_637_i2 line 807
  354. theorem OAI.SnakyPrototype.Certificate21.required_origin_637_i2 line 808
  355. theorem OAI.SnakyPrototype.Certificate21.required_exact_637_i2 line 810
  356. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_637_i2 line 814
  357. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_637_i2 line 816
  358. def OAI.SnakyPrototype.Certificate21.checked_637_i2 line 820
  359. def OAI.SnakyPrototype.Certificate21.height_637_i1 line 828
  360. def OAI.SnakyPrototype.Certificate21.childrenH_637_i1 line 829
  361. theorem OAI.SnakyPrototype.Certificate21.height_exact_637_i1 line 830
  362. theorem OAI.SnakyPrototype.Certificate21.required_origin_637_i1 line 831
  363. theorem OAI.SnakyPrototype.Certificate21.required_exact_637_i1 line 833
  364. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_637_i1 line 837
  365. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_637_i1 line 839
  366. def OAI.SnakyPrototype.Certificate21.checked_637_i1 line 843
  367. def OAI.SnakyPrototype.Certificate21.height_637_i0 line 851
  368. def OAI.SnakyPrototype.Certificate21.childrenH_637_i0 line 852
  369. theorem OAI.SnakyPrototype.Certificate21.height_exact_637_i0 line 853
  370. theorem OAI.SnakyPrototype.Certificate21.required_origin_637_i0 line 854
  371. theorem OAI.SnakyPrototype.Certificate21.required_exact_637_i0 line 856
  372. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_637_i0 line 860
  373. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_637_i0 line 862
  374. def OAI.SnakyPrototype.Certificate21.checked_637_i0 line 866
  375. def OAI.SnakyPrototype.Certificate21.height_637 line 874
  376. def OAI.SnakyPrototype.Certificate21.childrenH_637 line 875
  377. theorem OAI.SnakyPrototype.Certificate21.height_exact_637 line 876
  378. theorem OAI.SnakyPrototype.Certificate21.required_origin_637 line 877
  379. theorem OAI.SnakyPrototype.Certificate21.required_exact_637 line 879
  380. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_637 line 883
  381. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_637 line 885
  382. def OAI.SnakyPrototype.Certificate21.checked_637 line 889
  383. def OAI.SnakyPrototype.Certificate21.height_671_i0 line 897
  384. def OAI.SnakyPrototype.Certificate21.childrenH_671_i0 line 898
  385. theorem OAI.SnakyPrototype.Certificate21.height_exact_671_i0 line 899
  386. theorem OAI.SnakyPrototype.Certificate21.required_origin_671_i0 line 900
  387. theorem OAI.SnakyPrototype.Certificate21.required_exact_671_i0 line 902
  388. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_671_i0 line 906
  389. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_671_i0 line 908
  390. def OAI.SnakyPrototype.Certificate21.checked_671_i0 line 912
  391. def OAI.SnakyPrototype.Certificate21.height_671 line 920
  392. def OAI.SnakyPrototype.Certificate21.childrenH_671 line 921
  393. theorem OAI.SnakyPrototype.Certificate21.height_exact_671 line 922
  394. theorem OAI.SnakyPrototype.Certificate21.required_origin_671 line 923
  395. theorem OAI.SnakyPrototype.Certificate21.required_exact_671 line 925
  396. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_671 line 929
  397. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_671 line 931
  398. def OAI.SnakyPrototype.Certificate21.checked_671 line 935
  399. def OAI.SnakyPrototype.Certificate21.height_680_i0 line 943
  400. def OAI.SnakyPrototype.Certificate21.childrenH_680_i0 line 944
  401. theorem OAI.SnakyPrototype.Certificate21.height_exact_680_i0 line 945
  402. theorem OAI.SnakyPrototype.Certificate21.required_origin_680_i0 line 946
  403. theorem OAI.SnakyPrototype.Certificate21.required_exact_680_i0 line 948
  404. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_680_i0 line 952
  405. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_680_i0 line 954
  406. def OAI.SnakyPrototype.Certificate21.checked_680_i0 line 958
  407. def OAI.SnakyPrototype.Certificate21.height_680 line 966
  408. def OAI.SnakyPrototype.Certificate21.childrenH_680 line 967
  409. theorem OAI.SnakyPrototype.Certificate21.height_exact_680 line 968
  410. theorem OAI.SnakyPrototype.Certificate21.required_origin_680 line 969
  411. theorem OAI.SnakyPrototype.Certificate21.required_exact_680 line 971
  412. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_680 line 975
  413. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_680 line 977
  414. def OAI.SnakyPrototype.Certificate21.checked_680 line 981