enrich
   stream-basic, 
   nat-inf
with
   constants 
       [] : stream('a);
   
   functions 
       . + . : 'a × stream('a) → stream('a);
       . + . : stream('a) × stream('a) → stream('a);
       # . : stream('a) → natinf;
       . to . : (nat → 'a) × nat → list('a) prio 8 left;
       . from . : (nat → 'a) × nat → nat → 'a prio 8 left;
   
   predicates 
       . ⊑ . : stream('a) × stream('a);
   
   variables 
       σ : stream('a);
       nf : nat → 'a;
       x : list('a);
       y : list('a);
       z : list('a);
       a : 'a;
       m : nat;
       n : nat;
       n∞ : natinf;
   
   partial functions 
       hd : stream('a) → 'a with λ σ. σ ≠ [];
       tl : stream('a) → stream('a) with λ σ. σ ≠ [];
       . [ . ] : stream('a) × nat → 'a with λ σ, n. finp(σ) → ⌜n⌝  < # σ;
       . [ . := . ] : stream('a) × nat × 'a → stream('a) with λ σ, n, a. finp(σ) → ⌜n⌝  < # σ;
       . to . : stream('a) × nat → list('a) prio 8 left with λ σ, n. finp(σ) → ⌜n⌝  < # σ ∨ ⌜n⌝  = # σ;
       . to∞ . : stream('a) × natinf → stream('a) prio 8 left with λ σ, n∞. finp(σ) → n∞ < # σ ∨ n∞ = # σ;
       . from . : stream('a) × nat → stream('a) prio 8 left with λ σ, n. finp(σ) → ⌜n⌝  < # σ ∨ ⌜n⌝  = # σ;
       . to . : list('a) × nat → list('a) prio 8 left with λ x, n. n ≤ # x;
       . from . : list('a) × nat → list('a) prio 8 left with λ x, n. n ≤ # x;
   
   
   axioms 
      hd-fin: hd(⌜a + x⌝ ) = a;
      
      hd-inf: hd(⌜nf⌝ ) = nf(0);
      
      tl-fin: tl(⌜a + x⌝ ) = ⌜x⌝ ;
      
      tl-inf: tl(⌜nf⌝ ) = ⌜λ n. nf(n +1)⌝ ;
      
      prefix-def: σ ⊑ σ0 ↔ (∃ σ1. σ + σ1 = σ0);
      
      sel-fin: ⌜x⌝ [n] = x[n];
      used for: s, ls;
      
      sel-inf: ⌜nf⌝ [n] = nf(n);
      used for: s, ls;
      
      modify-fin: ⌜x⌝ [n := a] = ⌜x[n := a]⌝ ;
      used for: s, ls;
      
      modify-inf: ⌜nf⌝ [n := a] = ⌜λ m. (m = n ⊃ a;nf(m))⌝ ;
      
      empty: ⌜[]⌝  = [];
      used for: ls, s;
      
      cons-fin: ⌜a + x⌝  = a + ⌜x⌝ ;
      used for: s, ls;
      
      cons-inf: a + ⌜nf⌝  = ⌜λ n. (n = 0 ⊃ a;nf(n -1))⌝ ;
      
      append-finfin: ⌜x + y⌝  = ⌜x⌝  + ⌜y⌝ ;
      used for: s, ls;
      
      append-fininf: ⌜x⌝  + ⌜nf⌝  = ⌜λ n. (n < # x ⊃ x[n];nf(n - # x))⌝ ;
      
      append-inf: ⌜nf⌝  + σ = ⌜nf⌝ ;
      used for: s, ls;
      
      size-fin: # ⌜x⌝  = ⌜# x⌝ ;
      used for: s, ls;
      
      size-inf: # ⌜nf⌝  = ∞;
      used for: s, ls;
      
      to-fin: ⌜x⌝  to n = x to n;
      used for: s, ls;
      
      to-inf: ⌜nf⌝  to n = nf to n;
      used for: s, ls;
      
      from-fin: ⌜x⌝  from n = ⌜x from n⌝ ;
      used for: s, ls;
      
      from-inf: ⌜nf⌝  from n = ⌜nf from n⌝ ;
      used for: s, ls;
      
      to-zero-nf: nf to 0 = [];
      used for: s, ls;
      
      to-succ-nf: nf to n + 1 = nf(0) + ((λ n. nf(n + 1)) to n);
      
      from-nf: nf from n = (λ m. nf(n + m));
      
      from-zero-l: x from 0 = x;
      used for: s, ls;
      
      from-succ-cons-l: a + x from n + 1 = x from n;
      used for: s, ls;
      
      to-zero-l: x to 0 = [];
      used for: s, ls;
      
      to-succ-cons-l: a + x to n + 1 = a + (x to n);
      used for: s, ls;
      
      toinf-fin: σ to∞ ⌜n⌝  = ⌜σ to n⌝ ;
      used for: s, ls;
      
      toinf-inf: σ to∞ ∞ = σ;
      used for: s, ls;
   
   
end enrich