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: |
|---|---|---|
| coinduction | monotone(f), ∀ x. φ(x) → f(λ x. ν(f)(x) ∨ φ(x))(x) ⊦ ∀ x. φ(x) → ν(f)(x) | A User Theorem |
| induction | monotone(f), ∀ x. f(λ x. μ(f)(x) ∧ φ(x))(x) → φ(x) ⊦ ∀ x. μ(f)(x) → φ(x) | A User Theorem |
| induction-hol | monotone(f), μ(f)(x), ∀ x. f(λ x. μ(f)(x) ∧ φ(x))(x) → φ(x) ⊦ φ(x) | A User Theorem |