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: |
|---|---|---|
| Extension | ⊦ s1 = s2 ↔ (∀ a. a ∈ s1 ↔ a ∈ s2) | An Axiom |
| In-empty | ⊦ ¬ a ∈ ∅ | An Axiom |
| In-insert | ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s | An Axiom |
| Subset | ⊦ s1 ⊆ s2 ↔ (∀ a. a ∈ s1 → a ∈ s2) | An Axiom |
| add | ⊦ ¬ a ∈ s ++ b ↔ a ≠ b ∧ ¬ a ∈ s | A User Theorem |
| add-01 | ⊦ s ++ a ++ a = s ++ a | A User Theorem |
| addthree | ⊦ s ++ a ++ b ++ c ++ a = s ++ a ++ b ++ c | A User Theorem |
| addtwo | ⊦ s ++ a ++ b ++ a = s ++ b ++ a | A User Theorem |
| alle | ∀ a. ¬ a ∈ s ⊦ s = ∅ | A User Theorem |
| eq | ⊦ a ∈ s → s ++ a = s | A User Theorem |
| eq-01 | ⊦ ¬ a ∈ s ∧ ¬ a ∈ s0 → (s ++ a = s0 ++ a ↔ s = s0) | A User Theorem |
| eq-02 | ⊦ ¬ a ∈ s → (s ++ a = ∅ ++ b ↔ a = b ∧ s = ∅) | A User Theorem |
| eq-03 | ⊦ s ++ a = s ↔ a ∈ s | A User Theorem |
| eq-04 | ⊦ s ++ b ++ a = s ++ a ++ b ↔ true | A User Theorem |
| eq-05 | ⊦ ∅ ++ a ++ b = ∅ ++ b ++ a ↔ true | A User Theorem |
| eq-06 | ⊦ ∅ ++ a ++ b = ∅ ++ b ++ a | A User Theorem |
| eq-subset | ⊦ s = s0 ↔ s ⊆ s0 ∧ s0 ⊆ s | A User Theorem |
| eqtwo | ⊦ ∅ ++ a ++ b = ∅ ++ a ++ c ↔ b = c | A User Theorem |
| eqtwo-01 | ⊦ ∅ ++ a ++ b = ∅ ++ c ++ b ↔ a = c | A User Theorem |
| in | ⊦ a ∈ s → a ∈ s ++ b | A User Theorem |
| in-01 | ⊦ a ∈ s ++ a | A User Theorem |
| in-02 | ⊦ a ≠ b → (a ∈ s ++ b ↔ a ∈ s) | A User Theorem |
| in-03 | ⊦ ¬ a ∈ s → (a ∈ s ++ b ↔ a = b) | A User Theorem |
| in-04 | ⊦ a ∈ ∅ ++ b ↔ a = b | A User Theorem |
| in-05 | ⊦ s ++ a = s0 ++ b ∧ a ≠ b → a ∈ s0 | A User Theorem |
| in-06 | ⊦ a ∈ s ∧ s = ∅ ++ b → a = b | A User Theorem |
| ins-two | ⊦ a ∈ s → s ++ b ++ a = s ++ b | A User Theorem |
| ne | ⊦ ∅ ≠ s ++ a | A User Theorem |
| ne-01 | ⊦ a ∈ s → s ≠ ∅ | A User Theorem |
| ne-02 | ⊦ a ∈ s → (s = ∅ ↔ false) | A User Theorem |
| one | ⊦ (∀ a. a ∈ s → a = b) ∧ s ≠ ∅ → s = ∅ ++ b | A User Theorem |
| rax | ⊦ a ∈ s ++ b ↔ ¬ ¬(a = b ∨ a ∈ s) | A User Theorem |
| sel | ⊦ s = ∅ ∨ (∃ a. a ∈ s) | A User Theorem |
| sub-add | ⊦ a ∈ s0 → (s ++ a ⊆ s0 ↔ s ⊆ s0) | A User Theorem |
| sub-add-01 | ⊦ s ⊆ s ++ a | A User Theorem |
| sub-add-02 | ⊦ s ++ a ⊆ s0 → s ⊆ s0 | A User Theorem |
| sub-add-03 | ⊦ s ++ a ⊆ s0 ↔ s ⊆ s0 ∧ a ∈ s0 | A User Theorem |
| sub-add-04 | ⊦ s1 ⊆ s2 → s1 ++ a ⊆ s2 ++ a | A User Theorem |
| sub-e | ⊦ ∅ ⊆ s | A User Theorem |
| sub-idem | ⊦ s ⊆ s | A User Theorem |
| sub-in | ⊦ a ∈ s ∧ s ⊆ s0 → a ∈ s0 | A User Theorem |
| sub-insert | ⊦ ¬ a ∈ s → (s ⊆ s0 ++ a ↔ s ⊆ s0) | A User Theorem |
| sub-insert-01 | ⊦ s ⊆ s0 → s ⊆ s0 ++ a | A User Theorem |
| sub-ntrans | ⊦ s ⊆ s0 ∧ ¬ s ⊆ s1 → ¬ s0 ⊆ s1 | A User Theorem |
| sub-ntrans-01 | ⊦ s0 ⊆ s1 ∧ ¬ s ⊆ s1 → ¬ s ⊆ s0 | A User Theorem |
| sub-one-01 | ⊦ s ≠ ∅ ++ a → (s ⊆ ∅ ++ a ↔ s = ∅) | A User Theorem |
| sub-one-02 | ⊦ ∅ ++ a ⊆ s ↔ a ∈ s | A User Theorem |
| sub-trans | ⊦ s ⊆ s0 ∧ s0 ⊆ s1 → s ⊆ s1 | A User Theorem |
| sub-two | ⊦ ∅ ++ a ++ b ⊆ ∅ ++ c ↔ a = b ∧ a = c | A User Theorem |
| subset | ⊦ s ⊆ s ++ a ++ b | A User Theorem |
| subset-empty | ⊦ s ⊆ ∅ ↔ s = ∅ | A User Theorem |
| subset-equal | ⊦ s ⊆ s0 → (s0 ⊆ s ↔ s = s0) | A User Theorem |
| subset-ins | ⊦ s ++ a ⊆ s0 ++ a ++ b ↔ s ⊆ s0 ++ a ++ b | A User Theorem |
| sw | ⊦ s ++ b ++ a = s ++ a ++ b | A User Theorem |
| sw-01 | ⊦ s ++ a ++ b ++ c = s ++ c ++ a ++ b | A User Theorem |
| two | ⊦ a ≠ a0 → (∅ ++ a ++ b = ∅ ++ a0 ++ c ↔ a = c ∧ b = a0) | A User Theorem |
| two-01 | a ∈ s, s ≠ ∅ ++ a ⊦ ∃ b. b ∈ s ∧ b ≠ a | A User Theorem |