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 | ⊦ bag0 = bag1 ↔ (∀ a. count(a, bag0) = count(a, bag1)) | An Axiom |
| count-empty | ⊦ count(a, ∅) = 0 | An Axiom |
| count-insert | ⊦ count(a, bag ++ b) = (a = b ⊃ 1;0) + count(a, bag) | An Axiom |
| gen | bag generated by ∅, ++; | An Axiom |
| bag-add2-eq-elim | ⊦ bag0 ++ a ++ b ≠ bag1 ++ a ↔ bag0 ++ b ≠ bag1 | A User Theorem |
| count-1 | ⊦ count(a, ∅ ++ a) = 1 | A User Theorem |
| count-other | ⊦ a ≠ b → count(a, bag ++ b) = count(a, bag) | A User Theorem |
| count-same | ⊦ count(a, bag ++ a) = count(a, bag) + 1 | A User Theorem |
| ext-rec | ⊦ bag1 = bag0 ++ a ↔ (∀ b. count(b, bag1) = (a = b ⊃ 1;0) + count(b, bag0)) | A User Theorem |
| insert-inj | ⊦ bag0 ++ a = bag1 ++ a ↔ bag0 = bag1 | A User Theorem |
| insert-nonempty | ⊦ bag ++ a ≠ ∅ | A User Theorem |