Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Added "harmony-lemma-formalization" as a new case study #273

Merged
merged 2 commits into from
Jul 29, 2024
Merged

Added "harmony-lemma-formalization" as a new case study #273

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
af517fd
added harmony-lemma-formalization
GabrieleCecilia Jul 28, 2024
eab7c5b
Apply suggestions from code review
MartyO256 Jul 29, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
107 changes: 107 additions & 0 deletions case-studies/harmony-lemma-formalization/1_definitions.bel
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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'
;
72 changes: 72 additions & 0 deletions case-studies/harmony-lemma-formalization/2_input_rewriting.bel
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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]
;
70 changes: 70 additions & 0 deletions case-studies/harmony-lemma-formalization/3_free_output_rewriting.bel
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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]
;
85 changes: 85 additions & 0 deletions case-studies/harmony-lemma-formalization/4_bound_output_rewriting.bel
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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]
;
Loading
Loading