enrich
   product, 
   IOtrace-lift, 
   streamseq-mon-lim

with
   functions 
       πrs : ('ls × 'la × 'ls → Bool) × ('rs × 'ra × 'rs → Bool) × ('la → 'pa) × ('ra → 'pa) × Stream(('ls, 'rs)) × Stream('pa) → Stream('rs);
       πra : ('ls × 'la × 'ls → Bool) × ('rs × 'ra × 'rs → Bool) × ('la → 'pa) × ('ra → 'pa) × Stream(('ls, 'rs)) × Stream('pa) → Stream('ra);
       πrs : ('ls × 'la × 'ls → Bool) × ('rs × 'ra × 'rs → Bool) × ('la → 'pa) × ('ra → 'pa) × List(('ls, 'rs)) × List('pa) → List('rs);
       πra : ('ls × 'la × 'ls → Bool) × ('rs × 'ra × 'rs → Bool) × ('la → 'pa) × ('ra → 'pa) × List(('ls, 'rs)) × List('pa) → List('ra);
       fu : ('la → 'pa) × ('ra → 'pa) → 'pa → Option('pa);
      comment: filters unshared actions: Some(a) for an unshared action, None otherwise;
   
   variables 
       ps : ('ls, 'rs);
       pa : 'pa;
       la : 'la;
       ra : 'ra;
       ls : 'ls;
       rs : 'rs;
       psl : List(('ls, 'rs));
       pσ : Stream(('ls, 'rs));
       lsl : List('ls);
       lσ : Stream('ls);
       rsl : List('rs);
       rσ : Stream('rs);
       pal : List('pa);
       pα : Stream('pa);
       lal : List('la);
       lα : Stream('la);
       ral : List('ra);
       rα : Stream('ra);
       laf : Nat → 'la;
       e : 'e;
       el : List('e);
       ef : Nat → 'e;
       β : Stream('e);
       raf : Nat → 'ra;
       paf : Nat → 'pa;
       lsf : Nat → 'ls;
       rsf : Nat → 'rs;
       psf : Nat → ('ls, 'rs);
       lstart : 'ls → Bool;
       rstart : 'rs → Bool;
       lstep : 'ls × 'la × 'ls → Bool;
       rstep : 'rs × 'ra × 'rs → Bool;
       lext : 'la → Option('e);
       rext : 'ra → Option('e);
       lren : 'la → 'pa;
       rren : 'ra → 'pa;
       n : Nat;
       hideext : 'e → Option('f);
   
   
   axioms 
      fu-def: fu(lren, rren)(pa) = (cod(lren)(pa) ∧ cod(rren)(pa) ⊃ None;Some(pa));
      
      projstate-fin-def: # psl = # pal + 1 → πrs(lstep, rstep, lren, rren, ⌜psl⌝ , ⌜pal⌝ ) = ⌜πrs(lstep, rstep, lren, rren, psl, pal)⌝ ;
      
      projstate-inf-def: πrs(lstep, rstep, lren, rren, ⌜psf⌝ , ⌜paf⌝ ) = lim(⌜λ n. ⌜πrs(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ );
      
      projaction-fin-def: # psl = # pal + 1 → πra(lstep, rstep, lren, rren, ⌜psl⌝ , ⌜pal⌝ ) = ⌜πra(lstep, rstep, lren, rren, psl, pal)⌝ ;
      
      projaction-inf-def: πra(lstep, rstep, lren, rren, ⌜psf⌝ , ⌜paf⌝ ) = lim(⌜λ n. ⌜πra(lstep, rstep, lren, rren, psf.take(n + 1), paf.take(n))⌝ ⌝ );
      
      projstate-base: πrs(lstep, rstep, lren, rren, (ls, rs) ', []) = rs ';
      used for: s, ls;
      
      projaction-base: πra(lstep, rstep, lren, rren, (ls, rs) ', []) = [];
      used for: s, ls;
      
      projstate-rec-addR: 
        # psl = # pal ∧ rstep(rs, ra, rs0) ∧ ¬ cod(lren)(rren(ra))
      → πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls, rs0) ' + psl, rren(ra) ' + pal) = rs ' + πrs(lstep, rstep, lren, rren, (ls, rs0) ' + psl, pal);
      used for: s, ls;
      
      projaction-rec-addR: 
        # psl = # pal ∧ rstep(rs, ra, rs0) ∧ ¬ cod(lren)(rren(ra))
      → πra(lstep, rstep, lren, rren, (ls, rs) ' + (ls, rs0) ' + psl, rren(ra) ' + pal) = ra + πra(lstep, rstep, lren, rren, (ls, rs0) + psl, pal);
      used for: s, ls;
      
      projstate-rec-addboth: 
      pa = lren(la)
      ⊦   # psl = # pal ∧ rstep(rs, ra, rs0) ∧ rren(ra) = lren(la) ∧ lstep(ls, la, ls0)
        → πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs0) ' + psl, pa ' + pal) = rs ' + πrs(lstep, rstep, lren, rren, (ls0, rs0) ' + psl, pal);
      used for: s, ls;
      
      projaction-rec-addboth: 
      pa = lren(la)
      ⊦   # psl = # pal ∧ rstep(rs, ra, rs0) ∧ rren(ra) = lren(la) ∧ lstep(ls, la, ls0)
        → πra(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs0) ' + psl, pa ' + pal) = ra + πra(lstep, rstep, lren, rren, (ls0, rs0) ' + psl, pal);
      used for: s, ls;
      
      projstate-rec-skipL: 
        # psl = # pal ∧ lstep(ls, la, ls0) ∧ ¬ cod(rren)(lren(la))
      → πrs(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs) ' + psl, lren(la) ' + pal) = πrs(lstep, rstep, lren, rren, (ls0, rs) ' + psl, pal);
      used for: s, ls;
      
      projaction-rec-skipL: 
        # psl = # pal ∧ lstep(ls, la, ls0) ∧ ¬ cod(rren)(lren(la))
      → πra(lstep, rstep, lren, rren, (ls, rs) ' + (ls0, rs) ' + psl, lren(la) ' + pal) = πra(lstep, rstep, lren, rren, (ls0, rs) ' + psl, pal);
      used for: s, ls;
   
   theorems 
      proj-exec: 
      IOAut?(IOAut(lstart, lstep, lext)), IOAut?(IOAut(rstart, rstep, rext)), Πok(lext, rext, lren, rren), 
      exec(Π(IOAut(lstart, lstep, lext), IOAut(rstart, rstep, rext), lren, rren))(pσ, pα)
      ⊦ exec(IOAut(rstart, rstep, rext))(πrs(lstep, rstep, lren, rren, pσ, pα), πra(lstep, rstep, lren, rren, pσ, pα));
   
   
end enrich