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: |
|---|---|---|
| dups | ⊦ dups(x) ↔ (∃ a, x0, y, z. x = x0 + (a + (y + (a + z)))) | An Axiom |
| rmdup-e | ⊦ rmdup([]) = [] | An Axiom |
| rmdup-y | ⊦ a ∈ x → rmdup(a ' + x) = rmdup(x) | An Axiom |
| rmdup-n | ⊦ ¬ a ∈ x → rmdup(a ' + x) = a + rmdup(x) | An Axiom |
| disjoint | ⊦ disj(x, y) ↔ (∀ a. ¬(a ∈ x ∧ a ∈ y)) | An Axiom |
| adjoin-notin | ⊦ ¬ a ∈ x → x ++ a = a + x | An Axiom |
| adjoin-in | ⊦ a ∈ x → x ++ a = x | An Axiom |
| a | ⊦ ¬ dups(x + y) → ¬ dups(x) ∧ ¬ dups(y) | A User Theorem |
| a-01 | ⊦ dups(x + a ' + a ' + y) | A User Theorem |
| aa | ⊦ disj(x + y, x0 + y0) ↔ disj(x, x0) ∧ disj(x, y0) ∧ disj(y, x0) ∧ disj(y, y0) | A User Theorem |
| app | ⊦ disj(x, y + z) → disj(x, y) | A User Theorem |
| app-01 | ⊦ disj(x, y + z) → disj(x, z) | A User Theorem |
| app-01-02 | ⊦ dups(y) → dups(x + y) | A User Theorem |
| app-02 | ⊦ disj(x, y + z) ↔ disj(x, y) ∧ disj(x, z) | A User Theorem |
| app-03 | ⊦ disj(y + z, x) ↔ disj(x, y) ∧ disj(x, z) | A User Theorem |
| app-05 | ⊦ dups(x) → dups(x + y) | A User Theorem |
| c | ⊦ ¬ dups(a ') | A User Theorem |
| c-01 | ⊦ a ∈ x → dups(a ' + x) | A User Theorem |
| c-02 | ⊦ ¬ a ∈ x → (dups(a ' + x) ↔ dups(x)) | A User Theorem |
| c-03 | ⊦ ¬ dups(x) → (dups(a ' + x) ↔ a ∈ x) | A User Theorem |
| cons | ⊦ disj(x, y) → (disj(x, a ' + y) ↔ ¬ a ∈ x) | A User Theorem |
| cons-01 | ⊦ disj(x, y) → (disj(a ' + x, y) ↔ ¬ a ∈ y) | A User Theorem |
| cons-02 | ⊦ disj(x, y) → (disj(y, a ' + x) ↔ ¬ a ∈ y) | A User Theorem |
| cons-03 | ⊦ disj(x, y) → (disj(x + a ', y) ↔ ¬ a ∈ y) | A User Theorem |
| cons-04 | ⊦ disj(x, y) → (disj(y, x + a ') ↔ ¬ a ∈ y) | A User Theorem |
| d | ⊦ ¬ a ∈ x ∧ ¬ a ∈ y → (dups(x + a ' + y) ↔ dups(x + y)) | A User Theorem |
| dis-empty | ⊦ disj([], x) | A User Theorem |
| dups-01 | ⊦ dups(x ++ a) ↔ dups(x) | A User Theorem |
| dups-appex | ⊦ dups(x + y) ↔ dups(x) ∨ dups(y) ∨ (∃ a. a ∈ x ∧ a ∈ y) | A User Theorem |
| dups-cons | ⊦ dups(a ' + x) ↔ dups(x) ∨ a ∈ x | A User Theorem |
| dups-eqsize | ¬ dups(x), ¬ dups(y), ∀ a. a ∈ x ↔ a ∈ y ⊦ # x = # y | A User Theorem |
| dups-eqsize-01 | # x = # y, ¬ dups(x), ¬ dups(y), ∀ a. a ∈ x → a ∈ y ⊦ ∀ a. a ∈ y → a ∈ x | A User Theorem |
| dups-eqsize-02 | # x = # y, ¬ dups(x), ∀ a. a ∈ x → a ∈ y ⊦ ¬ dups(y) ∧ (∀ a. a ∈ y → a ∈ x) | A User Theorem |
| dups-eqsize-ext | ¬ dups(x), ¬ dups(y), ∀ a. a ∈ x ↔ a ∈ y ⊦ # x ≠ # y ↔ false | A User Theorem |
| dups-firstoc-rew | ⊦ dups(x) ↔ (∃ y, a, z. x = y + a ' + z ∧ a ∈ y ∧ ¬ dups(y)) | A User Theorem |
| dups-in | ⊦ ¬ dups(x) ∧ x ≠ [] → ¬ x.first ∈ x.rest | A User Theorem |
| dups-lesize | ¬ dups(x), ¬ dups(y), ∀ a. a ∈ x → a ∈ y ⊦ # x ≤ # y | A User Theorem |
| dups-rest | ⊦ ¬ dups(x) ∧ x ≠ [] → ¬ dups(x.rest) | A User Theorem |
| dups-rmdup-size-equiv | ⊦ dups(x) ↔ # x ≠ # rmdup(x) | A User Theorem |
| dups-sw | ⊦ dups(x + y) → dups(y + x) | A User Theorem |
| dups-switch | ⊦ dups(x + y) ↔ dups(y + x) | A User Theorem |
| e | ⊦ disj(x, []) | A User Theorem |
| e-01 | ⊦ ¬ dups([]) | A User Theorem |
| empty-01 | ⊦ [] ++ a = a ' | A User Theorem |
| eq | ⊦ x + a ' + b ' + y + c ' + z = x0 + c ' + a ' + z0 ∧ ¬ a ∈ y ∧ a ≠ b → dups(x + a ' + c ' + z) | A User Theorem |
| eq-01 | ⊦ x + a ' + b ' + y + c ' + z = x0 + a ' + c ' + z0 ∧ ¬ a ∈ y ∧ a ≠ b ∧ b ≠ c → dups(x + a ' + c ' + z) | A User Theorem |
| f | ⊦ dups(x + a ') ↔ a ∈ x ∨ dups(x) | A User Theorem |
| f-01 | ⊦ dups(x + a ' + y) ↔ a ∈ x ∨ a ∈ y ∨ dups(x + y) | A User Theorem |
| fin | ⊦ ¬ dups(a ' + x) → ¬ a ∈ x | A User Theorem |
| first | ⊦ ¬ a ∈ x → (disj(x, a ' + y) ↔ disj(x, y)) | A User Theorem |
| first-01 | ⊦ ¬ a ∈ x → (disj(a ' + y, x) ↔ disj(y, x)) | A User Theorem |
| firstoc | a ∈ x, a ∈ x0 ⊦ ∃ b, y, y0. b ∈ x ∧ x0 = y + b ' + y0 ∧ disj(x, y) | A User Theorem |
| in | ⊦ disj(x, y) ∧ a ∈ x → ¬ a ∈ y | A User Theorem |
| in-01-02 | ⊦ a ∈ y → dups(x + a ' + y) | A User Theorem |
| in-02-01 | ⊦ a ∈ x → dups(x + b ' + a ' + y) | A User Theorem |
| in-03-01 | ⊦ b ∈ y → dups(x + b ' + a ' + y) | A User Theorem |
| in-04-01 | ⊦ a ∈ x → dups(x + a ' + y) | A User Theorem |
| in-05-01 | ⊦ dups(x + a ' + y + a ' + z) | A User Theorem |
| in-06 | ⊦ a ∈ x ∧ a ∈ y → dups(x + y) | A User Theorem |
| in-06-01 | ⊦ ¬ dups(x + a ') → (dups(x + a ' + b ') ↔ ¬ ¬(a = b ∨ b ∈ x)) | A User Theorem |
| in-07 | ⊦ ¬ dups(x + a ' + b ') → (dups(x + a ' + b ' + c ') ↔ ¬ ¬(a = c ∨ b = c ∨ c ∈ x)) | A User Theorem |
| in-08 | ⊦ a ∈ x ++ b ↔ a = b ∨ a ∈ x | A User Theorem |
| in-09 | ⊦ x + a ' = y + b ' + z ∧ b ∈ z → dups(x + a ') | A User Theorem |
| inapp | ⊦ a ' + x + b ' = y + c ' + c ' + z ∧ a ≠ b ∧ ¬ a ∈ x ∧ ¬ b ∈ x → dups(x) | A User Theorem |
| inapp-01 | ⊦ a ' + x + b ' = y + c ' + a0 ' + z ∧ a ≠ b ∧ ¬ a ∈ x ∧ ¬ b ∈ x ∧ c ∈ z → dups(x) | A User Theorem |
| k-dups | ⊦ dups(x) ↔ # x > 1 ∧ (x.first ∈ x.rest ∨ dups(x.rest)) | A User Theorem |
| l | ⊦ a ∈ x → dups(x + a ') | A User Theorem |
| l-01 | ⊦ a ≠ b ∧ ¬ b ∈ x → (dups(x + a ' + b ') ↔ dups(x + a ')) | A User Theorem |
| l-02 | ⊦ dups(x) → dups(x + b ') | A User Theorem |
| l-03 | ⊦ ¬ b ∈ x → (dups(x + b ') ↔ dups(x)) | A User Theorem |
| last | ⊦ ¬ b ∈ x → (disj(x, y + b ') ↔ disj(x, y)) | A User Theorem |
| last-01 | ⊦ ¬ b ∈ x → (disj(y + b ', x) ↔ disj(x, y)) | A User Theorem |
| lastoc | a ∈ x, a ∈ x0 ⊦ ∃ b, y, y0. b ∈ x ∧ x0 = y + b ' + y0 ∧ disj(x, y0) | A User Theorem |
| n | ⊦ a ≠ c ∧ a ≠ b ∧ ¬ a ∈ x → (dups(x + b ' + c ' + a ') ↔ dups(x + b ' + c ')) | A User Theorem |
| one | ⊦ disj(a ', x) ↔ ¬ a ∈ x | A User Theorem |
| one-01 | ⊦ disj(x, a ') ↔ ¬ a ∈ x | A User Theorem |
| one-03 | ⊦ ¬ dups(a + []) | A User Theorem |
| rec | ⊦ dups(a ' + x) ↔ ¬ ¬(a ∈ x ∨ dups(x)) | A User Theorem |
| rm-allsize | ∀ a. a ∈ x ↔ a ∈ y ⊦ # rmdup(x) = # rmdup(y) | A User Theorem |
| rm-empty | ⊦ rmdup(x) = [] ↔ x = [] | A User Theorem |
| rm-eq | ⊦ ¬ dups(x) → rmdup(x) = x | A User Theorem |
| rm-ifrec | ⊦ rmdup(a ' + x) = (a ∈ x ⊃ rmdup(x);a ' + rmdup(x)) | A User Theorem |
| rm-in | ⊦ a ∈ rmdup(x + y) ↔ a ∈ x ∨ a ∈ y | A User Theorem |
| rm-in-01 | ⊦ a ∈ rmdup(x) → a ∈ x | A User Theorem |
| rm-in-02 | ⊦ a ∈ rmdup(x) ↔ a ∈ x | A User Theorem |
| rm-in-03 | ⊦ ¬ a ∈ rmdup(x) → ¬ a ∈ x | A User Theorem |
| rm-in-04 | ⊦ a ∈ y → rmdup(a ' + x + y) = rmdup(x + y) | A User Theorem |
| rm-in-05 | ⊦ a ∈ x → rmdup(a ' + x + y) = rmdup(x + y) | A User Theorem |
| rm-nodups | ⊦ ¬ dups(rmdup(x)) | A User Theorem |
| rm-notin | ⊦ ¬ a ∈ x → ¬ a ∈ rmdup(x) | A User Theorem |
| rm-notin-01 | ⊦ rmdup(x) = y + a ' + z → a ∈ x ∧ ¬ a ∈ y ∧ ¬ a ∈ z | A User Theorem |
| rm-one | ⊦ rmdup(a ') = a ' | A User Theorem |
| rm-rm | ⊦ rmdup(rmdup(x)) = rmdup(x) | A User Theorem |
| rm-rm-01 | ⊦ rmdup(rmdup(x) + y) = rmdup(x + y) | A User Theorem |
| rm-rm-02 | ⊦ rmdup(x + rmdup(y)) = rmdup(x + y) | A User Theorem |
| rm-size | ⊦ ¬ a ∈ x ∧ ¬ a ∈ y → # rmdup(x + a ' + y) = # rmdup(x + y) + 1 | A User Theorem |
| rm-size-01 | ⊦ a ∈ x → # rmdup(x + a ' + y) = # rmdup(x + y) | A User Theorem |
| rm-size-02 | ⊦ a ∈ y → # rmdup(x + a ' + y) = # rmdup(x + y) | A User Theorem |
| rm-size-03 | ⊦ # rmdup(x + y) ≤ # rmdup(y) → # rmdup(x + y) = # rmdup(y) | A User Theorem |
| rm-size-04 | ⊦ # rmdup(x + y + z) ≤ # rmdup(x + z) → # rmdup(x + y + z) = # rmdup(x + z) | A User Theorem |
| rm-size-05 | ⊦ ¬ # x < # rmdup(x) | A User Theorem |
| rm-size-in | ⊦ # rmdup(x + y) = # rmdup(y) ∧ a ∈ x → a ∈ y | A User Theorem |
| rm-size-in-01 | ⊦ # rmdup(x + y + z) = # rmdup(x + z) ∧ a ∈ y → a ∈ x ∨ a ∈ z | A User Theorem |
| rm-size-le | ⊦ # rmdup(x) ≤ # x | A User Theorem |
| rm-size-not | ⊦ # rmdup(x) ≠ # x + 1 | A User Theorem |
| rmdup-last | ⊦ ¬ a ∈ x → rmdup(x + a ') = rmdup(x) + a ' | A User Theorem |
| sym | ⊦ disj(x, y) → disj(y, x) | A User Theorem |
| two | ⊦ dups(a + b + []) ↔ a = b | A User Theorem |
| two-01 | ⊦ dups(a ' + b ') ↔ a = b | A User Theorem |
| two-02 | ⊦ a ≠ b ∧ ¬ dups(x) ∧ ¬ a ∈ x → (dups(a ' + b ' + x) ↔ b ∈ x) | A User Theorem |
| two-03 | ⊦ dups(x + x) ↔ x ≠ [] | A User Theorem |