[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-old
enrich
   infinite-append-old
with
   predicates 
       mon : stream(stream('a));
   
   variables 
       σf : nat → stream('a);
       p : 'a → bool;
       nf : nat → 'a;
       σ : stream('a);
       nnf : nat → nat;
       np : nat → bool;
       x : list('a);
       a : 'a;
       b : 'a;
       m : nat;
       n : nat;
       n∞ : natinf;
       σσ : stream(stream('a));
   
   partial functions 
       lim : stream(stream('a)) → stream('a) 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