OAI/GameTheory/SnakyTwentyOne/Cards/Height13Part02.lean

GitHub source file

396 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_564_i2 line 30
  2. def OAI.SnakyPrototype.Certificate21.envelope_564_i2 line 31
  3. def OAI.SnakyPrototype.Certificate21.childrenC_564_i2 line 32
  4. def OAI.SnakyPrototype.Certificate21.childrenD_564_i2 line 33
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_564_i2 line 34
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_564_i2 line 35
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_564_i2 line 36
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_564_i2 line 37
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_564_i2 line 38
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_564_i2 line 43
  11. def OAI.SnakyPrototype.Certificate21.required_564_i7 line 48
  12. def OAI.SnakyPrototype.Certificate21.envelope_564_i7 line 49
  13. def OAI.SnakyPrototype.Certificate21.childrenC_564_i7 line 50
  14. def OAI.SnakyPrototype.Certificate21.childrenD_564_i7 line 51
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_564_i7 line 52
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_564_i7 line 53
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_564_i7 line 54
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_564_i7 line 55
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_564_i7 line 56
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_564_i7 line 61
  21. def OAI.SnakyPrototype.Certificate21.required_564_i8 line 66
  22. def OAI.SnakyPrototype.Certificate21.envelope_564_i8 line 67
  23. def OAI.SnakyPrototype.Certificate21.childrenC_564_i8 line 68
  24. def OAI.SnakyPrototype.Certificate21.childrenD_564_i8 line 69
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_564_i8 line 70
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_564_i8 line 71
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_564_i8 line 72
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_564_i8 line 73
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_564_i8 line 74
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_564_i8 line 79
  31. def OAI.SnakyPrototype.Certificate21.required_564_i6 line 84
  32. def OAI.SnakyPrototype.Certificate21.envelope_564_i6 line 85
  33. def OAI.SnakyPrototype.Certificate21.childrenC_564_i6 line 86
  34. def OAI.SnakyPrototype.Certificate21.childrenD_564_i6 line 87
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_564_i6 line 88
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_564_i6 line 89
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_564_i6 line 90
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_564_i6 line 91
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_564_i6 line 92
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_564_i6 line 98
  41. def OAI.SnakyPrototype.Certificate21.required_564_i5 line 103
  42. def OAI.SnakyPrototype.Certificate21.envelope_564_i5 line 104
  43. def OAI.SnakyPrototype.Certificate21.childrenC_564_i5 line 105
  44. def OAI.SnakyPrototype.Certificate21.childrenD_564_i5 line 106
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_564_i5 line 107
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_564_i5 line 108
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_564_i5 line 109
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_564_i5 line 110
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_564_i5 line 111
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_564_i5 line 116
  51. def OAI.SnakyPrototype.Certificate21.required_564_i4 line 121
  52. def OAI.SnakyPrototype.Certificate21.envelope_564_i4 line 122
  53. def OAI.SnakyPrototype.Certificate21.childrenC_564_i4 line 123
  54. def OAI.SnakyPrototype.Certificate21.childrenD_564_i4 line 124
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_564_i4 line 125
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_564_i4 line 126
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_564_i4 line 127
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_564_i4 line 128
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_564_i4 line 129
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_564_i4 line 135
  61. def OAI.SnakyPrototype.Certificate21.required_564_i3 line 140
  62. def OAI.SnakyPrototype.Certificate21.envelope_564_i3 line 141
  63. def OAI.SnakyPrototype.Certificate21.childrenC_564_i3 line 142
  64. def OAI.SnakyPrototype.Certificate21.childrenD_564_i3 line 143
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_564_i3 line 144
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_564_i3 line 145
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_564_i3 line 146
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_564_i3 line 147
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_564_i3 line 148
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_564_i3 line 158
  71. def OAI.SnakyPrototype.Certificate21.required_564_i1 line 163
  72. def OAI.SnakyPrototype.Certificate21.envelope_564_i1 line 164
  73. def OAI.SnakyPrototype.Certificate21.childrenC_564_i1 line 165
  74. def OAI.SnakyPrototype.Certificate21.childrenD_564_i1 line 166
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_564_i1 line 167
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_564_i1 line 168
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_564_i1 line 169
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_564_i1 line 170
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_564_i1 line 171
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_564_i1 line 179
  81. def OAI.SnakyPrototype.Certificate21.required_564_i0 line 184
  82. def OAI.SnakyPrototype.Certificate21.envelope_564_i0 line 185
  83. def OAI.SnakyPrototype.Certificate21.childrenC_564_i0 line 186
  84. def OAI.SnakyPrototype.Certificate21.childrenD_564_i0 line 187
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_564_i0 line 188
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_564_i0 line 189
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_564_i0 line 190
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_564_i0 line 191
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_564_i0 line 192
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_564_i0 line 201
  91. def OAI.SnakyPrototype.Certificate21.required_564 line 206
  92. def OAI.SnakyPrototype.Certificate21.envelope_564 line 207
  93. def OAI.SnakyPrototype.Certificate21.childrenC_564 line 208
  94. def OAI.SnakyPrototype.Certificate21.childrenD_564 line 209
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_564 line 210
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_564 line 211
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_564 line 212
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_564 line 213
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_564 line 214
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_564 line 221
  101. def OAI.SnakyPrototype.Certificate21.required_568_i0 line 226
  102. def OAI.SnakyPrototype.Certificate21.envelope_568_i0 line 227
  103. def OAI.SnakyPrototype.Certificate21.childrenC_568_i0 line 228
  104. def OAI.SnakyPrototype.Certificate21.childrenD_568_i0 line 229
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_568_i0 line 230
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_568_i0 line 231
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_568_i0 line 232
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_568_i0 line 233
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_568_i0 line 234
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_568_i0 line 239
  111. def OAI.SnakyPrototype.Certificate21.required_568_i3 line 244
  112. def OAI.SnakyPrototype.Certificate21.envelope_568_i3 line 245
  113. def OAI.SnakyPrototype.Certificate21.childrenC_568_i3 line 246
  114. def OAI.SnakyPrototype.Certificate21.childrenD_568_i3 line 247
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_568_i3 line 248
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_568_i3 line 249
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_568_i3 line 250
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_568_i3 line 251
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_568_i3 line 252
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_568_i3 line 257
  121. def OAI.SnakyPrototype.Certificate21.required_568_i6 line 262
  122. def OAI.SnakyPrototype.Certificate21.envelope_568_i6 line 263
  123. def OAI.SnakyPrototype.Certificate21.childrenC_568_i6 line 264
  124. def OAI.SnakyPrototype.Certificate21.childrenD_568_i6 line 265
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_568_i6 line 266
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_568_i6 line 267
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_568_i6 line 268
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_568_i6 line 269
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_568_i6 line 270
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_568_i6 line 275
  131. def OAI.SnakyPrototype.Certificate21.required_568_i7 line 280
  132. def OAI.SnakyPrototype.Certificate21.envelope_568_i7 line 281
  133. def OAI.SnakyPrototype.Certificate21.childrenC_568_i7 line 282
  134. def OAI.SnakyPrototype.Certificate21.childrenD_568_i7 line 283
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_568_i7 line 284
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_568_i7 line 285
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_568_i7 line 286
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_568_i7 line 287
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_568_i7 line 288
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_568_i7 line 293
  141. def OAI.SnakyPrototype.Certificate21.required_568_i5 line 298
  142. def OAI.SnakyPrototype.Certificate21.envelope_568_i5 line 299
  143. def OAI.SnakyPrototype.Certificate21.childrenC_568_i5 line 300
  144. def OAI.SnakyPrototype.Certificate21.childrenD_568_i5 line 301
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_568_i5 line 302
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_568_i5 line 303
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_568_i5 line 304
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_568_i5 line 305
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_568_i5 line 306
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_568_i5 line 313
  151. def OAI.SnakyPrototype.Certificate21.required_568_i4 line 318
  152. def OAI.SnakyPrototype.Certificate21.envelope_568_i4 line 319
  153. def OAI.SnakyPrototype.Certificate21.childrenC_568_i4 line 320
  154. def OAI.SnakyPrototype.Certificate21.childrenD_568_i4 line 321
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_568_i4 line 322
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_568_i4 line 323
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_568_i4 line 324
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_568_i4 line 325
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_568_i4 line 326
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_568_i4 line 331
  161. def OAI.SnakyPrototype.Certificate21.required_568_i2 line 336
  162. def OAI.SnakyPrototype.Certificate21.envelope_568_i2 line 337
  163. def OAI.SnakyPrototype.Certificate21.childrenC_568_i2 line 338
  164. def OAI.SnakyPrototype.Certificate21.childrenD_568_i2 line 339
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_568_i2 line 340
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_568_i2 line 341
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_568_i2 line 342
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_568_i2 line 343
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_568_i2 line 344
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_568_i2 line 350
  171. def OAI.SnakyPrototype.Certificate21.required_568_i1 line 355
  172. def OAI.SnakyPrototype.Certificate21.envelope_568_i1 line 356
  173. def OAI.SnakyPrototype.Certificate21.childrenC_568_i1 line 357
  174. def OAI.SnakyPrototype.Certificate21.childrenD_568_i1 line 358
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_568_i1 line 359
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_568_i1 line 360
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_568_i1 line 361
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_568_i1 line 362
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_568_i1 line 363
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_568_i1 line 372
  181. def OAI.SnakyPrototype.Certificate21.required_568 line 377
  182. def OAI.SnakyPrototype.Certificate21.envelope_568 line 378
  183. def OAI.SnakyPrototype.Certificate21.childrenC_568 line 379
  184. def OAI.SnakyPrototype.Certificate21.childrenD_568 line 380
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_568 line 381
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_568 line 382
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_568 line 383
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_568 line 384
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_568 line 385
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_568 line 392
  191. def OAI.SnakyPrototype.Certificate21.required_572_i0 line 397
  192. def OAI.SnakyPrototype.Certificate21.envelope_572_i0 line 398
  193. def OAI.SnakyPrototype.Certificate21.childrenC_572_i0 line 399
  194. def OAI.SnakyPrototype.Certificate21.childrenD_572_i0 line 400
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_572_i0 line 401
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_572_i0 line 402
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_572_i0 line 403
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_572_i0 line 404
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_572_i0 line 405
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_572_i0 line 410
  201. def OAI.SnakyPrototype.Certificate21.required_572 line 415
  202. def OAI.SnakyPrototype.Certificate21.envelope_572 line 416
  203. def OAI.SnakyPrototype.Certificate21.childrenC_572 line 417
  204. def OAI.SnakyPrototype.Certificate21.childrenD_572 line 418
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_572 line 419
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_572 line 420
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_572 line 421
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_572 line 422
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_572 line 423
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_572 line 430
  211. def OAI.SnakyPrototype.Certificate21.required_590 line 435
  212. def OAI.SnakyPrototype.Certificate21.envelope_590 line 436
  213. def OAI.SnakyPrototype.Certificate21.childrenC_590 line 437
  214. def OAI.SnakyPrototype.Certificate21.childrenD_590 line 438
  215. theorem OAI.SnakyPrototype.Certificate21.common_sub_590 line 439
  216. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_590 line 440
  217. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_590 line 441
  218. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_590 line 442
  219. theorem OAI.SnakyPrototype.Certificate21.children_work_590 line 443
  220. theorem OAI.SnakyPrototype.Certificate21.row_works_590 line 448
  221. def OAI.SnakyPrototype.Certificate21.height_564_i2 line 453
  222. def OAI.SnakyPrototype.Certificate21.childrenH_564_i2 line 454
  223. theorem OAI.SnakyPrototype.Certificate21.height_exact_564_i2 line 455
  224. theorem OAI.SnakyPrototype.Certificate21.required_origin_564_i2 line 456
  225. theorem OAI.SnakyPrototype.Certificate21.required_exact_564_i2 line 458
  226. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_564_i2 line 462
  227. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_564_i2 line 464
  228. def OAI.SnakyPrototype.Certificate21.checked_564_i2 line 468
  229. def OAI.SnakyPrototype.Certificate21.height_564_i7 line 476
  230. def OAI.SnakyPrototype.Certificate21.childrenH_564_i7 line 477
  231. theorem OAI.SnakyPrototype.Certificate21.height_exact_564_i7 line 478
  232. theorem OAI.SnakyPrototype.Certificate21.required_origin_564_i7 line 479
  233. theorem OAI.SnakyPrototype.Certificate21.required_exact_564_i7 line 481
  234. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_564_i7 line 485
  235. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_564_i7 line 487
  236. def OAI.SnakyPrototype.Certificate21.checked_564_i7 line 491
  237. def OAI.SnakyPrototype.Certificate21.height_564_i8 line 499
  238. def OAI.SnakyPrototype.Certificate21.childrenH_564_i8 line 500
  239. theorem OAI.SnakyPrototype.Certificate21.height_exact_564_i8 line 501
  240. theorem OAI.SnakyPrototype.Certificate21.required_origin_564_i8 line 502
  241. theorem OAI.SnakyPrototype.Certificate21.required_exact_564_i8 line 504
  242. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_564_i8 line 508
  243. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_564_i8 line 510
  244. def OAI.SnakyPrototype.Certificate21.checked_564_i8 line 514
  245. def OAI.SnakyPrototype.Certificate21.height_564_i6 line 522
  246. def OAI.SnakyPrototype.Certificate21.childrenH_564_i6 line 523
  247. theorem OAI.SnakyPrototype.Certificate21.height_exact_564_i6 line 524
  248. theorem OAI.SnakyPrototype.Certificate21.required_origin_564_i6 line 525
  249. theorem OAI.SnakyPrototype.Certificate21.required_exact_564_i6 line 527
  250. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_564_i6 line 531
  251. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_564_i6 line 533
  252. def OAI.SnakyPrototype.Certificate21.checked_564_i6 line 537
  253. def OAI.SnakyPrototype.Certificate21.height_564_i5 line 545
  254. def OAI.SnakyPrototype.Certificate21.childrenH_564_i5 line 546
  255. theorem OAI.SnakyPrototype.Certificate21.height_exact_564_i5 line 547
  256. theorem OAI.SnakyPrototype.Certificate21.required_origin_564_i5 line 548
  257. theorem OAI.SnakyPrototype.Certificate21.required_exact_564_i5 line 550
  258. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_564_i5 line 554
  259. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_564_i5 line 556
  260. def OAI.SnakyPrototype.Certificate21.checked_564_i5 line 560
  261. def OAI.SnakyPrototype.Certificate21.height_564_i4 line 568
  262. def OAI.SnakyPrototype.Certificate21.childrenH_564_i4 line 569
  263. theorem OAI.SnakyPrototype.Certificate21.height_exact_564_i4 line 570
  264. theorem OAI.SnakyPrototype.Certificate21.required_origin_564_i4 line 571
  265. theorem OAI.SnakyPrototype.Certificate21.required_exact_564_i4 line 573
  266. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_564_i4 line 577
  267. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_564_i4 line 579
  268. def OAI.SnakyPrototype.Certificate21.checked_564_i4 line 583
  269. def OAI.SnakyPrototype.Certificate21.height_564_i3 line 591
  270. def OAI.SnakyPrototype.Certificate21.childrenH_564_i3 line 592
  271. theorem OAI.SnakyPrototype.Certificate21.height_exact_564_i3 line 593
  272. theorem OAI.SnakyPrototype.Certificate21.required_origin_564_i3 line 594
  273. theorem OAI.SnakyPrototype.Certificate21.required_exact_564_i3 line 596
  274. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_564_i3 line 600
  275. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_564_i3 line 602
  276. def OAI.SnakyPrototype.Certificate21.checked_564_i3 line 606
  277. def OAI.SnakyPrototype.Certificate21.height_564_i1 line 614
  278. def OAI.SnakyPrototype.Certificate21.childrenH_564_i1 line 615
  279. theorem OAI.SnakyPrototype.Certificate21.height_exact_564_i1 line 616
  280. theorem OAI.SnakyPrototype.Certificate21.required_origin_564_i1 line 617
  281. theorem OAI.SnakyPrototype.Certificate21.required_exact_564_i1 line 619
  282. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_564_i1 line 623
  283. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_564_i1 line 625
  284. def OAI.SnakyPrototype.Certificate21.checked_564_i1 line 629
  285. def OAI.SnakyPrototype.Certificate21.height_564_i0 line 637
  286. def OAI.SnakyPrototype.Certificate21.childrenH_564_i0 line 638
  287. theorem OAI.SnakyPrototype.Certificate21.height_exact_564_i0 line 639
  288. theorem OAI.SnakyPrototype.Certificate21.required_origin_564_i0 line 640
  289. theorem OAI.SnakyPrototype.Certificate21.required_exact_564_i0 line 642
  290. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_564_i0 line 646
  291. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_564_i0 line 648
  292. def OAI.SnakyPrototype.Certificate21.checked_564_i0 line 652
  293. def OAI.SnakyPrototype.Certificate21.height_564 line 660
  294. def OAI.SnakyPrototype.Certificate21.childrenH_564 line 661
  295. theorem OAI.SnakyPrototype.Certificate21.height_exact_564 line 662
  296. theorem OAI.SnakyPrototype.Certificate21.required_origin_564 line 663
  297. theorem OAI.SnakyPrototype.Certificate21.required_exact_564 line 665
  298. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_564 line 669
  299. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_564 line 671
  300. def OAI.SnakyPrototype.Certificate21.checked_564 line 675
  301. def OAI.SnakyPrototype.Certificate21.height_568_i0 line 683
  302. def OAI.SnakyPrototype.Certificate21.childrenH_568_i0 line 684
  303. theorem OAI.SnakyPrototype.Certificate21.height_exact_568_i0 line 685
  304. theorem OAI.SnakyPrototype.Certificate21.required_origin_568_i0 line 686
  305. theorem OAI.SnakyPrototype.Certificate21.required_exact_568_i0 line 688
  306. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_568_i0 line 692
  307. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_568_i0 line 694
  308. def OAI.SnakyPrototype.Certificate21.checked_568_i0 line 698
  309. def OAI.SnakyPrototype.Certificate21.height_568_i3 line 706
  310. def OAI.SnakyPrototype.Certificate21.childrenH_568_i3 line 707
  311. theorem OAI.SnakyPrototype.Certificate21.height_exact_568_i3 line 708
  312. theorem OAI.SnakyPrototype.Certificate21.required_origin_568_i3 line 709
  313. theorem OAI.SnakyPrototype.Certificate21.required_exact_568_i3 line 711
  314. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_568_i3 line 715
  315. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_568_i3 line 717
  316. def OAI.SnakyPrototype.Certificate21.checked_568_i3 line 721
  317. def OAI.SnakyPrototype.Certificate21.height_568_i6 line 729
  318. def OAI.SnakyPrototype.Certificate21.childrenH_568_i6 line 730
  319. theorem OAI.SnakyPrototype.Certificate21.height_exact_568_i6 line 731
  320. theorem OAI.SnakyPrototype.Certificate21.required_origin_568_i6 line 732
  321. theorem OAI.SnakyPrototype.Certificate21.required_exact_568_i6 line 734
  322. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_568_i6 line 738
  323. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_568_i6 line 740
  324. def OAI.SnakyPrototype.Certificate21.checked_568_i6 line 744
  325. def OAI.SnakyPrototype.Certificate21.height_568_i7 line 752
  326. def OAI.SnakyPrototype.Certificate21.childrenH_568_i7 line 753
  327. theorem OAI.SnakyPrototype.Certificate21.height_exact_568_i7 line 754
  328. theorem OAI.SnakyPrototype.Certificate21.required_origin_568_i7 line 755
  329. theorem OAI.SnakyPrototype.Certificate21.required_exact_568_i7 line 757
  330. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_568_i7 line 761
  331. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_568_i7 line 763
  332. def OAI.SnakyPrototype.Certificate21.checked_568_i7 line 767
  333. def OAI.SnakyPrototype.Certificate21.height_568_i5 line 775
  334. def OAI.SnakyPrototype.Certificate21.childrenH_568_i5 line 776
  335. theorem OAI.SnakyPrototype.Certificate21.height_exact_568_i5 line 777
  336. theorem OAI.SnakyPrototype.Certificate21.required_origin_568_i5 line 778
  337. theorem OAI.SnakyPrototype.Certificate21.required_exact_568_i5 line 780
  338. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_568_i5 line 784
  339. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_568_i5 line 786
  340. def OAI.SnakyPrototype.Certificate21.checked_568_i5 line 790
  341. def OAI.SnakyPrototype.Certificate21.height_568_i4 line 798
  342. def OAI.SnakyPrototype.Certificate21.childrenH_568_i4 line 799
  343. theorem OAI.SnakyPrototype.Certificate21.height_exact_568_i4 line 800
  344. theorem OAI.SnakyPrototype.Certificate21.required_origin_568_i4 line 801
  345. theorem OAI.SnakyPrototype.Certificate21.required_exact_568_i4 line 803
  346. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_568_i4 line 807
  347. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_568_i4 line 809
  348. def OAI.SnakyPrototype.Certificate21.checked_568_i4 line 813
  349. def OAI.SnakyPrototype.Certificate21.height_568_i2 line 821
  350. def OAI.SnakyPrototype.Certificate21.childrenH_568_i2 line 822
  351. theorem OAI.SnakyPrototype.Certificate21.height_exact_568_i2 line 823
  352. theorem OAI.SnakyPrototype.Certificate21.required_origin_568_i2 line 824
  353. theorem OAI.SnakyPrototype.Certificate21.required_exact_568_i2 line 826
  354. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_568_i2 line 830
  355. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_568_i2 line 832
  356. def OAI.SnakyPrototype.Certificate21.checked_568_i2 line 836
  357. def OAI.SnakyPrototype.Certificate21.height_568_i1 line 844
  358. def OAI.SnakyPrototype.Certificate21.childrenH_568_i1 line 845
  359. theorem OAI.SnakyPrototype.Certificate21.height_exact_568_i1 line 846
  360. theorem OAI.SnakyPrototype.Certificate21.required_origin_568_i1 line 847
  361. theorem OAI.SnakyPrototype.Certificate21.required_exact_568_i1 line 849
  362. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_568_i1 line 853
  363. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_568_i1 line 855
  364. def OAI.SnakyPrototype.Certificate21.checked_568_i1 line 859
  365. def OAI.SnakyPrototype.Certificate21.height_568 line 867
  366. def OAI.SnakyPrototype.Certificate21.childrenH_568 line 868
  367. theorem OAI.SnakyPrototype.Certificate21.height_exact_568 line 869
  368. theorem OAI.SnakyPrototype.Certificate21.required_origin_568 line 870
  369. theorem OAI.SnakyPrototype.Certificate21.required_exact_568 line 872
  370. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_568 line 876
  371. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_568 line 878
  372. def OAI.SnakyPrototype.Certificate21.checked_568 line 882
  373. def OAI.SnakyPrototype.Certificate21.height_572_i0 line 890
  374. def OAI.SnakyPrototype.Certificate21.childrenH_572_i0 line 891
  375. theorem OAI.SnakyPrototype.Certificate21.height_exact_572_i0 line 892
  376. theorem OAI.SnakyPrototype.Certificate21.required_origin_572_i0 line 893
  377. theorem OAI.SnakyPrototype.Certificate21.required_exact_572_i0 line 895
  378. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_572_i0 line 899
  379. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_572_i0 line 901
  380. def OAI.SnakyPrototype.Certificate21.checked_572_i0 line 905
  381. def OAI.SnakyPrototype.Certificate21.height_572 line 913
  382. def OAI.SnakyPrototype.Certificate21.childrenH_572 line 914
  383. theorem OAI.SnakyPrototype.Certificate21.height_exact_572 line 915
  384. theorem OAI.SnakyPrototype.Certificate21.required_origin_572 line 916
  385. theorem OAI.SnakyPrototype.Certificate21.required_exact_572 line 918
  386. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_572 line 922
  387. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_572 line 924
  388. def OAI.SnakyPrototype.Certificate21.checked_572 line 928
  389. def OAI.SnakyPrototype.Certificate21.height_590 line 936
  390. def OAI.SnakyPrototype.Certificate21.childrenH_590 line 937
  391. theorem OAI.SnakyPrototype.Certificate21.height_exact_590 line 938
  392. theorem OAI.SnakyPrototype.Certificate21.required_origin_590 line 939
  393. theorem OAI.SnakyPrototype.Certificate21.required_exact_590 line 941
  394. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_590 line 945
  395. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_590 line 947
  396. def OAI.SnakyPrototype.Certificate21.checked_590 line 951