Library HoweSound

Require Export Howe.

Notation refl0 Rel := ( P, is_proc P Rel P P).

Notation pseudo_sim :=
  ( {V W:Set} Rel (P1 Q1:proc V)(P2 Q2:proc W) a F1 C1 (f:V proc0)(g: W proc0),
   simulation Rel refl0 Rel rename_compatible Rel (Rincl sc0 Rel) trans Rel
    howe Rel P2 Q2 howe Rel P1 Q1
    ( v, is_proc (f v)) ( v, is_proc (g v))
    lts (bind f P1) (inp a) (ag_abs F1) lts (bind g P2) (out a) (ag_conc C1)
    F2 C2 P'2 Q'2, lts (bind f Q1) (inp a) (ag_abs F2)
                            lts (bind g Q2) (out a) (ag_conc C2)
                            sc0 P'2 (appr F1 C1)
                            sc0 Q'2 (appr F2 C2)
                            howe Rel P'2 Q'2).


Sequential proof, input then output


Lemma pseudo_inp_first {V:Set}:
   Rel (P1 Q1:proc V)(P2 Q2:proc0) a F1 (f:V proc0),
    simulation Rel refl0 Rel rename_compatible Rel
   ( P Q, Rel (P // PO) (Q // PO) Rel P Q)
   howe Rel P1 Q1 howe Rel P2 Q2 ( v, is_proc (f v))
   lts (bind f P1) (inp a) (ag_abs F1)
   F2, lts (bind f Q1) (inp a) (ag_abs F2)
                howe Rel (asubst F1 P2) (asubst F2 Q2).
Proof.
  introv Hsim Hrefl Hrename HpO Hp1q1. gen a f F1 P2 Q2.
  induction Hp1q1; introv Hp2q2 Hf HltsP1; try solve [inverts HltsP1].
  - forwards*: IHHp1q1 Hp2q2 HltsP1. destruct H1 as [F2 [Hltsf2 Hhowe]].
    forwards*: H0 f. destruct Hsim as [Hisproc Hsim].
    assert (is_agent (conc_def 0 Q2 PO)).
      intros_all. assert (is_proc Q2) by auto with howe.
      apply is_proc_bn in H3. rewrite H3 in H2. autofs.
    assert (Hwf:conc_wf (conc_def 0 Q2 PO)).
      intros_all. omega.
    forwards_test Rel.
    destruct F2 as [R']; destruct F'0 as [Q'1]; subst. simpl in H7.
    apply HpO in H7. repeat (rewrite mapN_id' in H7).
     (abs_def Q'1); intuition. simpl.
    apply howe_comp with (subst R' Q2); eauto with howe hopi.
      apply× oe_proc0.
  - simpl in ×. F1; intuition. destruct F1 as [P']; simpl.
    apply howe_subst; auto with howe. apply howe_refl.
    forwards: lts_is_proc HltsP1; auto with howe.
  - inverts HltsP1.
    + forwards: lts_inp_abs H2. destruct H as [F'1]. subst. simpl in H3.
      forwards*: IHHp1q1_1 Hp2q2 H2. destruct H as [F'2 [Hltsf'2 Hhowe]].
       (abs_parl F'2 (bind f Q')). split.
      eapply lts_parl'; eauto.
      inverts H3. destruct F'1 as [P'1]. destruct F'2 as [Q'1]. simpl.
      simpl in Hhowe. apply howe_par; auto with howe.
    + forwards: lts_inp_abs H2. destruct H as [F'1]. subst. simpl in H3.
      forwards*: IHHp1q1_2 Hp2q2 H2. destruct H as [F'2 [Hltsf'2 Hhowe]].
       (abs_parr (bind f Q) F'2 ). split.
      eapply lts_parr'; eauto.
      inverts H3. destruct F'1 as [P'1]. destruct F'2 as [Q'1]. simpl.
      simpl in Hhowe. apply howe_par; auto with howe.
  - inverts HltsP1. (abs_def (bind (liftV f) Q)). split.
    simpl. auto with hopi.
    simpl. apply howe_subst; auto with howe. apply× @howe_bind.
      intros [ |]; simpl; auto with howe.
  - simpl in ×. inverts HltsP1.
    pick_fresh_fset_V V
      (fn (bind (fun xmapN (fun x0S x0) (f x)) Q) \u
       fn P2 \u fn Q2) x.
    forwards: H4 x; auto.
    forwards: lts_inp_abs H1. destruct H3 as [Fx].
    rewrite H3 in H1.
    assert ( y, is_proc (mapN (fun x1S x1) (f y)))
      by auto with hopi.
    rewrite× <- @bind_open in H1.
    forwards*: H0 Hp2q2 H1.
    destruct H6 as [F'x [ HltsF'x HhoweF'x]]. destruct F'x as [P'x].
     (abs_def (nu (close 0 x P'x))). split.
    apply (lts_new' L) with (abs_def (close 0 x P'x)); auto.
    intros. rewrite× @bind_open in HltsF'x.
    forwards: lts_open HltsF'x; eauto.
      rewrite× <- @bind_open. apply× @is_proc_bind.
      forwards*: @howe_implies_proc (H x). intuition.
    destruct H8 as [A' [Ha' [HxA' HltsA']]]. specialize (HltsA' x0). simpl.
    inverts Ha'. destruct A' as [ |[Q''] |[] ]; inverts H9. simpl in HxA'.
    rewrite× @close_open. rewrite× subst_lab_id in HltsA'. simpl; autofs.
    destruct A as [ | [] | [] ]; inverts H3. inverts H2; simpl in ×.
    apply (howe_nu (L \u fn (subst p P2) \u fn (subst (close 0 x P'x) Q2))).
    intros. do 2 (rewrite <- bind_open; auto with hopi).
    asserts_rewrite ((fun x1 : incV Empty_setmapN (fun x2 : natS x2) (subst_func P2 x1))
      = subst_func P2).
      extens. intros [ |]; simpl; auto. rewrite is_proc_mapN; auto with howe.
    asserts_rewrite ((fun x1 : incV Empty_setmapN (fun x2 : natS x2) (subst_func Q2 x1))
      = subst_func Q2).
      extens. intros [ |]; simpl; auto. rewrite is_proc_mapN; auto with howe.
    asserts_rewrite (P'x= (open 0 x (close 0 x P'x))) in HhoweF'x.
      rewrite× @open_close. forwards*: lts_is_proc HltsF'x.
      forwards: @howe_implies_proc (H x); intuition.
    do 2 (rewrite bind_open in HhoweF'x; auto with hopi).
    forwards: @howe_rename HhoweF'x x0; auto.
      autofnF.
      rewrite <- bind_open; auto with hopi howe.
      forwards: lts_is_proc (H4 x); auto with hopi howe.
      rewrite <- bind_open; auto with hopi howe.
      forwards: @howe_implies_proc (H x); intuition.
      rewrite <- bind_open; auto with hopi howe.
      forwards*: @howe_implies_proc (H x); destruct_hyps.
      apply is_proc_bind; auto with hopi.
    do 2 (rewrite <- bind_open in H3; auto with hopi).
Qed.

Lemma pseudo_inp_conc {V:Set}: Rel (P1 Q1:proc V) a F1 C (f:V proc0),
    simulation Rel refl0 Rel rename_compatible Rel
   ( P Q, Rel (P // PO) (Q // PO) Rel P Q)
   howe Rel P1 Q1 is_agent (ag_conc C) ( v, is_proc (f v))
   lts (bind f P1) (inp a) (ag_abs F1)
   F2, lts (bind f Q1) (inp a) (ag_abs F2) howe Rel (appr F1 C) (appr F2 C).
Proof.
  intros. destruct C. pick_freshes_fset_V V (fn p \u fn p0 \u fn (bind f Q1)) n l.
  forwards: @pseudo_inp_first (open_list l p) (open_list l p) H2 H5; auto with hopi howe.
    apply howe_refl. apply is_proc_open_list. forwards: fresh_length Fr.
    simpl in H3. rewrite <- H6. intros. forwards: H3 k; autofs.
  destruct H6 as [F2 [HltsF2 Hhowe]]. repeat (rewrite bind_proc0 in Hhowe).
   F2; intuition. destruct F1 as [P'1]; destruct F2 as [P'2]; simpl in ×.
  assert (is_proc P'1). forwards: lts_is_proc H5; auto with howe.
  assert (is_proc P'2). forwards: lts_is_proc HltsF2; auto with howe.
  repeat (rewrite is_proc_mapN); auto. forwards: fresh_length Fr.
  subst. apply× @howe_open_list.
    simpl. apply fresh_union_l; auto. apply fresh_sub with (fn P'1 \u fn p).
    auto. apply fn_subst.
    simpl. apply fresh_union_l; auto. apply fresh_sub with (fn (bind f Q1) \u fn p).
    auto. forwards: @fn_subst P'2 p. forwards: lts_fn HltsF2. simpl in H9.
    assert (fn P'2 \u fn p \c fn (bind f Q1) \u fn p) by autofs. autofs.
    intros. simpl in H8. autofs. apply bn_subst in H9.
    rewrite× @is_proc_bn in H9. rewrite union_empty_l in H9.
    forwards: H3 k; autofs; try omega. forwards: H3 k; autofs; try omega.
    intros. simpl in H8. autofs. apply bn_subst in H9.
    rewrite is_proc_bn in H9; auto. rewrite union_empty_l in H9.
    forwards: H3 k; autofs; try omega. forwards: H3 k; autofs; try omega.
  repeat (rewrite open_list_par). repeat (rewrite open_list_subst).
  rewrite× (open_list_id P'1). rewrite× (open_list_id P'2).
  apply howe_par; auto with howe. apply howe_refl. apply is_proc_open_list.
  intros. forwards: H3 k; autofs; try omega.
Qed.

Lemma pseudo_sim_out : pseudo_sim.
Proof.
  introv Hsim Hrefl Hrename Hsc0 Htrans Hp2q2.
  assert ( P Q : proc0, Rel (P // PO) (Q // PO) Rel P Q) as HpO.
    intros. apply Htrans with (P//PO). apply Hsc0.
    destruct Hsim. apply sc0_def; auto with bisim sc.
    apply is_proc_sc with (P//PO); auto with bisim sc.
    apply Htrans with (Q//PO); auto. apply Hsc0.
    destruct Hsim. apply sc0_def; auto with bisim sc.
    apply is_proc_sc with (Q//PO); auto with bisim sc.
  gen a f g F1 C1 P1 Q1.
  induction Hp2q2; introv Hp1q1 Hf Hg HltsP1 HltsP2; try solve [inverts HltsP2].
  - forwards*: IHHp2q2 a F1 C1 P1 Q1.
    destruct H1 as [F2 [C2 [ P'2 [R' [HltsQ1 [ HltsR [Hp'2 [Hr' HhoweP1R]]]]]]]].
    forwards*: H0 g. destruct Hsim as [Hisproc Hsim].
    assert (is_agent F2) by auto with howe hopi.
    forwards_test Rel.
     F2 C'0 P'2 (appr F2 C'0); intuition.
    apply howe_comp with R'; auto with hopi howe.
      apply oe_trans with (appr F2 C2); auto.
      apply× oe_sc0. apply× oe_proc0.
  - forwards: @pseudo_inp_conc P1 Q1 F1 C1; eauto with hopi.
    destruct H as [F2 []]. F2 C1 (appr F1 C1) (appr F2 C1); intuition.
  - inverts HltsP2.
    + forwards: lts_out_conc H2. destruct H as [C'1]. subst. simpl in H3.
      forwards*: IHHp2q2_1 Hp1q1 HltsP1 H2.
      destruct H as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
      inverts Hp'2. inverts Hq'2.
       F'2 (conc_parl C'2 (bind g Q')) (P'2// bind g P') (Q'2//bind g Q').
      splits; eauto with hopi howe.
      eapply lts_parl'; eauto.
      apply sc0_trans with (appr F1 C'1 // bind g P'); auto with sc hopi howe.
      inverts H3. assert (struct_congr
        (appr F1 C'1 // bind g P') (appr F1 (conc_parl C'1 (bind g P')))).
        destruct F1, C'1; simpl. eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H3.
      apply sc0_trans with (appr F'2 C'2 // bind g Q'); auto with sc hopi howe.
      assert (struct_congr
        (appr F'2 C'2 // bind g Q') (appr F'2 (conc_parl C'2 (bind g Q')))).
        destruct F'2, C'2; simpl. eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H7.
    + forwards: lts_out_conc H2. destruct H as [C'1]. subst. simpl in H3.
      forwards*: IHHp2q2_2 Hp1q1 HltsP1 H2.
      destruct H as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
      inverts Hp'2. inverts Hq'2.
       F'2 (conc_parr (bind g Q) C'2) (bind g P // P'2) (bind g Q // Q'2).
      splits; eauto with hopi howe.
      eapply lts_parr'; eauto.
      apply sc0_trans with (bind g P // appr F1 C'1); auto with sc hopi howe.
      inverts H3. assert (struct_congr
        (bind g P // appr F1 C'1) (appr F1 (conc_parr (bind g P) C'1))).
        destruct F1, C'1; simpl. apply sc_trans with
          (genNu n (shiftN n (bind g P) // (subst ((shiftN n) p) p0 // p1))); eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H3.
      apply sc0_trans with (bind g Q // appr F'2 C'2); auto with sc hopi howe.
      assert (struct_congr (bind g Q // appr F'2 C'2)
                            (appr F'2 (conc_parr (bind g Q) C'2))).
        destruct F'2, C'2; simpl. apply sc_trans with
          (genNu n (shiftN n (bind g Q) // (subst ((shiftN n) p) p0 // p1))); eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H7.
  - inverts HltsP2. simpl.
    forwards*: @pseudo_inp_first Rel P1 Q1 (bind g P)(bind g Q).
      apply @howe_bind; auto with howe. apply HltsP1.
    destruct H as [F2 [HltsQ1 HhoweF1F2]]. assert ( F, fshiftN 0 F = F).
      destruct F; simpl; rewrite× @mapN_id'.
     F2 (conc_def 0 (bind g Q) (bind g Q'))
        (appr F1 (conc_def 0 (bind g P) (bind g P')))
        (appr F2 (conc_def 0 (bind g Q) (bind g Q'))); intuition auto with hopi howe;
      simpl; repeat (rewrite H); auto with sc hopi howe.
  - simpl in ×. inversion HltsP2; subst.
    pick_fresh_fset_V V
      (fn (bind (fun xmapN (fun x0S x0) (g x)) Q) \u fn (bind f Q1)) x.
    forwards*: H4 x. forwards: lts_out_conc H1. destruct H3 as [Cx].
    rewrite H3 in H1.
    assert ( y, is_proc (mapN (fun x1S x1) (g y))) by auto with hopi.
    rewrite <- bind_open in H1; auto with hopi.
    forwards: H0 Hp1q1 H1; auto with hopi.
      apply HltsP1.
    destruct H6 as [F'1 [ C'x [ P'x [Q'x [HltsF'x [HltsC'x [Hp'x [Hq'x HhoweF'x]]]]]]]].
    destruct C'x as [n P1x P2x].
    assert (lts (nu bind (fun x0mapN (fun x1S x1) (g x0)) Q) (out a)
        (conc_new (conc_def n (close n x P1x) (close n x P2x)))).
    apply (lts_new' L) with (conc_def n (close n x P1x) (close n x P2x)); auto.
    intros. rewrite bind_open in HltsC'x; auto with hopi.
    forwards: lts_open HltsC'x; eauto.
      rewrite <- bind_open; auto with hopi. apply is_proc_bind; auto with hopi.
      forwards: @howe_implies_proc (H x); auto. intuition.
    destruct H8 as [A' [Ha' [HxA' HltsA']]]. specialize (HltsA' x0). simpl.
    inverts Ha'. destruct A' as [ | [] |[] ]; inverts H9. simpl in HxA'.
    repeat (rewrite close_open; auto). rewrite subst_lab_id in HltsA'; auto. simpl; autofs.
     F'1 (conc_new (conc_def n (close n x P1x) (close n x P2x)))
        (nu close 0 x P'x) (nu close 0 x Q'x). splits; auto.
    assert (is_agent F1) by auto with howe hopi.
    assert (is_agent C1).
      forwards*: @lts_is_proc HltsP2.
      apply (proc_nu L). intros. unfold open. rewrite× <- @bind_open.
      apply× @is_proc_bind. forwards*: H x0. auto with howe. inverts Hp'x.
    apply sc0_def; auto with hopi.
      apply (proc_nu L). intros. auto with hopi.
    destructA A; inverts H2. fold (conc_new (conc_def n0 p p0)).
    apply sc_trans with (nu appr F1 (conc_def n0 p p0)); auto with sc.
    apply sc_nu'. destruct F1 as [P12].
    destruct Cx as [n1 px p0x]; inverts H3. simpl in ×.
    asserts_rewrite (genNu n1 (subst ((shiftN n1) P12) p // p0)
          = close 0 x (genNu n1 (subst ((shiftN n1) P12)(open n1 x p) //(open n1 x p0)))).
      rewrite close_genNu. simpl. fequals.
      rewrite close_subst. repeat (rewrite close_open); try solve [autofnF].
      rewrite× @close_id. autofnF.
    apply× @sc_close.
    apply sc_symmetric. apply× sc_F_newC.
      forwards*: H x. forwards*: lts_is_proc H1; auto with hopi howe.
      simpl in H3. rewrite <- H3 in H12.
      simpl in H12. intros. destruct (classic (k=n0)); try omega.
      forwards: H12 k. autobnF. omega.
    assert (is_agent F'1) by auto with howe hopi.
    inverts Hq'x.
    apply sc0_def; auto with hopi.
      apply (proc_nu L). intros. auto with hopi.
      apply× is_proc_app. forwards*: @lts_is_proc H6.
      apply (proc_nu L). intros. rewrite× <- @bind_open.
      apply× @is_proc_bind. forwards*: H x0. auto with howe.
    apply sc_trans with (nu appr F'1 (conc_def n (close n x P1x)(close n x P2x))); auto with sc.
    apply sc_nu'. destruct F'1 as [P12]. simpl in ×.
    asserts_rewrite (genNu n (subst ((shiftN n) P12) (close n x P1x) // (close n x P2x))
          = close 0 x (genNu n (subst ((shiftN n) P12) P1x // P2x))).
      rewrite close_genNu. simpl. fequals.
      rewrite close_subst. fequals. fequals. rewrite× @close_id.
      rewrite× @is_proc_mapN. forwards*: lts_fn HltsF'x. simpl in H11. autofnF.
    apply× @sc_close.
    apply sc_symmetric. apply× sc_F_newC.
      forwards*: lts_is_proc HltsC'x; auto with howe hopi.
      apply× @is_proc_bind. forwards*: H x. auto with howe.
      simpl in H11. intros. destruct (classic (k=n)); try omega.
      forwards: H11 k. autobnF. omega.
    apply (howe_nu (L \u fn (close 0 x P'x) \u fn (close 0 x Q'x))).
    intros. unfold open.
    eapply (howe_rename _ Hrename) with x; eauto;
          try solve [rewrite open_close; auto with howe].
      autofnF.
    rewrite open_close; auto with howe. rewrite open_close; auto with howe.
Qed.


Sequential proof, output then input


Lemma pseudo_out_first {V:Set}: Rel (P1 Q1:proc V)(P2 Q2:proc1) a C1
  (f:V proc0), simulation Rel refl0 Rel
  rename_compatible Rel (Rincl sc0 Rel) trans Rel
  howe Rel P1 Q1 howe Rel P2 Q2
  ( v, is_proc (f v))
  lts (bind f P1) (out a) (ag_conc C1)
   C2 P'2 Q'2, lts (bind f Q1) (out a) (ag_conc C2)
     sc0 P'2 (appr (abs_def P2) C1)
     sc0 Q'2 (appr (abs_def Q2) C2) howe Rel P'2 Q'2.
Proof.
  introv Hsim Hrefl Hrename Hsc0 Htrans Hp1q1. gen a f C1 P2 Q2.
  induction Hp1q1; introv Hp2q2 Hf HltsP1; try solve [inverts HltsP1].
  - forwards*: IHHp1q1 Hp2q2 HltsP1.
    destruct H1 as [C2 [P'2 [Q'2 [Hltsc2 [Hp'2 [Hq'2 Hhowe]]]]]].
    forwards: H0 f; auto. destruct Hsim as [Hisproc Hsim].
    assert (is_agent (abs_def Q2)) by (simpl; auto with howe).
    forwards_test Rel.
     C'0 P'2 (appr (abs_def Q2) C'0); intuition.
    apply howe_comp with Q'2; auto with hopi howe.
      apply oe_trans with (appr (abs_def Q2) C2); auto.
      apply× oe_sc0. apply× oe_proc0.
  - simpl in ×. assert (is_agent (ag_conc C1)) by auto with hopi.
    assert (is_proc (appr (abs_def P2) C1)).
      apply× is_proc_app. simpl; auto with hopi howe.
    assert (is_proc (appr (abs_def Q2) C1)).
      apply× is_proc_app. simpl; auto with hopi howe.
     C1 (appr (abs_def P2) C1)(appr (abs_def Q2) C1);
                                          intuition auto with sc.
    destruct C1 as [n P Q]; simpl.
    pick_freshes_fset_V V (fn P \u fn Q \u fn P2 \u fn Q2) n l.
    forwards: fresh_length Fr. subst.
    forwards*: @howe_subst Rel (open_list l P) (open_list l P) P2 Q2.
      apply× @howe_refl. apply× @is_proc_open_list. intros. forwards: H k; autofs.
    repeat (rewrite is_proc_mapN); auto with howe. apply× @howe_open_list.
      simpl. apply fresh_union_l; auto.
      apply fresh_sub with (fn P2 \u fn P). auto. apply fn_subst.
      simpl. apply fresh_union_l; auto.
      apply fresh_sub with (fn Q2 \u fn P). auto. apply fn_subst.
      intros. simpl in H3. autofs. apply bn_subst in H4.
      rewrite @is_proc_bn in H4; auto with howe. rewrite union_empty_l in H4.
      forwards: H k; autofs; try omega. forwards: H k; autofs; try omega.
      intros. simpl in H3. autofs. apply bn_subst in H4.
      rewrite @is_proc_bn in H4; auto with howe. rewrite union_empty_l in H4.
      forwards: H k; autofs; try omega. forwards: H k; autofs; try omega.
    repeat (rewrite open_list_par). repeat (rewrite open_list_subst).
    rewrite (open_list_id P2); auto with howe.
    rewrite (open_list_id Q2); auto with howe.
    apply howe_par; auto with howe. apply howe_refl. apply is_proc_open_list.
    intros. forwards: H k; autofs; try omega.
  - inverts HltsP1.
    + forwards: lts_out_conc H2. destruct H as [C'1]. subst. simpl in H3.
      forwards*: IHHp1q1_1 Hp2q2 H2.
      destruct H as [ C'2 [P'2 [Q'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]].
      inverts Hp'2. inverts Hq'2.
       (conc_parl C'2 (bind f Q')) (P'2// bind f P') (Q'2//bind f Q').
      splits; eauto with hopi howe.
      eapply lts_parl'; eauto.
      apply sc0_trans with (appr (abs_def P2) C'1 // bind f P');
                                                        auto with sc hopi howe.
      inverts H3. assert (struct_congr
        (appr (abs_def P2) C'1 // bind f P')
        (appr (abs_def P2) (conc_parl C'1 (bind f P')))).
        destruct C'1; simpl. eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H3.
      apply sc0_trans with (appr (abs_def Q2) C'2 // bind f Q');
                                                        auto with sc hopi howe.
      assert (struct_congr
        (appr (abs_def Q2) C'2 // bind f Q')
        (appr (abs_def Q2) (conc_parl C'2 (bind f Q')))).
        destruct C'2; simpl. eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H7.
    + forwards: lts_out_conc H2. destruct H as [C'1]. subst. simpl in H3.
      forwards*: IHHp1q1_2 Hp2q2 H2.
      destruct H as [ C'2 [P'2 [Q'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]].
      inverts Hp'2. inverts Hq'2.
       (conc_parr (bind f Q) C'2) (bind f P // P'2) (bind f Q // Q'2).
      splits; eauto with hopi howe.
      eapply lts_parr'; eauto.
      apply sc0_trans with (bind f P // appr (abs_def P2) C'1);
                                                      auto with sc hopi howe.
      inverts H3. assert (struct_congr
        (bind f P // appr (abs_def P2) C'1)
        (appr (abs_def P2) (conc_parr (bind f P) C'1))).
        destruct C'1; simpl. apply sc_trans with
          (genNu n (shiftN n (bind f P) // (subst ((shiftN n) P2) p // p0))); eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H3.
      apply sc0_trans with (bind f Q // appr (abs_def Q2) C'2); auto with sc hopi howe.
      assert (struct_congr (bind f Q // appr (abs_def Q2) C'2)
                   (appr (abs_def Q2) (conc_parr (bind f Q) C'2))).
        destruct C'2; simpl. apply sc_trans with
          (genNu n (shiftN n (bind f Q) // (subst ((shiftN n) Q2) p // p0))); eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H7.
  - inverts HltsP1. simpl.
    assert (is_proc (subst (mapN (fun xx) P2) (bind f P) // bind f P')).
      rewrite is_proc_mapN; auto with howe. auto with hopi howe.
    assert (is_proc (subst (mapN (fun xx) Q2) (bind f Q) // bind f Q')).
      rewrite is_proc_mapN; auto with howe. auto with hopi howe.
     (conc_def 0 (bind f Q) (bind f Q'))
        (appr (abs_def P2) (conc_def 0 (bind f P) (bind f P')))
        (appr (abs_def Q2) (conc_def 0 (bind f Q) (bind f Q')));
    simpl; intuition auto with hopi sc.
    repeat (rewrite is_proc_mapN; auto with howe).
  - simpl in ×. inversion HltsP1; subst.
    pick_fresh_fset_V V
      (fn (bind (fun xmapN (fun x0S x0) (f x)) Q) \u fn Q2 \u fn P2) x.
    forwards*: H4 x. forwards: lts_out_conc H1. destruct H3 as [Cx].
    rewrite H3 in H1.
    assert ( y, is_proc (mapN (fun x1S x1) (f y))) by auto with hopi.
    rewrite <- bind_open in H1; auto with hopi.
    forwards: H0 Hp2q2 H1; auto with hopi.
    destruct H6 as [ C'x [ P'x [Q'x [HltsC'x [Hp'x [Hq'x HhoweF'x]]]]]].
    destruct C'x as [n P1x P2x].
    assert (lts (nu bind (fun x0mapN (fun x1S x1) (f x0)) Q) (out a)
        (conc_new (conc_def n (close n x P1x) (close n x P2x)))).
    apply (lts_new' L) with (conc_def n (close n x P1x) (close n x P2x)); auto.
    intros. rewrite bind_open in HltsC'x; auto with hopi.
    forwards: lts_open HltsC'x; eauto with hopi.
      rewrite <- bind_open; auto with hopi. apply is_proc_bind; auto with hopi.
      forwards*: @howe_implies_proc (H x). intuition.
    destruct H8 as [A' [Ha' [HxA' HltsA']]]. specialize (HltsA' x0). simpl.
    inverts Ha'. destruct A' as [ | [] |[] ]; inverts H9. simpl in HxA'.
    repeat (rewrite× @close_open). rewrite× subst_lab_id in HltsA'. simpl; autofs.
     (conc_new (conc_def n (close n x P1x) (close n x P2x)))
        (nu close 0 x P'x) (nu close 0 x Q'x). splits×.
    assert (is_agent C1).
      forwards*: @lts_is_proc HltsP1.
      apply (proc_nu L). intros. rewrite× <- @bind_open.
      apply× @is_proc_bind. forwards*: H x0. auto with howe.
    inverts Hp'x. apply sc0_def; auto with hopi.
      apply (proc_nu L). intros. auto with hopi.
      apply× is_proc_app. simpl; auto with howe.
    destruct A as [ | [] |[] ]; inverts H2. fold (conc_new (conc_def n0 p p0)).
    apply sc_trans with (nu appr (abs_def P2)(conc_def n0 p p0)); auto with sc.
    apply sc_nu'. destruct Cx as [n1 px p0x]; inverts H3. simpl in ×.
    asserts_rewrite (genNu n1 (subst ((shiftN n1) P2) p // p0)
          = close 0 x (genNu n1 (subst ((shiftN n1) P2)(open n1 x p) //(open n1 x p0)))).
      rewrite close_genNu. simpl. fequals.
      rewrite close_subst. repeat (rewrite close_open); try solve [autofnF].
      rewrite× @close_id. autofnF.
    apply× @sc_close.
    apply sc_symmetric. apply× sc_F_newC.
      simpl; auto with howe.
      forwards*: H x. forwards*: lts_is_proc H1; auto with hopi howe.
      simpl in H3. rewrite <- H3 in H11.
      simpl in H11. intros. destruct (classic (k=n0)); try omega.
      forwards: H11 k. autobnF. omega.
    inverts Hq'x. apply sc0_def; auto with hopi.
      apply (proc_nu L). intros. auto with hopi.
      apply× is_proc_app. simpl; auto with howe. forwards*: @lts_is_proc H6.
      apply (proc_nu L). intros. rewrite× <- @bind_open.
      apply× @is_proc_bind. forwards*: H x0. auto with howe.
    apply sc_trans with (nu appr (abs_def Q2)
            (conc_def n (close n x P1x)(close n x P2x))); auto with sc.
    apply sc_nu'. simpl in ×.
    asserts_rewrite (genNu n (subst ((shiftN n) Q2) (close n x P1x) // (close n x P2x))
          = close 0 x (genNu n (subst ((shiftN n) Q2) P1x // P2x))).
      rewrite close_genNu. simpl. fequals.
      rewrite close_subst. do 2 fequals. rewrite× @close_id.
      rewrite× @is_proc_mapN. auto with howe.
    apply× @sc_close.
    apply sc_symmetric. apply× sc_F_newC.
      simpl; auto with howe.
      forwards*: lts_is_proc HltsC'x; auto with howe hopi.
      apply× @is_proc_bind. forwards*: H x. auto with howe.
      simpl in H10. intros. destruct (classic (k=n)); try omega.
      forwards: H10 k. autobnF. omega.
    apply (howe_nu (L \u fn (close 0 x P'x) \u fn (close 0 x Q'x))).
    intros. eapply (howe_rename _ Hrename) with x; eauto;
          try solve [rewrite open_close; auto with howe].
      autofnF.
    rewrite open_close; auto with howe. rewrite open_close; auto with howe.
Qed.

Lemma pseudo_sim_in : pseudo_sim.
Proof.
  introv Hsim Hrefl Hrename Hsc0 Htrans Hp2q2 Hp1q1. gen a f g F1 C1 P2 Q2.
  induction Hp1q1; introv Hp2q2 Hf Hg HltsP1 HltsP2; try solve [inverts HltsP1].
  - forwards*: IHHp1q1 a F1 C1 P2 Q2.
    destruct H1 as [F2 [C2 [ P'2 [R' [HltsQ1 [ HltsR [Hp'2 [Hr' HhoweP1R]]]]]]]].
    forwards*: H0 f. destruct Hsim as [Hisproc Hsim].
    assert (is_agent C2) by auto with howe hopi.
    assert (conc_wf C2). forwards*: lts_conc_wf HltsR.
    forwards_test Rel.
     F'0 C2 P'2 (appr F'0 C2); intuition.
    apply howe_comp with R'; auto with hopi howe.
      apply oe_trans with (appr F2 C2); auto.
      apply× oe_sc0. apply× oe_proc0.
  - simpl in ×. destruct F1 as [P'1].
    forwards: @pseudo_out_first P2 Q2 P'1 P'1 C1; eauto with howe hopi.
    destruct H as [C2 [ P'2 [Q'2 [HltsC2 [Hp'2 [Hq'2 Hhowe]]]]]].
     (abs_def P'1) C2 P'2 Q'2; intuition.
  - inverts HltsP1.
    + forwards: lts_inp_abs H2. destruct H as [F'1]. subst. simpl in H3.
      forwards*: IHHp1q1_1 Hp2q2 H2 HltsP2.
      destruct H as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
      inverts Hp'2. inverts Hq'2.
       (abs_parl F'2 (bind f Q')) C'2 (P'2// bind f P') (Q'2//bind f Q').
      splits; eauto with hopi howe.
      eapply lts_parl'; eauto.
      apply sc0_trans with (appr F'1 C1 // bind f P'); auto with sc hopi howe.
      inverts H3. assert (struct_congr
        (appr F'1 C1 // bind f P') (appr (abs_parl F'1 (bind f P')) C1)).
        destruct F'1, C1; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
        apply sc_trans with
          (genNu n (subst ((shiftN n) p) p0 // p1 // (shiftN n)(bind f P'))); eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H3.
      apply sc0_trans with (appr F'2 C'2 // bind f Q'); auto with sc hopi howe.
      assert (struct_congr
        (appr F'2 C'2 // bind f Q') (appr (abs_parl F'2 (bind f Q')) C'2)).
        destruct F'2, C'2; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
        apply sc_trans with
          (genNu n (subst ((shiftN n) p) p0 // p1 // (shiftN n)(bind f Q'))); eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H7.
    + forwards: lts_inp_abs H2. destruct H as [F'1]. subst. simpl in H3.
      forwards*: IHHp1q1_2 Hp2q2 H2 HltsP2.
      destruct H as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
      inverts Hp'2. inverts Hq'2.
       (abs_parr (bind f Q) F'2) C'2 (bind f P // P'2) (bind f Q // Q'2).
      splits; eauto with hopi howe.
      eapply lts_parr'; eauto.
      apply sc0_trans with (bind f P // appr F'1 C1); auto with sc hopi howe.
      inverts H3. assert (struct_congr
        (bind f P // appr F'1 C1) (appr (abs_parr (bind f P) F'1) C1)).
        destruct F'1, C1; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
      apply sc_trans with
          (genNu n (shiftN n (bind f P) // (subst ((shiftN n) p) p0 // p1))); eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H3.
      apply sc0_trans with (bind f Q // appr F'2 C'2); auto with sc hopi howe.
      assert (struct_congr (bind f Q // appr F'2 C'2)
                            (appr (abs_parr (bind f Q) F'2) C'2)).
        destruct F'2, C'2; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
      apply sc_trans with
          (genNu n (shiftN n (bind f Q) // (subst ((shiftN n) p) p0 // p1))); eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H7.
  - inverts HltsP1. simpl. forwards*: @pseudo_out_first Rel P2 Q2 (bind (liftV f) P)(bind (liftV f) Q).
      apply× @howe_bind. intros [|]; simpl; auto with howe. apply HltsP2.
    destruct H as [ C'2 [P'2 [Q'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]].
     (abs_def (bind (liftV f) Q)) C'2 P'2 Q'2; intuition.
  - simpl in ×. inversion HltsP1; subst.
    pick_fresh_fset_V V
      (fn (bind (fun xmapN (fun x0S x0) (f x)) Q) \u fn (bind g Q2)) x.
    forwards*: H4 x. forwards: lts_inp_abs H1. destruct H3 as [Fx].
    rewrite H3 in H1.
    assert ( y, is_proc (mapN (fun x1S x1) (f y))) by auto with hopi.
    rewrite <- bind_open in H1; auto with hopi.
    forwards: H0 Hp2q2 H1; auto with hopi.
      apply HltsP2.
    destruct H6 as [F'x [ C'1 [ P'x [Q'x [HltsF'x [HltsC'1 [Hp'x [Hq'x HhoweF'x]]]]]]]].
    destruct F'x as [Pfx].
    assert (lts (nu bind (fun x0mapN (fun x1S x1) (f x0)) Q) (inp a)
        (abs_new (abs_def (close 0 x Pfx)))).
    apply (lts_new' L) with (abs_def (close 0 x Pfx)); auto.
    intros. rewrite× @bind_open in HltsF'x.
    forwards: lts_open HltsF'x; eauto.
      rewrite <- bind_open; auto. apply is_proc_bind; auto.
      forwards: @howe_implies_proc (H x); auto. intuition.
    destruct H8 as [A' [Ha' [HxA' HltsA']]]. specialize (HltsA' x0). simpl.
    inverts Ha'. destruct A' as [ |[Q''] |[] ]; inverts H9. simpl in HxA'.
    rewrite× @close_open. rewrite× subst_lab_id in HltsA'. simpl; autofs.
     (abs_new (abs_def (close 0 x Pfx))) C'1
        (nu close 0 x P'x) (nu close 0 x Q'x). splits; auto.
    assert (is_agent C1) by auto with howe hopi.
    assert (is_agent F1).
      forwards*: @lts_is_proc HltsP1.
      apply (proc_nu L). intros. rewrite× <- @bind_open.
      apply× @is_proc_bind. forwards*: H x0. auto with howe.
    inverts Hp'x. apply sc0_def; auto with hopi.
      apply (proc_nu L); auto with hopi.
    destructA A; inverts H2.
    apply sc_trans with (nu appr (abs_def p) C1); auto with sc.
    apply sc_nu'. destruct C1 as [n P22 P23].
    destruct Fx as [px]; inverts H3. simpl in ×.
    asserts_rewrite (genNu n (subst ((shiftN n) p) P22 // P23)
          = close 0 x (genNu n (subst ((shiftN n)(open 0 x p)) P22 // P23))).
      rewrite close_genNu. simpl. fequals.
      rewrite close_subst. rewrite mapN_open; auto using shiftN_injective.
      replace (n+0) with n by omega. rewrite close_open; try solve [autofnF].
      repeat (rewrite× @close_id).
    apply× @sc_close. apply sc_symmetric. apply× (sc_newF_C (abs_def p)).
    assert (is_agent C'1) by auto with howe hopi.
    inverts Hq'x. apply sc0_def; auto with hopi.
      apply (proc_nu L); auto with hopi.
      apply× is_proc_app. forwards*: @lts_is_proc H6.
      apply (proc_nu L). intros. rewrite× <- @bind_open.
      apply× @is_proc_bind. forwards*: H x0. auto with howe.
    apply sc_trans with (nu appr (abs_def (close 0 x Pfx)) C'1); auto with sc.
    apply sc_nu'. destruct C'1 as [n P22 P23]. simpl in ×.
    asserts_rewrite (genNu n (subst ((shiftN n)(close 0 x Pfx)) P22 // P23)
          = close 0 x (genNu n (subst ((shiftN n) Pfx) P22 // P23))).
      rewrite close_genNu. simpl. fequals.
      rewrite close_subst. forwards*: lts_fn HltsC'1. simpl in H11.
      rewrite <- mapN_close. replace (n+0) with n by omega.
      repeat fequals; rewrite× @close_id.
      assert (fn P22 \c fn (bind g Q2)).
        apply subset_trans with (fn P22 \u fn P23); auto. autofs.
      autofnF.
      assert (fn P23 \c fn (bind g Q2)).
        apply subset_trans with (fn P22 \u fn P23); auto. autofs.
      autofnF.
    apply× @sc_close.
    apply sc_symmetric. apply× (sc_newF_C (abs_def (close 0 x Pfx))).
    apply (howe_nu (L \u fn (close 0 x P'x) \u fn (close 0 x Q'x))).
    intros. eapply (howe_rename _ Hrename) with x; eauto;
          try solve [rewrite open_close; auto with howe].
      autofnF.
    do 2 (rewrite open_close; auto with howe).
Qed.


Simultaneous proof

the measure is lexico ordering of (size of output proof, size of input proof) see the variable case for input to see why. For a calculus with join patterns, the ordering should be lexico of (sum of size of outputs, size of input)

Lemma pseudo_sim_sim' :
  ( {V W:Set} Rel (P1 Q1:proc V)(P2 Q2:proc W) a F1 C1 (f:V proc0)(g: W proc0) n1 n2,
   simulation Rel refl0 Rel rename_compatible Rel (Rincl sc0 Rel) trans Rel
    howe' Rel P2 Q2 n2 howe' Rel P1 Q1 n1
    ( v, is_proc (f v)) ( v, is_proc (g v))
    lts (bind f P1) (inp a) (ag_abs F1) lts (bind g P2) (out a) (ag_conc C1)
    F2 C2 P'2 Q'2 n3, lts (bind f Q1) (inp a) (ag_abs F2)
                               lts (bind g Q2) (out a) (ag_conc C2)
                               sc0 P'2 (appr F1 C1)
                               sc0 Q'2 (appr F2 C2)
                               howe' Rel P'2 Q'2 n3).
Proof.
  introv Hsim Hrefl Hrename Hsc0 Htrans.
  Require Import TLC.LibWf.
  assert (wf (lexico2 lt lt)).
    rewrite <- LibNat.lt_peano.
    apply wf_lexico2; auto with wf.
  remember (n2, n1) as p. gen V W.
  gen n1 n2 a F1 C1.
  induction_wf: H p. intros n1 n2 Hp. subst.
  assert ( (V2 : Set) (a:var) (P1 Q1 : proc1) (n1 : nat) (P2 Q2 : proc V2),
     howe' Rel P1 Q1 n1
      howe' Rel P2 Q2 n2
          (g : V2 proc0) (C1 : conc),
           ( v : V2, is_proc (g v))
               lts (bind g P2) (out a) C1
                  (C2:conc) P'2 Q'2 x3,
                     lts (bind g Q2) (out a) C2
                    sc0 P'2 (appr (abs_def P1) C1)
                    sc0 Q'2 (appr (abs_def Q1) C2) howe' Rel P'2 Q'2 x3).
  { intros.
    assert (howe' Rel (a? P1) (a? Q1)(S n0)) by auto with howe.
    remember (pr_var (V:=Empty_set)) as f.
    assert ( P, bind (liftV f) P = P).
      intros; rewrite× @bind_return. intros [|]; simpl; auto.
      intros. inverts e.
    destruct H1; try solve [inverts H3].
    - forwards*: IH (k, S n0) f H6 H4 H3; try solve [subst; simpl; eauto with hopi].
      destruct_hyps. assert (is_agent x) by auto with hopi howe. simpl in H8.
      inverts H8. specialize (H7 g H2). destruct Hsim as [ Hbla Hsim].
      rewrite H5 in ×.
      forwards_test Rel.
       C'0 x1 (appr (abs_def Q1) C'0)(S x3); intuition.
        apply howe_comp' with x2; auto with hopi howe.
        apply oe_trans with (appr (abs_def Q1) x0); auto.
        apply× oe_sc0. apply× oe_proc0.
    - simpl in ×. assert (is_agent (ag_conc C1)) by auto with hopi.
      assert (is_proc (appr (abs_def P1) C1)).
        apply× is_proc_app. simpl; auto with hopi howe.
      assert (is_proc (appr (abs_def Q1) C1)).
        apply× is_proc_app. simpl; auto with hopi howe.
      assert ( n3, howe' Rel (appr (abs_def P1) C1) (appr (abs_def Q1) C1) n3).
        destruct C1 as [n P Q]; simpl.
        pick_freshes_fset_V V2 (fn P \u fn Q \u fn P1 \u fn Q1) n l.
        forwards: fresh_length Fr. subst.
        forwards*: @howe_subst Rel (open_list l P) (open_list l P) P1 Q1.
          eapply @howe'_implies_howe; eauto.
          apply× @howe_refl. apply× @is_proc_open_list.
          intros. forwards: H1 k; autofs.
        apply× @howe_implies_howe'.
        repeat (rewrite is_proc_mapN); auto with howe. apply× @howe_open_list.
        simpl. apply fresh_union_l; auto.
        apply fresh_sub with (fn P1 \u fn P). auto. apply fn_subst.
        simpl. apply fresh_union_l; auto.
        apply fresh_sub with (fn Q1 \u fn P). auto. apply fn_subst.
        intros. simpl in H9. autofs. apply bn_subst in H10.
        rewrite @is_proc_bn in H10; auto with howe. rewrite union_empty_l in H10.
        forwards: H1 k; autofs; try omega. forwards: H1 k; autofs; try omega.
        intros. simpl in H9. autofs. apply bn_subst in H10.
        rewrite @is_proc_bn in H10; auto with howe. rewrite union_empty_l in H10.
        forwards: H1 k; autofs; try omega. forwards: H1 k; autofs; try omega.
        repeat (rewrite open_list_par). repeat (rewrite open_list_subst).
        rewrite (open_list_id P1); auto with howe.
        rewrite (open_list_id Q1); auto with howe.
        apply howe_par; auto with howe. apply howe_refl. apply is_proc_open_list.
        intros. forwards: H1 k; autofs; try omega.
      destruct H8. C1 (appr (abs_def P1) C1)(appr (abs_def Q1) C1) x0;
      intuition auto with sc.
  - inverts H3.
    + forwards: lts_out_conc H8. destruct H1 as [C'1].
      rewrite_all H1 in *; clear H1. simpl in H9.
      forwards*: IH f H1_ H4 H8; try solve [subst; simpl; eauto with hopi].
        apply lexico2_1. omega.
      destruct H1 as [ F2 [ C'2 [P'2 [Q'2 [ n3 [ HltsF2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]]].
      inverts Hp'2. inverts Hq'2. inverts HltsF2.
      rewrite H5 in H3,H6, H11, H10.
      assert ( n4, howe' Rel (P'2// bind g P') (Q'2//bind g Q') n4).
        apply× @howe_implies_howe'. apply howe'_implies_howe in H1_0.
        apply howe'_implies_howe in Hhowe. apply× @howe_par. apply× @howe_bind.
        intros; auto with howe hopi.
      destruct H12.
       (conc_parl C'2 (bind g Q')) (P'2// bind g P') (Q'2//bind g Q') x.
      splits; eauto with hopi howe.
      eapply lts_parl'; eauto.
      apply sc0_trans with (appr (abs_def P1) C'1 // bind g P');
                                                        auto with sc hopi howe.
      inverts H9. assert (struct_congr
        (appr (abs_def P1) C'1 // bind g P')
        (appr (abs_def P1) (conc_parl C'1 (bind g P')))).
        destruct C'1; simpl. eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H9.
      apply sc0_trans with (appr (abs_def Q1) C'2 // bind g Q');
                                                        auto with sc hopi howe.
      assert (struct_congr
        (appr (abs_def Q1) C'2 // bind g Q')
        (appr (abs_def Q1) (conc_parl C'2 (bind g Q')))).
        destruct C'2; simpl. eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H13.
    + forwards: lts_out_conc H8. destruct H1 as [C'1].
      rewrite_all H1 in *; clear H1. simpl in H9.
      forwards*: IH f H1_0 H4 H8; try solve [subst; simpl; eauto with hopi].
        apply lexico2_1. omega.
      destruct H1 as [ F2 [ C'2 [P'2 [Q'2 [ n3 [ HltsF2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]]].
      inverts Hp'2. inverts Hq'2. inverts HltsF2.
      rewrite H5 in H3,H6, H11, H10.
      assert ( n4, howe' Rel (bind g P // P'2) (bind g Q // Q'2) n4).
        apply× @howe_implies_howe'. apply howe'_implies_howe in H1_.
        apply howe'_implies_howe in Hhowe. apply× @howe_par. apply× @howe_bind.
        intros; auto with howe hopi.
      destruct H12.
       (conc_parr (bind g Q) C'2) (bind g P // P'2) (bind g Q // Q'2) x.
      splits; eauto with hopi howe.
      eapply lts_parr'; eauto.
      apply sc0_trans with (bind g P // appr (abs_def P1) C'1);
                                                      auto with sc hopi howe.
      inverts H9. assert (struct_congr
        (bind g P // appr (abs_def P1) C'1)
        (appr (abs_def P1) (conc_parr (bind g P) C'1))).
        destruct C'1; simpl. apply sc_trans with
          (genNu n (shiftN n (bind g P) // (subst ((shiftN n) P1) p // p0))); eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H9.
      apply sc0_trans with (bind g Q // appr (abs_def Q1) C'2); auto with sc hopi howe.
      assert (struct_congr (bind g Q // appr (abs_def Q1) C'2)
                   (appr (abs_def Q1) (conc_parr (bind g Q) C'2))).
        destruct C'2; simpl. apply sc_trans with
          (genNu n (shiftN n (bind g Q) // (subst ((shiftN n) Q1) p // p0))); eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H13.
  - inverts H3. simpl.
    assert (is_proc (subst (mapN (fun xx) P1) (bind g P) // bind g P')).
      rewrite is_proc_mapN; auto with howe. auto with hopi howe.
    assert (is_proc (subst (mapN (fun xx) Q1) (bind g Q) // bind g Q')).
      rewrite is_proc_mapN; auto with howe. auto with hopi howe.
    assert ( n, howe' Rel (appr (abs_def P1) (conc_def 0 (bind g P) (bind g P')))
        (appr (abs_def Q1) (conc_def 0 (bind g Q) (bind g Q'))) n).
      apply× @howe_implies_howe'. simpl. apply howe'_implies_howe in H1_.
      apply howe'_implies_howe in H1_0. apply howe'_implies_howe in H0.
      repeat (rewrite is_proc_mapN; auto with howe).
    destruct H6.
     (conc_def 0 (bind g Q) (bind g Q'))
        (appr (abs_def P1) (conc_def 0 (bind g P) (bind g P')))
        (appr (abs_def Q1) (conc_def 0 (bind g Q) (bind g Q'))) x;
    intuition auto with hopi sc.
  - simpl in ×. inversion H3.
    pick_fresh_fset_V V2
      (fn (bind (fun xmapN (fun x0S x0) (g x)) Q) \u fn Q1 \u fn P1) x.
    forwards*: H9 x. forwards: lts_out_conc H10. destruct H11 as [Cx].
    rewrite H11 in H10.
    assert ( y, is_proc (mapN (fun x1S x1) (g y))) by auto with hopi.
    rewrite <- bind_open in H10; auto with hopi. forwards*: H1 x.
    forwards: IH f H13 H4 H10; try solve [subst; simpl; eauto with hopi].
      apply lexico2_1. omega.
    destruct H14 as [ F2 [ C'x [ P'x [Q'x [n3 [HltsF2 [HltsC'x [Hp'x [Hq'x HhoweF'x]]]]]]]]].
    destruct C'x as [n P1x P2x].
    assert (lts (nu bind (fun x0mapN (fun x1S x1) (g x0)) Q) (out a)
        (conc_new (conc_def n (close n x P1x) (close n x P2x)))).
    apply (lts_new' L) with (conc_def n (close n x P1x) (close n x P2x)); auto.
    intros. rewrite bind_open in HltsC'x; auto with hopi.
    forwards: lts_open HltsC'x; eauto with hopi.
      rewrite <- bind_open; auto with hopi.
    destruct H16 as [A' [Ha' [HxA' HltsA']]]. specialize (HltsA' x0). simpl.
    inverts Ha'. destructA A'; inverts H17. simpl in HxA'.
    repeat (rewrite close_open; auto). rewrite subst_lab_id in HltsA'; auto. simpl; autofs.
    assert ( n, howe' Rel (nu close 0 x P'x) (nu close 0 x Q'x) n).
      apply× @howe_implies_howe'.
      apply (howe_nu (L \u fn (close 0 x P'x) \u fn (close 0 x Q'x))).
      intros. eapply (howe_rename _ Hrename) with x; eauto;
          try solve [rewrite open_close; auto with howe].
      autofnF.
      rewrite open_close; auto with howe. rewrite open_close; auto with howe.
      apply howe'_implies_howe in HhoweF'x; auto.
    destruct H15. inverts HltsF2. rewrite H5 in Hq'x, Hp'x.
     (conc_new (conc_def n (close n x P1x) (close n x P2x)))
        (nu close 0 x P'x) (nu close 0 x Q'x) x0. splits×.
    assert (is_agent C1).
      forwards*: @lts_is_proc H3.
      apply (proc_nu L). intros. rewrite× <- @bind_open.
      apply× @is_proc_bind. forwards*: H1 x1. auto with howe.
    inverts Hp'x. apply sc0_def; auto with hopi.
      apply (proc_nu L); auto with hopi.
      apply× is_proc_app. simpl; auto with howe.
    destruct A as [ | [] |[] ]; inverts H7. fold (conc_new (conc_def n2 p p0)).
    inverts H11.
    apply sc_trans with (nu appr (abs_def P1)(conc_def n2 p p0)); auto with sc.
    apply sc_nu'. simpl.
    asserts_rewrite (genNu n2 (subst ((shiftN n2) P1) p // p0)
          = close 0 x (genNu n2 (subst ((shiftN n2) P1)(open n2 x p) //(open n2 x p0)))).
      rewrite close_genNu. simpl. fequals.
      rewrite close_subst. repeat (rewrite close_open); try solve [autofnF].
      rewrite× @close_id. autofnF.
    apply× @sc_close.
    apply sc_symmetric. subst. apply× sc_F_newC.
      simpl; auto with howe.
      forwards*: H1 x. forwards*: lts_is_proc H10; auto with hopi howe.
      intros. destruct (classic (k0=n2)); try omega.
      forwards: H7 k0. autobnF. omega.
    inverts Hq'x.
    apply sc0_def; auto with hopi.
      apply (proc_nu L); auto with hopi.
      apply× is_proc_app. simpl; auto with howe. forwards*: @lts_is_proc H14.
      apply (proc_nu L). intros. rewrite× <- @bind_open.
      apply× @is_proc_bind. forwards*: H1 x1. auto with howe.
    apply sc_trans with (nu appr (abs_def Q1)
            (conc_def n (close n x P1x)(close n x P2x))); auto with sc.
    apply sc_nu'. simpl in ×.
    asserts_rewrite (genNu n (subst ((shiftN n) Q1) (close n x P1x) // (close n x P2x))
          = close 0 x (genNu n (subst ((shiftN n) Q1) P1x // P2x))).
      rewrite close_genNu. simpl. fequals.
      rewrite close_subst. do 2 fequals. rewrite× @close_id.
      rewrite× @is_proc_mapN. auto with howe.
    apply× @sc_close.
    apply sc_symmetric. apply× sc_F_newC.
      simpl; auto with howe.
      forwards*: lts_is_proc HltsC'x; auto with howe hopi.
      intros. destruct (classic (k0=n)); try omega.
      forwards: H19 k0. autobnF. omega.
    }
  intros. destruct H2; try solve [inverts H5].
  + forwards*: IH H1 H7; try solve [simpl; eauto with hopi].
    destruct H9 as [F2 [C2 [ P'2 [R' [n3 [HltsQ1 [ HltsR [Hp'2 [Hr' HhoweP1R]]]]]]]]].
    forwards*: H8 f. destruct Hsim as [Hisproc Hsim].
    assert (is_agent C2) by auto with howe hopi.
    assert (conc_wf C2). forwards*: lts_conc_wf HltsR.
    forwards_test Rel.
    assert ( n, howe' Rel P'2 (appr F'0 C2) n).
      apply× @howe_implies_howe'. apply howe'_implies_howe in HhoweP1R.
      apply howe_comp with R'; auto with hopi howe.
      apply oe_trans with (appr F2 C2); auto.
      apply× oe_sc0. apply× oe_proc0.
    destruct H17. F'0 C2 P'2 (appr F'0 C2) x; intuition.
  + simpl in ×. destruct F1 as [P1'].
    assert ( n1, howe' Rel P1' P1' n1).
      apply howe_implies_howe'; auto with howe hopi.
    destruct H2. forwards*: H0 H2 H1 H6. destruct_hyps.
    do 5 eexists; intuition (try eassumption).
  + inverts H5.
    - forwards: lts_inp_abs H9. destruct H2 as [F'1]. subst. simpl in H10.
      forwards*: IH H1 H2_; try solve [simpl; eauto with hopi].
        apply lexico2_2; omega.
      destruct H2 as [F'2 [ C'2 [P'2 [Q'2 [n3 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]]].
      inverts Hp'2. inverts Hq'2.
      assert ( n4, howe' Rel (P'2 // bind f P') (Q'2 // bind f Q') n4).
        apply× @howe_implies_howe'. apply howe'_implies_howe in H2_0.
        apply howe'_implies_howe in Hhowe. auto with hopi howe.
      destruct H13.
       (abs_parl F'2 (bind f Q')) C'2 (P'2// bind f P') (Q'2//bind f Q') x.
      splits; eauto with hopi howe.
      eapply lts_parl'; eauto.
      apply sc0_trans with (appr F'1 C1 // bind f P'); auto with sc hopi howe.
      inverts H10. assert (struct_congr
        (appr F'1 C1 // bind f P') (appr (abs_parl F'1 (bind f P')) C1)).
        destruct F'1, C1; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
        apply sc_trans with
          (genNu n (subst ((shiftN n) p) p0 // p1 // (shiftN n)(bind f P'))); eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H10.
      apply sc0_trans with (appr F'2 C'2 // bind f Q'); auto with sc hopi howe.
      assert (struct_congr
        (appr F'2 C'2 // bind f Q') (appr (abs_parl F'2 (bind f Q')) C'2)).
        destruct F'2, C'2; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
        apply sc_trans with
          (genNu n (subst ((shiftN n) p) p0 // p1 // (shiftN n)(bind f Q'))); eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H14.
    - forwards: lts_inp_abs H9. destruct H2 as [F'1]. subst. simpl in H10.
      forwards*: IH H1 H2_0; try solve [simpl; eauto with hopi].
        apply lexico2_2; omega.
      destruct H2 as [F'2 [ C'2 [P'2 [Q'2 [n3 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]]].
      inverts Hp'2. inverts Hq'2.
      assert ( n4, howe' Rel (bind f P // P'2) (bind f Q // Q'2) n4).
        apply× @howe_implies_howe'. apply howe'_implies_howe in H2_.
        apply howe'_implies_howe in Hhowe. auto with hopi howe.
      destruct H13.
       (abs_parr (bind f Q) F'2) C'2 (bind f P // P'2) (bind f Q // Q'2) x.
      splits; eauto with hopi howe.
      eapply lts_parr'; eauto.
      apply sc0_trans with (bind f P // appr F'1 C1); auto with sc hopi howe.
      inverts H10. assert (struct_congr
        (bind f P // appr F'1 C1) (appr (abs_parr (bind f P) F'1) C1)).
        destruct F'1, C1; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
      apply sc_trans with
          (genNu n (shiftN n (bind f P) // (subst ((shiftN n) p) p0 // p1))); eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H10.
      apply sc0_trans with (bind f Q // appr F'2 C'2); auto with sc hopi howe.
      assert (struct_congr (bind f Q // appr F'2 C'2)
                            (appr (abs_parr (bind f Q) F'2) C'2)).
        destruct F'2, C'2; simpl. rewrite <- mapV_mapN. rewrite subst_shift.
      apply sc_trans with
          (genNu n (shiftN n (bind f Q) // (subst ((shiftN n) p) p0 // p1))); eauto with sc.
      apply sc0_def; eauto with sc hopi howe. forwards*: @is_proc_sc H14.
  + inverts H5. assert ( n1, howe' Rel (bind (liftV f) P)(bind (liftV f) Q) n1).
      apply× @howe_implies_howe'. apply× @howe_bind. apply× @howe'_implies_howe. eassumption.
      intros [|]; simpl; auto with howe.
    destruct H5. forwards*: H0 H5 H1 H6. destruct_hyps.
    do 5 eexists; intuition (try eassumption).
    simpl. auto with hopi.
  + simpl in ×. inversion H5; subst.
    pick_fresh_fset_V V
      (fn (bind (fun xmapN (fun x0S x0) (f x)) Q) \u fn (bind g Q2)) x.
    forwards*: H10 x. forwards: lts_inp_abs H7. destruct H9 as [Fx].
    rewrite H9 in H7.
    assert ( y, is_proc (mapN (fun x1S x1) (f y))) by auto with hopi.
    rewrite <- bind_open in H7; auto with hopi.
    forwards*: H2 x.
    forwards: IH H1 H12 H7; try solve [simpl; eauto with hopi].
      apply lexico2_2; omega.
    destruct H13 as [F'x [ C'1 [ P'x [Q'x [n3 [HltsF'x [HltsC'1 [Hp'x [Hq'x HhoweF'x]]]]]]]]].
    destruct F'x as [Pfx].
    assert (lts (nu bind (fun x0mapN (fun x1S x1) (f x0)) Q) (inp a)
        (abs_new (abs_def (close 0 x Pfx)))).
    apply (lts_new' L) with (abs_def (close 0 x Pfx)); auto.
    intros. rewrite bind_open in HltsF'x; auto.
    forwards: lts_open HltsF'x; eauto.
      rewrite <- bind_open; auto. apply× @is_proc_bind. intuition.
    destruct H15 as [A' [Ha' [HxA' HltsA']]]. specialize (HltsA' x0). simpl.
    inverts Ha'. destruct A' as [ |[Q''] |[] ]; inverts H16. simpl in HxA'.
    rewrite× @close_open. rewrite× subst_lab_id in HltsA'. simpl; autofs.
    assert ( n, howe' Rel (nu close 0 x P'x) (nu close 0 x Q'x) n).
      apply× @howe_implies_howe'.
      apply (howe_nu (L \u fn (close 0 x P'x) \u fn (close 0 x Q'x))).
      intros. eapply (howe_rename _ Hrename) with x; eauto;
          try solve [rewrite open_close; auto with howe].
      autofnF.
      rewrite open_close; auto with howe. rewrite open_close; auto with howe.
      apply howe'_implies_howe in HhoweF'x; auto.
    destruct H14.
     (abs_new (abs_def (close 0 x Pfx))) C'1
        (nu close 0 x P'x) (nu close 0 x Q'x) x0. splits; auto.
    assert (is_agent C1) by auto with howe hopi.
    assert (is_agent F1).
      forwards*: @lts_is_proc H5.
      apply (proc_nu L). intros. rewrite× <- @bind_open.
      apply× @is_proc_bind. forwards*: H2 x1. auto with howe.
    inverts Hp'x. apply sc0_def; auto with hopi.
      apply (proc_nu L); auto with hopi.
    destructA A; inverts H9.
    apply sc_trans with (nu appr (abs_def p) C1); auto with sc.
    apply sc_nu'. destruct C1 as [n P22 P23]. simpl in ×.
    asserts_rewrite (genNu n (subst ((shiftN n) p) P22 // P23)
          = close 0 x (genNu n (subst ((shiftN n)(open 0 x p)) P22 // P23))).
      rewrite close_genNu. simpl. fequals.
      rewrite close_subst. rewrite mapN_open; auto using shiftN_injective.
      replace (n+0) with n by omega. rewrite close_open; try solve [autofnF].
      repeat (rewrite× @close_id).
    apply× @sc_close. apply sc_symmetric.
    inverts H8. apply× (sc_newF_C (abs_def p)).
    assert (is_agent C'1) by auto with howe hopi.
    inverts Hq'x.
    apply sc0_def; auto with hopi.
      apply (proc_nu L); auto with hopi.
      apply× is_proc_app. forwards*: @lts_is_proc H13.
      apply (proc_nu L). intros. rewrite× <- @bind_open.
      apply× @is_proc_bind. forwards*: H2 x1. auto with howe.
    apply sc_trans with (nu appr (abs_def (close 0 x Pfx)) C'1); auto with sc.
    apply sc_nu'. destruct C'1 as [n P22 P23]. simpl in ×.
    asserts_rewrite (genNu n (subst ((shiftN n)(close 0 x Pfx)) P22 // P23)
          = close 0 x (genNu n (subst ((shiftN n) Pfx) P22 // P23))).
      rewrite close_genNu. simpl. fequals.
      rewrite close_subst. forwards*: lts_fn HltsC'1. simpl in H19.
      rewrite <- mapN_close. replace (n+0) with n by omega.
      repeat fequals; rewrite× @close_id.
      assert (fn P22 \c fn (bind g Q2)).
        apply subset_trans with (fn P22 \u fn P23); auto. autofs.
      autofnF.
      assert (fn P23 \c fn (bind g Q2)).
        apply subset_trans with (fn P22 \u fn P23); auto. autofs.
      autofnF.
    apply× @sc_close.
    apply sc_symmetric. apply× (sc_newF_C (abs_def (close 0 x Pfx))).
Qed.

Lemma pseudo_sim_sim : pseudo_sim.
Proof.
  intros. apply howe_implies_howe' in H3; auto.
  apply howe_implies_howe' in H4; auto. destruct H3, H4.
  forwards*: @pseudo_sim_sim' H2 H3; try eassumption. destruct_hyps.
  apply howe'_implies_howe in H13. do 4 eexists; intuition eassumption.
Qed.


Part common to all proofs

to adapt the proof according to the chosen path
Notation lpseudo_sim := pseudo_sim_in .

Lemma pseudo_tau {V:Set}: Rel (P Q:proc V) P'
  (f:V proc0), simulation Rel refl0 Rel rename_compatible Rel
  (Rincl sc0 Rel) trans Rel howe Rel P Q ( v, is_proc (f v))
  lts (bind f P) tau (ag_proc P')
   Q' P'' Q'', lts (bind f Q) tau (ag_proc Q')
                sc0 P' P'' sc0 Q' Q'' howe Rel P'' Q''.
Proof.
  introv Hsim Hrefl Hrename Hincl Htrans Hp1q1. gen f P'.
  induction Hp1q1; introv Hf HltsP1; try solve [inverts HltsP1].
  - forwards*: IHHp1q1 P'.
    destruct H1 as [R' [P'' [R'' [HltsR [Hp'p'' [Hr'r'' HhoweP1R]]]]]].
    forwards: H0 f; auto. destruct Hsim as [Hisproc Hsim]. forwards_test Rel.
     Q'0 P'' Q'0; intuition.
    apply howe_comp with R''; auto with hopi howe.
      apply oe_trans with R'; auto. apply oe_sc0; auto with sc. apply× oe_proc0.
  - P' P' P'; intuition.
  - inversion HltsP1; subst.
    + forwards: lts_tau_proc H2. destruct H as [P'1]. subst. simpl in H3.
      forwards: IHHp1q1_1 H2; auto.
      destruct H as [Q'1 [P''1 [Q''1 [HltsQ' [Hp'1p''1 [Hq'1q''1 Hhowe]]]]]].
      inverts Hp'1p''1. inverts Hq'1q''1.
       (Q'1 // (bind f Q')) (P''1 // (bind f P')) (Q''1 // (bind f Q')).
      inverts H3. splits; auto with sc howe hopi.
      eapply lts_parl'; eauto.
    + forwards: lts_tau_proc H2. destruct H as [P'1]. subst. simpl in H3.
      forwards: IHHp1q1_2 H2; auto.
      destruct H as [Q'1 [P''1 [Q''1 [HltsQ' [Hp'1p''1 [Hq'1q''1 Hhowe]]]]]].
      inverts Hp'1p''1. inverts Hq'1q''1.
       ((bind f Q) // Q'1) ((bind f P) // P''1) ((bind f Q) // Q''1).
      inverts H3. splits; auto with sc howe hopi.
      eapply lts_parr'; eauto.
    + forwards: lpseudo_sim H3 H2; eauto.
      destruct H as [F2 [C2 [P'2 [Q'2 [HltsQ' [HltsQ [Hp'2 [Hq'2 Hhowe]]]]]]]].
       (appl C2 F2) P'2 Q'2. inverts Hp'2. inverts Hq'2. splits; eauto.
      eapply lts_taul'; eauto.
      apply sc0_def; auto with howe hopi sc. apply sc_trans with (appr F C); auto with sc.
      apply sc_appr_appl.
      apply sc0_def; auto with howe hopi sc. apply sc_trans with (appr F2 C2); auto with sc.
      apply sc_appr_appl.
    + forwards: lpseudo_sim H2 H3; eauto.
      destruct H as [F2 [C2 [P'2 [Q'2 [HltsQ' [HltsQ [Hp'2 [Hq'2 Hhowe]]]]]]]].
       (appr F2 C2) P'2 Q'2. inverts Hp'2. inverts Hq'2. splits; eauto with sc.
      eapply lts_taur'; eauto.
  - inverts HltsP1. destruct A as [ P'1 | [] | [] ]; inverts H2.
    pick_fresh_fset_V V (fn P'1 \u
        fn (bind (fun x1mapN (fun x2S x2) (f x1)) Q)) x.
    forwards*: H4 x.
    assert ( y, is_proc (mapN (fun x0S x0) (f y))) by auto with hopi.
    rewrite× <- @bind_open in H1. forwards: H0 x H1; eauto.
    destruct H3 as [Q'1 [P''1 [Q''1 [HltsQ' [Hp'1p''1 [Hq'1q''1 Hhowe]]]]]].
    inverts Hp'1p''1. inverts Hq'1q''1.
     (nu (close 0 x Q'1)) (nu (close 0 x P''1)) (nu (close 0 x Q''1)).
    splits.
    apply (lts_new' L) with (ag_proc (close 0 x Q'1)); try solve [simpl; auto].
    fold @bind. intros. simpl. rewrite bind_open in HltsQ'; auto.
    forwards:lts_open HltsQ'; eauto.
      rewrite× <- @bind_open. apply× @is_proc_bind.
      forwards: H x; intuition.
    destruct H12 as [A' [Ha' [HxA' HltsAy]]]. specialize (HltsAy x0).
    destruct A' as [Q'' |[]|[]]; inverts Ha'. simpl in HltsAy.
    rewrite× @close_open.
    apply sc0_def; auto with howe hopi sc.
    apply (proc_nu L). intros. apply is_proc_rename with x; auto.
    apply (proc_nu L). intros. apply is_proc_rename with x; auto.
    rewrite× @open_close.
    apply sc_nu'.
    replace P'1 with (close 0 x (open 0 x P'1)) by (rewrite× @close_open).
    apply× @sc_close.
    apply sc0_def; auto with howe hopi sc.
    apply (proc_nu L). intros. apply is_proc_rename with x; auto.
    rewrite× @open_close.
    apply (proc_nu L). intros. apply is_proc_rename with x; auto.
    rewrite× @open_close.
    apply× @sc_nu'. apply× @sc_close.
    apply (howe_nu (L \u fn (close 0 x P''1) \u fn (close 0 x Q''1))). intros.
    assert (0 \notin bn P''1).
      apply is_proc_bn in H5. rewrite× H5.
    assert (0 \notin bn Q''1).
      apply is_proc_bn in H8. rewrite× H8.
    rewrite× <- (open_close_gen P''1 0 x) in Hhowe.
    rewrite× <- (open_close_gen Q''1 0 x) in Hhowe.
    forwards: @howe_rename Hhowe x0; eauto.
      autofnF.
      rewrite× @open_close_gen.
      rewrite× @open_close_gen.
Qed.

Lemma conc_to_proc : (C:conc) a, conc_wf C is_agent C
     P, is_proc P lts P (out a) C
        ( (C':conc), lts P (out a) C' C = C').
Proof.
  intros. destruct C as [n P1 P2]. gen P1 P2. induction n; intros.
  + (a!(P1) P2); intuition; auto with hopi. simpl in H0.
    assert (bn P1 = \{}). autofs. forwards*: H0 x; autofs. omega.
    assert (bn P2 = \{}). autofs. forwards*: H0 x; autofs. omega.
    apply proc_out; apply× @is_proc_bn_rev.
    inverts× H1.
  + pick_fresh x. forwards*: IHn (open n x P1) (open n x P2).
    intros. rewrite bn_open. forwards*: H k. autofs. omega.
    intros. forwards*: H0 k. autobnF. autobnF; omega.
    destruct H1 as [P []]. forwards*: @decomp_proc P 0 x.
    destruct H3 as [P' [H13 [H12 H22]]]. subst.
     (nu P'). splits.
    - apply (proc_nu (fn P')). intros. unfold open. eapply is_proc_rename; eauto.
    - apply (lts_new' (fn P' \u fn P1 \u fn P2 \u \{ a})) with
        (conc_def n P1 P2). intros.
      simpl. forwards*: lts_open H2.
      destruct H5 as [A' [Ha' [HxA' HltsA']]].
      destruct A' as [ |[]|[]]; inverts Ha'.
      simpl in HxA'. forwards*: @open_injective H7. forwards*: @open_injective H8.
      subst. specialize (HltsA' x0). rewrite subst_lab_id in HltsA'; try simpl; auto.
      simpl. assert (n \in bn P1). forwards*: H n. case_if×.
    - intros. inverts H3. pick_fresh y. forwards*: H7 y.
      forwards*: lts_out_conc H3. destruct H4 as [[]].
      forwards× HltsA': lts_rename H3 x.
      destruct A as [ |[]|[]]; inverts H4.
      destruct H2. rewrite subst_lab_id in HltsA'; try solve [simpl; autofs].
      simpl in HltsA'. forwards*: H4 HltsA'. inverts H6.
      assert (x \notin (fn p1 \u fn p2)).
        forwards*: lts_fn H3. simpl in H6. forwards: @fn_open_sub P' 0 y.
        forwards*: @subset_trans H6 H8. clear H6 H8.
        forwards: @fn_open_rev p1 n0 y. forwards: @fn_open_rev p2 n0 y.
        assert (fn p1 \u fn p2 \c fn P' \u \{ y}).
          apply subset_trans with (fn (open n0 y p1) \u fn(open n0 y p2)); autofs.
        clear H8 H6 H9. intros_all. apply H13 in H6. autofs.
      forwards*: @open_injective H10. forwards*: @open_injective H11. subst.
      inverts H5. assert (n0 \in bn p1). apply H. omega. case_if×.
Qed.

Lemma abs_to_proc : (F:abs) a, is_agent F
     P, is_proc P lts P (inp a) F
        ( (F':abs), lts P (inp a) F' F = F').
Proof.
  intros. destruct F as [P]. (a? P); splits*; auto with hopi.
  intros. inverts× H0.
Qed.

Lemma simulation_up_to_sc_howe : Rel, simulation Rel refl0 Rel rename_compatible Rel
  (Rincl sc0 Rel) trans Rel simulation_up_to_sc (howe Rel).
Proof.
  intros. split.
    intros_all. auto with howe.
  intros. splits; intros.
  + replace P with (bind (pr_var (V:=Empty_set)) P) in H4 by (rewrite× bind_proc0).
    forwards: @pseudo_tau H3; eauto with hopi.
    destruct H5 as [Q' [P'' [Q'' [HltsQ' [Hpp'' [Hq'q'' Hhowe]]]]]].
    replace (bind (pr_var (V:=Empty_set)) Q) with Q in HltsQ' by (rewrite× bind_proc0).
     Q'. split×. do 2 (eexists; intuition eauto with sc).
  + replace P with (bind (pr_var (V:=Empty_set)) P) in H4 by (rewrite× bind_proc0).
    forwards*: conc_to_proc C a. destruct H7 as [R [Hr [Hlts Hc']]].
    assert (howe Rel R R) by apply× @howe_refl.
    replace R with (bind (pr_var (V:=Empty_set)) R) in Hlts by (rewrite× bind_proc0).
    forwards: lpseudo_sim H7 H3; eauto with hopi.
    destruct H8 as [F2 [C2 [P'2 [Q'2 [HltsQ [HltsR [Hpp'' [Hq'q'' Hhowe]]]]]]]].
    replace (bind (pr_var (V:=Empty_set)) Q) with Q in HltsQ by (rewrite× bind_proc0).
    replace (bind (pr_var (V:=Empty_set)) R) with R in HltsR by (rewrite× bind_proc0).
    forwards*: Hc' HltsR. subst. do 3 (eexists; intuition eauto with sc).
  + replace P with (bind (pr_var (V:=Empty_set)) P) in H4 by (rewrite× bind_proc0).
    forwards*: abs_to_proc F a. destruct H6 as [R [Hr [Hlts Hf']]].
    assert (howe Rel R R) by apply× @howe_refl.
    replace R with (bind (pr_var (V:=Empty_set)) R) in Hlts by (rewrite× bind_proc0).
    forwards: lpseudo_sim H3 H6; eauto with hopi.
    destruct H7 as [F2 [C2 [P'2 [Q'2 [HltsR [HltsQ [Hpp'' [Hq'q'' Hhowe]]]]]]]].
    replace (bind (pr_var (V:=Empty_set)) Q) with Q in HltsQ by (rewrite× bind_proc0).
    replace (bind (pr_var (V:=Empty_set)) R) with R in HltsR by (rewrite× bind_proc0).
    forwards*: Hf' HltsR. subst. do 3 (eexists; intuition eauto with sc).
Qed.

Lemma Rincl_sc0_howe : Rel, (Rincl sc0 Rel) Rincl sc0 (howe Rel).
Proof.
  intros_all. apply howe_comp with x; auto with sc howe.
  apply× oe_proc0.
Qed.

Lemma bisimulation_tclos_howe : Rel, simulation Rel refl0 Rel
    rename_compatible Rel (Rincl sc0 Rel) trans Rel sym Rel
    bisimulation (tclosure (howe Rel)).
Proof.
  intros. rename H3 into Hsym. apply sim_sym_imply_bisim.
  ×
    split.
      intros_all. induction H3; intuition auto with howe.
    intros. assert (Rincl sc0 (tclosure (howe Rel))).
      intros_all. apply× tclosure_once. apply× Rincl_sc0_howe.
    induction H3.
    + forwards*: simulation_up_to_sc_howe Rel.
      destruct H5. specialize (H6 x y H3).
      splits; intros; forwards_test (sc0° (howe Rel) ° sc0); destruct_comp;
      repeat (eexists; intuition (try eassumption)); intuition;
      repeat (match goal with
        | H1: Rincl sc0 (tclosure (howe Rel)),
          H2: sc0 _ _ |- _apply H1 in H2 end); eauto with howe.
    + splits; intros; forwards_test (tclosure (@howe Empty_set Rel)); clear H3_;
      forwards_test (tclosure (@howe Empty_set Rel)); destruct_comp;
        repeat (eexists; intuition (try eassumption)); intuition eauto with howe.
 × apply× @howe_sym.
Qed.

Theorem bisimilarity_howe : bisimilarity = howe bisimilarity.
Proof.
  apply binary_ext; split.
  - intros. assert (Hbisim:=H). unfold bisimilarity in H. destruct H. destruct H.
    apply howe_comp with x; auto with bisim. apply howe_refl; auto with bisim.
    apply× oe_proc0.
  - intros. (tclosure (@howe Empty_set bisimilarity)).
    split. apply bisimulation_tclos_howe; auto using bisim_sym, bisim_trans, bisim_refl,
      bisim_rename_compatible.
      forwards*: bisim_is_bisimulation; intuition.
      intros_all. sc0. intuition. apply struct_congr_bisim.
      apply× tclosure_once.
Qed.