Require Export Howe.

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 → refl Rel → rename_compatible Rel → (Rincl sc0 Rel) → trans Rel
   → howe Rel P2 Q2 → howe Rel P1 Q1
   → ltsabs (bind f P1) a F1 → ltsconc (bind g P2) a C1
   → ∃ F2 C2 P'2 Q'2, ltsabs (bind f Q1) a F2 ∧
                            ltsconc (bind g Q2) a C2 ∧
                            sc0 P'2 (appr F1 C1) ∧
                            sc0 Q'2 (appr F2 C2) ∧
                            howe Rel P'2 Q'2).

Lemma pseudo_inp_first {V:Set}:
  ∀ Rel (P1 Q1:proc V)(P2 Q2:proc0) a F1 (f:V → proc0),
    simulation Rel → refl Rel → rename_compatible Rel
  → (∀ P Q, Rel (P // PO) (Q // PO) → Rel P Q)
  → howe Rel P1 Q1 → howe Rel P2 Q2
  → ltsabs (bind f P1) a F1
  → ∃ F2, ltsabs (bind f Q1) a F2 ∧
                howe Rel (subst F1 P2) (subst F2 Q2).
Proof.
  introv Hsim Hrefl Hrename HpO Hp1q1. gen a f F1 P2 Q2.
  induction Hp1q1; introv Hp2q2 HltsP1; try solve [inverts HltsP1].
  - forwards*: IHHp1q1 Hp2q2 HltsP1. destruct H0 as [F2 [Hltsf2 Hhowe]].
    forwards*: H f. remember (conc_def Q2 PO) as C.
    assert (Hwf:conc_wf C). subst.
      unfold conc_wf. repeat constructor×.
    unfold simulation in Hsim. forwards_test Rel.
    subst. simpl in H5. apply HpO in H5.
    ∃ F'0; intuition.
    apply howe_comp with (subst F2 Q2); eauto with howe hopi.
      apply× oe_proc0.
  - simpl in ×. ∃ F1; intuition.
  - inverts HltsP1.
    + forwards*: IHHp1q1_1 Hp2q2 H3. destruct H as [F'2 [Hltsf'2 Hhowe]].
      ∃ (abs_parl F'2 (bind f Q')). split; simpl; eauto with hopi howe.
    + forwards*: IHHp1q1_2 Hp2q2 H3. destruct H as [F'2 [Hltsf'2 Hhowe]].
      ∃ (abs_parr (bind f Q) F'2 ). split; simpl; eauto with hopi howe.
  - inverts HltsP1. ∃ (bind (liftV f) Q). split; simpl; auto with hopi howe.
  - simpl in ×. inverts HltsP1.
    fresh_lp (a::L++L0) ((nu (fun x ⇒ bind f (P x))) // (a ? (nu F)) //
      (nu (fun x ⇒ bind f (Q x))) // P2 // Q2).
    forwards*: H2 x.
    forwards*: H0 x; auto with hopi.
    destruct H11 as [F2' [ HltsF2' Hrel ]]. exp x F2'. rename F2'0 into F2'.
    ∃ (nu F2'). split.
    apply ltsa_new with L0; intros; auto with hopi.
    assert (subst_name x b a a) by constructor×.
    forwards*: ltsabs_rename (fun b ⇒ bind f (Q b)) F2' x b.
    apply howe_nu with L; intros; fold @bind in ×.
    forwards*: @howe_rename (fun x⇒ subst (F x) P2)
          (fun x ⇒ (subst (F2' x) Q2)) x a0; auto with hopi;
      intros_all; apply× @notin_bind;
      intros [|]; simpl; auto with hopi.
Qed.

Lemma pseudo_inp_conc {V:Set}: ∀ Rel (P1 Q1:proc V) a F1 C (f:V → proc0),
    simulation Rel → refl Rel → rename_compatible Rel
  → (∀ P Q, Rel (P // PO) (Q // PO) → Rel P Q)
  → howe Rel P1 Q1
  → ltsabs (bind f P1) a F1
  → ∃ F2, ltsabs (bind f Q1) a F2 ∧ howe Rel (appr F1 C) (appr F2 C).
Proof.
  intros. induction C; simpl.
  forwards: @pseudo_inp_first p p H2 H3; auto with hopi howe.
  destruct H4 as [F2 []]. ∃ F2; split; auto with hopi howe.
  fresh_pc ((nu (fun x ⇒ appr F1 (c x)))// bind f Q1) (conc_nu c).
  forwards*: H4 x. destruct H5 as [F2 []]. ∃ F2; split; auto with hopi howe.
  apply howe_nu with (@nil name); intros.
  forwards*: @howe_rename (fun x ⇒ appr F1 (c x))
    (fun x ⇒ appr F2 (c x)) x a0.
    intros_all. solve_notin'. eapply ltsabs_notin; eauto.
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. eauto with sc.
  gen a f g F1 C1 P1 Q1.
  induction Hp2q2; introv Hp1q1 HltsP1 HltsP2; try solve [inverts HltsP2].
  - forwards*: IHHp2q2 a F1 C1 P1 Q1.
    destruct H0 as [F2 [C2 [ P'2 [R' [HltsQ1 [ HltsR [Hp'2 [Hr' HhoweP1R]]]]]]]].
    forwards*: H g. unfold simulation in ×.
    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*: IHHp2q2_1 Hp1q1 HltsP1 H3.
      destruct H as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
      ∃ F'2 (conc_parl C'2 (bind g Q')) (P'2// bind g P') (Q'2//bind g Q').
      splits; simpl; eauto with hopi howe sc.
    + forwards*: IHHp2q2_2 Hp1q1 HltsP1 H3.
      destruct H as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
      ∃ F'2 (conc_parr (bind g Q) C'2) (bind g P // P'2) (bind g Q // Q'2).
      splits; simpl; eauto with hopi howe sc.
  - inverts HltsP2. simpl.
    forwards*: @pseudo_inp_first Rel P1 Q1 (bind g P)(bind g Q).
      apply @howe_bind; auto with howe.
    destruct H as [F2 [HltsQ1 HhoweF1F2]].
    ∃ F2 (conc_def (bind g Q) (bind g Q'))
        (appr F1 (conc_def (bind g P) (bind g P')))
        (appr F2 (conc_def (bind g Q) (bind g Q'))); intuition auto with hopi howe;
      simpl; auto with sc hopi howe.
  - simpl in ×. inverts HltsP2.
    fresh_lpc (L0++L) ((nu (fun x ⇒ bind g (P x))) // (a ? F1) // bind f Q1 //
      nu (fun x ⇒ bind g (Q x))) (conc_nu C).
    forwards*: H2 x.
    forwards*: H0 x; auto with hopi.
    destruct H6 as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
    conc_exp x C'2. destruct (exists_cnew C'0) as [C'2].
    exp x P'2. exp x Q'2.
    ∃ F'2 C'2 (nu P'0) (nu Q'0); splits; auto.
    apply ltsc_new with C'0 L0; auto; intros.
    assert (subst_name x b a a) by constructor×.
    forwards*: ltsconc_rename (fun b ⇒ bind g (Q b)) C'0 x b.
    apply sc_trans with (nu (fun x ⇒ appr F1 (C x))); auto with sc.
    apply sc_nu with L; intros.
    change (sc0 (P'0 a0) ((fun a0 ⇒ appr F1 (C a0)) a0)).
    eapply sc_rename; eauto with hopi.
    apply sc_trans with (nu (fun x ⇒ appr F'2 (C'0 x))); auto with sc.
    apply sc_nu with L; intros.
    change (sc0 (Q'0 a0) ((fun a0 ⇒ appr F'2 (C'0 a0)) a0)).
    eapply sc_rename; eauto with hopi.
    intros_all. solve_notin'. eapply ltsabs_notin; eauto.
    apply howe_nu with L; intros.
    forwards*: @howe_rename P'0 Q'0 x a0.
Qed.

Lemma pseudo_out_first {V:Set}: ∀ Rel (P1 Q1:proc V)(P2 Q2:proc1) a C1
  (f:V → proc0), simulation Rel → refl Rel →
  rename_compatible Rel → (Rincl sc0 Rel) → trans Rel →
  howe Rel P1 Q1 → howe Rel P2 Q2 →
  ltsconc (bind f P1) a C1 →
  ∃ C2 P'2 Q'2, ltsconc (bind f Q1) a C2 ∧
     sc0 P'2 (appr P2 C1) ∧
     sc0 Q'2 (appr 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 HltsP1; try solve [inverts HltsP1].
  - forwards*: IHHp1q1 Hp2q2 HltsP1.
    destruct H0 as [C2 [P'2 [Q'2 [Hltsc2 [Hp'2 [Hq'2 Hhowe]]]]]].
    forwards: H f; auto. unfold simulation in ×.
    forwards_test Rel.
    ∃ C'0 P'2 (appr Q2 C'0); intuition.
    apply howe_comp with Q'2; auto with hopi howe.
      apply oe_trans with (appr Q2 C2); auto.
      apply× oe_sc0. apply× oe_proc0.
  - simpl in ×.
    ∃ C1 (appr P2 C1)(appr Q2 C1); intuition auto with howe sc.
    ind_conc; simpl; eauto with howe.
  - inverts HltsP1.
    + forwards*: IHHp1q1_1 Hp2q2 H3.
      destruct H as [ C'2 [P'2 [Q'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]].
      ∃ (conc_parl C'2 (bind f Q')) (P'2// bind f P') (Q'2//bind f Q').
      splits; simpl; eauto with hopi howe sc.
    + forwards*: IHHp1q1_2 Hp2q2 H3.
      destruct H as [ C'2 [P'2 [Q'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]].
      ∃ (conc_parr (bind f Q) C'2) (bind f P // P'2) (bind f Q // Q'2).
      splits; simpl; eauto with hopi howe sc.
  - inverts HltsP1. simpl.
    ∃ (conc_def (bind f Q) (bind f Q'))
        (appr P2 (conc_def (bind f P) (bind f P')))
        (appr Q2 (conc_def (bind f Q) (bind f Q')));
    simpl; intuition auto with hopi sc howe.
  - simpl in ×. inverts HltsP1.
    fresh_lpc (L0++L) ((nu (fun x ⇒ bind f (P x))) // (a ? P2) // (a ? Q2) //
      nu (fun x ⇒ bind f (Q x))) (conc_nu C).
    forwards*: H2 x.
    forwards*: H0 x; auto with hopi.
    destruct H6 as [C2' [P'2 [Q'2 [HltsC2' [Hp'2 [HQ'2 Hrel]]]]]].
    conc_exp x C2'. destruct (exists_cnew C2'0) as [C'2].
    exp x P'2. exp x Q'2.
    ∃ C'2 (nu P'0) (nu Q'0); splits; auto.
    apply ltsc_new with C2'0 L0; auto; intros.
    assert (subst_name x b a a) by constructor×.
    forwards*: ltsconc_rename (fun b ⇒ bind f (Q b)) C2'0 x b.
    apply sc_trans with (nu (fun x ⇒ appr P2 (C x))); auto with sc.
    apply sc_nu with L; intros.
    change (sc0 (P'0 a0) ((fun a0 ⇒ appr P2 (C a0)) a0)).
    eapply sc_rename; eauto with hopi.
    apply sc_trans with (nu (fun x ⇒ appr Q2 (C2'0 x))); auto with sc.
    apply sc_nu with L; intros.
    change (sc0 (Q'0 a0) ((fun a0 ⇒ appr Q2 (C2'0 a0)) a0)).
    eapply sc_rename; eauto with hopi.
    apply howe_nu with L; intros.
    forwards*: @howe_rename P'0 Q'0 x a0.
    Unshelve. exact (@nil name).
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 HltsP1 HltsP2; try solve [inverts HltsP1].
  - forwards*: IHHp1q1 a F1 C1 P2 Q2.
    destruct H0 as [F2 [C2 [ P'2 [R' [HltsQ1 [ HltsR [Hp'2 [Hr' HhoweP1R]]]]]]]].
    forwards*: H f. unfold simulation in ×.
    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 ×.
    forwards: @pseudo_out_first P2 Q2 F1 F1 C1; eauto with howe hopi.
    destruct H as [C2 [ P'2 [Q'2 [HltsC2 [Hp'2 [Hq'2 Hhowe]]]]]].
    ∃ F1 C2 P'2 Q'2; intuition.
  - inverts HltsP1.
    + forwards*: IHHp1q1_1 Hp2q2 H3 HltsP2.
      destruct H as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
      ∃ (abs_parl F'2 (bind f Q')) C'2 (P'2// bind f P') (Q'2//bind f Q').
      splits; simpl; eauto with hopi howe sc.
    + forwards*: IHHp1q1_2 Hp2q2 H3 HltsP2.
      destruct H as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
      ∃ (abs_parr (bind f Q) F'2) C'2 (bind f P // P'2) (bind f Q // Q'2).
      splits; simpl; eauto with hopi howe sc.
  - 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.
    destruct H as [ C'2 [P'2 [Q'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]].
    ∃ (bind (liftV f) Q) C'2 P'2 Q'2; intuition.
  - simpl in ×. inverts HltsP1.
    fresh_lpc (L0++L) ((nu (fun x ⇒ bind f (P x))) // (a ? (nu F)) // bind g Q2 //
      nu (fun x ⇒ bind f (Q x))) C1.
    forwards*: H2 x.
    forwards*: H0 x; auto with hopi.
    destruct H8 as [F'2 [ C'2 [P'2 [Q'2 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]].
    exp x F'2. exp x P'2. exp x Q'2.
    ∃ (nu F'0) C'2 (nu P'0)(nu Q'0); splits; auto.
    apply ltsa_new with L0; intros; auto with hopi.
    assert (subst_name x b a a) by constructor×.
    forwards*: ltsabs_rename (fun b ⇒ bind f (Q b)) F'0 x b.
    apply sc_trans with (nu (fun x ⇒ appr (F x) C1)); auto with sc.
    apply sc_nu with L; intros.
    change (sc0 (P'0 a0) ((fun a0 ⇒ appr (F a0) C1) a0)).
    eapply sc_rename; eauto with hopi.
    apply sc_trans with (nu (fun x ⇒ appr (F'0 x) C'2)); auto with sc.
    apply sc_nu with L; intros.
    change (sc0 (Q'0 a0) ((fun a0 ⇒ appr (F'0 a0) C'2) a0)).
    eapply sc_rename; eauto with hopi.
    intros_all. solve_notin'. eapply ltsconc_notin; eauto with hopi.
    apply howe_nu with L; intros.
    forwards*: @howe_rename P'0 Q'0 x a0.
Qed.

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 → refl Rel → rename_compatible Rel → (Rincl sc0 Rel) → trans Rel
   → howe' Rel P2 Q2 n2 → howe' Rel P1 Q1 n1
   → ltsabs (bind f P1) a F1 → ltsconc (bind g P2) a C1
   → ∃ F2 C2 P'2 Q'2 n3, ltsabs (bind f Q1) a F2 ∧
                               ltsconc (bind g Q2) a 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 Peano.lt Peano.lt)).
    apply wf_lexico2; auto with wf.
  remember (n2, n1) as p. gen V W.
  gen n1 n2 a F1 C1.
  induction_wf IH: H p. intros n1 n2 Hp. subst.
  assert (∀ (V2 : Set) a (P1 Q1 : proc1) (n1 : nat) (P2 Q2 : proc V2),
     howe' Rel P1 Q1 n1
     → howe' Rel P2 Q2 n2
         → ∀ (g : V2 → proc0) (C1 : conc),
              ltsconc (bind g P2) a C1
                 → ∃ (C2:conc) P'2 Q'2 x3,
                     ltsconc (bind g Q2) a C2
                   ∧ sc0 P'2 (appr P1 C1)
                   ∧ sc0 Q'2 (appr 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 H2].
    - forwards*: IH (k, S n0) f; try solve [subst; simpl; eauto with hopi].
      destruct_hyps. specialize (H5 g). unfold simulation in ×.
      forwards_test Rel. inverts H6. rewrite H4 in ×.
      ∃ C'0 x1 (appr Q1 C'0)(S x3); intuition.
        apply howe_comp' with x2; auto with hopi howe.
        apply oe_trans with (appr Q1 x0); auto.
        apply× oe_sc0. apply× oe_proc0.
    - simpl in ×.
      assert (∃ n3, howe' Rel (appr P1 C1) (appr Q1 C1) n3).
        apply× @howe_implies_howe'. apply howe'_implies_howe in H0.
        ind_conc; simpl; eauto with howe.
      destruct H1. ∃ C1 (appr P1 C1)(appr Q1 C1) x0;
      intuition auto with sc.
  - inverts H2.
    + forwards*: IH f H3 H8; try solve [subst; simpl; eauto with hopi].
        apply lexico2_1. nat_math.
      destruct H1 as [ F2 [ C'2 [P'2 [Q'2 [ n3 [ HltsF2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]]].
      inverts HltsF2. rewrite H4 in ×.
      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. auto with howe.
      destruct H2. ∃ (conc_parl C'2 (bind g Q')) (P'2// bind g P') (Q'2//bind g Q') x.
      splits; simpl; eauto with hopi howe sc.
    + forwards*: IH f H1_0 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 HltsF2. rewrite H4 in ×.
      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. auto with howe.
      destruct H2. ∃ (conc_parr (bind g Q) C'2) (bind g P // P'2) (bind g Q // Q'2) x.
      splits; simpl; eauto with hopi howe sc.
  - inverts H2. simpl.
    assert (∃ n, howe' Rel (appr P1 (conc_def (bind g P) (bind g P')))
        (appr Q1 (conc_def (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.
      auto with howe.
    destruct H1. ∃ (conc_def (bind g Q) (bind g Q'))
        (appr P1 (conc_def (bind g P) (bind g P')))
        (appr Q1 (conc_def (bind g Q) (bind g Q'))) x;
    intuition auto with hopi sc.
  - simpl in ×. inverts H2.
    fresh_lpc (L0++L) ((nu (fun x ⇒ bind g (P x))) // (a ? P1) // (a ? Q1) //
      nu (fun x ⇒ bind g (Q x))) (conc_nu C).
    forwards*: H6 x.
    forwards*: H1 x; auto with hopi.
    forwards*: IH H9 H3; auto with hopi.
      apply lexico2_1. nat_math.
      rewrite bind_return'. apply ltsa_inp.
    destruct H14 as [F2 [C2' [P'2 [Q'2 [n3 [HltsF2 [HltsC2' [Hp'2 [HQ'2 Hrel]]]]]]]]].
    conc_exp x C2'. destruct (exists_cnew C2'0) as [C'2].
    exp x P'2. exp x Q'2. rewrite bind_return' in HltsF2. inverts HltsF2.
    ∃ C'2 (nu P'0) (nu Q'0) (S n3); splits; auto.
    apply ltsc_new with C2'0 L0; auto; intros.
    assert (subst_name x b a a) by constructor×.
    forwards*: ltsconc_rename (fun b ⇒ bind g (Q b)) C2'0 x b.
    apply sc_trans with (nu (fun x ⇒ appr P1 (C x))); auto with sc.
    apply sc_nu with L; intros.
    change (sc0 (P'0 a0) ((fun a0 ⇒ appr P1 (C a0)) a0)).
    eapply sc_rename; eauto with hopi.
    apply sc_trans with (nu (fun x ⇒ appr F2 (C2'0 x))); auto with sc.
    apply sc_nu with L; intros.
    change (sc0 (Q'0 a0) ((fun a0 ⇒ appr F2 (C2'0 a0)) a0)).
    eapply sc_rename; eauto with hopi.
    apply howe_nu' with L; intros.
    forwards*: @howe'_rename P'0 Q'0 x a0.
    }
  intros. destruct H2; try solve [inverts H3].
  + forwards*: IH H1 H3; try solve [simpl; eauto with hopi].
    destruct H6 as [F2 [C2 [ P'2 [R' [n3 [HltsQ1 [ HltsR [Hp'2 [Hr' HhoweP1R]]]]]]]]].
    forwards*: H5 f. unfold simulation in ×. 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 H13. ∃ F'0 C2 P'2 (appr F'0 C2) x; intuition.
  + simpl in ×. assert (∃ n1, howe' Rel F1 F1 n1).
      apply howe_implies_howe'; auto with howe hopi.
    destruct H2. forwards*: H0 H2 H1 H4. destruct_hyps.
    do 5 eexists; intuition (try eassumption).
  + inverts H3.
    - 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]]]]]]]]].
      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 H2. ∃ (abs_parl F'2 (bind f Q')) C'2 (P'2// bind f P') (Q'2//bind f Q') x.
      splits; simpl; eauto with hopi sc howe.
    - 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]]]]]]]]].
      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 H2. ∃ (abs_parr (bind f Q) F'2) C'2 (bind f P // P'2) (bind f Q // Q'2) x.
      splits; simpl; eauto with hopi howe sc.
  + inverts H3. assert (∃ n1, howe' Rel (bind (liftV f) P)(bind (liftV f) Q) n1).
      apply× @howe_implies_howe'. apply× @howe_bind. apply× @howe'_implies_howe.
      intros [|]; simpl; auto with howe.
    destruct H3. forwards*: H0 H3 H1. destruct_hyps.
    do 5 eexists; intuition (try eassumption).
    simpl. auto with hopi.
  + simpl in ×. inverts H3.
    fresh_lpc (L0++L) ((nu (fun x ⇒ bind f (P x))) // (a ? (nu F)) // bind g Q2 //
      nu (fun x ⇒ bind f (Q x))) C1.
    forwards*: H6 x.
    forwards*: H2 x; auto with hopi.
    forwards*: IH H1 H11 H5 ; auto with hopi.
      apply lexico2_2; nat_math.
    destruct H15 as [F'2 [ C'2 [P'2 [Q'2 [n3 [HltsF'2 [ HltsC'2 [Hp'2 [Hq'2 Hhowe]]]]]]]]].
    exp x F'2. exp x P'2. exp x Q'2.
    ∃ (nu F'0) C'2 (nu P'0)(nu Q'0)(S n3); splits; auto.
    apply ltsa_new with L0; intros; auto with hopi.
    assert (subst_name x b a a) by constructor×.
    forwards*: ltsabs_rename (fun b ⇒ bind f (Q b)) F'0 x b.
    apply sc_trans with (nu (fun x ⇒ appr (F x) C1)); auto with sc.
    apply sc_nu with L; intros.
    change (sc0 (P'0 a0) ((fun a0 ⇒ appr (F a0) C1) a0)).
    eapply sc_rename; eauto with hopi.
    apply sc_trans with (nu (fun x ⇒ appr (F'0 x) C'2)); auto with sc.
    apply sc_nu with L; intros.
    change (sc0 (Q'0 a0) ((fun a0 ⇒ appr (F'0 a0) C'2) a0)).
    eapply sc_rename; eauto with hopi.
    intros_all. solve_notin'. eapply ltsconc_notin; eauto with hopi.
    apply howe_nu' with L; intros.
    forwards*: @howe'_rename P'0 Q'0 x a0.
    Unshelve. exact (@nil name).
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 H11. do 4 eexists; intuition eassumption.
Qed.

Notation lpseudo_sim := pseudo_sim_in .

Lemma pseudo_tau {V:Set}: ∀ Rel (P Q:proc V) P'
  (f:V → proc0), simulation Rel → refl Rel → rename_compatible Rel →
  (Rincl sc0 Rel) → trans Rel → howe Rel P Q →
  ltsproc (bind f P) P' →
  ∃ Q' P'' Q'', ltsproc (bind f Q) 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 HltsP1; try solve [inverts HltsP1].
  - forwards*: IHHp1q1 P'.
    destruct H0 as [R' [P'' [R'' [HltsR [Hp'p'' [Hr'r'' HhoweP1R]]]]]].
    forwards: H f; auto. unfold simulation in ×. 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.
  - inverts HltsP1.
    + forwards: IHHp1q1_1 H2; auto.
      destruct H as [Q'1 [P''1 [Q''1 [HltsQ' [Hp'1p''1 [Hq'1q''1 Hhowe]]]]]].
      ∃ (Q'1 // (bind f Q')) (P''1 // (bind f P')) (Q''1 // (bind f Q')).
      splits; simpl; auto with sc howe hopi.
    + forwards: IHHp1q1_2 H2; auto.
      destruct H as [Q'1 [P''1 [Q''1 [HltsQ' [Hp'1p''1 [Hq'1q''1 Hhowe]]]]]].
      ∃ ((bind f Q) // Q'1) ((bind f P) // P''1) ((bind f Q) // Q''1).
      splits; simpl; auto with sc howe hopi.
    + forwards: lpseudo_sim H3 H1; eauto.
      destruct H as [F2 [C2 [P'2 [Q'2 [HltsQ' [HltsQ [Hp'2 [Hq'2 Hhowe]]]]]]]].
      ∃ (appl C2 F2) P'2 Q'2. splits; eauto with sc.
      eapply lts_taul'; eauto.
    + forwards: lpseudo_sim H1 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. splits; eauto with sc.
      eapply lts_taur'; eauto.
  - inverts HltsP1.
    fresh_lp (L0++L) ((nu (fun x ⇒ bind f (Q x))) //
      (nu (fun x ⇒ bind f (P x))) // nu P'0).
    forwards*: H2 x.
    forwards*: H0 x; auto with hopi.
    destruct H8 as [Q'1 [P''1 [Q''1 [HltsQ' [Hp'1p''1 [Hq'1q''1 Hhowe]]]]]].
    all_exp x.
    ∃ (nu Q'0) (nu P''0) (nu Q''0); splits; eauto.
    apply ltsp_new with L; intros.
    forwards*: ltsproc_rename (fun b ⇒ bind f (Q b)) Q'0 x a.
    apply sc_nu with L; intros.
    eapply sc_rename; eauto with hopi.
    apply sc_nu with L; intros.
    eapply sc_rename; eauto with hopi.
    apply howe_nu with L; intros.
    forwards*: @howe_rename P''0 Q''0 x a.
Qed.



Inductive pull: conc → (name → conc) → Prop :=
| pull_nudef : ∀ P Q, pull (conc_nu (fun x ⇒ conc_def (P x)(Q x)))
      (fun x ⇒ conc_def (P x)(Q x))
| pull_nunu : ∀ C C' L, (∀ a, ¬In a L →
    conc_notin_ho a (fun x ⇒ conc_nu (C x)) →
    conc_notin_ho a (fun x ⇒ conc_nu (C' x)) →
    pull (conc_nu (C a))(C' a)) →
    pull (conc_nu (fun x ⇒ conc_nu (C x)))
         (fun y ⇒ conc_nu (fun x ⇒ C' x y)).


Lemma pull_conc_new : ∀ C, conc_wf (conc_nu C) →
             ∀ C', pull (conc_nu C) C' →
             conc_new C' (conc_nu C).
Proof.
  intros. gen C'. induction H; intros.
  + inverts H0.
  + inverts H1.
    × fresh_lpc (L'++L)((nu P) // nu Q) (conc_nu C). forwards*: H x.
        auto with hopi.
      inverts H2. constructor. inverts H9.
      intros. apply isin_arg with x; eauto.
    × fn(conc_nu (fun x ⇒ conc_nu (C1 x))). fn(conc_nu(fun x ⇒ conc_nu (C'0 x))).
      apply cnew_nu with (L++L'++L0++L1++L2); intros.
      simpl_notin. forwards*: H1. forwards*: H2. simpl_notin.
Qed.

Lemma pull_size : ∀ n C, sizec C (S n) →
    ∀ C', pull C C' → ∀ a, sizec (C' a) n.
Proof.
  intros. gen n. induction H0; auto; intros.
  inverts× H. inverts H1.
  fn(conc_nu (fun x⇒conc_nu (fun y ⇒ C' x y))).
  fresh_lc (a::L++L0)(conc_nu (fun x ⇒ conc_nu (C x))).
  forwards*: H1. simpl_notin.
  destruct n. forwards*: H4 x. inverts H3.
  forwards*: H x. forwards*: H0. constructor; intros.
  change (sizec ((fun a0 ⇒ C' a0 a) a0) n).
  eapply sizec_rename; eauto. auto with hopi.
Qed.

Lemma pull_rename : ∀ C C' a, conc_notin_ho a C →
  conc_notin_ho a (fun x ⇒ conc_nu (C' x)) → pull (C a)(C' a) →
  ∀ b, pull (C b)(C' b).
Proof.
  intros. remember (C a) as Ca. remember (C' a) as C'a.
  gen a b C C'. induction H1; intros.
  + ho_exp a P. ho_exp a Q. conc_change_ext.
    assert (conc_nu (fun x ⇒ conc_def (P0 a x)(Q0 a x)) = conc_nu (C' a)).
     rewrite HeqC'a. auto.
    change ((fun a ⇒ conc_nu (fun x ⇒ conc_def (P0 a x) (Q0 a x))) a
      = (fun a ⇒ conc_nu (C' a)) a) in H3.
    auto_conc_ext. apply equal_f with b in H4. inverts H4.
    constructor.
  + destruct (conc_ho_ho_beta_exp a C) as [C'' []].
    subst. conc_change_ext.
    destruct (conc_ho_ho_beta_exp a C') as [C''' []]. subst.
    assert (conc_nu (fun y ⇒ conc_nu (fun x ⇒ C''' a x y)) = conc_nu (C'0 a)).
     rewrite× HeqC'a.
    change ((fun a ⇒ conc_nu (fun y ⇒ conc_nu (fun x ⇒ C''' a x y))) a
      = (fun a ⇒ conc_nu (C'0 a)) a) in H5.
    auto_conc_ext.
    apply equal_f with b in H6. inverts H6.
    apply pull_nunu with (a::b::L); intros. simpl_notin.
    change (pull ((fun b ⇒ conc_nu (C'' b a0)) b) ((fun b ⇒ C''' b a0) b)).
    eapply H0; eauto; auto with hopi.
      intros_all. constructor; intros.
      forwards*: H6 b0. simpl_notin. forwards*: H16 b1.
      change (conc_notin a0 ((fun a ⇒ C'' a b0 b1) a)).
      eapply conc_notin_rename; eauto.
      intros_all. constructor; intros.
      forwards*: H8 b0. simpl_notin. forwards*: H16 b1.
      change (conc_notin a0 ((fun a ⇒ C''' a b0 b1) a)).
      eapply conc_notin_rename; eauto.
      intros_all. constructor; intros.
      forwards*: H3 a0. simpl_notin. forwards*: H16 b0. simpl_notin.
      intros_all. constructor; intros.
      forwards*: H4 a0. simpl_notin. forwards*: H16 b0. simpl_notin.
Qed.

Lemma exists_pull' : ∀ n C'', sizec C'' n →
  ∀ a C, conc_notin_ho a C → C'' = C a →
  ∃ C', pull (conc_nu C) C'.
Proof.
  induction n; intros; inverts H.
  conc_exp_ext a. eexists; econstructor.
  ho_conc_exp a C0. conc_change_ext.
  fresh_conc (conc_nu (C1 a)).
  forwards*: IHn x (C1 a). destruct H1 as [C'].
  ho_conc_exp a C'. ∃ (fun y ⇒ conc_nu (fun x ⇒ C'0 x y)).
  apply pull_nunu with (a::nil); intros.
  change (pull ((fun a0 ⇒ conc_nu (C1 a0)) a0)(C'0 a0)).
  apply pull_rename with a; auto with hopi.
Qed.

Lemma exists_pull : ∀ C, ∃ C', pull (conc_nu C) C'.
Proof.
  intros. fresh_conc (conc_nu C).
  destruct (exists_szc (C x)). forwards*: exists_pull'.
Qed.

Lemma pull_conc_wf : ∀ L C C',
   cwf_aux L C → pull C C' → ∀ b, cwf_aux (b::L)(C' b).
Proof.
  intros. gen L C'. induction C; intros.
  + inverts× H0.
  + inverts H1.
    - inverts H0. fresh_lp (b::L++L')((nu P) // nu Q).
      forwards*: H3 x. auto with hopi.
      rewrite <- (@app_nil_l name (b::L)).
      change (cwf_aux (nil ++ b :: L) ((fun x ⇒ conc_def (P x) (Q x)) b)).
      apply cwf_aux_change with x; auto with hopi.
    - inverts H0. fn (conc_nu (fun x ⇒ conc_nu (fun y ⇒ (C'0 x y)))).
      fn (conc_nu (fun x ⇒ conc_nu (C x))).
      apply cwf_nu with (b::L++L'++L0++L1++L2); intros.
      simpl_notin. forwards*: H1. forwards*: H0 a.
      simpl_notin. forwards*: H3 a.
      forwards*: H a (a::L).
      eapply cwf_include; eauto. intros_all.
      default_simp.
Qed.

Lemma conc_to_proc : ∀ n (C:conc), sizec C n →
   conc_wf C → ∀ a, ∃ P, ltsconc P a C ∧
        (∀ (C':conc), ltsconc P a C' → C = C').
Proof.
  induction n; intros; inverts H.
  + ∃ (a!(P) Q). split; auto with hopi.
    intros. inverts× H.
  +
    forwards*: exists_pull C0. destruct H as [C'].
    assert (Hnew: conc_new C' (conc_nu C0)) by apply× pull_conc_new.
    fresh_lc (a::nil)(conc_nu C0).
    forwards*: IHn (C' x) a.
      forwards*: pull_size H. constructor×.
      forwards*: pull_conc_wf x.
      eapply cwf_include; eauto. intros_all. default_simp.
    destruct H2 as [P []]. exp x P. ∃ (nu P0).
    split. apply ltsc_new with C' (a::nil); intros.
    assert (subst_name x b a a). constructor×.
    apply ltsconc_rename with a x; auto.
      forwards*: cnew_notin_rev; auto with hopi.
    auto.
    intros. assert (HxC'0:conc_notin x C'0).
      eapply ltsconc_notin; eauto with hopi.
    inverts H7. fresh_lpc (a::x::L) (nu P0) (conc_nu C).
    forwards*: H9 x0. assert (ltsconc (P0 x) a (C x)).
      apply ltsconc_rename with a x0; auto.
      constructor×.
    forwards*: H4. auto_conc_ext.
      forwards*: cnew_notin_rev Hnew x; auto with hopi.
      forwards*: cnew_notin_rev H10 x; auto with hopi.
    eapply cnew_unique; eauto.
Qed.

Lemma abs_to_proc : ∀ (F:abs) a,
    ∃ P, ltsabs P a F ∧
        (∀ (F':abs), ltsabs P a F' → F = F').
Proof.
  intros. ∃ (a? F); splits*; auto with hopi.
  intros. inverts× H.
Qed.

Lemma simulation_up_to_sc_howe : ∀ Rel, simulation Rel → refl Rel → rename_compatible Rel →
  (Rincl sc0 Rel) → trans Rel → simulation_up_to_sc (howe Rel).
Proof.
  intros_all. 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).
    destruct (exists_szc C) as [n Hszc].
    forwards*: conc_to_proc C a. destruct H6 as [R [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 H6 H3; eauto with hopi.
    destruct H7 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. eexists; intuition eauto with sc.
    ∃ P'2; intuition eauto with sc. 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 H5 as [R [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 H5; eauto with hopi.
    destruct H6 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. eexists; intuition eauto with sc.
    ∃ P'2; intuition eauto with sc. 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 → refl 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.
  ×
    intros. assert (Rincl sc0 (tclosure (howe Rel))).
      intros_all. apply× tclosure_once. apply× Rincl_sc0_howe.
    intros_all. induction H4.
    + forwards*: simulation_up_to_sc_howe Rel.
      specialize (H5 x y H4).
      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 H4_;
      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; apply bisim_refl.
      intros_all. ∃ sc0. intuition. apply struct_congr_bisim.
      apply× tclosure_once.
Qed.