Specification IOtrace-lift

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

enrich
   IOtrace, 
   remtau-cont
with
   variables 
       σ : Stream('s);
       α : Stream('a);
       s : 's;
       a : 'a;
       sl : List('s);
       al : List('a);
       sf : Nat → 's;
       af : Nat → 'a;
       ioa : IOAutomaton('s, 'a, 'e);
       β : Stream('e);
       el : List('e);
       ef : Nat → 'e;
       e : 'e;
       start : 's → Bool;
       step : 's × 'a × 's → Bool;
       ext : 'a → Option('e);
   
   
   theorems 
      frag-is-lift-fragstar: lift(frag*(ioa)) = frag(ioa);
      
      exec-is-lift-execstar: lift(exec*(ioa)) = exec(ioa);
      
      pfxclosed-trace: pfxclosed(trace(ioa));
      
      pfxclosed-tracestar: pfxclosed(trace*(ioa));
      
      pfxclosed-frag: pfxclosed(frag(ioa));
      
      pfxclosed-fragstar: pfxclosed(frag*(ioa));
      
      pfxclosed-exec: pfxclosed(exec(ioa));
      
      pfxclosed-execstar: pfxclosed(exec*(ioa));
   
   
end enrich