This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| is-empty | ⊦ is_empty(x) ↔ x = [] | An Axiom |
| depths-node | ⊦ depths(Node(t0, t1), i) = depths(t0, i + 1) + depths(t1, i + 1) | An Axiom |
| depths-leaf | ⊦ depths(Leaf, i) = i ' | An Axiom |
| max-rec | ⊦ max(i ' + j ' + x) = max(max(i, j), max(min(i, j) ' + x)) | An Axiom |
| max-one | ⊦ max(i ') = i | An Axiom |
| min-rec | ⊦ min(i ' + j ' + x) = min(min(i, j), min(max(i, j) ' + x)) | An Axiom |
| min-one | ⊦ min(i ') = i | An Axiom |
| depths-max | ⊦ i ≤ max(depths(t, i)) | A User Theorem |
| depths-min | ⊦ i ≤ min(depths(t, i)) | A User Theorem |
| depths-nonnil | ⊦ depths(t, i) ≠ [] | A User Theorem |
| depths-one | ⊦ depths(t, i) = j ' ↔ ¬ ¬ (i = j ∧ t = Leaf) | A User Theorem |
| depths-size-one | ⊦ # depths(t, i) = 1 ↔ t = Leaf | A User Theorem |
| first-in | ⊦ depths(t, i) + x = d ' + y → d ∈ depths(t, i) | A User Theorem |
| in-depths-gt | ⊦ d ∈ depths(t, i) → (d < i ↔ false) | A User Theorem |
| max-concat | ⊦ x ≠ [] ∧ y ≠ [] → max(x + y) = max(max(x), max(y)) | A User Theorem |
| max-ge | ⊦ i ∈ x → i ≤ max(x) | A User Theorem |
| max-gt-rec | ⊦ ¬ max(d ' + x) < d | A User Theorem |
| max-in | ⊦ x ≠ [] → max(x) ∈ x | A User Theorem |
| min-concat | ⊦ x ≠ [] ∧ y ≠ [] → min(x + y) = min(min(x), min(y)) | A User Theorem |
| min-in | ⊦ x ≠ [] → min(x) ∈ x | A User Theorem |
| min-le | ⊦ i ∈ x → min(x) ≤ i | A User Theorem |
| min-le-max | ⊦ x ≠ [] → min(x) ≤ max(x) | A User Theorem |
| unique-prefix | ⊦ depths(t0, i) + x = depths(t1, i) + y ↔ x = y ∧ t0 = t1 | A User Theorem |
| unique-prefix-nil | ⊦ depths(t0, i) = depths(t1, i) + y ↔ y = [] ∧ t0 = t1 | A User Theorem |