[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
   infinite-append
with
   predicates 
       mon : Stream(Stream('a));
   
   variables 
       σf : Nat → Stream('a);
       lf : Nat → List('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));
       ii : Nat → Nat;
   
   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