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: |
|---|---|---|
| Min-in | ⊦ st ≠ ∅ → st.min ∈ st | An Axiom |
| Min-min | ⊦ a ∈ st → ¬ a < st.min | An Axiom |
| Keys | ⊦ a ∈ st.keys ↔ a ∈ st | An Axiom |
| Butmin | ⊦ st.butmin = st -- st.min | An Axiom |
| butmin-at | ⊦ a ≠ st.min → st.butmin[a] = st[a] | A User Theorem |
| butmin-empty | ⊦ ∅.butmin = ∅ | A User Theorem |
| butmin-id | ⊦ st ≠ ∅ → st.butmin[st.min, st[st.min]] = st | A User Theorem |
| butmin-in | ⊦ a ∈ st.butmin ↔ st ≠ ∅ ∧ a ∈ st ∧ a ≠ st.min | A User Theorem |
| butmin-notin | ⊦ ¬ a ∈ st → ¬ a ∈ st.butmin | A User Theorem |
| butmin-one | ⊦ (∅)[a, d].butmin = ∅ | A User Theorem |
| butmin-put | ⊦ a = st.min ∧ ¬ a ∈ st → st[a, d].butmin = st | A User Theorem |
| butmin-put-01 | ⊦ a = st[a, d0].min ∧ ¬ a ∈ st → st[a, d].butmin = st | A User Theorem |
| butmin-put-02 | ⊦ a = st[a, d].min ∧ ¬ a ∈ st → st[a, d].butmin = st | A User Theorem |
| butmin-put-rew | ⊦ st.min < a ∧ st ≠ ∅ → st.butmin[a, d] = st[a, d].butmin | A User Theorem |
| butmin-rewput | ⊦ a ≠ st[a, d].min → st[a, d].butmin = st.butmin[a, d] | A User Theorem |
| butmin-size | ⊦ st ≠ ∅ → ¬ # st ≤ # st.butmin | A User Theorem |
| butmin-size-01 | ⊦ st ≠ ∅ → # st.butmin = (# st)-1 | A User Theorem |
| del | ⊦ a ∈ (st -- b).keys ↔ a ∈ st.keys ∧ a ≠ b | A User Theorem |
| del-01 | ⊦ a ∈ st.keys → (st -- a).keys = st.keys -- a | A User Theorem |
| empty | ⊦ ∅.keys = ∅ | A User Theorem |
| empty-01 | ⊦ st ≠ ∅ → (¬ st.keys ≠ ∅ ↔ false) | A User Theorem |
| empty-02 | ⊦ a ∈ st → (¬ st.keys ≠ ∅ ↔ false) | A User Theorem |
| inf | ⊦ a ∈ st → a ∈ st.keys | A User Theorem |
| inf-01 | ⊦ a ∈ st.keys → a ∈ st | A User Theorem |
| inkeys | ⊦ a ∈ st ↔ a ∈ st.keys | A User Theorem |
| inkeys-01 | ⊦ a ∈ st → (¬ a ∈ st.keys ↔ false) | A User Theorem |
| insert | ⊦ a ∈ st → st[a, d].keys = st.keys | A User Theorem |
| insert-01 | ⊦ a ∈ s ∧ ¬ b ∈ s → st[b, d][a] = st[a] | A User Theorem |
| insert-02 | ⊦ a ∈ s ∧ ¬ b ∈ s → st[a, d][b] = st[b] | A User Theorem |
| insert-03 | ⊦ st[a, d].keys = st.keys ++ a | A User Theorem |
| k-keys-rec | ⊦ ¬ a ∈ st → st[a, d].keys = st.keys ++ a | A User Theorem |
| min | ⊦ (∅)[a, d].min = a | A User Theorem |
| min-def | ⊦ st ≠ ∅ → st.min = st.keys.min | A User Theorem |
| min-in | ⊦ st.min = a ∧ st ≠ ∅ → a ∈ st | A User Theorem |
| min-put | ⊦ a ≠ st[a, d].min → st[a, d].min = st.min | A User Theorem |
| min-put-01 | ⊦ st[a, d].min = a → st[a, d0].min = a | A User Theorem |
| min-put-ls | ⊦ st.min < a ∧ st ≠ ∅ → st[a, d].min = st.min | A User Theorem |
| mk-in | ⊦ st ≠ ∅ → (¬ st.keys.min ∈ st ↔ false) | A User Theorem |
| neq | ⊦ st[a, d].keys ≠ st.keys ↔ ¬ a ∈ st | A User Theorem |
| notempty | ⊦ a ∈ st.keys → st.keys ≠ ∅ | A User Theorem |
| size-del | ⊦ a ∈ st.keys → ¬ # st.keys ≤ # (st -- a).keys | A User Theorem |
| size-del-01 | ⊦ a ∈ st.keys → # (st -- a).keys = # st.keys - 1 | A User Theorem |
| size-del-02 | ⊦ a ∈ st → ¬ # st.keys ≤ # (st -- a).keys | A User Theorem |
| sub | ⊦ a ∈ s ∧ s ⊆ st.keys → a ∈ st | A User Theorem |