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: |
|---|---|---|
| iterate-rec | ⊦ ((f ^ (n + 1)))(S) = f(((f ^ n))(S)) | An Axiom |
| iterate-base | ⊦ ((f ^ 0))(S) = S | An Axiom |
| cont-def | ⊦ cont(f) ↔ (∀ Sn. chain(Sn) → (∀ x. f(λ x0. ∃ n. Sn(n)(x0))(x) ↔ (∃ n. f(Sn(n))(x)))) | An Axiom |
| chain-def | ⊦ chain(Sn) ↔ (∀ m, n. Sn(m) ⊆ Sn(n) ∨ Sn(n) ⊆ Sn(m)) | An Axiom |
| cont-iterate-fix | cont(f) ⊦ (λ x0. ∃ n. ((f ^ n))(λ x. false)(x0)) = f(λ x0. ∃ n. ((f ^ n))(λ x. false)(x0)) | A User Theorem |
| cont-monotone | cont(f) ⊦ monotone(f) | A User Theorem |
| iterate-is-fix | cont(f) ⊦ μ(f)(x) ↔ (∃ n. ((f ^ n))(λ x. false)(x)) | A User Theorem |
| iterate-subseq | monotone(f) ⊦ ((f ^ n))(λ x. false) ⊆ ((f ^ (n + 1)))(λ x. false) | A User Theorem |
| iterate-subseq-leq | monotone(f), m ≤ n ⊦ ((f ^ m))(λ x. false) ⊆ ((f ^ n))(λ x. false) | A User Theorem |
| iterate-subseq-mu | monotone(f) ⊦ ((f ^ n))(λ x. false) ⊆ μ(f) | A User Theorem |