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: |
|---|---|---|
| oc-e | ⊦ #oc(a, []) = 0 | An Axiom |
| oc-y | ⊦ #oc(a, a ' + x) = #oc(a, x) + 1 | An Axiom |
| oc-n | ⊦ a ≠ b → #oc(a, b ' + x) = #oc(a, x) | An Axiom |
| msubset | ⊦ x ⊆m y ↔ (∀ a. #oc(a, x) ≤ #oc(a, y)) | An Axiom |
| perm | ⊦ perm(x, y) ↔ x ⊆m y ∧ y ⊆m x | An Axiom |
| a | ⊦ perm(x, y) → perm(z + x, z + y) | A User Theorem |
| ad | ⊦ a ∈ y → perm(x + (y -1l a), (x + y) -1l a) | A User Theorem |
| adjoin | ⊦ perm(x, y) → perm(x ++ a, y ++ a) | A User Theorem |
| app | ⊦ perm(x + y, x + z) ↔ perm(y, z) | A User Theorem |
| app-01 | ⊦ perm(x + y, z + y) ↔ perm(x, z) | A User Theorem |
| app-02 | ⊦ perm(x + y, z + x) ↔ perm(y, z) | A User Theorem |
| app-03 | ⊦ perm(x, x + y) ↔ y = [] | A User Theorem |
| app-04 | ⊦ perm(y, x + y) ↔ x = [] | A User Theorem |
| app-05 | ⊦ perm(x + a ', y + a ') ↔ perm(x, y) | A User Theorem |
| c | ⊦ perm(x, y + z) → perm(x0 + x, y + x0 + z) | A User Theorem |
| cons | ⊦ perm(a ' + x, a ' + y) ↔ perm(x, y) | A User Theorem |
| del | ⊦ perm(x, a ' + y) ↔ a ∈ x ∧ perm(x -1l a, y) | A User Theorem |
| del-01 | ⊦ perm(a ' + x, y) ↔ ¬ ¬(a ∈ y ∧ perm(x, y -1l a)) | A User Theorem |
| del-02 | ⊦ perm(x -1l a, y -1l a) ∧ a ∈ x ∧ a ∈ y → perm(x, y) | A User Theorem |
| del-03 | ⊦ perm(x, a ' + y) ↔ ¬ ¬(a ∈ x ∧ perm(x -1l a, y)) | A User Theorem |
| del-04 | ⊦ perm(x, y) → perm(x -1l a, y -1l a) | A User Theorem |
| del-05 | ⊦ perm(x, x -1l a) ↔ ¬ a ∈ x | A User Theorem |
| del-in | ⊦ a ∈ x ∧ a ∈ y → (perm(x -1l a, y -1l a) ↔ perm(x, y)) | A User Theorem |
| del1 | ⊦ a ∈ x → #oc(a, x -1l a) = #oc(a, x) -1 | A User Theorem |
| del1-01 | ⊦ a ≠ b → #oc(a, x -1l b) = #oc(a, x) | A User Theorem |
| delapp | ⊦ perm(x + y, y -1l a) ↔ x = [] ∧ ¬ a ∈ y | A User Theorem |
| diff | ⊦ perm(x, x0) ∧ perm(y, y0) → perm(x \ y, x0 \ y0) | A User Theorem |
| empty | ⊦ perm(x, []) ↔ x = [] | A User Theorem |
| empty-01 | ⊦ perm([], y) ↔ y = [] | A User Theorem |
| filter | ⊦ perm(x, x0) ∧ perm(y, y0) → perm(filter(x, y), filter(x0, y0)) | A User Theorem |
| in | ⊦ a ∈ y ∧ ¬ a ∈ x → ¬ perm(x, y) | A User Theorem |
| in-01 | ⊦ ¬ a ∈ x → ¬ perm(x, a ' + y) | A User Theorem |
| in-02 | ⊦ perm(a ' + x, b ' + y) ∧ a ≠ b → a ∈ y | A User Theorem |
| in-03 | ⊦ perm(a ' + x, b ' + y) ∧ a ≠ b → b ∈ x | A User Theorem |
| in-04 | ⊦ perm(x, y) ∧ a ∈ x → a ∈ y | A User Theorem |
| in-05 | ⊦ a ∈ x → #oc(a, x) ≠ 0 | A User Theorem |
| in-put | ⊦ 1 < #oc(a, x) ∧ m < # x → a ∈ x[m, b] | A User Theorem |
| l | ⊦ perm(x, y) → (# x = # y ↔ true) | A User Theorem |
| neq | ⊦ perm(x, y) ∧ ¬ perm(x0, y) → x ≠ x0 | A User Theorem |
| nodups | ∀ a. a ∈ x ↔ a ∈ y, ¬ dups(x), ¬ dups(y) ⊦ perm(x, y) | A User Theorem |
| notin | ⊦ ¬ a ∈ x → #oc(a, x) = 0 | A User Theorem |
| oc | ⊦ x ⊆m y → ¬ #oc(a, y) < #oc(a, x) | A User Theorem |
| oc-adjoin | ⊦ a ≠ b → #oc(a, x ++ b) = #oc(a, x) | A User Theorem |
| oc-del | ⊦ ¬ #oc(a, x) < #oc(a, x -1l b) | A User Theorem |
| oc-del-01 | ⊦ a ∈ y → #oc(a, (x + y) -1l a) = #oc(a, x + y) -1 | A User Theorem |
| oc-del-02 | ⊦ #oc(a0, x) ≤ #oc(a0, y) → ¬ #oc(a0, y -1l a) < #oc(a0, x -1l a) | A User Theorem |
| oc-diff | ⊦ a ∈ y → #oc(a, x \ y) = 0 | A User Theorem |
| oc-diff-01 | ⊦ ¬ a ∈ y → #oc(a, x \ y) = #oc(a, x) | A User Theorem |
| oc-dups | ⊦ n < #oc(a, x) ∧ ¬ dups(x) → #oc(a, x) = 1 | A User Theorem |
| oc-filt | ⊦ a ∈ y → #oc(a, filter(x, y)) = #oc(a, x) | A User Theorem |
| oc-filt-01 | ⊦ ¬ a ∈ y → #oc(a, filter(x, y)) = 0 | A User Theorem |
| oc-zero | ⊦ #oc(a, x) = 0 ↔ ¬ a ∈ x | A User Theorem |
| ocappend | ⊦ #oc(a, x + y) = #oc(a, x) + #oc(a, y) | A User Theorem |
| ocnodups | ⊦ n ≤ #oc(a, x) ∧ ¬ dups(x) → n ≤ 1 | A User Theorem |
| ocnodups-01 | ⊦ ¬ dups(x) → (1 ≤ #oc(a, x) ↔ a ∈ x) | A User Theorem |
| ocone | ⊦ a ∈ x → (#oc(a, x) ≤ 1 ↔ #oc(a, x) = 1) | A User Theorem |
| ocs-del | ⊦ #oc(a, x -l a) = 0 | A User Theorem |
| ocs-del-del1 | ⊦ #oc(a, x) = 1 → x -l a = x -1l a | A User Theorem |
| ocs-del-length | ⊦ a ≠ b → #oc(a, x -l b) = #oc(a, x) | A User Theorem |
| ocs-del1 | ⊦ 1 < #oc(a, x) → a ∈ x -1l a | A User Theorem |
| ocs-del1-if | ⊦ #oc(a, x -1l b) = (a ≠ b ∨ ¬ b ∈ x ⊃ #oc(a, x);#oc(a, x) -1) | A User Theorem |
| ocs-dups-ex | ⊦ dups(x) ↔ (∃ a. a ∈ x ∧ #oc(a, x) > 1) | A User Theorem |
| ocs-mklist | ⊦ x = mklist(a, #oc(a, x)) ↔ x -l a = [] | A User Theorem |
| ocs-not-more | ⊦ ¬ # x < #oc(a, x) | A User Theorem |
| ocs-put | ⊦ x[m] ≠ a ∧ m < # x → #oc(a, x[m, a]) = #oc(a, x) + 1 | A User Theorem |
| ocs-put-01 | ⊦ x[m] ≠ a ∧ a ≠ b ∧ m < # x → #oc(a, x[m, b]) = #oc(a, x) | A User Theorem |
| ocs-put-02 | ⊦ x[m] = a ∧ a ≠ b ∧ m < # x → #oc(a, x[m, b]) = #oc(a, x) -1 | A User Theorem |
| ocs-same-length-all | ⊦ #oc(a, x) = # x ↔ (∀ b. b ∈ x → b = a) | A User Theorem |
| ocs-same-length-mklist | ⊦ #oc(a, x) = # x ↔ x = mklist(a, # x) | A User Theorem |
| ocs-sw | ⊦ m < # x ∧ n < # x → #oc(a, x[m, x[n]][n, x[m]]) = #oc(a, x) | A User Theorem |
| one | ⊦ #oc(a, a ') = 1 | A User Theorem |
| one-01 | ⊦ a ≠ b → #oc(a, b ') = 0 | A User Theorem |
| papp | perm(x, x0), perm(y, y0) ⊦ perm(x + y, x0 + y0) | A User Theorem |
| papp-01 | perm(x, x0), perm(y, y0) ⊦ perm(x + y, y0 + x0) | A User Theorem |
| papp-02 | perm(x, x0), perm(x + y, y0 + x0) ⊦ perm(y, y0) | A User Theorem |
| papp-03 | ⊦ perm(x, x0) → (perm(x + y, x0 + y0) ↔ perm(y, y0)) | A User Theorem |
| perm-all | ⊦ perm(x, y) ↔ (∀ a. a ∈ x ∨ a ∈ y → #oc(a, x) = #oc(a, y)) | A User Theorem |
| perm-com1 | ⊦ perm(x + y, z) → perm(y + x, z) | A User Theorem |
| perm-com2 | ⊦ perm(x, y + z) → perm(x, z + y) | A User Theorem |
| perm-def | ⊦ perm(x, y) ↔ ¬ ¬(x ⊆m y ∧ y ⊆m x) | A User Theorem |
| perm-del | ⊦ perm(x, y) → (perm(x -1l a, z) ↔ perm(y -1l a, z)) | A User Theorem |
| perm-del-01 | ⊦ perm(x -l a, z) ∧ perm(x, y) → (¬ perm(y -l a, z) ↔ false) | A User Theorem |
| perm-del-in | ⊦ a ∈ y → ¬ perm(x -l a, y) | A User Theorem |
| perm-dups | perm(x, y), ¬ dups(x) ⊦ ¬ dups(y) | A User Theorem |
| perm-dups-01 | ⊦ dups(x) ∧ ¬ dups(y) → ¬ perm(x, y) | A User Theorem |
| perm-dups-02 | ⊦ ¬ dups(x) ∧ dups(y) → ¬ perm(x, y + z) | A User Theorem |
| perm-dups-03 | ⊦ ¬ dups(x) ∧ dups(z) → ¬ perm(x, y + z) | A User Theorem |
| perm-e | ⊦ perm([], []) | A User Theorem |
| perm-l | ⊦ perm(a ' + x, y) ↔ a ∈ y ∧ perm(x, y -1l a) | A User Theorem |
| perm-last-rec | ⊦ perm(x, y + a ') ↔ a ∈ x ∧ perm(x -1l a, y) | A User Theorem |
| perm-mklist | ⊦ perm(x, mklist(a, n)) ↔ x = mklist(a, n) | A User Theorem |
| perm-mklist-del | ⊦ ¬ a ∈ y → (perm(x, mklist(a, #oc(a, x)) + y) ↔ perm(x -l a, y)) | A User Theorem |
| perm-one | ⊦ perm(x, a ') ↔ x = a ' | A User Theorem |
| perm-put | ⊦ n < # y → (perm(x, y[n, a]) ↔ a ∈ x ∧ perm(x -1l a, y -1l y[n])) | A User Theorem |
| perm-put-del1 | ⊦ n < # y → perm(y[n, a] -1l a, y -1l y[n]) | A User Theorem |
| perm-r | ⊦ y ≠ [] → ¬ perm([], y) | A User Theorem |
| perm-rec | ⊦ perm(y, z + a ' + x) ↔ a ∈ y ∧ perm(y -1l a, z + x) | A User Theorem |
| perm-rev | ⊦ perm(x, rev(x)) | A User Theorem |
| perm-rev-01 | ⊦ perm(x, rev(y)) ↔ perm(x, y) | A User Theorem |
| perm-rmdup-rev | ⊦ perm(x, rmdup(rev(y))) ↔ perm(x, rmdup(y)) | A User Theorem |
| perm-rmv-in | ⊦ perm(x + (a + y), x0 + (a + y0)) ↔ perm(x + y, x0 + y0) | A User Theorem |
| perm-rmv-in-list | ⊦ perm(x + a ' + y, x0 + a ' + y0) ↔ perm(x + y, x0 + y0) | A User Theorem |
| perm-same-prefix | ⊦ perm(y, z) ↔ (∃ x, y0, z0. y = x + y0 ∧ z = x + z0 ∧ perm(y0, z0)) | A User Theorem |
| perm-shift-in2 | ⊦ perm(x, y + z + a ') → perm(x, y + a ' + z) | A User Theorem |
| perm-shift-out2 | ⊦ perm(x, y + a ' + z) → perm(x, y + z + a ') | A User Theorem |
| perm-switch | ⊦ m < # y ∧ n < # y ∧ a = y[n] ∧ b = y[m] → (perm(x, y[m, a][n, b]) ↔ perm(x, y)) | A User Theorem |
| rec | ⊦ a ≠ b → (perm(a ' + x, b ' + y) ↔ a ∈ y ∧ b ∈ x ∧ perm(x -1l b, y -1l a)) | A User Theorem |
| rec-01 | ⊦ perm(x + a ' + x0, y) ↔ a ∈ y ∧ perm(x + x0, y -1l a) | A User Theorem |
| ref | ⊦ perm(x, x) | A User Theorem |
| rest | ⊦ a ' + x ⊆m b ' + x ↔ a = b | A User Theorem |
| shift | ⊦ perm(x + y, y + x) | A User Theorem |
| shift-01 | ⊦ perm(x + a ' + y, a ' + x + y) | A User Theorem |
| shift-02 | ⊦ perm(x + x0, y) ↔ perm(x0 + x, y) | A User Theorem |
| shift-03 | ⊦ perm(x + a ' + x0, y) ↔ perm(a ' + x + x0, y) | A User Theorem |
| size-perm | # x = # y, ¬ dups(x), ∀ a. a ∈ x → a ∈ y ⊦ perm(x, y) | A User Theorem |
| sub-del-any | ⊦ x ⊆m y ↔ x -l a ⊆m y -l a ∧ #oc(a, x) ≤ #oc(a, y) | A User Theorem |
| subapp | ⊦ x ⊆m x0 ∧ y ⊆m y0 → x + y ⊆m x0 + y0 | A User Theorem |
| subapp-01 | ⊦ x ⊆m x0 ∧ y ⊆m y0 → y + x ⊆m x0 + y0 | A User Theorem |
| subapp-02 | ⊦ x ⊆m x0 → x ⊆m x0 + y | A User Theorem |
| subapp-03 | ⊦ x ⊆m x0 → x ⊆m y + x0 | A User Theorem |
| subdel | ⊦ x ⊆m y -1l a → (¬ x ⊆m y ↔ false) | A User Theorem |
| subdel-01 | ⊦ x ⊆m y + (y0 -1l a) ∧ a ∈ y0 → x ⊆m (y + y0) -1l a | A User Theorem |
| subdel-02 | ⊦ x -1l a ⊆m y ↔ x -l a ⊆m y -l a ∧ #oc(a, x) ≤ #oc(a, y) + 1 | A User Theorem |
| subdel-03 | ⊦ x ⊆m y -1l a ↔ x -l a ⊆m y -l a ∧ (#oc(a, x) < #oc(a, y) ∨ ¬ a ∈ x) | A User Theorem |
| subempty | ⊦ [] ⊆m x | A User Theorem |
| subperm | ⊦ x ⊆ y ∧ perm(x, x0) → x0 ⊆ y | A User Theorem |
| subperm-01 | ⊦ x ⊆ y ∧ perm(y, y0) → x ⊆ y0 | A User Theorem |
| subrec | ⊦ a ' + x ⊆m y ↔ ¬ ¬(a ∈ y ∧ x ⊆m y -1l a) | A User Theorem |
| subrec-01 | ⊦ x ⊆m a ' + y ↔ #oc(a, x) ≤ #oc(a, y) + 1 ∧ x -1l a ⊆m y | A User Theorem |
| subsize | ⊦ x ⊆m y → # x ≤ # y | A User Theorem |
| sym | ⊦ perm(x, y) ↔ perm(y, x) | A User Theorem |
| sym-01 | ⊦ perm(x, y) → perm(y, x) | A User Theorem |
| sym-02 | ⊦ ¬ perm(x, y) → ¬ perm(y, x) | A User Theorem |
| trans | ⊦ perm(x, y) ∧ perm(y, z) → perm(x, z) | A User Theorem |