added harmony-lemma-formalization

case-studies/harmony-lemma-formalization/1_definitions.bel

@@ -0,0 +1,107 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%% Definitions %%%
+
+% Set of Channel Names
+LF names: type =
+;
+
+% Processes
+% In order to encode input and restriction processes, which both bind names, we exploit higher order abstract syntax
+% and use higher-order functions from names to proc.
+% In this way we don't need to give an explicit name to bound names and deal with alpha-renaming or substitution.
+LF proc: type =
+  | p_zero: proc                                % 0
+  | p_in: names → (names → proc) → proc         % x(y).P(y), where x(y) is an input of the name y through channel x
+  | p_out: names → names → proc → proc          % x(u).P, where x(u) is an output of the name u through channel x
+  | p_par: proc → proc → proc                   % P|Q, where P and Q are processes
+  | p_res: (names → proc) → proc                % (nu x) P, where x is a name and P is a process
+;
+--infix p_par 11 left.
+
+% Contexts
+schema ctx = names;
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%% Reduction Semantics %%%
+
+% Structural Congruence
+LF cong: proc → proc → type =
+% Abelian Monoid Laws for Parallel Composition
+  | par_assoc: cong (P p_par (Q p_par R)) ((P p_par Q) p_par R)
+  | par_unit: cong (P p_par p_zero) P
+  | par_comm: cong (P p_par Q) (Q p_par P)
+% Scope Extension Laws
+  | sc_ext_zero: cong (p_res \x.p_zero) p_zero
+  | sc_ext_par: cong ((p_res P) p_par Q) (p_res \x.((P x) p_par Q))
+  | sc_ext_res: cong (p_res \x.(p_res \y.(P x y))) (p_res \y.(p_res \x.(P x y)))
+% Compatibility Laws
+  | c_in: ({y:names} cong (P y) (Q y)) → cong (p_in X P) (p_in X Q)
+  | c_out: cong P Q → cong (p_out X Y P) (p_out X Y Q)
+  | c_par: cong P P' → cong (P p_par Q) (P' p_par Q)
+  | c_res: ({x:names} cong (P x) (Q x)) → cong (p_res P) (p_res Q)
+% Equivalence Relation Laws
+  | c_ref: cong P P
+  | c_sym: cong P Q → cong Q P
+  | c_trans: cong P Q → cong Q R → cong P R
+;
+--infix cong 11 left.
+
+% Reduction
+LF red: proc → proc → type =
+  | r_com: red ((p_out X Y P) p_par (p_in X Q)) (P p_par (Q Y))
+  | r_par: red P Q → red (P p_par R) (Q p_par R)
+  | r_res: ({x:names} red (P x) (Q x)) → red (p_res P) (p_res Q)
+  | r_str: P cong P' → red P' Q' → Q' cong Q → red P Q
+;
+--infix red 11 left.
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%% LTS Semantics %%%
+% We follow "Pi-Calculus in (Co)Inductive Type Theory" [Honsell et al. 2001] for the encoding of late LTS semantics.
+% We define two different types for free/bound actions, and two different relations for transitions via free/bound actions.
+% The result of a free transition is a process, while the result of a bound transition is a function from names to processes:
+% instead of stating the bound name involved in the transition explicitly, that name is the argument of the aforementioned function.
+
+% Free Actions
+LF f_act: type =
+  | f_tau: f_act
+  | f_out: names → names → f_act
+;
+
+% Bound Actions
+LF b_act: type =
+  | b_in: names → b_act
+  | b_out: names → b_act
+;
+
+
+% Transition Relation
+LF fstep: proc → f_act → proc → type =
+  | fs_out: fstep (p_out X Y P) (f_out X Y) P
+  | fs_par1: fstep P A P' → fstep (P p_par Q) A (P' p_par Q)
+  | fs_par2: fstep Q A Q' → fstep (P p_par Q) A (P p_par Q')
+  | fs_com1: fstep P (f_out X Y) P' → bstep Q (b_in X) Q'
+    → fstep (P p_par Q) f_tau (P' p_par (Q' Y))
+  | fs_com2: bstep P (b_in X) P' → fstep Q (f_out X Y) Q'
+    → fstep (P p_par Q) f_tau ((P' Y) p_par Q')
+  | fs_res: ({z:names} fstep (P z) A (P' z))
+    → fstep (p_res P) A (p_res P')
+  | fs_close1: bstep P (b_out X) P' → bstep Q (b_in X) Q'
+    → fstep (P p_par Q) f_tau (p_res \z.((P' z) p_par (Q' z)))
+  | fs_close2: bstep P (b_in X) P' → bstep Q (b_out X) Q'
+    → fstep (P p_par Q) f_tau (p_res \z.((P' z) p_par (Q' z)))
+
+and bstep: proc → b_act → (names → proc) → type =
+  | bs_in: bstep (p_in X P) (b_in X) P
+  | bs_par1: bstep P A P' → bstep (P p_par Q) A \x.((P' x) p_par Q)
+  | bs_par2: bstep Q A Q' → bstep (P p_par Q) A \x.(P p_par (Q' x))
+  | bs_res: ({z:names} bstep (P z) A (P' z))
+    → bstep (p_res P) A \x.(p_res \z.(P' z x))
+  | bs_open: ({z:names} fstep (P z) (f_out X z) (P' z))
+    → bstep (p_res P) (b_out X) P'
+;

case-studies/harmony-lemma-formalization/2_input_rewriting.bel

@@ -0,0 +1,72 @@
+% Predicate about syntactic equivalence of processes involved in input transitions:
+% ex_inp_rew Q X Q' holds iff there exist R, S, x_1,...,x_n such that Q cong (nu x_1)...(nu x_n)((p_in X R) p_par S) and
+% (Q' y) cong (nu x_1)...(nu x_n)((R Y) p_par S).
+% We encode this type via two constructors: one representing the base case without restrictions, and one representing the inductive case
+% in which Q cong (nu x)P and Q' cong (nu x)P', where ex_inp_rew P X P' holds inductively.
+
+LF ex_inp_rew: proc → names → (names → proc) → type =
+  | inp_base: Q cong ((p_in X R) p_par S)
+    → ({y:names} (Q' y) cong ((R y) p_par S)) → ex_inp_rew Q X Q'
+  | inp_ind: Q cong (p_res P) → ({y:names} (Q' y) cong (p_res (P' y)))
+    → ({w:names} ex_inp_rew (P w) X \y.(P' y w)) → ex_inp_rew Q X Q'
+;
+
+
+% We prove the lemma which states that processes involved in input transitions (bstep Q (b_in X) Q')
+% can be rewritten (up to congruence) in a canonic way (ex_inp_rew Q X Q').
+% Before, we need three additional lemmas which prove the result in particular cases.
+
+rec bs_in_rew_par1: (g:ctx) {R:[g ⊢ proc]} [g ⊢ ex_inp_rew Q X \y.Q'[..,y]]
+  → [g ⊢ ex_inp_rew (Q p_par R) X \y.(Q'[..,y] p_par R[..])] =
+/ total d (bs_in_rew_par1 _ _ _ _ _ d) /
+mlam R ⇒ fn d ⇒ case d of
+   | [g ⊢ inp_base C1 \y.C2[..,y]] ⇒ [g ⊢ inp_base (c_trans (c_par C1)
+     (c_sym par_assoc)) \y.(c_trans (c_par C2[..,y]) (c_sym par_assoc))]
+   | [g ⊢ inp_ind C1 (\y.C2[..,y]) (\w.D1[..,w])] ⇒
+     let [g,w:names ⊢ D2[..,w]] = bs_in_rew_par1 [g,w:names ⊢ R[..]]
+     [g,w:names ⊢ D1[..,w]] in [g ⊢ inp_ind (c_trans (c_par C1)
+     sc_ext_par) (\y.(c_trans (c_par C2[..,y]) sc_ext_par)) (\w.D2[..,w])]
+;
+
+rec bs_in_rew_par2: (g:ctx) {R:[g ⊢ proc]} [g ⊢ ex_inp_rew Q X \y.Q'[..,y]]
+  → [g ⊢ ex_inp_rew (R p_par Q) X \y.(R[..] p_par Q'[..,y])] =
+/ total d (bs_in_rew_par2 _ _ _ _ _ d) /
+mlam R ⇒ fn d ⇒ case d of
+   | [g ⊢ inp_base C1 \y.C2[..,y]] ⇒
+     [g ⊢ inp_base (c_trans par_comm (c_trans (c_par C1) (c_sym par_assoc)))
+     \y.(c_trans par_comm (c_trans (c_par C2[..,y]) (c_sym par_assoc)))]
+   | [g ⊢ inp_ind C1 (\y.C2[..,y]) (\w.D1[..,w])] ⇒
+     let [g,w:names ⊢ D2[..,w]] = bs_in_rew_par2 [g,w:names ⊢ R[..]]
+     [g, w:names ⊢ D1[..,w]] in [g ⊢ inp_ind (c_trans par_comm (c_trans (c_par C1)
+     (c_trans sc_ext_par (c_res \z.par_comm)))) (\y.(c_trans par_comm (c_trans
+     (c_par C2[..,y]) (c_trans sc_ext_par (c_res \z.par_comm))))) (\w.D2[..,w])]
+;
+
+rec bs_in_rew_res: (g:ctx) [g,z:names ⊢ ex_inp_rew Q[..,z] X[..] \y.Q'[..,z,y]]
+  → [g ⊢ ex_inp_rew (p_res \z.Q[..,z]) X \y.(p_res \z.Q'[..,z,y])] =
+/ total d (bs_in_rew_res _ _ _ _ d) /
+fn d ⇒ case d of
+   | [g,z:names ⊢ inp_base C1[..,z] \y.C2[..,z,y]] ⇒
+     [g ⊢ inp_ind (c_res \z.C1[..,z]) (\y.(c_res \z.C2[..,z,y]))
+     (\w.(inp_base c_ref \y.c_ref))]
+   | [g,z:names ⊢ inp_ind C1[..,z] (\y.C2[..,z,y]) (\w.D1[..,z,w])] ⇒
+     let [g,z:names ⊢ D2[..,z]] = bs_in_rew_res [g,z:names,w:names ⊢ D1[..,z,w]] in
+     [g ⊢ inp_ind (c_res \z.C1[..,z]) (\y.(c_res \z.C2[..,z,y])) (\z.D2[..,z])]
+;
+
+
+rec bs_in_rew: (g:ctx) [g ⊢ bstep Q (b_in X) \y.Q'[..,y]]
+  → [g ⊢ ex_inp_rew Q X \y.Q'[..,y]] =
+/ total b (bs_in_rew _ _ _ _ b) /
+fn b ⇒ case b of
+   | [g ⊢ bs_in] ⇒ [g ⊢ inp_base (c_sym par_unit) \y.(c_sym par_unit)]
+   | [g ⊢ bs_par1 B1]:[g ⊢ bstep (P p_par R) (b_in X) \y.(P' p_par (R[..]))] ⇒
+     let [g ⊢ D1] = bs_in_rew [g ⊢ B1] in
+     let [g ⊢ D2] = bs_in_rew_par1 [g ⊢ R] [g ⊢ D1] in [g ⊢ D2]
+   | [g ⊢ bs_par2 B2]:[g ⊢ bstep (R p_par P) (b_in X) \y.((R[..]) p_par P')] ⇒
+     let [g ⊢ D1] = bs_in_rew [g ⊢ B2] in 
+     let [g ⊢ D2] = bs_in_rew_par2 [g ⊢ R] [g ⊢ D1] in [g ⊢ D2]
+   | [g ⊢ bs_res \y.B[..,y]] ⇒
+     let [g,y:names ⊢ D1[..,y]] = bs_in_rew [g,y:names ⊢ B[..,y]] in
+     let [g ⊢ D2] = bs_in_rew_res [g,y:names ⊢ D1[..,y]] in [g ⊢ D2]
+;

case-studies/harmony-lemma-formalization/3_free_output_rewriting.bel

@@ -0,0 +1,70 @@
+% Predicate about syntactic equivalence of processes involved in free output transitions:
+% ex_fout_rew Q X Y Q' holds iff there exist R, S, x_1,...,x_n such that Q cong (nu x_1)...(nu x_n)((p_out X Y R) p_par S) and
+% Q' cong (nu x_1)...(nu x_n)(R p_par S).
+% We encode this type via two constructors: one representing the base case without restrictions, and one representing the inductive case
+% in which Q cong (nu x)P and Q' cong (nu x)P', where ex_fout_rew P X P' holds inductively.
+
+LF ex_fout_rew: proc → names → names → proc → type =
+  | fout_base: Q cong ((p_out X Y R) p_par S) → Q' cong (R p_par S)
+    → ex_fout_rew Q X Y Q'
+  | fout_ind: Q cong (p_res P) → Q' cong (p_res P')
+    → ({w:names} ex_fout_rew (P w) X Y (P' w)) → ex_fout_rew Q X Y Q'
+;
+
+
+% We prove the lemma which states that processes involved in free output transitions (fstep Q (f_out X Y) Q')
+% can be rewritten (up to congruence) in a canonic way (ex_fout_rew Q X Y Q').
+% Before, we need three additional lemmas which prove the result in particular cases.
+
+rec fs_out_rew_par1: (g:ctx) {R:[g ⊢ proc]} [g ⊢ ex_fout_rew Q X Y Q']
+  → [g ⊢ ex_fout_rew (Q p_par R) X Y (Q' p_par R)] =
+/ total d (fs_out_rew_par1 _ _ _ _ _ _ d) /
+mlam R ⇒ fn d ⇒ case d of
+   | [g ⊢ fout_base C1 C2] ⇒ [g ⊢ fout_base (c_trans (c_par C1)
+     (c_sym par_assoc)) (c_trans (c_par C2) (c_sym par_assoc))]
+   | [g ⊢ fout_ind C1 C2 \w.D1[..,w]] ⇒ let [g,w:names ⊢ D2[..,w]]
+     = fs_out_rew_par1 [g,w:names ⊢ R[..]] [g,w:names ⊢ D1[..,w]] in
+       [g ⊢ fout_ind (c_trans (c_par C1) sc_ext_par)
+       (c_trans (c_par C2) sc_ext_par) \w.D2[..,w]]
+;
+
+rec fs_out_rew_par2: (g:ctx) {R:[g ⊢ proc]} [g ⊢ ex_fout_rew Q X Y Q']
+  → [g ⊢ ex_fout_rew (R p_par Q) X Y (R p_par Q')] =
+/ total d (fs_out_rew_par2 _ _ _ _ _ _ d) /
+mlam R ⇒ fn d ⇒ case d of
+   | [g ⊢ fout_base C1 C2] ⇒ [g ⊢ fout_base (c_trans par_comm (c_trans (c_par C1)
+     (c_sym par_assoc))) (c_trans par_comm (c_trans (c_par C2) (c_sym par_assoc)))]
+   | [g ⊢ fout_ind C1 C2 \w.D1[..,w]] ⇒ let [g,w:names ⊢ D2[..,w]]
+     = fs_out_rew_par2 [g,w:names ⊢ R[..]] [g,w:names ⊢ D1[..,w]] in
+     [g ⊢ fout_ind (c_trans par_comm (c_trans (c_par C1) (c_trans sc_ext_par
+       (c_res \w.par_comm)))) (c_trans par_comm (c_trans (c_par C2)
+       (c_trans sc_ext_par (c_res \w.par_comm)))) \w.D2[..,w]]
+;
+
+rec fs_out_rew_res: (g:ctx) ([g,z:names ⊢ ex_fout_rew Q[..,z] X[..] Y[..] Q'[..,z]])
+  → [g ⊢ ex_fout_rew (p_res \z.Q[..,z]) X Y (p_res \z.Q'[..,z])] =
+/ total d (fs_out_rew_res _ _ _ _ _ d) /
+fn d ⇒ case d of
+   | [g,z:names ⊢ fout_base C1[..,z] C2[..,z]] ⇒ [g ⊢ fout_ind (c_res \z.C1[..,z])
+     (c_res \z.C2[..,z]) \z.(fout_base c_ref c_ref)]
+   | [g,z:names ⊢ fout_ind C1[..,z] C2[..,z] \w.D1[..,z,w]] ⇒ let [g,z:names ⊢ D2[..,z]]
+     = fs_out_rew_res [g,z:names,w:names ⊢ D1[..,z,w]] in
+       [g ⊢ fout_ind (c_res \z.C1[..,z]) (c_res \z.C2[..,z]) \z.D2[..,z]]
+;
+
+
+rec fs_out_rew: (g:ctx) [g ⊢ fstep Q (f_out X Y) Q']
+   → [g ⊢ ex_fout_rew Q X Y Q'] =
+/ total f (fs_out_rew _ _ _ _ _ f) /
+fn f ⇒ case f of
+   | [g ⊢ fs_out] ⇒ [g ⊢ fout_base (c_sym par_unit) (c_sym par_unit)]
+   | [g ⊢ fs_par1 B1]:[g ⊢ fstep (P p_par R) (f_out X Y) (P' p_par R)] ⇒
+     let [g ⊢ D1] = fs_out_rew [g ⊢ B1] in
+     let [g ⊢ D2] = fs_out_rew_par1 [g ⊢ R] [g ⊢ D1] in [g ⊢ D2]
+   | [g ⊢ fs_par2 B2]:[g ⊢ fstep (R p_par P) (f_out X Y) (R p_par P')] ⇒
+     let [g ⊢ D1] = fs_out_rew [g ⊢ B2] in
+     let [g ⊢ D2] = fs_out_rew_par2 [g ⊢ R] [g ⊢ D1] in [g ⊢ D2]
+   | [g ⊢ fs_res \z.F[..,z]] ⇒
+     let [g,z:names ⊢ D1[..,z]] = fs_out_rew [g,z:names ⊢ F[..,z]] in
+     let [g ⊢ D2] = fs_out_rew_res [g,z:names ⊢ D1[..,z]] in [g ⊢ D2]
+;

case-studies/harmony-lemma-formalization/4_bound_output_rewriting.bel

@@ -0,0 +1,85 @@
+% Predicate about syntactic equivalence of processes involved in bound output transitions:
+% ex_bout_rew Q X Q' holds iff there exist R, S, z, x_1,...,x_n such that Q cong (nu z)(nu x_1)...(nu x_n)((p_out X z R) p_par S) and
+% (Q' z) cong (nu x_1)...(nu x_n)((R z) p_par (S z)).
+% We encode this type via two constructors: one representing the base case without restrictions, and one representing the inductive case
+% in which Q cong (nu x)P and Q' cong (nu x)P', where ex_bout_rew P X P' holds inductively.
+
+LF ex_bout_rew: proc → names → (names → proc) → type =
+  | bout_base: Q cong (p_res \z.((p_out X z (R z)) p_par (S z)))
+    → ({y:names} (Q' y) cong ((R y) p_par (S y))) → ex_bout_rew Q X Q'
+  | bout_ind: Q cong (p_res P) → ({y:names} (Q' y) cong (p_res (P' y)))
+    → ({w:names} ex_bout_rew (P w) X \y.(P' y w)) → ex_bout_rew Q X Q'
+;
+
+
+% We prove the lemma which states that processes involved in bound output transitions (bstep Q (b_out X) Q')
+% can be rewritten (up to congruence) in a canonic way (ex_bout_rew Q X Q').
+% Before, we need four additional lemmas which prove the result in particular cases.
+
+rec bs_out_rew_par1: (g:ctx) {R:[g ⊢ proc]} [g ⊢ ex_bout_rew Q X \y.Q'[..,y]]
+  → [g ⊢ ex_bout_rew (Q p_par R) X \y.(Q'[..,y] p_par R[..])] =
+/ total d (bs_out_rew_par1 _ _ _ _ _ d) /
+mlam R ⇒ fn d ⇒ case d of
+   | [g ⊢ bout_base C1 \y.C2[..,y]] ⇒
+     [g ⊢ bout_base (c_trans (c_par C1) (c_trans sc_ext_par (c_res \z.(c_sym par_assoc))))
+     \y.(c_trans (c_par C2[..,y]) (c_sym par_assoc))]
+   | [g ⊢ bout_ind C1 (\y.C2[..,y]) (\w.D1[..,w])] ⇒ let [g,w:names ⊢ D2[..,w]]
+     = bs_out_rew_par1 [g,w:names ⊢ R[..]] [g,w:names ⊢ D1[..,w]] in
+ 	   [g ⊢ bout_ind (c_trans (c_par C1) sc_ext_par)
+       (\y.(c_trans (c_par C2[..,y]) sc_ext_par)) (\w.D2[..,w])]
+;
+
+rec bs_out_rew_par2: (g:ctx) {R:[g ⊢ proc]} [g ⊢ ex_bout_rew Q X \y.Q'[..,y]]
+  → [g ⊢ ex_bout_rew (R p_par Q) X \y.(R[..] p_par Q'[..,y])] =
+/ total d (bs_out_rew_par2 _ _ _ _ _ d) /
+mlam R ⇒ fn d ⇒ case d of
+   | [g ⊢ bout_base C1 \y.C2[..,y]] ⇒ [g ⊢ bout_base (c_trans par_comm
+     (c_trans (c_par C1) (c_trans sc_ext_par (c_res \z.(c_sym par_assoc)))))
+     \y.(c_trans par_comm (c_trans (c_par C2[..,y]) (c_sym par_assoc)))]
+   | [g ⊢ bout_ind C1 (\y.C2[..,y]) (\w.D1[..,w])] ⇒ let [g,w:names ⊢ D2[..,w]]
+     = bs_out_rew_par2 [g,w:names ⊢ R[..]] [g,w:names ⊢ D1[..,w]] in
+       [g ⊢ bout_ind (c_trans par_comm (c_trans (c_par C1) (c_trans sc_ext_par
+       (c_res \w.par_comm)))) (\y.(c_trans par_comm (c_trans (c_par C2[..,y])
+       (c_trans sc_ext_par (c_res \w.par_comm))))) (\w.D2[..,w])]
+;
+
+rec bs_out_rew_res: (g:ctx) [g,z:names ⊢ ex_bout_rew Q[..,z] X[..] \y.Q'[..,z,y]]
+  → [g ⊢ ex_bout_rew (p_res \z.Q[..,z]) X \y.(p_res \z.Q'[..,z,y])] =
+/ total d (bs_out_rew_res _ _ _ _ d) /
+fn d ⇒ case d of
+   | [g,z:names ⊢ bout_base C1[..,z] \y.C2[..,z,y]] ⇒ [g ⊢ bout_ind (c_res \z.C1[..,z])
+     (\y.(c_res \z.C2[..,z,y])) (\z.(bout_base c_ref \y.c_ref))]
+   | [g,z:names ⊢ bout_ind C1[..,z] (\y.C2[..,z,y]) (\w.D1[..,z,w])] ⇒
+     let [g,z:names ⊢ D2[..,z]] = bs_out_rew_res [g,z:names,w:names ⊢ D1[..,z,w]] in
+       [g ⊢ bout_ind (c_res \z.C1[..,z]) (\y.(c_res \z.C2[..,z,y])) (\z.D2[..,z])]
+;
+
+rec bs_out_rew_open: (g:ctx) [g,z:names ⊢ ex_fout_rew Q[..,z] X[..] z Q'[..,z]]
+  → [g ⊢ ex_bout_rew (p_res \z.Q[..,z]) X \z.Q'[..,z]] =
+/ total d (bs_out_rew_open _ _ _ _ d) /
+fn d ⇒ case d of
+   | [g,z:names ⊢ fout_base C1[..,z] C2[..,z]] ⇒
+     [g ⊢ bout_base (c_res \z.C1[..,z]) \z.C2[..,z]]
+   | [g,z:names ⊢ fout_ind C1[..,z] C2[..,z] \w.D1[..,w,z]] ⇒
+     let [g,z:names ⊢ D2[..,z]] = bs_out_rew_open [g,z:names,w:names ⊢ D1[..,z,w]] in
+       [g ⊢ bout_ind (c_trans (c_res \z.C1[..,z]) sc_ext_res) (\z.C2[..,z]) (\w.D2[..,w])]
+;
+
+
+rec bs_out_rew: (g:ctx) [g ⊢ bstep Q (b_out X) \y.Q'[..,y]]
+   → [g ⊢ ex_bout_rew Q X \y.Q'[..,y]] =
+/ total b (bs_out_rew _ _ _ _ b) /
+fn b ⇒ case b of
+   | [g ⊢ bs_par1 B1]:[g ⊢ bstep (P p_par R) (b_out X) \y.(P' p_par R[..])] ⇒
+     let [g ⊢ D1] = bs_out_rew [g ⊢ B1] in
+     let [g ⊢ D2] = bs_out_rew_par1 [g ⊢ R] [g ⊢ D1] in [g ⊢ D2]
+   | [g ⊢ bs_par2 B2]:[g ⊢ bstep (R p_par P) (b_out X) \y.(R[..] p_par P')] ⇒
+     let [g ⊢ D1] = bs_out_rew [g ⊢ B2] in
+     let [g ⊢ D2] = bs_out_rew_par2 [g ⊢ R] [g ⊢ D1] in [g ⊢ D2]
+   | [g ⊢ bs_res \z.B[..,z]] ⇒
+     let [g,z:names ⊢ D1[..,z]] = bs_out_rew [g,z:names ⊢ B[..,z]] in
+     let [g ⊢ D2] = bs_out_rew_res [g,z:names ⊢ D1[..,z]] in [g ⊢ D2]
+   | [g ⊢ bs_open \z.F[..,z]] ⇒
+     let [g,z:names ⊢ D1[..,z]] = fs_out_rew [g,z:names ⊢ F[..,z]] in
+     let [g ⊢ D2] = bs_out_rew_open [g,z:names ⊢ D1[..,z]] in [g ⊢ D2]
+;