[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Specification streamseq-mon-lim
enrich
   stream-of-streams, 
   infinite-append
with
   predicates 
       mon : Streamstream;
   
   variables 
       σ : Stream;
       x : List;
       σσ : Streamstream;
       n : Nat;
       m : Nat;
       nf : Nat → Elem;
       f : Stream → Stream;
       lf : Nat → List;
   
   partial functions 
       lim : Streamstream → Stream with λ σσ. mon(σσ) ∧ σσ ≠ [];
   
   
   axioms 
      mon-def: mon(σσ) ↔ (∀ n. ⌜n⌝  + ⌜1⌝  < # σσ → σσ[n] ⊑ σσ[n + 1]);
      used for: ls;
      
      lim-def: 
        mon(σσ) ∧ σσ ≠ []
      → (∀ n. ⌜n⌝  < # σσ → σσ[n] ⊑ lim(σσ)) ∧ (∀ m. ¬ # lim(σσ) < ⌜m⌝  → (∃ n. ⌜n⌝  < # σσ ∧ lim(σσ) to m ⊑ σσ[n]));
      comment: definition justified as skolem-function of theorems lim-exists and lim-unique.;
   
   
end enrich