enrich
   IO-Automaton, 
   funops
with
   functions 
       Π : ('ls → Bool) × ('rs → Bool) → ('ls, 'rs) → Bool;
      comment: initial states of the product.;
       Π
      : ('ls × 'la × 'ls → Bool) × ('rs × 'ra × 'rs → Bool) × ('la → 'pa) × ('ra → 'pa) × ('la → Option('e)) × ('ra → Option('e))
        → ('ls, 'rs) × 'pa × ('ls, 'rs) → Bool
      ;
      comment: step relation of the product.;
       Π : ('la → Option('e)) × ('ra → Option('e)) × ('la → 'pa) × ('ra → 'pa) → 'pa → Option('e);
      comment: external actions of the product.;
       Πh : ('la → Option('e)) × ('ra → Option('e)) × ('la → 'pa) × ('ra → 'pa) × ('e → Option('f)) → 'pa → Option('f);
      comment: external actions of the product hiding shared actions.;
   
   predicates 
       Πok : ('la → Option('e)) × ('ra → Option('e)) × ('la → 'pa) × ('ra → 'pa);
       Πhok : ('la → Option('e)) × ('ra → Option('e)) × ('la → 'pa) × ('ra → 'pa) × ('e → Option('f));
       sharingok : ('la → Option('e)) × ('ra → Option('e)) × ('la → 'pa) × ('ra → 'pa);
       hidingok : ('la → Option('e)) × ('ra → Option('e)) × ('la → 'pa) × ('ra → 'pa) × ('e → Option('f));
      comment: check for correct renaming of actions to product actions;
       surj : ('la → 'pa) × ('ra → 'pa);
   
   variables 
       pa : 'pa;
       ra : 'ra;
       la : 'la;
       ps : ('ls, 'rs);
       ls : 'ls;
       rs : 'rs;
       a : 'a;
       e : 'e;
       ren : 'a → 'b;
      comment: embedding of actions of L into actions of L x R;
       lren : 'la → 'pa;
       rren : 'ra → 'pa;
       lstep : 'ls × 'la × 'ls → Bool;
       rstep : 'rs × 'ra × 'rs → Bool;
      comment: embedding of actions of L into actions of L x R;
       pstep : ('ls × 'la × 'ls → Bool) × ('rs × 'ra × 'rs → Bool) → ('ls, 'rs) × 'pa × ('ls, 'rs) → Bool;
      comment: step of the product L X R;
       lstart : 'ls → Bool;
       rstart : 'rs → Bool;
       pstart : ('ls, 'rs) → Bool;
      comment: initialisation of the product S x C;
       lext : 'la → Option('e);
       rext : 'ra → Option('e);
       pext : 'pa → Option('e);
       lioaut : IOAutomaton('ls, 'la, 'e);
       rioaut : IOAutomaton('rs, 'ra, 'e);
       pioaut : IOAutomaton(('ls, 'rs), 'pa, 'e);
       hideext : 'e → Option('f);
      comment: reduces external actions to the subset of unshared external actions in Πh;
   
   partial functions 
       Π
      : IOAutomaton('ls, 'la, 'e) × IOAutomaton('rs, 'ra, 'e) × ('la → 'pa) × ('ra → 'pa) → IOAutomaton(('ls, 'rs), 'pa, 'e)
      with λ lioaut, rioaut, lren, rren. Πok(lioaut.ext, rioaut.ext, lren, rren)
      ;
      comment: product of two automata. Two renamings are given that embed the actions 'la and 'ra into the actions 'pa of the product;
       Πh
      : IOAutomaton('ls, 'la, 'e) × IOAutomaton('rs, 'ra, 'e) × ('la → 'pa) × ('ra → 'pa) × ('e → Option('f)) → IOAutomaton(('ls, 'rs), 'pa, 'f)
      with λ lioaut, rioaut, lren, rren, hideext. Πhok(lioaut.ext, rioaut.ext, lren, rren, hideext)
      ;
      comment: product of two automata hiding shared actions.;
   
   
   axioms 
      product-def: 
        Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren)
      = IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Π(lext, rext, lren, rren));
      used for: ls;
      
      hidingproduct-def: 
        Πh(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren, hideext)
      = IOAut(Π(lstart, rstart), Π(lstep, rstep, lren, rren, lext, rext), Πh(lext, rext, lren, rren, hideext));
      used for: ls;
      
      lrstep-def: 
        Π(lstep, rstep, lren, rren, lext, rext)((ls, rs), pa, (ls0, rs0))
      ↔   rs = rs0 ∧ (∃ la. lstep(ls, la, ls0) ∧ pa = lren(la) ∧ ¬ cod(rren)(pa))
        ∨ ls = ls0 ∧ (∃ ra. rstep(rs, ra, rs0) ∧ pa = rren(ra) ∧ ¬ cod(lren)(pa))
        ∨ (∃ la, ra. lstep(ls, la, ls0) ∧ lext(la) ≠ None ∧ pa = lren(la) ∧ rstep(rs, ra, rs0) ∧ rext(ra) ≠ None ∧ pa = rren(ra));
      used for: ls;
      comment: steps are either steps of left or right for unshared actions or combined external steps.;
      
      lrstart-def: Π(lstart, rstart)((ls, rs)) ↔ lstart(ls) ∧ rstart(rs);
      used for: s, ls;
      
      lrext-def-left: Πok(lext, rext, lren, rren) → Π(lext, rext, lren, rren)(lren(la)) = lext(la);
      used for: s, ls;
      comment: Πok must be assumed to avoid an inconsinstent definition when lren(la) = rren(ra);
      
      lrext-def-right: Πok(lext, rext, lren, rren) → Π(lext, rext, lren, rren)(rren(ra)) = rext(ra);
      used for: s, ls;
      
      lrexth-def-left: Πhok(lext, rext, lren, rren, hideext) → Πh(lext, rext, lren, rren, hideext)(lren(la)) = ((hideext o lext))(la);
      used for: s, ls;
      comment: shared actions are not exported;
      
      lrexth-def-right: Πhok(lext, rext, lren, rren, hideext) → Πh(lext, rext, lren, rren, hideext)(rren(ra)) = ((hideext o rext))(ra);
      used for: s, ls;
      comment: shared actions are not exported;
      
      surj-def: surj(lren, rren) ↔ (∀ pa. (∃ la. pa = lren(la)) ∨ (∃ ra. pa = rren(ra)));
      comment: all actions of the product are reached.;
      
      sharingok-def: 
        sharingok(lext, rext, lren, rren)
      ↔ (∀ la, ra. 
             (lren(la) = rren(ra) → lext(la) ≠ None ∧ rext(ra) ≠ None ∧ lext(la) = rext(ra))
           ∧ (¬ cod(rren)(lren(la)) ∧ ¬ cod(lren)(rren(ra)) ∧ lext(la) ≠ None ∧ rext(ra) ≠ None → lext(la) ≠ rext(ra)));
      comment: shared actions must be mapped to the same external action.
         unshared actions are never mapped to the same external one.;
      
      productok-def: Πok(lext, rext, lren, rren) ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren);
      used for: ls;
      comment: all product action must be in the image of injective renamings lren and rren, internal actions cannot be shared.;
      
      hidingproductok-def: 
        Πhok(lext, rext, lren, rren, hideext)
      ↔ inj(lren) ∧ inj(rren) ∧ surj(lren, rren) ∧ sharingok(lext, rext, lren, rren) ∧ hidingok(lext, rext, lren, rren, hideext);
      used for: ls;
      comment: all product action must be in the image of injective renamings lren and rren, internal actions cannot be shared.;
      
      hidingok-def: 
        hidingok(lext, rext, lren, rren, hideext)
      ↔ oinj(hideext) ∧ osurj(hideext) ∧ (∀ e. hideext(e) = None ↔ (∃ la, ra. lren(la) = rren(ra) ∧ Some(e) = lext(la) ∧ Some(e) = rext(ra)));
      used for: ls;
      comment: mapping from 'e to 'f hides hides precisely the shared actions. Is bijective on the rest.;
   
   theorems 
      PCIOAut: 
        IOAut?(IOAut(lstart, lstep, lext)) ∧ IOAut?(IOAut(rstart, rstep, rext)) ∧ Πok(lext, rext, lren, rren)
      → IOAut?(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren));
      used for: ss, lss;
      
      PhIOAut: 
        IOAut?(IOAut(lstart, lstep, lext)) ∧ IOAut?(IOAut(rstart, rstep, rext)) ∧ Πhok(lext, rext, lren, rren, hideext)
      → IOAut?(Πh(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren, hideext));
      used for: ss, lss;
   
   
end enrich