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: |
|---|---|---|
| diff-rec | ⊦ bag0 \ (bag1 ++ a) = (bag0 -- a) \ bag1 | An Axiom |
| diff-empty | ⊦ bag0 \ ∅ = bag0 | An Axiom |
| one | ⊦ {a} = ∅ ++ a | An Axiom |
| in | ⊦ a ∈ bag ↔ count(a, bag) ≠ 0 | An Axiom |
| count-subset | ⊦ bag0 ⊆ bag1 ↔ (∀ a. count(a, bag0) ≤ count(a, bag1)) | An Axiom |
| size-rec | ⊦ #(bag ++ a) = # bag + 1 | An Axiom |
| size-empty | ⊦ # ∅ = 0 | An Axiom |
| union-empty | ⊦ ∅ ∪ bag = bag | An Axiom |
| union-rec | ⊦ (bag0 ++ a) ∪ bag1 = (bag0 ∪ bag1) ++ a | An Axiom |
| del-rec | ⊦ (bag ++ a) -- b = (a = b ⊃ bag;(bag -- b) ++ a) | An Axiom |
| del-empty | ⊦ ∅ -- a = ∅ | An Axiom |
| bag-rm-add-eq | ⊦ (bag -- a) ++ a = bag ↔ a ∈ bag | A User Theorem |
| count-del | ⊦ count(a, bag -- b) = count(a, bag) - (a = b ∧ count(a, bag) ≠ 0 ⊃ 1;0) | A User Theorem |
| count-diff-subset | ⊦ bag0 ⊆ bag1 → count(a, bag1 \ bag0) = count(a, bag1) - count(a, bag0) | A User Theorem |
| count-one | ⊦ count(a, {b} ) = (a = b ⊃ 1;0) | A User Theorem |
| del-notin | ⊦ count(a, bag) = 0 → bag -- a = bag | A User Theorem |
| del-size | ⊦ #(bag -- a) = # bag - (a ∈ bag ⊃ 1;0) | A User Theorem |
| diff-add-sw | ⊦ ¬ a ∈ bag1 → (bag0 ++ a) \ bag1 = (bag0 \ bag1) ++ a | A User Theorem |
| diff-empty1 | ⊦ ∅ \ bag = ∅ | A User Theorem |
| diff-size | bag1 ⊆ bag0 ⊦ #(bag0 \ bag1) = # bag0 - # bag1 | A User Theorem |
| difference | ⊦ count(a, bag0 \ bag1) = (count(a, bag1) ≤ count(a, bag0) ⊃ count(a, bag0) - count(a, bag1);0) | A User Theorem |
| differente-notin | ⊦ a ∈ bag0 ∧ ¬ a ∈ bag1 → (¬ a ∈ bag0 \ bag1 ↔ false) | A User Theorem |
| exin | ⊦ a ∈ bag → (∃ bag0. bag = bag0 ++ a) | A User Theorem |
| in-add | ⊦ a ∈ bag ++ b ↔ a ∈ bag ∨ a = b | A User Theorem |
| in-at | ⊦ a ∈ bag ++ a | A User Theorem |
| in-diff-notfirst | ⊦ ¬ a ∈ bag0 → ¬ a ∈ bag0 \ bag1 | A User Theorem |
| in-emp | ⊦ ¬ a ∈ ∅ | A User Theorem |
| in-one | ⊦ a ∈ {b} ↔ a = b | A User Theorem |
| in-rem-notrem | ⊦ a ≠ b → (¬ a ∈ bag -- b ↔ ¬ a ∈ bag) | A User Theorem |
| in-union | ⊦ a ∈ bag0 ∪ bag1 ↔ a ∈ bag0 ∨ a ∈ bag1 | A User Theorem |
| some | ⊦ bag ≠ ∅ ↔ (∃ a. a ∈ bag) | A User Theorem |
| still-in-diff | ⊦ a ∈ bag0 \ bag1 → (¬ a ∈ bag0 ↔ false) | A User Theorem |
| still-in-rem | ⊦ a ∈ bag0 -- b → (¬ a ∈ bag0 ↔ false) | A User Theorem |
| subset-antisym | ⊦ bag0 ⊆ bag1 → (bag1 ⊆ bag0 ↔ bag0 = bag1) | A User Theorem |
| subset-elem | ⊦ bag0 ⊆ bag1 ∧ a ∈ bag0 → (¬ a ∈ bag1 ↔ false) | A User Theorem |
| subset-emp | ⊦ bag ⊆ ∅ ↔ bag = ∅ | A User Theorem |
| subset-empty-size | ⊦ bag ⊆ ∅ → # bag = 0 | A User Theorem |
| subset-exdiff | ⊦ bag0 ⊆ bag1 ↔ (∃ bag. bag0 ∪ bag = bag1) | A User Theorem |
| subset-in | ⊦ bag0 ++ a ⊆ bag1 → (count(a, bag1) = 0 ↔ false) | A User Theorem |
| subset-one | ⊦ ∅ ++ a ⊆ bag ↔ a ∈ bag | A User Theorem |
| subset-plus | ⊦ ¬ ¬ bag0 ++ a ⊆ bag1 ↔ (∃ bag2. bag1 = bag2 ++ a ∧ bag0 ⊆ bag2) | A User Theorem |
| subset-plusminus | ⊦ count(a, bag1) ≠ 0 → (bag0 ⊆ bag1 -- a ↔ bag0 ++ a ⊆ bag1) | A User Theorem |
| subset-plusplus | ⊦ bag0 ++ a ⊆ bag1 ++ a ↔ bag0 ⊆ bag1 | A User Theorem |
| subset-refl | ⊦ bag ⊆ bag | A User Theorem |
| subset-size | ⊦ bag0 ⊆ bag1 → # bag0 ≤ # bag1 | A User Theorem |
| subset-smaller | ⊦ bag0 ++ a ⊆ bag1 → (¬ bag0 ⊆ bag1 ↔ false) | A User Theorem |
| subset-trans | ⊦ bag0 ⊆ bag1 ∧ bag1 ⊆ bag2 → bag0 ⊆ bag2 | A User Theorem |
| union | ⊦ count(a, bag0 ∪ bag1) = count(a, bag0) + count(a, bag1) | A User Theorem |
| union-ass | ⊦ bag0 ∪ bag1 ∪ bag2 = (bag0 ∪ bag1) ∪ bag2 | A User Theorem |
| union-com | ⊦ bag0 ∪ bag1 = bag1 ∪ bag0 | A User Theorem |
| union-diff-cancel | ⊦ (bag0 ∪ bag1) \ bag1 = bag0 | A User Theorem |
| union-diff-distr | bag1 ⊆ bag0 ⊦ (bag0 \ bag1) ∪ bag2 = (bag0 ∪ bag2) \ bag1 | A User Theorem |
| union-inj | ⊦ bag ∪ bag1 = bag ∪ bag2 ↔ bag1 = bag2 | A User Theorem |
| union-size | ⊦ #(bag0 ∪ bag1) = # bag0 + # bag1 | A User Theorem |
| union-subset | ⊦ bag ⊆ bag ∪ bag0 | A User Theorem |
| union-subset-inj | ⊦ bag ∪ bag1 ⊆ bag ∪ bag2 ↔ bag1 ⊆ bag2 | A User Theorem |