Specification IObackward-INV-is-leqstarrefine

[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
   IObackward-INV, 
   IOrefine-def
with
   variables 
       cioaut : IOAutomaton('cs, 'ca, 'e);
       aioaut : IOAutomaton('as, 'aa, 'e);
       t : 'cs × 'as → Bool;
       aINV : 'as → Bool;
       cINV : 'cs → Bool;
       cstart : 'cs → Bool;
       astart : 'as → Bool;
       astep : 'as × 'aa × 'as → Bool;
       cstep : 'cs × 'ca × 'cs → Bool;
       cext : 'ca → Option('e);
       aext : 'aa → Option('e);
       cs : 'cs;
       as : 'as;
       csf : Nat → 'cs;
       asf : Nat → 'as;
       cal : List('ca);
       cα : Stream('ca);
       aal : List('aa);
       aα : Stream('aa);
       asl : List('as);
       csl : List('cs);
       ca : 'ca;
       aa : 'aa;
       cσ : Stream('cs);
       aσ : Stream('as);
       el : List('e);
   
   
   
end enrich