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: |
|---|---|---|
| setequal-def | ⊦ x ≡ y ↔ ¬ ¬(x ⊆ y ∧ y ⊆ x) | An Axiom |
| elem-setequal | ⊦ x ≡ y ∧ a ∈ x → a ∈ y | A User Theorem |
| elem-setequal2 | ⊦ y ≡ x ∧ a ∈ x → a ∈ y | A User Theorem |
| ext-setequal | ⊦ x ≡ y ↔ (∀ a. a ∈ x ↔ a ∈ y) | A User Theorem |
| setequal-refl | ⊦ x ≡ x | A User Theorem |
| setequal-subset-trans1 | ⊦ x ≡ y ∧ x ⊆ z → y ⊆ z | A User Theorem |
| setequal-subset-trans2 | ⊦ x ≡ y ∧ y ⊆ z → x ⊆ z | A User Theorem |
| setequal-sym | ⊦ x ≡ y → (¬ y ≡ x ↔ false) | A User Theorem |
| setequal-trans | ⊦ x ≡ y ∧ y ≡ z → x ≡ z | A User Theorem |
| setequal-trans2 | ⊦ x ≡ y ∧ z ≡ y → x ≡ z | A User Theorem |
| setequal-trans3 | ⊦ y ≡ x ∧ y ≡ z → x ≡ z | A User Theorem |
| subset-setequal-trans1 | ⊦ x ⊆ y ∧ y ≡ z → x ⊆ z | A User Theorem |
| subset-setequal-trans2 | ⊦ x ⊆ y ∧ z ≡ y → x ⊆ z | A User Theorem |
| swap-init-setequal | ⊦ a ' + a0 ' + x ≡ a0 ' + a ' + x | A User Theorem |