OAI/GameTheory/SnakyTwentyOne/Cards/Height15Part01.lean

GitHub source file

378 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SnakyPrototype.Certificate21.required_573_i0 line 46
  2. def OAI.SnakyPrototype.Certificate21.envelope_573_i0 line 47
  3. def OAI.SnakyPrototype.Certificate21.childrenC_573_i0 line 48
  4. def OAI.SnakyPrototype.Certificate21.childrenD_573_i0 line 49
  5. theorem OAI.SnakyPrototype.Certificate21.common_sub_573_i0 line 50
  6. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_573_i0 line 51
  7. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_573_i0 line 52
  8. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_573_i0 line 53
  9. theorem OAI.SnakyPrototype.Certificate21.children_work_573_i0 line 54
  10. theorem OAI.SnakyPrototype.Certificate21.row_works_573_i0 line 62
  11. def OAI.SnakyPrototype.Certificate21.required_573_i1 line 67
  12. def OAI.SnakyPrototype.Certificate21.envelope_573_i1 line 68
  13. def OAI.SnakyPrototype.Certificate21.childrenC_573_i1 line 69
  14. def OAI.SnakyPrototype.Certificate21.childrenD_573_i1 line 70
  15. theorem OAI.SnakyPrototype.Certificate21.common_sub_573_i1 line 71
  16. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_573_i1 line 72
  17. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_573_i1 line 73
  18. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_573_i1 line 74
  19. theorem OAI.SnakyPrototype.Certificate21.children_work_573_i1 line 75
  20. theorem OAI.SnakyPrototype.Certificate21.row_works_573_i1 line 82
  21. def OAI.SnakyPrototype.Certificate21.required_573_i2 line 87
  22. def OAI.SnakyPrototype.Certificate21.envelope_573_i2 line 88
  23. def OAI.SnakyPrototype.Certificate21.childrenC_573_i2 line 89
  24. def OAI.SnakyPrototype.Certificate21.childrenD_573_i2 line 90
  25. theorem OAI.SnakyPrototype.Certificate21.common_sub_573_i2 line 91
  26. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_573_i2 line 92
  27. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_573_i2 line 93
  28. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_573_i2 line 94
  29. theorem OAI.SnakyPrototype.Certificate21.children_work_573_i2 line 95
  30. theorem OAI.SnakyPrototype.Certificate21.row_works_573_i2 line 102
  31. def OAI.SnakyPrototype.Certificate21.required_573_i3 line 107
  32. def OAI.SnakyPrototype.Certificate21.envelope_573_i3 line 108
  33. def OAI.SnakyPrototype.Certificate21.childrenC_573_i3 line 109
  34. def OAI.SnakyPrototype.Certificate21.childrenD_573_i3 line 110
  35. theorem OAI.SnakyPrototype.Certificate21.common_sub_573_i3 line 111
  36. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_573_i3 line 112
  37. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_573_i3 line 113
  38. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_573_i3 line 114
  39. theorem OAI.SnakyPrototype.Certificate21.children_work_573_i3 line 115
  40. theorem OAI.SnakyPrototype.Certificate21.row_works_573_i3 line 120
  41. def OAI.SnakyPrototype.Certificate21.required_573_i4 line 125
  42. def OAI.SnakyPrototype.Certificate21.envelope_573_i4 line 126
  43. def OAI.SnakyPrototype.Certificate21.childrenC_573_i4 line 127
  44. def OAI.SnakyPrototype.Certificate21.childrenD_573_i4 line 128
  45. theorem OAI.SnakyPrototype.Certificate21.common_sub_573_i4 line 129
  46. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_573_i4 line 130
  47. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_573_i4 line 131
  48. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_573_i4 line 132
  49. theorem OAI.SnakyPrototype.Certificate21.children_work_573_i4 line 133
  50. theorem OAI.SnakyPrototype.Certificate21.row_works_573_i4 line 138
  51. def OAI.SnakyPrototype.Certificate21.required_573_i5 line 143
  52. def OAI.SnakyPrototype.Certificate21.envelope_573_i5 line 144
  53. def OAI.SnakyPrototype.Certificate21.childrenC_573_i5 line 145
  54. def OAI.SnakyPrototype.Certificate21.childrenD_573_i5 line 146
  55. theorem OAI.SnakyPrototype.Certificate21.common_sub_573_i5 line 147
  56. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_573_i5 line 148
  57. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_573_i5 line 149
  58. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_573_i5 line 150
  59. theorem OAI.SnakyPrototype.Certificate21.children_work_573_i5 line 151
  60. theorem OAI.SnakyPrototype.Certificate21.row_works_573_i5 line 158
  61. def OAI.SnakyPrototype.Certificate21.required_573 line 163
  62. def OAI.SnakyPrototype.Certificate21.envelope_573 line 164
  63. def OAI.SnakyPrototype.Certificate21.childrenC_573 line 165
  64. def OAI.SnakyPrototype.Certificate21.childrenD_573 line 166
  65. theorem OAI.SnakyPrototype.Certificate21.common_sub_573 line 167
  66. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_573 line 168
  67. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_573 line 169
  68. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_573 line 170
  69. theorem OAI.SnakyPrototype.Certificate21.children_work_573 line 171
  70. theorem OAI.SnakyPrototype.Certificate21.row_works_573 line 184
  71. def OAI.SnakyPrototype.Certificate21.required_583_i2 line 189
  72. def OAI.SnakyPrototype.Certificate21.envelope_583_i2 line 190
  73. def OAI.SnakyPrototype.Certificate21.childrenC_583_i2 line 191
  74. def OAI.SnakyPrototype.Certificate21.childrenD_583_i2 line 192
  75. theorem OAI.SnakyPrototype.Certificate21.common_sub_583_i2 line 193
  76. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_583_i2 line 194
  77. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_583_i2 line 195
  78. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_583_i2 line 196
  79. theorem OAI.SnakyPrototype.Certificate21.children_work_583_i2 line 197
  80. theorem OAI.SnakyPrototype.Certificate21.row_works_583_i2 line 202
  81. def OAI.SnakyPrototype.Certificate21.required_583_i3 line 207
  82. def OAI.SnakyPrototype.Certificate21.envelope_583_i3 line 208
  83. def OAI.SnakyPrototype.Certificate21.childrenC_583_i3 line 209
  84. def OAI.SnakyPrototype.Certificate21.childrenD_583_i3 line 210
  85. theorem OAI.SnakyPrototype.Certificate21.common_sub_583_i3 line 211
  86. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_583_i3 line 212
  87. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_583_i3 line 213
  88. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_583_i3 line 214
  89. theorem OAI.SnakyPrototype.Certificate21.children_work_583_i3 line 215
  90. theorem OAI.SnakyPrototype.Certificate21.row_works_583_i3 line 220
  91. def OAI.SnakyPrototype.Certificate21.required_583_i1 line 225
  92. def OAI.SnakyPrototype.Certificate21.envelope_583_i1 line 226
  93. def OAI.SnakyPrototype.Certificate21.childrenC_583_i1 line 227
  94. def OAI.SnakyPrototype.Certificate21.childrenD_583_i1 line 228
  95. theorem OAI.SnakyPrototype.Certificate21.common_sub_583_i1 line 229
  96. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_583_i1 line 230
  97. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_583_i1 line 231
  98. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_583_i1 line 232
  99. theorem OAI.SnakyPrototype.Certificate21.children_work_583_i1 line 233
  100. theorem OAI.SnakyPrototype.Certificate21.row_works_583_i1 line 240
  101. def OAI.SnakyPrototype.Certificate21.required_583_i0 line 245
  102. def OAI.SnakyPrototype.Certificate21.envelope_583_i0 line 246
  103. def OAI.SnakyPrototype.Certificate21.childrenC_583_i0 line 247
  104. def OAI.SnakyPrototype.Certificate21.childrenD_583_i0 line 248
  105. theorem OAI.SnakyPrototype.Certificate21.common_sub_583_i0 line 249
  106. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_583_i0 line 250
  107. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_583_i0 line 251
  108. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_583_i0 line 252
  109. theorem OAI.SnakyPrototype.Certificate21.children_work_583_i0 line 253
  110. theorem OAI.SnakyPrototype.Certificate21.row_works_583_i0 line 258
  111. def OAI.SnakyPrototype.Certificate21.required_583_i5 line 263
  112. def OAI.SnakyPrototype.Certificate21.envelope_583_i5 line 264
  113. def OAI.SnakyPrototype.Certificate21.childrenC_583_i5 line 265
  114. def OAI.SnakyPrototype.Certificate21.childrenD_583_i5 line 266
  115. theorem OAI.SnakyPrototype.Certificate21.common_sub_583_i5 line 267
  116. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_583_i5 line 268
  117. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_583_i5 line 269
  118. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_583_i5 line 270
  119. theorem OAI.SnakyPrototype.Certificate21.children_work_583_i5 line 271
  120. theorem OAI.SnakyPrototype.Certificate21.row_works_583_i5 line 277
  121. def OAI.SnakyPrototype.Certificate21.required_583_i6 line 282
  122. def OAI.SnakyPrototype.Certificate21.envelope_583_i6 line 283
  123. def OAI.SnakyPrototype.Certificate21.childrenC_583_i6 line 284
  124. def OAI.SnakyPrototype.Certificate21.childrenD_583_i6 line 285
  125. theorem OAI.SnakyPrototype.Certificate21.common_sub_583_i6 line 286
  126. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_583_i6 line 287
  127. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_583_i6 line 288
  128. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_583_i6 line 289
  129. theorem OAI.SnakyPrototype.Certificate21.children_work_583_i6 line 290
  130. theorem OAI.SnakyPrototype.Certificate21.row_works_583_i6 line 296
  131. def OAI.SnakyPrototype.Certificate21.required_583_i4 line 301
  132. def OAI.SnakyPrototype.Certificate21.envelope_583_i4 line 302
  133. def OAI.SnakyPrototype.Certificate21.childrenC_583_i4 line 303
  134. def OAI.SnakyPrototype.Certificate21.childrenD_583_i4 line 304
  135. theorem OAI.SnakyPrototype.Certificate21.common_sub_583_i4 line 305
  136. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_583_i4 line 306
  137. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_583_i4 line 307
  138. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_583_i4 line 308
  139. theorem OAI.SnakyPrototype.Certificate21.children_work_583_i4 line 309
  140. theorem OAI.SnakyPrototype.Certificate21.row_works_583_i4 line 317
  141. def OAI.SnakyPrototype.Certificate21.required_583 line 322
  142. def OAI.SnakyPrototype.Certificate21.envelope_583 line 323
  143. def OAI.SnakyPrototype.Certificate21.childrenC_583 line 324
  144. def OAI.SnakyPrototype.Certificate21.childrenD_583 line 325
  145. theorem OAI.SnakyPrototype.Certificate21.common_sub_583 line 326
  146. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_583 line 327
  147. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_583 line 328
  148. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_583 line 329
  149. theorem OAI.SnakyPrototype.Certificate21.children_work_583 line 330
  150. theorem OAI.SnakyPrototype.Certificate21.row_works_583 line 341
  151. def OAI.SnakyPrototype.Certificate21.required_648 line 346
  152. def OAI.SnakyPrototype.Certificate21.envelope_648 line 347
  153. def OAI.SnakyPrototype.Certificate21.childrenC_648 line 348
  154. def OAI.SnakyPrototype.Certificate21.childrenD_648 line 349
  155. theorem OAI.SnakyPrototype.Certificate21.common_sub_648 line 350
  156. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_648 line 351
  157. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_648 line 352
  158. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_648 line 353
  159. theorem OAI.SnakyPrototype.Certificate21.children_work_648 line 354
  160. theorem OAI.SnakyPrototype.Certificate21.row_works_648 line 369
  161. def OAI.SnakyPrototype.Certificate21.required_656_i1 line 374
  162. def OAI.SnakyPrototype.Certificate21.envelope_656_i1 line 375
  163. def OAI.SnakyPrototype.Certificate21.childrenC_656_i1 line 376
  164. def OAI.SnakyPrototype.Certificate21.childrenD_656_i1 line 377
  165. theorem OAI.SnakyPrototype.Certificate21.common_sub_656_i1 line 378
  166. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_656_i1 line 379
  167. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_656_i1 line 380
  168. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_656_i1 line 381
  169. theorem OAI.SnakyPrototype.Certificate21.children_work_656_i1 line 382
  170. theorem OAI.SnakyPrototype.Certificate21.row_works_656_i1 line 392
  171. def OAI.SnakyPrototype.Certificate21.required_656_i2 line 397
  172. def OAI.SnakyPrototype.Certificate21.envelope_656_i2 line 398
  173. def OAI.SnakyPrototype.Certificate21.childrenC_656_i2 line 399
  174. def OAI.SnakyPrototype.Certificate21.childrenD_656_i2 line 400
  175. theorem OAI.SnakyPrototype.Certificate21.common_sub_656_i2 line 401
  176. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_656_i2 line 402
  177. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_656_i2 line 403
  178. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_656_i2 line 404
  179. theorem OAI.SnakyPrototype.Certificate21.children_work_656_i2 line 405
  180. theorem OAI.SnakyPrototype.Certificate21.row_works_656_i2 line 410
  181. def OAI.SnakyPrototype.Certificate21.required_656_i3 line 415
  182. def OAI.SnakyPrototype.Certificate21.envelope_656_i3 line 416
  183. def OAI.SnakyPrototype.Certificate21.childrenC_656_i3 line 417
  184. def OAI.SnakyPrototype.Certificate21.childrenD_656_i3 line 418
  185. theorem OAI.SnakyPrototype.Certificate21.common_sub_656_i3 line 419
  186. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_656_i3 line 420
  187. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_656_i3 line 421
  188. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_656_i3 line 422
  189. theorem OAI.SnakyPrototype.Certificate21.children_work_656_i3 line 423
  190. theorem OAI.SnakyPrototype.Certificate21.row_works_656_i3 line 428
  191. def OAI.SnakyPrototype.Certificate21.required_656_i0 line 433
  192. def OAI.SnakyPrototype.Certificate21.envelope_656_i0 line 434
  193. def OAI.SnakyPrototype.Certificate21.childrenC_656_i0 line 435
  194. def OAI.SnakyPrototype.Certificate21.childrenD_656_i0 line 436
  195. theorem OAI.SnakyPrototype.Certificate21.common_sub_656_i0 line 437
  196. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_656_i0 line 438
  197. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_656_i0 line 439
  198. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_656_i0 line 440
  199. theorem OAI.SnakyPrototype.Certificate21.children_work_656_i0 line 441
  200. theorem OAI.SnakyPrototype.Certificate21.row_works_656_i0 line 452
  201. def OAI.SnakyPrototype.Certificate21.required_656 line 457
  202. def OAI.SnakyPrototype.Certificate21.envelope_656 line 458
  203. def OAI.SnakyPrototype.Certificate21.childrenC_656 line 459
  204. def OAI.SnakyPrototype.Certificate21.childrenD_656 line 460
  205. theorem OAI.SnakyPrototype.Certificate21.common_sub_656 line 461
  206. theorem OAI.SnakyPrototype.Certificate21.child_required_sub_656 line 462
  207. theorem OAI.SnakyPrototype.Certificate21.child_envelope_sub_656 line 463
  208. theorem OAI.SnakyPrototype.Certificate21.pivot_mem_656 line 464
  209. theorem OAI.SnakyPrototype.Certificate21.children_work_656 line 465
  210. theorem OAI.SnakyPrototype.Certificate21.row_works_656 line 479
  211. def OAI.SnakyPrototype.Certificate21.height_573_i0 line 484
  212. def OAI.SnakyPrototype.Certificate21.childrenH_573_i0 line 485
  213. theorem OAI.SnakyPrototype.Certificate21.height_exact_573_i0 line 486
  214. theorem OAI.SnakyPrototype.Certificate21.required_origin_573_i0 line 487
  215. theorem OAI.SnakyPrototype.Certificate21.required_exact_573_i0 line 489
  216. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_573_i0 line 493
  217. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_573_i0 line 495
  218. def OAI.SnakyPrototype.Certificate21.checked_573_i0 line 499
  219. def OAI.SnakyPrototype.Certificate21.height_573_i1 line 507
  220. def OAI.SnakyPrototype.Certificate21.childrenH_573_i1 line 508
  221. theorem OAI.SnakyPrototype.Certificate21.height_exact_573_i1 line 509
  222. theorem OAI.SnakyPrototype.Certificate21.required_origin_573_i1 line 510
  223. theorem OAI.SnakyPrototype.Certificate21.required_exact_573_i1 line 512
  224. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_573_i1 line 516
  225. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_573_i1 line 518
  226. def OAI.SnakyPrototype.Certificate21.checked_573_i1 line 522
  227. def OAI.SnakyPrototype.Certificate21.height_573_i2 line 530
  228. def OAI.SnakyPrototype.Certificate21.childrenH_573_i2 line 531
  229. theorem OAI.SnakyPrototype.Certificate21.height_exact_573_i2 line 532
  230. theorem OAI.SnakyPrototype.Certificate21.required_origin_573_i2 line 533
  231. theorem OAI.SnakyPrototype.Certificate21.required_exact_573_i2 line 535
  232. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_573_i2 line 539
  233. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_573_i2 line 541
  234. def OAI.SnakyPrototype.Certificate21.checked_573_i2 line 545
  235. def OAI.SnakyPrototype.Certificate21.height_573_i3 line 553
  236. def OAI.SnakyPrototype.Certificate21.childrenH_573_i3 line 554
  237. theorem OAI.SnakyPrototype.Certificate21.height_exact_573_i3 line 555
  238. theorem OAI.SnakyPrototype.Certificate21.required_origin_573_i3 line 556
  239. theorem OAI.SnakyPrototype.Certificate21.required_exact_573_i3 line 558
  240. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_573_i3 line 562
  241. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_573_i3 line 564
  242. def OAI.SnakyPrototype.Certificate21.checked_573_i3 line 568
  243. def OAI.SnakyPrototype.Certificate21.height_573_i4 line 576
  244. def OAI.SnakyPrototype.Certificate21.childrenH_573_i4 line 577
  245. theorem OAI.SnakyPrototype.Certificate21.height_exact_573_i4 line 578
  246. theorem OAI.SnakyPrototype.Certificate21.required_origin_573_i4 line 579
  247. theorem OAI.SnakyPrototype.Certificate21.required_exact_573_i4 line 581
  248. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_573_i4 line 585
  249. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_573_i4 line 587
  250. def OAI.SnakyPrototype.Certificate21.checked_573_i4 line 591
  251. def OAI.SnakyPrototype.Certificate21.height_573_i5 line 599
  252. def OAI.SnakyPrototype.Certificate21.childrenH_573_i5 line 600
  253. theorem OAI.SnakyPrototype.Certificate21.height_exact_573_i5 line 601
  254. theorem OAI.SnakyPrototype.Certificate21.required_origin_573_i5 line 602
  255. theorem OAI.SnakyPrototype.Certificate21.required_exact_573_i5 line 604
  256. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_573_i5 line 608
  257. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_573_i5 line 610
  258. def OAI.SnakyPrototype.Certificate21.checked_573_i5 line 614
  259. def OAI.SnakyPrototype.Certificate21.height_573 line 622
  260. def OAI.SnakyPrototype.Certificate21.childrenH_573 line 623
  261. theorem OAI.SnakyPrototype.Certificate21.height_exact_573 line 624
  262. theorem OAI.SnakyPrototype.Certificate21.required_origin_573 line 625
  263. theorem OAI.SnakyPrototype.Certificate21.required_exact_573 line 627
  264. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_573 line 631
  265. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_573 line 633
  266. def OAI.SnakyPrototype.Certificate21.checked_573 line 637
  267. def OAI.SnakyPrototype.Certificate21.height_583_i2 line 645
  268. def OAI.SnakyPrototype.Certificate21.childrenH_583_i2 line 646
  269. theorem OAI.SnakyPrototype.Certificate21.height_exact_583_i2 line 647
  270. theorem OAI.SnakyPrototype.Certificate21.required_origin_583_i2 line 648
  271. theorem OAI.SnakyPrototype.Certificate21.required_exact_583_i2 line 650
  272. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_583_i2 line 654
  273. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_583_i2 line 656
  274. def OAI.SnakyPrototype.Certificate21.checked_583_i2 line 660
  275. def OAI.SnakyPrototype.Certificate21.height_583_i3 line 668
  276. def OAI.SnakyPrototype.Certificate21.childrenH_583_i3 line 669
  277. theorem OAI.SnakyPrototype.Certificate21.height_exact_583_i3 line 670
  278. theorem OAI.SnakyPrototype.Certificate21.required_origin_583_i3 line 671
  279. theorem OAI.SnakyPrototype.Certificate21.required_exact_583_i3 line 673
  280. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_583_i3 line 677
  281. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_583_i3 line 679
  282. def OAI.SnakyPrototype.Certificate21.checked_583_i3 line 683
  283. def OAI.SnakyPrototype.Certificate21.height_583_i1 line 691
  284. def OAI.SnakyPrototype.Certificate21.childrenH_583_i1 line 692
  285. theorem OAI.SnakyPrototype.Certificate21.height_exact_583_i1 line 693
  286. theorem OAI.SnakyPrototype.Certificate21.required_origin_583_i1 line 694
  287. theorem OAI.SnakyPrototype.Certificate21.required_exact_583_i1 line 696
  288. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_583_i1 line 700
  289. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_583_i1 line 702
  290. def OAI.SnakyPrototype.Certificate21.checked_583_i1 line 706
  291. def OAI.SnakyPrototype.Certificate21.height_583_i0 line 714
  292. def OAI.SnakyPrototype.Certificate21.childrenH_583_i0 line 715
  293. theorem OAI.SnakyPrototype.Certificate21.height_exact_583_i0 line 716
  294. theorem OAI.SnakyPrototype.Certificate21.required_origin_583_i0 line 717
  295. theorem OAI.SnakyPrototype.Certificate21.required_exact_583_i0 line 719
  296. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_583_i0 line 723
  297. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_583_i0 line 725
  298. def OAI.SnakyPrototype.Certificate21.checked_583_i0 line 729
  299. def OAI.SnakyPrototype.Certificate21.height_583_i5 line 737
  300. def OAI.SnakyPrototype.Certificate21.childrenH_583_i5 line 738
  301. theorem OAI.SnakyPrototype.Certificate21.height_exact_583_i5 line 739
  302. theorem OAI.SnakyPrototype.Certificate21.required_origin_583_i5 line 740
  303. theorem OAI.SnakyPrototype.Certificate21.required_exact_583_i5 line 742
  304. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_583_i5 line 746
  305. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_583_i5 line 748
  306. def OAI.SnakyPrototype.Certificate21.checked_583_i5 line 752
  307. def OAI.SnakyPrototype.Certificate21.height_583_i6 line 760
  308. def OAI.SnakyPrototype.Certificate21.childrenH_583_i6 line 761
  309. theorem OAI.SnakyPrototype.Certificate21.height_exact_583_i6 line 762
  310. theorem OAI.SnakyPrototype.Certificate21.required_origin_583_i6 line 763
  311. theorem OAI.SnakyPrototype.Certificate21.required_exact_583_i6 line 765
  312. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_583_i6 line 769
  313. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_583_i6 line 771
  314. def OAI.SnakyPrototype.Certificate21.checked_583_i6 line 775
  315. def OAI.SnakyPrototype.Certificate21.height_583_i4 line 783
  316. def OAI.SnakyPrototype.Certificate21.childrenH_583_i4 line 784
  317. theorem OAI.SnakyPrototype.Certificate21.height_exact_583_i4 line 785
  318. theorem OAI.SnakyPrototype.Certificate21.required_origin_583_i4 line 786
  319. theorem OAI.SnakyPrototype.Certificate21.required_exact_583_i4 line 788
  320. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_583_i4 line 792
  321. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_583_i4 line 794
  322. def OAI.SnakyPrototype.Certificate21.checked_583_i4 line 798
  323. def OAI.SnakyPrototype.Certificate21.height_583 line 806
  324. def OAI.SnakyPrototype.Certificate21.childrenH_583 line 807
  325. theorem OAI.SnakyPrototype.Certificate21.height_exact_583 line 808
  326. theorem OAI.SnakyPrototype.Certificate21.required_origin_583 line 809
  327. theorem OAI.SnakyPrototype.Certificate21.required_exact_583 line 811
  328. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_583 line 815
  329. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_583 line 817
  330. def OAI.SnakyPrototype.Certificate21.checked_583 line 821
  331. def OAI.SnakyPrototype.Certificate21.height_648 line 829
  332. def OAI.SnakyPrototype.Certificate21.childrenH_648 line 830
  333. theorem OAI.SnakyPrototype.Certificate21.height_exact_648 line 831
  334. theorem OAI.SnakyPrototype.Certificate21.required_origin_648 line 832
  335. theorem OAI.SnakyPrototype.Certificate21.required_exact_648 line 834
  336. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_648 line 838
  337. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_648 line 840
  338. def OAI.SnakyPrototype.Certificate21.checked_648 line 844
  339. def OAI.SnakyPrototype.Certificate21.height_656_i1 line 852
  340. def OAI.SnakyPrototype.Certificate21.childrenH_656_i1 line 853
  341. theorem OAI.SnakyPrototype.Certificate21.height_exact_656_i1 line 854
  342. theorem OAI.SnakyPrototype.Certificate21.required_origin_656_i1 line 855
  343. theorem OAI.SnakyPrototype.Certificate21.required_exact_656_i1 line 857
  344. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_656_i1 line 861
  345. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_656_i1 line 863
  346. def OAI.SnakyPrototype.Certificate21.checked_656_i1 line 867
  347. def OAI.SnakyPrototype.Certificate21.height_656_i2 line 875
  348. def OAI.SnakyPrototype.Certificate21.childrenH_656_i2 line 876
  349. theorem OAI.SnakyPrototype.Certificate21.height_exact_656_i2 line 877
  350. theorem OAI.SnakyPrototype.Certificate21.required_origin_656_i2 line 878
  351. theorem OAI.SnakyPrototype.Certificate21.required_exact_656_i2 line 880
  352. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_656_i2 line 884
  353. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_656_i2 line 886
  354. def OAI.SnakyPrototype.Certificate21.checked_656_i2 line 890
  355. def OAI.SnakyPrototype.Certificate21.height_656_i3 line 898
  356. def OAI.SnakyPrototype.Certificate21.childrenH_656_i3 line 899
  357. theorem OAI.SnakyPrototype.Certificate21.height_exact_656_i3 line 900
  358. theorem OAI.SnakyPrototype.Certificate21.required_origin_656_i3 line 901
  359. theorem OAI.SnakyPrototype.Certificate21.required_exact_656_i3 line 903
  360. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_656_i3 line 907
  361. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_656_i3 line 909
  362. def OAI.SnakyPrototype.Certificate21.checked_656_i3 line 913
  363. def OAI.SnakyPrototype.Certificate21.height_656_i0 line 921
  364. def OAI.SnakyPrototype.Certificate21.childrenH_656_i0 line 922
  365. theorem OAI.SnakyPrototype.Certificate21.height_exact_656_i0 line 923
  366. theorem OAI.SnakyPrototype.Certificate21.required_origin_656_i0 line 924
  367. theorem OAI.SnakyPrototype.Certificate21.required_exact_656_i0 line 926
  368. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_656_i0 line 930
  369. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_656_i0 line 932
  370. def OAI.SnakyPrototype.Certificate21.checked_656_i0 line 936
  371. def OAI.SnakyPrototype.Certificate21.height_656 line 944
  372. def OAI.SnakyPrototype.Certificate21.childrenH_656 line 945
  373. theorem OAI.SnakyPrototype.Certificate21.height_exact_656 line 946
  374. theorem OAI.SnakyPrototype.Certificate21.required_origin_656 line 947
  375. theorem OAI.SnakyPrototype.Certificate21.required_exact_656 line 949
  376. theorem OAI.SnakyPrototype.Certificate21.envelope_origin_656 line 953
  377. theorem OAI.SnakyPrototype.Certificate21.envelope_exact_656 line 955
  378. def OAI.SnakyPrototype.Certificate21.checked_656 line 959