OAI/GameTheory/SnakyTwentyOne/Cards/Height10Part02.lean

GitHub source file

414 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_529_i4 line 29
  2. def OAI.SnakyPrototype.Certificate21.envelope_529_i4 line 30
  3. def OAI.SnakyPrototype.Certificate21.childrenC_529_i4 line 31
  4. def OAI.SnakyPrototype.Certificate21.childrenD_529_i4 line 32
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_529_i4 line 33
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_529_i4 line 34
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_529_i4 line 35
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_529_i4 line 36
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_529_i4 line 37
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_529_i4 line 42
  11. def OAI.SnakyPrototype.Certificate21.required_529_i5 line 47
  12. def OAI.SnakyPrototype.Certificate21.envelope_529_i5 line 48
  13. def OAI.SnakyPrototype.Certificate21.childrenC_529_i5 line 49
  14. def OAI.SnakyPrototype.Certificate21.childrenD_529_i5 line 50
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_529_i5 line 51
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_529_i5 line 52
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_529_i5 line 53
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_529_i5 line 54
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_529_i5 line 55
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_529_i5 line 60
  21. def OAI.SnakyPrototype.Certificate21.required_529_i3 line 65
  22. def OAI.SnakyPrototype.Certificate21.envelope_529_i3 line 66
  23. def OAI.SnakyPrototype.Certificate21.childrenC_529_i3 line 67
  24. def OAI.SnakyPrototype.Certificate21.childrenD_529_i3 line 68
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_529_i3 line 69
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_529_i3 line 70
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_529_i3 line 71
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_529_i3 line 72
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_529_i3 line 73
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_529_i3 line 78
  31. def OAI.SnakyPrototype.Certificate21.required_529_i2 line 83
  32. def OAI.SnakyPrototype.Certificate21.envelope_529_i2 line 84
  33. def OAI.SnakyPrototype.Certificate21.childrenC_529_i2 line 85
  34. def OAI.SnakyPrototype.Certificate21.childrenD_529_i2 line 86
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_529_i2 line 87
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_529_i2 line 88
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_529_i2 line 89
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_529_i2 line 90
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_529_i2 line 91
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_529_i2 line 96
  41. def OAI.SnakyPrototype.Certificate21.required_529_i1 line 101
  42. def OAI.SnakyPrototype.Certificate21.envelope_529_i1 line 102
  43. def OAI.SnakyPrototype.Certificate21.childrenC_529_i1 line 103
  44. def OAI.SnakyPrototype.Certificate21.childrenD_529_i1 line 104
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_529_i1 line 105
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_529_i1 line 106
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_529_i1 line 107
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_529_i1 line 108
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_529_i1 line 109
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_529_i1 line 114
  51. def OAI.SnakyPrototype.Certificate21.required_529_i0 line 119
  52. def OAI.SnakyPrototype.Certificate21.envelope_529_i0 line 120
  53. def OAI.SnakyPrototype.Certificate21.childrenC_529_i0 line 121
  54. def OAI.SnakyPrototype.Certificate21.childrenD_529_i0 line 122
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_529_i0 line 123
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_529_i0 line 124
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_529_i0 line 125
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_529_i0 line 126
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_529_i0 line 127
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_529_i0 line 133
  61. def OAI.SnakyPrototype.Certificate21.required_529 line 138
  62. def OAI.SnakyPrototype.Certificate21.envelope_529 line 139
  63. def OAI.SnakyPrototype.Certificate21.childrenC_529 line 140
  64. def OAI.SnakyPrototype.Certificate21.childrenD_529 line 141
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_529 line 142
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_529 line 143
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_529 line 144
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_529 line 145
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_529 line 146
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_529 line 156
  71. def OAI.SnakyPrototype.Certificate21.required_535 line 161
  72. def OAI.SnakyPrototype.Certificate21.envelope_535 line 162
  73. def OAI.SnakyPrototype.Certificate21.childrenC_535 line 163
  74. def OAI.SnakyPrototype.Certificate21.childrenD_535 line 164
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_535 line 165
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_535 line 166
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_535 line 167
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_535 line 168
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_535 line 169
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_535 line 179
  81. def OAI.SnakyPrototype.Certificate21.required_540_i0 line 184
  82. def OAI.SnakyPrototype.Certificate21.envelope_540_i0 line 185
  83. def OAI.SnakyPrototype.Certificate21.childrenC_540_i0 line 186
  84. def OAI.SnakyPrototype.Certificate21.childrenD_540_i0 line 187
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_540_i0 line 188
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_540_i0 line 189
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_540_i0 line 190
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_540_i0 line 191
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_540_i0 line 192
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_540_i0 line 197
  91. def OAI.SnakyPrototype.Certificate21.required_540_i3 line 202
  92. def OAI.SnakyPrototype.Certificate21.envelope_540_i3 line 203
  93. def OAI.SnakyPrototype.Certificate21.childrenC_540_i3 line 204
  94. def OAI.SnakyPrototype.Certificate21.childrenD_540_i3 line 205
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_540_i3 line 206
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_540_i3 line 207
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_540_i3 line 208
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_540_i3 line 209
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_540_i3 line 210
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_540_i3 line 216
  101. def OAI.SnakyPrototype.Certificate21.required_540_i2 line 221
  102. def OAI.SnakyPrototype.Certificate21.envelope_540_i2 line 222
  103. def OAI.SnakyPrototype.Certificate21.childrenC_540_i2 line 223
  104. def OAI.SnakyPrototype.Certificate21.childrenD_540_i2 line 224
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_540_i2 line 225
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_540_i2 line 226
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_540_i2 line 227
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_540_i2 line 228
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_540_i2 line 229
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_540_i2 line 234
  111. def OAI.SnakyPrototype.Certificate21.required_540_i1 line 239
  112. def OAI.SnakyPrototype.Certificate21.envelope_540_i1 line 240
  113. def OAI.SnakyPrototype.Certificate21.childrenC_540_i1 line 241
  114. def OAI.SnakyPrototype.Certificate21.childrenD_540_i1 line 242
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_540_i1 line 243
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_540_i1 line 244
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_540_i1 line 245
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_540_i1 line 246
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_540_i1 line 247
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_540_i1 line 252
  121. def OAI.SnakyPrototype.Certificate21.required_540 line 257
  122. def OAI.SnakyPrototype.Certificate21.envelope_540 line 258
  123. def OAI.SnakyPrototype.Certificate21.childrenC_540 line 259
  124. def OAI.SnakyPrototype.Certificate21.childrenD_540 line 260
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_540 line 261
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_540 line 262
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_540 line 263
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_540 line 264
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_540 line 265
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_540 line 271
  131. def OAI.SnakyPrototype.Certificate21.required_541_i6 line 276
  132. def OAI.SnakyPrototype.Certificate21.envelope_541_i6 line 277
  133. def OAI.SnakyPrototype.Certificate21.childrenC_541_i6 line 278
  134. def OAI.SnakyPrototype.Certificate21.childrenD_541_i6 line 279
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_541_i6 line 280
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_541_i6 line 281
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_541_i6 line 282
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_541_i6 line 283
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_541_i6 line 284
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_541_i6 line 289
  141. def OAI.SnakyPrototype.Certificate21.required_541_i5 line 294
  142. def OAI.SnakyPrototype.Certificate21.envelope_541_i5 line 295
  143. def OAI.SnakyPrototype.Certificate21.childrenC_541_i5 line 296
  144. def OAI.SnakyPrototype.Certificate21.childrenD_541_i5 line 297
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_541_i5 line 298
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_541_i5 line 299
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_541_i5 line 300
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_541_i5 line 301
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_541_i5 line 302
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_541_i5 line 307
  151. def OAI.SnakyPrototype.Certificate21.required_541_i4 line 312
  152. def OAI.SnakyPrototype.Certificate21.envelope_541_i4 line 313
  153. def OAI.SnakyPrototype.Certificate21.childrenC_541_i4 line 314
  154. def OAI.SnakyPrototype.Certificate21.childrenD_541_i4 line 315
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_541_i4 line 316
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_541_i4 line 317
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_541_i4 line 318
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_541_i4 line 319
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_541_i4 line 320
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_541_i4 line 326
  161. def OAI.SnakyPrototype.Certificate21.required_541_i3 line 331
  162. def OAI.SnakyPrototype.Certificate21.envelope_541_i3 line 332
  163. def OAI.SnakyPrototype.Certificate21.childrenC_541_i3 line 333
  164. def OAI.SnakyPrototype.Certificate21.childrenD_541_i3 line 334
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_541_i3 line 335
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_541_i3 line 336
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_541_i3 line 337
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_541_i3 line 338
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_541_i3 line 339
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_541_i3 line 344
  171. def OAI.SnakyPrototype.Certificate21.required_541_i2 line 349
  172. def OAI.SnakyPrototype.Certificate21.envelope_541_i2 line 350
  173. def OAI.SnakyPrototype.Certificate21.childrenC_541_i2 line 351
  174. def OAI.SnakyPrototype.Certificate21.childrenD_541_i2 line 352
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_541_i2 line 353
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_541_i2 line 354
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_541_i2 line 355
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_541_i2 line 356
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_541_i2 line 357
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_541_i2 line 362
  181. def OAI.SnakyPrototype.Certificate21.required_541_i1 line 367
  182. def OAI.SnakyPrototype.Certificate21.envelope_541_i1 line 368
  183. def OAI.SnakyPrototype.Certificate21.childrenC_541_i1 line 369
  184. def OAI.SnakyPrototype.Certificate21.childrenD_541_i1 line 370
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_541_i1 line 371
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_541_i1 line 372
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_541_i1 line 373
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_541_i1 line 374
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_541_i1 line 375
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_541_i1 line 380
  191. def OAI.SnakyPrototype.Certificate21.required_541_i0 line 385
  192. def OAI.SnakyPrototype.Certificate21.envelope_541_i0 line 386
  193. def OAI.SnakyPrototype.Certificate21.childrenC_541_i0 line 387
  194. def OAI.SnakyPrototype.Certificate21.childrenD_541_i0 line 388
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_541_i0 line 389
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_541_i0 line 390
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_541_i0 line 391
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_541_i0 line 392
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_541_i0 line 393
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_541_i0 line 398
  201. def OAI.SnakyPrototype.Certificate21.required_541 line 403
  202. def OAI.SnakyPrototype.Certificate21.envelope_541 line 404
  203. def OAI.SnakyPrototype.Certificate21.childrenC_541 line 405
  204. def OAI.SnakyPrototype.Certificate21.childrenD_541 line 406
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_541 line 407
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_541 line 408
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_541 line 409
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_541 line 410
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_541 line 411
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_541 line 416
  211. def OAI.SnakyPrototype.Certificate21.required_545_i0 line 421
  212. def OAI.SnakyPrototype.Certificate21.envelope_545_i0 line 422
  213. def OAI.SnakyPrototype.Certificate21.childrenC_545_i0 line 423
  214. def OAI.SnakyPrototype.Certificate21.childrenD_545_i0 line 424
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_545_i0 line 425
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_545_i0 line 426
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_545_i0 line 427
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_545_i0 line 428
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_545_i0 line 429
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_545_i0 line 436
  221. def OAI.SnakyPrototype.Certificate21.required_545 line 441
  222. def OAI.SnakyPrototype.Certificate21.envelope_545 line 442
  223. def OAI.SnakyPrototype.Certificate21.childrenC_545 line 443
  224. def OAI.SnakyPrototype.Certificate21.childrenD_545 line 444
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_545 line 445
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_545 line 446
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_545 line 447
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_545 line 448
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_545 line 449
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_545 line 456
  231. def OAI.SnakyPrototype.Certificate21.height_529_i4 line 461
  232. def OAI.SnakyPrototype.Certificate21.childrenH_529_i4 line 462
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_529_i4 line 463
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_529_i4 line 464
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_529_i4 line 466
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_529_i4 line 470
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_529_i4 line 472
  238. def OAI.SnakyPrototype.Certificate21.checked_529_i4 line 476
  239. def OAI.SnakyPrototype.Certificate21.height_529_i5 line 484
  240. def OAI.SnakyPrototype.Certificate21.childrenH_529_i5 line 485
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_529_i5 line 486
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_529_i5 line 487
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_529_i5 line 489
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_529_i5 line 493
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_529_i5 line 495
  246. def OAI.SnakyPrototype.Certificate21.checked_529_i5 line 499
  247. def OAI.SnakyPrototype.Certificate21.height_529_i3 line 507
  248. def OAI.SnakyPrototype.Certificate21.childrenH_529_i3 line 508
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_529_i3 line 509
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_529_i3 line 510
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_529_i3 line 512
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_529_i3 line 516
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_529_i3 line 518
  254. def OAI.SnakyPrototype.Certificate21.checked_529_i3 line 522
  255. def OAI.SnakyPrototype.Certificate21.height_529_i2 line 530
  256. def OAI.SnakyPrototype.Certificate21.childrenH_529_i2 line 531
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_529_i2 line 532
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_529_i2 line 533
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_529_i2 line 535
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_529_i2 line 539
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_529_i2 line 541
  262. def OAI.SnakyPrototype.Certificate21.checked_529_i2 line 545
  263. def OAI.SnakyPrototype.Certificate21.height_529_i1 line 553
  264. def OAI.SnakyPrototype.Certificate21.childrenH_529_i1 line 554
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_529_i1 line 555
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_529_i1 line 556
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_529_i1 line 558
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_529_i1 line 562
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_529_i1 line 564
  270. def OAI.SnakyPrototype.Certificate21.checked_529_i1 line 568
  271. def OAI.SnakyPrototype.Certificate21.height_529_i0 line 576
  272. def OAI.SnakyPrototype.Certificate21.childrenH_529_i0 line 577
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_529_i0 line 578
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_529_i0 line 579
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_529_i0 line 581
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_529_i0 line 585
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_529_i0 line 587
  278. def OAI.SnakyPrototype.Certificate21.checked_529_i0 line 591
  279. def OAI.SnakyPrototype.Certificate21.height_529 line 599
  280. def OAI.SnakyPrototype.Certificate21.childrenH_529 line 600
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_529 line 601
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_529 line 602
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_529 line 604
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_529 line 608
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_529 line 610
  286. def OAI.SnakyPrototype.Certificate21.checked_529 line 614
  287. def OAI.SnakyPrototype.Certificate21.height_535 line 622
  288. def OAI.SnakyPrototype.Certificate21.childrenH_535 line 623
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_535 line 624
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_535 line 625
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_535 line 627
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_535 line 631
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_535 line 633
  294. def OAI.SnakyPrototype.Certificate21.checked_535 line 637
  295. def OAI.SnakyPrototype.Certificate21.height_540_i0 line 645
  296. def OAI.SnakyPrototype.Certificate21.childrenH_540_i0 line 646
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_540_i0 line 647
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_540_i0 line 648
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_540_i0 line 650
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_540_i0 line 654
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_540_i0 line 656
  302. def OAI.SnakyPrototype.Certificate21.checked_540_i0 line 660
  303. def OAI.SnakyPrototype.Certificate21.height_540_i3 line 668
  304. def OAI.SnakyPrototype.Certificate21.childrenH_540_i3 line 669
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_540_i3 line 670
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_540_i3 line 671
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_540_i3 line 673
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_540_i3 line 677
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_540_i3 line 679
  310. def OAI.SnakyPrototype.Certificate21.checked_540_i3 line 683
  311. def OAI.SnakyPrototype.Certificate21.height_540_i2 line 691
  312. def OAI.SnakyPrototype.Certificate21.childrenH_540_i2 line 692
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_540_i2 line 693
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_540_i2 line 694
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_540_i2 line 696
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_540_i2 line 700
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_540_i2 line 702
  318. def OAI.SnakyPrototype.Certificate21.checked_540_i2 line 706
  319. def OAI.SnakyPrototype.Certificate21.height_540_i1 line 714
  320. def OAI.SnakyPrototype.Certificate21.childrenH_540_i1 line 715
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_540_i1 line 716
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_540_i1 line 717
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_540_i1 line 719
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_540_i1 line 723
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_540_i1 line 725
  326. def OAI.SnakyPrototype.Certificate21.checked_540_i1 line 729
  327. def OAI.SnakyPrototype.Certificate21.height_540 line 737
  328. def OAI.SnakyPrototype.Certificate21.childrenH_540 line 738
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_540 line 739
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_540 line 740
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_540 line 742
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_540 line 746
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_540 line 748
  334. def OAI.SnakyPrototype.Certificate21.checked_540 line 752
  335. def OAI.SnakyPrototype.Certificate21.height_541_i6 line 760
  336. def OAI.SnakyPrototype.Certificate21.childrenH_541_i6 line 761
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_541_i6 line 762
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_541_i6 line 763
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_541_i6 line 765
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_541_i6 line 769
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_541_i6 line 771
  342. def OAI.SnakyPrototype.Certificate21.checked_541_i6 line 775
  343. def OAI.SnakyPrototype.Certificate21.height_541_i5 line 783
  344. def OAI.SnakyPrototype.Certificate21.childrenH_541_i5 line 784
  345. theorem OAI.SnakyPrototype.Certificate21.height_exact_541_i5 line 785
  346. theorem OAI.SnakyPrototype.Certificate21.required_origin_541_i5 line 786
  347. theorem OAI.SnakyPrototype.Certificate21.required_exact_541_i5 line 788
  348. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_541_i5 line 792
  349. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_541_i5 line 794
  350. def OAI.SnakyPrototype.Certificate21.checked_541_i5 line 798
  351. def OAI.SnakyPrototype.Certificate21.height_541_i4 line 806
  352. def OAI.SnakyPrototype.Certificate21.childrenH_541_i4 line 807
  353. theorem OAI.SnakyPrototype.Certificate21.height_exact_541_i4 line 808
  354. theorem OAI.SnakyPrototype.Certificate21.required_origin_541_i4 line 809
  355. theorem OAI.SnakyPrototype.Certificate21.required_exact_541_i4 line 811
  356. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_541_i4 line 815
  357. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_541_i4 line 817
  358. def OAI.SnakyPrototype.Certificate21.checked_541_i4 line 821
  359. def OAI.SnakyPrototype.Certificate21.height_541_i3 line 829
  360. def OAI.SnakyPrototype.Certificate21.childrenH_541_i3 line 830
  361. theorem OAI.SnakyPrototype.Certificate21.height_exact_541_i3 line 831
  362. theorem OAI.SnakyPrototype.Certificate21.required_origin_541_i3 line 832
  363. theorem OAI.SnakyPrototype.Certificate21.required_exact_541_i3 line 834
  364. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_541_i3 line 838
  365. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_541_i3 line 840
  366. def OAI.SnakyPrototype.Certificate21.checked_541_i3 line 844
  367. def OAI.SnakyPrototype.Certificate21.height_541_i2 line 852
  368. def OAI.SnakyPrototype.Certificate21.childrenH_541_i2 line 853
  369. theorem OAI.SnakyPrototype.Certificate21.height_exact_541_i2 line 854
  370. theorem OAI.SnakyPrototype.Certificate21.required_origin_541_i2 line 855
  371. theorem OAI.SnakyPrototype.Certificate21.required_exact_541_i2 line 857
  372. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_541_i2 line 861
  373. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_541_i2 line 863
  374. def OAI.SnakyPrototype.Certificate21.checked_541_i2 line 867
  375. def OAI.SnakyPrototype.Certificate21.height_541_i1 line 875
  376. def OAI.SnakyPrototype.Certificate21.childrenH_541_i1 line 876
  377. theorem OAI.SnakyPrototype.Certificate21.height_exact_541_i1 line 877
  378. theorem OAI.SnakyPrototype.Certificate21.required_origin_541_i1 line 878
  379. theorem OAI.SnakyPrototype.Certificate21.required_exact_541_i1 line 880
  380. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_541_i1 line 884
  381. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_541_i1 line 886
  382. def OAI.SnakyPrototype.Certificate21.checked_541_i1 line 890
  383. def OAI.SnakyPrototype.Certificate21.height_541_i0 line 898
  384. def OAI.SnakyPrototype.Certificate21.childrenH_541_i0 line 899
  385. theorem OAI.SnakyPrototype.Certificate21.height_exact_541_i0 line 900
  386. theorem OAI.SnakyPrototype.Certificate21.required_origin_541_i0 line 901
  387. theorem OAI.SnakyPrototype.Certificate21.required_exact_541_i0 line 903
  388. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_541_i0 line 907
  389. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_541_i0 line 909
  390. def OAI.SnakyPrototype.Certificate21.checked_541_i0 line 913
  391. def OAI.SnakyPrototype.Certificate21.height_541 line 921
  392. def OAI.SnakyPrototype.Certificate21.childrenH_541 line 922
  393. theorem OAI.SnakyPrototype.Certificate21.height_exact_541 line 923
  394. theorem OAI.SnakyPrototype.Certificate21.required_origin_541 line 924
  395. theorem OAI.SnakyPrototype.Certificate21.required_exact_541 line 926
  396. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_541 line 930
  397. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_541 line 932
  398. def OAI.SnakyPrototype.Certificate21.checked_541 line 936
  399. def OAI.SnakyPrototype.Certificate21.height_545_i0 line 944
  400. def OAI.SnakyPrototype.Certificate21.childrenH_545_i0 line 945
  401. theorem OAI.SnakyPrototype.Certificate21.height_exact_545_i0 line 946
  402. theorem OAI.SnakyPrototype.Certificate21.required_origin_545_i0 line 947
  403. theorem OAI.SnakyPrototype.Certificate21.required_exact_545_i0 line 949
  404. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_545_i0 line 953
  405. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_545_i0 line 955
  406. def OAI.SnakyPrototype.Certificate21.checked_545_i0 line 959
  407. def OAI.SnakyPrototype.Certificate21.height_545 line 967
  408. def OAI.SnakyPrototype.Certificate21.childrenH_545 line 968
  409. theorem OAI.SnakyPrototype.Certificate21.height_exact_545 line 969
  410. theorem OAI.SnakyPrototype.Certificate21.required_origin_545 line 970
  411. theorem OAI.SnakyPrototype.Certificate21.required_exact_545 line 972
  412. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_545 line 976
  413. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_545 line 978
  414. def OAI.SnakyPrototype.Certificate21.checked_545 line 982