[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
   

   
   
   functions  lim : streamstream → stream;
   predicates  mon : streamstream;
               . ⊑ . : stream × stream;
   
   
   
   

   

   axioms prefix-def :  ⊦ σ ⊑ σ0 ↔ (∃ σ1. σ + σ1 = σ0);
          used for: ls;
          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