Library HOC19Coincide
Require Import HOC01Defs.
Require Import HOC02BaseLemmas.
Require Import HOC03CanonicalLemmas.
Require Import HOC04DefLTS.
Require Import HOC05WFProcesses.
Require Import HOC06FreshLemmas.
Require Import HOC07SizeLemmas.
Require Import HOC08SubstLemmas.
Require Import HOC09GVLemmas.
Require Import HOC10CongrLemmas.
Require Import HOC11TransLemmas.
Require Import HOC12Guarded.
Require Import HOC13Bisimulations.
Require Import HOC14IObis.
Require Import HOC15HObis.
Require Import HOC16CONbis.
Require Import HOC17NORbis.
Require Import HOC18ONORbis.
Lemma IObis_IObis : IO_bisimulation IObis.
Proof.
splits¬.
apply IObis_in.
apply IObis_out.
apply IObis_var.
Qed.
Lemma HObis_HObis : HigherOrder_bisimulation HObis.
Proof.
splits¬.
apply HObis_tau.
apply HObis_out.
apply HObis_closed.
Qed.
Lemma CONbis_CONbis : Context_bisimulation CONbis.
Proof.
splits¬.
apply CONbis_sym.
apply CONbis_tau.
apply CONbis_out_context.
apply CONbis_closed.
Qed.
Lemma NORbis_NORbis : Normal_bisimulation NORbis.
Proof.
splits¬.
apply NORbis_sym.
apply NORbis_tau.
apply NORbis_out_normal.
apply NORbis_in_normal.
Qed.
Lemma ONORbis_ONORbis : OpenNormal_bisimulation ONORbis.
Proof.
splits¬.
apply ONORbis_tau.
apply ONORbis_out_normal.
apply ONORbis_in.
apply ONORbis_var.
Qed.
Lemma IObis_closed : closed_relation IObis.
Proof.
unfolds. introv Hp; introv Ht.
lets (X & Hf) : find_fresh((proc p)::(proc q)::nil).
rewrite Forall_to_conj_2 in Hf. destruct Hf as (Hfp & Hfq).
destruct Hp as (R & HR & HO). lets HR´: HR. destruct HR´ as (_ & I & _).
unfolds in I. specialize (I p q HO a fp Ht).
destruct I as (fq & Ht´ & Hq). specializes Hq X Hfp Hfq.
∃ fq; splits×.
introv Hcp.
rewrites¬ (wfp_inst_subst fp a X p r). rewrites¬ (wfp_inst_subst fq a X q r).
applys× IObis_subst1.
∃ R. split¬.
Qed.
Lemma IObis_congr_pipe : ∀ a xs p q,
p≈q → (wfp_pipe a xs p) ≈ (wfp_pipe a xs q).
Proof with automate.
induction xs; introv Hbis...
applys¬ IObis_congr_abs.
Qed.
Lemma IObis_HObis : HigherOrder_bisimulation IObis.
Proof.
splits.
apply IObis_sym.
apply IObis_tau.
apply IObis_out.
apply IObis_closed.
Qed.
Lemma IObis_HObisE: ∀ p q,
p ≈ q → p ≈*HO q.
Proof.
introv Hbis. unfolds. introv Hfl.
apply (IObis_congr_pipe a xs p q) in Hbis.
splits.
applys¬ wfp_closed_pipe.
apply permut_from_list in Hfl. rewrite Hfl. rewrite from_to_list. apply subset_union_weak_l.
applys¬ wfp_closed_pipe.
apply permut_from_list in Hfl. rewrite Hfl. rewrite from_to_list. apply subset_union_weak_r.
∃ IObis. splits¬. apply IObis_HObis.
Qed.
Fixpoint list_subset (cs : list (var × chan)) (ys : list var) :=
match cs with
| nil ⇒ nil
| (a :: x) ⇒ ifb (Mem (fst a) ys)
then (a :: (list_subset x ys))
else (list_subset x ys)
end.
Lemma list_subset_in_fst: ∀ xs ms ys x, length xs = length ms →
Mem x (fst (split (list_subset (combine xs ms) ys))) → Mem x xs.
Proof.
induction xs.
simpls¬.
introv Hl; lets Hl´ : Hl; symmetry in Hl; apply lengthn in Hl.
destruct Hl as (m & ms´ & Hy); subst; rew_length in ×.
simpl; cases_if; introv Hm.
rewrite fst_split_cons in Hm; simpls.
apply Mem_inv in Hm; inverts¬ Hm; constructor×.
constructor×.
Qed.
Lemma list_subset_in_snd: ∀ xs ms ys y, length xs = length ms →
Mem y (snd (split (list_subset (combine xs ms) ys))) → Mem y ms.
Proof.
induction xs.
simpls; introv _ Hl Hm; rewrite× Mem_nil_eq in Hm.
introv Hl; lets Hl´ : Hl; symmetry in Hl; apply lengthn in Hl.
destruct Hl as (m & ms´ & Hy); subst; rew_length in ×.
simpl; cases_if; introv Hm.
rewrite snd_split_cons in Hm; simpls.
apply Mem_inv in Hm; inverts¬ Hm; constructor×.
constructor×.
Qed.
Lemma list_subset_in_set: ∀ cs A x,
Mem x (fst (split (list_subset cs (to_list A)))) → x \in A.
Proof.
induction cs; simpls~; introv Hm.
rewrites× Mem_nil_eq in Hm.
cases_if~; rewrite <- (from_list_spec (fst a)) in *; rewrite from_to_list in ×.
rewrite fst_split_cons in Hm; apply Mem_inv in Hm; inverts× Hm.
Qed.
Lemma list_subset_in_set_inv: ∀ xs ms ys x, length xs = length ms →
Mem x xs → Mem x ys → Mem x (fst (split (list_subset (combine xs ms) ys))).
Proof.
induction xs.
simpls¬.
introv Hl Hf Hm; lets Hl´ : Hl; symmetry in Hl; apply lengthn in Hl;
rew_length in ×.
destruct Hl as (m & ms´ & Hms´); subst; simpl; cases_if; rew_length in ×.
rewrite fst_split_cons; simpl; inverts¬ Hf; constructor¬.
inverts× Hf.
Qed.
Lemma list_subset_Forall_fst : ∀ xs ms A P, length xs = length ms →
Forall P xs → Forall P (fst (split (list_subset (combine xs ms) (to_list A)))).
Proof.
inductions xs; simpls¬.
introv Hl Hf; lets Hl´ : Hl; symmetry in Hl; apply lengthn in Hl;
rew_length in ×.
destruct Hl as (m & ms´ & Hms´); subst; simpl; cases_if; rew_length in ×.
rewrite fst_split_cons; simpl; constructor; inverts¬ Hf.
applys¬ IHxs; inverts¬ Hf.
Qed.
Lemma list_subset_Forall_snd : ∀ xs ms A P, length xs = length ms →
Forall P ms → Forall P (snd (split (list_subset (combine xs ms) (to_list A)))).
Proof.
inductions xs; simpls; try constructor.
introv Hl Hf; lets Hl´ : Hl; symmetry in Hl; apply lengthn in Hl;
rew_length in ×.
destruct Hl as (m & ms´ & Hms´); subst; simpl; cases_if; rew_length in ×.
rewrite snd_split_cons; simpl; constructor; inverts¬ Hf.
applys¬ IHxs; inverts¬ Hf.
Qed.
Lemma list_subset_nodup_fst : ∀ xs ms A, length xs = length ms →
noDup xs → noDup (fst (split (list_subset (combine xs ms) (to_list A)))).
Proof.
inductions xs.
simpls¬.
introv Hl Hnd.
lets Hl´ : Hl; symmetry in Hl´; apply lengthn in Hl´; destruct Hl´ as (b & ms´ & Heq); subst; rename ms´ into ms.
simpls; destruct Hnd as (Hna & Hnd); cases_if×.
rewrite fst_split_cons; split; simpl.
introv Hin; apply list_subset_in_fst in Hin; auto.
applys¬ IHxs.
Qed.
Lemma list_subset_nodup_snd : ∀ xs ms A, length xs = length ms →
noDup ms → noDup (snd (split (list_subset (combine xs ms) (to_list A)))).
Proof.
introv; generalize xs; clear xs.
inductions ms; introv Hl Hnd.
rew_length in Hl; apply length0 in Hl; subst; simpls¬.
lets Hl´ : Hl; apply lengthn in Hl´; destruct Hl´ as (b & xs´ & Heq); subst; rename xs´ into xs.
simpls; destruct Hnd as (Hna & Hnd); cases_if×.
rewrite snd_split_cons; split; simpl.
introv Hin; apply list_subset_in_snd in Hin; auto.
applys¬ IHms.
Qed.
Lemma list_subset_subset: ∀ cs ys x,
Mem x (list_subset cs ys) → Mem x cs.
Proof.
induction cs; introv Hm; simpls~; cases_if×.
rewrite Mem_cons_eq in Hm; inverts Hm; constructor×.
constructor×.
Qed.
Lemma list_subset_combine_in : ∀ xs ms v w E, length xs = length ms → Mem (v, w) (combine xs ms) → v \in E → Mem (v, w) (list_subset (combine xs ms) (to_list E)).
Proof.
inductions xs.
simpls¬.
introv Hl Hm Hin.
lets Hl´ : Hl; symmetry in Hl´; apply lengthn in Hl´; destruct Hl´ as (b & ms´ & Heq); subst; rename ms´ into ms.
simpls; cases_if*; rewrite Mem_cons_eq in *; inverts× Hm.
inverts H. rewrite <- from_list_spec in n; rewrite× from_to_list in n.
Qed.
Inductive R_HO_IO : binary wfprocess :=
| RHOIO : ∀ (p q : wfprocess) (xs : list var) (ms : list chan),
length xs = length ms →
noDup xs → noDup ms →
Forall (fun x ⇒ x \in GV p ∨ x \in GV q) xs →
Forall (fun m ⇒ m ### p ∧ m ### q) ms →
wfp_multisubst (combine xs (¬¬ms)) p ≈*HO wfp_multisubst (combine xs (¬¬ms)) q →
R_HO_IO p q.
Lemma in_R_HO_IO : in_relation R_HO_IO.
Proof.
introv Hr; intros a fp Htp.
inverts Hr as Hlxsms Hndxs Hndms Hnfxs Hfms HHxs.
assert (Hloxsms : length xs = length (¬¬ms)) by rewrite¬ wfp_length_opl.
assert (Hclms : closed_proc_list_wfp (¬¬ms)) by apply wfp_cpl_opl.
assert (Hfams : ∀ fq (Htq : {{q -- LabIn a ->> AA fq}}) X, Forall (fun m : chan ⇒ m ### wfp_inst_Abs fp (wfp_Gvar X) ∧ m ### wfp_inst_Abs fq (wfp_Gvar X)) ms).
intros; rewrite <- Forall_Mem in *; introv Hm.
specializes Hfms Hm; simpl; split.
applys× (wfp_cfresh_in a x p); apply cfresh_gvar.
applys× (wfp_cfresh_in a x q); apply cfresh_gvar.
assert (Hnfaxs : ∀ fq (Htq : {{q -- LabIn a ->> AA fq}}) X, Forall (fun x : var ⇒ x \in GV (wfp_inst_Abs fp (wfp_Gvar X)) ∨ x \in GV (wfp_inst_Abs fq (wfp_Gvar X))) xs).
intros; rewrite <- Forall_Mem in *; introv Hm; simpl.
specializes Hnfxs Hm; inverts Hnfxs; [left | right].
applys¬ (GV_trans_in_sub _ _ _ Htp (wfp_Gvar X) x).
applys¬ (GV_trans_in_sub _ _ _ Htq (wfp_Gvar X) x).
set (pxs := wfp_multisubst (combine xs (¬¬ms)) p); fold pxs in HHxs.
set (qxs := wfp_multisubst (combine xs (¬¬ms)) q); fold qxs in HHxs.
set (gv := to_list (GV pxs \u GV qxs)).
set (n´ := length gv).
lets (mmms & Hlgvmmms & Hndmmms & Hfmmms & Hneqmmms) : (find_fresh_chan_n n´ ((proc pxs) :: (proc qxs) :: nil) ms).
symmetry in Hlgvmmms; unfold n´ in Hlgvmmms.
assert (Hlogvmmms : length gv = length (¬¬mmms)) by rewrite¬ wfp_length_opl.
assert (Hclmmms : closed_proc_list_wfp (¬¬mmms)) by apply wfp_cpl_opl.
assert (Hnfgv : Forall (fun x : var ⇒ x \in GV p ∨ x \in GV q) gv).
rewrite <- Forall_Mem in ×.
introv Hm; subst gv; rewrite <- from_list_spec in Hm; rewrite from_to_list in Hm.
rewrite in_union in Hm; inverts Hm; [subst pxs | subst qxs]; rewrites¬ wfp_GV_Msubst_cp in H; rewrite in_remove in H; destruct H as (H & _); auto.
assert (Hnfagv : ∀ fq (Htq : {{q -- LabIn a ->> AA fq}}) X, Forall (fun x : var ⇒ x \in GV (wfp_inst_Abs fp (wfp_Gvar X)) ∨ x \in (GV (wfp_inst_Abs fq (wfp_Gvar X)))) gv).
intros; rewrite <- Forall_Mem in *; introv Hm; specialize (Hnfgv x Hm).
inverts Hnfgv; [left | right]; simpl.
applys¬ (GV_trans_in_sub _ _ _ Htp (wfp_Gvar X)).
applys¬ (GV_trans_in_sub _ _ _ Htq (wfp_Gvar X)).
assert (Hfmmms´ : Forall (fun m : chan ⇒ m ### p ∧ m ### q) mmms).
rewrite <- Forall_Mem in *; introv Hm.
specializes Hfmmms Hm; rewrite Forall_to_conj_2 in Hfmmms.
destruct Hfmmms as (Hfmp & Hfmq); split;
unfold pxs in Hfmp; unfold qxs in Hfmq;
apply wfp_cfresh_msubst_from in Hfmp; apply wfp_cfresh_msubst_from in Hfmq; auto.
clear Hfmmms; rename Hfmmms´ into Hfmmms.
assert (Hyfammms : ∀ fq (Htq : {{q -- LabIn a ->> AA fq}}) X, Forall (fun m : chan ⇒ m ### wfp_inst_Abs fp (wfp_Gvar X) ∧ m ### wfp_inst_Abs fq (wfp_Gvar X)) mmms).
intros; rewrite <- Forall_Mem in *; introv Hm.
specializes Hfmmms Hm; destruct Hfmmms as (Hfp & Hfq); simpl; split.
applys× (wfp_cfresh_in a x p); apply cfresh_gvar.
applys× (wfp_cfresh_in a x q); apply cfresh_gvar.
lets HHgvmmms´ : HHxs; rewrites¬ (HObisE_equiv pxs qxs gv) in HHgvmmms´.
specializes¬ HHgvmmms´ Hclmmms.
set (pxsgv := wfp_multisubst (combine gv (¬¬mmms)) pxs); fold pxsgv in HHgvmmms´.
set (qxsgv := wfp_multisubst (combine gv (¬¬mmms)) qxs); fold qxsgv in HHgvmmms´.
lets (fpxs & Htpxs & Hyppxs) : (wfp_trans_Msubst_in _ xs (¬¬ms) _ _ Htp); auto.
fold pxs in Htpxs; fold pxs in Hyppxs.
lets¬ (fpxsgv & Htpxsgv & Hyppxsgv) : (wfp_trans_Msubst_in _ gv (¬¬mmms) _ _ Htpxs).
fold pxsgv in Htpxsgv, Hyppxsgv.
lets (Hclpxsgv & Hclqxsgv & R & (HSym & Htau & Hout & Hcl) & Hr) : HHgvmmms´.
lets (fqxsgv & Htqxsgv & Hclabs) : (Hcl _ _ Hr _ _ Htpxsgv).
assert (HclinstAbs : ∀ r : wfprocess, closed_process r → closed_process (wfp_inst_Abs fpxsgv r) ∧ closed_process (wfp_inst_Abs fqxsgv r)).
introv Hclr; splits; eapply cp_trans_in; auto; try apply Htpxsgv; try apply Htqxsgv; [apply Hclpxsgv | apply Hclqxsgv].
assert (Hp´q´_HO :
∀ r : wfprocess, closed_process r →
(wfp_inst_Abs fpxsgv r ≈HO wfp_inst_Abs fqxsgv r)).
introv Hclr; specialize (HclinstAbs r Hclr); splits; intuition; ∃× R; repeat splits¬.
assert (Hp´q´_HOE :
∀ r : wfprocess, closed_process r →
(wfp_inst_Abs fpxsgv r ≈*HO wfp_inst_Abs fqxsgv r)).
introv Hclr; specialize (Hp´q´_HO r Hclr); applys¬ HO_HOE.
lets¬ (fqms & Htqms & Hypqxs) : (wfp_trans_Msubst_name_in _ _ _ _ _ Htqxsgv).
lets¬ (fq & Htq & Hypq) : (wfp_trans_Msubst_name_in _ _ _ _ _ Htqms).
∃ fq; splits¬.
introv Hfp Hfq.
assert (Hnmgv : ¬ Mem X gv).
rewrite <- from_list_spec; unfold gv; rewrite from_to_list; rewrite in_union; rew_logic; split; unfold pxs; repeat applys¬ wfp_fresh_Msubst1.
specialize (Hyppxsgv X Hnmgv); specialize (Hypqxs X Hnmgv).
assert (Hnmxs : ¬ Mem X xs).
introv Hm.
apply (Forall_mem) with (P := (fun x : var ⇒ x \in GV p ∨ x \in GV q)) in Hm; auto.
unfold fresh_gvar in *; intuition.
specialize (Hyppxs X Hnmxs); specialize (Hypq X Hnmxs).
fold qxsgv in Hypqxs; fold qxs in Hypq.
rewrite Hypq in Hypqxs; clear Hypq.
rewrite Hyppxs in Hyppxsgv; clear Hyppxs.
assert (Hfpxsfvgv : X # pxsgv) by (applys¬ wfp_fresh_cp).
assert (Hfqxsfvgv : X # qxsgv) by (applys¬ wfp_fresh_cp).
assert (Heqp : ∀ (r : wfprocess), closed_process r → wfp_inst_Abs fpxsgv r = wfp_multisubst (combine (X::nil) (r::nil)) (wfp_inst_Abs fpxsgv (wfp_Gvar X))) by
(introv Hcr; simpl; rewrite wfp_subst_on_inst_Abs with (p := pxsgv) (a := a) (X := X); jauto).
assert (Heqq : ∀ (r : wfprocess), closed_process r → wfp_inst_Abs fqxsgv r = wfp_multisubst (combine (X::nil) (r::nil)) (wfp_inst_Abs fqxsgv (wfp_Gvar X))) by
(introv Hcr; simpl; rewrite wfp_subst_on_inst_Abs with (p := qxsgv) (a := a) (X := X); auto).
assert (Hp´q´_HO´ : ∀ r : wfprocess, closed_process r →
wfp_multisubst (combine (X :: nil) (r :: nil)) (wfp_inst_Abs fpxsgv (wfp_Gvar X)) ≈HO wfp_multisubst (combine (X :: nil) (r :: nil))
(wfp_inst_Abs fqxsgv (wfp_Gvar X))) by (introv Hcr; rewrites¬ <- Heqp; rewrites¬ <- Heqq); clear Hp´q´_HO.
rewrite Hyppxsgv in Hp´q´_HO´; rewrite Hypqxs in Hp´q´_HO´.
set (paxsgv := wfp_multisubst (combine gv (¬¬mmms)) (wfp_multisubst (combine xs (¬¬ms)) (wfp_inst_Abs fp (wfp_Gvar X))));
set (qaxsgv := wfp_multisubst (combine gv (¬¬mmms)) (wfp_multisubst (combine xs (¬¬ms)) (wfp_inst_Abs fq (wfp_Gvar X)))).
fold paxsgv in Hp´q´_HO´; fold qaxsgv in Hp´q´_HO´.
assert (HHa : paxsgv ≈*HO qaxsgv).
assert (Hypgv : GV paxsgv \u GV qaxsgv = \{} ∨ GV paxsgv \u GV qaxsgv = \{X}).
elim (classic (const_abs fqxsgv)); elim (classic (const_abs fpxsgv)); introv Hcap Hcaq;
try apply (GV_trans_in_const _ _ _ Htpxsgv) with (q := wfp_Gvar X) in Hcap;
try apply (GV_trans_in_const _ _ _ Htqxsgv) with (q := wfp_Gvar X) in Hcaq;
try apply (GV_trans_in _ _ _ Htpxsgv) with (q := wfp_Gvar X) in Hcap;
try apply (GV_trans_in _ _ _ Htqxsgv) with (q := wfp_Gvar X) in Hcaq;
unfold paxsgv; unfold qaxsgv;
rewrite <- Hyppxsgv; rewrite <- Hypqxs; simpl;
try rewrite Hcap; try rewrite Hcaq;
try rewrite Hclpxsgv; try rewrite Hclqxsgv; simpl;
repeat rewrite¬ union_same; repeat rewrite¬ union_empty_l;
repeat rewrite¬ union_empty_r.
inverts Hypgv as Hypgv.
assert (Hp : permut nil (to_list (GV paxsgv \u GV qaxsgv))) by
(rewrite Hypgv; apply to_from_list).
apply (HObisE_equiv paxsgv qaxsgv nil Hp); simpl.
intros _ _ _.
apply union_empty in Hypgv; inverts Hypgv as He1 He2.
specialize (Hp´q´_HO´ paxsgv He1); simpl in Hp´q´_HO´; do 2 rewrite¬ wfp_gfresh_subst_rewrite in Hp´q´_HO´; unfolds fresh_gvar; try rewrite He1; try rewrite He2; unfold notin; rewrite¬ in_empty.
assert (Haux : \{X} = from_list (X :: nil)).
apply fset_extens; introv Hm; rewrite from_list_spec in ×.
rewrite in_singleton in Hm; subst; constructor.
inverts Hm as Hm; rewrite¬ in_singleton.
rewrite× Mem_nil_eq in Hm.
assert (Hp : permut (X :: nil) (to_list (GV paxsgv \u GV qaxsgv))).
rewrite Hypgv; rewrite Haux; apply to_from_list.
apply (HObisE_equiv paxsgv qaxsgv (X :: nil) Hp).
introv Hllr Hclr.
lets Hllr´ : Hllr; apply lengthn in Hllr´; destruct Hllr´ as (r & lr´ & Heq); subst; rename lr´ into lr.
assert (Heq : lr = nil) by (apply length0; rew_length in *; nat_math); subst.
apply Hp´q´_HO´; simpls×.
assert (Heq : length (gv ++ xs) = length (mmms ++ ms)).
repeat rewrite length_app; nat_math.
assert (Hndf : noDup (gv ++ xs)).
repeat rewrite nodup_app_iff; repeat splits¬.
subst gv; apply nodup_tolist.
apply fset_extens; introv Hin; rewrite in_empty in *; try solve [false].
rewrite in_inter in Hin; subst gv.
rewrite from_to_list in Hin; rewrite in_union in Hin; subst pxs qxs.
inverts Hin; inverts H; rewrite¬ wfp_GV_Msubst_cp in H1; rewrite in_remove in H1; jauto.
assert (Hndm : noDup (mmms ++ ms)).
repeat rewrite nodup_app_iff; repeat splits~; apply fset_extens; introv Hin; rewrite in_empty in *; try solve [false].
rewrite in_inter in Hin; do 2 rewrite from_list_spec in Hin; destruct Hin as (Hin1 & Hin2).
specializes Hneqmmms Hin1; rewrite <- Forall_Mem in Hneqmmms.
specializes¬ Hneqmmms Hin2.
assert (Hnff : Forall (fun x : var ⇒ x \in GV (wfp_inst_Abs fp (wfp_Gvar X)) ∨ x \in GV (wfp_inst_Abs fq (wfp_Gvar X))) (gv ++ xs)) by repeat applys¬ Forall_app.
assert (Hyff : Forall (fun m : chan ⇒ m ### wfp_inst_Abs fp (wfp_Gvar X) ∧
m ### wfp_inst_Abs fq (wfp_Gvar X)) (mmms ++ ms)) by repeat applys¬ Forall_app.
apply (RHOIO (wfp_inst_Abs fp (wfp_Gvar X)) (wfp_inst_Abs fq (wfp_Gvar X)) (gv ++ xs) (mmms ++ ms) Heq Hndf Hndm Hnff Hyff).
subst paxsgv qaxsgv.
repeat rewrite <- wfp_mult_sub_separate2 in HHa.
rewrite <- permut_combine_step in HHa; repeat rewrite¬ <- wfp_opl_app in HHa; try (repeat rewrites¬ length_app; repeat rewrite¬ wfp_length_opl); repeat rewrite¬ app_assoc in HHa.
Qed.
Lemma var_R_HO_IO : var_relation R_HO_IO.
Proof.
introv Hr; introv Htp; lets Hr´ : Hr; inverts Hr´ as Hlxsms Hndxs Hndms HinGVxs Hfms HHxs.
set (pxs := wfp_multisubst (combine xs (¬¬ms)) p); fold pxs in HHxs.
set (qxs := wfp_multisubst (combine xs (¬¬ms)) q); fold qxs in HHxs.
set (gv := to_list (GV pxs \u GV qxs)).
set (n´ := length gv).
lets (mmms & Hlgvmmms & Hndmmms & Hfmmms & Hneqmmms) : (find_fresh_chan_n n´ ((proc p) :: (proc q) :: nil) ms).
symmetry in Hlgvmmms; unfold n´ in Hlgvmmms.
assert (Hlofvmmms : length gv = length (¬¬mmms)) by rewrite¬ wfp_length_opl.
assert (Hclmmms : closed_proc_list_wfp (¬¬mmms)) by apply wfp_cpl_opl.
assert (Haux : length (¬¬mmms) = length gv) by (rewrite¬ wfp_length_opl).
lets HHxsgv : HHxs; rewrites¬ (HObisE_equiv pxs qxs gv) in HHxsgv.
specialize (HHxsgv (¬¬mmms) Haux (wfp_cpl_opl _)); clear Haux.
unfold pxs, qxs in HHxsgv.
repeat rewrite <- wfp_mult_sub_separate2 in HHxsgv.
repeat (rewrite <- permut_combine_step in HHxsgv; try rew_length; repeat rewrite¬ wfp_length_opl).
assert (Hndf : noDup (gv ++ xs)).
repeat rewrite nodup_app_iff; repeat splits¬.
subst gv; apply nodup_tolist.
apply fset_extens; introv Hin; rewrite in_empty in *; try solve [false].
rewrite in_inter in Hin; subst gv.
rewrite from_to_list in Hin; rewrite in_union in Hin; subst pxs qxs.
inverts Hin; inverts H; rewrite¬ wfp_GV_Msubst_cp in H1; try rewrite¬ wfp_length_opl; try apply wfp_cpl_opl; rewrite in_remove in H1; jauto.
assert (Hndm : noDup (mmms ++ ms)).
repeat rewrite nodup_app_iff; repeat splits~; apply fset_extens; introv Hin; rewrite in_empty in *; try solve [false].
rewrite in_inter in Hin; do 2 rewrite from_list_spec in Hin; destruct Hin as (Hin1 & Hin2).
specializes Hneqmmms Hin1; rewrite <- Forall_Mem in Hneqmmms.
specializes¬ Hneqmmms Hin2.
assert (HmX : Mem X (gv ++ xs)).
repeat rewrite Mem_app_or_eq.
elim (classic (Mem X xs)); intro Hyp; jauto; left.
rewrite <- from_list_spec; unfold gv; rewrite from_to_list; rewrite in_union; left.
unfold pxs; rewrite wfp_GV_Msubst_cp; try rewrite¬ wfp_length_opl; try apply wfp_cpl_opl; rewrite in_remove; split.
eapply GV_trans_rem1; apply Htp.
unfold notin; rewrite¬ from_list_spec.
lets Hp : HmX; apply permut_mem_exists in Hp; destruct Hp as (l & Hpl).
assert (Hlxsgv : length (gv ++ xs) = length ((¬¬mmms) ++ (¬¬ms))).
repeat rewrite length_app; repeat rewrite¬ wfp_length_opl.
lets (s & Hps & Hp) : permut_exists Hpl ((¬¬mmms) ++ ¬¬ms) Hlxsgv.
assert (Haux´ : length (X :: l) = length s).
apply permut_len in Hpl; apply permut_len in Hps; nat_math.
symmetry in Haux´; rew_length in Haux´; apply lengthn in Haux´; destruct Haux´ as (x & s´ & Heq); subst s; rename s´ into s.
repeat rewrite <- wfp_opl_app in Hps.
lets Heqs : (wfp_permut_opl _ _ Hps).
destruct Heqs as (ns & Heqns & _).
assert (Hex : ∃ x´ ns´, ns = x´ :: ns´).
assert (length (x :: s) = length (¬¬ns)) by (rewrite¬ Heqns).
symmetry in H; rewrite wfp_length_opl in H; rew_length in H; apply lengthn in H.
destruct H as (x´ & ns´ & Heq); ∃¬ x´ ns´.
destruct Hex as (x´ & ns´ & Heq); subst ns; rewrite Heqns in *; clear Heqns x s; rename x´ into x; rename ns´ into ns.
assert (Hllns : length l = length ns) by (repeat rewrite wfp_opl_app in Hps; simpls; apply permut_len in Hpl; apply permut_len in Hps; rew_length in *; repeat rewrite wfp_length_opl in *; nat_math).
assert (HpauxX : permut (X :: l) (l & X)).
assert (Haux : noDup (X :: l)).
apply permut_nodup with (l := (gv ++ xs)); auto.
rewrite permut_count_forall; introv.
rewrite count_app_plus; simpl; nat_math.
assert (Hpauxx : permut (x :: ns) (ns & x)).
assert (Haux : noDup (x :: ns)).
apply permut_nodup with (l := (mmms ++ ms)); auto.
rewrite¬ wfp_permut_opl_iff.
rewrite permut_count_forall; introv.
rewrite count_app_plus; simpl; nat_math.
assert (Hpr : permut (combine (gv ++ xs) ((¬¬mmms) ++ ¬¬ms))
(combine (l & X) ((¬¬ns) & (wfp_Send x wfp_Nil)))).
apply permut_trans with (l2 := combine (X :: l) (wfp_Send x wfp_Nil :: (¬¬ns))); auto.
apply permut_ndfl.
apply nodup_combine_fst; try (rew_length; rewrite¬ wfp_length_opl).
apply permut_nodup with (l := (gv ++ xs)); auto.
apply nodup_combine_fst; try (rew_length; rewrite¬ wfp_length_opl).
apply permut_nodup with (l := (X :: l)); auto.
apply permut_nodup with (l := (gv ++ xs)); auto.
rewrite permut_combine_step; try rewrite¬ wfp_length_opl; try (rew_length; nat_math); simpl.
rewrite from_list_app; repeat rewrite from_list_cons; rewrite from_list_nil; simpl.
apply fset_extens; introv Hin; rewrite in_union in *; inverts× Hin.
right; rewrite in_union; left; auto.
left; rewrite in_union in H; inverts× H.
rewrite× in_empty in H0.
lets HHxsgv´ : HHxsgv; rewrite wfp_Msubst_invariant_permut with (xr := (l & X)) (yr := ((¬¬ns) & (wfp_Send x wfp_Nil))) in HHxsgv; auto;
try solve [rew_length; rewrite¬ wfp_length_opl];
try solve [repeat rewrite <- wfp_opl_app; apply wfp_cpl_opl];
rewrite (wfp_Msubst_invariant_permut (gv ++ xs)) with (xr := (l & X)) (yr := ((¬¬ns) & (wfp_Send x wfp_Nil))) in HHxsgv; auto;
try solve [rew_length; rewrite¬ wfp_length_opl];
try solve [repeat rewrite <- wfp_opl_app; apply wfp_cpl_opl].
lets Htp´ : Htp; apply (wfp_trans_rem_is_out x X) in Htp´; replace Nil with (proc (wfp_Nil)) in Htp´ by auto.
eapply (wfp_trans_Msubst_out x) in Htp´. Focus 2. apply Hllns.
do 2 rewrite¬ <- wfp_multisubst_to_subst_tail in Htp´; try rewrite¬ wfp_length_opl.
lets Hout : (HObisC_out (wfp_multisubst (combine (l & X) ((¬¬ns) & wfp_Send x wfp_Nil)) p) (wfp_multisubst (combine (l & X) ((¬¬ns) & wfp_Send x wfp_Nil)) q) HHxsgv _ _ _ Htp´).
destruct Hout as (qa´1 & qa´´1 & Ht1 & HHq´1 & HHq´´1).
rewrite¬ wfp_multisubst_to_subst_tail in Ht1; try rewrite¬ wfp_length_opl.
eapply wfp_trans_Msubst_name_out in Ht1; auto.
destruct Ht1 as (q´1 & q´´1 & Htq´ & Heq´1 & Heq´2); subst qa´1 qa´´1.
apply wfp_trans_out_is_rem in Htq´.
destruct Htq´ as (q´ & Htq & Heq´1 & Heq´2); subst q´1 q´´1.
∃ q´; splits¬.
rewrite wfp_multisubst_to_subst_tail in HHq´1; try rewrite¬ wfp_length_opl.
rename HHq´1 into HHp´q´; clear HHq´´1.
assert (Hypgvpq : GV p \u GV q = from_list (gv ++ xs)).
destruct HHxsgv´ as (Hcp & Hcq & _).
unfold closed_process in Hcp, Hcq; rewrite wfp_GV_Msubst_cp in Hcp, Hcq;
repeat rewrite length_app; repeat rewrite wfp_length_opl;
repeat rewrite <- wfp_opl_app; try apply wfp_cpl_opl; try nat_math.
apply fset_extens; introv Hin.
rewrite <- fset_extens_iff in Hcp, Hcq;
specializes Hcp x0; specializes Hcq x0.
rewrite in_remove in *; unfold notin in *; rewrite in_empty in ×.
apply not_not_elim; introv Hnin.
rewrite in_union in Hin; inverts Hin; [rewrite× <- Hcp | rewrite× <- Hcq].
repeat rewrite from_list_app in *; repeat rewrite in_union in ×.
inverts Hin as Hin.
subst gv; rewrite from_to_list in Hin.
rewrite in_union in Hin; inverts Hin as Hin; subst pxs qxs;
rewrite wfp_GV_Msubst_cp in Hin;
try rewrite¬ wfp_length_opl; try apply wfp_cpl_opl;
repeat rewrite× in_remove in Hin.
rewrite <- Forall_Mem in HinGVxs; rewrite from_list_spec in Hin;
specializes¬ HinGVxs Hin.
assert (Hypgvp´q´ : GV p´ \u GV q´ = from_list l ∨ GV p´ \u GV q´ = from_list l \u \{X}).
lets Hgvp´ : (GV_trans_rem2 _ _ _ Htp); lets Hgvq´ : (GV_trans_rem2 _ _ _ Htq).
lets Hpl´ : Hpl; apply permut_from_list in Hpl´; rewrite Hpl´ in Hypgvpq.
rewrite Hgvp´ in Hypgvpq; rewrite Hgvq´ in Hypgvpq; clear Hgvp´ Hgvq´.
rewrite <- union_assoc in Hypgvpq; rewrite (union_assoc \{X}) in Hypgvpq;
rewrite (union_comm \{X}) in Hypgvpq; rewrite <- union_assoc in Hypgvpq;
rewrite union_same in Hypgvpq.
rewrite from_list_cons in Hypgvpq; rewrite (union_comm \{X}) in Hypgvpq.
elim (classic (X \in (GV p´ \u GV q´))); intro Hin; [right | left].
rewrite union_assoc in Hypgvpq; rewrite union_comm in Hypgvpq.
rewrite (union_already_in Hin) in Hypgvpq; auto.
assert (Hnin : ¬ X \in from_list l).
apply permut_nodup in Hpl; auto.
rewrite from_list_spec; simpls×.
rewrite <- fset_extens_iff in Hypgvpq.
apply fset_extens; introv Hyp; specializes Hypgvpq x0.
assert (x0 ≠ X) by (intro Heq; rewrite Heq in Hyp; false).
assert (x0 \in GV p´ \u GV q´ \u \{X}).
rewrite union_assoc; rewrite in_union; left; auto.
rewrite Hypgvpq in H0; rewrite in_union in H0; inverts¬ H0.
rewrite× in_singleton in H1.
assert (x0 ≠ X) by (intro Heq; rewrite Heq in Hyp; false).
assert (x0 \in from_list l \u \{X}).
rewrite in_union; left; auto.
rewrite <- Hypgvpq in H0; rewrite in_union in *; inverts H0; [left | right]; auto.
rewrite in_union in H1; inverts¬ H1; rewrite× in_singleton in H0.
inverts Hypgvp´q´ as HypGV.
applys¬ (RHOIO p´ q´ l ns).
apply permut_nodup in Hpl; auto; simpls×.
rewrite <- wfp_permut_opl_iff in Hps; apply permut_nodup in Hps; auto; simpls×.
rewrite <- Forall_Mem; introv Hm.
rewrite <- fset_extens_iff in HypGV; specialize (HypGV x0); rewrite in_union in HypGV; rewrite HypGV; rewrite¬ from_list_spec.
rewrite <- Forall_Mem; introv Hm.
assert (Hin : Mem x0 (mmms ++ ms)).
rewrite <- wfp_permut_opl_iff in Hps; apply permut_sym in Hps.
apply permut_mem with (l := (x :: ns)); auto; constructor¬.
repeat rewrite Mem_app_or_eq in Hin; inverts Hin as Hin.
split; eapply wfp_cfresh_rem. Focus 2. apply Htp. Focus 3. apply Htq.
specializes Hfmmms Hin; rewrite× Forall_to_conj_2 in Hfmmms.
specializes Hfmmms Hin; rewrite× Forall_to_conj_2 in Hfmmms.
rewrite <- Forall_Mem in Hfms; specializes¬ Hfms Hin.
split; eapply wfp_cfresh_rem. Focus 2. apply Htp. Focus 3. apply Htq.
jauto. jauto.
assert (Hfp´ : X # p´).
unfold fresh_gvar; unfold notin; intro Hin.
assert (Haux : X \in from_list l).
rewrite <- HypGV; rewrite in_union; left; auto.
apply permut_nodup in Hpl; auto; simpls; rewrite from_list_spec in Haux; false×.
assert (Hfq´ : X # q´).
unfold fresh_gvar; unfold notin; intro Hin.
assert (Haux : X \in from_list l).
rewrite <- HypGV; rewrite in_union; right; auto.
apply permut_nodup in Hpl; auto; simpls; rewrite from_list_spec in Haux; false×.
do 2 rewrite¬ wfp_gfresh_subst_rewrite in HHp´q´; apply¬ HO_HOE.
applys¬ (RHOIO p´ q´ (l & X) (ns & x)).
rew_length; nat_math.
apply permut_nodup with (l := (X :: l)); auto.
apply permut_nodup in Hpl; auto; simpls×.
apply permut_nodup with (l := (x :: ns)); auto.
rewrite <- wfp_permut_opl_iff in Hps; apply permut_nodup in Hps; auto; simpls×.
apply Forall_permut with (l1 := (X :: l)); auto.
rewrite <- Forall_Mem; introv Hm.
rewrite <- fset_extens_iff in HypGV; specialize (HypGV x0); rewrite in_union in HypGV; rewrite HypGV.
rewrite in_union; rewrite Mem_cons_eq in Hm; inverts Hm.
right; rewrite¬ in_singleton.
left; rewrite¬ from_list_spec.
apply Forall_permut with (l1 := (x :: ns)); auto.
rewrite <- Forall_Mem; introv Hm.
assert (Hin : Mem x0 (mmms ++ ms)).
rewrite <- wfp_permut_opl_iff in Hps; apply permut_sym in Hps.
apply permut_mem with (l := (x :: ns)); auto; constructor¬.
repeat rewrite Mem_app_or_eq in Hin; inverts Hin as Hin.
split; eapply wfp_cfresh_rem. Focus 2. apply Htp. Focus 3. apply Htq.
specializes Hfmmms Hin; rewrite× Forall_to_conj_2 in Hfmmms.
specializes Hfmmms Hin; rewrite× Forall_to_conj_2 in Hfmmms.
rewrite <- Forall_Mem in Hfms; specializes¬ Hfms Hin.
split; eapply wfp_cfresh_rem. Focus 2. apply Htp. Focus 3. apply Htq.
jauto. jauto.
do 2 rewrite <- wfp_multisubst_to_subst_tail in HHp´q´; try rewrite¬ wfp_length_opl.
rewrite wfp_opl_app; simpl; applys¬ HO_HOE.
rewrite <- wfp_permut_opl_iff in Hps.
apply permut_sym in Hps; apply permut_mem with (x := x) in Hps; try solve [constructor].
repeat rewrite Mem_app_or_eq in Hps; inverts Hps as Hm.
specializes Hfmmms Hm; rewrite× Forall_to_conj_2 in Hfmmms.
rewrite <- Forall_Mem in Hfms; specializes Hfms Hm; jauto.
rewrite <- wfp_permut_opl_iff in Hps.
apply permut_nodup in Hps; auto.
simpls×.
Qed.
Lemma out_R_HO_IO : out_relation R_HO_IO.
Proof.
introv Hr; introv Htp.
inverts Hr as Hlxs Hndxs Hndms HGVxs Hfms HHxs.
assert (Hloxs : length xs = length (¬¬ms)) by rewrite¬ wfp_length_opl.
assert (Hclms : closed_proc_list_wfp (¬¬ms)) by apply wfp_cpl_opl.
assert (Hnmams : ¬ Mem a ms).
apply wfp_cfresh_out_inv in Htp.
introv Hm; apply Forall_mem with (P := fun m : chan ⇒ m ### p ∧ m ### q) in Hm; jauto.
set (pxs := wfp_multisubst (combine xs (¬¬ms)) p); fold pxs in HHxs.
set (qxs := wfp_multisubst (combine xs (¬¬ms)) q); fold qxs in HHxs.
generalize (wfp_trans_Msubst_out _ _ _ _ Htp xs ms Hlxs).
set (p´xs := wfp_multisubst (combine xs (¬¬ms)) p´);
set (p´´xs := wfp_multisubst (combine xs (¬¬ms)) p´´); fold pxs; intro Htpxs.
set (lxsp´ := list_subset (combine xs ms) (to_list (GV p´))).
set (xsp´ := fst (split(lxsp´))); set (msp´ := snd (split (lxsp´))).
assert (Hlxsp´ : length xsp´ = length msp´) by (subst xsp´ msp´; rewrite split_length_l; rewrite¬ split_length_r).
assert (Hndxsp´ : noDup xsp´) by applys¬ list_subset_nodup_fst.
assert (Hndmsp´ : noDup msp´) by applys¬ list_subset_nodup_snd.
assert (Hclmsp´ : closed_proc_list_wfp (¬¬msp´)) by apply wfp_cpl_opl.
set (lxsp´´ := list_subset (combine xs ms) (to_list (GV p´´))).
set (xsp´´ := fst (split(lxsp´´))); set (msp´´ := snd (split (lxsp´´))).
assert (Hleqxsp´´ : length xsp´´ = length msp´´) by (subst xsp´´ msp´´; rewrite split_length_l; rewrite¬ split_length_r).
assert (Hndxsp´´ : noDup xsp´´) by applys¬ list_subset_nodup_fst.
assert (Hndmsp´´ : noDup msp´´) by applys¬ list_subset_nodup_snd.
assert (Hclmsp´´ : closed_proc_list_wfp (¬¬msp´´)) by apply wfp_cpl_opl.
assert (Hleqp´xs : p´xs = wfp_multisubst (combine xsp´ (¬¬msp´)) p´).
unfold p´xs, xsp´, msp´, lxsp´; generalize Hlxs; generalize ms; clear.
induction xs.
simpls¬.
introv H0; lets H0´ : H0; symmetry in H0; apply lengthn in H0; destruct H0 as (b0 & ms´ & Heq); subst;
rew_length in *; simpl; cases_if; rewrites¬ IHxs.
repeat rewrite fst_split_cons; repeat rewrite snd_split_cons; simpls¬.
rewrite <- from_list_spec in n; rewrite from_to_list in n.
rewrites¬ wfp_gfresh_subst_rewrite.
unfolds fresh_gvar; try rewrite wfp_GV_Msubst_cp.
unfold notin; rewrite in_remove; rew_logic; auto.
apply wfp_cpl_opl.
rewrite¬ wfp_length_opl; rewrite split_length_l; rewrites¬ split_length_r.
assert (Hleqp´´xs : p´´xs = wfp_multisubst (combine xsp´´ (¬¬msp´´)) p´´).
unfold p´´xs, xsp´´, msp´´, lxsp´´; generalize Hlxs; generalize ms; clear.
induction xs.
simpls¬.
introv H0; lets H0´ : H0; symmetry in H0; apply lengthn in H0; destruct H0 as (b0 & ms´ & Heq); subst;
rew_length in *; simpl; cases_if; rewrites¬ IHxs.
repeat rewrite fst_split_cons; repeat rewrite snd_split_cons; simpls¬.
rewrite <- from_list_spec in n; rewrite from_to_list in n.
rewrites¬ wfp_gfresh_subst_rewrite.
unfolds fresh_gvar; try rewrite wfp_GV_Msubst_cp;
try rewrite wfp_list_proc_len; try rewrite¬ wfp_length_opl; try rewrite wfp_length_opl;
try applys¬ wfp_cpl_opl; try rewrite split_length_l; try rewrites¬ split_length_r.
unfold notin; rewrite in_remove; rew_logic; auto.
set (gv := to_list (GV pxs \u GV qxs)).
set (n´ := length gv).
lets (mmms & Hlgv & Hndmmms & Hfmmms´ & Hneqmmms) : (find_fresh_chan_n n´ ((proc p) :: (proc q) :: (Send a Nil) :: nil) ms).
symmetry in Hlgv; unfold n´ in Hlgv.
assert (Hlogv : length gv = length (¬¬mmms)) by rewrite¬ wfp_length_opl.
assert (Hclmmms : closed_proc_list_wfp (¬¬mmms)) by apply wfp_cpl_opl.
assert (Hndgv : noDup gv) by apply nodup_tolist.
assert (Hnfgv : Forall (fun x : var ⇒ x \in GV p ∨ x \in GV q) gv).
unfold gv.
assert (∀ x, x \in from_list (to_list (GV pxs \u GV qxs)) → x \in GV p ∨ x \in GV q).
unfold pxs, qxs; repeat rewrite wfp_Msubst_eq; simpls; try rewrites¬ wfp_length_opl.
introv Hin; rewrite from_to_list in Hin; rewrite in_union in *; elim Hin; clear Hin; intro Hin; [left | right];
rewrite wfp_GV_Msubst_cp in Hin; try rewrites¬ <- wfp_cpl_cpl; try applys¬ wfp_cpl_opl; try rewrites¬ wfp_list_proc_len;
try rewrites¬ wfp_length_opl; rewrite in_remove in Hin; jauto.
rewrite <- Forall_Mem; introv Hm; rewrite <- from_list_spec in Hm; specializes¬ H Hm.
assert (Hfmmms : Forall (fun m : chan ⇒ m ### p ∧ m ### q) mmms).
rewrite <- Forall_Mem; introv Hm; specializes Hfmmms´ Hm.
rewrite× Forall_to_conj_3 in Hfmmms´.
assert (Hnmammms : ¬ Mem a mmms).
introv Hm; specializes Hfmmms´ Hm; rewrite× Forall_to_conj_3 in Hfmmms´.
destruct Hfmmms´ as (_ & _ & Hfm´); unfold fresh_chan in Hfm´; simpl in Hfm´; rewrite union_empty_r in Hfm´; unfold notin in Hfm´; rewrite¬ in_singleton in Hfm´.
clear Hfmmms´.
assert (Haux´ : length (¬¬mmms) = length gv) by auto.
lets HHxsgv : HHxs; rewrites¬ (HObisE_equiv pxs qxs gv) in HHxsgv.
specialize (HHxsgv (¬¬mmms) Haux´ (wfp_cpl_opl _)); clear Haux´.
set (pxsgv := wfp_multisubst (combine gv (¬¬mmms)) pxs); fold pxsgv in HHxsgv.
set (qxsgv := wfp_multisubst (combine gv (¬¬mmms)) qxs); fold qxsgv in HHxsgv.
generalize (wfp_trans_Msubst_out _ _ _ _ Htpxs gv mmms Hlgv).
set (p´xsgv := wfp_multisubst (combine gv (¬¬mmms)) p´xs);
set (p´´xsgv := wfp_multisubst (combine gv (¬¬mmms)) p´´xs); fold pxsgv; intro Htpxsgv.
set (lgvp´ := list_subset (combine gv mmms) (to_list (GV p´xs))).
set (gvp´ := fst (split(lgvp´))); set (mmmsp´ := snd (split (lgvp´))).
assert (Hleqgvp´ : length gvp´ = length mmmsp´) by (subst gvp´ mmmsp´; rewrite split_length_l; rewrite¬ split_length_r).
assert (Hndgvp´ : noDup gvp´) by applys¬ list_subset_nodup_fst.
assert (Hndmmmsp´ : noDup mmmsp´) by applys¬ list_subset_nodup_snd.
assert (Hclmmmsp´ : closed_proc_list_wfp (¬¬mmmsp´)) by applys¬ wfp_cpl_opl.
set (lgvp´´ := list_subset (combine gv mmms) (to_list (GV p´´xs))).
set (gvp´´ := fst (split(lgvp´´))); set (mmmsp´´ := snd (split (lgvp´´))).
assert (Hleqgvp´´ : length gvp´´ = length mmmsp´´) by (subst gvp´´ mmmsp´´; rewrite split_length_l; rewrite¬ split_length_r).
assert (Hndgvp´´ : noDup gvp´´) by applys¬ list_subset_nodup_fst.
assert (Hndmmmsp´´ : noDup mmmsp´´) by applys¬ list_subset_nodup_snd.
assert (Hclmmmsp´´ : closed_proc_list_wfp (¬¬mmmsp´´)) by applys¬ wfp_cpl_opl.
assert (Hleqp´gv : p´xsgv = wfp_multisubst (combine gvp´ (¬¬mmmsp´)) p´xs).
unfold p´xsgv, gvp´, mmmsp´, lgvp´; generalize Hlgv; clear.
generalize mmms; unfold gv; clear mmms gv.
induction (to_list (GV pxs \u GV qxs)).
simpls¬.
introv H0; lets H0´ : H0; symmetry in H0; apply lengthn in H0; destruct H0 as (b0 & mms´ & Heq); subst;
rew_length in *; simpl; cases_if; rewrites¬ IHl.
repeat rewrite fst_split_cons; repeat rewrite snd_split_cons; simpls¬.
rewrite <- from_list_spec in n; rewrite from_to_list in n.
rewrites¬ wfp_gfresh_subst_rewrite.
unfolds fresh_gvar; try rewrite¬ wfp_GV_Msubst_cp; try rewrite wfp_list_proc_len; try rewrite¬ wfp_length_opl; try rewrite wfp_length_opl; try applys¬ wfp_cpl_opl; try rewrite split_length_l; try rewrites¬ split_length_r.
unfold notin; rewrite in_remove; rew_logic; auto.
assert (Hleqp´´gv : p´´xsgv = wfp_multisubst (combine gvp´´ (¬¬mmmsp´´)) p´´xs).
unfold p´´xsgv, gvp´´, mmmsp´´, lgvp´´; generalize Hlgv; clear.
generalize mmms; unfold gv; clear mmms gv.
induction (to_list (GV pxs \u GV qxs)).
simpls¬.
introv H0; lets H0´ : H0; symmetry in H0; apply lengthn in H0; destruct H0 as (b0 & mms´ & Heq); subst;
rew_length in *; simpl; cases_if; rewrites¬ IHl.
repeat rewrite fst_split_cons; repeat rewrite snd_split_cons; simpls¬.
rewrite <- from_list_spec in n; rewrite from_to_list in n.
rewrites¬ wfp_gfresh_subst_rewrite.
unfolds fresh_gvar; try rewrite¬ wfp_GV_Msubst_cp; try rewrite wfp_list_proc_len; try rewrite¬ wfp_length_opl; try rewrite wfp_length_opl; try applys¬ wfp_cpl_opl; try rewrite split_length_l; try rewrites¬ split_length_r.
unfold notin; rewrite in_remove; rew_logic; auto.
lets (Hclpmsgv & Hclqmsgv & R & (HSym & Htau & Hout & Hcl) & Hr) : HHxsgv.
lets (q´xsgv & q´´xsgv & Htqxsgv & Rq´xsgv & Rq´´xsgv) : (Hout _ _ Hr _ _ _ Htpxsgv).
lets (q´xs & q´´xs & Htqxs & Heq´xsgv & Heq´´xsgv) : (wfp_trans_Msubst_name_out a gv mmms _ _ _ Hlgv Hnmammms Htqxsgv).
set (lgvq´ := list_subset (combine gv mmms) (to_list (GV q´xs))).
set (gvq´ := fst (split(lgvq´))); set (mmmsq´ := snd (split (lgvq´))).
set (lgvq´´ := list_subset (combine gv mmms) (to_list (GV q´´xs))).
set (gvq´´ := fst (split(lgvq´´))); set (mmmsq´´ := snd (split (lgvq´´))).
assert (Hleqgvq´ : length gvq´ = length mmmsq´) by (subst gvq´ mmmsq´; rewrite split_length_l; rewrite¬ split_length_r).
assert (Hleqgvq´´ : length gvq´´ = length mmmsq´´) by (subst gvq´´ mmmsq´´; rewrite split_length_l; rewrite¬ split_length_r).
assert (Hndgvq´ : noDup gvq´) by applys¬ list_subset_nodup_fst.
assert (Hndgvq´´ : noDup gvq´´) by applys¬ list_subset_nodup_fst.
assert (Hndmmmsq´ : noDup mmmsq´) by applys¬ list_subset_nodup_snd.
assert (Hndmmmsq´´ : noDup mmmsq´´) by applys¬ list_subset_nodup_snd.
assert (Hclmmmsq´ : closed_proc_list_wfp (¬¬mmmsp´)) by applys¬ wfp_cpl_opl.
assert (Hclmmmsq´´ : closed_proc_list_wfp (¬¬mmmsp´´)) by applys¬ wfp_cpl_opl.
assert (Hleqq´gv : q´xsgv = wfp_multisubst (combine gvq´ (¬¬mmmsq´)) q´xs).
rewrite Heq´xsgv; unfold gvq´, mmmsq´, lgvq´; generalize Hlgv; clear.
generalize mmms; unfold gv; clear mmms gv.
induction (to_list (GV pxs \u GV qxs)).
simpls¬.
introv H0; lets H0´ : H0; symmetry in H0; apply lengthn in H0; destruct H0 as (b0 & mms´ & Heq); subst;
rew_length in *; simpl; cases_if; rewrites¬ IHl.
repeat rewrite fst_split_cons; repeat rewrite snd_split_cons; simpls¬.
rewrite <- from_list_spec in n; rewrite from_to_list in n.
rewrites¬ wfp_gfresh_subst_rewrite.
unfolds fresh_gvar; try rewrite¬ wfp_GV_Msubst_cp; try rewrite wfp_list_proc_len; try rewrite¬ wfp_length_opl; try rewrite wfp_length_opl; try applys¬ wfp_cpl_opl; try rewrite split_length_l; try rewrites¬ split_length_r.
unfold notin; rewrite in_remove; rew_logic; auto.
assert (Hleqq´´gv : q´´xsgv = wfp_multisubst (combine gvq´´ (¬¬mmmsq´´)) q´´xs).
rewrite Heq´´xsgv; unfold gvq´´, mmmsq´´, lgvq´´; generalize Hlgv; clear.
generalize mmms; unfold gv; clear mmms gv.
induction (to_list (GV pxs \u GV qxs)).
simpls¬.
introv H0; lets H0´ : H0; symmetry in H0; apply lengthn in H0; destruct H0 as (b0 & mms´ & Heq); subst;
rew_length in *; simpl; cases_if; rewrites¬ IHl.
repeat rewrite fst_split_cons; repeat rewrite snd_split_cons; simpls¬.
rewrite <- from_list_spec in n; rewrite from_to_list in n.
rewrites¬ wfp_gfresh_subst_rewrite.
unfolds fresh_gvar; try rewrite¬ wfp_GV_Msubst_cp; try rewrite wfp_list_proc_len; try rewrite¬ wfp_length_opl; try rewrite wfp_length_opl; try applys¬ wfp_cpl_opl; try rewrite split_length_l; try rewrites¬ split_length_r.
unfold notin; rewrite in_remove; rew_logic; auto.
lets (q´ & q´´ & Htq & Heq´ & Heq´´) : (wfp_trans_Msubst_name_out a xs ms _ _ _ Hlxs Hnmams Htqxs).
set (lxsq´ := list_subset (combine xs ms) (to_list (GV q´))).
set (xsq´ := fst (split(lxsq´))); set (msq´ := snd (split (lxsq´))).
set (lxsq´´ := list_subset (combine xs ms) (to_list (GV q´´))).
set (xsq´´ := fst (split(lxsq´´))); set (msq´´ := snd (split (lxsq´´))).
assert (Hleqxsq´ : length xsq´ = length msq´) by (subst xsq´ msq´; rewrite split_length_l; rewrite¬ split_length_r).
assert (Hleqxsq´´ : length xsq´´ = length msq´´) by (subst xsq´´ msq´´; rewrite split_length_l; rewrite¬ split_length_r).
assert (Hndxsq´ : noDup xsq´) by applys¬ list_subset_nodup_fst.
assert (Hndxsq´´ : noDup xsq´´) by applys¬ list_subset_nodup_fst.
assert (Hndmsq´ : noDup msq´) by applys¬ list_subset_nodup_snd.
assert (Hndmsq´´ : noDup msq´´) by applys¬ list_subset_nodup_snd.
assert (Hclmsq´ : closed_proc_list_wfp (¬¬msp´)) by applys¬ wfp_cpl_opl.
assert (Hclmsq´´ : closed_proc_list_wfp (¬¬msp´´)) by applys¬ wfp_cpl_opl.
assert (Hleqq´xs : q´xs = wfp_multisubst (combine xsq´ (¬¬msq´)) q´).
rewrite Heq´; unfold xsq´, msq´, lxsq´; generalize Hlxs; generalize ms; clear.
induction xs.
simpls¬.
introv H0; lets H0´ : H0; symmetry in H0; apply lengthn in H0; destruct H0 as (b0 & ms´ & Heq); subst;
rew_length in *; simpl; cases_if; rewrites¬ IHxs.
repeat rewrite fst_split_cons; repeat rewrite snd_split_cons; simpls¬.
rewrite <- from_list_spec in n; rewrite from_to_list in n.
rewrites¬ wfp_gfresh_subst_rewrite.
unfolds fresh_gvar; try rewrite¬ wfp_GV_Msubst_cp; try rewrite wfp_list_proc_len; try rewrite¬ wfp_length_opl; try rewrite wfp_length_opl; try applys¬ wfp_cpl_opl; try rewrite split_length_l; try rewrites¬ split_length_r.
unfold notin; rewrite in_remove; rew_logic; auto.
assert (Hleqq´´xs : q´´xs = wfp_multisubst (combine xsq´´ (¬¬msq´´)) q´´).
rewrite Heq´´; unfold xsq´´, msq´´, lxsq´´; generalize Hlxs; generalize ms; clear.
induction xs.
simpls¬.
introv H0; lets H0´ : H0; symmetry in H0; apply lengthn in H0; destruct H0 as (b0 & ms´ & Heq); subst;
rew_length in *; simpl; cases_if; rewrites¬ IHxs.
repeat rewrite fst_split_cons; repeat rewrite snd_split_cons; simpls¬.
rewrite <- from_list_spec in n; rewrite from_to_list in n.
rewrites¬ wfp_gfresh_subst_rewrite.
unfolds fresh_gvar; try rewrite¬ wfp_GV_Msubst_cp; try rewrite wfp_list_proc_len; try rewrite¬ wfp_length_opl; try rewrite wfp_length_opl; try applys¬ wfp_cpl_opl; try rewrite split_length_l; try rewrites¬ split_length_r.
unfold notin; rewrite in_remove; rew_logic; auto.
lets Hgvp´ : (GV_trans_out _ _ _ _ Htpxsgv); rewrite Hclpmsgv in Hgvp´; symmetry in Hgvp´; apply union_empty in Hgvp´; destruct Hgvp´ as (Hclp´ & Hclp´´).
lets Hgvq´ : (GV_trans_out _ _ _ _ Htqxsgv); rewrite Hclqmsgv in Hgvq´; symmetry in Hgvq´; apply union_empty in Hgvq´; destruct Hgvq´ as (Hclq´ & Hclq´´).
set (l´xs := remDup ((combine xsp´ msp´) ++ (combine xsq´ msq´))).
set (xs´ := fst (split(l´xs))); set (ms´ := snd(split(l´xs))).
set (l´gv := remDup ((combine gvp´ mmmsp´) ++ (combine gvq´ mmmsq´))).
set (gv´ := fst (split(l´gv))); set (mmms´ := snd(split(l´gv))).
assert (Hndxs´ : noDup xs´).
unfold xs´, l´xs; rewrites¬ <- permut_combine_step; apply noDup_fst_remDup_combine with (l := xs) (r := ms); auto;
unfold xsp´, msp´, lxsp´, xsq´, msq´, lxsq´; rewrite <- split_combine_fs; apply list_subset_subset.
assert (Hndgv´ : noDup gv´).
unfold gv´, l´gv; rewrites¬ <- permut_combine_step; apply noDup_fst_remDup_combine with (l := gv) (r := mmms); auto;
unfold gvp´, msp´, lgvp´, gvq´, mmmsq´, lgvq´; rewrite <- split_combine_fs; apply list_subset_subset.
assert (Hndms´ : noDup ms´).
unfold ms´, l´xs; rewrites¬ <- permut_combine_step; apply noDup_snd_remDup_combine with (l := xs) (r := ms); auto;
unfold xsp´, msp´, lxsp´, xsq´, msq´, lxsq´; rewrite <- split_combine_fs; apply list_subset_subset.
assert (Hndmmms´ : noDup mmms´).
unfold mmms´, l´gv; rewrites¬ <- permut_combine_step; apply noDup_snd_remDup_combine with (l := gv) (r := mmms); auto;
unfold gvp´, msp´, lgvp´, gvq´, mmmsq´, lgvq´; rewrite <- split_combine_fs; apply list_subset_subset.
assert (H´pms : wfp_multisubst (combine xs´ (¬¬ms´)) p´= wfp_multisubst (combine xsp´ (¬¬msp´)) p´).
symmetry; applys¬ wfp_Msubst_subst_subset.
subst xs´ ms´; rewrite split_length_l; rewrites¬ split_length_r.
introv Hin; split; intro Hm.
lets Hm´ : Hm; apply mem_comb in Hm´; try (rewrite wfp_length_opl; subst xsp´ msp´; rewrite split_length_l; rewrite¬ split_length_r); destruct Hm´ as (Hmv & Hmw).
elim (classic (msp´ = nil)); introv Hneq.
rewrite Hneq in Hmw; simpls; rewrite× Mem_nil_eq in Hmw.
lets (w´ & Heq) : (wfp_opl_mem _ _ Hneq Hmw); subst w.
rewrite wfp_opl_mem_combine_iff; rewrite wfp_opl_mem_combine_iff in Hm; try solve [subst xsp´ msp´ xs´ ms´; rewrite split_length_l; rewrite¬ split_length_r].
subst xs´ ms´; rewrite <- split_combine_fs; subst l´xs.
rewrite mem_remdup_iff; rewrites¬ Mem_app_or_eq.
lets Hm´ : Hm; apply mem_comb in Hm´; try (rewrite¬ wfp_length_opl; subst xs´ ms´; rewrite split_length_l; rewrite¬ split_length_r); destruct Hm´ as (Hmv & Hmw).
elim (classic (ms´ = nil)); introv Hneq.
rewrite Hneq in Hmw; simpls; rewrite× Mem_nil_eq in Hmw.
lets (w´ & Heq) : (wfp_opl_mem _ _ Hneq Hmw); subst w.
rewrite wfp_opl_mem_combine_iff; rewrite wfp_opl_mem_combine_iff in Hm; try solve [subst xsp´ msp´ xs´ ms´; rewrite split_length_l; rewrite¬ split_length_r].
subst xsp´ msp´; rewrite <- split_combine_fs; subst lxsp´.
subst xs´ ms´ xsq´ msq´ lxsq´; rewrite <- split_combine_fs in Hm; unfold l´xs in Hm.
rewrite mem_remdup_iff in Hm; repeat rewrite <- split_combine_fs in Hm.
rewrite Mem_app_or_eq in Hm; inverts¬ Hm.
lets H´ : H; apply list_subset_subset in H´.
applys¬ list_subset_combine_in.
assert (H´qms : wfp_multisubst (combine xs´ (¬¬ms´)) q´= q´xs).
rewrite Hleqq´xs; symmetry; applys¬ wfp_Msubst_subst_subset.
subst xs´ ms´; rewrite split_length_l; rewrites¬ split_length_r.
introv Hin; split; intro Hm.
lets Hm´ : Hm; apply mem_comb in Hm´; try (rewrite wfp_length_opl; subst xsq´ msq´; rewrite split_length_l; rewrite¬ split_length_r); destruct Hm´ as (Hmv & Hmw).
elim (classic (msq´ = nil)); introv Hneq.
rewrite Hneq in Hmw; simpls; rewrite× Mem_nil_eq in Hmw.
lets (w´ & Heq) : (wfp_opl_mem _ _ Hneq Hmw); subst w.
rewrite wfp_opl_mem_combine_iff; rewrite wfp_opl_mem_combine_iff in Hm; try solve [subst xsq´ msq´ xs´ ms´; rewrite split_length_l; rewrite¬ split_length_r].
subst xs´ ms´; rewrite <- split_combine_fs; subst l´xs.
rewrite mem_remdup_iff; rewrites¬ Mem_app_or_eq.
lets Hm´ : Hm; apply mem_comb in Hm´; try (rewrite¬ wfp_length_opl; subst xs´ ms´; rewrite split_length_l; rewrite¬ split_length_r); destruct Hm´ as (Hmv & Hmw).
elim (classic (ms´ = nil)); introv Hneq.
rewrite Hneq in Hmw; simpls; rewrite× Mem_nil_eq in Hmw.
lets (w´ & Heq) : (wfp_opl_mem _ _ Hneq Hmw); subst w.
rewrite wfp_opl_mem_combine_iff; rewrite wfp_opl_mem_combine_iff in Hm; try solve [subst xsq´ msq´ xs´ ms´; rewrite split_length_l; rewrite¬ split_length_r].
subst xsq´ msq´; rewrite <- split_combine_fs; subst lxsq´.
subst xs´ ms´ xsp´ msp´ lxsp´; rewrite <- split_combine_fs in Hm; unfold l´xs in Hm.
rewrite mem_remdup_iff in Hm; repeat rewrite <- split_combine_fs in Hm.
rewrite Mem_app_or_eq in Hm; inverts¬ Hm.
lets H´ : H; apply list_subset_subset in H´.
applys¬ list_subset_combine_in.
assert (H´pmsgv : wfp_multisubst (combine gv´ (¬¬mmms´)) p´xs = wfp_multisubst (combine gvp´ (¬¬mmmsp´)) p´xs).
symmetry; applys¬ wfp_Msubst_subst_subset.
subst gv´ mmms´; rewrite split_length_l; rewrites¬ split_length_r.
introv Hin; split; intro Hm.
lets Hm´ : Hm; apply mem_comb in Hm´; try (rewrite wfp_length_opl; subst gvp´ mmmsp´; rewrite split_length_l; rewrite¬ split_length_r); destruct Hm´ as (Hmv & Hmw).
elim (classic (mmmsp´ = nil)); introv Hneq.
rewrite Hneq in Hmw; simpls; rewrite× Mem_nil_eq in Hmw.
lets (w´ & Heq) : (wfp_opl_mem _ _ Hneq Hmw); subst w.
rewrite wfp_opl_mem_combine_iff; rewrite wfp_opl_mem_combine_iff in Hm; try solve [subst gvp´ mmmsp´ gv´ mmms´; rewrite split_length_l; rewrite¬ split_length_r].
subst gv´ mmms´; rewrite <- split_combine_fs; subst l´gv.
rewrite mem_remdup_iff; rewrites¬ Mem_app_or_eq.
lets Hm´ : Hm; apply mem_comb in Hm´; try (rewrite¬ wfp_length_opl; subst gv´ mmms´; rewrite split_length_l; rewrite¬ split_length_r); destruct Hm´ as (Hmv & Hmw).
elim (classic (mmms´ = nil)); introv Hneq.
rewrite Hneq in Hmw; simpls; rewrite× Mem_nil_eq in Hmw.
lets (w´ & Heq) : (wfp_opl_mem _ _ Hneq Hmw); subst w.
rewrite wfp_opl_mem_combine_iff; rewrite wfp_opl_mem_combine_iff in Hm; try solve [subst gvp´ mmmsp´ gv´ mmms´; rewrite split_length_l; rewrite¬ split_length_r].
subst gvp´ mmmsp´; rewrite <- split_combine_fs; subst lgvp´.
subst gv´ mmms´ gvq´ mmmsq´ lgvq´; rewrite <- split_combine_fs in Hm; unfold l´gv in Hm.
rewrite mem_remdup_iff in Hm; repeat rewrite <- split_combine_fs in Hm.
rewrite Mem_app_or_eq in Hm; inverts¬ Hm.
lets H´ : H; apply list_subset_subset in H´.
applys¬ list_subset_combine_in.
assert (H´qmsgv : wfp_multisubst (combine gv´ (¬¬mmms´)) q´xs = q´xsgv).
rewrite Hleqq´gv; symmetry; applys¬ wfp_Msubst_subst_subset.
subst gv´ mmms´; rewrite split_length_l; rewrites¬ split_length_r.
introv Hin; split; intro Hm.
lets Hm´ : Hm; apply mem_comb in Hm´; try (rewrite wfp_length_opl; subst gvq´ mmmsq´; rewrite split_length_l; rewrite¬ split_length_r); destruct Hm´ as (Hmv & Hmw).
elim (classic (mmmsq´ = nil)); introv Hneq.
rewrite Hneq in Hmw; simpls; rewrite× Mem_nil_eq in Hmw.
lets (w´ & Heq) : (wfp_opl_mem _ _ Hneq Hmw); subst w.
rewrite wfp_opl_mem_combine_iff; rewrite wfp_opl_mem_combine_iff in Hm; try solve [subst gvq´ mmmsq´ gv´ mmms´; rewrite split_length_l; rewrite¬ split_length_r].
subst gv´ mmms´; rewrite <- split_combine_fs; subst l´gv.
rewrite mem_remdup_iff; rewrites¬ Mem_app_or_eq.
lets Hm´ : Hm; apply mem_comb in Hm´; try (rewrite¬ wfp_length_opl; subst gv´ mmms´; rewrite split_length_l; rewrite¬ split_length_r); destruct Hm´ as (Hmv & Hmw).
elim (classic (mmms´ = nil)); introv Hneq.
rewrite Hneq in Hmw; simpls; rewrite× Mem_nil_eq in Hmw.
lets (w´ & Heq) : (wfp_opl_mem _ _ Hneq Hmw); subst w.
rewrite wfp_opl_mem_combine_iff; rewrite wfp_opl_mem_combine_iff in Hm; try solve [subst gvq´ mmmsq´ gv´ mmms´; rewrite split_length_l; rewrite¬ split_length_r].
subst gvq´ mmmsq´; rewrite <- split_combine_fs; subst lgvq´.
subst gv´ mmms´ gvp´ mmmsp´ lgvp´; rewrite <- split_combine_fs in Hm; unfold l´gv in Hm.
rewrite mem_remdup_iff in Hm; repeat rewrite <- split_combine_fs in Hm.
rewrite Mem_app_or_eq in Hm; inverts¬ Hm.
lets H´ : H; apply list_subset_subset in H´.
applys¬ list_subset_combine_in.
assert (Heql´ : length (gv´ ++ xs´) = length (mmms´ ++ ms´)).
subst gv´ xs´ mmms´ ms´.
repeat rewrite length_app; repeat rewrite split_length_l; repeat rewrites¬ split_length_r.
assert (Hnff´ : Forall (fun x : var ⇒ x \in GV p´ ∨ x \in GV q´) (gv´ ++ xs´)).
rewrite <- Forall_Mem; introv Hm.
assert (Hm´ : Mem x ((gvp´ ++ gvq´) ++ (xsp´ ++ xsq´))).
repeat rewrite Mem_app_or_eq in Hm; repeat rewrite Mem_app_or_eq; inverts Hm.
left; subst gv´ l´gv.
rewrite <- permut_combine_step in H; auto.
rewrite combine_remdup_fst_iff in H; try (rew_length in *; nat_math); rewrite Mem_app_or_eq in H; auto.
right.
subst xs´ l´xs; rewrite <- permut_combine_step in H; auto.
rewrite combine_remdup_fst_iff in H; try (rew_length in *; nat_math); rewrite Mem_app_or_eq in H; auto.
subst gv´ xs´ gvp´ gvq´ xsp´ xsq´ lgvp´ lgvq´ lxsp´ lxsq´.
repeat rewrite Mem_app_or_eq in Hm´; inverts Hm´; inverts H;
try (apply list_subset_in_set in H0; subst p´xsgv p´xs;
try rewrite Heq´xsgv in H0; try rewrite Heq´ in H0;
rewrite wfp_GV_Msubst_cp in H0; try rewrites¬ wfp_length_opl;
try applys¬ wfp_cpl_opl; repeat rewrite× in_remove in H0).
left; eapply list_subset_in_set; apply H0.
right; eapply list_subset_in_set; apply H0.
assert (Hyff´mmms : Forall (fun m : chan ⇒ m ### p´ ∧ m ### q´) mmms).
rewrite <- Forall_Mem in *; introv Hm; destruct mmms.
rewrite× Mem_nil_eq in Hm.
assert (a ≠ c) by (rewrite Mem_cons_eq in Hnmammms; rew_logic in Hnmams; auto).
rewrite Mem_cons_eq in Hm; specialize (Hfmmms x); inverts Hm.
assert (Hmm´ : Mem c (c :: mmms)) by constructor; specialize (Hfmmms Hmm´).
destruct Hfmmms as (Hfmmmsp & Hfmmmsq); split; lets Hfoutp: (wfp_cfresh_out a c _ _ _ Hfmmmsp Htp); lets Hfoutq : (wfp_cfresh_out a c _ _ _ Hfmmmsq Htq); jauto.
assert (Hmm´ : Mem x (c :: mmms)) by constructor~; specialize (Hfmmms Hmm´).
destruct Hfmmms as (Hfmmmsp & Hfmmmsq); split; lets Hfoutp: (wfp_cfresh_out a x _ _ _ Hfmmmsp Htp); lets Hfoutq : (wfp_cfresh_out a x _ _ _ Hfmmmsq Htq); jauto.
assert (Hyff´ms : Forall (fun m : chan ⇒ m ### p´ ∧ m ### q´) ms).
rewrite <- Forall_Mem in *; introv Hm.
assert (a ≠ x) by (intro Heqax; apply Hnmams; rewrites¬ Heqax).
specialize (Hfms x Hm); destruct Hfms as (Hfmsp & Hfmsq); split; lets Hfoutp: (wfp_cfresh_out a x _ _ _ Hfmsp Htp); lets Hfoutq : (wfp_cfresh_out a x _ _ _ Hfmsq Htq); jauto.
assert (Hyff´ : Forall (fun m : chan ⇒ m ### p´ ∧ m ### q´) (mmms´ ++ ms´)).
rewrite <- Forall_Mem.
introv Hm; assert (Hm´ : Mem x (mmms ++ ms)).
repeat rewrite Mem_app_or_eq in Hm; repeat rewrite Mem_app_or_eq; inverts Hm.
left; subst mmms´ l´gv.
rewrite <- permut_combine_step in H; auto.
apply combine_remdup_snd in H; try (rew_length in *; nat_math); rewrite Mem_app_or_eq in H; inverts H;
subst mmmsp´ mmmsq´ lgvp´; apply list_subset_in_snd in H0; auto.
right; subst ms´ l´xs; rewrite <- permut_combine_step in H; auto.
apply combine_remdup_snd in H; try (rew_length in *; nat_math); rewrite Mem_app_or_eq in H; auto; inverts H;
subst msp´ msq´ lxsp´; apply list_subset_in_snd in H0; auto.
generalize Hm´; generalize x; clear Hm Hm´ x; rewrite Forall_Mem; repeat apply Forall_app; auto.
set (l´´xs := remDup ((combine xsp´´ msp´´) ++ (combine xsq´´ msq´´))).
set (xs´´ := fst (split(l´´xs))); set (ms´´ := snd(split(l´´xs))).
set (l´´gv := remDup ((combine gvp´´ mmmsp´´) ++ (combine gvq´´ mmmsq´´))).
set (gv´´ := fst (split(l´´gv))); set (mmms´´ := snd(split(l´´gv))).
assert (Hndxs´´ : noDup xs´´).
subst xs´´ l´´xs; rewrites¬ <- permut_combine_step; apply noDup_fst_remDup_combine with (l := xs) (r := ms); auto;
subst xsp´´ msp´´ lxsp´´ xsq´´ msq´´ lxsq´´; rewrite <- split_combine_fs; apply list_subset_subset.
assert (Hndgv´´ : noDup gv´´).
subst gv´´ l´´gv; rewrites¬ <- permut_combine_step; apply noDup_fst_remDup_combine with (l := gv) (r := mmms); auto;
subst gvp´´ msp´´ lgvp´´ gvq´´ mmmsq´´ lgvq´´; rewrite <- split_combine_fs; apply list_subset_subset.
assert (Hndms´´ : noDup ms´´).
unfold ms´´, l´´xs; rewrites¬ <- permut_combine_step; apply noDup_snd_remDup_combine with (l := xs) (r := ms); auto;
unfold xsp´´, msp´´, lxsp´´, xsq´´, msq´´, lxsq´´; rewrite <- split_combine_fs; apply list_subset_subset.
assert (Hndmmms´´ : noDup mmms´´).
unfold mmms´´, l´´gv; rewrites¬ <- permut_combine_step; apply noDup_snd_remDup_combine with (l := gv) (r := mmms); auto;
unfold gvp´´, msp´´, lgvp´´, gvq´´, mmmsq´´, lgvq´´; rewrite <- split_combine_fs; apply list_subset_subset.
assert (H´´pms : wfp_multisubst (combine xs´´ (¬¬ms´´)) p´´= wfp_multisubst (combine xsp´´ (¬¬msp´´)) p´´).
symmetry; applys¬ wfp_Msubst_subst_subset.
subst xs´´ ms´´; rewrite split_length_l; rewrites¬ split_length_r.
introv Hin; split; intro Hm.
lets Hm´´ : Hm; apply mem_comb in Hm´´; try (rewrite wfp_length_opl; subst xsp´´ msp´´; rewrite split_length_l; rewrite¬ split_length_r); destruct Hm´´ as (Hmv & Hmw).
elim (classic (msp´´ = nil)); introv Hneq.
rewrite Hneq in Hmw; simpls; rewrite× Mem_nil_eq in Hmw.
lets (w´´ & Heq) : (wfp_opl_mem _ _ Hneq Hmw); subst w.
rewrite wfp_opl_mem_combine_iff; rewrite wfp_opl_mem_combine_iff in Hm; try solve [subst xsp´´ msp´´ xs´´ ms´´; rewrite split_length_l; rewrite¬ split_length_r].
subst xs´´ ms´´; rewrite <- split_combine_fs; subst l´´xs.
rewrite mem_remdup_iff; rewrites¬ Mem_app_or_eq.
lets Hm´´ : Hm; apply mem_comb in Hm´´; try (rewrite¬ wfp_length_opl; subst xs´´ ms´´; rewrite split_length_l; rewrite¬ split_length_r); destruct Hm´´ as (Hmv & Hmw).
elim (classic (ms´´ = nil)); introv Hneq.
rewrite Hneq in Hmw; simpls; rewrite× Mem_nil_eq in Hmw.
lets (w´´ & Heq) : (wfp_opl_mem _ _ Hneq Hmw); subst w.
rewrite wfp_opl_mem_combine_iff; rewrite wfp_opl_mem_combine_iff in Hm; try solve [subst xsp´´ msp´´ xs´´ ms´´; rewrite split_length_l; rewrite¬ split_length_r].
subst xsp´´ msp´´; rewrite <- split_combine_fs; subst lxsp´´.
subst xs´´ ms´´ xsq´´ msq´´ lxsq´´; rewrite <- split_combine_fs in Hm; unfold l´´xs in Hm.
rewrite mem_remdup_iff in Hm; repeat rewrite <- split_combine_fs in Hm.
rewrite Mem_app_or_eq in Hm; inverts¬ Hm.
lets H´´ : H; apply list_subset_subset in H´´.
applys¬ list_subset_combine_in.
assert (H´´qms : wfp_multisubst (combine xs´´ (¬¬ms´´)) q´´= q´´xs).
rewrite Hleqq´´xs; symmetry; applys¬ wfp_Msubst_subst_subset.
subst xs´´ ms´´; rewrite split_length_l; rewrites¬ split_length_r.
introv Hin; split; intro Hm.
lets Hm´´ : Hm; apply mem_comb in Hm´´; try (rewrite wfp_length_opl; subst xsq´´ msq´´; rewrite split_length_l; rewrite¬ split_length_r); destruct Hm´´ as (Hmv & Hmw).
elim (classic (msq´´ = nil)); introv Hneq.
rewrite Hneq in Hmw; simpls; rewrite× Mem_nil_eq in Hmw.
lets (w´´ & Heq) : (wfp_opl_mem _ _ Hneq Hmw); subst w.
rewrite wfp_opl_mem_combine_iff; rewrite wfp_opl_mem_combine_iff in Hm; try solve [subst xsq´´ msq´´ xs´´ ms´´; rewrite split_length_l; rewrite¬ split_length_r].
subst xs´´ ms´´; rewrite <- split_combine_fs; subst l´´xs.
rewrite mem_remdup_iff; rewrites¬ Mem_app_or_eq.
lets Hm´´ : Hm; apply mem_comb in Hm´´; try (rewrite¬ wfp_length_opl; subst xs´´ ms´´; rewrite split_length_l; rewrite¬ split_length_r); destruct Hm´´ as (Hmv & Hmw).
elim (classic (ms´´ = nil)); introv Hneq.
rewrite Hneq in Hmw; simpls; rewrite× Mem_nil_eq in Hmw.
lets (w´´ & Heq) : (wfp_opl_mem _ _ Hneq Hmw); subst w.
rewrite wfp_opl_mem_combine_iff; rewrite wfp_opl_mem_combine_iff in Hm; try solve [subst xsq´´ msq´´ xs´´ ms´´; rewrite split_length_l; rewrite¬ split_length_r].
subst xsq´´ msq´´; rewrite <- split_combine_fs; subst lxsq´´.
subst xs´´ ms´´ xsp´´ msp´´ lxsp´´; rewrite <- split_combine_fs in Hm; unfold l´´xs in Hm.
rewrite mem_remdup_iff in Hm; repeat rewrite <- split_combine_fs in Hm.
rewrite Mem_app_or_eq in Hm; inverts¬ Hm.
lets H´´ : H; apply list_subset_subset in H´´.
applys¬ list_subset_combine_in.
assert (H´´pmsgv : wfp_multisubst (combine gv´´ (¬¬mmms´´)) p´´xs = wfp_multisubst (combine gvp´´ (¬¬mmmsp´´)) p´´xs).
symmetry; applys¬ wfp_Msubst_subst_subset.
subst gv´´ mmms´´; rewrite split_length_l; rewrites¬ split_length_r.
introv Hin; split; intro Hm.
lets Hm´´ : Hm; apply mem_comb in Hm´´; try (rewrite wfp_length_opl; subst gvp´´ mmmsp´´; rewrite split_length_l; rewrite¬ split_length_r); destruct Hm´´ as (Hmv & Hmw).
elim (classic (mmmsp´´ = nil)); introv Hneq.
rewrite Hneq in Hmw; simpls; rewrite× Mem_nil_eq in Hmw.
lets (w´´ & Heq) : (wfp_opl_mem _ _ Hneq Hmw); subst w.
rewrite wfp_opl_mem_combine_iff; rewrite wfp_opl_mem_combine_iff in Hm; try solve [subst gvp´´ mmmsp´´ gv´´ mmms´´; rewrite split_length_l; rewrite¬ split_length_r].
subst gv´´ mmms´´; rewrite <- split_combine_fs; subst l´´gv.
rewrite mem_remdup_iff; rewrites¬ Mem_app_or_eq.
lets Hm´´ : Hm; apply mem_comb in Hm´´; try (rewrite¬ wfp_length_opl; subst gv´´ mmms´´; rewrite split_length_l; rewrite¬ split_length_r); destruct Hm´´ as (Hmv & Hmw).
elim (classic (mmms´´ = nil)); introv Hneq.
rewrite Hneq in Hmw; simpls; rewrite× Mem_nil_eq in Hmw.
lets (w´´ & Heq) : (wfp_opl_mem _ _ Hneq Hmw); subst w.
rewrite wfp_opl_mem_combine_iff; rewrite wfp_opl_mem_combine_iff in Hm; try solve [subst gvp´´ mmmsp´´ gv´´ mmms´´; rewrite split_length_l; rewrite¬ split_length_r].
subst gvp´´ mmmsp´´; rewrite <- split_combine_fs; subst lgvp´´.
subst gv´´ mmms´´ gvq´´ mmmsq´´ lgvq´´; rewrite <- split_combine_fs in Hm; unfold l´´gv in Hm.
rewrite mem_remdup_iff in Hm; repeat rewrite <- split_combine_fs in Hm.
rewrite Mem_app_or_eq in Hm; inverts¬ Hm.
lets H´´ : H; apply list_subset_subset in H´´.
applys¬ list_subset_combine_in.
assert (H´´qmsgv : wfp_multisubst (combine gv´´ (¬¬mmms´´)) q´´xs = q´´xsgv).
rewrite Hleqq´´gv; symmetry; applys¬ wfp_Msubst_subst_subset.
subst gv´´ mmms´´; rewrite split_length_l; rewrites¬ split_length_r.
introv Hin; split; intro Hm.
lets Hm´´ : Hm; apply mem_comb in Hm´´; try (rewrite wfp_length_opl; subst gvq´´ mmmsq´´; rewrite split_length_l; rewrite¬ split_length_r); destruct Hm´´ as (Hmv & Hmw).
elim (classic (mmmsq´´ = nil)); introv Hneq.
rewrite Hneq in Hmw; simpls; rewrite× Mem_nil_eq in Hmw.
lets (w´´ & Heq) : (wfp_opl_mem _ _ Hneq Hmw); subst w.
rewrite wfp_opl_mem_combine_iff; rewrite wfp_opl_mem_combine_iff in Hm; try solve [subst gvq´´ mmmsq´´ gv´´ mmms´´; rewrite split_length_l; rewrite¬ split_length_r].
subst gv´´ mmms´´; rewrite <- split_combine_fs; subst l´´gv.
rewrite mem_remdup_iff; rewrites¬ Mem_app_or_eq.
lets Hm´´ : Hm; apply mem_comb in Hm´´; try (rewrite¬ wfp_length_opl; subst gv´´ mmms´´; rewrite split_length_l; rewrite¬ split_length_r); destruct Hm´´ as (Hmv & Hmw).
elim (classic (mmms´´ = nil)); introv Hneq.
rewrite Hneq in Hmw; simpls; rewrite× Mem_nil_eq in Hmw.
lets (w´´ & Heq) : (wfp_opl_mem _ _ Hneq Hmw); subst w.
rewrite wfp_opl_mem_combine_iff; rewrite wfp_opl_mem_combine_iff in Hm; try solve [subst gvq´´ mmmsq´´ gv´´ mmms´´; rewrite split_length_l; rewrite¬ split_length_r].
subst gvq´´ mmmsq´´; rewrite <- split_combine_fs; subst lgvq´´.
subst gv´´ mmms´´ gvp´´ mmmsp´´ lgvp´´; rewrite <- split_combine_fs in Hm; unfold l´´gv in Hm.
rewrite mem_remdup_iff in Hm; repeat rewrite <- split_combine_fs in Hm.
rewrite Mem_app_or_eq in Hm; inverts¬ Hm.
lets H´´ : H; apply list_subset_subset in H´´.
applys¬ list_subset_combine_in.
assert (Heql´´ : length (gv´´ ++ xs´´) = length (mmms´´ ++ ms´´)).
subst gv´´ xs´´ mmms´´ ms´´;
repeat rewrite length_app; repeat rewrite split_length_l; repeat rewrites¬ split_length_r.
assert (Hnff´´ : Forall (fun x : var ⇒ x \in GV p´´ ∨ x \in GV q´´) (gv´´ ++ xs´´)).
rewrite <- Forall_Mem; introv Hm.
assert (Hm´ : Mem x ((gvp´´ ++ gvq´´) ++ (xsp´´ ++ xsq´´))).
repeat rewrite Mem_app_or_eq in Hm; repeat rewrite Mem_app_or_eq; inverts Hm.
left; subst gv´´ l´´gv.
rewrite <- permut_combine_step in H; auto.
rewrite combine_remdup_fst_iff in H; try (rew_length in *; nat_math); rewrite Mem_app_or_eq in H; auto.
right.
subst xs´´ l´´xs; rewrite <- permut_combine_step in H; auto.
rewrite combine_remdup_fst_iff in H; try (rew_length in *; nat_math); rewrite Mem_app_or_eq in H; auto.
subst gv´´ xs´´ gvp´´ gvq´´ xsp´´ xsq´´ lgvp´´ lgvq´´ lxsp´´ lxsq´´.
repeat rewrite Mem_app_or_eq in Hm´; inverts Hm´; inverts H;
try (apply list_subset_in_set in H0; subst p´´xsgv p´´xs;
try rewrite Heq´´xsgv in H0; try rewrite Heq´´ in H0;
rewrite wfp_GV_Msubst_cp in H0; try rewrites¬ wfp_length_opl;
try applys¬ wfp_cpl_opl; repeat rewrite× in_remove in H0).
left; eapply list_subset_in_set; apply H0.
right; eapply list_subset_in_set; apply H0.
assert (Hyff´´mmms : Forall (fun m : chan ⇒ m ### p´´ ∧ m ### q´´) mmms).
rewrite <- Forall_Mem in *; introv Hm; destruct mmms.
rewrite× Mem_nil_eq in Hm.
assert (a ≠ c) by (rewrite Mem_cons_eq in Hnmammms; rew_logic in Hnmams; auto).
rewrite Mem_cons_eq in Hm; specialize (Hfmmms x); inverts Hm.
assert (Hmm´ : Mem c (c :: mmms)) by constructor; specialize (Hfmmms Hmm´).
destruct Hfmmms as (Hfmmmsp & Hfmmmsq); split; lets Hfoutp: (wfp_cfresh_out a c _ _ _ Hfmmmsp Htp); lets Hfoutq : (wfp_cfresh_out a c _ _ _ Hfmmmsq Htq); jauto.
assert (Hmm´ : Mem x (c :: mmms)) by constructor~; specialize (Hfmmms Hmm´).
destruct Hfmmms as (Hfmmmsp & Hfmmmsq); split; lets Hfoutp: (wfp_cfresh_out a x _ _ _ Hfmmmsp Htp); lets Hfoutq : (wfp_cfresh_out a x _ _ _ Hfmmmsq Htq); jauto.
assert (Hyff´´ms : Forall (fun m : chan ⇒ m ### p´´ ∧ m ### q´´) ms).
rewrite <- Forall_Mem in *; introv Hm.
assert (a ≠ x) by (intro Heqax; apply Hnmams; rewrites¬ Heqax).
specialize (Hfms x Hm); destruct Hfms as (Hfmsp & Hfmsq); split; lets Hfoutp: (wfp_cfresh_out a x _ _ _ Hfmsp Htp); lets Hfoutq : (wfp_cfresh_out a x _ _ _ Hfmsq Htq); jauto.
assert (Hyff´´ : Forall (fun m : chan ⇒ m ### p´´ ∧ m ### q´´) (mmms´´ ++ ms´´)).
rewrite <- Forall_Mem.
introv Hm; assert (Hm´ : Mem x (mmms ++ ms)).
repeat rewrite Mem_app_or_eq in Hm; repeat rewrite Mem_app_or_eq; inverts Hm.
left; subst mmms´´ l´´gv.
rewrite <- permut_combine_step in H; auto.
apply combine_remdup_snd in H; try (rew_length in *; nat_math); rewrite Mem_app_or_eq in H; inverts H;
subst mmmsp´´ mmmsq´´ lgvp´´; apply list_subset_in_snd in H0; auto.
right; subst ms´´ l´´xs; rewrite <- permut_combine_step in H; auto.
apply combine_remdup_snd in H; try (rew_length in *; nat_math); rewrite Mem_app_or_eq in H; auto; inverts H;
subst msp´´ msq´´ lxsp´´; apply list_subset_in_snd in H0; auto.
generalize Hm´; generalize x; clear Hm Hm´ x; rewrite Forall_Mem; repeat apply Forall_app; auto.
assert (Hnd´ : noDup (gv´ ++ xs´)).
rewrite nodup_app_iff; splits¬.
apply inter_empty_subset with (E1 := from_list gv) (E2 := from_list xs).
apply fset_extens; introv Hin.
rewrite in_inter in Hin; unfold gv in Hin; rewrite from_to_list in Hin.
subst pxs qxs; inverts Hin.
do 2 rewrite¬ wfp_GV_Msubst_cp in H; try rewrites¬ wfp_length_opl; try applys wfp_cpl_opl.
rewrite in_union in H; repeat rewrite in_remove in H; unfold notin in H; intuition.
rewrite× in_empty in Hin.
introv Hin.
subst gv´ l´gv; rewrite from_list_spec in ×.
rewrite¬ <- permut_combine_step in Hin; try solve [rew_length; nat_math].
rewrite combine_remdup_fst_iff in Hin; try solve [repeat rewrite length_app; nat_math].
rewrite Mem_app_or_eq in Hin; inverts Hin; subst gvp´ gvq´ lgvp´ lgvq´; apply list_subset_in_fst in H; auto.
introv Hin.
subst xs´ l´xs; rewrite from_list_spec in ×.
rewrite¬ <- permut_combine_step in Hin; try solve [rew_length; nat_math].
rewrite combine_remdup_fst_iff in Hin; try solve [repeat rewrite length_app; nat_math].
rewrite Mem_app_or_eq in Hin; inverts Hin; subst xsp´ xsq´ lxsp´ lxsq´; apply list_subset_in_fst in H; auto.
assert (Hnd´´ : noDup (gv´´ ++ xs´´)).
repeat (rewrite nodup_app_iff; splits~).
apply inter_empty_subset with (E1 := from_list gv) (E2 := from_list xs).
apply fset_extens; introv Hin.
rewrite in_inter in Hin; unfold gv in Hin; rewrite from_to_list in Hin.
subst pxs qxs; inverts Hin.
do 2 rewrite¬ wfp_GV_Msubst_cp in H; try rewrites¬ wfp_length_opl; try applys wfp_cpl_opl.
rewrite in_union in H; repeat rewrite in_remove in H; unfold notin in H; intuition.
rewrite× in_empty in Hin.
introv Hin.
subst gv´´ l´´gv; rewrite from_list_spec in ×.
rewrite¬ <- permut_combine_step in Hin; try solve [rew_length; nat_math].
rewrite combine_remdup_fst_iff in Hin; try solve [repeat rewrite length_app; nat_math].
rewrite Mem_app_or_eq in Hin; inverts Hin; subst gvp´´ gvq´´ lgvp´´ lgvq´´; apply list_subset_in_fst in H; auto.
introv Hin.
subst xs´´ l´´xs; rewrite from_list_spec in ×.
rewrite¬ <- permut_combine_step in Hin; try solve [rew_length; nat_math].
rewrite combine_remdup_fst_iff in Hin; try solve [repeat rewrite length_app; nat_math].
rewrite Mem_app_or_eq in Hin; inverts Hin; subst xsp´´ xsq´´ lxsp´´ lxsq´´; apply list_subset_in_fst in H; auto.
assert (Hnd´m : noDup (mmms´ ++ ms´)).
repeat (rewrite nodup_app_iff; splits~).
apply fset_extens; introv Hin; try solve [rewrite× in_empty in Hin].
rewrite in_inter in Hin; repeat rewrite from_list_spec in Hin; destruct Hin as (Hin1 & Hin2).
assert (Hin1´ : Mem x mmms).
unfold mmms´, l´gv in Hin1; rewrite¬ <- permut_combine_step in Hin1; rewrite combine_remdup_snd_iff in Hin1;
try rew_length; auto;
rewrite Mem_app_or_eq in Hin1; inverts Hin1 as Hin1;
apply list_subset_in_snd in Hin1; auto.
assert (Hin2´ : Mem x ms).
unfold ms´, l´xs in Hin2; rewrite¬ <- permut_combine_step in Hin2; rewrite¬ combine_remdup_snd_iff in Hin2;
try rew_length; auto;
rewrite Mem_app_or_eq in Hin2; inverts Hin2 as Hin2;
apply list_subset_in_snd in Hin2; auto.
specializes Hneqmmms Hin1´; rewrite <- Forall_Mem in Hneqmmms; specializes Hneqmmms Hin2´; intuition.
assert (Hnd´´m : noDup (mmms´´ ++ ms´´)).
repeat (rewrite nodup_app_iff; splits~).
apply fset_extens; introv Hin; try solve [rewrite× in_empty in Hin].
rewrite in_inter in Hin; repeat rewrite from_list_spec in Hin; destruct Hin as (Hin1 & Hin2).
assert (Hin1´ : Mem x mmms).
unfold mmms´´, l´´gv in Hin1; rewrite¬ <- permut_combine_step in Hin1; rewrite combine_remdup_snd_iff in Hin1;
try rew_length; auto;
rewrite Mem_app_or_eq in Hin1; inverts Hin1 as Hin1;
apply list_subset_in_snd in Hin1; auto.
assert (Hin2´ : Mem x ms).
unfold ms´´, l´´xs in Hin2; rewrite¬ <- permut_combine_step in Hin2; rewrite¬ combine_remdup_snd_iff in Hin2;
try rew_length; auto;
rewrite Mem_app_or_eq in Hin2; inverts Hin2 as Hin2;
apply list_subset_in_snd in Hin2; auto.
specializes Hneqmmms Hin1´; rewrite <- Forall_Mem in Hneqmmms; specializes Hneqmmms Hin2´; intuition.
∃ q´ q´´; splits¬.
applys¬ (RHOIO p´ q´ (gv´ ++ xs´) (mmms´ ++ ms´) Heql´ Hnd´ Hnd´m Hnff´ Hyff´).
repeat rewrite wfp_opl_app; repeat rewrite permut_combine_step; repeat rewrite length_app; repeat rewrites¬ wfp_length_opl;
try solve [subst gv´ xs´ ms´ mmms´ gvp´ xsp´ mmmsp´ msp´ gvq´ xsq´ mmmsq´ msq´;
repeat rewrite length_app; repeat rewrite split_length_l; repeat rewrites¬ split_length_r].
repeat rewrite wfp_mult_sub_separate2.
rewrite H´pms; rewrite <- Hleqp´xs; rewrite H´pmsgv; rewrite <- Hleqp´gv.
rewrite H´qms; rewrite H´qmsgv.
applys¬ HO_HOE; splits~; ∃ R; repeat splits¬.
applys¬ (RHOIO p´´ q´´ (gv´´ ++ xs´´) (mmms´´ ++ ms´´) Heql´´ Hnd´´ Hnd´´m Hnff´´ Hyff´´).
repeat rewrite wfp_opl_app; repeat rewrite permut_combine_step; repeat rewrite length_app; repeat rewrites¬ wfp_length_opl;
try solve [subst gv´´ xs´´ ms´´ mmms´´ gvp´´ xsp´´ mmmsp´´ msp´´ gvq´´ xsq´´ mmmsq´´ msq´´;
repeat rewrite length_app; repeat rewrite split_length_l; repeat rewrites¬ split_length_r].
repeat rewrite wfp_mult_sub_separate2.
rewrite H´´pms; rewrite <- Hleqp´´xs; rewrite H´´pmsgv; rewrite <- Hleqp´´gv.
rewrite H´´qms; rewrite H´´qmsgv.
applys¬ HO_HOE; splits~; ∃ R; repeat splits¬.
Qed.
Lemma IObis_RHOIO : IO_bisimulation R_HO_IO.
Proof.
splits.
introv Hxy; inverts Hxy.
applys¬ (RHOIO y x xs ms).
clear H0 H1 H3 H4; inductions xs; constructor~; inverts× H2.
lets H´ : H; symmetry in H´; rew_length in H´; apply lengthn in H´; destruct H´ as (b & ms´ & Heq); subst; rename ms´ into ms.
applys¬ (IHxs ms).
clear H0 H1 H2 H4; generalize H; generalize xs; clear H xs. inductions ms; constructor~; inverts× H3.
lets H´ : H; rew_length in H´; apply lengthn in H´; destruct H´ as (b & xs´ & Heq); subst; rename xs´ into xs.
apply IHms with (xs := xs); auto.
applys¬ (HObisE_sym).
apply in_R_HO_IO.
apply out_R_HO_IO.
apply var_R_HO_IO.
Qed.
Lemma HObisE_IObis : ∀ p q,
p ≈*HO q → p ≈ q.
Proof.
introv HHOE.
∃ R_HO_IO; splits.
apply IObis_RHOIO.
applys¬ (RHOIO p q nil nil); simpl; try apply Forall_nil; auto.
Qed.
Lemma HObis_IObis: ∀ p q,
p ≈HO q → p ≈ q.
Proof.
introv HHO.
apply HObisE_IObis; applys¬ HO_HOE.
Qed.
Lemma IObis_HObis_cp: ∀ (p q : wfprocess),
closed_process p → closed_process q → p ≈ q → p ≈HO q.
Proof.
introv Hcp1 Hcp2 Hio. splits¬. ∃ IObis. split¬. apply IObis_HObis.
Qed.
Lemma HObisE_unguardeds_eq : ∀ p q,
p ≈*HO q → unguardeds p = unguardeds q.
Proof.
introv HOEpq.
assert (HOEqp : q ≈*HO p) by applys¬ HObisE_sym.
assert (HRpq : R_HO_IO p q).
applys× (RHOIO p q nil nil); constructor.
assert (HRqp : R_HO_IO q p).
applys× (RHOIO q p nil nil); constructor.
lets Hvpq : var_R_HO_IO; lets Hvqp : var_R_HO_IO.
specialize (Hvpq p q HRpq); specialize (Hvqp q p HRqp).
lets Hrem : wfp_unguarded_remove_iff.
apply fset_extens; introv Hin; rewrite Hrem in Hin; destruct Hin as (r & Ht).
apply Hvpq in Ht; destruct Ht as (q´ & Ht & _); rewrite Hrem; ∃¬ q´.
apply Hvqp in Ht; destruct Ht as (p´ & Ht & _); rewrite Hrem; ∃¬ p´.
Qed.
Lemma HObisC_out_context: out_context_relation HObisC.
Proof.
unfolds. introv Hr Ht.
destruct Hr as (Hcp1 & Hcp2 & Hbis).
lets¬ (Hcpp´ & Hcpp´´): cp_trans_out Ht.
lets Ht´: Ht. eapply (HObis_out p q) in Ht; eauto.
destruct Ht as (q´ & q´´ & Ht & Hpq1 & Hpq2).
lets¬ (Hcpq´ & Hcpq´´): cp_trans_out Ht.
∃ q´ q´´. splits¬. introv H.
apply IObis_HObis_cp.
applys cp_par. split¬. unfolds. simpl; rewrite¬ GV_subst_cp. apply fset_extens; unfolds subset; introv H´.
rewrite in_remove in H´. destruct H´ as (H´&H´´). specializes H H´.
unfolds notin. false.
rewrite in_empty in H´. false.
applys cp_par. split¬. unfolds. simpl; rewrite¬ GV_subst_cp. apply fset_extens; unfolds subset; introv H´.
rewrite in_remove in H´. destruct H´ as (H´&H´´). specializes H H´.
unfolds notin. false.
rewrite in_empty in H´. false.
applys¬ IObis_congr_par; eauto. applys¬ IObis_subst.
applys¬ HObis_IObis. splits¬.
applys¬ HObis_IObis. splits¬.
Qed.
Lemma HObis_CONbis: Context_bisimulation HObisC.
Proof.
splits.
apply HObisC_sym.
apply HObisC_tau.
apply HObisC_out_context.
apply HObisC_closed.
Qed.
Lemma HObisE_CONbisE: ∀ p q, p ≈*HO q → p ≈*CON q.
Proof.
introv Hbis. unfolds in Hbis. unfolds.
introv Hfv. specializes Hbis a xs Hfv.
lets Hbis´: Hbis. destruct Hbis as (Hcp1 & Hcp2 & Hbis). splits¬.
unfolds. ∃ HObisC. split¬. apply HObis_CONbis.
Qed.
Lemma CONbisC_in_normal: in_normal_relation CONbisC.
Proof.
unfolds. introv Hbis Ht.
eapply CONbisC_closed in Hbis; auto. specialize (Hbis a fp Ht).
destruct Hbis as (fq & Htq & Hr). ∃ fq; splits¬.
introv Hf1 Hf2. apply Hr.
unfolds¬.
Qed.
Lemma CONbisC_out_normal: out_normal_relation CONbisC.
Proof with automate.
unfolds. introv Hbis Ht.
lets Hbis´: Hbis.
apply CONbisC_out_context in Hbis; auto. specializes Hbis Ht.
destruct Hbis as (q´ & q´´ & Htq & Hr). ∃ q´ q´´. split¬.
introv Hfn1 Hfn2 Hfv1 Hv2.
lets (Y & Hf): find_fresh ((Gvar X)::nil). rewrite Forall_to_conj_1 in Hf.
specializes Hr Y (wfp_Abs m X (wfp_Gvar Y)). unfolds in Hf. simpl in Hf.
rewrite notin_singleton in Hf.
do 2 rewrite¬ wfp_eq_subst_abs2 in Hr... repeat cases_if×.
apply Hr. simpl; cases_if. apply subset_refl.
Qed.
Lemma CONbis_NORbis: Normal_bisimulation CONbisC.
Proof.
splits.
apply CONbisC_sym.
apply CONbisC_tau.
apply CONbisC_out_normal.
apply CONbisC_in_normal.
Qed.
Lemma CONbisE_NORbisE: ∀ p q, p ≈*CON q → p ≈*NOR q.
Proof.
introv Hbis. unfolds in Hbis. unfolds.
introv Hfv. specializes Hbis a xs Hfv.
lets Hbis´: Hbis. destruct Hbis as (Hcp1 & Hcp2 & Hbis). splits¬.
unfolds. ∃ CONbisC. split¬. apply CONbis_NORbis.
Qed.
Lemma NORbis_congr_par_nil : ∀ p : wfprocess, closed_process p →
wfp_Par wfp_Nil p ≈NOR p.
Proof.
introv Hcp.
splits¬. apply cp_par. split¬. unfolds¬.
∃ CONbisC. split. apply CONbis_NORbis.
splits¬. apply cp_par. split¬. unfolds¬.
∃ HObisC. split. apply HObis_CONbis.
splits¬. apply cp_par. split¬. unfolds¬.
apply HObis_congr_par_nil.
Qed.
Inductive R_transNOR : binary wfprocess :=
| RtransNOR : ∀ p q r, p ≈NOR q → q ≈NOR r → R_transNOR p r.
Hint Resolve RtransNOR.
Lemma NORbis_trans : Transitive NORbisC.
Proof.
intros p q r Hio1 Hio2.
destruct Hio1 as (Hcp1 & Hcp2 & Hio1). destruct Hio2 as (_ & Hcp3 & Hio2).
splits¬. ∃ R_transNOR. split×. clear. splits.
unfold Symmetric. introv Hr. inverts Hr. econstructor.
applys× NORbisC_sym. applys× NORbisC_sym.
unfold tau_relation. introv Hr Ht. inverts Hr.
forwards (q´0 & Htq0 & Hpq´0): (>> NORbisC_tau p q0 H p´ Ht).
lets (q´ & Htq & Hpq´): (>> NORbisC_tau q0 q H0 Htq0).
∃ q´. split×.
unfold out_normal_relation. introv Hr Ht. inverts Hr.
lets (q0´ & q0´´ & Ht2 & Hq0): (>> NORbisC_out_normal p q0 H a p´ p´´ Ht).
lets (q´ & q´´ & Ht3 & Hq): (>> NORbisC_out_normal q0 q H0 a q0´ q0´´ Ht2).
apply NORbisC_sym in H0. ∃ q´ q´´. splits¬.
intros. specializes Hq0 m X H1 H3. applys¬ (cfresh_NORbis m q).
specializes Hq m X H2 H4. applys¬ (cfresh_NORbis m q).
destruct H as (_ & Hcp2 & _). unfolds.
lets Hcl : GV_trans_out Ht2.
unfolds in Hcp2; auto. rewrite Hcp2 in Hcl.
symmetry in Hcl; apply union_empty in Hcl. destruct Hcl as (_ & Hcl); rewrite Hcl; apply notin_empty.
apply (RtransNOR _ (wfp_Par (wfp_Abs m X q0´´) q0´) _).
apply Hq0.
destruct H as (_ & Hcp2 & _). unfolds.
lets (_ & Hcpq´´): cp_trans_out Hcp2 Ht2.
unfolds in Hcpq´´. rewrite Hcpq´´. apply notin_empty.
apply Hq.
unfold in_normal_relation. introv Hr H; inverts Hr.
lets (fq0 & Htfq & Hf0): (NORbisC_in_normal p q0 H0 a fp H).
lets (fq & Htq & Hf): (NORbisC_in_normal q0 q H1 a fq0 Htfq).
apply NORbisC_sym in H0. ∃ fq; splits¬.
intros. specializes Hf0 m H2.
specializes Hf m H3. applys¬ (cfresh_NORbis m q); applys ×NORbisC_sym.
apply (RtransNOR _ (wfp_inst_Abs fq0 (wfp_Send m wfp_Nil)) _).
apply Hf0. applys¬ (cfresh_NORbis m q); applys ×NORbisC_sym.
apply Hf.
econstructor. splits¬. apply Hcp2. apply Hio1.
splits¬.
Qed.
Lemma aux_fresh_rem: ∀ X ms (p p´ q q´ : wfprocess),
Forall (fun m : chan ⇒ m ### p ∧ m ### q) ms →
{{p--LabRem X->>AP p´}} → {{q--LabRem X->>AP q´}} →
Forall (fun m : chan ⇒ m ### p´ ∧ m ### q´) ms.
Proof.
induction ms; introv Hf Ht1 Ht2.
apply Forall_nil.
inverts Hf. apply Forall_cons.
split.
applys× (wfp_cfresh_rem a X p).
applys× (wfp_cfresh_rem a X q).
applys× IHms.
Qed.
Lemma NORbisE_sym: Symmetric NORbisE.
Proof.
introv H. unfolds NORbisE. intros. applys NORbisC_sym.
applys¬ H. rewrite¬ union_comm.
Qed.
Lemma NORbisE_out_normal: out_normal_relation NORbisE.
Proof.
apply NORbisE_ONE_ON.
introv Hbis Ht.
assert (∃ xs, permut xs (to_list (GV p \u GV q))). ∃ (to_list (GV p \u GV q)). permut_simpl.
lets Ht´: Ht.
destruct H as (xs & Hp).
lets Hbis´: Hbis. unfolds in Hbis´. specializes Hbis´ a Hp.
eapply (left413NOR (length xs)) in Hbis´; eauto. destruct Hbis´ as (ms & Hls & Hf & Hnd & Hnor).
asserts Hls´: (length xs = length (¬¬ms)). rewrite¬ wfp_length_opl.
eapply (wfp_trans_Msubst_out) in Ht.
apply (NORbisC_out_normal (wfp_multisubst (combine xs (¬¬ms)) p) (wfp_multisubst (combine xs (¬¬ms)) q)) in Ht; auto.
Focus 2.
symmetry; auto.
destruct Ht as (q´ & q´´ & Ht & Hpq´). apply wfp_trans_Msubst_name_out in Ht; auto.
destruct Ht as (q´0 & q´´0 & Ht & Hr1 & Hr2). substs.
∃ q´0 q´´0. split¬.
lets (m & Hfs): wfp_find_fresh_chan (p::q::¬¬ms). inverts Hfs as Hfmp Hfs. inverts Hfs as Hfmq Hfms.
lets (X & Hfs): find_fresh ((proc p´´)::(proc q´´0)::(^xs)). inverts Hfs as HfXp Hfs. inverts Hfs as HfXq Hfxs.
∃ m X. splits¬.
eapply (NORbisE_equiv (length xs) _ _ xs); eauto.
simpl. rewrite_all¬ gfresh_subst_rewrite.
lets: GV_trans_out. specializes H a p p´ p´´ Ht´. rewrite union_comm in H.
rewrite H in Hp. clear H.
lets: GV_trans_out. specializes H a q q´0 q´´0 Ht. rewrite union_comm in H.
rewrite H in Hp. clear H. apply Hp.
∃ ms. splits¬.
clear Hpq´ Hls´ Hnor Hnd Hls. apply wfp_Forall_cfresh_neq in Hfms. induction ms.
apply Forall_nil.
inverts Hfms. inverts Hf. destruct H3 as (Hneq & Hfa0p & Hfa0q).
lets (_ & Hfa0p1 & Hfa0p2): (wfp_cfresh_out a a0 p p´ p´´ Hfa0p Ht´).
lets (_ & Hfa0q1 & Hfa0q2): (wfp_cfresh_out a a0 q q´0 q´´0 Hfa0q Ht).
apply Forall_cons.
split; rewrite wfp_cfresh_par_iff. split¬.
rewrite¬ wfp_cfresh_Abs.
split¬.
rewrite¬ wfp_cfresh_Abs.
applys¬ IHms.
assert (¬Mem X xs).
clear Hpq´ Hls´ Hnor Hls Hp. induction xs.
rewrite Mem_nil_eq. rew_logic¬.
inverts Hfxs. rewrite Mem_cons_eq. rew_logic. split.
rewrite gfresh_gvar in H1. assumption.
apply¬ IHxs.
assert ( Forall (fun p0 : wfprocess ⇒ X # p0) (¬¬ms)).
clear Hfms Hpq´ Hls´ Hls Hnor Hf Hnd. induction ms; simpl.
apply Forall_nil.
apply¬ Forall_cons. simpl; rewrite gfresh_send. apply gfresh_nil.
apply wfp_Forall_cfresh_neq in Hfms.
rewrite_all¬ wfp_mult_sub_par. rewrite_all¬ wfp_mult_sub_Abs. applys¬ Hpq´.
applys¬ wfp_cfresh_Msubst1. applys¬ wfp_cfresh_Msubst1.
applys¬ wfp_fresh_Msubst1. apply wfp_cpl_opl. applys¬ wfp_fresh_Msubst1. apply wfp_cpl_opl.
clear Hpq´ Ht Hnor Hnd Hls Hls´. induction ms.
simpl; rewrite Mem_nil_eq. auto.
inverts Hf. rewrite Mem_cons_eq. rew_logic. split×.
Qed.
Lemma NORbisE_in: in_relation NORbisE.
Proof.
introv Hbis Ht.
assert (∃ xs, permut xs (to_list (GV p \u GV q))). ∃ (to_list (GV p \u GV q)). permut_simpl.
lets Ht´: Ht. destruct H as (xs & Hp).
lets Hbis´: Hbis. unfolds in Hbis´. specializes Hbis´ a Hp.
eapply (left413NOR (length xs)) in Hbis´; eauto. destruct Hbis´ as (ms & Hls & Hf & Hnd & Hnor).
asserts Hls´: (length xs = length (¬¬ms)). rewrite¬ wfp_length_opl.
rename Ht into Ht´´.
generalize (wfp_trans_Msubst_in a xs (¬¬ms) p fp Ht´´ Hls´); intro Ht.
destruct Ht as (fp´ & Ht & Hfp´). lets Htfp´: Ht.
generalize (NORbisC_in_normal (wfp_multisubst (combine xs (¬¬ms)) p) (wfp_multisubst (combine xs (¬¬ms)) q) Hnor a fp´ Ht); intro Ht´´´.
destruct Ht´´´ as (fq´ & Ht´´´ & Hpq´). lets Htfq´: Ht´´´. symmetry in Hls.
generalize (wfp_trans_Msubst_name_in a xs ms q fq´ Ht´´´ Hls); intro Ht4.
destruct Ht4 as (fq & Ht4 & Hfq´).
∃ fq; splits¬.
introv Hf1 Hf2.
lets (m & Hf´): wfp_find_fresh_chan (p::q::(¬¬ms)).
inverts Hf´. inverts H2.
assert (m###(wfp_multisubst (combine xs (¬¬ms)) p)).
applys¬ wfp_cfresh_Msubst1.
clear Htfp´ Htfq´ Hfp´ Hfq´ Hpq´ Hls´ Hnor Hnd Hf Hls Ht Ht´´´. induction ms.
apply Forall_nil.
inverts H4. simpl in H2; rewrite cfresh_send in H2. destruct H2 as (_ & Hneq).
applys¬ Forall_cons.
assert (m###(wfp_multisubst (combine xs (¬¬ms)) q)).
applys¬ wfp_cfresh_Msubst1.
clear Htfp´ Htfq´ Hfp´ Hfq´ Hpq´ Hls´ Hnor Hnd Hf Hls H Ht Ht´´´. induction ms.
apply Forall_nil.
inverts H4. simpl in H2; rewrite cfresh_send in H2. destruct H2 as (_ & Hneq).
applys¬ Forall_cons.
specializes Hpq´ m H H0.
rewrite (wfp_inst_subst _ a X (wfp_multisubst (combine xs (¬¬ms)) p)) in Hpq´; auto.
rewrite (wfp_inst_subst _ a X (wfp_multisubst (combine xs (¬¬ms)) q) (wfp_Send m wfp_Nil)) in Hpq´; auto.
rewrite¬ Hfp´ in Hpq´. rewrite¬ Hfq´ in Hpq´.
clear Htfq´ Htfp´. replace Ht´´ with Ht´ in Hfp´, Hpq´ by (apply proof_irrelevance); clear Ht´´; rename Ht4 into Ht´´.
lets (b1 & dec1) : (const_abs_decidable fp). lets (b2 & dec2) : (const_abs_decidable fq).
destruct b1, b2; symmetry in dec1, dec2.
rewrite isTrue_def in dec1, dec2. cases_if. cases_if. clear dec1 dec2.
lets Hfi1: GV_trans_in_const Ht´ H5 (wfp_Gvar X).
lets Hfi2: GV_trans_in_const Ht´´ H2 (wfp_Gvar X).
eapply (NORbisE_equiv (length (xs)) _ _ (xs)); eauto.
simpl; rewrite Hfi1, Hfi2; assumption.
∃ ms. splits¬.
simpl; clear Ht´´´ Ht Hfp´ Hfq´ Hpq´ Hls´ Hnor Hnd Hls H H0 H4; simpl. induction ms.
apply Forall_nil.
inverts Hf. destruct H4 as (_&Hfp&Hfq). apply Forall_cons. split.
applys¬ (wfp_cfresh_in a a0 p fp). apply cfresh_gvar.
applys¬ (wfp_cfresh_in a a0 q fq). apply cfresh_gvar.
applys¬ IHms.
rewrite wfp_gfresh_subst_rewrite in Hpq´. rewrite wfp_gfresh_subst_rewrite in Hpq´. assumption.
applys× wfp_fresh_Msubst1.
unfolds; simpl; rewrite¬ Hfi2.
apply wfp_cpl_opl.
applys× wfp_fresh_Msubst1.
unfolds; simpl; rewrite¬ Hfi1.
apply wfp_cpl_opl.
rewrite isTrue_def in dec1, dec2. cases_if. cases_if. clear dec1 dec2.
lets Hfi1: GV_trans_in_const Ht´ H5 (wfp_Gvar X).
lets Hfi2: GV_trans_in Ht´´ H2 (wfp_Gvar X).
eapply (NORbisE_equiv (length (X::xs)) _ _ (X::xs)); eauto.
simpl; rewrite Hfi1, Hfi2. rewrite union_assoc.
apply permut_sym. eapply permut_trans. apply permut_sym.
apply to_list_cons_union. rewrite notin_union. split¬.
apply permut_rem1_l.
rewrite Mem_cons_eq. left¬.
simpl. cases_if.
apply¬ permut_sym.
∃ (m::ms). splits.
rewrite_all length_cons. nat_math.
apply Forall_cons. split.
applys¬ (wfp_cfresh_in a m p fp). apply cfresh_gvar.
applys¬ (wfp_cfresh_in a m q fq). apply cfresh_gvar.
clear Ht´´´ Ht Hfp´ Hfq´ Hpq´ Hls´ Hnor Hnd Hls H H0 H4; simpl. induction ms.
apply Forall_nil.
inverts Hf. destruct H4 as (_&Hfp&Hfq). apply Forall_cons. split.
applys¬ (wfp_cfresh_in a a0 p fp). apply cfresh_gvar.
applys¬ (wfp_cfresh_in a a0 q fq). apply cfresh_gvar.
applys¬ IHms.
simpl. split¬.
clear Ht´´´ Ht Hfp´ Hfq´ Hpq´ Hls´ Hnor Hnd Hls H H0 Hf; simpl. induction ms.
rewrite Mem_nil_eq. rew_logic¬.
inverts H4; simpl in H6; rewrite cfresh_send in H6. destruct H6 as (_&Hneq).
rewrite Mem_cons_eq. rew_logic. split¬.
simpls¬.
rewrite isTrue_def in dec1, dec2. cases_if. cases_if. clear dec1 dec2.
lets Hfi1: GV_trans_in Ht´ H5 (wfp_Gvar X).
lets Hfi2: GV_trans_in_const Ht´´ H2 (wfp_Gvar X).
eapply (NORbisE_equiv (length (X::xs)) _ _ (X::xs)); eauto.
simpl; rewrite Hfi1, Hfi2.
rewrite <- union_assoc. rewrite union_comm_assoc. rewrite union_comm.
apply permut_sym. eapply permut_trans. apply permut_sym.
apply to_list_cons_union. rewrite notin_union. split¬.
apply permut_rem1_l.
rewrite Mem_cons_eq. left¬.
simpl. cases_if.
apply¬ permut_sym.
∃ (m::ms). splits.
rewrite_all length_cons. nat_math.
apply Forall_cons. split.
applys¬ (wfp_cfresh_in a m p fp). apply cfresh_gvar.
simpl; applys¬ (wfp_cfresh_in a m q fq). apply cfresh_gvar.
clear Ht´´´ Ht Hfp´ Hfq´ Hpq´ Hls´ Hnor Hnd Hls H H0 H4; simpl. induction ms.
apply Forall_nil.
inverts Hf. destruct H4 as (_&Hfp&Hfq). apply Forall_cons. split.
applys¬ (wfp_cfresh_in a a0 p fp). apply cfresh_gvar.
applys¬ (wfp_cfresh_in a a0 q fq). apply cfresh_gvar.
applys¬ IHms.
simpl. split¬.
clear Ht´´´ Ht Hfp´ Hfq´ Hpq´ Hls´ Hnor Hnd Hls H H0 Hf; simpl. induction ms.
rewrite Mem_nil_eq. rew_logic¬.
inverts H4; simpl in H6; rewrite cfresh_send in H6. destruct H6 as (_&Hneq).
rewrite Mem_cons_eq. rew_logic. split¬.
simpls¬.
rewrite isTrue_def in dec1, dec2. cases_if. cases_if. clear dec1 dec2.
lets Hfi1: GV_trans_in Ht´ H5 (wfp_Gvar X).
lets Hfi2: GV_trans_in Ht´´ H2 (wfp_Gvar X).
eapply (NORbisE_equiv (length (X::xs)) _ _ (X::xs)); eauto.
simpl; rewrite Hfi1, Hfi2. rewrite union_comm_assoc. rewrite <- union_assoc.
rewrite union_same. simpl. rewrite union_assoc.
apply permut_sym. eapply permut_trans. apply permut_sym.
apply to_list_cons_union. rewrite notin_union. split¬.
apply permut_rem1_l.
rewrite Mem_cons_eq. left¬.
simpl. cases_if.
apply permut_sym. rewrite¬ union_comm.
∃ (m::ms). splits.
rewrite_all length_cons. nat_math.
apply Forall_cons. split.
applys¬ (wfp_cfresh_in a m p fp). apply cfresh_gvar.
simpl; applys¬ (wfp_cfresh_in a m q fq). apply cfresh_gvar.
clear Ht´´´ Ht Hfp´ Hfq´ Hpq´ Hls´ Hnor Hnd Hls H H0 H4; simpl. induction ms.
apply Forall_nil.
inverts Hf. destruct H4 as (_&Hfp&Hfq). apply Forall_cons. split.
applys¬ (wfp_cfresh_in a a0 p fp). apply cfresh_gvar.
applys¬ (wfp_cfresh_in a a0 q fq). apply cfresh_gvar.
applys¬ IHms.
simpl. split¬.
clear Ht´´´ Ht Hfp´ Hfq´ Hpq´ Hls´ Hnor Hnd Hls H H0 Hf; simpl. induction ms.
rewrite Mem_nil_eq. rew_logic¬.
inverts H4. simpl in H6; rewrite cfresh_send in H6. destruct H6 as (_&Hneq).
rewrite Mem_cons_eq. rew_logic. split¬.
simpls¬.
rewrite <- from_list_spec. apply permut_from_list in Hp.
rewrite Hp. rewrite from_to_list. rewrite in_union. rew_logic. split.
unfolds¬ fresh_chan.
unfolds¬ fresh_chan.
rewrite <- from_list_spec. apply permut_from_list in Hp.
rewrite Hp. rewrite from_to_list. rewrite in_union. rew_logic. split.
unfolds¬ fresh_chan.
unfolds¬ fresh_chan.
applys¬ wfp_fresh_Msubst1.
apply wfp_cpl_opl.
applys¬ wfp_fresh_Msubst1.
apply wfp_cpl_opl.
Qed.
Lemma leave_permut_fst: ∀ xs ps E, length xs = length ps → noDup xs →
E \c from_list xs → permut (fst (split (leave E (combine xs ps)))) (to_list E).
Proof.
induction xs; introv Hls Hnd Hfl.
simpl. rewrite from_list_nil in Hfl. apply subset_of_empty in Hfl.
subst. apply permut_ndfl.
simpls¬.
apply nodup_tolist.
rewrite from_to_list. apply from_list_nil.
lets Hls´: Hls. rewrite length_cons in Hls´. symmetry in Hls´.
apply lengthn in Hls´. destruct Hls´ as (p & ps´ & Hps). subst.
rewrite_all length_cons in Hls.
simpls. cases_if.
rewrite fst_split_cons. simpl. apply permut_rem1_l.
rewrite <- from_list_spec. rewrite¬ from_to_list.
apply permut_sym. eapply permut_trans. apply rem1_to_list_perm.
apply permut_sym. rewrite× (leave_red_set E xs ps´ a). applys× IHxs.
unfolds subset. introv Hin. rewrite in_remove in Hin. destruct Hin as (Hin & Hneq).
specializes Hfl Hin. rewrite from_list_cons in Hfl. rewrite in_union in Hfl. destruct¬ Hfl.
false.
applys× IHxs.
rewrite from_list_cons in Hfl. unfolds subset. introv H´.
specializes Hfl x H´. rewrite in_union in Hfl. rewrite in_singleton in Hfl.
destruct¬ Hfl.
subst. false.
Qed.
Lemma NORbisE_tau: tau_relation NORbisE.
Proof.
introv Hbis Ht. assert (∃ xs, permut xs (to_list (GV p \u GV q))). ∃ (to_list (GV p \u GV q)). permut_simpl.
destruct H as (xs & Hp).
eapply (NORbisE_equiv (length xs) _ _ xs) in Hbis; eauto.
destruct Hbis as (ms & Hls & Hfs & Hnd & Hnor).
lets Htp´: Ht.
asserts Hls´´: (length xs = length (¬¬ms)). rewrite¬ wfp_length_opl.
eapply wfp_trans_Msubst_tau in Ht; eauto; try apply wfp_cpl_opl.
eapply (NORbisC_tau _ (wfp_multisubst (combine xs (¬¬ms)) q)) in Ht; eauto.
destruct Ht as (aq & Ht & Hpq´).
apply wfp_trans_Msubst_name_tau in Ht; auto.
Focus 2.
clear Hls Hls´´ Hnd Hnor Htp´ Hls Ht Hpq´.
induction ms; simpls*; constructor; inverts× Hfs.
destruct Ht as (q´ & Htq´ & Haq). subst.
∃ q´. split¬.
lets Htp: Htp´. apply wfp_decomposition_tau1 in Htp´.
destruct Htp´ as (a & p1 & p´´ & fp & Hpout & Hpin & Hps).
lets Htq: Htq´. apply wfp_decomposition_tau1 in Htq´.
destruct Htq´ as (c & q1 & q´´ & fq & Hqout & Hqin & Hqs).
lets (b1 & dec1) : (const_abs_decidable fp). lets (b2 & dec2) : (const_abs_decidable fq).
destruct b1, b2; symmetry in dec1, dec2; rewrite isTrue_def in dec1, dec2; cases_if; cases_if; clear dec1 dec2.
eapply (NORbisE_equiv (length (leave (GV p1 \u GV q1) (combine xs (¬¬ms)))) _ _ (fst (split (leave (GV p1 \u GV q1) (combine xs (¬¬ms)))))); eauto.
forwards Hgvp: GV_trans_out Hpout.
forwards Hgvq: GV_trans_out Hqout.
lets Hgvp1: GV_trans_in_const a p1 fp Hpin H0.
lets Hgvq1: GV_trans_in_const c q1 fq Hqin H.
rewrite Hqs; simpl; subst; simpl. rewrite (Hgvp1 p´´), (Hgvq1 q´´).
applys¬ leave_permut_fst.
eapply permut_nodup. apply permut_sym. apply Hp. apply nodup_tolist.
apply permut_from_list in Hp. rewrite Hp. rewrite from_to_list.
rewrite Hgvp, Hgvq. unfolds subset. introv H´.
rewrite <- union_assoc. rewrite union_comm_assoc.
rewrite (union_comm (GV p´´)). rewrite in_union. left.
rewrite union_assoc. rewrite in_union. left¬.
lets¬ (ns & Hns & Hm): (leave_ex (GV p1 \u GV q1) xs ms). ∃ ns. splits.
rewrite <- wfp_length_opl. rewrite <- Hns. rewrite¬ split_length_r. clear Hns.
rewrite <- Forall_Mem in *; introv Hm´.
specialize (Hm _ Hm´); specialize (Hfs _ Hm); split.
applys× (wfp_cfresh_tau x p p´).
applys× (wfp_cfresh_tau x q q´).
apply wfp_nodup_opl. rewrite <- Hns. apply leave_nodup_r.
rewrite¬ combine_split. simpl. applys¬ wfp_nodup_opl.
rewrite <- Hns. rewrite_all <- split_combine_fs.
rewrite_all× <- leave_not_fresh; try apply wfp_cpl_opl.
rewrite Hqs; simpl. rewrite¬ (GV_trans_in_const c q1 fq). apply subset_union_weak_r.
subst; simpl. rewrite¬ (GV_trans_in_const a p1 fp). apply subset_union_weak_l.
forwards Hgvp: GV_trans_out Hpout.
forwards Hgvq: GV_trans_out Hqout.
lets Hgvp1: GV_trans_in_const a p1 fp Hpin H0.
lets Hgvq1: GV_trans_in c q1 fq Hqin H.
eapply (NORbisE_equiv (length (leave (GV p1 \u GV q) (combine xs (¬¬ms)))) _ _ (fst (split (leave (GV p1 \u GV q) (combine xs (¬¬ms)))))); eauto.
rewrite Hqs; simpl; subst; simpl. rewrite Hgvp1, Hgvq1. rewrite <- Hgvq.
applys¬ leave_permut_fst.
eapply permut_nodup. apply permut_sym. apply Hp. apply nodup_tolist.
apply permut_from_list in Hp. rewrite Hp. rewrite from_to_list.
rewrite Hgvp. rewrite <- union_assoc. rewrite <- union_comm_assoc.
rewrite (union_comm (GV p´´)). apply subset_union_weak_l.
lets¬ (ns & Hns & Hm): (leave_ex (GV p1 \u GV q) xs ms). ∃ ns. splits.
rewrite <- wfp_length_opl. rewrite <- Hns. rewrite¬ split_length_r. clear Hns.
rewrite <- Forall_Mem in *; introv Hm´.
specialize (Hm _ Hm´); specialize (Hfs _ Hm); split.
applys× (wfp_cfresh_tau x p p´).
applys× (wfp_cfresh_tau x q q´).
apply wfp_nodup_opl. rewrite <- Hns. apply leave_nodup_r.
rewrite¬ combine_split. simpl. applys¬ wfp_nodup_opl.
rewrite <- Hns. rewrite_all <- split_combine_fs.
rewrite_all× <- leave_not_fresh; try apply wfp_cpl_opl.
rewrite Hqs; simpl. rewrite¬ (GV_trans_in c q1 fq). rewrite <- Hgvq. apply subset_union_weak_r.
subst; simpl. rewrite¬ (GV_trans_in_const a p1 fp). apply subset_union_weak_l.
forwards Hgvp: GV_trans_out Hpout.
forwards Hgvq: GV_trans_out Hqout.
lets Hgvp1: GV_trans_in a p1 fp Hpin H0.
lets Hgvq1: GV_trans_in_const c q1 fq Hqin H.
eapply (NORbisE_equiv (length (leave (GV p \u GV q1) (combine xs (¬¬ms)))) _ _ (fst (split (leave (GV p \u GV q1) (combine xs (¬¬ms)))))); eauto.
rewrite Hqs; simpl; subst; simpl. rewrite Hgvp1, Hgvq1. rewrite <- Hgvp.
applys¬ leave_permut_fst.
eapply permut_nodup. apply permut_sym. apply Hp. apply nodup_tolist.
apply permut_from_list in Hp. rewrite Hp. rewrite from_to_list.
rewrite Hgvq. rewrite union_assoc. apply subset_union_weak_l.
lets¬ (ns & Hns & Hm): (leave_ex (GV p \u GV q1) xs ms). ∃ ns. splits.
rewrite <- wfp_length_opl. rewrite <- Hns. rewrite¬ split_length_r. clear Hns.
rewrite <- Forall_Mem in *; introv Hm´.
specialize (Hm _ Hm´); specialize (Hfs _ Hm); split.
applys× (wfp_cfresh_tau x p p´).
applys× (wfp_cfresh_tau x q q´).
apply wfp_nodup_opl. rewrite <- Hns. apply leave_nodup_r.
rewrite¬ combine_split. simpl. applys¬ wfp_nodup_opl.
rewrite <- Hns. rewrite_all <- split_combine_fs.
rewrite_all× <- leave_not_fresh; try apply wfp_cpl_opl.
rewrite Hqs; simpl. rewrite¬ (GV_trans_in_const c q1 fq). apply subset_union_weak_r.
subst; simpl. rewrite¬ (GV_trans_in a p1 fp). rewrite <- Hgvp. apply subset_union_weak_l.
eapply (NORbisE_equiv (length xs) _ _ xs); eauto.
subst; simpl. rewrite¬ (GV_trans_in a p1). rewrite¬ (GV_trans_in c q1).
rewrite¬ <- (GV_trans_out a p). rewrite¬ <- (GV_trans_out c q).
∃ ms. splits¬.
clear Hnd Hnor Hls Hls´´ Hpq´. induction ms.
apply Forall_nil.
inverts Hfs. destruct H3 as (Hfp & Hfq). apply Forall_cons. split.
applys¬ (wfp_cfresh_tau a0 p p´).
applys¬ (wfp_cfresh_tau a0 q q´).
applys¬ IHms.
Qed.
Lemma NORbisE_var: var_relation NORbisE.
Proof.
introv Hbis Ht.
assert (∃ xs, permut xs (to_list (GV p \u GV q))). ∃ (to_list (GV p \u GV q)). permut_simpl.
destruct H as (xs & Hp). lets Ht´: Ht. lets Hbis´: NORbisE_equiv.
specializes Hbis´ Hp. destruct Hbis´ as (Hbis´ & _). reflexivity.
specializes Hbis´ Hbis. destruct Hbis´ as (ms & Hls & Hf & Hnd & Hnor).
asserts Hls´: (length xs = length (¬¬ms)). rewrite¬ wfp_length_opl.
asserts Hxm: (Mem X xs).
apply permut_from_list in Hp. rewrite from_to_list in Hp. rewrite <- from_list_spec.
rewrite Hp. rewrite in_union. left. applys¬ (GV_trans_rem1 X p p´).
lets: sublists_3. specializes H X xs (¬¬ms).
edestruct H as (p0 & xs1 & xs2 & ps1 & ps2 & Happ1 & Happ2 & Hl1 & Hl2); auto. clear H.
lets (ms1 & ms2´ & Hms1 & Hms2´ & Hms): wfp_opl_app_ex Happ2.
lets (ms0 & ms2 & Hms0 & Hms2 & Hms´): wfp_opl_app_ex Hms2´. inverts Hms0.
apply wfp_opl_base in H0. destruct H0 as (m & Hp0 & Hs). subst ms0. rewrite Hms´ in Hms. clear Hms2´ Hms´.
asserts Hmm: (Mem m ms).
rewrite Hms. rew_app. rewrite Mem_app_or_eq. rewrite¬ Mem_cons_eq.
lets Hf´ : Hf; rewrite <- Forall_Mem in Hf; specialize (Hf _ Hmm); destruct Hf as (Hf1 & Hf2).
rewrite Happ1 in Hnor. rewrite Happ2 in Hnor. subst ps1 ps2 p0.
asserts Hl1´: (length xs1 = length ms1). rewrite¬ <- wfp_length_opl.
asserts Hl2´: (length xs2 = length ms2). rewrite¬ <- wfp_length_opl.
do 2 rewrite¬ permut_combine_step in Hnor; try (rewrite_all length_app; simpls~).
do 4 rewrite wfp_mult_sub_separate2 in Hnor. simpl in Hnor.
lets Hnd´: Hnd. rewrite Hms in Hnd´. rew_app in Hnd´. apply nodup_middle in Hnd´.
destruct Hnd´ as (H1 & H2). rewrite Mem_app_or_eq in H1. rew_logic in H1.
lets Hndms12: H2. apply nodup_app_inv in H2. destruct H1 as (Hnms1 & Hnms2).
destruct H2 as (Hndms1 & Hndms2).
lets Hnd´: (nodup_tolist (GV p \u GV q)).
lets Hndxs´: permut_sym Hp. apply permut_nodup in Hndxs´; auto. clear Hnd´.
lets Hndxs: Hndxs´.
rewrite Happ1 in Hndxs´. apply nodup_middle in Hndxs´.
destruct Hndxs´ as (H1 & H2). rewrite Mem_app_or_eq in H1. rew_logic in H1.
apply nodup_app_inv in H2. destruct H1 as (Hnxs1 & Hnxs2). destruct H2 as (Hndxs1 & Hndxs2).
do 2 rewrite¬ wfp_mult_sub_commute in Hnor; try apply wfp_cpl_opl; try unfolds¬.
apply (wfp_trans_rem_is_out m X) in Ht; replace Nil with (proc (wfp_Nil)) in Ht by auto.
eapply (wfp_trans_Msubst_out m) in Ht. Focus 2. apply Hl2´.
eapply (wfp_trans_Msubst_out m) in Ht. Focus 2. apply Hl1´.
lets Hff: Forall_forall (gfresh_nil). lets Hopl: wfp_cpl_opl.
rewrites¬ (wfp_fresh_Msubst_lemma xs2 (¬¬ms2) wfp_Nil) in Ht.
rewrites¬ (wfp_fresh_Msubst_lemma xs1 (¬¬ms1) wfp_Nil) in Ht.
eapply (NORbisC_out_normal _ (wfp_multisubst (combine xs1 (¬¬ms1)) (wfp_multisubst (combine xs2 (¬¬ms2)) (wfp_subst (wfp_Send m wfp_Nil) X q)))) in Ht; auto. destruct Ht as (q´2 & q´´2 & Ht & Hr).
eapply wfp_trans_Msubst_name_out in Ht; auto. destruct Ht as (q´1 & q´´1 & Ht & Hr1 & Hr2).
eapply wfp_trans_Msubst_name_out in Ht; auto. destruct Ht as (q´0 & q´´0 & Ht & Hr1´ & Hr2´).
apply wfp_trans_out_is_rem in Ht; auto. destruct Ht as (q´ & Ht & Hq1 & Hq2).
∃ q´. split¬.
lets (a & Htemp): wfp_find_fresh_chan (p::q::(¬¬ms)).
inverts Htemp. inverts H2. rewrite Happ2 in H4.
apply Forall_app_inv in H4. destruct H4.
apply Forall_app_inv in H0. destruct H0.
rewrite Forall_to_conj_1 in H0.
specializes Hr a X. rewrite Hr2 in Hr. rewrite Hr2´ in Hr. rewrite Hq2 in Hr.
rewrite¬ (wfp_fresh_Msubst_lemma xs2 (¬¬ms2) wfp_Nil) in Hr.
rewrite¬ (wfp_fresh_Msubst_lemma xs1 (¬¬ms1) wfp_Nil) in Hr.
apply NORbis_in_par in Hr; try apply gfresh_nil.
eapply (NORbis_trans _ _ q´2) in Hr.
apply NORbisC_sym in Hr. eapply (NORbis_trans _ _ (wfp_multisubst (combine xs1 (¬¬ms1)) (wfp_multisubst (combine xs2 (¬¬ms2))(wfp_subst (wfp_Send m wfp_Nil) X p´)))) in Hr.
apply NORbisC_sym in Hr. rewrite Hr1 in Hr. rewrite Hr1´ in Hr. rewrite Hq1 in Hr.
lets (b1 & dec1): fresh_gvar_decidable p´ X.
lets (b2 & dec2): fresh_gvar_decidable q´ X.
destruct b1, b2.
apply eq_true_l in dec1. rewrite istrue_isTrue in dec1.
apply eq_true_l in dec2. rewrite istrue_isTrue in dec2.
do 2 rewrite¬ wfp_gfresh_subst_rewrite in Hr.
eapply (NORbisE_equiv (length (xs1 ++ xs2)) _ _ (xs1++xs2)); eauto.
rewrite¬ (GV_trans_rem2 X p p´) in Hp. rewrite¬ (GV_trans_rem2 X q q´) in Hp.
rewrite union_comm_assoc in Hp. rewrite <- union_assoc in Hp.
rewrite union_same in Hp. rewrite union_comm_assoc in Hp.
assert (permut (X::(xs1++xs2)) xs).
rewrite Happ1. rewrite <- app_cons_one. permut_simpl.
erewrite permut_cons_iff. eapply permut_trans. apply H4.
apply permut_sym. eapply permut_trans. apply to_list_cons_union.
rewrite notin_union. splits¬. apply permut_sym. rewrite¬ <- union_assoc.
∃ (ms1 ++ ms2). splits¬.
rewrite_all length_app. rewrite_all <- wfp_length_opl. nat_math.
rewrite Hms in Hf´. apply Forall_app_inv in Hf´.
destruct Hf´ as (Hfs1 & Hf´). apply Forall_app_inv in Hf´. destruct Hf´ as (Hfm & Hfs2).
applys¬ Forall_app.
applys¬ (aux_fresh_rem X ms1 p p´ q q´).
applys¬ (aux_fresh_rem X ms2 p p´ q q´).
rewrite wfp_opl_app. rewrite¬ permut_combine_step. do 2 rewrite¬ wfp_mult_sub_separate2.
apply eq_true_l in dec1. rewrite istrue_isTrue in dec1.
apply eq_false_l in dec2. rewrite istrue_neg in dec2. rewrite istrue_isTrue in dec2.
eapply (NORbisE_equiv (length xs) _ _ xs); eauto.
unfolds¬ fresh_gvar. unfolds notin. rew_logic in dec2.
rewrite¬ <- (union_already_in dec2). rewrite¬ <- (union_already_in dec2).
rewrite (union_comm \{X} (GV q´)).
rewrite¬ <- (GV_trans_rem2 X q). rewrite union_assoc. rewrite¬ <- (GV_trans_rem2 X p).
∃ ms. splits¬.
applys¬ (aux_fresh_rem X ms p p´ q q´).
rewrite Happ1, Happ2. rewrite¬ permut_combine_step. rewrite¬ permut_combine_step.
do 4 rewrite wfp_mult_sub_separate2. simpl.
rewrite_all¬ wfp_mult_sub_commute; try apply wfp_cpl_opl; try unfolds¬.
rewrite_all length_app. simpls¬.
apply eq_false_l in dec1. rewrite istrue_neg in dec1. rewrite istrue_isTrue in dec1.
apply eq_true_l in dec2. rewrite istrue_isTrue in dec2.
eapply (NORbisE_equiv (length xs) _ _ xs); eauto.
unfolds¬ fresh_gvar. unfolds notin. rew_logic in dec1.
rewrite¬ <- (union_already_in dec1). rewrite¬ <- (union_already_in dec1).
rewrite union_comm. rewrite union_assoc.
rewrite¬ <- (GV_trans_rem2 X q). rewrite (union_comm \{X} (GV p´)). rewrite¬ <- (GV_trans_rem2 X p).
rewrite¬ union_comm.
∃ ms. splits¬.
applys¬ (aux_fresh_rem X ms p p´ q q´).
rewrite Happ1, Happ2. rewrite¬ permut_combine_step. rewrite¬ permut_combine_step.
do 4 rewrite wfp_mult_sub_separate2. simpl.
rewrite_all¬ wfp_mult_sub_commute; try apply wfp_cpl_opl; try unfolds¬.
rewrite_all length_app. simpls¬.
apply eq_false_l in dec2. rewrite istrue_neg in dec2. rewrite istrue_isTrue in dec2.
apply eq_false_l in dec1. rewrite istrue_neg in dec1. rewrite istrue_isTrue in dec1.
eapply (NORbisE_equiv (length xs) _ _ xs); eauto.
unfolds¬ fresh_gvar. unfolds notin. rew_logic in dec1. rew_logic in dec2.
rewrite¬ <- (union_already_in dec1). rewrite¬ <- (union_already_in dec2).
rewrite (union_comm \{X} (GV p´)). rewrite (union_comm \{X} (GV q´)).
rewrite¬ <- (GV_trans_rem2 X p). rewrite¬ <- (GV_trans_rem2 X q).
∃ ms. splits¬.
applys¬ (aux_fresh_rem X ms p p´ q q´).
rewrite Happ1, Happ2. rewrite¬ permut_combine_step. rewrite¬ permut_combine_step.
do 4 rewrite wfp_mult_sub_separate2. simpl.
rewrite_all¬ wfp_mult_sub_commute; try apply wfp_cpl_opl; try unfolds¬.
rewrite_all length_app. simpls¬.
inversion Hr as (Hcpq´2 & Hcpp´ & _). simpl in Hcpp´. apply cp_par in Hcpp´. destructs Hcpp´.
splits¬. applys¬ cp_par. applys¬ NORbis_congr_par_nil.
inversion Hr as (Hcpq´2 & Hcpp´ & _). simpl in Hcpp´. apply cp_par in Hcpp´. destructs Hcpp´.
splits¬. applys¬ cp_par. applys¬ NORbis_congr_par_nil.
subst q´2 q´1 q´0. applys¬ wfp_cfresh_Msubst1. applys¬ wfp_cfresh_Msubst1. applys¬ wfp_cfresh_subst_in.
applys¬ (wfp_cfresh_rem a X q q´). applys¬ wfp_Forall_cfresh_neq. applys¬ wfp_Forall_cfresh_neq.
applys¬ wfp_cfresh_Msubst1. applys¬ wfp_cfresh_Msubst1. applys¬ wfp_cfresh_subst_in.
applys¬ wfp_Forall_cfresh_neq. applys¬ wfp_Forall_cfresh_neq.
applys¬ wfp_cfresh_Msubst1. applys¬ wfp_cfresh_Msubst1. applys¬ wfp_cfresh_subst_in.
applys¬ wfp_Forall_cfresh_neq. applys¬ wfp_Forall_cfresh_neq.
Qed.
Lemma NORbisE_ONORbis: OpenNormal_bisimulation NORbisE.
Proof.
splits.
apply NORbisE_sym.
apply NORbisE_tau.
apply NORbisE_out_normal.
apply NORbisE_in.
apply NORbisE_var.
Qed.
Lemma ONORbis_out: out_relation ONORbis.
Proof.
unfolds. introv Hbis Ht.
apply ONORbis_out_normal in Hbis; auto.
specializes Hbis (>> a p´ p´´ Ht).
destruct Hbis as (q´ & q´´ & Htq & H).
∃ q´ q´´. split¬.
lets (m & Hf): wfp_find_fresh_chan (p::q::nil).
rewrite Forall_to_conj_2 in Hf. destruct Hf as (Hf1 & Hf2).
lets (X & Hf): find_fresh ((proc p´´)::(proc q´´)::nil).
rewrite Forall_to_conj_2 in Hf. destruct Hf as (Hf3 & Hf4).
lets Ht´ : Ht; apply (wfp_cfresh_out a m p p´ p´´) in Ht; auto. destruct Ht as (_ & Hf5 & Hf6).
lets Htq´ : Htq; apply (wfp_cfresh_out a m q q´ q´´) in Htq; auto. destruct Htq as (_& Hf7 & Hf8).
specializes H (>> m X Hf1 Hf2 Hf3 Hf4). apply¬ (lemma415 p´ p´´ q´ q´´ m X).
Qed.
Lemma ONORbis_IObis: IO_bisimulation ONORbis.
Proof.
splits.
apply ONORbis_sym.
apply ONORbis_in.
apply ONORbis_out.
apply ONORbis_var.
Qed.