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 | ⊦ s1 = s2 ↔ (∀ a. a ∈ s1 ↔ a ∈ s2) | An Axiom |
| In-empty | ⊦ ¬ a ∈ ∅ | An Axiom |
| In-insert | ⊦ a ∈ s ++ b ↔ a = b ∨ a ∈ s | An Axiom |
| Size-empty | ⊦ # ∅ = 0 | An Axiom |
| Size-insert | ⊦ ¬ a ∈ s → #(s ++ a) = # s + 1 | An Axiom |
| Subset | ⊦ s1 ⊆ s2 ↔ (∀ a. a ∈ s1 → a ∈ s2) | An Axiom |
| gen | set generated by ∅, ++; | An Axiom |
| add | ⊦ ¬ a ∈ s ++ b ↔ a ≠ b ∧ ¬ a ∈ s | A User Theorem |
| add-01 | ⊦ s ++ a ++ a = s ++ a | A User Theorem |
| addthree | ⊦ s ++ a ++ b ++ c ++ a = s ++ a ++ b ++ c | A User Theorem |
| addtwo | ⊦ s ++ a ++ b ++ a = s ++ b ++ a | A User Theorem |
| alle | ∀ a. ¬ a ∈ s ⊦ s = ∅ | A User Theorem |
| del | a ∈ s ⊦ ∃ s0. s = s0 ++ a ∧ ¬ a ∈ s0 | A User Theorem |
| eq | ⊦ a ∈ s → s ++ a = s | A User Theorem |
| eq-01 | ⊦ ¬ a ∈ s ∧ ¬ a ∈ s0 → (s ++ a = s0 ++ a ↔ s = s0) | A User Theorem |
| eq-02 | ⊦ ¬ a ∈ s → (s ++ a = ∅ ++ b ↔ a = b ∧ s = ∅) | A User Theorem |
| eq-03 | ⊦ s ++ a = s ↔ a ∈ s | A User Theorem |
| eq-04 | ⊦ s ++ b ++ a = s ++ a ++ b ↔ true | A User Theorem |
| eq-05 | ⊦ ∅ ++ a ++ b = ∅ ++ b ++ a ↔ true | A User Theorem |
| eq-06 | ⊦ ∅ ++ a ++ b = ∅ ++ b ++ a | A User Theorem |
| eq-subset | ⊦ s = s0 ↔ s ⊆ s0 ∧ s0 ⊆ s | A User Theorem |
| eqtwo | ⊦ ∅ ++ a ++ b = ∅ ++ a ++ c ↔ b = c | A User Theorem |
| eqtwo-01 | ⊦ ∅ ++ a ++ b = ∅ ++ c ++ b ↔ a = c | A User Theorem |
| ext-rec | ⊦ s1 = s0 ++ a ↔ (∀ b. b ∈ s1 ↔ b = a ∨ b ∈ s0) | A User Theorem |
| in | ⊦ a ∈ s → a ∈ s ++ b | A User Theorem |
| in-01 | ⊦ a ∈ s ++ a | A User Theorem |
| in-02 | ⊦ a ≠ b → (a ∈ s ++ b ↔ a ∈ s) | A User Theorem |
| in-03 | ⊦ ¬ a ∈ s → (a ∈ s ++ b ↔ a = b) | A User Theorem |
| in-04 | ⊦ a ∈ ∅ ++ b ↔ a = b | A User Theorem |
| in-05 | ⊦ s ++ a = s0 ++ b ∧ a ≠ b → a ∈ s0 | A User Theorem |
| in-06 | ⊦ a ∈ s ∧ s = ∅ ++ b → a = b | A User Theorem |
| indef | ⊦ a ∈ s ↔ (∃ s0. s = s0 ++ a ∧ ¬ a ∈ s0) | A User Theorem |
| ins-two | ⊦ a ∈ s → s ++ b ++ a = s ++ b | A User Theorem |
| ne | ⊦ ∅ ≠ s ++ a | A User Theorem |
| ne-01 | ⊦ a ∈ s → s ≠ ∅ | A User Theorem |
| ne-02 | ⊦ a ∈ s → (s = ∅ ↔ false) | A User Theorem |
| one | ⊦ (∀ a. a ∈ s → a = b) ∧ s ≠ ∅ → s = ∅ ++ b | A User Theorem |
| one-in | ⊦ # s = 1 ∧ a ∈ s → s = ∅ ++ a | A User Theorem |
| one-size | ⊦ s = ∅ ++ a → # s = 1 | A User Theorem |
| rax | ⊦ a ∈ s ++ b ↔ ¬ ¬(a = b ∨ a ∈ s) | A User Theorem |
| sel | ⊦ s = ∅ ∨ (∃ a. a ∈ s) | A User Theorem |
| selsize | ⊦ # s ≠ 0 → (∃ a. a ∈ s) | A User Theorem |
| size-exgr | # s < # s0 ⊦ ∃ a. a ∈ s0 ∧ ¬ a ∈ s | A User Theorem |
| size-ins | ⊦ # s + 1 = #(s ++ a) ↔ ¬ a ∈ s | A User Theorem |
| size-less | ⊦ ¬ # s + 1 < #(s ++ a) | A User Theorem |
| size-less-01 | ⊦ ¬ #(s ++ a) < # s | A User Theorem |
| size-one | ⊦ # s = 1 → (∃ a. s = ∅ ++ a) | A User Theorem |
| size-one-01 | ⊦ #(∅ ++ a) = 1 | A User Theorem |
| size-one-02 | ⊦ # s = 1 ∧ a ∈ s ∧ b ∈ s → a = b | A User Theorem |
| size-one-03 | ⊦ # s = 1 ↔ (∃ a. s = ∅ ++ a) | A User Theorem |
| size-three | ⊦ 2 < # s → (∃ a, b, c. a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c) | A User Theorem |
| size-three-01 | ⊦ a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ a ≠ b ∧ a ≠ c ∧ b ≠ c → 3 ≤ # s | A User Theorem |
| size-three-02 | ⊦ # s = 3 ↔ (∃ a, b, c. a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ s = ∅ ++ a ++ b ++ c) | A User Theorem |
| size-two | ⊦ # s = 2 ↔ (∃ a, b. a ≠ b ∧ s = ∅ ++ a ++ b) | A User Theorem |
| size-two-01 | ⊦ #(∅ ++ a ++ b) = 2 ↔ a ≠ b | A User Theorem |
| size-two-02 | ⊦ #(∅ ++ a ++ b) ≤ 2 | A User Theorem |
| size-two-03 | 1 < # s ⊦ ∃ a, b. a ≠ b ∧ a ∈ s ∧ b ∈ s | A User Theorem |
| size-two-04 | ⊦ # s ≠ 0 ∧ # s ≠ 1 ∧ a ∈ s → (∃ b. b ∈ s ∧ a ≠ b) | A User Theorem |
| size-two-05 | ⊦ # s = 2 ↔ (∃ a, b. a ≠ b ∧ s = ∅ ++ a ++ b ∧ a ∈ s ∧ b ∈ s) | A User Theorem |
| size-two-06 | ⊦ a ∈ s ∧ b ∈ s ∧ a ≠ b → 2 ≤ # s | A User Theorem |
| size-zero | ⊦ # s ≠ 0 → s ≠ ∅ | A User Theorem |
| size-zero-01 | ⊦ s ≠ ∅ → # s ≠ 0 | A User Theorem |
| size-zero-02 | ⊦ # s = 0 → s = ∅ | A User Theorem |
| size-zero-03 | ⊦ s = ∅ → # s = 0 | A User Theorem |
| sizesub | ⊦ s ⊆ s0 → # s ≤ # s0 | A User Theorem |
| sizesubl | ⊦ s ⊆ s0 ∧ a ∈ s0 ∧ ¬ a ∈ s → # s < # s0 | A User Theorem |
| sub-add | ⊦ a ∈ s0 → (s ++ a ⊆ s0 ↔ s ⊆ s0) | A User Theorem |
| sub-add-01 | ⊦ s ⊆ s ++ a | A User Theorem |
| sub-add-02 | ⊦ s ++ a ⊆ s0 → s ⊆ s0 | A User Theorem |
| sub-add-03 | ⊦ s ++ a ⊆ s0 ↔ s ⊆ s0 ∧ a ∈ s0 | A User Theorem |
| sub-add-04 | ⊦ s1 ⊆ s2 → s1 ++ a ⊆ s2 ++ a | A User Theorem |
| sub-e | ⊦ ∅ ⊆ s | A User Theorem |
| sub-idem | ⊦ s ⊆ s | A User Theorem |
| sub-in | ⊦ a ∈ s ∧ s ⊆ s0 → a ∈ s0 | A User Theorem |
| sub-insert | ⊦ ¬ a ∈ s → (s ⊆ s0 ++ a ↔ s ⊆ s0) | A User Theorem |
| sub-insert-01 | ⊦ s ⊆ s0 → s ⊆ s0 ++ a | A User Theorem |
| sub-ntrans | ⊦ s ⊆ s0 ∧ ¬ s ⊆ s1 → ¬ s0 ⊆ s1 | A User Theorem |
| sub-ntrans-01 | ⊦ s0 ⊆ s1 ∧ ¬ s ⊆ s1 → ¬ s ⊆ s0 | A User Theorem |
| sub-one | ⊦ s ≠ ∅ ∧ # s0 = 1 → (s ⊆ s0 ↔ s = s0) | A User Theorem |
| sub-one-01 | ⊦ s ≠ ∅ ++ a → (s ⊆ ∅ ++ a ↔ s = ∅) | A User Theorem |
| sub-one-02 | ⊦ ∅ ++ a ⊆ s ↔ a ∈ s | A User Theorem |
| sub-size | ⊦ s ⊆ s0 → ¬ # s0 < # s | A User Theorem |
| sub-size-eq | ⊦ s ⊆ s0 → (# s0 ≤ # s ↔ s = s0) | A User Theorem |
| sub-sizeneqex | s ⊆ s0, # s ≠ # s0 ⊦ ∃ a. a ∈ s0 ∧ ¬ a ∈ s | A User Theorem |
| sub-trans | ⊦ s ⊆ s0 ∧ s0 ⊆ s1 → s ⊆ s1 | A User Theorem |
| sub-two | ⊦ ∅ ++ a ++ b ⊆ ∅ ++ c ↔ a = b ∧ a = c | A User Theorem |
| subset | ⊦ s ⊆ s ++ a ++ b | A User Theorem |
| subset-empty | ⊦ s ⊆ ∅ ↔ s = ∅ | A User Theorem |
| subset-equal | ⊦ s ⊆ s0 → (s0 ⊆ s ↔ s = s0) | A User Theorem |
| subset-ins | ⊦ s ++ a ⊆ s0 ++ a ++ b ↔ s ⊆ s0 ++ a ++ b | A User Theorem |
| subset-insert | ⊦ s ⊆ s ++ a ++ b ++ c | A User Theorem |
| subset-insert-01 | ⊦ s ⊆ s ++ a ++ a0 ++ b ++ c | A User Theorem |
| subset-insert-02 | ⊦ s ⊆ s ++ a ++ a0 ++ a1 ++ b ++ c | A User Theorem |
| subset-insert-03 | ⊦ s ⊆ s ++ a ++ a0 ++ a1 ++ a2 ++ b ++ c | A User Theorem |
| subset-insert-04 | ⊦ s ⊆ s ++ a ++ a0 ++ a1 ++ a2 ++ a3 ++ b ++ c | A User Theorem |
| subset-insert-05 | ⊦ s ⊆ s ++ a ++ a0 ++ a1 ++ a2 ++ a3 ++ a4 ++ b ++ c | A User Theorem |
| subset-insert-06 | ⊦ s ⊆ s ++ a ++ a0 ++ a1 ++ a2 ++ a3 ++ a4 ++ a5 ++ b ++ c | A User Theorem |
| subset-insert-same | ⊦ s ++ a ⊆ s0 ++ a ↔ s ⊆ s0 ++ a | A User Theorem |
| subsize-eq | ⊦ s ⊆ s0 ∧ # s = # s0 → s = s0 | A User Theorem |
| subsize-eq-01 | ⊦ # s = # s0 → (s ⊆ s0 ↔ s = s0) | A User Theorem |
| sw | ⊦ s ++ b ++ a = s ++ a ++ b | A User Theorem |
| sw-01 | ⊦ s ++ a ++ b ++ c = s ++ c ++ a ++ b | A User Theorem |
| two | ⊦ a ≠ a0 → (∅ ++ a ++ b = ∅ ++ a0 ++ c ↔ a = c ∧ b = a0) | A User Theorem |
| two-01 | a ∈ s, s ≠ ∅ ++ a ⊦ ∃ b. b ∈ s ∧ b ≠ a | A User Theorem |