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: |
|---|---|---|
| prefix-def | ⊦ σ ⊑ σ0 ↔ (∃ σ1. σ + σ1 = σ0) | An Axiom |
| mon-def | ⊦ mon(σσ) ↔ (∀ n. ⌜n⌝ + ⌜1⌝ < # σσ → σσ[n] ⊑ σσ[n + 1]) | An Axiom |
| lim-def | ⊦ mon(σσ) ∧ σσ ≠ [] → (∀ n. ⌜n⌝ < # σσ → σσ[n] ⊑ lim(σσ)) ∧ (∀ m. ¬ # lim(σσ) < ⌜m⌝ → (∃ n. ⌜n⌝ < # σσ ∧ lim(σσ) to m ⊑ σσ[n])) | An Axiom |
| lim-exists | mon(σσ), σσ ≠ [] ⊦ ∃ σ. (∀ n. ⌜n⌝ < # σσ → σσ[n] ⊑ σ) ∧ (∀ m. ¬ # σ < ⌜m⌝ → (∃ n. ⌜n⌝ < # σσ ∧ σ to m ⊑ σσ[n])) | A User Theorem |
| lim-unique | mon(σσ), σσ ≠ [], ∀ n. ⌜n⌝ < # σσ → σσ[n] ⊑ σ, ∀ n. ⌜n⌝ < # σσ → σσ[n] ⊑ σ0, ∀ m. ¬ # σ < ⌜m⌝ → (∃ n. ⌜n⌝ < # σσ ∧ σ to m ⊑ σσ[n]), ∀ m. ¬ # σ0 < ⌜m⌝ → (∃ n. ⌜n⌝ < # σσ ∧ σ0 to m ⊑ σσ[n]) ⊦ σ = σ0 | A User Theorem |
| mon-lem | mon(σσ), m ≤ n, ⌜n⌝ < # σσ ⊦ σσ[m] ⊑ σσ[n] | A User Theorem |
| prefix-trans | ⊦ σ ⊑ σ0 ∧ σ0 ⊑ σ1 → σ ⊑ σ1 | A User Theorem |