OAI/GameTheory/SnakyTwentyOne/Cards/Height08Part04.lean

GitHub source file

414 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_559_i0 line 23
  2. def OAI.SnakyPrototype.Certificate21.envelope_559_i0 line 24
  3. def OAI.SnakyPrototype.Certificate21.childrenC_559_i0 line 25
  4. def OAI.SnakyPrototype.Certificate21.childrenD_559_i0 line 26
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_559_i0 line 27
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_559_i0 line 28
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_559_i0 line 29
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_559_i0 line 30
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_559_i0 line 31
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_559_i0 line 36
  11. def OAI.SnakyPrototype.Certificate21.required_559_i6 line 41
  12. def OAI.SnakyPrototype.Certificate21.envelope_559_i6 line 42
  13. def OAI.SnakyPrototype.Certificate21.childrenC_559_i6 line 43
  14. def OAI.SnakyPrototype.Certificate21.childrenD_559_i6 line 44
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_559_i6 line 45
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_559_i6 line 46
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_559_i6 line 47
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_559_i6 line 48
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_559_i6 line 49
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_559_i6 line 54
  21. def OAI.SnakyPrototype.Certificate21.required_559_i5 line 59
  22. def OAI.SnakyPrototype.Certificate21.envelope_559_i5 line 60
  23. def OAI.SnakyPrototype.Certificate21.childrenC_559_i5 line 61
  24. def OAI.SnakyPrototype.Certificate21.childrenD_559_i5 line 62
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_559_i5 line 63
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_559_i5 line 64
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_559_i5 line 65
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_559_i5 line 66
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_559_i5 line 67
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_559_i5 line 72
  31. def OAI.SnakyPrototype.Certificate21.required_559_i4 line 77
  32. def OAI.SnakyPrototype.Certificate21.envelope_559_i4 line 78
  33. def OAI.SnakyPrototype.Certificate21.childrenC_559_i4 line 79
  34. def OAI.SnakyPrototype.Certificate21.childrenD_559_i4 line 80
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_559_i4 line 81
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_559_i4 line 82
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_559_i4 line 83
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_559_i4 line 84
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_559_i4 line 85
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_559_i4 line 90
  41. def OAI.SnakyPrototype.Certificate21.required_559_i3 line 95
  42. def OAI.SnakyPrototype.Certificate21.envelope_559_i3 line 96
  43. def OAI.SnakyPrototype.Certificate21.childrenC_559_i3 line 97
  44. def OAI.SnakyPrototype.Certificate21.childrenD_559_i3 line 98
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_559_i3 line 99
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_559_i3 line 100
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_559_i3 line 101
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_559_i3 line 102
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_559_i3 line 103
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_559_i3 line 108
  51. def OAI.SnakyPrototype.Certificate21.required_559_i2 line 113
  52. def OAI.SnakyPrototype.Certificate21.envelope_559_i2 line 114
  53. def OAI.SnakyPrototype.Certificate21.childrenC_559_i2 line 115
  54. def OAI.SnakyPrototype.Certificate21.childrenD_559_i2 line 116
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_559_i2 line 117
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_559_i2 line 118
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_559_i2 line 119
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_559_i2 line 120
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_559_i2 line 121
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_559_i2 line 126
  61. def OAI.SnakyPrototype.Certificate21.required_559_i1 line 131
  62. def OAI.SnakyPrototype.Certificate21.envelope_559_i1 line 132
  63. def OAI.SnakyPrototype.Certificate21.childrenC_559_i1 line 133
  64. def OAI.SnakyPrototype.Certificate21.childrenD_559_i1 line 134
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_559_i1 line 135
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_559_i1 line 136
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_559_i1 line 137
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_559_i1 line 138
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_559_i1 line 139
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_559_i1 line 144
  71. def OAI.SnakyPrototype.Certificate21.required_559 line 149
  72. def OAI.SnakyPrototype.Certificate21.envelope_559 line 150
  73. def OAI.SnakyPrototype.Certificate21.childrenC_559 line 151
  74. def OAI.SnakyPrototype.Certificate21.childrenD_559 line 152
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_559 line 153
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_559 line 154
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_559 line 155
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_559 line 156
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_559 line 157
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_559 line 164
  81. def OAI.SnakyPrototype.Certificate21.required_566 line 169
  82. def OAI.SnakyPrototype.Certificate21.envelope_566 line 170
  83. def OAI.SnakyPrototype.Certificate21.childrenC_566 line 171
  84. def OAI.SnakyPrototype.Certificate21.childrenD_566 line 172
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_566 line 173
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_566 line 174
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_566 line 175
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_566 line 176
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_566 line 177
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_566 line 186
  91. def OAI.SnakyPrototype.Certificate21.required_604_i0 line 191
  92. def OAI.SnakyPrototype.Certificate21.envelope_604_i0 line 192
  93. def OAI.SnakyPrototype.Certificate21.childrenC_604_i0 line 193
  94. def OAI.SnakyPrototype.Certificate21.childrenD_604_i0 line 194
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_604_i0 line 195
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_604_i0 line 196
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_604_i0 line 197
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_604_i0 line 198
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_604_i0 line 199
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_604_i0 line 204
  101. def OAI.SnakyPrototype.Certificate21.required_604 line 209
  102. def OAI.SnakyPrototype.Certificate21.envelope_604 line 210
  103. def OAI.SnakyPrototype.Certificate21.childrenC_604 line 211
  104. def OAI.SnakyPrototype.Certificate21.childrenD_604 line 212
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_604 line 213
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_604 line 214
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_604 line 215
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_604 line 216
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_604 line 217
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_604 line 222
  111. def OAI.SnakyPrototype.Certificate21.required_607_i0 line 227
  112. def OAI.SnakyPrototype.Certificate21.envelope_607_i0 line 228
  113. def OAI.SnakyPrototype.Certificate21.childrenC_607_i0 line 229
  114. def OAI.SnakyPrototype.Certificate21.childrenD_607_i0 line 230
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_607_i0 line 231
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_607_i0 line 232
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_607_i0 line 233
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_607_i0 line 234
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_607_i0 line 235
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_607_i0 line 240
  121. def OAI.SnakyPrototype.Certificate21.required_607_i3 line 245
  122. def OAI.SnakyPrototype.Certificate21.envelope_607_i3 line 246
  123. def OAI.SnakyPrototype.Certificate21.childrenC_607_i3 line 247
  124. def OAI.SnakyPrototype.Certificate21.childrenD_607_i3 line 248
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_607_i3 line 249
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_607_i3 line 250
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_607_i3 line 251
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_607_i3 line 252
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_607_i3 line 253
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_607_i3 line 258
  131. def OAI.SnakyPrototype.Certificate21.required_607_i2 line 263
  132. def OAI.SnakyPrototype.Certificate21.envelope_607_i2 line 264
  133. def OAI.SnakyPrototype.Certificate21.childrenC_607_i2 line 265
  134. def OAI.SnakyPrototype.Certificate21.childrenD_607_i2 line 266
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_607_i2 line 267
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_607_i2 line 268
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_607_i2 line 269
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_607_i2 line 270
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_607_i2 line 271
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_607_i2 line 276
  141. def OAI.SnakyPrototype.Certificate21.required_607_i1 line 281
  142. def OAI.SnakyPrototype.Certificate21.envelope_607_i1 line 282
  143. def OAI.SnakyPrototype.Certificate21.childrenC_607_i1 line 283
  144. def OAI.SnakyPrototype.Certificate21.childrenD_607_i1 line 284
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_607_i1 line 285
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_607_i1 line 286
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_607_i1 line 287
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_607_i1 line 288
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_607_i1 line 289
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_607_i1 line 295
  151. def OAI.SnakyPrototype.Certificate21.required_607_i4 line 300
  152. def OAI.SnakyPrototype.Certificate21.envelope_607_i4 line 301
  153. def OAI.SnakyPrototype.Certificate21.childrenC_607_i4 line 302
  154. def OAI.SnakyPrototype.Certificate21.childrenD_607_i4 line 303
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_607_i4 line 304
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_607_i4 line 305
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_607_i4 line 306
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_607_i4 line 307
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_607_i4 line 308
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_607_i4 line 315
  161. def OAI.SnakyPrototype.Certificate21.required_607 line 320
  162. def OAI.SnakyPrototype.Certificate21.envelope_607 line 321
  163. def OAI.SnakyPrototype.Certificate21.childrenC_607 line 322
  164. def OAI.SnakyPrototype.Certificate21.childrenD_607 line 323
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_607 line 324
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_607 line 325
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_607 line 326
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_607 line 327
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_607 line 328
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_607 line 336
  171. def OAI.SnakyPrototype.Certificate21.required_619_i0 line 341
  172. def OAI.SnakyPrototype.Certificate21.envelope_619_i0 line 342
  173. def OAI.SnakyPrototype.Certificate21.childrenC_619_i0 line 343
  174. def OAI.SnakyPrototype.Certificate21.childrenD_619_i0 line 344
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_619_i0 line 345
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_619_i0 line 346
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_619_i0 line 347
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_619_i0 line 348
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_619_i0 line 349
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_619_i0 line 354
  181. def OAI.SnakyPrototype.Certificate21.required_619 line 359
  182. def OAI.SnakyPrototype.Certificate21.envelope_619 line 360
  183. def OAI.SnakyPrototype.Certificate21.childrenC_619 line 361
  184. def OAI.SnakyPrototype.Certificate21.childrenD_619 line 362
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_619 line 363
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_619 line 364
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_619 line 365
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_619 line 366
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_619 line 367
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_619 line 376
  191. def OAI.SnakyPrototype.Certificate21.required_651_i0 line 381
  192. def OAI.SnakyPrototype.Certificate21.envelope_651_i0 line 382
  193. def OAI.SnakyPrototype.Certificate21.childrenC_651_i0 line 383
  194. def OAI.SnakyPrototype.Certificate21.childrenD_651_i0 line 384
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_651_i0 line 385
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_651_i0 line 386
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_651_i0 line 387
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_651_i0 line 388
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_651_i0 line 389
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_651_i0 line 394
  201. def OAI.SnakyPrototype.Certificate21.required_651_i1 line 399
  202. def OAI.SnakyPrototype.Certificate21.envelope_651_i1 line 400
  203. def OAI.SnakyPrototype.Certificate21.childrenC_651_i1 line 401
  204. def OAI.SnakyPrototype.Certificate21.childrenD_651_i1 line 402
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_651_i1 line 403
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_651_i1 line 404
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_651_i1 line 405
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_651_i1 line 406
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_651_i1 line 407
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_651_i1 line 413
  211. def OAI.SnakyPrototype.Certificate21.required_651_i2 line 418
  212. def OAI.SnakyPrototype.Certificate21.envelope_651_i2 line 419
  213. def OAI.SnakyPrototype.Certificate21.childrenC_651_i2 line 420
  214. def OAI.SnakyPrototype.Certificate21.childrenD_651_i2 line 421
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_651_i2 line 422
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_651_i2 line 423
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_651_i2 line 424
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_651_i2 line 425
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_651_i2 line 426
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_651_i2 line 431
  221. def OAI.SnakyPrototype.Certificate21.required_651 line 436
  222. def OAI.SnakyPrototype.Certificate21.envelope_651 line 437
  223. def OAI.SnakyPrototype.Certificate21.childrenC_651 line 438
  224. def OAI.SnakyPrototype.Certificate21.childrenD_651 line 439
  225. theorem OAI.SnakyPrototype.Certificate21.common_sub_651 line 440
  226. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_651 line 441
  227. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_651 line 442
  228. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_651 line 443
  229. theorem OAI.SnakyPrototype.Certificate21.children_work_651 line 444
  230. theorem OAI.SnakyPrototype.Certificate21.row_works_651 line 450
  231. def OAI.SnakyPrototype.Certificate21.height_559_i0 line 455
  232. def OAI.SnakyPrototype.Certificate21.childrenH_559_i0 line 456
  233. theorem OAI.SnakyPrototype.Certificate21.height_exact_559_i0 line 457
  234. theorem OAI.SnakyPrototype.Certificate21.required_origin_559_i0 line 458
  235. theorem OAI.SnakyPrototype.Certificate21.required_exact_559_i0 line 460
  236. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_559_i0 line 464
  237. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_559_i0 line 466
  238. def OAI.SnakyPrototype.Certificate21.checked_559_i0 line 470
  239. def OAI.SnakyPrototype.Certificate21.height_559_i6 line 478
  240. def OAI.SnakyPrototype.Certificate21.childrenH_559_i6 line 479
  241. theorem OAI.SnakyPrototype.Certificate21.height_exact_559_i6 line 480
  242. theorem OAI.SnakyPrototype.Certificate21.required_origin_559_i6 line 481
  243. theorem OAI.SnakyPrototype.Certificate21.required_exact_559_i6 line 483
  244. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_559_i6 line 487
  245. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_559_i6 line 489
  246. def OAI.SnakyPrototype.Certificate21.checked_559_i6 line 493
  247. def OAI.SnakyPrototype.Certificate21.height_559_i5 line 501
  248. def OAI.SnakyPrototype.Certificate21.childrenH_559_i5 line 502
  249. theorem OAI.SnakyPrototype.Certificate21.height_exact_559_i5 line 503
  250. theorem OAI.SnakyPrototype.Certificate21.required_origin_559_i5 line 504
  251. theorem OAI.SnakyPrototype.Certificate21.required_exact_559_i5 line 506
  252. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_559_i5 line 510
  253. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_559_i5 line 512
  254. def OAI.SnakyPrototype.Certificate21.checked_559_i5 line 516
  255. def OAI.SnakyPrototype.Certificate21.height_559_i4 line 524
  256. def OAI.SnakyPrototype.Certificate21.childrenH_559_i4 line 525
  257. theorem OAI.SnakyPrototype.Certificate21.height_exact_559_i4 line 526
  258. theorem OAI.SnakyPrototype.Certificate21.required_origin_559_i4 line 527
  259. theorem OAI.SnakyPrototype.Certificate21.required_exact_559_i4 line 529
  260. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_559_i4 line 533
  261. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_559_i4 line 535
  262. def OAI.SnakyPrototype.Certificate21.checked_559_i4 line 539
  263. def OAI.SnakyPrototype.Certificate21.height_559_i3 line 547
  264. def OAI.SnakyPrototype.Certificate21.childrenH_559_i3 line 548
  265. theorem OAI.SnakyPrototype.Certificate21.height_exact_559_i3 line 549
  266. theorem OAI.SnakyPrototype.Certificate21.required_origin_559_i3 line 550
  267. theorem OAI.SnakyPrototype.Certificate21.required_exact_559_i3 line 552
  268. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_559_i3 line 556
  269. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_559_i3 line 558
  270. def OAI.SnakyPrototype.Certificate21.checked_559_i3 line 562
  271. def OAI.SnakyPrototype.Certificate21.height_559_i2 line 570
  272. def OAI.SnakyPrototype.Certificate21.childrenH_559_i2 line 571
  273. theorem OAI.SnakyPrototype.Certificate21.height_exact_559_i2 line 572
  274. theorem OAI.SnakyPrototype.Certificate21.required_origin_559_i2 line 573
  275. theorem OAI.SnakyPrototype.Certificate21.required_exact_559_i2 line 575
  276. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_559_i2 line 579
  277. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_559_i2 line 581
  278. def OAI.SnakyPrototype.Certificate21.checked_559_i2 line 585
  279. def OAI.SnakyPrototype.Certificate21.height_559_i1 line 593
  280. def OAI.SnakyPrototype.Certificate21.childrenH_559_i1 line 594
  281. theorem OAI.SnakyPrototype.Certificate21.height_exact_559_i1 line 595
  282. theorem OAI.SnakyPrototype.Certificate21.required_origin_559_i1 line 596
  283. theorem OAI.SnakyPrototype.Certificate21.required_exact_559_i1 line 598
  284. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_559_i1 line 602
  285. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_559_i1 line 604
  286. def OAI.SnakyPrototype.Certificate21.checked_559_i1 line 608
  287. def OAI.SnakyPrototype.Certificate21.height_559 line 616
  288. def OAI.SnakyPrototype.Certificate21.childrenH_559 line 617
  289. theorem OAI.SnakyPrototype.Certificate21.height_exact_559 line 618
  290. theorem OAI.SnakyPrototype.Certificate21.required_origin_559 line 619
  291. theorem OAI.SnakyPrototype.Certificate21.required_exact_559 line 621
  292. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_559 line 625
  293. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_559 line 627
  294. def OAI.SnakyPrototype.Certificate21.checked_559 line 631
  295. def OAI.SnakyPrototype.Certificate21.height_566 line 639
  296. def OAI.SnakyPrototype.Certificate21.childrenH_566 line 640
  297. theorem OAI.SnakyPrototype.Certificate21.height_exact_566 line 641
  298. theorem OAI.SnakyPrototype.Certificate21.required_origin_566 line 642
  299. theorem OAI.SnakyPrototype.Certificate21.required_exact_566 line 644
  300. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_566 line 648
  301. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_566 line 650
  302. def OAI.SnakyPrototype.Certificate21.checked_566 line 654
  303. def OAI.SnakyPrototype.Certificate21.height_604_i0 line 662
  304. def OAI.SnakyPrototype.Certificate21.childrenH_604_i0 line 663
  305. theorem OAI.SnakyPrototype.Certificate21.height_exact_604_i0 line 664
  306. theorem OAI.SnakyPrototype.Certificate21.required_origin_604_i0 line 665
  307. theorem OAI.SnakyPrototype.Certificate21.required_exact_604_i0 line 667
  308. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_604_i0 line 671
  309. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_604_i0 line 673
  310. def OAI.SnakyPrototype.Certificate21.checked_604_i0 line 677
  311. def OAI.SnakyPrototype.Certificate21.height_604 line 685
  312. def OAI.SnakyPrototype.Certificate21.childrenH_604 line 686
  313. theorem OAI.SnakyPrototype.Certificate21.height_exact_604 line 687
  314. theorem OAI.SnakyPrototype.Certificate21.required_origin_604 line 688
  315. theorem OAI.SnakyPrototype.Certificate21.required_exact_604 line 690
  316. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_604 line 694
  317. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_604 line 696
  318. def OAI.SnakyPrototype.Certificate21.checked_604 line 700
  319. def OAI.SnakyPrototype.Certificate21.height_607_i0 line 708
  320. def OAI.SnakyPrototype.Certificate21.childrenH_607_i0 line 709
  321. theorem OAI.SnakyPrototype.Certificate21.height_exact_607_i0 line 710
  322. theorem OAI.SnakyPrototype.Certificate21.required_origin_607_i0 line 711
  323. theorem OAI.SnakyPrototype.Certificate21.required_exact_607_i0 line 713
  324. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_607_i0 line 717
  325. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_607_i0 line 719
  326. def OAI.SnakyPrototype.Certificate21.checked_607_i0 line 723
  327. def OAI.SnakyPrototype.Certificate21.height_607_i3 line 731
  328. def OAI.SnakyPrototype.Certificate21.childrenH_607_i3 line 732
  329. theorem OAI.SnakyPrototype.Certificate21.height_exact_607_i3 line 733
  330. theorem OAI.SnakyPrototype.Certificate21.required_origin_607_i3 line 734
  331. theorem OAI.SnakyPrototype.Certificate21.required_exact_607_i3 line 736
  332. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_607_i3 line 740
  333. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_607_i3 line 742
  334. def OAI.SnakyPrototype.Certificate21.checked_607_i3 line 746
  335. def OAI.SnakyPrototype.Certificate21.height_607_i2 line 754
  336. def OAI.SnakyPrototype.Certificate21.childrenH_607_i2 line 755
  337. theorem OAI.SnakyPrototype.Certificate21.height_exact_607_i2 line 756
  338. theorem OAI.SnakyPrototype.Certificate21.required_origin_607_i2 line 757
  339. theorem OAI.SnakyPrototype.Certificate21.required_exact_607_i2 line 759
  340. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_607_i2 line 763
  341. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_607_i2 line 765
  342. def OAI.SnakyPrototype.Certificate21.checked_607_i2 line 769
  343. def OAI.SnakyPrototype.Certificate21.height_607_i1 line 777
  344. def OAI.SnakyPrototype.Certificate21.childrenH_607_i1 line 778
  345. theorem OAI.SnakyPrototype.Certificate21.height_exact_607_i1 line 779
  346. theorem OAI.SnakyPrototype.Certificate21.required_origin_607_i1 line 780
  347. theorem OAI.SnakyPrototype.Certificate21.required_exact_607_i1 line 782
  348. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_607_i1 line 786
  349. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_607_i1 line 788
  350. def OAI.SnakyPrototype.Certificate21.checked_607_i1 line 792
  351. def OAI.SnakyPrototype.Certificate21.height_607_i4 line 800
  352. def OAI.SnakyPrototype.Certificate21.childrenH_607_i4 line 801
  353. theorem OAI.SnakyPrototype.Certificate21.height_exact_607_i4 line 802
  354. theorem OAI.SnakyPrototype.Certificate21.required_origin_607_i4 line 803
  355. theorem OAI.SnakyPrototype.Certificate21.required_exact_607_i4 line 805
  356. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_607_i4 line 809
  357. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_607_i4 line 811
  358. def OAI.SnakyPrototype.Certificate21.checked_607_i4 line 815
  359. def OAI.SnakyPrototype.Certificate21.height_607 line 823
  360. def OAI.SnakyPrototype.Certificate21.childrenH_607 line 824
  361. theorem OAI.SnakyPrototype.Certificate21.height_exact_607 line 825
  362. theorem OAI.SnakyPrototype.Certificate21.required_origin_607 line 826
  363. theorem OAI.SnakyPrototype.Certificate21.required_exact_607 line 828
  364. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_607 line 832
  365. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_607 line 834
  366. def OAI.SnakyPrototype.Certificate21.checked_607 line 838
  367. def OAI.SnakyPrototype.Certificate21.height_619_i0 line 846
  368. def OAI.SnakyPrototype.Certificate21.childrenH_619_i0 line 847
  369. theorem OAI.SnakyPrototype.Certificate21.height_exact_619_i0 line 848
  370. theorem OAI.SnakyPrototype.Certificate21.required_origin_619_i0 line 849
  371. theorem OAI.SnakyPrototype.Certificate21.required_exact_619_i0 line 851
  372. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_619_i0 line 855
  373. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_619_i0 line 857
  374. def OAI.SnakyPrototype.Certificate21.checked_619_i0 line 861
  375. def OAI.SnakyPrototype.Certificate21.height_619 line 869
  376. def OAI.SnakyPrototype.Certificate21.childrenH_619 line 870
  377. theorem OAI.SnakyPrototype.Certificate21.height_exact_619 line 871
  378. theorem OAI.SnakyPrototype.Certificate21.required_origin_619 line 872
  379. theorem OAI.SnakyPrototype.Certificate21.required_exact_619 line 874
  380. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_619 line 878
  381. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_619 line 880
  382. def OAI.SnakyPrototype.Certificate21.checked_619 line 884
  383. def OAI.SnakyPrototype.Certificate21.height_651_i0 line 892
  384. def OAI.SnakyPrototype.Certificate21.childrenH_651_i0 line 893
  385. theorem OAI.SnakyPrototype.Certificate21.height_exact_651_i0 line 894
  386. theorem OAI.SnakyPrototype.Certificate21.required_origin_651_i0 line 895
  387. theorem OAI.SnakyPrototype.Certificate21.required_exact_651_i0 line 897
  388. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_651_i0 line 901
  389. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_651_i0 line 903
  390. def OAI.SnakyPrototype.Certificate21.checked_651_i0 line 907
  391. def OAI.SnakyPrototype.Certificate21.height_651_i1 line 915
  392. def OAI.SnakyPrototype.Certificate21.childrenH_651_i1 line 916
  393. theorem OAI.SnakyPrototype.Certificate21.height_exact_651_i1 line 917
  394. theorem OAI.SnakyPrototype.Certificate21.required_origin_651_i1 line 918
  395. theorem OAI.SnakyPrototype.Certificate21.required_exact_651_i1 line 920
  396. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_651_i1 line 924
  397. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_651_i1 line 926
  398. def OAI.SnakyPrototype.Certificate21.checked_651_i1 line 930
  399. def OAI.SnakyPrototype.Certificate21.height_651_i2 line 938
  400. def OAI.SnakyPrototype.Certificate21.childrenH_651_i2 line 939
  401. theorem OAI.SnakyPrototype.Certificate21.height_exact_651_i2 line 940
  402. theorem OAI.SnakyPrototype.Certificate21.required_origin_651_i2 line 941
  403. theorem OAI.SnakyPrototype.Certificate21.required_exact_651_i2 line 943
  404. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_651_i2 line 947
  405. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_651_i2 line 949
  406. def OAI.SnakyPrototype.Certificate21.checked_651_i2 line 953
  407. def OAI.SnakyPrototype.Certificate21.height_651 line 961
  408. def OAI.SnakyPrototype.Certificate21.childrenH_651 line 962
  409. theorem OAI.SnakyPrototype.Certificate21.height_exact_651 line 963
  410. theorem OAI.SnakyPrototype.Certificate21.required_origin_651 line 964
  411. theorem OAI.SnakyPrototype.Certificate21.required_exact_651 line 966
  412. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_651 line 970
  413. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_651 line 972
  414. def OAI.SnakyPrototype.Certificate21.checked_651 line 976