actualize
   stream
with
   stream
   
by morphism
   :Elem → Stream; 
   :Stream → Streamstream; 
   :List → Streamlist; 
   [] : List → [] : Streamlist; 
   [] : Stream → [] : Streamstream; 
    . +2 .  →  . +l . ; 
    . + .  : (Elem × List → List) →  . + .  : (Stream × Streamlist → Streamlist); 
   # .  : (List → Nat) → # .  : (Streamlist → Nat); 
    . ' →  . ' : (Stream → Streamlist); 
    . + .  : (List × List → List) →  . + .  : (Streamlist × Streamlist → Streamlist); 
    . + .  : (List × Elem → List) →  . + .  : (Streamlist × Stream → Streamlist); 
    . ++ .  →  . ++ .  : (Streamlist × Stream → Streamlist); 
   rmdup → rmdup : (Streamlist → Streamlist); 
   rev → rev : (Streamlist → Streamlist); 
   mklist → mklist : (Stream × Nat → Streamlist); 
   fillfirst → fillfirst : (Nat × Stream × Streamlist → Streamlist); 
    . -l .  →  . -l .  : (Streamlist × Stream → Streamlist); 
    . -1l .  →  . -1l .  : (Streamlist × Stream → Streamlist); 
    . -p .  →  . -p .  : (Streamlist × Nat → Streamlist); 
   pos → pos : (Stream × Streamlist → Nat); 
   frome → frome : (Streamlist × Stream → Streamlist); 
   ⌜ . ⌝ : (List → Stream) → ⌜ . ⌝ : (Streamlist → Streamstream); 
   ⌜ . ⌝ : ((Nat → Elem) → Stream) → ⌜ . ⌝ : ((Nat → Stream) → Streamstream); 
    . + .  : (Elem × Stream → Stream) →  . + .  : (Stream × Streamstream → Streamstream); 
    . + .  : (Stream × Stream → Stream) →  . + .  : (Streamstream × Streamstream → Streamstream); 
   # .  : (Stream → Natinf) → # .  : (Streamstream → Natinf); 
    . to .  : ((Nat → Elem) × Nat → List) →  . to .  : ((Nat → Stream) × Nat → Streamlist); 
    . from .  : ((Nat → Elem) × Nat → Nat -> Elem) →  . from .  : ((Nat → Stream) × Nat → Nat -> Stream); 
    . < .  : (List × List → Bool) →  . < .  : (Streamlist × Streamlist → Bool); 
    . ∈ .  →  . ∈ .  : (Stream × Streamlist → Bool); 
   dups → dups : (Streamlist → Bool); 
   disj → disj : (Streamlist × Streamlist → Bool); 
    . ⊑ .  : (List × List → Bool) →  . ⊑ .  : (Streamlist × Streamlist → Bool); 
    . ⊒ .  →  . ⊒ .  : (Streamlist × Streamlist → Bool); 
   finp → finp : (Streamstream → Bool); 
    . ⊑ .  : (Stream × Stream → Bool) →  . ⊑ .  : (Streamstream × Streamstream → Bool); 
    . head →  . head : (Streamlist → Stream); 
    . tail →  . tail : (Streamlist → Streamlist); 
    . last →  . last : (Streamlist → Stream); 
    . butlast →  . butlast : (Streamlist → Streamlist); 
   butlastn → butlastn : (Nat × Streamlist → Streamlist); 
    . ( . ) : (List × Nat → Elem)  →  . ( . ) : (Streamlist × Nat → Stream) ; 
    . (. := .) : (List × Nat × Elem → List)  →  . (. := .) : (Streamlist × Nat × Stream → Streamlist) ; 
   firstn → firstn : (Nat × Streamlist → Streamlist); 
   restn → restn : (Nat × Streamlist → Streamlist); 
   lastn → lastn : (Nat × Streamlist → Streamlist); 
   sublist → sublist : (Nat × Nat × Streamlist → Streamlist); 
    . l →  . l : (Streamstream → Streamlist); 
    . f →  . f : (Streamstream → Nat -> Stream); 
   hd → hd : (Streamstream → Stream); 
   tl → tl : (Streamstream → Streamstream); 
    . ( . ) : (Stream × Nat → Elem)  →  . ( . ) : (Streamstream × Nat → Stream) ; 
    . (. := .) : (Stream × Nat × Elem → Stream)  →  . (. := .) : (Streamstream × Nat × Stream → Streamstream) ; 
    . to .  : (Stream × Nat → Stream) →  . to .  : (Streamstream × Nat → Streamstream); 
    . to∞ .  →  . to∞ .  : (Streamstream × Natinf → Streamstream); 
    . from .  : (Stream × Nat → Stream) →  . from .  : (Streamstream × Nat → Streamstream); 
    . to .  : (List × Nat → List) →  . to .  : (Streamlist × Nat → Streamlist); 
    . from .  : (List × Nat → List) →  . from .  : (Streamlist × Nat → Streamlist); 
end actualize