enrich
   IOrefine-conds, 
   IOrefine-def, 
   min-of-Pnat, 
   Koenigs-Lemma-gen
with
   variables 
       r : 'as × 'cs → Bool;
       t : 'cs × 'as → Bool;
       rbc : 'bs × 'cs → Bool;
       rab : 'as × 'bs → Bool;
       cal : List('ca);
       bal : List('ba);
       aal : List('aa);
       el : List('e);
       csf : Nat → 'cs;
       bsf : Nat → 'bs;
       asf : Nat → 'as;
       csl : List('cs);
       bsl : List('bs);
       asl : List('as);
       as : 'as;
       as' : 'as;
       bs : 'bs;
       cs : 'cs;
       cs' : 'cs;
       ca : 'ca;
       ba : 'ba;
       aa : 'aa;
       cα : Stream('aa);
       bα : Stream('ba);
       aα : Stream('aa);
       β : Stream('e);
       cσ : Stream('cs);
       bσ : Stream('bs);
       aσ : Stream('as);
       cstart : 'cs → Bool;
       bstart : 'bs → Bool;
       astart : 'as → Bool;
       cstep : 'cs × 'ca × 'cs → Bool;
       bstep : 'bs × 'ba × 'bs → Bool;
       astep : 'as × 'aa × 'as → Bool;
       cext : 'ca → Option('e);
       bext : 'ba → Option('e);
       aext : 'aa → Option('e);
       cioaut : IOAutomaton('cs, 'ca, 'e);
       bioaut : IOAutomaton('bs, 'ba, 'e);
       aioaut : IOAutomaton('as, 'aa, 'e);
       size01f : 'cs × 'ca × 'cs × 'as → Nat;
       aabs : 'ca → Option('aa);
       aINV : 'as → Bool;
       cINV : 'cs → Bool;
       ass : Set('as);
       caf : Nat → 'ca;
       aaf : Nat → 'aa;
       asn : ('as, Nat);
       asn-s : Set(('as, Nat));
       asnf : Nat → ('as, Nat);
       n : Nat;
   
   
   theorems 
      branchingfw-normedfw: ≤bF(cioaut, aioaut) ⊦ ≤nF(cioaut, aioaut);
      
      branchinfw-fw: ≤bF(cioaut, aioaut) ⊦ ≤F(cioaut, aioaut);
      
      normedfw-branchingfw: ≤nF(cioaut, aioaut) ⊦ ≤bF(cioaut, aioaut);
      
      forward-implies-leqrefine: ≤F(cioaut, aioaut) ⊦ C_≤T_A(cioaut, aioaut);
      
      bwtrueinv: ≤B(cioaut, aioaut) ⊦ ≤BI(cioaut, aioaut);
      
      bwinv-leqstar: ≤BI(cioaut, aioaut) ⊦ C_≤*T_A(cioaut, aioaut);
      
      bw-leqstar: ≤B(cioaut, aioaut) ⊦ C_≤*T_A(cioaut, aioaut);
      
      wbw-leqstar: ≤wB(cioaut, aioaut) ⊦ C_≤*T_A(cioaut, aioaut);
      
      imfiniobackwardinv-implies-leqrefine: ≤iBI(cioaut, aioaut) ⊦ C_≤T_A(cioaut, aioaut);
   
   
end enrich