enrich
   remtau, 
   IO-Automaton, 
   infinite-append

with
   functions 
       trace* : IOAutomaton('s, 'a, 'e) → List('e) → Bool;
       traceω : IOAutomaton('s, 'a, 'e) → (Nat → 'e) → Bool;
       trace : IOAutomaton('s, 'a, 'e) → Stream('e) → Bool;
       frag* : IOAutomaton('s, 'a, 'e) → List('s) × List('a) → Bool;
       fragω : IOAutomaton('s, 'a, 'e) → (Nat → 's) × (Nat → 'a) → Bool;
       frag : IOAutomaton('s, 'a, 'e) → Stream('s) × Stream('a) → Bool;
       exec* : IOAutomaton('s, 'a, 'e) → List('s) × List('a) → Bool;
       execω : IOAutomaton('s, 'a, 'e) → (Nat → 's) × (Nat → 'a) → Bool;
       exec : IOAutomaton('s, 'a, 'e) → Stream('s) × Stream('a) → Bool;
       move : IOAutomaton('s, 'a, 'e) → 's × List('e) × 's → Bool;
   
   variables 
       ioa : IOAutomaton('s, 'a, 'e);
       movev : 's × Stream('e) × 's → Bool;
       fragv : Stream('s) × Stream('a) → Bool;
       tracev : Stream('e) → Bool;
       iNV : 's → Bool;
       sl : List('s);
       al : List('a);
       α : Stream('a);
       β : Stream('e);
       el : List('e);
       ef : Nat → 'e;
       σ : Stream('s);
       af : Nat → 'a;
       sf : Nat → 's;
       start : 's → Bool;
       step : 's × 'a × 's → Bool;
       ext : 'a → Option('e);
       s : 's;
       a : 'a;
       e : 'e;
       oe : Option('e);
       n : Nat;
       m : Nat;
       slf : Nat → List('s);
       alf : Nat → List('a);
       ii : Nat → Nat;
   
   
   axioms 
      move: move(ioa)(s1, el, s2) ↔ (∃ al, sl. frag*(ioa)(sl, al) ∧ s1 = sl[0] ∧ s2 = sl.last ∧ ioa.ext !(al) = el);
      
      frag: frag(IOAut(start, step, ext))(σ, α) ↔ # σ = # α + ⌜1⌝  ∧ (∀ n. ⌜n⌝  < # α → step(σ[n], α[n], σ[n +1]));
      
      fragstar-def: frag(ioa)(⌜sl⌝ , ⌜al⌝ ) ↔ frag*(ioa)(sl, al);
      used for: s, ls;
      
      fragomega-def: frag(ioa)(⌜sf⌝ , ⌜af⌝ ) ↔ fragω(ioa)(sf, af);
      used for: s, ls;
      
      exec: exec(ioa)(σ, α) ↔ frag(ioa)(σ, α) ∧ ioa.start(σ[0]);
      used for: s, ls;
      
      execstar: exec(ioa)(⌜sl⌝ , ⌜al⌝ ) ↔ exec*(ioa)(sl, al);
      used for: s, ls;
      
      execomega: exec(ioa)(⌜sf⌝ , ⌜af⌝ ) ↔ execω(ioa)(sf, af);
      used for: s, ls;
      
      trace: trace(IOAut(start, step, ext))(β) ↔ (∃ σ, α. β = ext !(α) ∧ exec(IOAut(start, step, ext))(σ, α));
      
      tracestar-def: trace(ioa)(⌜el⌝ ) ↔ trace*(ioa)(el);
      used for: s, ls;
      
      traceomega: trace(ioa)(⌜ef⌝ ) ↔ traceω(ioa)(ef);
      used for: s, ls;
   
   
end enrich