This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| montr-relative-def | ⊦ pmon(trp)(βf) ↔ (∀ σ1, α1, σ2, α2. # σ1 = # α1 + ⌜1⌝ ∧ # σ2 = # α2 + ⌜1⌝ ∧ σ1 ⊑ σ2 ∧ α1 ⊑ α2 ∧ trp(σ1, α1) ∧ trp(σ2, α2) → βf(σ1, α1) ⊑ βf(σ2, α2)) | An Axiom |
| lift-not-trp-fininf | ⊦ ¬ lift(trlp)(⌜sl⌝ , ⌜af⌝ ) | An Axiom |
| pbdtr-def | ⊦ pbd(βf) ↔ (∀ sf, af, bl. (∀ n. βf(⌜sf.take(n + 1)⌝ , ⌜af.take(n)⌝ ) ⊑ ⌜bl⌝ ) ↔ βf(⌜sf⌝ , ⌜af⌝ ) ⊑ ⌜bl⌝ ) | An Axiom |
| pbd-relative-def | ⊦ ppbd(αp)(f) ↔ (∀ af, bl. αp(⌜af⌝ ) → ((∀ n. f(⌜af.take(n)⌝ ) ⊑ ⌜bl⌝ ) ↔ f(⌜af⌝ ) ⊑ ⌜bl⌝ )) | An Axiom |
| montrl-equiv | ⊦ mon(trf) ↔ (∀ sf, af. mon(⌜λ n. ⌜trf(sf.take(n + 1), af.take(n))⌝ ⌝ )) | A User Theorem |
| lift-trp-fin | ⊦ lift(trlp)(⌜sl⌝ , ⌜al⌝ ) ↔ trlp(sl, al) | An Axiom |
| conttr-def | ⊦ cont(βf) ↔ mon(βf) ∧ pbd(βf) | An Axiom |
| twomon-limsize | mon(⌜σf⌝ ), mon(⌜αf⌝ ), ∀ n. # σf(n) = # αf(n) + ⌜m⌝ ⊦ # lim(⌜σf⌝ ) = # lim(⌜αf⌝ ) + ⌜m⌝ | A User Theorem |
| pfxclosed-lift | ⊦ pfxclosed(alp) → pfxclosed(lift(alp)) | A User Theorem |
| lift-cont | ⊦ mon(lf) → cont(lift(lf)) | A User Theorem |
| montrl-relative-def | ⊦ pmon(trlp)(trf) ↔ (∀ sl1, al1, sl2, al2. # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 ∧ al1 ⊑ al2 ∧ sl1 ⊑ sl2 ∧ trlp(sl1, al1) ∧ trlp(sl2, al2) → trf(sl1, al1) ⊑ trf(sl2, al2)) | An Axiom |
| lifttr-pcont | ⊦ pmon(trlp)(trf) → pcont(lift(trlp))(lift(trf)) | A User Theorem |
| conttr-thm | ⊦ cont(βf) ∧ mon(⌜σf⌝ ) ∧ mon(⌜αf⌝ ) ∧ (∀ n. # σf(n) = # αf(n) + ⌜1⌝ ) → lim(⌜λ n. βf(σf(n), αf(n))⌝ ) = βf(lim(⌜σf⌝ ), lim(⌜αf⌝ )) | A User Theorem |
| lifted-def | ⊦ lifted(alp)(lf, f) ↔ (∀ α. lift(alp)(α) → lift(lf)(α) = f(α)) | An Axiom |
| conttr-relative-def | ⊦ pcont(trp)(βf) ↔ pmon(trp)(βf) ∧ ppbd(trp)(βf) | An Axiom |
| lift-trp-inf | ⊦ lift(trlp)(⌜sf⌝ , ⌜af⌝ ) ↔ (∀ n. trlp(sf.take(n + 1), af.take(n))) | An Axiom |
| liftedtr-def | ⊦ lifted(trlp)(trf, βf) ↔ (∀ σ, α. lift(trlp)(σ, α) → lift(trf)(σ, α) = βf(σ, α)) | An Axiom |
| pdfclosedtr-def | ⊦ pfxclosed(trp) ↔ (∀ σ1, σ2, α1, α2. trp(σ2, α2) ∧ σ1 ⊑ σ2 ∧ α1 ⊑ α2 ∧ # σ1 = # α1 + ⌜1⌝ ∧ # σ2 = # α2 + ⌜1⌝ → trp(σ1, α1)) | An Axiom |
| lift-pred-inf | ⊦ lift(alp)(⌜af⌝ ) ↔ (∀ n. alp(af.take(n))) | An Axiom |
| lifttr-inf | ⊦ lift(trf)(⌜sf⌝ , ⌜af⌝ ) = lim(⌜λ n. ⌜trf(sf.take(n + 1), af.take(n))⌝ ⌝ ) | An Axiom |
| lift-fin | ⊦ lift(lf)(⌜al⌝ ) = ⌜lf(al)⌝ | An Axiom |
| cont-rel-thm | ⊦ pcont(lift(alp))(f) ∧ mon(⌜λ n. ⌜alf(n)⌝ ⌝ ) ∧ (∀ n. alp(alf(n))) ∧ lift(alp)(lim(⌜λ n. ⌜alf(n)⌝ ⌝ )) ∧ pfxclosed(alp) → lim(⌜λ n. f(⌜alf(n)⌝ )⌝ ) = f(lim(⌜λ n. ⌜alf(n)⌝ ⌝ )) | A User Theorem |
| montr-def | ⊦ mon(βf) ↔ (∀ σ1, α1, σ2, α2. # σ1 = # α1 + ⌜1⌝ ∧ # σ2 = # α2 + ⌜1⌝ ∧ σ1 ⊑ σ2 ∧ α1 ⊑ α2 → βf(σ1, α1) ⊑ βf(σ2, α2)) | An Axiom |
| cont-relative-thm | ⊦ pcont(αp)(f) ∧ mon(⌜αf⌝ ) ∧ (∀ n. αp(αf(n))) ∧ αp(lim(⌜αf⌝ )) ∧ pfxclosed(αp) → lim(⌜λ n. f(αf(n))⌝ ) = f(lim(⌜αf⌝ )) | A User Theorem |
| pbdtr-relative-def | ⊦ ppbd(trp)(βf) ↔ (∀ sf, af, bl. trp(⌜sf⌝ , ⌜af⌝ ) → ((∀ n. βf(⌜sf.take(n + 1)⌝ , ⌜af.take(n)⌝ ) ⊑ ⌜bl⌝ ) ↔ βf(⌜sf⌝ , ⌜af⌝ ) ⊑ ⌜bl⌝ )) | An Axiom |
| lift-not-trp-inffin | ⊦ ¬ lift(trlp)(⌜sf⌝ , ⌜al⌝ ) | An Axiom |
| cont-relative-def | ⊦ pcont(αp)(f) ↔ pmon(αp)(f) ∧ ppbd(αp)(f) | An Axiom |
| fun-neq | ⊦ bf ≠ bf0 ↔ (∃ n. bf(n) ≠ bf0(n) ∧ (∀ n0. n0 < n → bf(n0) = bf0(n0))) | A User Theorem |
| pdfclosedtrl-def | ⊦ pfxclosed(trlp) ↔ (∀ sl1, sl2, al1, al2. trlp(sl2, al2) ∧ sl1 ⊑ sl2 ∧ al1 ⊑ al2 ∧ # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 → trlp(sl1, al1)) | An Axiom |
| cont-thm | ⊦ cont(f) ∧ mon(⌜αf⌝ ) → lim(⌜λ n. f(αf(n))⌝ ) = f(lim(⌜αf⌝ )) | A User Theorem |
| montrl-def | ⊦ mon(trf) ↔ (∀ sl1, al1, sl2, al2. # sl1 = # al1 + 1 ∧ # sl2 = # al2 + 1 ∧ al1 ⊑ al2 ∧ sl1 ⊑ sl2 → trf(sl1, al1) ⊑ trf(sl2, al2)) | An Axiom |
| mon-def | ⊦ mon(f) ↔ (∀ α1, α2. α1 ⊑ α2 → f(α1) ⊑ f(α2)) | An Axiom |
| pcont-lifted | ⊦ lifted(alp)(lf, f) ∧ pmon(alp)(lf) → pcont(lift(alp))(f) | A User Theorem |
| lift-pcont | ⊦ pmon(alp)(lf) → pcont(lift(alp))(lift(lf)) | A User Theorem |
| lifttr-cont | ⊦ mon(trf) → cont(lift(trf)) | A User Theorem |
| conttr-relative-thm | ⊦ pcont(trp)(βf) ∧ mon(⌜σf⌝ ) ∧ mon(⌜αf⌝ ) ∧ (∀ n. trp(σf(n), αf(n))) ∧ trp(lim(⌜σf⌝ ), lim(⌜αf⌝ )) ∧ pfxclosed(trp) ∧ (∀ n. # σf(n) = # αf(n) + ⌜1⌝ ) → lim(⌜λ n. βf(σf(n), αf(n))⌝ ) = βf(lim(⌜σf⌝ ), lim(⌜αf⌝ )) | A User Theorem |
| conttr-rel-thm | ⊦ pcont(lift(trlp))(βf) ∧ mon(⌜λ n. ⌜slf(n)⌝ ⌝ ) ∧ mon(⌜λ n. ⌜alf(n)⌝ ⌝ ) ∧ (∀ n. trlp(slf(n), alf(n))) ∧ lift(trlp)(lim(⌜λ n. ⌜slf(n)⌝ ⌝ ), lim(⌜λ n. ⌜alf(n)⌝ ⌝ )) ∧ pfxclosed(trlp) ∧ (∀ n. # slf(n) = # alf(n) + 1) → lim(⌜λ n. βf(⌜slf(n)⌝ , ⌜alf(n)⌝ )⌝ ) = βf(lim(⌜λ n. ⌜slf(n)⌝ ⌝ ), lim(⌜λ n. ⌜alf(n)⌝ ⌝ )) | A User Theorem |
| lifttr-fin | ⊦ lift(trf)(⌜sl⌝ , ⌜al⌝ ) = ⌜trf(sl, al)⌝ | An Axiom |
| pfxclosed-lift-tr | ⊦ pfxclosed(trlp) → pfxclosed(lift(trlp)) | A User Theorem |
| pbd-def | ⊦ pbd(f) ↔ (∀ af, bl. (∀ n. f(⌜af.take(n)⌝ ) ⊑ ⌜bl⌝ ) ↔ f(⌜af⌝ ) ⊑ ⌜bl⌝ ) | An Axiom |
| monl-def | ⊦ mon(lf) ↔ (∀ al1, al2. al1 ⊑ al2 → lf(al1) ⊑ lf(al2)) | An Axiom |
| monl-equiv | ⊦ mon(lf) ↔ (∀ af. mon(⌜λ n. ⌜lf(af.take(n))⌝ ⌝ )) | A User Theorem |
| lift-inf | ⊦ lift(lf)(⌜af⌝ ) = lim(⌜λ n. ⌜lf(af.take(n))⌝ ⌝ ) | An Axiom |
| lift-pred-fin | ⊦ lift(alp)(⌜al⌝ ) ↔ alp(al) | An Axiom |
| mon-relative-def | ⊦ pmon(αp)(f) ↔ (∀ α1, α2. αp(α1) ∧ αp(α2) ∧ α1 ⊑ α2 → f(α1) ⊑ f(α2)) | An Axiom |
| pfxclosedl-def | ⊦ pfxclosed(alp) ↔ (∀ al1, al2. alp(al2) ∧ al1 ⊑ al2 → alp(al1)) | An Axiom |
| pfxclosed-def | ⊦ pfxclosed(αp) ↔ (∀ α1, α2. αp(α2) ∧ α1 ⊑ α2 → αp(α1)) | An Axiom |
| monl-relative-def | ⊦ pmon(alp)(lf) ↔ (∀ al1, al2. alp(al1) ∧ alp(al2) ∧ al1 ⊑ al2 → lf(al1) ⊑ lf(al2)) | An Axiom |
| pconttr-lifted | ⊦ lifted(trlp)(trf, βf) ∧ pmon(trlp)(trf) → pcont(lift(trlp))(βf) | A User Theorem |
| cont-def | ⊦ cont(f) ↔ mon(f) ∧ pbd(f) | An Axiom |