OAI/GameTheory/SnakyTwentyOne/Cards/Height06Part06.lean

GitHub source file

396 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_521_i1 line 15
  2. def OAI.SnakyPrototype.Certificate21.envelope_521_i1 line 16
  3. def OAI.SnakyPrototype.Certificate21.childrenC_521_i1 line 17
  4. def OAI.SnakyPrototype.Certificate21.childrenD_521_i1 line 18
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_521_i1 line 19
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_521_i1 line 20
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_521_i1 line 21
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_521_i1 line 22
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_521_i1 line 23
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_521_i1 line 28
  11. def OAI.SnakyPrototype.Certificate21.required_521_i0 line 33
  12. def OAI.SnakyPrototype.Certificate21.envelope_521_i0 line 34
  13. def OAI.SnakyPrototype.Certificate21.childrenC_521_i0 line 35
  14. def OAI.SnakyPrototype.Certificate21.childrenD_521_i0 line 36
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_521_i0 line 37
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_521_i0 line 38
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_521_i0 line 39
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_521_i0 line 40
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_521_i0 line 41
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_521_i0 line 46
  21. def OAI.SnakyPrototype.Certificate21.required_521 line 51
  22. def OAI.SnakyPrototype.Certificate21.envelope_521 line 52
  23. def OAI.SnakyPrototype.Certificate21.childrenC_521 line 53
  24. def OAI.SnakyPrototype.Certificate21.childrenD_521 line 54
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_521 line 55
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_521 line 56
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_521 line 57
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_521 line 58
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_521 line 59
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_521 line 64
  31. def OAI.SnakyPrototype.Certificate21.required_525_i1 line 69
  32. def OAI.SnakyPrototype.Certificate21.envelope_525_i1 line 70
  33. def OAI.SnakyPrototype.Certificate21.childrenC_525_i1 line 71
  34. def OAI.SnakyPrototype.Certificate21.childrenD_525_i1 line 72
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_525_i1 line 73
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_525_i1 line 74
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_525_i1 line 75
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_525_i1 line 76
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_525_i1 line 77
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_525_i1 line 83
  41. def OAI.SnakyPrototype.Certificate21.required_525_i0 line 88
  42. def OAI.SnakyPrototype.Certificate21.envelope_525_i0 line 89
  43. def OAI.SnakyPrototype.Certificate21.childrenC_525_i0 line 90
  44. def OAI.SnakyPrototype.Certificate21.childrenD_525_i0 line 91
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_525_i0 line 92
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_525_i0 line 93
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_525_i0 line 94
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_525_i0 line 95
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_525_i0 line 96
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_525_i0 line 101
  51. def OAI.SnakyPrototype.Certificate21.required_525 line 106
  52. def OAI.SnakyPrototype.Certificate21.envelope_525 line 107
  53. def OAI.SnakyPrototype.Certificate21.childrenC_525 line 108
  54. def OAI.SnakyPrototype.Certificate21.childrenD_525 line 109
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_525 line 110
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_525 line 111
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_525 line 112
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_525 line 113
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_525 line 114
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_525 line 119
  61. def OAI.SnakyPrototype.Certificate21.required_544_i1 line 124
  62. def OAI.SnakyPrototype.Certificate21.envelope_544_i1 line 125
  63. def OAI.SnakyPrototype.Certificate21.childrenC_544_i1 line 126
  64. def OAI.SnakyPrototype.Certificate21.childrenD_544_i1 line 127
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_544_i1 line 128
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_544_i1 line 129
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_544_i1 line 130
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_544_i1 line 131
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_544_i1 line 132
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_544_i1 line 137
  71. def OAI.SnakyPrototype.Certificate21.required_544_i0 line 142
  72. def OAI.SnakyPrototype.Certificate21.envelope_544_i0 line 143
  73. def OAI.SnakyPrototype.Certificate21.childrenC_544_i0 line 144
  74. def OAI.SnakyPrototype.Certificate21.childrenD_544_i0 line 145
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_544_i0 line 146
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_544_i0 line 147
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_544_i0 line 148
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_544_i0 line 149
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_544_i0 line 150
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_544_i0 line 156
  81. def OAI.SnakyPrototype.Certificate21.required_544 line 161
  82. def OAI.SnakyPrototype.Certificate21.envelope_544 line 162
  83. def OAI.SnakyPrototype.Certificate21.childrenC_544 line 163
  84. def OAI.SnakyPrototype.Certificate21.childrenD_544 line 164
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_544 line 165
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_544 line 166
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_544 line 167
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_544 line 168
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_544 line 169
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_544 line 174
  91. def OAI.SnakyPrototype.Certificate21.required_600_i0 line 179
  92. def OAI.SnakyPrototype.Certificate21.envelope_600_i0 line 180
  93. def OAI.SnakyPrototype.Certificate21.childrenC_600_i0 line 181
  94. def OAI.SnakyPrototype.Certificate21.childrenD_600_i0 line 182
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_600_i0 line 183
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_600_i0 line 184
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_600_i0 line 185
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_600_i0 line 186
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_600_i0 line 187
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_600_i0 line 192
  101. def OAI.SnakyPrototype.Certificate21.required_600 line 197
  102. def OAI.SnakyPrototype.Certificate21.envelope_600 line 198
  103. def OAI.SnakyPrototype.Certificate21.childrenC_600 line 199
  104. def OAI.SnakyPrototype.Certificate21.childrenD_600 line 200
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_600 line 201
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_600 line 202
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_600 line 203
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_600 line 204
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_600 line 205
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_600 line 210
  111. def OAI.SnakyPrototype.Certificate21.required_606_i0 line 215
  112. def OAI.SnakyPrototype.Certificate21.envelope_606_i0 line 216
  113. def OAI.SnakyPrototype.Certificate21.childrenC_606_i0 line 217
  114. def OAI.SnakyPrototype.Certificate21.childrenD_606_i0 line 218
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_606_i0 line 219
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_606_i0 line 220
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_606_i0 line 221
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_606_i0 line 222
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_606_i0 line 223
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_606_i0 line 228
  121. def OAI.SnakyPrototype.Certificate21.required_606 line 233
  122. def OAI.SnakyPrototype.Certificate21.envelope_606 line 234
  123. def OAI.SnakyPrototype.Certificate21.childrenC_606 line 235
  124. def OAI.SnakyPrototype.Certificate21.childrenD_606 line 236
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_606 line 237
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_606 line 238
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_606 line 239
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_606 line 240
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_606 line 241
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_606 line 247
  131. def OAI.SnakyPrototype.Certificate21.required_609_i0 line 252
  132. def OAI.SnakyPrototype.Certificate21.envelope_609_i0 line 253
  133. def OAI.SnakyPrototype.Certificate21.childrenC_609_i0 line 254
  134. def OAI.SnakyPrototype.Certificate21.childrenD_609_i0 line 255
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_609_i0 line 256
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_609_i0 line 257
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_609_i0 line 258
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_609_i0 line 259
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_609_i0 line 260
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_609_i0 line 265
  141. def OAI.SnakyPrototype.Certificate21.required_609_i1 line 270
  142. def OAI.SnakyPrototype.Certificate21.envelope_609_i1 line 271
  143. def OAI.SnakyPrototype.Certificate21.childrenC_609_i1 line 272
  144. def OAI.SnakyPrototype.Certificate21.childrenD_609_i1 line 273
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_609_i1 line 274
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_609_i1 line 275
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_609_i1 line 276
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_609_i1 line 277
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_609_i1 line 278
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_609_i1 line 283
  151. def OAI.SnakyPrototype.Certificate21.required_609 line 288
  152. def OAI.SnakyPrototype.Certificate21.envelope_609 line 289
  153. def OAI.SnakyPrototype.Certificate21.childrenC_609 line 290
  154. def OAI.SnakyPrototype.Certificate21.childrenD_609 line 291
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_609 line 292
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_609 line 293
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_609 line 294
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_609 line 295
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_609 line 296
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_609 line 301
  161. def OAI.SnakyPrototype.Certificate21.required_611_i0 line 306
  162. def OAI.SnakyPrototype.Certificate21.envelope_611_i0 line 307
  163. def OAI.SnakyPrototype.Certificate21.childrenC_611_i0 line 308
  164. def OAI.SnakyPrototype.Certificate21.childrenD_611_i0 line 309
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_611_i0 line 310
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_611_i0 line 311
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_611_i0 line 312
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_611_i0 line 313
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_611_i0 line 314
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_611_i0 line 320
  171. def OAI.SnakyPrototype.Certificate21.required_611 line 325
  172. def OAI.SnakyPrototype.Certificate21.envelope_611 line 326
  173. def OAI.SnakyPrototype.Certificate21.childrenC_611 line 327
  174. def OAI.SnakyPrototype.Certificate21.childrenD_611 line 328
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_611 line 329
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_611 line 330
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_611 line 331
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_611 line 332
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_611 line 333
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_611 line 339
  181. def OAI.SnakyPrototype.Certificate21.required_641_i0 line 344
  182. def OAI.SnakyPrototype.Certificate21.envelope_641_i0 line 345
  183. def OAI.SnakyPrototype.Certificate21.childrenC_641_i0 line 346
  184. def OAI.SnakyPrototype.Certificate21.childrenD_641_i0 line 347
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_641_i0 line 348
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_641_i0 line 349
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_641_i0 line 350
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_641_i0 line 351
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_641_i0 line 352
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_641_i0 line 358
  191. def OAI.SnakyPrototype.Certificate21.required_641 line 363
  192. def OAI.SnakyPrototype.Certificate21.envelope_641 line 364
  193. def OAI.SnakyPrototype.Certificate21.childrenC_641 line 365
  194. def OAI.SnakyPrototype.Certificate21.childrenD_641 line 366
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_641 line 367
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_641 line 368
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_641 line 369
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_641 line 370
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_641 line 371
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_641 line 377
  201. def OAI.SnakyPrototype.Certificate21.required_714_i0 line 382
  202. def OAI.SnakyPrototype.Certificate21.envelope_714_i0 line 383
  203. def OAI.SnakyPrototype.Certificate21.childrenC_714_i0 line 384
  204. def OAI.SnakyPrototype.Certificate21.childrenD_714_i0 line 385
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_714_i0 line 386
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_714_i0 line 387
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_714_i0 line 388
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_714_i0 line 389
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_714_i0 line 390
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_714_i0 line 395
  211. def OAI.SnakyPrototype.Certificate21.required_714 line 400
  212. def OAI.SnakyPrototype.Certificate21.envelope_714 line 401
  213. def OAI.SnakyPrototype.Certificate21.childrenC_714 line 402
  214. def OAI.SnakyPrototype.Certificate21.childrenD_714 line 403
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_714 line 404
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_714 line 405
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_714 line 406
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_714 line 407
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_714 line 408
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_714 line 414
  221. def OAI.SnakyPrototype.Certificate21.height_521_i1 line 419
  222. def OAI.SnakyPrototype.Certificate21.childrenH_521_i1 line 420
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_521_i1 line 421
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_521_i1 line 422
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_521_i1 line 424
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_521_i1 line 428
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_521_i1 line 430
  228. def OAI.SnakyPrototype.Certificate21.checked_521_i1 line 434
  229. def OAI.SnakyPrototype.Certificate21.height_521_i0 line 442
  230. def OAI.SnakyPrototype.Certificate21.childrenH_521_i0 line 443
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_521_i0 line 444
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_521_i0 line 445
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_521_i0 line 447
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_521_i0 line 451
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_521_i0 line 453
  236. def OAI.SnakyPrototype.Certificate21.checked_521_i0 line 457
  237. def OAI.SnakyPrototype.Certificate21.height_521 line 465
  238. def OAI.SnakyPrototype.Certificate21.childrenH_521 line 466
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_521 line 467
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_521 line 468
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_521 line 470
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_521 line 474
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_521 line 476
  244. def OAI.SnakyPrototype.Certificate21.checked_521 line 480
  245. def OAI.SnakyPrototype.Certificate21.height_525_i1 line 488
  246. def OAI.SnakyPrototype.Certificate21.childrenH_525_i1 line 489
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_525_i1 line 490
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_525_i1 line 491
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_525_i1 line 493
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_525_i1 line 497
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_525_i1 line 499
  252. def OAI.SnakyPrototype.Certificate21.checked_525_i1 line 503
  253. def OAI.SnakyPrototype.Certificate21.height_525_i0 line 511
  254. def OAI.SnakyPrototype.Certificate21.childrenH_525_i0 line 512
  255. theorem OAI.SnakyPrototype.Certificate21.height_exact_525_i0 line 513
  256. theorem OAI.SnakyPrototype.Certificate21.required_origin_525_i0 line 514
  257. theorem OAI.SnakyPrototype.Certificate21.required_exact_525_i0 line 516
  258. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_525_i0 line 520
  259. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_525_i0 line 522
  260. def OAI.SnakyPrototype.Certificate21.checked_525_i0 line 526
  261. def OAI.SnakyPrototype.Certificate21.height_525 line 534
  262. def OAI.SnakyPrototype.Certificate21.childrenH_525 line 535
  263. theorem OAI.SnakyPrototype.Certificate21.height_exact_525 line 536
  264. theorem OAI.SnakyPrototype.Certificate21.required_origin_525 line 537
  265. theorem OAI.SnakyPrototype.Certificate21.required_exact_525 line 539
  266. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_525 line 543
  267. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_525 line 545
  268. def OAI.SnakyPrototype.Certificate21.checked_525 line 549
  269. def OAI.SnakyPrototype.Certificate21.height_544_i1 line 557
  270. def OAI.SnakyPrototype.Certificate21.childrenH_544_i1 line 558
  271. theorem OAI.SnakyPrototype.Certificate21.height_exact_544_i1 line 559
  272. theorem OAI.SnakyPrototype.Certificate21.required_origin_544_i1 line 560
  273. theorem OAI.SnakyPrototype.Certificate21.required_exact_544_i1 line 562
  274. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_544_i1 line 566
  275. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_544_i1 line 568
  276. def OAI.SnakyPrototype.Certificate21.checked_544_i1 line 572
  277. def OAI.SnakyPrototype.Certificate21.height_544_i0 line 580
  278. def OAI.SnakyPrototype.Certificate21.childrenH_544_i0 line 581
  279. theorem OAI.SnakyPrototype.Certificate21.height_exact_544_i0 line 582
  280. theorem OAI.SnakyPrototype.Certificate21.required_origin_544_i0 line 583
  281. theorem OAI.SnakyPrototype.Certificate21.required_exact_544_i0 line 585
  282. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_544_i0 line 589
  283. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_544_i0 line 591
  284. def OAI.SnakyPrototype.Certificate21.checked_544_i0 line 595
  285. def OAI.SnakyPrototype.Certificate21.height_544 line 603
  286. def OAI.SnakyPrototype.Certificate21.childrenH_544 line 604
  287. theorem OAI.SnakyPrototype.Certificate21.height_exact_544 line 605
  288. theorem OAI.SnakyPrototype.Certificate21.required_origin_544 line 606
  289. theorem OAI.SnakyPrototype.Certificate21.required_exact_544 line 608
  290. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_544 line 612
  291. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_544 line 614
  292. def OAI.SnakyPrototype.Certificate21.checked_544 line 618
  293. def OAI.SnakyPrototype.Certificate21.height_600_i0 line 626
  294. def OAI.SnakyPrototype.Certificate21.childrenH_600_i0 line 627
  295. theorem OAI.SnakyPrototype.Certificate21.height_exact_600_i0 line 628
  296. theorem OAI.SnakyPrototype.Certificate21.required_origin_600_i0 line 629
  297. theorem OAI.SnakyPrototype.Certificate21.required_exact_600_i0 line 631
  298. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_600_i0 line 635
  299. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_600_i0 line 637
  300. def OAI.SnakyPrototype.Certificate21.checked_600_i0 line 641
  301. def OAI.SnakyPrototype.Certificate21.height_600 line 649
  302. def OAI.SnakyPrototype.Certificate21.childrenH_600 line 650
  303. theorem OAI.SnakyPrototype.Certificate21.height_exact_600 line 651
  304. theorem OAI.SnakyPrototype.Certificate21.required_origin_600 line 652
  305. theorem OAI.SnakyPrototype.Certificate21.required_exact_600 line 654
  306. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_600 line 658
  307. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_600 line 660
  308. def OAI.SnakyPrototype.Certificate21.checked_600 line 664
  309. def OAI.SnakyPrototype.Certificate21.height_606_i0 line 672
  310. def OAI.SnakyPrototype.Certificate21.childrenH_606_i0 line 673
  311. theorem OAI.SnakyPrototype.Certificate21.height_exact_606_i0 line 674
  312. theorem OAI.SnakyPrototype.Certificate21.required_origin_606_i0 line 675
  313. theorem OAI.SnakyPrototype.Certificate21.required_exact_606_i0 line 677
  314. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_606_i0 line 681
  315. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_606_i0 line 683
  316. def OAI.SnakyPrototype.Certificate21.checked_606_i0 line 687
  317. def OAI.SnakyPrototype.Certificate21.height_606 line 695
  318. def OAI.SnakyPrototype.Certificate21.childrenH_606 line 696
  319. theorem OAI.SnakyPrototype.Certificate21.height_exact_606 line 697
  320. theorem OAI.SnakyPrototype.Certificate21.required_origin_606 line 698
  321. theorem OAI.SnakyPrototype.Certificate21.required_exact_606 line 700
  322. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_606 line 704
  323. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_606 line 706
  324. def OAI.SnakyPrototype.Certificate21.checked_606 line 710
  325. def OAI.SnakyPrototype.Certificate21.height_609_i0 line 718
  326. def OAI.SnakyPrototype.Certificate21.childrenH_609_i0 line 719
  327. theorem OAI.SnakyPrototype.Certificate21.height_exact_609_i0 line 720
  328. theorem OAI.SnakyPrototype.Certificate21.required_origin_609_i0 line 721
  329. theorem OAI.SnakyPrototype.Certificate21.required_exact_609_i0 line 723
  330. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_609_i0 line 727
  331. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_609_i0 line 729
  332. def OAI.SnakyPrototype.Certificate21.checked_609_i0 line 733
  333. def OAI.SnakyPrototype.Certificate21.height_609_i1 line 741
  334. def OAI.SnakyPrototype.Certificate21.childrenH_609_i1 line 742
  335. theorem OAI.SnakyPrototype.Certificate21.height_exact_609_i1 line 743
  336. theorem OAI.SnakyPrototype.Certificate21.required_origin_609_i1 line 744
  337. theorem OAI.SnakyPrototype.Certificate21.required_exact_609_i1 line 746
  338. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_609_i1 line 750
  339. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_609_i1 line 752
  340. def OAI.SnakyPrototype.Certificate21.checked_609_i1 line 756
  341. def OAI.SnakyPrototype.Certificate21.height_609 line 764
  342. def OAI.SnakyPrototype.Certificate21.childrenH_609 line 765
  343. theorem OAI.SnakyPrototype.Certificate21.height_exact_609 line 766
  344. theorem OAI.SnakyPrototype.Certificate21.required_origin_609 line 767
  345. theorem OAI.SnakyPrototype.Certificate21.required_exact_609 line 769
  346. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_609 line 773
  347. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_609 line 775
  348. def OAI.SnakyPrototype.Certificate21.checked_609 line 779
  349. def OAI.SnakyPrototype.Certificate21.height_611_i0 line 787
  350. def OAI.SnakyPrototype.Certificate21.childrenH_611_i0 line 788
  351. theorem OAI.SnakyPrototype.Certificate21.height_exact_611_i0 line 789
  352. theorem OAI.SnakyPrototype.Certificate21.required_origin_611_i0 line 790
  353. theorem OAI.SnakyPrototype.Certificate21.required_exact_611_i0 line 792
  354. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_611_i0 line 796
  355. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_611_i0 line 798
  356. def OAI.SnakyPrototype.Certificate21.checked_611_i0 line 802
  357. def OAI.SnakyPrototype.Certificate21.height_611 line 810
  358. def OAI.SnakyPrototype.Certificate21.childrenH_611 line 811
  359. theorem OAI.SnakyPrototype.Certificate21.height_exact_611 line 812
  360. theorem OAI.SnakyPrototype.Certificate21.required_origin_611 line 813
  361. theorem OAI.SnakyPrototype.Certificate21.required_exact_611 line 815
  362. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_611 line 819
  363. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_611 line 821
  364. def OAI.SnakyPrototype.Certificate21.checked_611 line 825
  365. def OAI.SnakyPrototype.Certificate21.height_641_i0 line 833
  366. def OAI.SnakyPrototype.Certificate21.childrenH_641_i0 line 834
  367. theorem OAI.SnakyPrototype.Certificate21.height_exact_641_i0 line 835
  368. theorem OAI.SnakyPrototype.Certificate21.required_origin_641_i0 line 836
  369. theorem OAI.SnakyPrototype.Certificate21.required_exact_641_i0 line 838
  370. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_641_i0 line 842
  371. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_641_i0 line 844
  372. def OAI.SnakyPrototype.Certificate21.checked_641_i0 line 848
  373. def OAI.SnakyPrototype.Certificate21.height_641 line 856
  374. def OAI.SnakyPrototype.Certificate21.childrenH_641 line 857
  375. theorem OAI.SnakyPrototype.Certificate21.height_exact_641 line 858
  376. theorem OAI.SnakyPrototype.Certificate21.required_origin_641 line 859
  377. theorem OAI.SnakyPrototype.Certificate21.required_exact_641 line 861
  378. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_641 line 865
  379. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_641 line 867
  380. def OAI.SnakyPrototype.Certificate21.checked_641 line 871
  381. def OAI.SnakyPrototype.Certificate21.height_714_i0 line 879
  382. def OAI.SnakyPrototype.Certificate21.childrenH_714_i0 line 880
  383. theorem OAI.SnakyPrototype.Certificate21.height_exact_714_i0 line 881
  384. theorem OAI.SnakyPrototype.Certificate21.required_origin_714_i0 line 882
  385. theorem OAI.SnakyPrototype.Certificate21.required_exact_714_i0 line 884
  386. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_714_i0 line 888
  387. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_714_i0 line 890
  388. def OAI.SnakyPrototype.Certificate21.checked_714_i0 line 894
  389. def OAI.SnakyPrototype.Certificate21.height_714 line 902
  390. def OAI.SnakyPrototype.Certificate21.childrenH_714 line 903
  391. theorem OAI.SnakyPrototype.Certificate21.height_exact_714 line 904
  392. theorem OAI.SnakyPrototype.Certificate21.required_origin_714 line 905
  393. theorem OAI.SnakyPrototype.Certificate21.required_exact_714 line 907
  394. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_714 line 911
  395. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_714 line 913
  396. def OAI.SnakyPrototype.Certificate21.checked_714 line 917