[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(σσ).take(m) ⊑ σσ(n)));
      comment: definition justified as skolem-function of theorems lim-exists and lim-unique.;
   
   
end enrich