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: |
|---|---|---|
| list2set-empty | ⊦ list2set([]) = ∅ | An Axiom |
| list2set-rec | ⊦ list2set(a ' + x) = list2set(x) ++ a | An Axiom |
| set2list-empty | ⊦ set2list(∅) = [] | An Axiom |
| set2list-rec | ⊦ s ≠ ∅ → set2list(s) = s.min + set2list(s.butmin) | An Axiom |
| dups | ⊦ ¬ dups(set2list(s)) | A User Theorem |
| dups-01 | ⊦ ¬ dups(x + set2list(s ∪ s0)) → ¬ dups(x + set2list(s)) ∧ ¬ dups(x + set2list(s0)) | A User Theorem |
| dups-02 | ⊦ ¬ dups(x + y) → list2set(x) ∩ list2set(y) = ∅ | A User Theorem |
| dups-03 | ⊦ ¬ dups(x) ∧ ¬ dups(y) → (dups(x + y) ↔ list2set(x) ∩ list2set(y) ≠ ∅) | A User Theorem |
| dups-04 | ⊦ ¬ dups(x) → (dups(set2list(s) + x) ↔ s ∩ list2set(x) ≠ ∅) | A User Theorem |
| dups-05 | ⊦ ¬ dups(x) → (dups(x + set2list(s)) ↔ s ∩ list2set(x) ≠ ∅) | A User Theorem |
| empty | ⊦ set2list(s) = [] ↔ s = ∅ | A User Theorem |
| firstN | ⊦ list2set(x) ∩ s = ∅ ∧ n < # x → list2set(firstn(n, x)) ∩ s = ∅ | A User Theorem |
| firstN-01 | ⊦ n < # x ∧ list2set(x) ∩ s = ∅ ∧ list2set(x) ∩ s0 = ∅ → list2set(firstn(n, x)) ∩ (s ∪ s0) = ∅ | A User Theorem |
| in | ⊦ a ∈ list2set(x) ↔ a ∈ x | A User Theorem |
| in-01 | ⊦ a ∈ set2list(s) ↔ a ∈ s | A User Theorem |
| in-union | ⊦ ¬ a ∈ x → (a ∈ list2set(x) ∪ s ↔ a ∈ s) | A User Theorem |
| intempty | ⊦ a ∈ x ∧ a ∈ y → list2set(x) ∩ list2set(y) ≠ ∅ | A User Theorem |
| intempty-01 | ⊦ list2set(x) ∩ s = ∅ ∧ a ∈ x → ¬ a ∈ s | A User Theorem |
| intempty-02 | ⊦ list2set(x) ∩ s = ∅ ∧ a ∈ s → ¬ a ∈ x | A User Theorem |
| len | ⊦ # set2list(s) = # s | A User Theorem |
| list2set-append | ⊦ list2set(x + y) = list2set(x) ∪ list2set(y) | A User Theorem |
| list2set-empty-01 | ⊦ list2set(x) = ∅ ↔ x = [] | A User Theorem |
| list2set-one | ⊦ list2set(a ') = ∅ ++ a | A User Theorem |
| set2list-one | ⊦ set2list(∅ ++ a) = a ' | A User Theorem |
| set2set | ⊦ list2set(set2list(s)) = s | A User Theorem |
| subset | ⊦ list2set(x) ⊆ s ∧ a ∈ x → a ∈ s | A User Theorem |