Library HOC13Bisimulations

Require Import HOC01Defs.
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 Relations.


Definition in_relation (R : RelWfP) : Prop :=
  ∀ (p q : wfprocess), (R p q) →
    ∀ (a : chan) (fp : abstraction), {{p -- LabIn a ->> (AA fp)}} →
    ∃ (fq : abstraction), {{q -- LabIn a ->> (AA fq)}} ∧
      ∀ X, X#p → X#q →
        R (wfp_inst_Abs fp (wfp_Gvar X)) (wfp_inst_Abs fq (wfp_Gvar X)).

Definition in_full_relation (R : RelWfP) : Prop :=
  ∀ (p q : wfprocess), (R p q) →
    ∀ (a : chan) (fp : abstraction), {{p -- LabIn a ->> (AA fp)}} →
    ∃ (fq : abstraction), {{q -- LabIn a ->> (AA fq)}} ∧
      ∀ X, R (wfp_inst_Abs fp (wfp_Gvar X)) (wfp_inst_Abs fq (wfp_Gvar X)).

Definition in_normal_relation (R : RelWfP) : Prop :=
  ∀ p q, (R p q) → ∀ a fp, {{p--LabIn a->>(AA fp)}} →
  ∃ fq, {{q--LabIn a->>(AA fq)}} ∧ ∀ m : chan, m###p → m###q →
    (R (wfp_inst_Abs fp (wfp_Send m wfp_Nil)) (wfp_inst_Abs fq (wfp_Send m wfp_Nil))).

Definition out_relation (R : RelWfP) : Prop :=
  ∀ (p q : wfprocess), (R p q) →
    ∀ (a : chan) (p´ p´´ : wfprocess),
    {{p -- LabOut a p´´ ->> (AP p´)}} →
      ∃ (q´ q´´ : wfprocess),
        ({{q -- LabOut a q´´ ->> (AP q´)}} ∧ (R p´ q´) ∧ (R p´´ q´´)).

Definition out_normal_relation (R : RelWfP) : Prop :=
  ∀ p q, (R p q) →
    ∀ a (p´ : wfprocess) (p´´ : wfprocess), {{p--LabOut a p´´->>(AP p´)}} →
      ∃ (q´ : wfprocess), ∃ (q´´ : wfprocess),
        ({{q--LabOut a q´´->>(AP q´)}} ∧
        ∀ (m:chan) (X:var), m###p → m###q → X#p´´ → X#q´´ →
          (R (wfp_Par (wfp_Abs m X p´´) p´)) (wfp_Par (wfp_Abs m X q´´) q´)).

Definition out_context_relation (R : RelWfP) : Prop :=
  ∀ p q, (R p q) →
    ∀ a (p´ p´´ : wfprocess), {{p--LabOut a p´´->>(AP p´)}} →
      ∃ (q´ : wfprocess), ∃ (q´´ : wfprocess),
        ({{q--LabOut a q´´->>(AP q´)}} ∧
        ∀ X (s : wfprocess), (GV s) \c (singleton X) →
          (R (wfp_Par (wfp_subst p´´ X s) p´) (wfp_Par (wfp_subst q´´ X s) q´))).

Definition var_relation (R : RelWfP) : Prop :=
  ∀ (p q : wfprocess), (R p q) →
    ∀ (X : var) (p´ : wfprocess), {{p -- LabRem X ->> (AP p´)}} →
      ∃ (q´ : wfprocess), {{q -- LabRem X ->> (AP q´)}} ∧ (R p´ q´).

Definition tau_relation (R : RelWfP) : Prop :=
  ∀ p q, (R p q) →
    ∀ (p´ : wfprocess), {{p--Tau->>(AP p´)}} →
      ∃ (q´ : wfprocess), ({{q--Tau->>(AP q´)}} ∧ R p´ q´).

Definition closed_relation (R : RelWfP) : Prop :=
  ∀ p q, (R p q) →
    ∀ a fp, {{p--LabIn a->>(AA fp)}} →
      ∃ fq, {{q -- LabIn a ->> (AA fq)}} ∧
        (∀ (r : wfprocess), closed_process r →
          R (wfp_inst_Abs fp r) (wfp_inst_Abs fq r)).


Definition IO_bisimulation (R : RelWfP) : Prop :=
 (Symmetric R) ∧ (in_relation R) ∧ (out_relation R) ∧ (var_relation R).

Definition IObis (p q : wfprocess) : Prop :=
  ∃ R, (IO_bisimulation R) ∧ (R p q).

Notation "p ≈ q" := (IObis p q) (at level 60).

Definition HigherOrder_bisimulation (R : RelWfP) : Prop :=
  (Symmetric R) ∧ (tau_relation R) ∧ (out_relation R) ∧ (closed_relation R).

Definition HObis (p q: wfprocess) : Prop :=
  ∃ R, (HigherOrder_bisimulation R) ∧ R p q.

Definition HObisC (p q: wfprocess) : Prop :=
  closed_process p ∧ closed_process q ∧ HObis p q.

Notation "p ≈HO q" := (HObisC p q) (at level 60).

Definition Context_bisimulation (R : RelWfP) : Prop :=
  (Symmetric R) ∧ (tau_relation R) ∧ (out_context_relation R) ∧ (closed_relation R).

Definition CONbis p q : Prop :=
  ∃ R, (Context_bisimulation R) ∧ (R p q).

Definition CONbisC (p q : wfprocess) : Prop :=
  closed_process p ∧ closed_process q ∧ CONbis p q.

Notation "p ≈CON q" := (CONbisC p q) (at level 60).

Definition Normal_bisimulation (R : RelWfP) : Prop :=
  (Symmetric R) ∧ (tau_relation R) ∧ (out_normal_relation R) ∧ (in_normal_relation R).

Definition NORbis p q : Prop :=
  ∃ R, (Normal_bisimulation R) ∧ (R p q).

Definition NORbisC (p q : wfprocess) : Prop :=
  closed_process p ∧ closed_process q ∧ NORbis p q.

Notation "p ≈NOR q" := (NORbisC p q) (at level 60).

Definition OpenNormal_bisimulation (R : RelWfP) : Prop :=
  (Symmetric R) ∧ (tau_relation R) ∧ (out_normal_relation R) ∧ (in_relation R) ∧ (var_relation R).

Definition ONORbis p q : Prop :=
  ∃ R, (OpenNormal_bisimulation R) ∧ (R p q).

Notation "p ≈ONOR q" := (ONORbis p q) (at level 60).


Definition HObisE (p q : wfprocess) : Prop := ∀ (a:chan) (xs:list var),
  permut xs (to_list (GV p \u GV q)) →
  (wfp_pipe a xs p) ≈HO (wfp_pipe a xs q).

Notation "p ≈*HO q" := (HObisE p q) (at level 60).

Definition CONbisE (p q : wfprocess) : Prop := ∀ (a:chan) (xs:list var),
  permut xs (to_list (GV p \u GV q)) →
  (wfp_pipe a xs p) ≈CON (wfp_pipe a xs q).

Notation "p ≈*CON q" := (CONbisE p q) (at level 60).

Definition NORbisE (p q : wfprocess) : Prop := ∀ (a:chan) (xs:list var),
  permut xs (to_list (GV p \u GV q)) →
  (wfp_pipe a xs p) ≈NOR (wfp_pipe a xs q).

Notation "p ≈*NOR q" := (NORbisE p q) (at level 60).



Inductive up_to (Re R: binary wfprocess) : binary wfprocess :=
 | UpTo : ∀ p q, (∃ p´ q´, Re p p´ ∧ Re q´ q ∧ R p´ q´) → up_to Re R p q.

Hint Resolve UpTo.

Lemma up_to_eq : ∀ (Re: binary wfprocess), Reflexive Re →
  ∀ (R: binary wfprocess) p q, R p q → up_to Re R p q.
Proof.
  introv HRe Hr. constructor. ∃¬ p q.
Qed.

Definition in_relation_up_to (Re R:binary wfprocess) : Prop :=
  ∀ p q, (R p q) → ∀ a fp, {{p--LabIn a->>(AA fp)}} →
    ∃ fq, {{q--LabIn a->>(AA fq)}} ∧
    ∀ (X:var), X#p → X#q →
      up_to Re R (wfp_inst_Abs fp (wfp_Gvar X)) (wfp_inst_Abs fq (wfp_Gvar X)).

Definition out_relation_up_to (Re R:binary wfprocess) : Prop :=
  ∀ p q, (R p q) → ∀ a (p´ p´´ : wfprocess), {{p--LabOut a p´´->>(AP p´)}} → ∃ (q´ : wfprocess), ∃ (q´´ : wfprocess), ({{q--LabOut a q´´->>(AP q´)}} ∧ (up_to Re R p´ q´) ∧ (up_to Re R p´´ q´´)).

Definition var_relation_up_to (Re R:binary wfprocess) : Prop :=
  ∀ p q, (R p q) → ∀ X (p´ : wfprocess), {{p--LabRem X->>(AP p´)}} →
∃ (q´ : wfprocess), {{q--LabRem X->>(AP q´)}} ∧ (up_to Re R p´ q´).

Definition tau_relation_up_to (Re R : RelWfP) : Prop :=
  ∀ p q, (R p q) →
    ∀ (p´ : wfprocess), {{p--Tau->>(AP p´)}} → ∃ (q´ : wfprocess), ({{q--Tau->>(AP q´)}} ∧ (up_to Re R p´ q´)).

Definition out_normal_relation_up_to (Re R : RelWfP) : Prop :=
  ∀ p q, (R p q) →
              ∀ a (p´ : wfprocess) (p´´ : wfprocess), {{p--LabOut a p´´->>(AP p´)}} →
              ∃ (q´ : wfprocess), ∃ (q´´ : wfprocess),
              ({{q--LabOut a q´´->>(AP q´)}} ∧
              ∀ (m:chan) (X:var), m###p → m###q → X#p´´ → X#q´´ →
              (up_to Re R
                (wfp_Par (wfp_Abs m X p´´) p´))
                (wfp_Par (wfp_Abs m X q´´) q´)).

Definition IO_bisimulation_up_to (Re R:binary wfprocess) : Prop :=
  (Symmetric R) ∧ (in_relation_up_to Re R) ∧ (out_relation_up_to Re R) ∧ (var_relation_up_to Re R).

Definition IObis_up_to Re p q : Prop :=
  ∃ R, (IO_bisimulation_up_to Re R) ∧ (R p q).

Definition OpenNormal_bisimulation_up_to (Re R : RelWfP) : Prop :=
  (Symmetric R) ∧ (tau_relation_up_to Re R) ∧ (out_normal_relation_up_to Re R) ∧
                   (in_relation_up_to Re R) ∧ (var_relation_up_to Re R).

Definition ONORbis_up_to Re p q : Prop :=
  ∃ R, (OpenNormal_bisimulation_up_to Re R) ∧ (R p q).


Lemma congr_in_strong : ∀ (p q : wfprocess) a fp,
  p ≡* q → {{p -- LabIn a ->> AA fp}} →
  (∃ fq, {{q -- LabIn a ->> AA fq}} ∧
    ∀ r : wfprocess, (wfp_inst_Abs fp r) ≡* (wfp_inst_Abs fq r)).
Proof with (introv; simpl; try solve [applys× t_step]; automate).
  introv Hr Ht.

  gen fp; inductions Hr.

  Focus 2.
  introv Ht.
  lets (fq & Ht´ & Hc) : (IHHr1 _ Ht).
    lets (fr & Ht´´ & Hc2): (IHHr2 _ Ht´). ∃ fr. split¬.
      introv. etransitivity.
        apply¬ Hc.
        apply¬ Hc2.

  inductions H; introv Ht...
inverts Ht.
  lets Heq : wfp_trans_in_chan_eq Ht; subst.
    lets Hyp : wfp_trans_in_abs_eq Ht; inverts Hyp as Hyp; subst.
    eexists. split. constructor¬.
    introv; simpl. applys× wfcgr_subst; constructor¬.
    destruct Hyp as (Y & Hneq & Hfy & Heq); subst.
    ∃ (AbsPure X q). splits¬.
      introv; simpl. rewrite¬ <- wfp_subst_decomposition_g.
      apply¬ wfcgr_subst...
inverts Ht...
destruct ap; inverts H5. lets (f2 & Ht´ & Hc): (IHwfcgr_step1 a0 H4).
    ∃ (AbsPar1 f2 q´). split...
      introv; simpl. apply wfcgr_par...
destruct aq; inverts H5. lets (f2 & Ht´ & Hc): (IHwfcgr_step2 a0 H4).
    ∃ (AbsPar2 p´ f2). split...
      introv; simpl. apply wfcgr_par...
∃ (AbsPar1 fp wfp_Nil). split...
inverts Ht...
      destruct ap; inverts H3. ∃ a0. split...
      inverts H2.
inverts Ht...
destruct ap; inverts H3. ∃ (AbsPar2 q a0). split...
destruct aq; inverts H3. ∃ (AbsPar1 a0 p). split...
inverts Ht...
destruct ap; inverts H3. ∃ (AbsPar1 (AbsPar1 a0 q) r). split...
inverts H2...
      destruct ap; inverts H3. ∃ (AbsPar1 (AbsPar2 p a0) r). split...
destruct aq0; inverts H3. ∃ (AbsPar2 (wfp_Par p q) a0). split...
inverts Ht...
destruct ap; inverts H3. inverts H2...
      destruct ap; inverts H4. ∃ (AbsPar1 a1 (wfp_Par q r)). split...
destruct aq; inverts H4. ∃ (AbsPar2 p (AbsPar1 a1 r)). split...
destruct aq; inverts H3. ∃ (AbsPar2 p (AbsPar2 q a0)). split...
∃ fp. split...
Qed.

Lemma congr_in : in_relation wfcgr.
Proof.
  introv Hr Ht.
  lets HDexM : congr_in_strong Hr Ht.
  destruct HDexM as (fq & H´ & Heq).
  ∃ fq; split¬.
Qed.

Lemma congr_out : out_relation wfcgr.
Proof with (try solve [applys× t_step]; automate).
  introv Hr Ht.
  inductions Hr.

  Focus 2.
  lets (q´ & q´´ & Ht´ & Hc1 & Hc1´): (IHHr1 _ _ _ Ht).
  lets (r´ & r´´ & Ht´´ & Hc2 & Hc2´): (IHHr2 _ _ _ Ht´).
  ∃ r´ r´´. splits¬.
    etransitivity; eassumption.
    etransitivity; eassumption.

  gen p´´ p´; inductions H; introv Ht...
inverts Ht...
    ∃ wfp_Nil q. splits...
inverts Ht.
inverts Ht...
destruct ap; inverts H5.
    lets (p2´ & p2´´ & Ht´ & Hc1 & Hc2): IHwfcgr_step1 H4.
    ∃ (wfp_Par p2´ q´) p2´´. splits...
      apply¬ wfcgr_par...
destruct aq; inverts H5.
    lets (q2´ & q2´´ & Ht´ & Hc1 & Hc2): IHwfcgr_step2 H4.
    ∃ (wfp_Par p´ q2´) q2´´. splits¬...
      apply¬ wfcgr_par...
∃ (wfp_Par p´ wfp_Nil) p´´. splits...
inverts Ht...
    destruct ap; inverts H3.
      ∃ w p´´; splits...
      inverts H2.
inverts Ht...
destruct ap; inverts H3...
      ∃ (wfp_Par q w) p´´. splits...
destruct aq; inverts H3...
      ∃ (wfp_Par w p) p´´. splits...
inverts Ht...
destruct ap; inverts H3...
      ∃ (wfp_Par (wfp_Par w q) r) p´´; splits...
inverts H2.
    destruct ap; inverts H3...
      ∃ (wfp_Par (wfp_Par p w) r) p´´. splits...
destruct aq0; inverts H3...
      ∃ (wfp_Par (wfp_Par p q) w) p´´. splits...
inverts Ht...
inverts H2...
    destruct ap0; inverts H3...
      ∃ (wfp_Par w (wfp_Par q r)) p´´. splits...
destruct aq; inverts H3...
      ∃ (wfp_Par p (wfp_Par w r)) p´´. splits...
destruct aq; inverts H3...
      ∃ (wfp_Par p (wfp_Par q w)) p´´; splits...
∃ p´ p´´. splits...
Qed.

Lemma congr_rem : var_relation wfcgr.
Proof with (try solve [applys× t_step]; automate).
  introv Hr Ht; inductions Hr...

  Focus 2.
    lets (r´ & Ht´ & Hc2): IHHr1 Ht.
    lets (r´´ & Ht´´ & Hc3): IHHr2 Ht´.
    ∃ r´´; splits...
      etransitivity; eassumption.

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

inverts Ht...
destruct ap; inverts H5.
      lets (p2´ & Ht´ & Hc): IHwfcgr_step1 H4.
      ∃ (wfp_Par p2´ q´). splits...
        apply¬ wfcgr_par...
destruct aq; inverts H5.
      lets (q1 & Ht´ & Hc): IHwfcgr_step2 H4.
      ∃ (wfp_Par p´ q1). splits...
        apply¬ wfcgr_par...
∃ (wfp_Par p´ wfp_Nil); splits...
inverts Ht...
    destruct ap; inverts H3.
    ∃ w. splits...
    inverts H2.
inverts Ht...
destruct ap; inverts H3.
      ∃ (wfp_Par q w). splits...
destruct aq; inverts H3.
      ∃ (wfp_Par w p). splits...
inverts Ht...
destruct ap; inverts H3.
      ∃ (wfp_Par (wfp_Par w q) r). splits...
inverts H2...
      destruct ap; inverts H3...
       ∃ (wfp_Par (wfp_Par p w) r). splits...
destruct aq0; inverts H3...
       ∃ (wfp_Par (wfp_Par p q) w). splits...
inverts Ht...
inverts H2...
      destruct ap0; inverts H3.
      ∃ (wfp_Par w (wfp_Par q r)). splits...
destruct aq; inverts H3...
       ∃ (wfp_Par p (wfp_Par w r)). splits...
destruct aq; inverts H3...
       ∃ (wfp_Par p (wfp_Par q w)). splits...
∃ p´. splits...
Qed.

Lemma congr_tau : tau_relation wfcgr.
Proof with (try solve [applys× t_step]; automate).
  introv Hr; inductions Hr.

  Focus 2.
  introv Htp.
  lets (q´ & Htq & Hcp´q´) : IHHr1 Htp.
  lets (r´ & Htr & Hcq´r´) : IHHr2 Htq.
  ∃ r´; splits¬...
  etransitivity; eassumption.

  inductions H; introv Htp; try solve [inverts Htp].

  rename IHwfcgr_step1 into HIp;
  rename IHwfcgr_step2 into HIp´.
  inverts Htp...
    lets (p´´ & Heq) : wfp_agent_tau H4; subst; inverts H5.
    lets (q´´ & Htq & Hcp´´q´´) : HIp H4; clear HIp.
    ∃ (wfp_Par q´´ q´); splits...
      applys¬ wfcgr_par...
    lets (p´´ & Heq) : wfp_agent_tau H4; subst; inverts H5.
    lets (q´´ & Htq & Hcp´´q´´) : HIp´ H4.
    ∃ (wfp_Par p´ q´´); splits...
      applys¬ wfcgr_par...

    lets (q0´ & q0´´ & Htq0 & Hcq0´ & Hcq0´´) : congr_out p´ H4...
    lets (fq1 & Htq1 & Heq) : congr_in_strong q´ H5...
    ∃ (wfp_Par q0´ (wfp_inst_Abs fq1 q0´´)); splits...
      applys wfcgr_par...
        etransitivity.
          apply Heq. applys¬ wfcgr_inst_Abs.

    rename p into p0, q into p1, p´ into q0, q´ into q1,
           q´´ into p1´´, q´0 into p1´, fp into fp0.
    apply (t_step _ wfcgr_step) in H.
    apply (t_step _ wfcgr_step) in H0.

    lets (q1´ & q1´´ & Htq1 & Hcq1´ & Hcq1´´) : congr_out H0 H5.
    lets (fq0 & Htq0 & Heq) : (congr_in_strong p0 q0 a fp0 H H4).
    ∃ (wfp_Par (wfp_inst_Abs fq0 q1´´) q1´); splits; simpls.
      applys¬ (TrTau2 a).
      applys× wfcgr_par; try solve [inverts¬ Hcq1´].
        etransitivity.
          apply Heq. applys¬ wfcgr_inst_Abs.

  ∃ (wfp_Par p´ wfp_Nil); splits...

  inverts Htp...
    destruct ap; inverts H3...
      ∃ w; splits...
    inverts H2...
    inverts H3...
    inverts H3...
  inverts Htp...
    destruct ap; inverts H3...
      ∃ (wfp_Par q w); splits...
    destruct aq; inverts H3...
      ∃ (wfp_Par w p); splits...
    ∃ (wfp_Par (wfp_inst_Abs fq p´´) p´0); splits...
    ∃ (wfp_Par q´ (wfp_inst_Abs fp q´´)); splits...

  inverts Htp...
    destruct ap; inverts H3.
    ∃ (wfp_Par (wfp_Par w q) r); splits...

    destruct aq; inverts H3.
    inverts H2...
      destruct ap; inverts H4.
      ∃ (wfp_Par (wfp_Par p w0) r); splits...
      destruct aq; inverts H4.
      ∃ (wfp_Par (wfp_Par p q) w0); splits...
      rename fq into fr; rename p´ into q´; rename p´´ into q´´.
      apply TrAct2 with (p := p) in H3.
      ∃ (wfp_Par (wfp_Par p q´) (wfp_inst_Abs fr q´´)); splits; simpls...
      rename fp into fq; rename q´ into r´; rename q´´ into r´´.
      apply TrAct2 with (p := p) in H3.
      ∃ (wfp_Par (wfp_inst_Abs (AbsPar2 p fq) r´´) r´); splits...
        simpls...

    rename p´0 into p´, fq into fqr.
      inverts H3...
      destruct ap; inverts H5... rename a0 into fq.
      assert ({{wfp_Par p q -- Tau ->> AP (wfp_Par p´ (wfp_inst_Abs fq p´´))}}) by applys¬ (TrTau1 a).
      ∃ (wfp_Par (wfp_Par p´ (wfp_inst_Abs fq p´´)) r); splits; simpl...
      destruct aq; inverts H5... rename a0 into fr.
      apply act1_out with (p2 := q) in H2.
      ∃ (wfp_Par (wfp_Par p´ q) (wfp_inst_Abs fr p´´)); splits; simpl...

    rename q´´ into qr´´, q´ into qr´. inverts H3...
      destruct ap; inverts H5.
      assert ({{wfp_Par p q -- Tau ->> AP (wfp_Par (wfp_inst_Abs fp qr´´) w)}}) by applys¬ (TrTau2 a).
      ∃ (wfp_Par (wfp_Par (wfp_inst_Abs fp qr´´) w) r); splits...
      destruct aq; inverts H5.
      apply act1_in with (p2 := q) in H2.
      ∃ (wfp_Par (wfp_inst_Abs (AbsPar1 fp q) qr´´) w); splits... simpls...

  inverts Htp...

    destruct ap; inverts H3.
    inverts H2...
      destruct ap; inverts H4...
      ∃ (wfp_Par w0 (wfp_Par q r)); splits...
      destruct aq; inverts H4...
      ∃ (wfp_Par p (wfp_Par w0 r)); splits...
      apply act1_in with (p2 := r) in H4.
      ∃ (wfp_Par p´ (wfp_inst_Abs (AbsPar1 fq r) p´´)); splits... simpls...
      apply act1_out with (p2 := r) in H4.
      ∃ (wfp_Par (wfp_inst_Abs fp q´´) (wfp_Par q´ r)); splits...

    destruct aq; inverts H3.
    ∃ (wfp_Par p (wfp_Par q w)); splits...

    rename p´´ into pq´´, p´0 into pq´, fq into fr.
      inverts H2...
      destruct ap; inverts H5.
      apply act2_in with (p1 := q) in H3.
      ∃ (wfp_Par w (wfp_inst_Abs (AbsPar2 q fr) pq´´)); splits... simpls...
      destruct aq; inverts H5.
      assert ({{wfp_Par q r -- Tau ->> AP (wfp_Par w (wfp_inst_Abs fr pq´´))}}) by applys¬ (TrTau1 a).
      ∃ (wfp_Par p (wfp_Par w (wfp_inst_Abs fr pq´´))); splits...

    rename q´´ into r´´, q´ into r´, fp into fpq.
    inverts H2...
      destruct ap; inverts H5. rename a0 into fp.
      apply act2_out with (p1 := q) in H3.
      ∃ (wfp_Par (wfp_inst_Abs fp r´´) (wfp_Par q r´)); splits... simpl...
      destruct aq; inverts H5. rename a0 into fq.
      assert ({{wfp_Par q r -- Tau ->> AP (wfp_Par (wfp_inst_Abs fq r´´) r´)}})...
      ∃ (wfp_Par p (wfp_Par (wfp_inst_Abs fq r´´) r´)). splits... simpls...

  ∃ p´; splits...
Qed.

Lemma congr_out_normal_strong : ∀ a (p p´ p´´ q: wfprocess),
      p ≡* q → {{p -- LabOut a p´´ ->> AP p´}} →
      ∃ (q´ q´´ : wfprocess), {{q -- LabOut a q´´ ->> AP q´}} ∧
      (∀ (m : chan) (X : var), (wfp_Par (wfp_Abs m X p´´) p´) ≡* (wfp_Par (wfp_Abs m X q´´) q´)).
Proof with (try solve [applys× t_step]; try apply wfcgr_par; automate).
  introv Hr; gen p´ p´´; inductions Hr.

  Focus 2.
  introv Htx.
  lets (q´ & q´´ & Hty & Heqy) : IHHr1 Htx.
  lets (r´ & r´´ & Htr & Heqr) : IHHr2 Hty.
  ∃ r´ r´´; splits...
  introv; etransitivity; jauto.

  inductions H.

  introv Ht; inverts Ht...
  ∃ wfp_Nil q; splits...
    introv...

  introv Ht; inverts Ht.

  introv Ht; inverts Ht...
    destruct ap; inverts H5...
    lets (q0´ & q0´´ & Htq & Hc´ & Hc´´) : congr_out p´ H4...
    ∃ (wfp_Par q0´ q´) q0´´; splits...
      introv; simpls...
        apply wfcgr_abs...
        apply wfcgr_par...
    destruct aq; inverts H5.
    lets (q1´ & q1´´ & Htq & Hc´ & Hc´´) : congr_out q´ H4...
    ∃ (wfp_Par p´ q1´) q1´´; splits...
      introv; simpls...
        apply wfcgr_abs...
        apply wfcgr_par...

  introv Ht.
  ∃ (wfp_Par p´ wfp_Nil) p´´; splits; introv...

  introv Ht; inverts Ht...
    destruct ap; inverts H3.
    ∃ w p´´; splits; introv...
    inverts H2.

  introv Ht; inverts Ht...
    destruct ap; inverts H3.
    ∃ (wfp_Par q w) p´´; splits; introv...
    destruct aq; inverts H3.
    ∃ (wfp_Par w p) p´´; splits; introv...

  introv Htp; inverts Htp...
    destruct ap; inverts H3.
    ∃ (wfp_Par (wfp_Par w q) r) p´´; splits; introv...
    inverts H2...
      destruct ap; inverts H3.
      ∃ (wfp_Par (wfp_Par p w) r) p´´; splits; introv...
      destruct aq0; inverts H3.
      ∃ (wfp_Par (wfp_Par p q) w) p´´; splits; introv...

  introv Htp; inverts Htp...
    inverts H2...
    destruct ap0; inverts H3.
    ∃ (wfp_Par w (wfp_Par q r)) p´´; splits; introv...
    destruct aq; inverts H3.
    ∃ (wfp_Par p (wfp_Par w r)) p´´; splits; introv...
    destruct aq; inverts H3.
    ∃ (wfp_Par p (wfp_Par q w)) p´´; splits; introv...

  introv Ht; ∃ p´ p´´; splits; introv...
Qed.

Lemma congr_out_normal : out_normal_relation wfcgr.
Proof.
  introv Hr Ht.
  lets HDexM : congr_out_normal_strong Hr Ht.
  destruct HDexM as (q´ & q´´ & Htq & Heq).
  ∃ q´ q´´; splits~; introv _ _ _ _; jauto.
Qed.

Lemma congr_in_normal : in_normal_relation wfcgr.
Proof.
  introv Hr Ht.
  lets Hin : congr_in_strong Hr Ht.
  destruct Hin as (fq & Htq & Hyp).
  ∃× fq.
Qed.

Lemma congr_closed : closed_relation wfcgr.
Proof.
  introv Hr Ht.
  lets Hin : congr_in_strong Hr Ht.
  destruct Hin as (fq & Htq & Hyp).
  ∃× fq.
Qed.

Lemma congr_out_context_strong :
  ∀ p q : wfprocess, p ≡* q →
    ∀ a (p´ p´´ : wfprocess),
      {{p--LabOut a p´´->>(AP p´)}} →
        ∃ (q´ q´´ : wfprocess),
          ({{q--LabOut a q´´->>(AP q´)}} ∧ ∀ X s,
            ((wfp_Par (wfp_subst p´´ X s) p´) ≡* (wfp_Par (wfp_subst q´´ X s) q´))).
Proof with (try apply wfcgr_subst1; try solve [applys× t_step]; automate).
  introv Hr; inductions Hr.

  Focus 2.
  introv Htx.
  specializes IHHr1 Htx. destruct IHHr1 as (q´ & q´´ & Htq & Hypq).
  specializes IHHr2 Htq. destruct IHHr2 as (r´ & r´´ & Htr & Hypr).
  ∃ r´ r´´; splits...
  introv; specialize (Hypq X s); specialize (Hypr X s).
  etransitivity; eassumption.

  inductions H; introv Ht.

    rename IHwfcgr_step into IH.
    inverts Ht...
    ∃ wfp_Nil q; splits...
      introv; apply wfcgr_par...

    inverts Ht.

    rename IHwfcgr_step1 into IH; rename IHwfcgr_step2 into IH1.
    inverts Ht...
      destruct ap; inverts H5.
      lets (q1 & q2 & Htq & Hypq) : IH H4; clear IH.
      ∃ (wfp_Par q1 q´) q2; splits; introv...
        introv; specialize (Hypq X s).
        etransitivity.
          constructor. apply WfCgrPar_assoc1.
          etransitivity.
            Focus 2. constructor. apply WfCgrPar_assoc2.
            applys wfcgr_par...
      destruct aq; inverts H5.
      lets (q1´ & q1´´ & Htq1 & Hypq1) : IH1 H4; clear IH1.
      ∃ (wfp_Par p´ q1´) q1´´; splits...
        introv; specialize (Hypq1 X s).
        assert (Hcp : (wfp_Par (wfp_subst p´´ X s) (wfp_Par w p)) ≡* (wfp_Par (wfp_subst p´´ X s) (wfp_Par p w)))...
        assert (Hcq : (wfp_Par (wfp_subst q1´´ X s) (wfp_Par q1´ p´)) ≡* (wfp_Par (wfp_subst q1´´ X s) (wfp_Par p´ q1´)))...
        etransitivity. symmetry. apply Hcp.
        etransitivity. Focus 2. apply Hcq.
         etransitivity.
          constructor. apply WfCgrPar_assoc1.
          etransitivity.
            Focus 2. constructor. apply WfCgrPar_assoc2.
            applys¬ wfcgr_par...

    ∃ (wfp_Par p´ wfp_Nil) p´´; splits; introv...

    inverts Ht...
      destruct ap; inverts H3...
      ∃ w p´´; splits; introv...
      inverts H2.

   inverts Ht...
     destruct ap; inverts H3.
     ∃ (wfp_Par q w) p´´; splits; introv...
     destruct aq; inverts H3.
     ∃ (wfp_Par w p) p´´; splits; introv...

   inverts Ht...
     destruct ap; inverts H3.
     ∃ (wfp_Par (wfp_Par w q) r) p´´; splits; introv...
     inverts H2...
       destruct ap; inverts H3.
       ∃ (wfp_Par (wfp_Par p w) r) p´´; splits; introv...
       destruct aq0; inverts H3.
       ∃ (wfp_Par (wfp_Par p q) w) p´´; splits; introv...

   inverts Ht...
     inverts H2...
     destruct ap0; inverts H3.
     ∃ (wfp_Par w (wfp_Par q r)) p´´; splits; introv...
     destruct aq; inverts H3.
     ∃ (wfp_Par p (wfp_Par w r)) p´´; splits; introv...
     destruct aq; inverts H3.
     ∃ (wfp_Par p (wfp_Par q w)) p´´; splits~; introv...

   ∃ p´ p´´; splits; introv...
Qed.

Lemma congr_out_context : out_context_relation wfcgr.
Proof.
  introv Hc Htp.
  lets (q´ & q´´ & Htq & Hyp) : congr_out_context_strong Hc Htp.
  ∃ q´ q´´; splits¬.
Qed.

Hint Resolve congr_in congr_out congr_rem congr_tau
             congr_in_normal congr_out_normal congr_closed
             congr_out_context : congr_bisim.

Lemma congr_IObisimulation : IO_bisimulation wfcgr.
Proof.
  splits; eauto with congr_bisim.
  apply wfcgr_is_eq_rel.
Qed.

Lemma congr_HObisimulation: HigherOrder_bisimulation wfcgr.
Proof.
  splits; auto with congr_bisim.
  apply wfcgr_is_eq_rel.
Qed.

Lemma congr_NORbisimulation: Normal_bisimulation wfcgr.
Proof.
  splits; auto with congr_bisim.
  apply wfcgr_is_eq_rel.
Qed.

Lemma congr_ONORbisimulation : OpenNormal_bisimulation wfcgr.
Proof.
  splits; auto with congr_bisim.
  apply wfcgr_is_eq_rel.
Qed.

Lemma congr_CONbisimulation : Context_bisimulation wfcgr.
Proof.
  splits; auto with congr_bisim.
  apply wfcgr_is_eq_rel.
Qed.

Hint Resolve congr_IObisimulation congr_HObisimulation
             congr_NORbisimulation congr_ONORbisimulation
             congr_CONbisimulation : congr_bisim.