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