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 | ⊦ x ∪ y = rmdup(x + y) | An Axiom |
| diff-e | ⊦ [] \ y = [] | An Axiom |
| diff-y | ⊦ a ∈ y → (a ' + x) \ y = x \ y | An Axiom |
| diff-n | ⊦ ¬ a ∈ y → (a ' + x) \ y = a + (x \ y) | An Axiom |
| filt-e | ⊦ filter([], y) = [] | An Axiom |
| filt-y | ⊦ a ∈ y → filter(a ' + x, y) = a ' + filter(x, y) | An Axiom |
| filt-n | ⊦ ¬ a ∈ y → filter(a ' + x, y) = filter(x, y) | An Axiom |
| subset | ⊦ x ⊆ y ↔ (∀ a. a ∈ x → a ∈ y) | An Axiom |
| Noassoc | ⊦ (a ' ∪ x) ∪ y = a ' ∪ x ∪ y | A User Theorem |
| app | ⊦ (x + y) ∪ z = x ∪ y ∪ z | A User Theorem |
| appsize | ⊦ #((x + y) ∪ z) = #((x ∪ y) ∪ z) | A User Theorem |
| assoc | ⊦ (x ∪ y) ∪ z = x ∪ y ∪ z | A User Theorem |
| assocsize | ⊦ #(x ∪ y ∪ z) = #((x ∪ y) ∪ z) | A User Theorem |
| commsize | ⊦ #(x ∪ y) = #(y ∪ x) | A User Theorem |
| del1 | ⊦ ¬ a ∈ x → filter(x, y -1l a) = filter(x, y) | A User Theorem |
| del1-01 | ⊦ ¬ a ∈ x → filter(rmdup(x), y -1l a) = filter(rmdup(x), y) | A User Theorem |
| diff-app | ⊦ x \ (x + y) = [] | A User Theorem |
| diff-app-01 | ⊦ x \ (y + x) = [] | A User Theorem |
| diff-app-02 | ⊦ x \ (y + x + z) = [] | A User Theorem |
| diff-append | ⊦ (x + y) \ z = (x \ z) + (y \ z) | A User Theorem |
| diff-consbothsame | ⊦ (a ' + x) \ (a ' + x0) = x \ (a ' + x0) | A User Theorem |
| diff-consnotin2 | ⊦ ¬ a ∈ x → x \ (a ' + x0) = x \ x0 | A User Theorem |
| diff-dups | ⊦ dups(x \ y) → dups(x) | A User Theorem |
| diff-empty | ⊦ x \ [] = x | A User Theorem |
| diff-empty-all | ⊦ x \ y = [] ↔ (∀ a. a ∈ x → a ∈ y) | A User Theorem |
| diff-empty-sub | ⊦ x \ y = [] ↔ x ⊆ y | A User Theorem |
| diff-firstofapp | ⊦ (x + y) \ x = y \ x | A User Theorem |
| diff-in | ⊦ a ∈ x \ y ↔ a ∈ x ∧ ¬ a ∈ y | A User Theorem |
| diff-in-one | ⊦ a ∈ x \ a0 ' ↔ a ∈ x ∧ a ≠ a0 | A User Theorem |
| diff-onenonmember | ⊦ ¬ a ∈ x → x \ a ' = x | A User Theorem |
| diff-same | ⊦ x \ x = [] | A User Theorem |
| diff-twice-append | ⊦ (x \ y) \ z = x \ (y + z) | A User Theorem |
| diff-twice-append-rev | ⊦ (x \ y) \ z = x \ (z + y) | A User Theorem |
| diff-twice-union | ⊦ (x \ y) \ z = x \ (y ∪ z) | A User Theorem |
| diff-unchanged | ⊦ x \ y = x ↔ (∀ a. ¬(a ∈ x ∧ a ∈ y)) | A User Theorem |
| diff-union | ⊦ (x ∪ y) \ z = (x \ z) ∪ (y \ z) | A User Theorem |
| diff-wfrec | ⊦ x \ (a + y) = (x -l a) \ y | A User Theorem |
| diffgetn-nodupssize | ⊦ ¬ dups(x) ∧ n < # x → #(x \ x[n] ') = # x - 1 | A User Theorem |
| diffone-nodupsget | ⊦ n + 1 < # x ∧ ¬ dups(x) ∧ a ∈ x → (x \ a ')[n] = (n < pos(a, x) ⊃ x[n];x[n + 1]) | A User Theorem |
| diffone-nodupssize | ⊦ ¬ dups(x) ∧ a ∈ x → #(x \ a ') = # x - 1 | A User Theorem |
| dups-app | ⊦ dups(x + y) ↔ dups(x) ∨ dups(y) ∨ filter(x, y) ≠ [] | A User Theorem |
| empty | ⊦ x ∪ [] = rmdup(x) | A User Theorem |
| empty-01 | ⊦ [] ∪ x = rmdup(x) | A User Theorem |
| emptyunion | ⊦ x ∪ y = [] ↔ x = [] ∧ y = [] | A User Theorem |
| f-rm | ⊦ filter(rmdup(x), y) = rmdup(filter(x, y)) | A User Theorem |
| filt-dups | ⊦ dups(filter(x, y)) → dups(x) | A User Theorem |
| filt-in | ⊦ a ∈ filter(x, y) ↔ a ∈ x ∧ a ∈ y | A User Theorem |
| filter-all | ∀ a. a ∈ x → ¬ a ∈ y ⊦ filter(x, y) = [] | A User Theorem |
| filter-dups | ⊦ filter(x, y) ≠ [] → dups(x + y) | A User Theorem |
| filter-empty | ⊦ filter(x + y, z) = [] ↔ filter(x, z) = [] ∧ filter(y, z) = [] | A User Theorem |
| filter-empty-01 | ⊦ filter(x, []) = [] | A User Theorem |
| filter-empty-app | ⊦ filter(x, y) ≠ [] → filter(x, y + z) ≠ [] | A User Theorem |
| filter-empty-app-01 | ⊦ filter(x, y) ≠ [] → filter(x, z + x0 + y) ≠ [] | A User Theorem |
| filter-empty-app-02 | ⊦ filter(x, y) ≠ [] → filter(x, z + y) ≠ [] | A User Theorem |
| filter-empty-app-03 | ⊦ filter(x, y) = [] ∧ filter(x, z) = [] → (filter(x, y + z) ≠ [] ↔ false) | A User Theorem |
| filter-empty-app-04 | ⊦ filter(x, x0) = [] ∧ filter(x, y) = [] ∧ filter(x, z) = [] → (filter(x, x0 + y + z) ≠ [] ↔ false) | A User Theorem |
| filter-empty-append | ⊦ filter(x, y + z) = [] ↔ filter(x, y) = [] ∧ filter(x, z) = [] | A User Theorem |
| filter-empty-commutative | ⊦ filter(x, y) ≠ [] → filter(y, x) ≠ [] | A User Theorem |
| filter-empty-cons | ⊦ filter(x, a ' + y) = [] ↔ ¬ a ∈ x ∧ filter(x, y) = [] | A User Theorem |
| filter-empty-cons-01 | ⊦ filter(a ' + x, y) = [] ↔ ¬ a ∈ y ∧ filter(x, y) = [] | A User Theorem |
| filter-empty-def | ⊦ filter(x, y) = [] ↔ (∀ a. a ∈ x → ¬ a ∈ y) | A User Theorem |
| filter-empty-in | ⊦ a ∈ x ∧ a ∈ z → filter(x, y + z) ≠ [] | A User Theorem |
| filter-empty-in-01 | ⊦ a ∈ x ∧ a ∈ z → filter(x, x0 + y + z) ≠ [] | A User Theorem |
| filter-empty-one | ⊦ filter(x, a ') = [] ↔ ¬ a ∈ x | A User Theorem |
| filter-empty-subset | ⊦ filter(x, z) = [] ∧ y ⊆ z → filter(x, y) = [] | A User Theorem |
| filter-empty-subset-01 | ⊦ filter(x, z) = [] ∧ y ⊆ x → filter(y, z) = [] | A User Theorem |
| filter-notempty | ⊦ a ∈ x ∧ a ∈ y → filter(x, y) ≠ [] | A User Theorem |
| filter-notin | ⊦ ¬ a ∈ x → filter(x, a ' + y) = filter(x, y) | A User Theorem |
| filter-one | ⊦ filter(a ', y) = [] ↔ ¬ a ∈ y | A User Theorem |
| filter-one-01 | ⊦ a ∈ y → filter(a ', y) = a ' | A User Theorem |
| filter-one-02 | ⊦ ¬ a ∈ y → filter(a ', y) = [] | A User Theorem |
| filter-rest | ⊦ filter(x, y) = [] ∧ x ≠ [] → filter(x.rest, y) = [] | A User Theorem |
| filter-rev-empty | ⊦ filter(rev(x), y) = [] ↔ filter(x, y) = [] | A User Theorem |
| firstin | ⊦ a ∈ x → a ' ∪ x = rmdup(x) | A User Theorem |
| firstinsub | ⊦ a ∈ z → (a ' + x ⊆ y ∪ z ↔ x ⊆ y ∪ z) | A User Theorem |
| firstsub | ⊦ x ⊆ y → x ∪ y = rmdup(y) | A User Theorem |
| in | ⊦ a ∈ x ∪ y ↔ a ∈ x ∨ a ∈ y | A User Theorem |
| in-01 | ⊦ ¬ a ∈ x → (a ∈ x ∪ y ↔ a ∈ y) | A User Theorem |
| in-01-01 | ⊦ a ∈ y → (a ∈ filter(x, y) ↔ a ∈ x) | A User Theorem |
| in-02 | ⊦ a ≠ b → (a ∈ b ' ∪ y ↔ a ∈ y) | A User Theorem |
| in-03 | ⊦ ¬ a ∈ y → (a ∈ x ∪ y ∪ z ↔ a ∈ x ∪ z) | A User Theorem |
| in-04 | ⊦ a ∈ x ∪ y ↔ ¬ ¬(a ∈ x ∨ a ∈ y) | A User Theorem |
| in-05 | ⊦ a ∈ x → (a ∈ filter(x, y) ↔ a ∈ y) | A User Theorem |
| in-06 | ⊦ a ∈ y ∧ a ∈ x → a ∈ filter(rmdup(x), y) | A User Theorem |
| insub | ⊦ a ∈ x ∧ x ∪ y ⊆ z → a ∈ z | A User Theorem |
| insub-01 | ⊦ a ∈ y ∧ x ∪ y ⊆ z → a ∈ z | A User Theorem |
| k-union-rec-n | ⊦ ¬(a ∈ x ∨ a ∈ y) → (a + x) ∪ y = a + (x ∪ y) | A User Theorem |
| k-union-rec-y | ⊦ a ∈ x ∨ a ∈ y → (a + x) ∪ y = x ∪ y | A User Theorem |
| le | ⊦ # filter(rmdup(x), y) ≤ # y | A User Theorem |
| nodups | ⊦ ¬ dups(x ∪ z) | A User Theorem |
| notin | ⊦ ¬ a ∈ x → a ' ∪ x = a ' + rmdup(x) | A User Theorem |
| notin-01 | ⊦ a ∈ y → ¬ a ∈ x \ y | A User Theorem |
| notin-02 | ⊦ ¬ a ∈ y → ¬ a ∈ filter(x, y) | A User Theorem |
| onein-diff | ⊦ a ∈ x → a ' \ x = [] | A User Theorem |
| onenotin-diff | ⊦ ¬ a ∈ x → a ' \ x = a ' | A User Theorem |
| rax-01 | ⊦ ¬ a ∈ y → (a ' + x) \ y = a ' + (x \ y) | A User Theorem |
| rmdup | ⊦ rmdup(x) ⊆ y ↔ x ⊆ y | A User Theorem |
| rmdup-01 | ⊦ x ⊆ rmdup(y) ↔ x ⊆ y | A User Theorem |
| rmdup-02 | ⊦ rmdup(x ∪ y) = x ∪ y | A User Theorem |
| rmdup-size | ⊦ # rmdup(x ∪ y) = #(x ∪ y) | A User Theorem |
| rotsize | ⊦ #(x ∪ y ∪ z) = #(y ∪ x ∪ z) | A User Theorem |
| size | ⊦ ¬ dups(x) ∧ ¬ dups(y) ∧ x ⊆ y ∧ y ⊆ x → (# x = # y ↔ true) | A User Theorem |
| size-le | ⊦ #(x ∪ y) ≤ # rmdup(y) ↔ x ⊆ y | A User Theorem |
| size-nle | ⊦ ¬ y ⊆ x ∪ z → ¬ #(x ∪ y ∪ z) ≤ #(x ∪ z) | A User Theorem |
| size-nls | ⊦ ¬ #((x ∪ y) ∪ z) < #(x ∪ y) | A User Theorem |
| size-nls-01 | ⊦ ¬ #(x ∪ y ∪ z) < #(y ∪ x ∪ z) | A User Theorem |
| sub | ⊦ x ∪ y ⊆ z ∪ y ↔ x ⊆ z ∪ y | A User Theorem |
| sub-01 | ⊦ x ∪ y ⊆ x ∪ z ↔ y ⊆ x ∪ z | A User Theorem |
| sub-02 | ⊦ x ⊆ y ∪ z ∪ x | A User Theorem |
| sub-03 | ⊦ x ⊆ y ∪ x ∪ z | A User Theorem |
| sub-04 | ⊦ x ∪ x0 ⊆ y ∪ x ∪ z ↔ x0 ⊆ y ∪ x ∪ z | A User Theorem |
| sub-05 | ⊦ x ∪ x0 ⊆ y ∪ z ∪ x ↔ x0 ⊆ y ∪ z ∪ x | A User Theorem |
| sub-06 | ⊦ x ∪ y ⊆ y ↔ x ⊆ y | A User Theorem |
| sub-07 | ⊦ x ∪ y ⊆ x ↔ y ⊆ x | A User Theorem |
| sub-in | ⊦ x ⊆ y ∧ a ∈ x → a ∈ y | A User Theorem |
| sub-notin | ⊦ x ⊆ y ∧ ¬ a ∈ y → ¬ a ∈ x | A User Theorem |
| sub-size | ⊦ x ⊆ y ∧ ¬ dups(x) → # x ≤ # y | A User Theorem |
| sub-size-01 | ⊦ x ⊆ y ∧ ¬ dups(x) → (# y < # x ↔ false) | A User Theorem |
| sub-size-02 | ⊦ ¬ x ⊆ y → ¬ #(x ∪ y) ≤ # rmdup(y) | A User Theorem |
| suband | ⊦ x ∪ y ⊆ z ↔ x ⊆ z ∧ y ⊆ z | A User Theorem |
| subonein | ⊦ a ' ∪ x ⊆ y → a ∈ y | A User Theorem |
| subset-01 | ⊦ x ⊆ x ∪ y | A User Theorem |
| subset-01-01 | ⊦ y ⊆ x ∪ y | A User Theorem |
| subset-app | ⊦ x ⊆ x + y | A User Theorem |
| subset-app-01 | ⊦ x ⊆ y + x | A User Theorem |
| subset-app-02 | ⊦ x ⊆ y + x + z | A User Theorem |
| subset-app-03 | ⊦ x + y ⊆ x + z ↔ y ⊆ x + z | A User Theorem |
| subset-app-04 | ⊦ x + y ⊆ z + y ↔ x ⊆ z + y | A User Theorem |
| subset-append | ⊦ ¬ x ⊆ y + z → ¬ x ⊆ y | A User Theorem |
| subset-append-01 | ⊦ ¬ x ⊆ y + z → ¬ x ⊆ z | A User Theorem |
| subset-append-02 | ⊦ x + y ⊆ z ↔ x ⊆ z ∧ y ⊆ z | A User Theorem |
| subset-del | ⊦ x ⊆ y → (¬ x ⊆ y -l a ↔ a ∈ x) | A User Theorem |
| subset-diff-union | ⊦ x \ y ⊆ z ↔ x ⊆ z ∪ y | A User Theorem |
| subset-empty | ⊦ [] ⊆ x | A User Theorem |
| subset-empty-01 | ⊦ x ⊆ [] ↔ x = [] | A User Theorem |
| subset-insert | ⊦ x ⊆ x ++ a | A User Theorem |
| subset-one | ⊦ a ' ⊆ x ↔ a ∈ x | A User Theorem |
| subset-perm | ⊦ x + y ⊆ y + x | A User Theorem |
| subset-rec | ⊦ a ' + x ⊆ y ↔ a ∈ y ∧ x ⊆ y | A User Theorem |
| subset-ref | ⊦ x ⊆ x | A User Theorem |
| subset-rmdup | ⊦ x ⊆ y → rmdup(x + y) = rmdup(y) | A User Theorem |
| subset-trans | ⊦ x ⊆ y ∧ y ⊆ z → x ⊆ z | A User Theorem |
| subsub | ⊦ x ⊆ y → x ⊆ y ∪ z | A User Theorem |
| subsub-01 | ⊦ x ⊆ z → x ⊆ y ∪ z | A User Theorem |
| union-twice | ⊦ x ∪ x = rmdup(x) | A User Theorem |