Library HOC15HObis

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.

Inductive R_refl : RelWfP :=
| Rrefl : ∀ p, R_refl p p.

Hint Resolve Rrefl.

Lemma HObis_refl : Reflexive HObis.
Proof.
  intro p. unfolds. ∃ R_refl. split¬.
    clear p. unfolds. splits; unfolds; introv Hr.
    inverts Hr. constructor.
    introv Ht. inverts Hr. ∃ p´. split¬.
    introv Ht. inverts Hr. ∃ p´ p´´. split¬.
    introv. inverts Hr. ∃ fp. split¬.
Qed.

Lemma HObis_sym : Symmetric HObis.
Proof.
  introv H. destruct H as (R & HO & HR).
  ∃ R. split¬. apply¬ HO.
Qed.

Lemma HObisC_sym : Symmetric HObisC.
Proof.
  introv H. destruct H as (Hcp1 & Hcp2 & H). splits¬. apply¬ HObis_sym.
Qed.

Lemma HObis_tau : tau_relation HObis.
Proof.
  unfolds.
  introv Hio Ht. unfolds in Hio.
  destruct Hio as (R & HO & HR).
  assert (∃ (q´ : wfprocess), {{q -- Tau ->> AP q´}} ∧ R p´ q´).
  unfold HigherOrder_bisimulation, tau_relation in HO. eapply HO.
  apply HR.
  assumption. inversion H as (q´ & Hq).
  ∃ q´. split. apply Hq.
  ∃ R. split. apply HO. apply Hq.
Qed.

Lemma HObisC_tau: tau_relation HObisC.
Proof.
  introv Hio Ht. destruct Hio as (Hcp1 & Hcp2 & Hio).
  apply HObis_tau in Hio; auto. destruct (Hio _ Ht) as (q´ & Ht´ & Hio´).
  lets Hcp3: cp_trans_tau Hcp1 Ht. lets Hcp4: cp_trans_tau Hcp2 Ht´.
  ∃ q´. unfolds HObisC. splits¬.
Qed.

Lemma HObis_out : out_relation HObis.
Proof.
  introv Hio Ht.
  inversion Hio as [R HR].
  assert (∃ (q´ q´´ : wfprocess), ({{q--LabOut a q´´->>(AP q´)}} ∧ (R p´ q´) ∧ (R p´´ q´´))).
  unfold HigherOrder_bisimulation, out_relation in HR. eapply HR. apply HR.
  eassumption. inversion H as [q´ Hex]. inversion Hex as [q´´ Hq].
  ∃ q´ q´´. split. apply Hq. split.
  ∃ R. split. apply HR. apply Hq.
  ∃ R. split. apply HR. apply Hq.
Qed.

Lemma HObisC_out: out_relation HObisC.
Proof.
  introv Hio Ht. destruct Hio as (Hcp1 & Hcp2 & Hio).
  apply HObis_out in Hio; auto. destruct (Hio _ _ _ Ht) as (q´ & q´´ & Ht´ & Hio´ & Hio´´).
  lets (Hcp3 & Hcp3´): cp_trans_out Hcp1 Ht. lets (Hcp4 & Hcp4´): cp_trans_out Hcp2 Ht´.
  ∃ q´ q´´. unfolds HObisC. splits¬.
Qed.

Lemma HObis_closed : closed_relation HObis.
Proof.
  introv Hio Ht.
  inversion Hio as (R & HR & Hr).
  lets HR´ : HR; destruct HR´ as (_ & _ & _ & Hc).
  specializes Hc Hr Ht. destruct Hc as (fq & Htq & Hrq).
  ∃ fq; splits¬.
  introv HC; ∃× R.
Qed.

Lemma HObisC_closed: closed_relation HObisC.
Proof.
  introv Hio Ht. destruct Hio as (Hcp1 & Hcp2 & Hio).
  apply HObis_closed in Hio; auto. destruct (Hio _ _ Ht) as (fq & Ht´ & Hio´).
  ∃ fq. splits¬. introv Hclr.
  unfolds HObisC; splits~; simpls¬.
  apply cp_trans_in with (a := a) (p := p); jauto.
  apply cp_trans_in with (a := a) (p := q); jauto.
Qed.

Lemma HObicC_var : var_relation HObisC.
Proof.
  introv (Hcp & Hcq & Hbis); introv Ht.
    assert (Hf : X \in unguardeds p).
      rewrite wfp_unguarded_remove_iff; ∃¬ p´.
      apply unguardeds_invariant in Hf; rewrite Hcp in Hf; rewrite× in_empty in Hf.
Qed.

Inductive R_ch: binary wfprocess :=
  | R_ch_base: ∀ a b X p q,
      (wfp_Abs a X p) ≈HO (wfp_Abs a X q) → R_ch (wfp_Abs b X p) (wfp_Abs b X q)
  | R_ch_bis: ∀ p q, p ≈HO q → R_ch p q.

Hint Resolve R_ch_bis R_ch_base.

Lemma HObisR_ch : HigherOrder_bisimulation R_ch.
Proof with automate.
  splits.
  introv H. inverts H.
    apply HObisC_sym in H0. applys× R_ch_base.
    apply R_ch_bis. apply¬ HObisC_sym.

  unfolds. introv Hr Ht. inverts Hr.
    inverts Ht.
    apply HObisC_tau in H; auto. destruct (H _ Ht) as ( q´ & Ht´ & H´).
    ∃ q´. splits¬.

  unfolds. introv Hr Ht. inverts Hr.
    inverts Ht.
    apply HObisC_out in H; auto. destruct (H _ _ _ Ht) as (q´ & q´´ & Ht´ & H´ & H´´).
    ∃ q´ q´´. splits¬.

  introv Hr Ht. inverts Hr.

  2: apply HObisC_closed in H; destruct (H _ _ Ht) as (fq & Ht´ & H´); ∃¬ fq.

  lets Heq : wfp_trans_in_chan_eq Ht; subst.
  eexists; splits... introv Hc.
  lets Ht0 : TrIn a0 X p0.
    apply HObisC_closed in H. specializes H Ht0.
    destruct H as (fq & Htq & Hc´). specializes Hc´ Hc.
    lets Hyp1 : wfp_trans_in_abs_eq Ht; inverts Hyp1 as Hyp1;
    lets Hyp2 : wfp_trans_in_abs_eq Htq; inverts Hyp2 as Hyp2; substs~;
      constructor; simpls.
      destruct Hyp2 as (Y & HneqY & Hfy & Heq); subst; simpls.
      rewrite <- wfp_subst_decomposition_g in Hc´...
      destruct Hyp1 as (Y & HneqY & Hfy & Heq); subst; simpls.
      rewrite <- wfp_subst_decomposition_g...
      destruct Hyp1 as (Z & HneqZ & Hfz & Heq); subst;
      destruct Hyp2 as (Y & HneqY & Hfy & Heq); subst; simpls.
      rewrite <- wfp_subst_decomposition_g in ×...
Qed.

Inductive R_r: binary wfprocess :=
  | R_r_base: ∀ p q a X, (∀ r : wfprocess, closed_process r →
      ((wfp_subst r X p) ≈HO (wfp_subst r X q))) → R_r (wfp_Abs a X p) (wfp_Abs a X q)
  | R_r_bis: ∀ p q, p ≈HO q → R_r p q.

Hint Resolve R_r_bis R_r_base.

Lemma HObisR_r : HigherOrder_bisimulation R_r.
Proof with automate.
  splits.
  unfolds. introv H. inverts H.
    applys× R_r_base. intros. applys¬ HObisC_sym.
    constructor. apply¬ HObisC_sym.

  introv Hr Ht. inverts Hr.
    inverts Ht.
    apply HObisC_tau in H; auto. destruct (H _ Ht) as ( q´ & Ht´ & H´).
    ∃ q´. splits¬.

  unfolds. introv Hr Ht. inverts Hr.
    inverts Ht.
    apply HObisC_out in H; auto. destruct (H _ _ _ Ht) as (q´ & q´´ & Ht´ & H´ & H´´).
    ∃ q´ q´´. splits¬.

  introv Hr Ht. inverts Hr.

  2: apply HObisC_closed in H; destruct (H _ _ Ht) as (fq & Ht´ & H´); ∃¬ fq.

  lets Heq : wfp_trans_in_chan_eq Ht; subst.
  eexists; splits... introv Hc.
  lets Hyp : wfp_trans_in_abs_eq Ht; inverts Hyp as Hyp; substs¬.
    simpl; constructor...
    destruct Hyp as (Y & HneqY & Hfy & Heq); subst; simpls.
    rewrite <- wfp_subst_decomposition_g...
Qed.

Lemma HObis_congr_receive : ∀ a X p q, (∀ r : wfprocess, closed_process r →
    (wfp_subst r X p) ≈HO (wfp_subst r X q)) → (wfp_Abs a X p) ≈HO (wfp_Abs a X q).
Proof with automate.
  introv Hr. lets : Hr.
  specializes Hr wfp_Nil. specializes Hr...
    simpl; unfolds¬.
  destruct Hr as (Hcp1 & Hcp2 & _); simpl in Hcp1; simpl in Hcp2.
  unfolds closed_process; simpl.
  rewrite GV_subst_cp in *; unfolds¬.
  splits~; unfold closed_process; simpls~;
    try rewrite GV_subst_cp in *; try unfolds...
  ∃ R_r. split...
    apply HObisR_r.
Qed.

Inductive R_trans : binary wfprocess :=
| Rtrans : ∀ p q r, HObis p q → HObis q r → R_trans p r.

Hint Resolve Rtrans.

Lemma HObis_trans : Transitive HObis.
Proof with automate.
  intros p q r Hio1 Hio2. ∃ R_trans. split.
    clear p q r Hio1 Hio2. unfolds. splits.
      unfold Symmetric. introv Hr. inverts Hr. econstructor.
        applys× HObis_sym. applys× HObis_sym.
      unfold tau_relation. introv Hr Ht. inverts Hr.
        lets (q´0 & Htq0 & Hpq´0): (>> HObis_tau p q0 H p´ Ht).
        lets (q´ & Htq & Hpq´): (>> HObis_tau q0 q H0 q´0 Htq0).
        ∃ q´. split×.
      unfold out_relation. introv Hr Ht. inverts Hr.
        lets (q0´ & q0´´ & Ht2 & Hq0): (>> HObis_out p q0 H a p´ p´´ Ht).
        lets (q´ & q´´ & Hq): (>> HObis_out q0 q H0 a q0´ q0´´ Ht2).
        ∃ q´ q´´. splits×.
      unfold closed_relation. introv Hr Ht. inverts Hr.
        lets (q´0 & Htq0 & Hpq´0): (HObis_closed p q0 H a fp Ht).
        lets (q´ & Htq & Hpq´): (HObis_closed q0 q H0 a q´0 Htq0).
        ∃ q´; splits...
    econstructor; eassumption.
Qed.

Lemma HObisC_trans : Transitive HObisC.
Proof.
  introv Hio1 Hio2.
  destruct Hio1 as (Hcpp & Hcpq & Hio1). destruct Hio2 as (_ & Hcpr & Hio2).
  splits¬. applys× HObis_trans.
Qed.

Instance HObis_is_eq_rel : Equivalence HObis.
Proof.
  split. apply HObis_refl. apply HObis_sym. apply HObis_trans.
Qed.

Hint Resolve HObis_refl HObis_sym HObis_trans.

Inductive R_nil : binary wfprocess :=
| Rn1 : ∀ p, (R_nil p (wfp_Par wfp_Nil p))
| Rn2 : ∀ p, (R_nil (wfp_Par wfp_Nil p) p)
| Rnrefl : ∀ p, (R_nil p p).

Hint Resolve Rn1 Rn2 Rnrefl.

Lemma HObis_congr_par_nil : ∀ p,
  HObis (wfp_Par wfp_Nil p) p.
Proof with automate.
  introv. ∃ R_nil. split¬.
    clear p. splits.
      introv Hr. inverts× Hr.

      introv Hr Ht. inverts Hr.
        ∃ (wfp_Par wfp_Nil p´). splits...
        inverts Ht...
          destruct ap; inverts H3. inverts H2.
          destruct aq; inverts H3.
          eexists. splits...
          inverts H2.
          inverts H2.
        ∃ p´. splits...

      introv Hr Ht. inverts Hr.
        ∃ (wfp_Par wfp_Nil p´) p´´. splits...
        inverts Ht...
          inverts H2.
          destruct aq; inverts H3.
          eexists; eexists. splits...
          ∃ p´ p´´; split¬.

      introv Hr Ht. inverts Hr.
        ∃ (AbsPar2 wfp_Nil fp). splits...
        introv Hcpr. simpls¬.
        inverts Ht...
          inverts H2.
          destruct aq; inverts H3.
          eexists; splits...
          introv Hcpr. simpls¬.
        ∃¬ fp.
Qed.

Inductive R_receive : binary wfprocess :=
| Rabs : ∀ a X p q, p ≈HO q → R_receive (wfp_Abs a X p) (wfp_Abs a X q)
| Rbis : ∀ p q, p ≈HO q → R_receive p q.

Hint Constructors R_receive.

Lemma HObis_congr_abs : ∀ a X p q,
  p ≈HO q → (wfp_Abs a X p) ≈HO (wfp_Abs a X q).
Proof with automate.
  introv Hio. destruct Hio as (Hcp1 & Hcp2 & Hio).
  splits; try apply¬ cp_abs. ∃ R_receive. split... 2: constructor; splits...
  clear; splits...
    introv Hr. inverts Hr;
      constructor~; apply¬ HObisC_sym.
    introv Hr Ht. inverts Hr.
      inverts Ht.
      lets (q´ & Htq & Hr): (HObisC_tau p q H p´ Ht). ∃ q´. split¬.
    introv Hr Ht. inverts Hr.
      inverts Ht.
      apply HObisC_out in H; auto. specializes H a p´ p´´ Ht.
        destruct H as (q´ & q´´ & Hq1 & Hq2 & Hq3). ∃ q´ q´´. splits¬.
    introv Hr Ht. inverts Hr.
      lets Heq : wfp_trans_in_chan_eq Ht; subst.
      eexists. splits...
      introv Hcr. lets Hyp1 : wfp_trans_in_abs_eq Ht; inverts Hyp1 as Hyp1.
        simpls. constructor. destruct H as (Hcp & Hcq & H).
        repeat rewrite¬ wfp_gfresh_subst_rewrite; try applys× fresh_GV. splits¬.
      destruct Hyp1 as (Y & Hneq & Hfy & Heq); subst; simpl.
        rewrite¬ <- wfp_subst_decomposition_g.
        constructor. destruct H as (Hcp & Hcq & H).
        repeat rewrite¬ wfp_gfresh_subst_rewrite; try applys× fresh_GV. splits¬.
      apply HObisC_closed in H; auto. specialize (H a fp Ht).
        destruct H as (fq & Hq1 & Hq2). ∃¬ fq.
Qed.

Inductive R_send : binary wfprocess :=
| Rs : ∀ a p q, p ≈HO q → (R_send (wfp_Send a p) (wfp_Send a q))
| Rsbis : ∀ p q, p ≈HO q → (R_send p q)
| RsN : (R_send wfp_Nil wfp_Nil).

Hint Resolve Rs Rsbis RsN.

Lemma HObis_congr_send : ∀ a p q,
  p ≈HO q → (wfp_Send a p) ≈HO (wfp_Send a q).
Proof with automate.
  introv Hio. destruct Hio as (Hcp1 & Hcp2 & Hio).
  splits¬. ∃ R_send. split¬. clear. splits.
      unfold Symmetric. introv Hr. inverts Hr;
        constructor~; apply¬ HObisC_sym.
        splits~; unfolds¬.
      unfold tau_relation. introv Hr Ht. inverts Hr.
        inverts Ht.
        lets: HObisC_tau. unfolds in H0.
        lets (q´ & Hq): (>> HObisC_tau p q H p´ Ht). ∃ q´. split×.
        inversion Ht.
      unfold out_relation. introv Hr Ht. inverts Hr.
        inverts Ht...
        lets (q´ & q´´ & Hq): (>> HObisC_out p q H a p´ p´´ Ht). ∃ q´ q´´. split×.
        inversion Ht.
      unfold closed_relation. introv Hr Ht. inverts Hr.
        inverts Ht...
        lets: HObisC_closed. unfolds in H0.
        lets (fq & Hq´ & Hq): (HObisC_closed p q H a fp Ht). ∃× fq.
        inverts Ht.
    constructor¬. splits¬.
Qed.


Lemma left413: ∀ a fv p q,
  permut fv (to_list (GV (proc p) \u GV (proc q))) →
  wfp_pipe a fv p ≈HO wfp_pipe a fv q →
    ∀ lr : list wfprocess,
      closed_proc_list_wfp lr →
      length lr = length fv →
      wfp_multisubst (combine fv lr) p ≈HO wfp_multisubst (combine fv lr) q.
Proof with automate.
  inductions fv; introv Hfv Hbis Hcl Hllr.
    simpl...

      lets Hnd: (nodup_tolist (GV p \u GV q)). apply permut_sym in Hfv.
      eapply permut_nodup in Hnd; eauto. apply permut_sym in Hfv.
      lets (z & zs & H2): (lengthn lr Hllr). subst lr. simpls.
      destruct Hcl as (Hcz & Hczs).
      destruct Hnd as (HnMem & HnoDup).
      asserts Hls: (length fv = length zs).
        rew_length in ×. nat_math.

      rewrite_all× wfp_mult_sub_commute.

      applys× (IHfv (wfp_subst z a0 p) (wfp_subst z a0 q))...

        simpl.
        rewrite_all× GV_subst_cp. rewrite <- union_remove.
        apply permut_rem1_r in Hfv. eapply permut_trans; eauto.
        apply rem1_to_list_perm.

        apply HObisC_closed in Hbis. lets H0 : TrIn a a0 (wfp_pipe a fv p).
        destruct (Hbis _ _ H0) as ( fq & Ht´ & Hr).
        specializes¬ Hr Hcz.
        lets Hyp1 : wfp_trans_in_abs_eq Ht´; inverts Hyp1 as Hyp1.
          simpls; do 2 rewrite× wfp_subst_on_pipe in Hr.
          destruct Hyp1 as (Y & Hneq & Hf & Heq); subst; simpls.
          rewrite¬ <- wfp_subst_decomposition_g in Hr.
          do 2 rewrite× wfp_subst_on_pipe in Hr.
Qed.

Lemma right413: ∀ a fv (p q : wfprocess),
  permut fv (to_list (GV p \u GV q)) →
    (∀ lr, closed_proc_list_wfp lr → length lr = length fv →
      (wfp_multisubst (combine fv lr) p) ≈HO (wfp_multisubst (combine fv lr) q)) →
        wfp_pipe a fv p ≈HO wfp_pipe a fv q.
Proof.
  inductions fv; introv Hfv H.
    assert (length (@nil wfprocess) = length (@nil wfprocess)) by auto.
    repeat rewrite¬ wfp_pipe_nil_eq; eapply H. Focus 2. apply H0. simpls¬.

    lets Hnd: (nodup_tolist (GV p \u GV q)). apply permut_sym in Hfv.
    eapply permut_nodup in Hnd; eauto. simpl in Hnd; apply permut_sym in Hfv.
    repeat rewrite wfp_pipe_to_Abs. applys¬ HObis_congr_receive.
    introv Hc. rewrite_all× wfp_subst_on_pipe. applys× IHfv.
      simpl; rewrite_all× GV_subst_cp. rewrite <- union_remove.
      apply permut_rem1_r in Hfv. eapply permut_trans; eauto.
      apply rem1_to_list_perm.
      introv Hc´ Hllr. asserts K: (∃ rs, r::lr = rs).
        ∃¬ (r::lr).
        destruct K as (rs & Hrs). asserts L: (closed_proc_list_wfp rs).
          rewrite <- Hrs. simpls¬.
          asserts M: (length rs = length (a0 :: fv)).
            rewrite <- Hrs. rew_length. nat_math.
          specialize (H rs L M). subst rs. simpls.
          asserts Hls: (length fv = length lr).
            rew_length in ×. nat_math.
          rewrite_all× <- wfp_mult_sub_commute.
Qed.

Lemma pre_lemma413: ∀ a fv (p q : wfprocess),
  permut fv (to_list (GV p \u GV q)) →
  (wfp_pipe a fv p ≈HO wfp_pipe a fv q ↔
    (∀ lr : list wfprocess, closed_proc_list_wfp lr → length lr = length fv →
    wfp_multisubst (combine fv lr) p ≈HO wfp_multisubst (combine fv lr) q)).
Proof.
  introv Hfv. split.
    introv HO. applys× left413.
    introv H. applys× right413.
Qed.

Lemma permute_subst_order: ∀ (xs : list var) rs p, noDup xs → closed_proc_list_wfp rs →
  length xs = length rs →
  ∀ l1 l2 l3 l4, l1 ++ l2 ++ l3 ++ l4 = combine xs rs →
    ∃ ys ps, l1 ++ l3 ++ l2 ++ l4 = combine ys ps
    ∧ noDup ys
    ∧ closed_proc_list_wfp ps
    ∧ length ys = length ps
    ∧ wfp_multisubst (l1 ++ l2 ++ l3 ++ l4) p = wfp_multisubst (l1 ++ l3 ++ l2 ++ l4) p.
Proof.
  introv Hnd Hcp Hls Hcm.
  lets (xs1 & xs2 & xs3 & xs4 & Hc & Hlxs1 & Hlxs2 & Hlxs3 & Hlxs4):
    (sublists_l xs rs l1 l2 l3 l4 Hls Hcm).
  lets (rs1 & rs2 & rs3 & rs4 & Hc´ & Hlrs1 & Hlrs2 & Hlrs3 & Hlrs4):
    (sublists_r xs rs l1 l2 l3 l4 Hls Hcm).
  subst xs rs.
  ∃ (xs1 ++ xs3 ++ xs2 ++ xs4). ∃ (rs1 ++ rs3 ++ rs2 ++ rs4).
  do 3 rewrite permut_combine_step in Hcm; try rewrite_all length_app; try nat_math.
  apply length_app_inv in Hcm; destruct Hcm.
  apply length_app_inv in H0; destruct H0.
  apply length_app_inv in H1; destruct H1.
  subst.
  splits.
  rewrite <- permut_combine_step; try nat_math.
  rewrite <- permut_combine_step; try rewrite_all length_app; try nat_math.
  rewrite <- permut_combine_step; try rewrite_all length_app; try nat_math.
  reflexivity.
  applys× permut_nodup (xs1 ++ xs2 ++ xs3 ++ xs4); permut_simpl.
  applys× wfp_permut_cp_list (rs1 ++ rs2 ++ rs3 ++ rs4); permut_simpl.
  nat_math.
  rewrite_all wfp_mult_sub_separate2.
  rewrite¬ <- (wfp_mult_sub_commute3 (combine xs2 rs2) (combine xs3 rs3) (wfp_multisubst (combine xs4 rs4)p)).

  rewrite fst_split_step. rewrite_all combine_split; try nat_math. simpl.
  apply nodup_app_inv in Hnd. destruct Hnd.
  rewrite nodup_app_comm in H0. rew_app in H0. rewrite nodup_app_comm in H0.
  rew_app in H0. apply nodup_app_inv in H0. destructs¬ H0.
  rewrite combine_split. simpl.
  apply wfp_cpl_app_inv in Hcp. destruct Hcp.
  apply wfp_cpl_app_inv in H0. destructs¬ H0. nat_math.
  rewrite combine_split. simpl.
  apply wfp_cpl_app_inv in Hcp. destruct Hcp.
  apply wfp_cpl_app_inv in H0. destruct H0.
  apply wfp_cpl_app_inv in H1. destructs¬ H1. nat_math.
  symmetry. rewrite length_combine; nat_math.
  symmetry. rewrite length_combine; nat_math.
  symmetry. rewrite length_combine; nat_math.
  symmetry. rewrite_all length_app. rewrite_all length_combine; nat_math.
  symmetry. rewrite length_combine; nat_math.
  symmetry. rewrite_all length_app. rewrite_all length_combine; nat_math.
Qed.

Lemma permut_subst: ∀ xs rs ys ps, noDup xs → noDup ys →
  length xs = length rs → closed_proc_list_wfp rs →
    permut (combine xs rs) (combine ys ps) →
      ∀ p, wfp_multisubst (combine xs rs)p = wfp_multisubst(combine ys ps)p.
Proof.
  introv Hnd1 Hnd2 Hls Hcp1 Hp . inductions Hp. rewrite¬ x.
  inverts H. introv.
  lets (xs´ & rs´ & H1´ & Hnd´ & Hcp´ & Hls´ & K):
    (permute_subst_order xs rs p Hnd1 Hcp1 Hls l1 l2 l3 l4 H1).
  rewrite K. rewrite H1´. applys× IHHp.
    assert (permut rs rs´).
      applys× (permut_inv_r rs rs´ xs xs´).
      rewrite <- H1´. rewrite <- H1. permut_simpl.
  rewrite¬ H1´.
Qed.


Lemma permuted_subst: ∀ (xs ys: list var) (rs: list wfprocess),
  noDup xs → noDup ys →
  closed_proc_list_wfp rs → length xs = length rs → permut xs ys →
  ∃ ps, permut rs ps ∧ ∀ p, wfp_multisubst (combine xs rs) p = wfp_multisubst (combine ys ps) p.
Proof.
  introv Hnd1 Hnd2 Hcp1 Hls Hp. lets Hp´: (permut_exists Hp rs Hls).
  destruct Hp´ as (ps & Hp´ & Hpz). ∃ ps. split¬. applys× permut_subst.
Qed.

Lemma permute_pipe : ∀ a xs ys (p q : wfprocess),
  permut xs (to_list (GV p \u GV q)) → permut ys (to_list (GV p \u GV q)) →
  wfp_pipe a xs p ≈HO wfp_pipe a xs q → wfp_pipe a ys p ≈HO wfp_pipe a ys q.
Proof.
  introv Hfv1 Hfv2 Hp. applys× pre_lemma413.
  introv Hcp Hl. remember Hfv1 as Hfve. clear HeqHfve.
  lets Hnd1: (nodup_tolist (GV p \u GV q)). apply permut_sym in Hfv1.
    eapply permut_nodup in Hnd1; eauto. apply permut_sym in Hfv1.
  lets Hnd2: (nodup_tolist (GV p \u GV q)). apply permut_sym in Hfv2.
    eapply permut_nodup in Hnd2; eauto. apply permut_sym in Hfv2.
  apply permut_sym in Hfve. eapply permut_trans in Hfve; eauto.
  symmetry in Hl.
  lets× P´: permuted_subst ys xs lr Hl Hfve. destruct P´ as (ps & P´ & H).
  rewrite (H p). rewrite (H q).
  asserts Hcpp: (closed_proc_list_wfp ps).
    applys× (wfp_permut_cp_list lr).
  asserts Hpsl: (length xs = length ps).
    apply permut_len in P´. rewrite <- P´. apply permut_len in Hfve. rewrite¬ <- Hfve.
  clear H P´; applys× (pre_lemma413 a xs p q).
Qed.

Lemma change_channel : ∀ a b xs (p q : wfprocess),
  permut xs (to_list (GV p \u GV q)) →
   wfp_pipe a xs p ≈HO wfp_pipe a xs q →
   wfp_pipe b xs p ≈HO wfp_pipe b xs q.
Proof with automate.
  induction xs; simpls¬.
    introv Hfl H. lets H´: H. destruct H as (Hcp1 & Hcp2 & _); splits;
      rewrite <- wfp_pipe_to_Abs; try apply wfp_closed_pipe;
      try rewrites (permut_from_list Hfl); try rewrite from_to_list;
      unfold subset; introv; try rewrite× in_union.

    unfolds. ∃ R_ch. split; simpl.
      applys¬ HObisR_ch.
      constructor; applys¬ HObis_congr_receive.
      asserts Hnd: (noDup (a0::xs)).
        eapply permut_nodup. apply permut_sym. eassumption. apply nodup_tolist.
      assert (HnMem : ¬Mem a0 xs) by (inverts¬ Hnd).
      introv Hc. rewrite_all× wfp_subst_on_pipe. applys× IHxs.
        simpl; rewrite_all¬ GV_subst_cp. rewrite <- union_remove.
        apply permut_sym. eapply permut_trans. apply permut_sym. apply rem1_to_list_perm.
        apply permut_sym. apply¬ permut_rem1_r.
      rewrite_all× <- wfp_subst_on_pipe.
      lets Ht: TrIn a a0 (wfp_pipe a xs p).
      eapply HObisC_closed in Ht; try eassumption.
      destruct Ht as (fq & Ht´ & Hr).
      lets Hyp1 : wfp_trans_in_abs_eq Ht´; inverts Hyp1 as Hyp1; simpls...
      destruct Hyp1 as (Y & Hneq & Hfy & Heq); subst; simpls.
      specializes Hr Hc; rewrite¬ <- wfp_subst_decomposition_g in Hr.
Qed.


Lemma piping_HOext : ∀ xs (p q : wfprocess),
  permut xs (to_list (GV p \u GV q)) → (∀ a, wfp_pipe a xs p ≈HO wfp_pipe a xs q ↔ p ≈*HO q).
Proof.
  introv Hgv. split.
    lets Hnd: (nodup_tolist (GV p \u GV q)). apply permut_sym in Hgv.
    eapply permut_nodup in Hnd; eauto. apply permut_sym in Hgv.
    introv Hho. unfolds. introv Hgv´. applys× (permute_pipe a0 xs xs0 p q).
    applys× (change_channel a a0).
    introv Hho. applys¬ Hho.
Qed.

Lemma HObisE_equiv: ∀ (p q : wfprocess) (fv : list var),
  permut fv (to_list (GV p \u GV q)) →
    (p ≈*HO q ↔ (∀ lr : list wfprocess,
                     length lr = length fv →
                     closed_proc_list_wfp lr →
                     wfp_multisubst (combine fv lr) p ≈HO wfp_multisubst (combine fv lr) q)).
Proof.
  introv Hfv. split.
    introv HO Hcl Hllr. applys× left413.
    introv H. applys× (piping_HOext fv p q Hfv). applys× right413.
    Existential 1:=1. Existential 1:=1.
Qed.


Lemma HObisE_sym: Symmetric HObisE.
Proof.
  introv H. unfolds. intros. apply HObisC_sym. applys¬ H. rewrite¬ union_comm.
Qed.

Lemma HObisE_subst: ∀ X (p q r : wfprocess), p ≈*HO q →
  closed_process r → (wfp_subst r X p) ≈*HO (wfp_subst r X q).
Proof.
  introv Hio Hcp Hfl. unfolds in Hio.
  elim (classic (X \in ((GV p) \u (GV q)))); introv Hnm.
  lets Hnd: (nodup_tolist (GV ([r // X]p) \u GV ([r // X]q))).
  assert (¬Mem X (to_list (GV ([r // X]p) \u GV ([r // X]q)))).
    introv H. apply permut_sym in Hfl. eapply permut_mem in H; eauto.
    apply permut_from_list in Hfl. rewrite from_to_list in Hfl.
    simpl in Hfl; rewrite¬ GV_subst_cp in Hfl. rewrite¬ GV_subst_cp in Hfl.
    rewrite <- union_remove in Hfl.
    rewrite <- from_list_spec in H. rewrite <- Hfl in H.
    rewrite¬ in_remove in H. destruct H. rewrite¬ notin_singleton in H0.
  applys× HObisE_equiv. introv Hcpr Hls.
  simpl in Hfl; rewrite¬ GV_subst_cp in Hfl. rewrite¬ GV_subst_cp in Hfl.
  rewrite <- union_remove in Hfl.
  rewrite_all× <- wfp_mult_sub_commute.

  change (wfp_multisubst (combine (X::(to_list (GV ([r // X]p) \u GV ([r // X]q)))) (r::lr)) p
≈HO wfp_multisubst (combine (X::(to_list (GV ([r // X]p) \u GV ([r // X]q)))) (r::lr)) q).
  applys× HObisE_equiv.
    apply permut_rem1_l. rewrite <- from_list_spec. rewrite¬ from_to_list.
    apply permut_sym. rewrite¬ GV_subst_cp. rewrite¬ GV_subst_cp.
    rewrite <- union_remove. apply rem1_to_list_perm.
    simpl in Hls; rewrite_all length_cons; simpls; nat_math.
    simpls¬.
    assert (wfp_subst r X p = p ∧ wfp_subst r X q = q).
      rewrite in_union in Hnm; rew_logic in Hnm.
      split; apply wfp_gfresh_subst_rewrite; unfolds fresh_gvar; unfolds× notin.
    destruct H as (H1 & H2); rewrite H1 in *; rewrites¬ H2 in ×.
Qed.

Lemma HObisE_Msubst: ∀ xs (p q : wfprocess) lp, p ≈*HO q →
  length xs = length lp →
  closed_proc_list_wfp lp → (wfp_multisubst (combine xs lp) p) ≈*HO (wfp_multisubst (combine xs lp) q).
Proof.
induction xs.
  simpls¬.
  introv Hio Hnm Hgv Hcp.
  lets Hnm´ : Hnm; rew_length in Hnm´.
  symmetry in Hnm´; apply lengthn in Hnm´. destruct Hnm´ as (x & xs´ & Hxs); subst.
  inverts Hgv; simpls.
  applys× HObisE_subst.
Qed.

Lemma guarding_HObisE: ∀ xs ms (p q : wfprocess), p ≈*HO q →
  length xs = length ms →
  permut xs (to_list (unguardeds p \u unguardeds q)) →
  (wfp_multisubst (combine xs (¬¬ms)) p) ≈*HO (wfp_multisubst (combine xs (¬¬ms)) q)
  ∧ @@ (wfp_multisubst (combine xs (¬¬ms)) p)
  ∧ @@ (wfp_multisubst (combine xs (¬¬ms)) q).
Proof.
  induction xs; introv Hbis Hls Hfl.
    simpls. apply permut_sym in Hfl. apply permut_from_list in Hfl.
    rewrite from_to_list in Hfl. rewrite from_list_nil in Hfl.
    apply union_empty in Hfl.
    destruct Hfl. splits~; unfolds; introv; rewrite <- unguardeds_spec;
    [rewrite H | rewrite H0]; apply notin_empty.

    lets Hls´: Hls. rewrite length_cons in Hls´.
    symmetry in Hls´. apply lengthn in Hls´. destruct Hls´ as (Y & YS´ & HYS).
    subst. lets Hnd´: (nodup_tolist (unguardeds p \u unguardeds q)).
    apply permut_sym in Hfl. lets Hnd: permut_nodup Hfl Hnd´. clear Hnd´; inverts Hnd.
    assert (length xs = length (¬¬ YS´)).
      rewrite wfp_length_opl. rewrite_all length_cons in Hls. nat_math.
    lets Hcp: wfp_cpl_opl YS´. simpl.
    replace ([Send Y Nil // a]wfp_multisubst (combine xs (¬¬YS´)) p) with (proc (wfp_subst (wfp_Send Y wfp_Nil) a (wfp_multisubst (combine xs (¬¬YS´)) p))) by (auto).
    replace ([Send Y Nil // a]wfp_multisubst (combine xs (¬¬YS´)) q) with (proc (wfp_subst (wfp_Send Y wfp_Nil) a (wfp_multisubst (combine xs (¬¬YS´)) q))) by (auto).
    rewrite_all× wfp_mult_sub_commute; [ | simpls; constructor¬ | simpls; constructor~].
      applys× IHxs.
        applys× HObisE_subst.
          unfolds¬.
        rewrite_all wfp_unguardeds_cp_subst; try unfolds¬.
          rewrite <- union_remove. apply permut_sym. eapply permut_trans.
          apply permut_sym. eapply rem1_to_list_perm. apply permut_sym.
          apply permut_rem1_r. applys¬ permut_sym.
Qed.

Lemma HO_HOE : ∀ (p q : wfprocess),
  p ≈HO q → p ≈*HO q.
Proof.
  introv Hio.
  assert (permut nil (to_list (GV p \u GV q))).
    destruct Hio as (Hcp & Hcq & _).
    rewrite Hcp, Hcq; rewrite union_same; apply to_from_list.
  rewrites¬ (HObisE_equiv p q nil H).
Qed.