[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,

Specification weakfin-startfin-IObackward-INV-is-leqrefine
enrich
   IObackward-INV-is-leqstarrefine
, 
   Koenigs-Lemma-gen, 
   IOrefine-def, 
   set-union
with
   variables 
       cioaut : IOAutomaton('cs, 'ca, 'e);
       aioaut : IOAutomaton('as, 'aa, 'e);
       t : 'cs × 'as → 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;
       caf : Nat → 'ca;
       aaf : Nat → 'aa;
       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);
       ass : Set('as);
       β : Stream('e);
       asn : ('as, Nat);
       n : Nat;
       asnf : Nat → ('as, Nat);
       aINV : 'as → Bool;
       cINV : 'cs → Bool;
       ef : Nat → 'e;
       asn-s : Set(('as, Nat));
   
   
   
end enrich