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 |
| add-inter-rem | ⊦ ((s0 ++ a) ∩ s1) -- a = (s0 ∩ s1) -- a | 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-ne | ⊦ 1 < # s → s -- a ≠ ∅ | 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-size | ⊦ a ∈ s → #(s -- a) = # s - 1 | A User Theorem |
| del-size-01 | ⊦ a ∈ s → (# s = n + 1 ↔ #(s -- a) = n) | A User Theorem |
| del-size-02 | ⊦ a ∈ s ∧ a ≠ b → #(s -- b -- a) = #(s -- b) - 1 | A User Theorem |
| del-three | ⊦ 2 < # s → #(s -- a -- b) ≠ 0 | A User Theorem |
| del-three-01 | ⊦ 2 < # s ∧ b ∈ s ∧ a ≠ b → #(s -- a -- b) = #(s -- a) - 1 | 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-shift | ⊦ a ∈ s → (s -- a = s0 ↔ s = s0 ++ a ∧ ¬ a ∈ s0) | 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-del-minus | ⊦ (s -- a) \ (s1 -- a) = (s -- a) \ s1 | A User Theorem |
| diff-del-minus-2 | ⊦ ¬ a ∈ s1 → (s -- a) \ s1 = (s \ s1) -- a | A User Theorem |
| diff-del-minus-3 | ⊦ a ∈ s1 → (s -- a) \ s1 = s \ s1 | A User Theorem |
| diff-del-plus-1 | ⊦ a ∈ s1 → (s ++ a) \ s1 = s \ s1 | A User Theorem |
| diff-del-plus-2 | ⊦ ¬ a ∈ s1 → (s ++ a) \ s1 = (s \ s1) ++ a | A User Theorem |
| diff-diff-right | ⊦ a ∈ s2 → (a ∈ s0 \ s1 \ s2 ↔ a ∈ s0) | 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-sub-size | s = s0 \ s1, s1 ⊆ s0 ⊦ # s = # s0 - # s1 | 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-supset-empty | ⊦ s \ (s ∪ s0) = ∅ | 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 |
| empty-intersection-diff | ⊦ s ∩ s0 = ∅ → s \ s0 = s | A User Theorem |
| equal-add-in | ⊦ s ++ a = s0 ++ b ∧ s0 ++ b = (s1 -- c) ++ a0 ∧ b ≠ a0 → b ∈ s1 -- c | 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 | ⊦ 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-empty-one | ⊦ (∅ ++ a) ∩ s = ∅ ↔ ¬ a ∈ s | 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 |
| intersect-add-rem | ⊦ (s0 ++ a) ∩ (s1 -- a) = (s0 ∩ s1) -- a | A User Theorem |
| intersect-empty-rem | ⊦ s0 ∩ s1 = ∅ → (s0 -- a) ∩ s1 = ∅ | A User Theorem |
| intersection-insert | ⊦ ¬ a ∈ s → s ∩ (s0 ++ a) = s ∩ s0 | A User Theorem |
| intersection-shift | ⊦ a ∈ s → s ∩ (s0 ++ a) = (s ∩ s0) ++ a | A User Theorem |
| intersection-size | ⊦ ¬ # s0 + # s < #(s0 ∩ s) | 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 |
| k-delete-rec | ⊦ ¬ b ∈ s ∧ a ≠ b → (s ++ b) -- a = (s -- a) ++ b | A User Theorem |
| k-diff-rec1 | ⊦ ¬ a ∈ s ∧ a ∈ s0 → s \ s0 = s \ (s0 -- a) | A User Theorem |
| k-diff-rec2 | ⊦ a ∈ s ∧ a ∈ s0 → s \ s0 = (s -- a) \ (s0 -- a) | A User Theorem |
| k-intersect-base | ⊦ ∅ ∩ s = ∅ | A User Theorem |
| k-intersect-rec1 | ⊦ a ∈ s ∧ a ∈ s0 → s ∩ s0 = ((s -- a) ∩ (s0 -- a)) ++ a | A User Theorem |
| k-intersect-rec2 | ⊦ ¬ a ∈ s ∨ ¬ a ∈ s0 → s ∩ s0 = (s -- a) ∩ (s0 -- a) | A User Theorem |
| k-union-base | ⊦ ∅ ∪ s = s | A User Theorem |
| k-union-rec1 | ⊦ ¬ a ∈ s ∧ a ∈ s0 → (s ++ a) ∪ s0 = s ∪ s0 | A User Theorem |
| k-union-rec2 | ⊦ ¬ a ∈ s ∧ ¬ a ∈ s0 → (s ++ a) ∪ s0 = (s ∪ s0) ++ a | A User Theorem |
| one-in | ⊦ a ∈ {b} ↔ a = b | A User Theorem |
| one-min | ⊦ s = ∅ ++ a → s -- a = ∅ | A User Theorem |
| rem-inter-empty3 | ⊦ (s0 \ s1) ∩ s = ∅ ∧ (s2 \ s0) ∩ s = ∅ → (s2 \ s1) ∩ s = ∅ | A User Theorem |
| rem-union-ins | ⊦ (s0 ∪ (s1 -- a)) ++ a = (s0 ∪ s1) ++ a | A User Theorem |
| selsub-diff | s1 ⊆ s2 ⊦ s1 = s2, ∃ s. s ⊆ s2 ∧ s1 = s2 \ s | A User Theorem |
| size-del-leq | ⊦ # s ≤ #(s -- a) ↔ ¬ a ∈ s | A User Theorem |
| size-eq | ⊦ s0 = s1 → (# s0 ≠ # s1 ↔ false) | A User Theorem |
| size-eq-ext | ∀ a. a ∈ s0 ↔ a ∈ s1 ⊦ # s0 ≠ # s1 ↔ false | A User Theorem |
| size-union | ⊦ s ∩ s0 = ∅ → #(s ∪ s0) = # s + # s0 | 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 |
| subset-is-union | ⊦ s ⊆ s0 ↔ (∃ s1. s ∪ s1 = s0 ∧ s ∩ s1 = ∅) | A User Theorem |
| subseteq-inter-empty-empty | ⊦ s0 ⊆ s1 ∧ s1 ∩ s2 = ∅ → s0 ∩ s2 = ∅ | A User Theorem |
| subseteq-rem-del | ⊦ a ∈ s0 ∧ s0 ⊆ s1 → s1 \ (s0 -- a) = (s1 \ s0) ++ a | 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-diff-union-same | ⊦ (s0 ∪ s1) \ (s2 ∪ s1) = s0 \ (s2 ∪ s1) | A User Theorem |
| union-difference | ⊦ s ⊆ s0 → s ∪ (s0 \ s) = s0 | A User Theorem |
| union-inter-inter-union | ⊦ (s0 ∪ s1) ∩ s2 = (s0 ∩ s2) ∪ (s1 ∩ s2) | A User Theorem |
| union-one | ⊦ a ≠ b → (a ∈ {b} ∪ s ↔ a ∈ s) | A User Theorem |
| union-rem-add | ⊦ a ∈ s0 → ((s0 -- a) ∪ s1) ++ a = s0 ∪ s1 | A User Theorem |
| union-rem-unchdg | ⊦ (s0 -- a) ∪ s1 = s0 ∪ s1 ↔ a ∈ s1 ∨ ¬ a ∈ s0 | A User Theorem |
| union-rem-union | ⊦ s0 ⊆ s2 → s0 \ s1 ⊆ s2 | A User Theorem |
| union-rewone | ⊦ s ++ a = s ∪ {a} | A User Theorem |
| union-size | ⊦ ¬ #(s ∪ s0) < # s | A User Theorem |
| union-size-01 | ⊦ ¬ a ∈ s → ¬ #((s ∪ s0) ++ a) ≤ # s | A User Theorem |
| union-size-02 | ⊦ ¬ a ∈ s ∧ a ∈ s0 → #(s ∪ s0) = #(s ∪ (s0 -- a)) + 1 | A User Theorem |
| union-size-03 | ⊦ #(s0 ∪ s1) = # s0 + # s1 - #(s0 ∩ s1) | A User Theorem |
| union-size-insert | ⊦ ¬ a ∈ s ∧ ¬ a ∈ s0 → #((s ∪ s0) ++ a) = #(s ∪ s0) + 1 | A User Theorem |
| union-size-le | ⊦ #(s0 ∪ s1) ≤ # s0 + # s1 | A User Theorem |
| union-size-ls-in | ⊦ a ∈ s0 ∧ a ∈ s1 → #(s0 ∪ s1) < # s0 + # s1 | A User Theorem |
| union-size-not-less | ⊦ ¬ # s0 + # s1 < #(s0 ∪ s1) | A User Theorem |
| union-size-not-less-01 | ⊦ # s0 ≤ m ∧ # s1 ≤ n → ¬ m + n < #(s0 ∪ s1) | A User Theorem |
| union-size-not-less-02 | ⊦ # s0 ≤ m ∧ # s1 ≤ n → ¬ m + n + 1 < #(s0 ∪ s1) | A User Theorem |
| union-sizeeq | ⊦ #(s ∪ s0) = # s ↔ s0 ⊆ s | A User Theorem |
| union-sizele | ⊦ #(s ∪ s0) ≤ # s ↔ s0 ⊆ s | A User Theorem |
| union-sizele-01 | ⊦ #((s ∪ s0) ++ a) ≤ # s ↔ s0 ⊆ s ∧ a ∈ s | A User Theorem |
| union-sub | ⊦ s0 ⊆ s → s ∪ s0 = s | A User Theorem |
| union-sub-01 | ⊦ s0 ⊆ s → s0 ∪ s = s | A User Theorem |
| union-subset | ⊦ s ⊆ s0 → s ∪ s1 ⊆ s0 ∪ s1 | A User Theorem |
| union-subset-01 | ⊦ ¬ s ∪ s1 ⊆ s0 ∪ s1 → ¬ s ⊆ s0 | A User Theorem |
| union-subset-02 | ⊦ s ⊆ s0 ∧ s1 ⊆ s2 → s ∪ s1 ⊆ (s0 ∪ s2) ++ a | A User Theorem |
| union-subset-03 | ⊦ s ⊆ s0 ∧ s1 ⊆ s2 ∧ s3 ⊆ s4 → s ∪ s1 ∪ s3 ⊆ s0 ∪ s2 ∪ s4 | A User Theorem |
| union-subset-04 | ⊦ s ⊆ s0 ∧ s1 ⊆ s2 ∧ s3 ⊆ s4 → s ∪ s1 ∪ s3 ⊆ (s0 ∪ s2 ∪ s4) ++ a | A User Theorem |
| union-subset-05 | ⊦ s ⊆ s0 → s ∪ s1 ⊆ (s0 ∪ s1) ++ a | A User Theorem |
| union-subseteq-union-same | ⊦ s0 ∪ s1 ⊆ s2 ∪ s1 ↔ s0 ⊆ s2 ∪ s1 | 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 |