Library HOC27BarbedRevisited

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 HOC17NORbis.
Require Import HOC19Coincide.
Require Import HOC20Barbed.
Require Import HOC23PrimeDecomposition.
Require Import HOC24PreCompleteness.
Require Import HOC25Axiomatization.
Require Import HOC26EarlyBisimulation.

Require Import Relations.


Lemma congr_context_closed : context_closed wfcgr.
Proof with automate.
  introv Hc. gen p q. inductions C; simpls¬.

  + applys¬ wfcgr_send.
  + applys¬ wfcgr_abs.
  + applys¬ wfcgr_par. reflexivity.
  + applys¬ wfcgr_par. reflexivity.
Qed.

Lemma congr_out_barb_preserving : out_barb_preserving wfcgr.
Proof with automate.
  introv Hc. inductions Hc; jauto. inductions H; jauto.

  introv (p´ & p´´ & Htp). inverts Htp...
  ∃ wfp_Nil q. constructor.

  introv (p´ & p´´ & Htp). inverts Htp.

  introv (r´ & r´´ & Htpar). inverts Htpar...
    destruct ap; inverts H5.
    lets (p1 & p2 & Htp´) : IHwfcgr_step1 a.
    eexists. eexists. eassumption.
    eexists. eexists. apply act1_out. eassumption.
    destruct aq; inverts H5.
    lets (p1 & p2 & Htp´) : IHwfcgr_step2 a.
    eexists. eexists. eassumption.
    eexists. eexists. apply act2_out. eassumption.

  introv (p´ & p´´ & Htp).
    eexists. eexists. apply act1_out. eassumption.

  introv (p´ & p´´ & Htp). inverts Htp...
    destruct ap; inverts H3. eexists. eexists. eassumption.
    inverts H2.

  introv (p´ & p´´ & Htp). inverts Htp...
    destruct ap; inverts H3. eexists. eexists. apply act2_out. eassumption.
    destruct aq; inverts H3. eexists. eexists. apply act1_out. eassumption.

  introv (p´ & p´´ & Htp). inverts Htp...
    destruct ap; inverts H3. eexists. eexists. repeat apply act1_out. eassumption.
    destruct aq; inverts H3. inverts H2...
      destruct ap; inverts H4.
        eexists. eexists. apply act1_out. apply act2_out. eassumption.
      destruct aq; inverts H4.
        eexists. eexists. repeat apply act2_out. eassumption.

  introv (p´ & p´´ & Htp). inverts Htp...
    destruct ap; inverts H3. inverts H2...
      destruct ap; inverts H4.
        eexists. eexists. repeat apply act1_out. eassumption.
      destruct aq; inverts H4.
        eexists. eexists. apply act2_out. apply act1_out. eassumption.
    destruct aq; inverts H3.
        eexists. eexists. repeat apply act2_out. eassumption.
Qed.

Lemma congr_async_barbed_relation : async_barbed_relation wfcgr.
Proof.
  splits¬.
    apply wfcgr_is_eq_rel.
    apply congr_tau.
    apply congr_context_closed.
    apply congr_out_barb_preserving.
Qed.

Lemma congr_async_barbed : ∀ p q, p ≡* q → async_barbed p q.
Proof.
  introv Hc. ∃ wfcgr. splits×.
  apply congr_async_barbed_relation.
Qed.

Instance async_barbed_refl : Reflexive async_barbed.
Proof.
  introv; apply congr_async_barbed. reflexivity.
Qed.

Hint Resolve async_barbed_refl async_barbed_sym async_barbed_trans.

Lemma async_barbed_congr_nil_l : ∀ p, async_barbed p (wfp_Par p wfp_Nil).
Proof.
  introv; apply congr_async_barbed. apply wfcgr_nil_l.
Qed.

Lemma async_barbed_congr_nil_r : ∀ p, async_barbed (wfp_Par p wfp_Nil) p.
Proof.
  introv; apply congr_async_barbed. apply wfcgr_nil_r.
Qed.

Lemma async_barbed_congr_par_com : ∀ p q, async_barbed (wfp_Par p q) (wfp_Par q p).
Proof.
  introv; apply congr_async_barbed. apply wfcgr_par_com.
Qed.

Lemma async_barbed_congr_par_assoc_l : ∀ p q r, async_barbed (wfp_Par p (wfp_Par q r)) (wfp_Par (wfp_Par p q) r).
Proof.
  introv; apply congr_async_barbed. apply wfcgr_par_assoc_l.
Qed.

Lemma async_barbed_congr_par_assoc_r : ∀ p q r, async_barbed (wfp_Par (wfp_Par p q) r) (wfp_Par p (wfp_Par q r)).
Proof.
  introv; apply congr_async_barbed. apply wfcgr_par_assoc_r.
Qed.

Lemma async_barbed_congr_send : ∀ p q a,
  async_barbed p q → async_barbed (wfp_Send a p) (wfp_Send a q).
Proof.
  introv Hab.
  set (Ctx := CSend a CHole).
  apply async_barbed_context_closed in Hab. specializes Hab Ctx.
  subst Ctx; simpls¬.
Qed.

Lemma async_barbed_congr_abs : ∀ p q a X,
  async_barbed p q → async_barbed (wfp_Abs a X p) (wfp_Abs a X q).
Proof.
  introv Hab.
  set (Ctx := CAbs a X CHole).
  apply async_barbed_context_closed in Hab. specializes Hab Ctx.
  subst Ctx; simpls¬.
Qed.

Lemma async_barbed_congr_par_l : ∀ p q r,
  async_barbed p q → async_barbed (wfp_Par p r) (wfp_Par q r).
Proof.
  introv Hab.
  set (Ctx := CParL CHole r).
  apply async_barbed_context_closed in Hab. specializes Hab Ctx.
  subst Ctx; simpls¬.
Qed.

Lemma async_barbed_congr_par_r : ∀ p q r,
  async_barbed p q → async_barbed (wfp_Par r p) (wfp_Par r q).
Proof.
  introv Hab.
  set (Ctx := CParR r CHole).
  apply async_barbed_context_closed in Hab. specializes Hab Ctx.
  subst Ctx; simpls¬.
Qed.

Lemma async_barbed_congr_par : ∀ p q r s,
  async_barbed p q → async_barbed r s →
    async_barbed (wfp_Par p r) (wfp_Par q s).
Proof.
  introv Hab_pq Hab_rs.
  apply async_barbed_context_closed in Hab_pq. specializes Hab_pq (CParL CHole r).
  simpls. etransitivity. eassumption.
  apply async_barbed_context_closed in Hab_rs. specializes Hab_rs (CParR q CHole).
  simpls¬.
Qed.

Lemma async_barbed_congr_send_inv : ∀ p q a,
  async_barbed (wfp_Send a p) (wfp_Send a q) → async_barbed p q.
Proof with automate.
  introv Hab. lets (X & _) : find_fresh (@nil process).

  lets Hab_cc : async_barbed_context_closed Hab (CParL CHole (wfp_Abs a X (wfp_Gvar X))); simpls.

  lets Hin_p : TrIn a X (wfp_Gvar X).
  lets Hout_p : TrOut a p.
  lets Htau_p : TrTau1 Hout_p Hin_p. simpls... cases_if×.

  lets (q´ & Htau_q & Hab´) : async_barbed_tau Hab_cc Htau_p.

  inverts Htau_q; subst_wfp;
  assert (p0 = wfp_Send a q) by rewrite_wfp_equal;
  assert (q0 = wfp_Abs a X (wfp_Gvar X)) by rewrite_wfp_equal; substs;
  try solve [inverts H2].

  clear H H0. inverts H2...
  assert (wfp_inst_Abs fq q = q).
    lets Hyp : wfp_trans_in_abs_eq H3.
    inverts Hyp as Hyp. simpls... cases_if×.
    destruct Hyp as (Y & HneqY & HfY & Heq); subst.
    simpls. rewrite¬ <- wfp_subst_decomposition_g... cases_if×.
  rewrite H in ×.

  etransitivity. apply async_barbed_congr_nil_l.
  etransitivity. apply async_barbed_congr_par_com.
  etransitivity. eassumption.
  etransitivity. apply async_barbed_congr_par_com.
  etransitivity. apply async_barbed_congr_nil_r.
  reflexivity.
Qed.

Lemma async_barbed_congr_abs_inv : ∀ p q a X,
  async_barbed (wfp_Abs a X p) (wfp_Abs a X q) → async_barbed p q.
Proof with automate.
  introv Hab.

  lets Hab_cc : async_barbed_context_closed Hab (CParL CHole (wfp_Send a (wfp_Gvar X))); simpls.

  lets Hin_p : TrIn a X p.
  lets Hout_p : TrOut a (wfp_Gvar X).
  lets Htau_p : TrTau2 Hin_p Hout_p. simpls... rewrite wfp_subst_gvar_idem in ×.

  lets (q´ & Htau_q & Hab´) : async_barbed_tau Hab_cc Htau_p.

  inverts Htau_q; subst_wfp;
  assert (q0 = wfp_Send a (wfp_Gvar X)) by rewrite_wfp_equal; substs;
  try solve [inverts H2].

  clear H0. inverts H3...
  assert (q´´ = wfp_Gvar X) by rewrite_wfp_equal; substs; clear H1.
  assert (wfp_inst_Abs fp (wfp_Gvar X) = q).
    lets Hyp : wfp_trans_in_abs_eq H2.
    inverts Hyp as Hyp. simpls... rewrite¬ wfp_subst_gvar_idem.
    destruct Hyp as (Y & HneqY & HfY & Heq); subst.
    simpls. rewrite¬ <- wfp_subst_decomposition_g... rewrite¬ wfp_subst_gvar_idem.
  rewrite H in ×.

  etransitivity. apply async_barbed_congr_nil_l.
  etransitivity. eassumption.
  etransitivity. apply async_barbed_congr_nil_r.
  reflexivity.
Qed.


Lemma async_barbed_swap_fresh : ∀ (p q : wfprocess) X Y,
  Y # p → Y # q → async_barbed p q →
    async_barbed (wfp_swap X Y p) (wfp_swap X Y q).
Proof with automate.
  introv Hfyp Hfyq Hab.
  tests Heq : (X = Y). repeat rewrite¬ wfp_swap_equal.

  lets (a & _) : find_fresh_chan (@nil process).
  lets Hab_cc_xy : async_barbed_context_closed Hab.
  specializes Hab_cc_xy (CParL (CAbs a X CHole) (wfp_Send a (wfp_Gvar Y))); simpls.

  lets Hin_p : TrIn a X p.
  lets Hout_p : TrOut a (wfp_Gvar Y).
  lets Htau_p : TrTau2 Hin_p Hout_p. simpls.
  rewrite wfp_gfresh_subst_is_swap in Htau_p; auto.
  etransitivity. apply async_barbed_congr_nil_l.

  lets (q´ & Htau_q & Hab´) : async_barbed_tau Hab_cc_xy Htau_p.
  etransitivity. eassumption.

  inverts Htau_q; subst_wfp;
  assert (q0 = wfp_Send a (wfp_Gvar Y)) by rewrite_wfp_equal; substs;
  try solve [inverts H2].

  clear H0. inverts H3...
  assert (q´´ = wfp_Gvar Y) by rewrite_wfp_equal; substs. clear H1.
  assert (wfp_inst_Abs fp (wfp_Gvar Y) = wfp_swap X Y q).
    rewrite¬ <- wfp_gfresh_subst_is_swap.
    lets Hyp : wfp_trans_in_abs_eq H2. inverts Hyp as Hyp.
    simpls¬. destruct Hyp as (Z & HneqZ & HfZ & Heq´). subst.
    simpls. rewrite¬ <- wfp_subst_decomposition_g.
  rewrite H in ×. apply async_barbed_congr_nil_r.
Qed.

Lemma async_barbed_swap : ∀ p q X Y, async_barbed p q →
  async_barbed (wfp_swap X Y p) (wfp_swap X Y q).
Proof with automate.
  introv Hab. tests Heq : (X = Y).
  repeat rewrite¬ wfp_swap_equal.
  lets (Z & Hfz) : find_fresh (proc p :: proc q :: proc (wfp_Gvar X) :: proc (wfp_Gvar Y) :: nil).
  rewrite Forall_to_conj_4 in Hfz; destruct Hfz as (Hfzp & Hfzq & Hfzx & Hfzy).
  simpls; rewrite gfresh_gvar in ×.

  lets Hab_xz : async_barbed_swap_fresh X Z Hfzp Hfzq Hab.
  lets Hab_zy : async_barbed_swap_fresh Y X Hab_xz.
    rewrite¬ <- wfp_gfresh_subst_is_swap; simpls; fresh_solve.
    rewrite¬ <- wfp_gfresh_subst_is_swap; simpls; fresh_solve.
  lets Hab_yx : async_barbed_swap_fresh Z Y Hab_zy.
    simpls; repeat (rewrite¬ <- gfresh_subst_is_swap; simpls; fresh_solve).
    simpls; repeat (rewrite¬ <- gfresh_subst_is_swap; simpls; fresh_solve).

  rewrite <- wfp_gfresh_subst_is_swap in Hab_yx;
    try (simpls; repeat (rewrite¬ <- gfresh_subst_is_swap; simpls; fresh_solve)).

  rewrite wfp_subst_on_swap in Hab_yx... cases_if×.
  rewrite wfp_swap_sym in Hab_yx. unfolds swap_gvar; repeat cases_if×.
  rewrite wfp_subst_on_swap in Hab_yx... cases_if×.
  unfolds swap_gvar; repeat cases_if×.
  rewrite¬ wfp_gfresh_subst_is_swap in Hab_yx.
  rewrite wfp_swap_involutive in Hab_yx.
  etransitivity. eassumption.

  rewrite <- wfp_gfresh_subst_is_swap;
    try (simpls; repeat (rewrite¬ <- gfresh_subst_is_swap; simpls; fresh_solve)).
  rewrite wfp_subst_on_swap... cases_if×.
  rewrite wfp_swap_sym. unfolds swap_gvar; repeat cases_if×.
  rewrite wfp_subst_on_swap... cases_if×.
  unfolds swap_gvar; repeat cases_if×.
  rewrite¬ wfp_gfresh_subst_is_swap.
  rewrite¬ wfp_swap_involutive.
Qed.


Lemma async_barbed_out_normal_early : out_normal_relation_early async_barbed.
Proof with automate.
  introv Hr Ht Hfmp Hfmq Hfxp Hfxq.

  lets (n & Hcn) : find_fresh_chan (proc p :: proc q :: Send m Nil :: nil).
  rewrite Forall_to_conj_3 in Hcn. destruct Hcn as (Hfnp & Hfnq & Hfnm).
  rewrite cfresh_send in Hfnm. destruct Hfnm as (_ & Hfnm).
  assert (Hfxp´´ : X # p´´).
    lets Hgv : GV_trans_out Ht.
    intros Hin; apply Hfxp.
    rewrite Hgv; rewrite¬ in_union.

  assert (Hfma : m ≠ a).
    eapply wfp_cfresh_out with (m := m) in Ht; jauto.

  assert (Hfna : n ≠ a).
    eapply wfp_cfresh_out with (m := n) in Ht; jauto.

  lets (Y & Hfy) : find_fresh (Gvar X :: nil).
    inverts Hfy as Hfy. clear H3. rewrite gfresh_gvar in Hfy.

  set (Ctx := CParL CHole (wfp_Abs a Y (wfp_Par (wfp_Abs m X (wfp_Gvar Y)) (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil))))).
  lets Hcc : async_barbed_context_closed Hr Ctx. subst Ctx. simpls.

  lets Hinl : TrIn a Y ((wfp_Par (wfp_Abs m X (wfp_Gvar Y)) (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)))).
  lets Htaul : TrTau1 Ht Hinl. simpls...
  repeat (rewrite wfp_eq_subst_abs2 in Htaul; jauto)... cases_if×.

  lets (Q & Htaur & HPQ) : async_barbed_tau Hcc Htaul.

  set (P := (wfp_Par p´
             (wfp_Par (wfp_Abs m X p´´)
                (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)))));
    fold P in HPQ.

  assert (Hout_P : perform_output P n).
  eexists. eexists. subst. repeat applys¬ act2_out.

  lets Hout_Q : async_barbed_out_barb_preserving HPQ Hout_P.

  inverts Htaur...

  + destruct ap; inverts H3.
    assert (q0 = wfp_Abs a Y (wfp_Par (wfp_Abs m X (wfp_Gvar Y)) (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)))).
      rewrite_wfp_equal. subst.
      destruct Hout_Q as (q´ & q´´ & Htr).
      inverts Htr...
      - false. eapply (false_trans_out n w); try eassumption.
        eapply wfp_cfresh_tau in H2. apply H2. auto.
      - assert (q0 = wfp_Abs a Y (wfp_Par (wfp_Abs m X (wfp_Gvar Y)) (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)))).
          rewrite_wfp_equal. subst q0. inverts H4.

  + assert (q0 = wfp_Abs a Y (wfp_Par (wfp_Abs m X (wfp_Gvar Y)) (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)))).
      rewrite_wfp_equal. subst q0. inverts H2.

  + assert (q0 = wfp_Abs a Y (wfp_Par (wfp_Abs m X (wfp_Gvar Y)) (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)))).
      rewrite_wfp_equal. subst q0.

    lets Heq : wfp_trans_in_chan_eq H3. subst a0.
    rename p´´0 into q´´, p´0 into q´. ∃ q´ q´´; splits×.
    assert (Hfxq´´ : X # q´´).
      lets Hgv : GV_trans_out H2.
      intros Hin; apply Hfxq.
      rewrite Hgv; rewrite¬ in_union.
    assert (wfp_inst_Abs fq q´´ = (wfp_Par (wfp_Abs m X q´´)
            (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)))).
      lets Heq : wfp_trans_in_abs_eq H3.
      inverts Heq as Heq. simpls...
      repeat (rewrite wfp_eq_subst_abs2; jauto)... cases_if×.
      destruct Heq as (Z & HneqZ & HfZ & Heq); subst.
      simpl; subst_wfp. rewrite¬ <- wfp_subst_decomposition_g...
      repeat (rewrite wfp_eq_subst_abs2; jauto)... cases_if×.
    repeat rewrite H in *; clear H.

    assert (Htau_P : {{P -- Tau ->> AP (wfp_Par p´ (wfp_Par (wfp_Abs m X p´´) (wfp_Par (wfp_Nil) (wfp_Nil))))}}).
      subst P. do 2 apply act2_tau.
      lets Htau : TrTau2 n (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil) wfp_Nil wfp_Nil. specializes Htau (AbsPure X wfp_Nil). simpls...

    lets (Q´ & Htau_Q & HP´Q´) : async_barbed_tau HPQ Htau_P.

    assert (Hno_out_P´ : ¬ perform_output (wfp_Par p´ (wfp_Par (wfp_Abs m X p´´) (wfp_Par wfp_Nil wfp_Nil))) n).
      introv Htr. destruct Htr as (P´ & P´´ & Htr).
      inverts Htr... apply false_trans_out in H5; auto.
        apply (wfp_cfresh_out _ _ _ _ _ Hfnp Ht).
        assert (q0 = wfp_Par (wfp_Abs m X p´´) (wfp_Par wfp_Nil wfp_Nil)).
          rewrite_wfp_equal. subst. clear H4. destruct aq; inverts H6...
        inverts H5... inverts H6. inverts H6; subst_wfp; inverts H8.

    assert (Hno_out_Q´ : ¬ perform_output Q´ n).
      introv Hout. elim Hno_out_P´. eapply async_barbed_out_barb_preserving.
      apply async_barbed_sym. eassumption. auto.

    inverts Htau_Q; subst_wfp;
    assert (q0 = (wfp_Par (wfp_Abs m X q´´) (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)))) by rewrite_wfp_equal; subst...

    - destruct ap; inverts H6.
      false. apply Hno_out_Q´.
        eexists. eexists. repeat applys¬ act2_out.

    - clear H4. destruct aq; inverts H6...
      inverts H5; subst_wfp;
      assert (q0 = (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil))) by rewrite_wfp_equal; subst...
      × inverts H6.
      × clear H4. destruct aq; inverts H7. inverts H6; subst_wfp;
        assert (q0 = wfp_Send n wfp_Nil) by rewrite_wfp_equal; subst; subst_wfp;
        try solve [inverts H5]. inverts H7...

        assert (Heq : wfp_inst_Abs fp wfp_Nil = wfp_Nil).
          lets Heq : wfp_trans_in_abs_eq H5.
          inverts Heq as Heq. simpls...
          destruct Heq as (Z & HneqZ & HfZ & Heq); subst.
          simpl; subst_wfp. rewrite¬ <- wfp_subst_decomposition_g...
        repeat rewrite Heq in *; clear Heq.

        etransitivity. apply async_barbed_congr_par_com.
        etransitivity. Focus 2. apply async_barbed_congr_par_com.
        etransitivity. apply async_barbed_congr_nil_l.
        etransitivity. apply async_barbed_congr_nil_l.
        etransitivity. apply async_barbed_congr_par_assoc_r.
        etransitivity. apply async_barbed_congr_par_assoc_r.
        etransitivity. eassumption.
        etransitivity. apply async_barbed_congr_par_assoc_l.
        etransitivity. apply async_barbed_congr_par_assoc_l.
        etransitivity. apply async_barbed_congr_nil_r.
        etransitivity. apply async_barbed_congr_nil_r.
        reflexivity.

      × inverts H6...
      × lets Heq : wfp_trans_in_chan_eq H6. subst a0.
        inverts H7...
          inverts H8. assert (q0 = wfp_Send n wfp_Nil).
            rewrite_wfp_equal. subst. inverts× H8. false¬ Hfnm.
    - clear H1. inverts H6; subst_wfp; assert (q0 = wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)) by rewrite_wfp_equal; subst...
      × clear H4; destruct ap; inverts H8...
        inverts H7. simpls. false Hno_out_Q´.
        eexists. eexists. repeat applys¬ act2_out.
      × clear H4; destruct aq; inverts H8...
        inverts H7; subst_wfp;
        assert (q0 = wfp_Send n wfp_Nil) by rewrite_wfp_equal; subst.
        inverts H6... inverts H8. false Hno_out_Q´.
        eexists. eexists. repeat applys¬ act2_out.
        false. rewrite wfprocess_eq in H; simpls; inverts H.
        inverts H6.

    - clear H1. inverts H6... inverts H7.
      assert (q0 = wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)).
        rewrite_wfp_equal. subst; clear H4. destruct aq; inverts H8.
      inverts H7... inverts H6. assert (q0 = wfp_Send n wfp_Nil).
        rewrite_wfp_equal. subst. clear H4. inverts H6...
      false. eapply (false_trans_in n). Focus 2. apply H5.
        apply (wfp_cfresh_out _ _ _ _ _ Hfnq H2).

  + assert (q0 = wfp_Abs a Y (wfp_Par (wfp_Abs m X (wfp_Gvar Y)) (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)))).
      rewrite_wfp_equal. subst q0. inverts H3.
Qed.

Lemma async_barbed_out_1 : ∀ (p q : wfprocess), (async_barbed p q) →
    ∀ (a : chan) (p´ p´´ : wfprocess),
    {{p -- LabOut a p´´ ->> (AP p´)}} →
      ∃ (q´ q´´ : wfprocess),
        ({{q -- LabOut a q´´ ->> (AP q´)}} ∧ (async_barbed p´ q´)).
Proof with automate.
  introv Hr Ht.

  lets (X & Hfx) : find_fresh (proc p :: proc q :: nil).
  rewrite Forall_to_conj_2 in Hfx; destruct Hfx as (Hfxp & Hfxq).

  assert (Hfxp´´ : X # p´´).
    lets Hgv : GV_trans_out Ht.
    intros Hin; apply Hfxp.
    rewrite Hgv; rewrite¬ in_union.

  lets (n & Hcn) : find_fresh_chan (proc p :: proc q :: nil).
  rewrite Forall_to_conj_2 in Hcn. destruct Hcn as (Hfnp & Hfnq).

  assert (Hfna : n ≠ a).
    eapply wfp_cfresh_out with (m := n) in Ht; jauto.

  lets (Y & Hfy) : find_fresh (Gvar X :: nil).
    inverts Hfy as Hfy. clear H3. rewrite gfresh_gvar in Hfy.

  set (Ctx := CParL CHole (wfp_Abs a Y (wfp_Par wfp_Nil (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil))))).

  lets Hcc : async_barbed_context_closed Hr Ctx. subst Ctx. simpls.

  lets Hinl : TrIn a Y ((wfp_Par wfp_Nil (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)))).
  lets Htaul : TrTau1 Ht Hinl. simpls...
  repeat (rewrite wfp_eq_subst_abs2 in Htaul; jauto)...

  lets (Q & Htaur & HPQ) : async_barbed_tau Hcc Htaul.

  set (P := (wfp_Par p´
             (wfp_Par wfp_Nil
                (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)))));
    fold P in HPQ.

  assert (Hout_P : perform_output P n).
  eexists. eexists. subst. repeat applys¬ act2_out.

  lets Hout_Q : async_barbed_out_barb_preserving HPQ Hout_P.

  inverts Htaur...

  + destruct ap; inverts H3.
    assert (q0 = wfp_Abs a Y (wfp_Par wfp_Nil (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)))).
      rewrite_wfp_equal. subst.
      destruct Hout_Q as (q´ & q´´ & Htr).
      inverts Htr...
      - false. eapply (false_trans_out n w); try eassumption.
        eapply wfp_cfresh_tau in H2. apply H2. auto.
      - assert (q0 = wfp_Abs a Y (wfp_Par wfp_Nil (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)))).
          rewrite_wfp_equal. subst q0. inverts H4.

  + assert (q0 = wfp_Abs a Y (wfp_Par wfp_Nil (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)))).
      rewrite_wfp_equal. subst q0. inverts H2.

  + assert (q0 = wfp_Abs a Y (wfp_Par wfp_Nil (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)))).
      rewrite_wfp_equal. subst q0.

    lets Heq : wfp_trans_in_chan_eq H3. subst a0.
    rename p´´0 into q´´, p´0 into q´. ∃ q´ q´´; splits×.
    assert (Hfxq´´ : X # q´´).
      lets Hgv : GV_trans_out H2.
      intros Hin; apply Hfxq.
      rewrite Hgv; rewrite¬ in_union.
    assert (wfp_inst_Abs fq q´´ = (wfp_Par wfp_Nil
            (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)))).
      lets Heq : wfp_trans_in_abs_eq H3.
      inverts Heq as Heq. simpls...
      repeat (rewrite wfp_eq_subst_abs2; jauto)...
      destruct Heq as (Z & HneqZ & HfZ & Heq); subst.
      simpl; subst_wfp. rewrite¬ <- wfp_subst_decomposition_g...
      repeat (rewrite wfp_eq_subst_abs2; jauto)...
    repeat rewrite H in *; clear H.

    assert (Htau_P : {{P -- Tau ->> AP (wfp_Par p´ (wfp_Par wfp_Nil (wfp_Par (wfp_Nil) (wfp_Nil))))}}).
      subst P. do 2 apply act2_tau.
      lets Htau : TrTau2 n (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil) wfp_Nil wfp_Nil. specializes Htau (AbsPure X wfp_Nil). simpls...

    lets (Q´ & Htau_Q & HP´Q´) : async_barbed_tau HPQ Htau_P.

    assert (Hno_out_P´ : ¬ perform_output (wfp_Par p´ (wfp_Par wfp_Nil (wfp_Par wfp_Nil wfp_Nil))) n).
      introv Htr. destruct Htr as (P´ & P´´ & Htr).
      inverts Htr... apply false_trans_out in H5; auto.
        apply (wfp_cfresh_out _ _ _ _ _ Hfnp Ht).
        assert (q0 = wfp_Par wfp_Nil (wfp_Par wfp_Nil wfp_Nil)).
          rewrite_wfp_equal. subst. clear H4. destruct aq; inverts H6...
        inverts H5... inverts H6. inverts H6; subst_wfp; inverts H8.

    assert (Hno_out_Q´ : ¬ perform_output Q´ n).
      introv Hout. elim Hno_out_P´. eapply async_barbed_out_barb_preserving.
      apply async_barbed_sym. eassumption. auto.

    inverts Htau_Q; subst_wfp;
    assert (q0 = (wfp_Par wfp_Nil (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)))) by rewrite_wfp_equal; subst...

    - destruct ap; inverts H6.
      false. apply Hno_out_Q´.
        eexists. eexists. repeat applys¬ act2_out.

    - clear H4. destruct aq; inverts H6...
      inverts H5; subst_wfp;
      assert (q0 = (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil))) by rewrite_wfp_equal; subst...
      × inverts H6.
      × clear H4. destruct aq; inverts H7. inverts H6; subst_wfp;
        assert (q0 = wfp_Send n wfp_Nil) by rewrite_wfp_equal; subst; subst_wfp;
        try solve [inverts H5]. inverts H7...

        assert (Heq : wfp_inst_Abs fp wfp_Nil = wfp_Nil).
          lets Heq : wfp_trans_in_abs_eq H5.
          inverts Heq as Heq. simpls...
          destruct Heq as (Z & HneqZ & HfZ & Heq); subst.
          simpl; subst_wfp. rewrite¬ <- wfp_subst_decomposition_g...
        repeat rewrite Heq in *; clear Heq.

        etransitivity. apply async_barbed_congr_nil_l.
        etransitivity. Focus 2. apply async_barbed_congr_nil_r.
        etransitivity. apply async_barbed_congr_nil_l.
        etransitivity. apply async_barbed_congr_nil_l.
        etransitivity. apply async_barbed_congr_par_assoc_r.
        etransitivity. apply async_barbed_congr_par_assoc_r.
        etransitivity. eassumption.
        etransitivity. apply async_barbed_congr_par_assoc_l.
        etransitivity. apply async_barbed_congr_par_assoc_l.
        etransitivity. apply async_barbed_congr_nil_r.
        etransitivity. apply async_barbed_congr_nil_r.
        reflexivity.

      × inverts H6...
      × inverts H6...

    - clear H1. inverts H6... inverts H7.
      assert (q0 = wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)).
        rewrite_wfp_equal. subst; clear H4. destruct aq; inverts H8.
      inverts H7... assert (q0 = wfp_Send n wfp_Nil).
        rewrite_wfp_equal. subst. clear H4. inverts H6...
      false. eapply (false_trans_out n). Focus 2. apply H5.
        apply (wfp_cfresh_out _ _ _ _ _ Hfnq H2).
      assert (q0 = wfp_Send n wfp_Nil).
        rewrite_wfp_equal. subst. inverts H6...

    - clear H1. inverts H6... inverts H7.
      assert (q0 = wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)).
        rewrite_wfp_equal. subst; clear H4. destruct aq; inverts H8.
      inverts H7... inverts H6... assert (q0 = wfp_Send n wfp_Nil).
        rewrite_wfp_equal. subst. clear H4. inverts H6...
      false. eapply (false_trans_in n). Focus 2. apply H5.
        apply (wfp_cfresh_out _ _ _ _ _ Hfnq H2).

  + assert (q0 = wfp_Abs a Y (wfp_Par wfp_Nil (wfp_Par (wfp_Abs n X wfp_Nil) (wfp_Send n wfp_Nil)))).
      rewrite_wfp_equal. subst q0. inverts H3.
Qed.


Lemma wfcgr_tr_in : ∀ p q, p ≡* q →
  ∀ a fp, {{p -- LabIn a ->> AA fp}} →
    ∃ fq, {{q -- LabIn a ->> AA fq}} ∧
      ∀ r, (wfp_inst_Abs fp r) ≡* (wfp_inst_Abs fq r).
Proof with automate.
  introv Hcgr. inductions Hcgr.

  + inductions H; introv Ht; try solve [inverts Ht].

    - lets Heq : wfp_trans_in_chan_eq Ht. subst a0.
      eexists. splits. constructor. introv; simpl.
      assert (wfp_inst_Abs fp r = wfp_subst r X p).
        lets Hyp : wfp_trans_in_abs_eq Ht. inverts Hyp as Hyp...
        destruct Hyp as (Y & HneqY & HfY & Heq). subst fp; simpls.
        rewrite¬ <- wfp_subst_decomposition_g.
      rewrite H0. apply wfcgr_subst; constructor¬.

    - inverts Ht...
      × destruct ap; inverts H5; rename a0 into fp.
        specializes IHwfcgr_step1 H4.
        destruct IHwfcgr_step1 as (fp´ & Htp´ & Hrp´).
        eexists; splits. apply act1_in; eassumption.
        introv; simpls. applys× wfcgr_par. constructor¬.
      × destruct aq; inverts H5; rename a0 into fq.
        specializes IHwfcgr_step2 H4.
        destruct IHwfcgr_step2 as (fq´ & Htq´ & Hrq´).
        eexists; splits. apply act2_in; eassumption.
        introv; simpls. applys× wfcgr_par. constructor¬.

    - eexists; splits. apply act1_in; eassumption.
      introv; simpls. apply wfcgr_nil_l.

    - inverts Ht...
      × destruct ap; inverts H3.
        eexists; splits×.
        introv; simpls. apply wfcgr_nil_r.
      × inverts H2.

    - inverts Ht...
      × destruct ap; inverts H3.
        eexists; splits. apply act2_in; eassumption.
        introv; simpls. apply wfcgr_par_com.
      × destruct aq; inverts H3.
        eexists; splits. apply act1_in; eassumption.
        introv; simpls. apply wfcgr_par_com.

    - inverts Ht...
      × destruct ap; inverts H3.
        eexists; splits. do 2 apply act1_in; eassumption.
        introv; simpls. apply wfcgr_par_assoc_l.
      × destruct aq; inverts H3. inverts H2...
          destruct ap; inverts H4.
          eexists; splits. apply act1_in; apply act2_in; eassumption.
          introv; simpls. apply wfcgr_par_assoc_l.
          destruct aq; inverts H4.
          eexists; splits. apply act2_in; eassumption.
          introv; simpls. apply wfcgr_par_assoc_l.

    - inverts Ht...
      × destruct ap; inverts H3. inverts H2...
          destruct ap; inverts H4.
          eexists; splits. apply act1_in; eassumption.
          introv; simpls. apply wfcgr_par_assoc_r.
          destruct aq; inverts H4.
          eexists; splits. apply act2_in; apply act1_in; eassumption.
          introv; simpls. apply wfcgr_par_assoc_r.
      × destruct aq; inverts H3.
        eexists; splits. do 2 apply act2_in; eassumption.
        introv; simpls. apply wfcgr_par_assoc_r.

    - eexists; splits×. introv; reflexivity.

  + introv Htx.
    lets (fy & Hty & Hmy) : IHHcgr1 Htx.
    lets (fz & Htz & Hmz) : IHHcgr2 Hty.
    ∃ fz; splits×. introv.
    etransitivity; jauto.
Qed.

Definition order_oiv (p : wfprocess) :=
  wfp_prod (get_outs p ++ get_ins p ++ get_vars p).

Lemma order_oiv_wfcgr : ∀ p, p ≡* order_oiv p.
Proof.
  introv. etransitivity. apply ordered_wfcgr.
  unfold ordered, order_oiv, get_components.
  etransitivity. apply wfp_prod_wfcgr_app.
  etransitivity. Focus 2. symmetry; apply wfp_prod_wfcgr_app.
  etransitivity. Focus 2. symmetry.
  apply wfcgr_par. reflexivity. apply wfp_prod_wfcgr_app.
  etransitivity. Focus 2. apply wfcgr_par_assoc_r.
  etransitivity. Focus 2. apply wfcgr_par_com.
  apply wfcgr_par. reflexivity.
  apply wfp_prod_wfcgr_app.
Qed.

Lemma order_oiv_async_barbed : ∀ p, async_barbed p (order_oiv p).
Proof.
  introv. apply congr_async_barbed.
  apply order_oiv_wfcgr.
Qed.

Hint Resolve async_barbed_sym.
Hint Resolve order_oiv_async_barbed.

Lemma async_barbed_to_order_oiv : ∀ p q,
  async_barbed p q → async_barbed (order_oiv p) (order_oiv q).
Proof.
  introv Hyp.
  transitivity p; auto.
  transitivity q; auto.
Qed.

Lemma order_oiv_cfresh_iff : ∀ m (p : wfprocess),
  m ### p ↔ m ### (order_oiv p).
Proof.
  introv; splits; intro Hyp; eapply wfcgr_alt_freshCh;
  [ | | symmetry | ]; try apply order_oiv_wfcgr; jauto.
Qed.