enrich
   stream-basic, 
   nat-inf
with
   constants 
       [] : Stream[A];
   
   functions 
       . + . : A × Stream[A] → Stream[A];
       . + . : Stream[A] × Stream[A] → Stream[A];
       . + . : List[A] × (Nat → A) → Nat → A;
       # . : Stream[A] → Natinf;
       . take ( . ) : (Nat → A) × Nat → List[A];
       . drop ( . ) : (Nat → A) × Nat → Nat → A;
   
   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⌝  < # σ;
       . take ( . ) : Stream[A] × Nat → List[A] with λ σ, n. finp(σ) → ⌜n⌝  < # σ ∨ ⌜n⌝  = # σ;
       . take ( . ) : Stream[A] × Natinf → Stream[A] with λ σ, n∞. finp(σ) → n∞ < # σ ∨ n∞ = # σ;
       . drop ( . ) : Stream[A] × Nat → Stream[A] with λ σ, n. finp(σ) → ⌜n⌝  < # σ ∨ ⌜n⌝  = # σ;
   
   axioms 
      add-list-fun-def: x + nf = (λ n. (n < # x ⊃ x(n);nf(n - # x)));
      
      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⌝ .take(n) = x.take(n);
      used for: s, ls;
      
      to-inf: ⌜nf⌝ .take(n) = nf.take(n);
      used for: s, ls;
      
      from-fin: ⌜x⌝ .drop(n) = ⌜x.drop(n)⌝ ;
      used for: s, ls;
      
      from-inf: ⌜nf⌝ .drop(n) = ⌜nf.drop(n)⌝ ;
      used for: s, ls;
      
      to-zero-nf: nf.take(0) = [];
      used for: s, ls;
      
      to-succ-nf: nf.take(n + 1) = nf(0) + (λ n. nf(n + 1)).take(n);
      
      from-nf: nf.drop(n) = (λ m. nf(n + m));
      
      toinf-fin: σ.take(⌜n⌝ ) = ⌜σ.take(n)⌝ ;
      used for: s, ls;
      
      toinf-inf: σ.take(∞) = σ;
      used for: s, ls;
   
   
end enrich