enrich
   IOtrace
with
   predicates 
       ≤BI : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e);
       bwsim : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('cs × 'as → Bool) × ('cs → Bool) × ('as → Bool);
       ≤B : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e);
       bwsim : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('cs × 'as → Bool);
       ≤wB : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e);
       weakbwsim : IOAutomaton('cs, 'ca, 'e) × IOAutomaton('as, 'aa, 'e) × ('cs × 'as → Bool) × ('as → Bool);
   
   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);
   
   
   axioms 
      backwardsim-def: ≤B(cioaut, aioaut) ↔ (∃ t. bwsim(cioaut, aioaut, t));
      
      proofobls-backwardsim: 
        bwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t)
      ↔   (∀ cs. ∃ as. t(cs, as)) ∧ (∀ cs, as. cstart(cs) ∧ t(cs, as) → astart(as))
        ∧ (∀ cs, ca, cs0, as0. cstep(cs, ca, cs0) ∧ t(cs0, as0) → (∃ as. move(IOAut(astart, astep, aext))(as, cext !(ca '), as0) ∧ t(cs, as)));
      
      backwardsiminv-def: ≤BI(cioaut, aioaut) ↔ (∃ t, aINV, cINV. bwsim(cioaut, aioaut, t, cINV, aINV));
      
      proofobls-backwardsiminv: 
        bwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, cINV, aINV)
      ↔   (∀ cs. cstart(cs) → cINV(cs)) ∧ (∀ as. astart(as) → aINV(as)) ∧ (∀ cs, ca, cs0. cINV(cs) ∧ cstep(cs, ca, cs0) → cINV(cs0))
        ∧ (∀ as, aa, as0. aINV(as) ∧ astep(as, aa, as0) → aINV(as0)) ∧ (∀ cs. cINV(cs) → (∃ as. t(cs, as) ∧ aINV(as)))
        ∧ (∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as))
        ∧ (∀ cs, ca, cs0, as0. 
               cINV(cs) ∧ cstep(cs, ca, cs0) ∧ t(cs0, as0) ∧ aINV(as0)
             → (∃ as. aINV(as) ∧ move(IOAut(astart, astep, aext))(as, cext !(ca '), as0) ∧ t(cs, as)));
      
      weakbackwardsim-def: ≤wB(cioaut, aioaut) ↔ (∃ t, aINV. weakbwsim(cioaut, aioaut, t, aINV));
      
      proofobls-weakbackwardsim: 
        weakbwsim(IOAut(cstart, cstep, cext), IOAut(astart, astep, aext), t, aINV)
      ↔   (∀ csl, cal. exec*(IOAut(cstart, cstep, cext))(csl, cal) → (∃ as. t(csl.last, as) ∧ aINV(as)))
        ∧ (∀ cs, as. cstart(cs) ∧ t(cs, as) ∧ aINV(as) → astart(as)) ∧ (∀ asl, aal. exec*(IOAut(astart, astep, aext))(asl, aal) → aINV(asl.last))
        ∧ (∀ csl, cal, ca, cs0, as0. 
               exec*(IOAut(cstart, cstep, cext))(csl, cal) ∧ cstep(csl.last, ca, cs0) ∧ t(cs0, as0) ∧ aINV(as0)
             → (∃ as. aINV(as) ∧ move(IOAut(astart, astep, aext))(as, cext !(ca '), as0) ∧ t(csl.last, as)));
   
   
end enrich