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: |
|---|---|---|
| subseteq-def | ⊦ S ⊆ S0 ↔ (∀ x. S(x) → S0(x)) | An Axiom |
| monotone-def | ⊦ monotone(f) ↔ (∀ S, S0. S ⊆ S0 → f(S) ⊆ f(S0)) | An Axiom |
| least-prefixpoint-def | ⊦ μ(f)(x) ↔ (∀ S. f(S) ⊆ S → S(x)) | An Axiom |
| union-def | ⊦ UN(SS)(x) ↔ (∃ S. SS(S) ∧ S(x)) | An Axiom |
| compl-def | ⊦ compl(f)(S)(x) ↔ ¬ f(λ x0. ¬ S(x0))(x) | An Axiom |
| greatest-prefixpoint-def | ⊦ ν(f)(x) ↔ ¬ μ(compl(f))(x) | An Axiom |
| intersection-def | ⊦ IS(SS)(x) ↔ (∀ S. SS(S) → S(x)) | An Axiom |
| compl-inverse | ⊦ compl(compl(f)) = f | A User Theorem |
| compl-monotone | ⊦ monotone(f) → (¬ monotone(compl(f)) ↔ false) | A User Theorem |
| eq-bothsubset | ⊦ S = S0 ↔ S ⊆ S0 ∧ S0 ⊆ S | A User Theorem |
| fixpoint | monotone(f) ⊦ f(μ(f)) = μ(f) | A User Theorem |
| fixpoint-nu | monotone(f) ⊦ f(ν(f)) = ν(f) | A User Theorem |
| least-fixpoint | monotone(f), f(S) = S ⊦ μ(f) ⊆ S | A User Theorem |
| mu-is-IS | ⊦ μ(f) = IS(λ S. f(S) ⊆ S) | A User Theorem |
| mu-subset-nu | monotone(f) ⊦ μ(f) ⊆ ν(f) | A User Theorem |
| nu-is-UN | ⊦ ν(f) = UN(λ S. S ⊆ f(S)) | A User Theorem |
| prefixpoint | monotone(f) ⊦ f(μ(f)) ⊆ μ(f) | A User Theorem |
| prefixpoint-aux | monotone(f), f(S) ⊆ S ⊦ μ(f) ⊆ S | A User Theorem |
| prefixpoint-aux-nu | monotone(f), S ⊆ f(S) ⊦ S ⊆ ν(f) | A User Theorem |
| prefixpoint-aux2 | ∀ S. f(S) ⊆ S → S0 ⊆ S ⊦ S0 ⊆ μ(f) | A User Theorem |
| prefixpoint-rev | monotone(f) ⊦ μ(f) ⊆ f(μ(f)) | A User Theorem |
| subset-refl | ⊦ S ⊆ S | A User Theorem |
| subset-trans | ⊦ S ⊆ S0 ∧ S0 ⊆ S1 → S ⊆ S1 | A User Theorem |