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: |
|---|---|---|
| Union | ⊦ a ∈ s1 ∪ s2 ↔ a ∈ s1 ∨ a ∈ s2 | An Axiom |
| Intersect | ⊦ a ∈ s1 ∩ s2 ↔ a ∈ s1 ∧ a ∈ s2 | An Axiom |
| Difference | ⊦ a ∈ s1 \ s2 ↔ a ∈ s1 ∧ ¬ a ∈ s2 | An Axiom |
| Delete | ⊦ a ∈ s -- b ↔ a ≠ b ∧ a ∈ s | An Axiom |
| One | ⊦ {a} = ∅ ++ a | An Axiom |
| del | a ∈ s ⊦ ∃ s0. s = s0 ++ a ∧ ¬ a ∈ s0 | A User Theorem |
| del-addeq | ⊦ a ≠ b ∧ ¬ a ∈ s ∧ ¬ a ∈ s0 → ((s ++ a) -- b = s0 ++ a ↔ s -- b = s0) | A User Theorem |
| del-addeq-01 | ⊦ (s ++ a) -- b -- a = s -- b -- a | A User Theorem |
| del-addeq-02 | ⊦ a ∈ s → (s -- a) ++ a = s | A User Theorem |
| del-addeq-03 | ⊦ a ∈ s ∧ a ≠ b → (s -- b) ++ a = s -- b | A User Theorem |
| del-addeq-04 | ⊦ ¬ a ∈ s → (s ++ a) -- a = s | A User Theorem |
| del-addeq-05 | ⊦ (s ++ a) -- a = s -- a | A User Theorem |
| del-addeq-06 | ⊦ (s ++ a ++ b) -- a = (s ++ b) -- a | A User Theorem |
| del-addin | ⊦ ¬ a ∈ s → (a ∈ (s -- a0) ++ b ++ c ↔ a = b ∨ a = c) | A User Theorem |
| del-addin-01 | ⊦ ¬ a ∈ s → (a ∈ (s -- b) ++ c ↔ a = c) | A User Theorem |
| del-d | ⊦ s -- a -- a = s -- a | A User Theorem |
| del-d-01 | ⊦ s -- a -- b -- a = s -- b -- a | A User Theorem |
| del-del-one | ⊦ a ≠ b → (∅ ++ a) -- b = ∅ ++ a | A User Theorem |
| del-e | ⊦ ¬ a ∈ s → ((s ++ a) -- b = ∅ ↔ s = ∅ ∧ a = b) | A User Theorem |
| del-e-01 | ⊦ ∅ -- a = ∅ | A User Theorem |
| del-e-02 | ⊦ s -- a = ∅ ↔ s = ∅ ∨ s = ∅ ++ a | A User Theorem |
| del-eq | ⊦ a ∈ s ∧ a ∈ s0 → (s -- a = s0 -- a ↔ s = s0) | A User Theorem |
| del-feq | ⊦ s -- a = s0 ++ b → a ≠ b ∧ b ∈ s ∧ ¬ a ∈ s0 | A User Theorem |
| del-feq-01 | ⊦ (s ++ a) -- b = s0 ++ c ∧ ¬ c ∈ s → a = c ∧ b ≠ c | A User Theorem |
| del-feq-02 | ⊦ (s ++ a) -- b = s0 ++ c ∧ a ≠ b ∧ ¬ a ∈ s0 → a = c | A User Theorem |
| del-in | ⊦ ¬ a ∈ s → s -- a = s | A User Theorem |
| del-in-01 | ⊦ a ≠ b → (¬ a ∈ s -- b ↔ ¬ a ∈ s) | A User Theorem |
| del-in-02 | ⊦ ¬ a ∈ s -- a | A User Theorem |
| del-in-03 | ⊦ s -- a = s ↔ ¬ a ∈ s | A User Theorem |
| del-neq | ⊦ s -- a ≠ s0 -- a → s ≠ s0 | A User Theorem |
| del-neq-01 | ⊦ a ≠ b → (s ++ a) -- b ≠ ∅ | A User Theorem |
| del-neq-02 | ⊦ s -- a ≠ s0 ++ a | A User Theorem |
| del-notin | ⊦ s0 = s -- a → ¬ a ∈ s0 | A User Theorem |
| del-rax | ⊦ a ∈ s -- b ↔ ¬ ¬(a ≠ b ∧ a ∈ s) | A User Theorem |
| del-two | s -- a -- b = ∅ ⊦ s = ∅ ∨ s = ∅ ++ a ∨ s = ∅ ++ b ∨ s = ∅ ++ a ++ b | A User Theorem |
| delete-insert | ⊦ (s -- a) ++ a = s ++ a | A User Theorem |
| delete-subset | ⊦ (s -- a) ++ b ⊆ s ++ b | A User Theorem |
| delsw | ⊦ a ≠ b → (s ++ b) -- a = (s -- a) ++ b | A User Theorem |
| delsw-01 | ⊦ s -- b -- a = s -- a -- b | A User Theorem |
| delsw-02 | ⊦ s -- b -- a = s -- a -- b ↔ true | A User Theorem |
| diff-add-del | ⊦ s1 \ (s2 ++ a) = (s1 \ s2) -- a | A User Theorem |
| diff-add-del-01 | ⊦ ¬ a ∈ s1 → s1 \ (s2 ++ a) = s1 \ s2 | A User Theorem |
| diff-del | ⊦ s = s1 \ s2 ∧ ¬ a ∈ s → (s = (s1 -- a) \ (s2 -- a) ↔ true) | A User Theorem |
| diff-del-01 | ⊦ ¬ a ∈ s → s \ s0 ⊆ (s \ s0) -- a | A User Theorem |
| diff-del-02 | ⊦ ¬ a ∈ s → s \ s0 ⊆ ((s \ s0) -- a) ++ b | A User Theorem |
| diff-e | ⊦ s \ ∅ = s | A User Theorem |
| diff-e-01 | ⊦ ∅ \ s = ∅ | A User Theorem |
| diff-empty | ⊦ s1 \ s2 = ∅ ∧ a ∈ s1 → a ∈ s2 | A User Theorem |
| diff-idem | ⊦ s \ s = ∅ | A User Theorem |
| diff-int | ⊦ (s \ s0) ∩ s0 = ∅ | A User Theorem |
| diff-int-01 | ⊦ (s \ (s0 ∪ s1)) ∩ s0 = ∅ | A User Theorem |
| diff-nin | ⊦ s = s1 \ s2 ∧ a ∈ s2 → ¬ a ∈ s | A User Theorem |
| diff-one | ⊦ (∅ ++ a) \ s ⊆ s0 ++ a | A User Theorem |
| diff-rc | ⊦ (s \ s1) \ s2 = (s \ s2) \ s1 | A User Theorem |
| diff-sub | ⊦ s \ s0 ⊆ s | A User Theorem |
| diff-subset | ⊦ s \ (s0 ∪ s1) ⊆ s \ s1 | A User Theorem |
| diff-subset-01 | ⊦ ((s -- a) ++ b) \ s0 ⊆ ((s \ s0) -- a) ++ b | A User Theorem |
| diff-union | ⊦ a ∈ s0 → (a ∈ (s \ s0) ∪ s1 ↔ a ∈ s1) | A User Theorem |
| diff-union-01 | ⊦ ¬ a ∈ s → (a ∈ (s \ s0) ∪ s1 ↔ a ∈ s1) | A User Theorem |
| diff-union-02 | ⊦ ¬ a ∈ s → (a ∈ ((s ∪ s2) \ s0) ∪ s1 ↔ a ∈ (s2 \ s0) ∪ s1) | A User Theorem |
| diff-union-03 | ⊦ (s ∪ s0) \ s1 = (s \ s1) ∪ (s0 \ s1) | A User Theorem |
| equal-add-in | ⊦ s ++ a = s0 ++ b ∧ s0 ++ b = (s1 -- c) ++ a0 ∧ b ≠ a0 → b ∈ s1 -- c | A User Theorem |
| ext | ⊦ s1 = s2 ↔ (∀ a. a ∈ s1 ↔ a ∈ s2) | A User Theorem |
| indef | ⊦ a ∈ s ↔ (∃ s0. s = s0 ++ a ∧ ¬ a ∈ s0) | A User Theorem |
| insdel-sub | ⊦ ¬ s -- a ⊆ s0 ∧ a ∈ s → ¬ s ⊆ s0 ++ a | A User Theorem |
| int-a | ⊦ (s ∩ s0) ∩ s1 = s ∩ s0 ∩ s1 | A User Theorem |
| int-c | ⊦ s ∩ s0 = s0 ∩ s | A User Theorem |
| int-del-rew | ⊦ ¬ a ∈ s → s ∩ (s0 -- a) = (s ∩ s0) -- a | A User Theorem |
| int-e | ⊦ s ∩ ∅ = ∅ | A User Theorem |
| int-empty | ⊦ s ∩ s0 = ∅ ∧ ¬ a ∈ s → s ∩ (s0 ++ a) = ∅ | A User Theorem |
| int-empty-01 | ⊦ s ∩ s0 = ∅ ↔ (∀ a. ¬ a ∈ s ∨ ¬ a ∈ s0) | A User Theorem |
| int-empty-02 | ⊦ s ∩ s0 = ∅ ∧ a ∈ s → (¬ ¬ a ∈ s0 ↔ false) | A User Theorem |
| int-eq | ⊦ s = s ∩ s0 ↔ s ⊆ s0 | A User Theorem |
| int-idem | ⊦ s ∩ s = s | A User Theorem |
| int-ins | ⊦ s ∩ (s0 ++ a) = ∅ ↔ s ∩ s0 = ∅ ∧ ¬ a ∈ s | A User Theorem |
| int-inse | ⊦ s ∩ (s0 ++ a) = ∅ → s ∩ s0 = ∅ ∧ ¬ a ∈ s | A User Theorem |
| int-inserte | ⊦ a ∈ s → s ∩ (s0 ++ a) ≠ ∅ | A User Theorem |
| int-notempty | ⊦ s ∩ s0 = ∅ → (s ∩ (s0 ++ b) ≠ ∅ ↔ b ∈ s) | A User Theorem |
| int-notempty-01 | ⊦ s ∩ s0 = ∅ → (s ∩ ((s0 -- a) ++ b) ≠ ∅ ↔ b ∈ s) | A User Theorem |
| int-rax | ⊦ a ∈ s1 ∩ s2 ↔ ¬ ¬(a ∈ s1 ∧ a ∈ s2) | A User Theorem |
| int-subs01 | ⊦ s ∩ s0 ⊆ s | A User Theorem |
| intdel-empty | ⊦ (s -- a) ∩ s0 ≠ ∅ → s ∩ s0 ≠ ∅ | A User Theorem |
| intexin | s ∩ s0 ≠ ∅ ⊦ ∃ a. a ∈ s ∧ a ∈ s0 | A User Theorem |
| intu-empty | ⊦ s ∩ (s0 ∪ s1) = ∅ ↔ s ∩ s0 = ∅ ∧ s ∩ s1 = ∅ | A User Theorem |
| one-in | ⊦ a ∈ {b} ↔ a = b | A User Theorem |
| one-min | ⊦ s = ∅ ++ a → s -- a = ∅ | A User Theorem |
| selsub-diff | s1 ⊆ s2 ⊦ s1 = s2, ∃ s. s ⊆ s2 ∧ s1 = s2 \ s | A User Theorem |
| sub-ade | ⊦ s ⊆ s0 → (s -- a) ++ b ⊆ (s0 -- a) ++ b | A User Theorem |
| sub-ade-01 | ⊦ s ⊆ s0 → (s -- a) ++ b ++ c ⊆ (s0 -- a) ++ b ++ c | A User Theorem |
| sub-ade-02 | ⊦ s ⊆ s0 ∧ ¬ a ∈ s → s ⊆ (s0 -- a) ++ b | A User Theorem |
| sub-ade-03 | ⊦ s ⊆ s0 ∧ ¬ a ∈ s → s ⊆ (s0 -- a) ++ b ++ c | A User Theorem |
| sub-del | ⊦ s ⊆ s0 → s -- a ⊆ s0 -- a | A User Theorem |
| sub-del-01 | ⊦ s ⊆ s0 ∧ ¬ a ∈ s → s ⊆ s0 -- a | A User Theorem |
| sub-del-02 | ⊦ s -- a ⊆ s | A User Theorem |
| sub-del-03 | ⊦ s ⊆ s0 → s -- a ⊆ s0 | A User Theorem |
| sub-del-04 | ⊦ s ⊆ s0 -- a ↔ s ⊆ s0 ∧ ¬ a ∈ s | A User Theorem |
| sub-del-05 | ⊦ a ≠ b ∧ ¬ a ∈ s → s -- b ⊆ s -- b -- a | A User Theorem |
| sub-union | ⊦ s ⊆ s0 → s ⊆ s0 ∪ s1 | A User Theorem |
| sub-union-01 | ⊦ s ⊆ s0 → s ⊆ (s0 ∪ s1) ++ a | A User Theorem |
| sub-union-02 | ⊦ s ⊆ (s ∪ s0) ++ a ++ b | A User Theorem |
| sub-union-03 | ⊦ s ++ a ⊆ (s ∪ s0) ++ a | A User Theorem |
| sub-union-04 | ⊦ s ++ a ⊆ (s ∪ s0) ++ b ++ a | A User Theorem |
| sub-union-05 | ⊦ s ⊆ (s ∪ s0) ++ a ++ b ++ c | A User Theorem |
| subdef | ⊦ s1 ⊆ s2 ↔ (∀ a. a ∈ s1 → a ∈ s2) | A User Theorem |
| subset-del | ⊦ s ⊆ s -- a ↔ ¬ a ∈ s | A User Theorem |
| subsub-del | ⊦ s -- a ⊆ s0 ∧ ¬ s ⊆ s0 ∧ a ∈ s → ¬ a ∈ s0 | A User Theorem |
| una | ⊦ (s ∪ s0) ∪ s1 = s ∪ s0 ∪ s1 | A User Theorem |
| unadd | ⊦ (s ++ a) ∪ s0 = (s ∪ s0) ++ a | A User Theorem |
| unadd-01 | ⊦ s ∪ (s0 ++ a) = (s ∪ s0) ++ a | A User Theorem |
| unall | ⊦ s = s0 ∪ s ↔ (∀ a. a ∈ s0 → a ∈ s) | A User Theorem |
| unc | ⊦ s ∪ s0 = s0 ∪ s | A User Theorem |
| undel | ⊦ a ∈ s → s ∪ (s0 -- a) = s ∪ s0 | A User Theorem |
| undel-01 | ⊦ (s ∪ s0) -- a = s ∪ (s0 -- a) ↔ ¬ a ∈ s | A User Theorem |
| undel-02 | ⊦ (s ∪ s0) -- a = (s -- a) ∪ (s0 -- a) | A User Theorem |
| undel-03 | ⊦ ¬ a ∈ s → s ∪ (s0 -- a) = (s ∪ s0) -- a | A User Theorem |
| undel-04 | ⊦ (s -- a) ∪ (s0 -- a) = (s ∪ s0) -- a | A User Theorem |
| undel-05 | ⊦ ¬ a ∈ s ∧ ¬ a ∈ s0 → (s -- a) ∪ (s0 -- a) = s ∪ s0 | A User Theorem |
| undel-06 | ⊦ (s -- a -- b) ∪ s0 ≠ (s -- b -- a) ∪ s0 ↔ false | A User Theorem |
| une | ⊦ s ∪ ∅ = s | A User Theorem |
| une-01 | ⊦ s1 ∪ s2 = ∅ ↔ s1 = ∅ ∧ s2 = ∅ | A User Theorem |
| uneq | ⊦ s ∪ s0 = s0 ↔ s ⊆ s0 | A User Theorem |
| unidem | ⊦ s ∪ s = s | A User Theorem |
| unin | ⊦ ¬ a ∈ s → (a ∈ s ∪ s0 ↔ a ∈ s0) | A User Theorem |
| unin-01 | ⊦ ¬ a ∈ s ∪ s0 ↔ ¬ a ∈ s ∧ ¬ a ∈ s0 | A User Theorem |
| unindel | ⊦ ¬ a ∈ s ∪ s0 → ¬ a ∈ (s -- b) ∪ s0 | A User Theorem |
| uninsert | ⊦ a ∈ s → (s ∪ s0) ++ a = s ∪ s0 | A User Theorem |
| uninsubdel | ⊦ ¬ a ∈ s ∪ s0 ∧ s1 ⊆ s → ¬ a ∈ (s1 -- b) ∪ s0 | A User Theorem |
| union-del | ⊦ a ∈ (s -- a) ∪ s0 ↔ a ∈ s0 | A User Theorem |
| union-diff | ⊦ ¬ a ∈ s0 ∧ ¬ a ∈ s1 → (a ∈ s \ (s0 ∪ s1) ↔ a ∈ s) | A User Theorem |
| union-difference | ⊦ s ⊆ s0 → s ∪ (s0 \ s) = s0 | A User Theorem |
| union-one | ⊦ a ≠ b → (a ∈ {b} ∪ s ↔ a ∈ s) | A User Theorem |
| union-rewone | ⊦ s ++ a = s ∪ {a} | A User Theorem |
| union-sub | ⊦ s0 ⊆ s → s ∪ s0 = s | A User Theorem |
| union-sub-01 | ⊦ s0 ⊆ s → s0 ∪ s = s | A User Theorem |
| unrax | ⊦ a ∈ s ∪ s0 ↔ ¬ ¬(a ∈ s ∨ a ∈ s0) | A User Theorem |
| unsub | ⊦ s ⊆ s ∪ s0 | A User Theorem |
| unsub-union-01 | ⊦ s1 ∪ s2 ⊆ s ↔ s1 ⊆ s ∧ s2 ⊆ s | A User Theorem |
| unsubdel | ⊦ s ⊆ s0 ∧ s1 ⊆ s2 ∧ ¬ a ∈ s ∧ ¬ a ∈ s1 → s ∪ s1 ⊆ (s0 -- a) ∪ (s2 -- a) | A User Theorem |
| unsubdel-01 | ⊦ s ⊆ s0 ∧ ¬ a ∈ s → (s0 -- a) ∪ s = s0 -- a | A User Theorem |
| unsubins | ⊦ s ++ a ⊆ s ∪ s0 ↔ a ∈ s ∪ s0 | A User Theorem |
| unsubins-01 | ⊦ s ⊆ (s ∪ s0) ++ a | A User Theorem |
| unsubsub | ⊦ s ⊆ s0 ∧ s1 ⊆ s2 → s ∪ s1 ⊆ s0 ∪ s2 | A User Theorem |