Library BisimTheory

Require Import SfLib.
Require Import LibTactics.
Require Export LabeledTransitionSystems.

Section Bisimulation.
  Variable lts: labeled_transition_system.
  Import Stepping.

Definition inv {A B C:Type} (R: A→B→C) := fun a b ⇒ R b a.

  Lemma inv_inv: ∀ {A B C: Type} (R: A→B→C), inv (inv R) = R.
  Proof. reflexivity. Qed.


  Definition strong_one_way_termination_sensitive {lts: labeled_transition_system} (R:lts_S→lts_S→Prop) : Prop :=
    ∀ p q, R p q →
    (is_halted p → q=p).

  Definition strong_simulation {lts: labeled_transition_system} (R:lts_S→lts_S→Prop) : Prop :=
    ∀ p q, R p q →
    (∀ p',
      tstep p p' →
      ∃ q', tstep q q' ∧ R p' q') ∧
    (∀ a p',
      lstep p a p' →
      ∃ q', lstep q a q' ∧ R p' q').

  Definition strong_bisimulation {lts: labeled_transition_system} (R:lts_S→lts_S→Prop) : Prop :=
    strong_one_way_termination_sensitive R ∧ strong_one_way_termination_sensitive (inv R) ∧
    strong_simulation R ∧ strong_simulation (inv R).

  Definition sbisimilar {lts: labeled_transition_system} p q :=
    ∃ R, strong_bisimulation R ∧ R p q.

  Lemma strong_one_way_termination_sensitive_halted: ∀ p q R,
    strong_one_way_termination_sensitive R → R p q →
    is_halted p → q = p.
  Proof. intros; eapply H; eauto. Qed.

  Lemma strong_simulation_tstep: ∀ p q R p',
    strong_simulation R → R p q →
    tstep p p' → ∃ q', tstep q q' ∧ R p' q'.
  Proof. intros; eapply H; eauto. Qed.

  Lemma strong_simulation_lstep: ∀ p q R p' a,
    strong_simulation R → R p q →
    lstep p a p' → ∃ q', lstep q a q' ∧ R p' q'.
  Proof. intros; eapply H; eauto. Qed.

  Lemma strong_simulation_step_star: ∀ p q R la p',
    strong_simulation R → R p q →
    step_star p la p' →
    ∃ q',
      step_star q la q' ∧ R p' q'.
  Proof.
    intros.
    revert q H H0.
    induction H1; intros.
    - ∃ q; split; auto. apply step_nil.
    - edestruct strong_simulation_lstep as [q'[??]]; eauto.
    edestruct IHstep_star as [q''[??]]; clear IHstep_star; eauto.
    ∃ q''; split; auto.
    eapply step_lcons; eauto.
    - edestruct strong_simulation_tstep as [q'[??]]; eauto.
    edestruct IHstep_star as [q''[??]]; eauto.
    ∃ q''; split; auto.
    eapply step_tcons; eauto.
  Qed.

  Lemma strong_bisimulation_symm: ∀ (R: lts_S→lts_S→Prop),
    strong_one_way_termination_sensitive R →
    strong_simulation R →
    (∀ p q, R p q → R q p) →
    strong_bisimulation R.
  Proof.
    intros.
    cut (∀ p q, R p q ↔ R q p); intros.
    splits; unfold inv; auto.
    introv; intros; eapply H; eauto.
    split; intros; simpl in H3; setoid_rewrite H2; rewrite H2 in H3; eapply H0; eauto.
    split; intros; eauto.
  Qed.

  Lemma sbisim_symm: ∀ p q,
    sbisimilar p q →
    sbisimilar q p.
  Proof.
    intros.
    destruct H as [R[[?[?[??]]]?]].
    ∃ (inv R); split; auto.
    splits; auto.
  Qed.

  Lemma strong_one_way_termination_sensitive_id: strong_one_way_termination_sensitive (fun p q ⇒ p = q).
  Proof. introv; intros; subst; auto. Qed.

  Lemma strong_simulation_id: strong_simulation (fun p q ⇒ p = q).
  Proof. split; intros; simpl in H; subst q; eauto. Qed.

  Lemma sbisim_refl: ∀ p,
    sbisimilar p p.
  Proof.
    intros.
    ∃ (fun (p q:lts_S) ⇒ p=q); split; auto.
    apply strong_bisimulation_symm; auto; clear p.
    apply strong_one_way_termination_sensitive_id.
    apply strong_simulation_id.
  Qed.

  Lemma sbisim_strong_one_way_termination_sensitive: ∀ (R: lts_S→lts_S→Prop),
    (∀ p q, R p q → sbisimilar p q) →
    strong_one_way_termination_sensitive R.
  Proof. red; intros; apply H in H0; destruct H0 as [R'[[?[? _]]?]]; eauto. Qed.

  Lemma sbisim_strong_simulation: ∀ (R: lts_S→lts_S→Prop),
    (∀ p q, R p q ↔ sbisimilar p q) →
    strong_simulation R.
  Proof.
    split; intros; apply H in H0; destruct H0 as [R'[[?[?[? ?]]]?]].
    edestruct strong_simulation_tstep with (R:=R') as [q'[??]]; eauto.
    ∃ q'; split; auto. apply H. ∃ R'; split; auto. splits; auto.
    edestruct strong_simulation_lstep with (R:=R') as [q'[??]]; eauto.
    ∃ q'; split; auto. apply H. ∃ R'; split; auto. splits; auto.
  Qed.

  Lemma tstep_sbisim1: ∀ p q p',
    tstep p p' →
    sbisimilar p q →
    ∃ q', tstep q q' ∧ sbisimilar p' q'.
  Proof.
    intros.
    edestruct strong_simulation_tstep as [q'[??]]; eauto.
    apply sbisim_strong_simulation; reflexivity.
  Qed.

  Lemma tstep_sbisim2: ∀ p q q',
    tstep q q' →
    sbisimilar p q →
    ∃ p', tstep p p' ∧ sbisimilar p' q'.
  Proof.
    intros.
    apply sbisim_symm in H0.
    edestruct strong_simulation_tstep as [p'[??]]; eauto.
    apply sbisim_strong_simulation; reflexivity.
    ∃ p'; split; auto.
    apply sbisim_symm; auto.
  Qed.

  Lemma lstep_sbisim1: ∀ p q a p',
    lstep p a p' →
    sbisimilar p q →
    ∃ q', lstep q a q' ∧ sbisimilar p' q'.
  Proof.
    intros.
    edestruct strong_simulation_lstep as [q'[??]]; eauto.
    apply sbisim_strong_simulation; reflexivity.
  Qed.

  Lemma lstep_sbisim2: ∀ p q a q',
    lstep q a q' →
    sbisimilar p q →
    ∃ p', lstep p a p' ∧ sbisimilar p' q'.
  Proof.
    intros.
    apply sbisim_symm in H0.
    edestruct strong_simulation_lstep as [p'[??]]; eauto.
    apply sbisim_strong_simulation; reflexivity.
    ∃ p'; split; auto.
    apply sbisim_symm; auto.
  Qed.

  Lemma halted_sbisim1: ∀ p q,
    is_halted p →
    sbisimilar p q →
    q=p.
  Proof.
    intros.
    eapply strong_one_way_termination_sensitive_halted; eauto.
    apply sbisim_strong_one_way_termination_sensitive; auto.
  Qed.

  Lemma halted_sbisim2: ∀ p q,
    is_halted q →
    sbisimilar p q →
    p=q.
  Proof.
    intros.
    eapply strong_one_way_termination_sensitive_halted; eauto.
    apply sbisim_strong_one_way_termination_sensitive; eauto.
    apply sbisim_symm; auto.
  Qed.

  Lemma step_star_sbisim1: ∀ p q la p',
    sbisimilar p q →
    step_star p la p' →
    ∃ q',
      step_star q la q' ∧ sbisimilar p' q'.
  Proof.
    intros.
    eapply strong_simulation_step_star; eauto.
    apply sbisim_strong_simulation; reflexivity.
  Qed.

  Lemma step_star_sbisim2: ∀ p q la q',
    sbisimilar p q →
    step_star q la q' →
    ∃ p',
      step_star p la p' ∧ sbisimilar p' q'.
  Proof.
    intros.
    edestruct strong_simulation_step_star as [p'[??]].
    apply sbisim_strong_simulation; reflexivity.
    apply sbisim_symm; eauto.
    eauto.
    ∃ p'; split; auto; apply sbisim_symm; auto.
  Qed.

  Lemma halted_converge_sbisim1: ∀ p q la p',
    step_star p la p' →
    is_halted p' →
    sbisimilar p q →
    step_star q la p'.
  Proof.
    intros.
    edestruct step_star_sbisim1 as [q'[??]]; eauto.
    apply halted_sbisim1 in H3; subst; auto.
  Qed.

  Lemma halted_converge_sbisim2: ∀ p q la q',
    step_star q la q' →
    is_halted q' →
    sbisimilar p q →
    step_star p la q'.
  Proof.
    intros.
    eapply halted_converge_sbisim1; eauto.
    apply sbisim_symm; auto.
  Qed.

  Lemma sbisim_trans: ∀ p q r,
    sbisimilar p q →
    sbisimilar q r →
    sbisimilar p r.
  Proof.
    intros.
    ∃ (fun p r ⇒ ∃ q, sbisimilar p q ∧ sbisimilar q r).
    split; eauto.
    clear p q r H H0.
    apply strong_bisimulation_symm; intros.
    - intros p r [q[??]] ?.
    apply halted_sbisim1 in H; subst; auto.
    apply halted_sbisim1 in H0; subst; auto.
    - intros p r [q[??]]; split; intros.
    edestruct tstep_sbisim1 as [q'[??]]; eauto.
    edestruct tstep_sbisim1 with (p:=q) as [r'[??]]; eauto.
    edestruct lstep_sbisim1 as [q'[??]]; eauto.
    edestruct lstep_sbisim1 with (p:=q) as [r'[??]]; eauto.
    - destruct H as [r[??]].
    ∃ r; split; apply sbisim_symm; auto.
  Qed.


  Definition one_way_termination_sensitive {lts: labeled_transition_system} (R:lts_S→lts_S→Prop) : Prop :=
    ∀ p q, R p q →
    (is_halted p → step_star q nil p).

  Definition weak_simulation {lts: labeled_transition_system} (R:lts_S→lts_S→Prop) : Prop :=
    ∀ p q, R p q →
    (∀ p',
      tstep p p' →
      ∃ q', step_star q nil q' ∧ R p' q') ∧
    (∀ a p',
      lstep p a p' →
      ∃ q', step_star q [a] q' ∧ R p' q').

  Definition weak_bisimulation {lts: labeled_transition_system} (R:lts_S→lts_S→Prop) : Prop :=
    one_way_termination_sensitive R ∧ one_way_termination_sensitive (inv R) ∧
    weak_simulation R ∧ weak_simulation (inv R).

  Definition wbisimilar {lts: labeled_transition_system} p q :=
    ∃ R, weak_bisimulation R ∧ R p q.

  Lemma one_way_termination_sensitive_halted: ∀ p q R,
    one_way_termination_sensitive R → R p q →
    is_halted p → step_star q nil p.
  Proof. intros; eapply H; eauto. Qed.

  Lemma weak_simulation_tstep: ∀ p q R p',
    weak_simulation R → R p q →
    tstep p p' → ∃ q', step_star q nil q' ∧ R p' q'.
  Proof. intros; eapply H; eauto. Qed.

  Lemma weak_simulation_lstep: ∀ p q R p' a,
    weak_simulation R → R p q →
    lstep p a p' → ∃ q', step_star q [a] q' ∧ R p' q'.
  Proof. intros; eapply H; eauto. Qed.

  Lemma weak_simulation_step_star: ∀ p q R la p',
    weak_simulation R → R p q →
    step_star p la p' →
    ∃ q',
      step_star q la q' ∧ R p' q'.
  Proof.
    intros.
    revert q H H0.
    induction H1; intros.
    - ∃ q; split; auto. apply step_nil.
    - edestruct weak_simulation_lstep as [q'[??]]; eauto.
    edestruct IHstep_star as [q''[??]]; clear IHstep_star; eauto.
    ∃ q''; split; auto.
    change (a::la) with ([a]++la).
    eapply step_star_app; eauto.
    - edestruct weak_simulation_tstep as [q'[??]]; eauto.
    edestruct IHstep_star as [q''[??]]; eauto.
    ∃ q''; split; auto.
    change la with (nil++la).
    eapply step_star_app; eauto.
  Qed.

  Lemma weak_bisimulation_symm: ∀ (R: lts_S→lts_S→Prop),
    one_way_termination_sensitive R →
    weak_simulation R →
    (∀ p q, R p q → R q p) →
    weak_bisimulation R.
  Proof.
    intros.
    cut (∀ p q, R p q ↔ R q p); intros.
    splits; unfold inv; auto.
    introv; intros; eapply H; eauto.
    split; intros; simpl in H3; setoid_rewrite H2; rewrite H2 in H3; eapply H0; eauto.
    split; intros; eauto.
  Qed.

  Lemma wbisim_symm: ∀ p q,
    wbisimilar p q →
    wbisimilar q p.
  Proof.
    intros.
    destruct H as [R[[?[?[??]]]?]].
    ∃ (inv R); split; auto.
    splits; auto.
  Qed.

  Lemma one_way_termination_sensitive_id: ∀ (R:lts_S→lts_S→Prop),
    (∀ p q, R p q → p=q) → one_way_termination_sensitive R.
  Proof. red; intros; simpl in *; apply H in H0; subst; apply step_nil. Qed.

  Lemma weak_simulation_id: ∀ (R:lts_S→lts_S→Prop),
    (∀ p q, R p q ↔ p=q) → weak_simulation R.
  Proof.
    split; intros; simpl in H; apply H in H0; subst q; (∃ p'; split; auto; [ | apply H; auto]).
    apply single_tstep; auto.
    apply single_lstep; auto.
  Qed.

  Lemma wbisim_refl: ∀ p,
    wbisimilar p p.
  Proof.
    intros.
    ∃ (fun (p q:lts_S) ⇒ p=q); split; auto.
    apply weak_bisimulation_symm; auto; clear p.
    apply one_way_termination_sensitive_id; auto.
    apply weak_simulation_id; reflexivity.
  Qed.

  Lemma wbisim_one_way_termination_sensitive: ∀ (R: lts_S→lts_S→Prop),
    (∀ p q, R p q → wbisimilar p q) → one_way_termination_sensitive R.
  Proof. red; intros; apply H in H0; destruct H0 as [R'[[?[? _]]?]]; eauto. Qed.

  Lemma wbisim_weak_simulation: ∀ (R: lts_S→lts_S→Prop),
    (∀ p q, R p q ↔ wbisimilar p q) → weak_simulation R.
  Proof.
    split; intros; apply H in H0; destruct H0 as [R'[[?[?[? ?]]]?]].
    edestruct weak_simulation_tstep with (R:=R') as [q'[??]]; eauto.
    ∃ q'; split; auto. apply H. ∃ R'; split; auto. splits; auto.
    edestruct weak_simulation_lstep with (R:=R') as [q'[??]]; eauto.
    ∃ q'; split; auto. apply H. ∃ R'; split; auto. splits; auto.
  Qed.

  Lemma tstep_wbisim1: ∀ p q p',
    tstep p p' →
    wbisimilar p q →
    ∃ q', step_star q nil q' ∧ wbisimilar p' q'.
  Proof.
    intros.
    edestruct weak_simulation_tstep as [q'[??]]; eauto.
    apply wbisim_weak_simulation; reflexivity.
  Qed.

  Lemma tstep_wbisim2: ∀ p q q',
    tstep q q' →
    wbisimilar p q →
    ∃ p', step_star p nil p' ∧ wbisimilar p' q'.
  Proof.
    intros.
    apply wbisim_symm in H0.
    edestruct weak_simulation_tstep as [p'[??]]; eauto.
    apply wbisim_weak_simulation; reflexivity.
    ∃ p'; split; auto.
    apply wbisim_symm; auto.
  Qed.

  Lemma lstep_wbisim1: ∀ p q a p',
    lstep p a p' →
    wbisimilar p q →
    ∃ q', step_star q [a] q' ∧ wbisimilar p' q'.
  Proof.
    intros.
    edestruct weak_simulation_lstep as [q'[??]]; eauto.
    apply wbisim_weak_simulation; reflexivity.
  Qed.

  Lemma lstep_wbisim2: ∀ p q a q',
    lstep q a q' →
    wbisimilar p q →
    ∃ p', step_star p [a] p' ∧ wbisimilar p' q'.
  Proof.
    intros.
    apply wbisim_symm in H0.
    edestruct weak_simulation_lstep as [p'[??]]; eauto.
    apply wbisim_weak_simulation; reflexivity.
    ∃ p'; split; auto.
    apply wbisim_symm; auto.
  Qed.

  Lemma halted_wbisim1: ∀ p q,
    is_halted p →
    wbisimilar p q →
    step_star q nil p.
  Proof.
    intros.
    eapply one_way_termination_sensitive_halted; eauto.
    apply wbisim_one_way_termination_sensitive; auto.
  Qed.

  Lemma halted_wbisim2: ∀ p q,
    is_halted q →
    wbisimilar p q →
    step_star p nil q.
  Proof.
    intros.
    apply halted_wbisim1; auto.
    apply wbisim_symm; auto.
  Qed.

  Lemma step_star_wbisim1: ∀ p q la p',
    wbisimilar p q →
    step_star p la p' →
    ∃ q',
      step_star q la q' ∧ wbisimilar p' q'.
  Proof.
    intros.
    eapply weak_simulation_step_star; eauto.
    apply wbisim_weak_simulation; reflexivity.
  Qed.

  Lemma step_star_wbisim2: ∀ p q la q',
    wbisimilar p q →
    step_star q la q' →
    ∃ p',
      step_star p la p' ∧ wbisimilar p' q'.
  Proof.
    intros.
    edestruct step_star_wbisim1 with (p:=q) as [p'[??]]; eauto.
    apply wbisim_symm; eauto.
    ∃ p'; split; auto; apply wbisim_symm; auto.
  Qed.

  Lemma halted_converge_wbisim1: ∀ p q la p',
    step_star p la p' →
    is_halted p' →
    wbisimilar p q →
    step_star q la p'.
  Proof.
    intros.
    edestruct step_star_wbisim1 as [q'[??]]; eauto.
    apply halted_wbisim1 in H3; subst; auto.
    replace la with (la++(@nil lts_L)).
    eapply step_star_app; eauto.
    apply app_nil_r.
  Qed.

  Lemma halted_converge_wbisim2: ∀ p q la q',
    step_star q la q' →
    is_halted q' →
    wbisimilar p q →
    step_star p la q'.
  Proof.
    intros.
    eapply halted_converge_wbisim1; eauto.
    apply wbisim_symm; auto.
  Qed.

  Lemma wbisim_trans: ∀ p q r,
    wbisimilar p q →
    wbisimilar q r →
    wbisimilar p r.
  Proof.
    intros.
    ∃ (fun p r ⇒ ∃ q, wbisimilar p q ∧ wbisimilar q r).
    split; eauto.
    clear p q r H H0.
    apply weak_bisimulation_symm; intros.
    - intros p r [q[??]] ?.
    change nil with (nil++(@nil lts_L)).
    eapply halted_converge_wbisim1; eauto.
    apply halted_wbisim1; auto.
    - intros p r [q[??]]; split; intros.
    edestruct tstep_wbisim1 as [q'[??]]; eauto.
    edestruct step_star_wbisim1 with (p:=q) as [r'[??]]; eauto.
    edestruct lstep_wbisim1 as [q'[??]]; eauto.
    edestruct step_star_wbisim1 with (p:=q) as [r'[??]]; eauto.
    - destruct H as [r[??]].
    ∃ r; split; apply wbisim_symm; auto.
  Qed.

  Lemma strong_weak_one_way_termination_sensitive: ∀ R,
    strong_one_way_termination_sensitive R → one_way_termination_sensitive R.
  Proof. repeat intro; eapply H in H1; eauto; subst q; apply step_nil. Qed.

  Lemma strong_weak_simulation: ∀ R,
    strong_simulation R → weak_simulation R.
  Proof.
    split; intros.
    edestruct strong_simulation_tstep as [q'[??]]; eauto.
    ∃ q'; split; auto; apply single_tstep; auto.
    edestruct strong_simulation_lstep as [q'[??]]; eauto.
    ∃ q'; split; auto; apply single_lstep; auto.
  Qed.

  Lemma sbisim_wbisim: ∀ p q,
    sbisimilar p q → wbisimilar p q.
  Proof.
    intros.
    ∃ sbisimilar; split; auto.
    splits.
    apply strong_weak_one_way_termination_sensitive.
    apply sbisim_strong_one_way_termination_sensitive; auto.
    apply strong_weak_one_way_termination_sensitive.
    apply sbisim_strong_one_way_termination_sensitive; auto.
    intros; apply sbisim_symm; auto.
    apply strong_weak_simulation.
    apply sbisim_strong_simulation; reflexivity.
    apply strong_weak_simulation.
    apply sbisim_strong_simulation.
    intros; split; apply sbisim_symm; auto.
  Qed.

  Definition tstep_weak_bisimulation (R: lts_S→lts_S→Prop) : Prop :=
    ∀ p q, R p q →
      (is_halted p → step_star q nil p) ∧
      (is_halted q → step_star p nil q) ∧
      (∀ p',
        tstep p p' →
        ∃ q',
          step_star q nil q' ∧ wbisimilar p' q') ∧
      (∀ q',
        tstep q q' →
        ∃ p',
          step_star p nil p' ∧ wbisimilar p' q') ∧
      (∀ a p',
        lstep p a p' →
        ∃ q',
          step_star q [a] q' ∧ R p' q') ∧
      (∀ a q',
        lstep q a q' →
        ∃ p',
          step_star p [a] p' ∧ R p' q').

  Lemma wbisim_tstep: ∀ R p q,
    tstep_weak_bisimulation R →
    R p q →
    wbisimilar p q.
  Proof.
   intros.
    ∃ (fun p q ⇒ R p q ∨ wbisimilar p q).
    split; auto.
    clear p q H0.
    splits; red; intros p q [?|?]; intros.
    - edestruct H as [? _]; eauto.
    - eapply halted_wbisim1; eauto.
    - edestruct H as [_[? _]]; eauto.
    - eapply halted_wbisim2; eauto.
    - split; intros.
    + edestruct H as [_[_[? _]]]; eauto.
    edestruct H2 as [q'[??]]; eauto.
    + edestruct H as [_[_[_[_[? _]]]]]; eauto.
    edestruct H2 as [q'[??]]; eauto.
    - split; intros.
    + edestruct tstep_wbisim1 as [q'[??]]; eauto.
    + edestruct lstep_wbisim1 as [q'[??]]; eauto.
    - split; intros; unfold inv.
    + edestruct H as [_[_[_[? _]]]]; eauto.
    edestruct H2 as [q'[??]]; eauto.
    + edestruct H as [_[_[_[_[_ ?]]]]]; eauto.
    edestruct H2 as [q'[??]]; eauto.
    - split; intros; unfold inv.
    + edestruct tstep_wbisim2 as [q'[??]]; eauto.
    + edestruct lstep_wbisim2 as [q'[??]]; eauto.
  Qed.

  Lemma wbisim_step: ∀ p q,
    (is_halted p → step_star q nil p) →
    (is_halted q → step_star p nil q) →
    (∀ p', tstep p p' → ∃ q', step_star q nil q' ∧ wbisimilar p' q') →
    (∀ q', tstep q q' → ∃ p', step_star p nil p' ∧ wbisimilar p' q') →
    (∀ a p', lstep p a p' → ∃ q', step_star q [a] q' ∧ wbisimilar p' q') →
    (∀ a q', lstep q a q' → ∃ p', step_star p [a] p' ∧ wbisimilar p' q') →
    wbisimilar p q.
  Proof.
    intros.
    ∃ (fun p q ⇒
      ((is_halted p → step_star q nil p) ∧
      (is_halted q → step_star p nil q) ∧
      (∀ p', tstep p p' → ∃ q', step_star q nil q' ∧ wbisimilar p' q') ∧
      (∀ q', tstep q q' → ∃ p', step_star p nil p' ∧ wbisimilar p' q') ∧
      (∀ a p', lstep p a p' → ∃ q', step_star q [a] q' ∧ wbisimilar p' q') ∧
      (∀ a q', lstep q a q' → ∃ p', step_star p [a] p' ∧ wbisimilar p' q'))
      ∨ wbisimilar p q).
    split; eauto.
    clear p q H H0 H1 H2 H3 H4.
    apply weak_bisimulation_symm.
    × intros p q [ [?[?[?[?[??]]]]] | ?]; intros.
    - apply H; auto; apply lstep_nil.
    - eapply halted_wbisim1; eauto.
    × intros p q [ [?[?[?[?[??]]]]] | ?]; intros.
    - split; intros.
    + edestruct H1 as [q'[??]]; eauto.
    + edestruct H3 as [q'[??]]; eauto.
    - split; intros.
    + edestruct tstep_wbisim1 as [q'[??]]; eauto.
    + edestruct lstep_wbisim1 as [q'[??]]; eauto.
    × intros q p [?|?]; intuition.
    left; splits; intros; auto.
    edestruct H2 as [q'[??]]; eauto; apply wbisim_symm in H7; eauto.
    edestruct H1 as [p'[??]]; eauto; apply wbisim_symm in H7; eauto.
    edestruct H5 as [q'[??]]; eauto; apply wbisim_symm in H7; eauto.
    edestruct H3 as [p'[??]]; eauto; apply wbisim_symm in H7; eauto.
    right; apply wbisim_symm; auto.
    × iauto.
  Qed.

  Lemma wbisim_tstep_det: ∀ p p',
    deterministic_lts lts →
    tstep p p' →
    wbisimilar p p'.
  Proof.
    intros.
    ∃ (fun p p' ⇒ tstep p p' ∨ p'=p).
    split; auto; clear p p' H0.
    splits; intros p p' [?|?]; intros; unfold inv in *; subst.
    × false; eapply halted_correct1; eauto.
    × apply step_nil.
    × apply single_tstep; auto.
    × apply step_nil.
    × split; intros.
    - destruct H as [_ ?].
    assert (p'0 = p') by (eapply H; eauto); subst p'0.
    ∃ p'; split; auto. apply step_nil.
    - false; eapply H; eauto.
    × split; intros.
    - ∃ p'; split; auto. apply single_tstep; auto.
    - ∃ p'; split; auto. apply single_lstep; auto.
    × split; intros.
    - ∃ p'0; split; auto.
    eapply step_tcons; eauto. apply single_tstep; auto.
    - ∃ p'0; split; auto.
    eapply step_tcons; eauto. apply single_lstep; auto.
    × split; intros.
    - ∃ p'0; split; auto. apply single_tstep; auto.
    - ∃ p'0; split; auto. apply single_lstep; auto.
  Qed.


  Definition coupled_simulation_flipping {lts: labeled_transition_system} (R1 R2: lts_S→lts_S→Prop) : Prop :=
    (∀ p q, R1 p q → ∃ q', step_star q nil q' ∧ R2 p q').

  Definition coupled_similar' {lts: labeled_transition_system} p q :=
    ∃ R1 R2,
      coupled_simulation_flipping R1 R2 ∧ coupled_simulation_flipping (inv R2) (inv R1) ∧
      one_way_termination_sensitive R1 ∧ one_way_termination_sensitive (inv R2) ∧
      weak_simulation R1 ∧ weak_simulation (inv R2) ∧
      R1 p q ∧ R2 p q.

  Definition partial_coupled_similar {lts: labeled_transition_system} p q :=
    ∃ R,
      one_way_termination_sensitive R ∧
      coupled_simulation_flipping R (inv R) ∧ weak_simulation R ∧
      R p q.

  Definition coupled_similar {lts: labeled_transition_system} p q :=
    ∃ R,
      one_way_termination_sensitive R ∧
      coupled_simulation_flipping R (inv R) ∧ weak_simulation R ∧
      R p q ∧ R q p.

  Lemma coupled_similar_equiv: ∀ p q,
    coupled_similar' p q ↔ coupled_similar p q.
  Proof.
    split; intros.
    × destruct H as [R1[R2[?[?[?[?[?[?[??]]]]]]]]].
    ∃ (fun p q ⇒ R1 p q ∨ R2 q p).
    splits; auto.
    - clear p q H5 H6; intros p q [?|?]; intros.
    eapply H1; eauto.
    eapply H2; eauto.
    - clear p q H5 H6; unfold inv in *; intros p q [?|?].
    + edestruct H as [q'[??]]; eauto.
    + edestruct H0 as [q'[??]]; eauto.
    - clear p q H5 H6; unfold inv in *; intros p q [?|?]; split; intros.
    + edestruct weak_simulation_tstep with (R:=R1) as [q'[??]]; eauto.
    + edestruct weak_simulation_lstep with (R:=R1) as [q'[??]]; eauto.
    + edestruct weak_simulation_tstep with (R:=inv R2) as [q'[??]]; eauto.
    + edestruct weak_simulation_lstep with (R:=inv R2) as [q'[??]]; eauto.
    × destruct H as [R[?[?[?[??]]]]].
    ∃ R (inv R); splits; auto.
  Qed.

  Lemma cssim_symm: ∀ p q,
    coupled_similar p q →
    coupled_similar q p.
  Proof. intros p q [R[?[?[?[??]]]]]; ∃ R; auto. Qed.

  Lemma coupled_simulation_flipping_id: ∀ (R1 R2: lts_S→lts_S→Prop),
    (∀ p q, R1 p q → p=q) → (∀ p, R2 p p) → coupled_simulation_flipping R1 R2.
  Proof.
    unfold coupled_simulation_flipping; intros.
    apply H in H1; subst.
    ∃ q; split; auto. apply step_nil.
  Qed.

  Lemma cssim_refl: ∀ p,
    coupled_similar p p.
  Proof.
    intros.
    ∃ (fun (p q:lts_S) ⇒ p=q).
    splits; auto.
    × apply one_way_termination_sensitive_id; auto.
    × apply coupled_simulation_flipping_id; unfold inv; auto.
    × apply weak_simulation_id; unfold inv; intuition.
  Qed.

  Lemma cssim_pcssim1: ∀ p q,
    coupled_similar p q → partial_coupled_similar p q.
  Proof.
    intros.
    destruct H as [R[?[?[?[??]]]]].
    ∃ R; auto.
  Qed.

  Lemma cssim_pcssim2: ∀ p q,
    coupled_similar p q → partial_coupled_similar q p.
  Proof. intros; apply cssim_pcssim1; apply cssim_symm; auto. Qed.

  Lemma pcssim_one_way_termination_sensitive: ∀ (R: lts_S→lts_S→Prop),
    (∀ p q, R p q → partial_coupled_similar p q) → one_way_termination_sensitive R.
  Proof. red; intros; apply H in H0; destruct H0 as [R'[?[?[??]]]]; eauto. Qed.

  Lemma pcssim_coupled_simulation_flipping: ∀ (R1 R2: lts_S→lts_S→Prop),
    (∀ p q, R1 p q → partial_coupled_similar p q) →
    (∀ p q, partial_coupled_similar p q → R2 q p) →
    coupled_simulation_flipping R1 R2.
  Proof.
    red; intros.
    apply H in H1.
    destruct H1 as [R'[?[?[??]]]].
    edestruct H2 as [q'[??]]; eauto.
    ∃ q'; split; auto.
    apply H0. ∃ R'; auto.
  Qed.

  Lemma pcssim_weak_simulation: ∀ (R: lts_S→lts_S→Prop),
    (∀ p q, R p q ↔ partial_coupled_similar p q) → weak_simulation R.
  Proof.
    split; intros; apply H in H0; destruct H0 as [R'[?[?[??]]]].
    edestruct weak_simulation_tstep with (R:=R') as [q'[??]]; eauto.
    ∃ q'; split; auto. apply H. ∃ R'; split; auto.
    edestruct weak_simulation_lstep with (R:=R') as [q'[??]]; eauto.
    ∃ q'; split; auto. apply H. ∃ R'; split; auto.
  Qed.

  Lemma tstep_pcssim: ∀ p q p',
    tstep p p' →
    partial_coupled_similar p q →
    ∃ q', step_star q nil q' ∧ partial_coupled_similar p' q'.
  Proof.
    intros.
    edestruct weak_simulation_tstep as [q'[??]]; eauto.
    apply pcssim_weak_simulation; reflexivity.
  Qed.

  Lemma lstep_pcssim: ∀ p q a p',
    lstep p a p' →
    partial_coupled_similar p q →
    ∃ q', step_star q [a] q' ∧ partial_coupled_similar p' q'.
  Proof.
    intros.
    edestruct weak_simulation_lstep as [q'[??]]; eauto.
    apply pcssim_weak_simulation; reflexivity.
  Qed.

  Lemma step_star_pcssim: ∀ p q la p',
    partial_coupled_similar p q →
    step_star p la p' →
    ∃ q',
      step_star q la q' ∧ partial_coupled_similar p' q'.
  Proof.
    intros.
    edestruct weak_simulation_step_star as [q'[??]]; eauto.
    apply pcssim_weak_simulation; reflexivity.
  Qed.

  Lemma flip_pcssim: ∀ p q,
    partial_coupled_similar p q →
    ∃ q',
      step_star q nil q' ∧ partial_coupled_similar q' p.
  Proof.
    intros.
    eapply pcssim_coupled_simulation_flipping with (R2 :=inv partial_coupled_similar); eauto.
  Qed.

  Lemma halted_pcssim1: ∀ p q,
    is_halted p →
    partial_coupled_similar p q →
    step_star q nil p.
  Proof. intros; eapply pcssim_one_way_termination_sensitive; eauto. Qed.

  Lemma halted_pcssim2: ∀ p q,
    is_halted q →
    partial_coupled_similar p q →
    step_star p nil q.
  Proof.
    intros.
    edestruct flip_pcssim as [q'[??]]; eauto.
    apply tstep_star_halted_resolve in H1; auto; subst q'.
    apply halted_pcssim1; auto.
  Qed.

  Lemma halted_converge_pcssim1: ∀ p q la p',
    step_star p la p' →
    is_halted p' →
    partial_coupled_similar p q →
    step_star q la p'.
  Proof.
    intros.
    edestruct step_star_pcssim as [q'[??]]; eauto.
    rewrite<- (List.app_nil_r la).
    eapply step_star_app; eauto.
    apply halted_pcssim1; auto.
  Qed.

  Lemma cssim_coupled_simulation_flipping: ∀ (R1 R2: lts_S→lts_S→Prop),
    (∀ p q, R1 p q ↔ coupled_similar p q) →
    (∀ p q, R1 p q ↔ R2 q p) →
    coupled_simulation_flipping R1 R2.
  Proof.
    red; intros.
    apply H in H1.
    ∃ q; split.
    apply step_nil.
    apply H0. apply H.
    apply cssim_symm; auto.
  Qed.

  Lemma pcssim_cssim: ∀ p q,
    partial_coupled_similar p q → partial_coupled_similar q p → coupled_similar p q.
  Proof.
    intros.
    ∃ (fun p q ⇒ partial_coupled_similar p q).
    splits; auto; clear p q H H0.
    × apply pcssim_one_way_termination_sensitive; auto.
    × apply pcssim_coupled_simulation_flipping; auto.
    × apply pcssim_weak_simulation; reflexivity.
  Qed.

  Lemma wbisim_coupled_sim: ∀ p q,
    wbisimilar p q →
    coupled_similar p q.
  Proof.
    intros.
    ∃ wbisimilar.
    splits; auto; try clear p q H.
    × apply wbisim_one_way_termination_sensitive; auto.
    × intros p q ?; ∃ q; split; auto. apply step_nil. apply wbisim_symm; auto.
    × apply wbisim_weak_simulation; reflexivity.
    × apply wbisim_symm; auto.
  Qed.


  Definition par_simulation {lts: labeled_transition_system} (R:lts_S→lts_S→Prop) : Prop :=
    ∀ p q, R p q →
    ∀ la p',
      step_star p la p' →
      (∃ q', step_star q la q' ∧ R p' q') ∨
      (∃ r', step_star p' nil r' ∧ step_star q la r').

  Definition par_bisimulation {lts: labeled_transition_system} (R:lts_S→lts_S→Prop) : Prop :=
    one_way_termination_sensitive R ∧ one_way_termination_sensitive (inv R) ∧
    weak_simulation R ∧ par_simulation (inv R).

  Definition par_bisimilar {lts: labeled_transition_system} p q :=
    ∃ R, par_bisimulation R ∧ R p q.

  Lemma par_simulation_step_star: ∀ p q R la p',
    par_simulation R → R p q →
    step_star p la p' →
    (∃ q', step_star q la q' ∧ R p' q') ∨ (∃ r', step_star p' nil r' ∧ step_star q la r').
  Proof. intros; eapply H; eauto. Qed.

  Lemma par_simulation_tstep: ∀ p q R p',
    par_simulation R → R p q →
    tstep p p' → (∃ q', step_star q nil q' ∧ R p' q') ∨ (∃ r', step_star p' nil r' ∧ step_star q nil r').
  Proof. intros; eapply par_simulation_step_star; eauto; apply single_tstep; auto. Qed.

  Lemma par_simulation_lstep: ∀ p q R p' a,
    par_simulation R → R p q →
    lstep p a p' → (∃ q', step_star q [a] q' ∧ R p' q') ∨ (∃ r', step_star p' nil r' ∧ step_star q [a] r').
  Proof. intros; eapply par_simulation_step_star; eauto; apply single_lstep; auto. Qed.

  Lemma weak_par_simulation: ∀ R,
    weak_simulation R → par_simulation R.
  Proof.
    intros.
    intros p q; intros.
    edestruct weak_simulation_step_star as [q'[??]]; eauto.
  Qed.

  Lemma pbisim_refl: ∀ p,
    par_bisimilar p p.
  Proof.
    intros.
    ∃ (fun (p q:lts_S) ⇒ p=q); split; auto.
    splits.
    apply one_way_termination_sensitive_id; auto.
    apply one_way_termination_sensitive_id; auto.
    apply weak_simulation_id; reflexivity.
    apply weak_par_simulation.
    apply weak_simulation_id; unfold inv; intros; iauto.
  Qed.

  Lemma pbisim_one_way_termination_sensitive1: ∀ (R: lts_S→lts_S→Prop),
    (∀ p q, R p q → par_bisimilar p q) → one_way_termination_sensitive R.
  Proof. red; intros; apply H in H0; destruct H0 as [R'[[?[? _]]?]]; eauto. Qed.

  Lemma pbisim_one_way_termination_sensitive2: ∀ (R: lts_S→lts_S→Prop),
    (∀ p q, R q p → par_bisimilar p q) → one_way_termination_sensitive R.
  Proof. red; intros; apply H in H0; destruct H0 as [R'[[?[? _]]?]]; eauto. Qed.

  Lemma pbisim_weak_simulation: ∀ (R: lts_S→lts_S→Prop),
    (∀ p q, R p q ↔ par_bisimilar p q) → weak_simulation R.
  Proof.
    split; intros; apply H in H0; destruct H0 as [R'[[?[?[? ?]]]?]].
    edestruct weak_simulation_tstep with (R:=R') as [q'[??]]; eauto.
    ∃ q'; split; auto. apply H. ∃ R'; split; auto. splits; auto.
    edestruct weak_simulation_lstep with (R:=R') as [q'[??]]; eauto.
    ∃ q'; split; auto. apply H. ∃ R'; split; auto. splits; auto.
  Qed.

  Lemma pbisim_par_simulation: ∀ (R: lts_S→lts_S→Prop),
    (∀ p q, R q p ↔ par_bisimilar p q) → par_simulation R.
  Proof.
    unfold par_simulation; intros; apply H in H0; destruct H0 as [R'[[?[?[? ?]]]?]].
    edestruct par_simulation_step_star with (R:=inv R') as [[q'[??]] | [r'[??]]]; eauto.
    left; ∃ q'; split; auto. apply H. ∃ R'; split; auto. splits; auto.
  Qed.

  Lemma wbisim_pbisim: ∀ p q,
    wbisimilar p q →
    par_bisimilar p q.
  Proof.
    intros.
    ∃ wbisimilar.
    split; auto.
    splits.
    apply wbisim_one_way_termination_sensitive; auto.
    apply wbisim_one_way_termination_sensitive; intros; apply wbisim_symm; auto.
    apply wbisim_weak_simulation; reflexivity.
    apply weak_par_simulation.
    apply wbisim_weak_simulation; split; intros; apply wbisim_symm; auto.
  Qed.

  Lemma tstep_pbisim1: ∀ p q p',
    tstep p p' →
    par_bisimilar p q →
    ∃ q', step_star q nil q' ∧ par_bisimilar p' q'.
  Proof.
    introv H [R[H0 H1]]. unfold par_bisimulation in ×.
    edestruct weak_simulation_tstep as [q'[??]]; jauto.
    ∃ q'; split; auto; ∃ R; auto.
  Qed.

  Lemma lstep_pbisim1: ∀ p q a p',
    lstep p a p' →
    par_bisimilar p q →
    ∃ q', step_star q [a] q' ∧ par_bisimilar p' q'.
  Proof.
    introv H [R[H0 H1]]. unfold par_bisimulation in ×.
    edestruct weak_simulation_lstep as [q'[??]]; jauto.
    ∃ q'; split; auto; ∃ R; auto.
  Qed.

  Lemma step_star_pbisim1: ∀ p q la p',
    step_star p la p' →
    par_bisimilar p q →
    ∃ q', step_star q la q' ∧ par_bisimilar p' q'.
  Proof.
    introv H [R[H0 H1]]; unfold par_bisimulation in ×.
    edestruct weak_simulation_step_star as [q'[??]]; jauto.
    ∃ q'; split; auto; ∃ R; auto.
  Qed.

  Lemma step_star_pbisim2: ∀ p q la q',
    step_star q la q' →
    par_bisimilar p q →
    (∃ p', step_star p la p' ∧ par_bisimilar p' q')
    ∨ (∃ r', step_star p la r' ∧ step_star q' nil r').
  Proof.
    introv H [R[H0 H1]]. unfold par_bisimulation in ×.
    edestruct par_simulation_step_star as [[p'[??]] | [r'[??]]]; jauto.
    left; ∃ p'; split; auto; ∃ R; auto.
  Qed.

  Lemma tstep_pbisim2: ∀ p q q',
    tstep q q' →
    par_bisimilar p q →
    (∃ p', step_star p nil p' ∧ par_bisimilar p' q')
    ∨ (∃ r', step_star p nil r' ∧ step_star q' nil r').
  Proof.
    intros.
    edestruct step_star_pbisim2 as [ [p'[??]] | [r'[??]] ]; eauto.
    apply single_tstep; auto.
  Qed.

  Lemma lstep_pbisim2: ∀ p q a q',
    lstep q a q' →
    par_bisimilar p q →
    (∃ p', step_star p [a] p' ∧ par_bisimilar p' q')
    ∨ (∃ r', step_star p [a] r' ∧ step_star q' nil r').
  Proof.
    intros.
    edestruct step_star_pbisim2 as [ [p'[??]] | [r'[??]] ]; eauto.
    apply single_lstep; auto.
  Qed.

  Lemma halted_pbisim1: ∀ p q,
    is_halted p →
    par_bisimilar p q →
    step_star q nil p.
  Proof.
    introv ? [R[H0 ?]]; unfold par_bisimulation in ×.
    eapply one_way_termination_sensitive_halted with (R:=R); jauto.
  Qed.

  Lemma halted_pbisim2: ∀ p q,
    is_halted q →
    par_bisimilar p q →
    step_star p nil q.
  Proof.
    introv ? [R[H0 ?]]; unfold par_bisimulation in ×.
    eapply one_way_termination_sensitive_halted with (R:=inv R); jauto.
  Qed.

  Lemma halted_converge_pbisim1: ∀ p q la p',
    step_star p la p' →
    is_halted p' →
    par_bisimilar p q →
    step_star q la p'.
  Proof.
    intros.
    edestruct step_star_pbisim1 as [q'[??]]; eauto.
    apply halted_pbisim1 in H3; subst; auto.
    replace la with (la++(@nil lts_L)).
    eapply step_star_app; eauto.
    apply app_nil_r.
  Qed.

  Lemma halted_converge_pbisim2: ∀ p q la q',
    step_star q la q' →
    is_halted q' →
    par_bisimilar p q →
    step_star p la q'.
  Proof.
    intros.
    edestruct step_star_pbisim2 as [[p'[??]] | [r'[??]]]; eauto.
    rewrite<- (List.app_nil_r la).
    eapply step_star_app; eauto.
    apply halted_pbisim2; auto.
    apply tstep_star_halted_resolve in H3; subst; auto.
  Qed.


  Definition eventual_simulation {lts: labeled_transition_system} (R:lts_S→lts_S→Prop) : Prop :=
    ∀ p q, R p q →
    ∀ la p',
      step_star p la p' →
      (∃ p'' q'', step_star p' nil p'' ∧ step_star q la q'' ∧ R p'' q'').

  Definition eventually_similar {lts: labeled_transition_system} p q :=
    ∃ R,
      one_way_termination_sensitive R ∧ one_way_termination_sensitive (inv R) ∧
      weak_simulation R ∧ eventual_simulation (inv R) ∧
      R p q.

  Definition eventually_bisimilar {lts: labeled_transition_system} p q :=
    ∃ R,
      one_way_termination_sensitive R ∧ one_way_termination_sensitive (inv R) ∧
      eventual_simulation R ∧ eventual_simulation (inv R) ∧
      R p q.

  Lemma eventual_simulation_step_star: ∀ p q R la p',
    eventual_simulation R → R p q →
    step_star p la p' →
    ∃ p'' q'', step_star p' nil p'' ∧ step_star q la q'' ∧ R p'' q''.
  Proof. intros; eapply H; eauto. Qed.

  Lemma eventual_simulation_tstep: ∀ p q R p',
    eventual_simulation R → R p q →
    tstep p p' →
    ∃ p'' q'', step_star p' nil p'' ∧ step_star q nil q'' ∧ R p'' q''.
  Proof. intros; eapply eventual_simulation_step_star; eauto; apply single_tstep; auto. Qed.

  Lemma eventual_simulation_lstep: ∀ p q R p' a,
    eventual_simulation R → R p q →
    lstep p a p' →
    ∃ p'' q'', step_star p' nil p'' ∧ step_star q [a] q'' ∧ R p'' q''.
  Proof. intros; eapply eventual_simulation_step_star; eauto; apply single_lstep; auto. Qed.

  Lemma par_eventual_simulation: ∀ (R: lts_S→lts_S→Prop),
    (∀ p, R p p) →
    par_simulation R → eventual_simulation R.
  Proof.
    intros.
    intros p q; intros.
    edestruct par_simulation_step_star as [ [q'[??]] | [r'[??]] ]; eauto.
    × ∃ p' q'; splits; auto; apply step_nil.
  Qed.

  Lemma weak_eventual_simulation: ∀ (R: lts_S→lts_S→Prop),
    weak_simulation R → eventual_simulation R.
  Proof.
    intros.
    intros p q; intros.
    edestruct weak_simulation_step_star as [q'[??]]; eauto.
    ∃ p' q'; splits; auto; apply step_nil.
  Qed.

  Lemma esim_refl: ∀ p,
    eventually_similar p p.
  Proof.
    intros.
    ∃ (fun (p q:lts_S) ⇒ p=q); splits; unfold inv; auto.
    apply one_way_termination_sensitive_id; auto.
    apply one_way_termination_sensitive_id; auto.
    apply weak_simulation_id; reflexivity.
    apply weak_eventual_simulation.
    apply weak_simulation_id; unfold inv; intros; iauto.
  Qed.

  Lemma ebisim_refl: ∀ p,
    eventually_bisimilar p p.
  Proof.
    intros.
    ∃ (fun (p q:lts_S) ⇒ p=q); splits; unfold inv; auto.
    apply one_way_termination_sensitive_id; auto.
    apply one_way_termination_sensitive_id; auto.
    apply weak_eventual_simulation.
    apply weak_simulation_id; reflexivity.
    apply weak_eventual_simulation.
    apply weak_simulation_id; unfold inv; intros; iauto.
  Qed.

  Lemma esim_ebisim1: ∀ p q,
    eventually_similar p q → eventually_bisimilar p q.
  Proof.
    introv [R[?[?[?[??]]]]].
    ∃ R; splits; auto.
    apply weak_eventual_simulation; auto.
  Qed.

  Lemma esim_ebisim2: ∀ p q,
    eventually_similar q p → eventually_bisimilar p q.
  Proof.
    introv [R[?[?[?[??]]]]].
    ∃ (inv R); splits; unfold inv in *; auto; clear p q H3.
    apply weak_eventual_simulation; auto.
  Qed.

  Lemma esim_one_way_termination_sensitive: ∀ (R: lts_S→lts_S→Prop),
    (∀ p q, R p q → eventually_similar p q) → one_way_termination_sensitive R.
  Proof. red; intros; apply H in H0; destruct H0 as [R'[?[?[?[??]]]]]; eauto. Qed.

  Lemma ebisim_one_way_termination_sensitive1: ∀ (R: lts_S→lts_S→Prop),
    (∀ p q, R p q → eventually_bisimilar p q) → one_way_termination_sensitive R.
  Proof. red; intros; apply H in H0; destruct H0 as [R'[?[?[?[??]]]]]; eauto. Qed.

  Lemma ebisim_one_way_termination_sensitive2: ∀ (R: lts_S→lts_S→Prop),
    (∀ p q, R q p → eventually_bisimilar p q) → one_way_termination_sensitive R.
  Proof. red; intros; apply H in H0; destruct H0 as [R'[?[?[?[??]]]]]; eauto. Qed.

  Lemma ebisim_eventual_simulation1: ∀ (R: lts_S→lts_S→Prop),
    (∀ p q, R p q ↔ eventually_bisimilar p q) → eventual_simulation R.
  Proof.
    unfold eventual_simulation; intros; apply H in H0; destruct H0 as [R'[?[?[?[??]]]]].
    edestruct eventual_simulation_step_star with (R:=R') as [p''[q''[?[??]]]]; eauto.
    ∃ p'' q''; splits; auto. apply H. ∃ R'; split; auto.
  Qed.

  Lemma ebisim_eventual_simulation2: ∀ (R: lts_S→lts_S→Prop),
    (∀ p q, R q p ↔ eventually_bisimilar p q) → eventual_simulation R.
  Proof.
    unfold eventual_simulation; intros; apply H in H0; destruct H0 as [R'[?[?[?[??]]]]].
    edestruct eventual_simulation_step_star with (R:=inv R') as [p''[q''[?[??]]]]; eauto.
    ∃ p'' q''; splits; auto. apply H. ∃ R'; split; auto.
  Qed.

  Lemma esim_weak_simulation: ∀ (R: lts_S→lts_S→Prop),
    (∀ p q, R p q ↔ eventually_similar p q) → weak_simulation R.
  Proof.
    split; intros; apply H in H0; destruct H0 as [R'[?[?[?[??]]]]].
    edestruct weak_simulation_tstep with (R:=R') as [q'[??]]; eauto.
    ∃ q'; split; auto. apply H. ∃ R'; split; auto.
    edestruct weak_simulation_lstep with (R:=R') as [q'[??]]; eauto.
    ∃ q'; split; auto. apply H. ∃ R'; split; auto.
  Qed.

  Lemma esim_par_simulation: ∀ (R: lts_S→lts_S→Prop),
    (∀ p q, R q p ↔ eventually_similar p q) → eventual_simulation R.
  Proof.
    unfold eventual_simulation; intros; apply H in H0; destruct H0 as [R'[?[?[?[??]]]]].
    edestruct eventual_simulation_step_star with (R:=inv R') as [p''[q''[?[??]]]]; eauto.
    ∃ p'' q''; splits; auto. apply H. ∃ R'; split; auto.
  Qed.

  Lemma ebisim_symm: ∀ p q,
    eventually_bisimilar q p → eventually_bisimilar p q.
  Proof.
    intros.
    ∃ (fun (p q:lts_S) ⇒ eventually_bisimilar q p); splits; unfold inv; auto; clear p q H.
    apply ebisim_one_way_termination_sensitive2; auto.
    apply ebisim_one_way_termination_sensitive1; auto.
    apply ebisim_eventual_simulation2; reflexivity.
    apply ebisim_eventual_simulation1; reflexivity.
  Qed.

  Lemma pbisim_esim: ∀ p q,
    par_bisimilar p q →
    eventually_similar p q.
  Proof.
    intros.
    ∃ par_bisimilar.
    splits; auto; clear p q H; unfold inv in ×.
    apply pbisim_one_way_termination_sensitive1; auto.
    apply pbisim_one_way_termination_sensitive2; auto.
    apply pbisim_weak_simulation; reflexivity.
    apply par_eventual_simulation; intros. apply pbisim_refl.
    apply pbisim_par_simulation; reflexivity.
  Qed.

  Lemma pbisim_ebisim: ∀ p q,
    par_bisimilar p q →
    eventually_bisimilar p q.
  Proof.
    intros.
    apply esim_ebisim1.
    apply pbisim_esim; auto.
  Qed.

  Lemma wbisim_esim: ∀ p q,
    wbisimilar p q →
    eventually_similar p q.
  Proof. intros; apply pbisim_esim; apply wbisim_pbisim; auto. Qed.

  Lemma wbisim_ebisim: ∀ p q,
    wbisimilar p q →
    eventually_bisimilar p q.
  Proof. intros; apply pbisim_ebisim; apply wbisim_pbisim; auto. Qed.

  Lemma tstep_esim1: ∀ p q p',
    tstep p p' →
    eventually_similar p q →
    ∃ q', step_star q nil q' ∧ eventually_similar p' q'.
  Proof.
    introv H [R[H0 H1]]. unfold eventual_simulation in ×.
    edestruct weak_simulation_tstep as [q'[??]]; jauto.
    ∃ q'; split; auto; ∃ R; splits; jauto.
  Qed.

  Lemma lstep_esim1: ∀ p q a p',
    lstep p a p' →
    eventually_similar p q →
    ∃ q', step_star q [a] q' ∧ eventually_similar p' q'.
  Proof.
    introv H [R[H0 H1]]. unfold eventual_simulation in ×.
    edestruct weak_simulation_lstep as [q'[??]]; jauto.
    ∃ q'; split; auto; ∃ R; splits; jauto.
  Qed.

  Lemma step_star_esim1: ∀ p q la p',
    step_star p la p' →
    eventually_similar p q →
    ∃ q', step_star q la q' ∧ eventually_similar p' q'.
  Proof.
    introv H [R[H0 H1]]; unfold eventual_simulation in ×.
    edestruct weak_simulation_step_star as [q'[??]]; jauto.
    ∃ q'; split; auto; ∃ R; splits; jauto.
  Qed.

  Lemma step_star_esim2: ∀ p q la q',
    step_star q la q' →
    eventually_similar p q →
    ∃ p'' q'', step_star p la p'' ∧ step_star q' nil q'' ∧ eventually_similar p'' q''.
  Proof.
    introv H [R[H0 H1]]. unfold eventual_simulation in ×.
    edestruct eventual_simulation_step_star as [q''[p''[?[??]]]]; jauto.
    ∃ p'' q''; splits; auto; ∃ R; splits; jauto.
  Qed.

  Lemma tstep_esim2: ∀ p q q',
    tstep q q' →
    eventually_similar p q →
    ∃ p'' q'', step_star p nil p'' ∧ step_star q' nil q'' ∧ eventually_similar p'' q''.
  Proof.
    intros.
    edestruct step_star_esim2 as [q''[p''[?[??]]]]; eauto.
    apply single_tstep; auto.
  Qed.

  Lemma lstep_esim2: ∀ p q a q',
    lstep q a q' →
    eventually_similar p q →
    ∃ p'' q'', step_star p [a] p'' ∧ step_star q' nil q'' ∧ eventually_similar p'' q''.
  Proof.
    intros.
    edestruct step_star_esim2 as [q''[p''[?[??]]]]; eauto.
    apply single_lstep; auto.
  Qed.

  Lemma halted_esim1: ∀ p q,
    is_halted p →
    eventually_similar p q →
    step_star q nil p.
  Proof.
    introv ? [R[H0 ?]]; unfold eventual_simulation in ×.
    eapply one_way_termination_sensitive_halted with (R:=R); jauto.
  Qed.

  Lemma halted_esim2: ∀ p q,
    is_halted q →
    eventually_similar p q →
    step_star p nil q.
  Proof.
    introv ? [R[H0 ?]]; unfold eventual_simulation in ×.
    eapply one_way_termination_sensitive_halted with (R:=inv R); jauto.
  Qed.

  Lemma halted_converge_esim1: ∀ p q la p',
    step_star p la p' →
    is_halted p' →
    eventually_similar p q →
    step_star q la p'.
  Proof.
    intros.
    edestruct step_star_esim1 as [q'[??]]; eauto.
    apply halted_esim1 in H3; subst; auto.
    replace la with (la++(@nil lts_L)).
    eapply step_star_app; eauto.
    apply app_nil_r.
  Qed.

  Lemma halted_converge_esim2: ∀ p q la q',
    step_star q la q' →
    is_halted q' →
    eventually_similar p q →
    step_star p la q'.
  Proof.
    intros.
    edestruct step_star_esim2 as [q''[p''[?[??]]]]; eauto.
    rewrite<- (List.app_nil_r la).
    eapply step_star_app; eauto.
    apply halted_esim2; auto.
    apply tstep_star_halted_resolve in H3; subst; auto.
  Qed.

  Lemma step_star_ebisim1: ∀ p q la p',
    step_star p la p' →
    eventually_bisimilar p q →
    ∃ p'' q'', step_star p' nil p'' ∧ step_star q la q'' ∧ eventually_bisimilar p'' q''.
  Proof.
    introv H [R ?].
    edestruct eventual_simulation_step_star with (R:=R) (p:=p) as [p''[q''[?[??]]]]; jauto.
    ∃ p'' q''; splits; auto; ∃ R; splits; jauto.
  Qed.

  Lemma tstep_ebisim1: ∀ p q p',
    tstep p p' →
    eventually_bisimilar p q →
    ∃ p'' q'', step_star p' nil p'' ∧ step_star q nil q'' ∧ eventually_bisimilar p'' q''.
  Proof.
    intros.
    edestruct step_star_ebisim1 as [p''[q''[?[??]]]]; eauto.
    apply single_tstep; auto.
  Qed.

  Lemma lstep_ebisim1: ∀ p q a p',
    lstep p a p' →
    eventually_bisimilar p q →
    ∃ p'' q'', step_star p' nil p'' ∧ step_star q [a] q'' ∧ eventually_bisimilar p'' q''.
  Proof.
    intros.
    edestruct step_star_ebisim1 as [p''[q''[?[??]]]]; eauto.
    apply single_lstep; auto.
  Qed.

  Lemma step_star_ebisim2: ∀ p q la q',
    step_star q la q' →
    eventually_bisimilar p q →
    ∃ p'' q'', step_star p la p'' ∧ step_star q' nil q'' ∧ eventually_bisimilar p'' q''.
  Proof.
    introv H [R ?].
    edestruct eventual_simulation_step_star as [q''[p''[?[??]]]]; jauto.
    ∃ p'' q''; splits; auto; ∃ R; splits; jauto.
  Qed.

  Lemma tstep_ebisim2: ∀ p q q',
    tstep q q' →
    eventually_bisimilar p q →
    ∃ p'' q'', step_star p nil p'' ∧ step_star q' nil q'' ∧ eventually_bisimilar p'' q''.
  Proof.
    intros.
    edestruct step_star_ebisim2 as [q''[p''[?[??]]]]; eauto.
    apply single_tstep; auto.
  Qed.

  Lemma lstep_ebisim2: ∀ p q a q',
    lstep q a q' →
    eventually_bisimilar p q →
    ∃ p'' q'', step_star p [a] p'' ∧ step_star q' nil q'' ∧ eventually_bisimilar p'' q''.
  Proof.
    intros.
    edestruct step_star_ebisim2 as [q''[p''[?[??]]]]; eauto.
    apply single_lstep; auto.
  Qed.

  Lemma halted_ebisim1: ∀ p q,
    is_halted p →
    eventually_bisimilar p q →
    step_star q nil p.
  Proof.
    introv ? [R ?].
    eapply one_way_termination_sensitive_halted with (R:=R); jauto.
  Qed.

  Lemma halted_ebisim2: ∀ p q,
    is_halted q →
    eventually_bisimilar p q →
    step_star p nil q.
  Proof.
    introv ? [R ?].
    eapply one_way_termination_sensitive_halted with (R:=inv R); jauto.
  Qed.

  Lemma halted_converge_ebisim1: ∀ p q la p',
    step_star p la p' →
    is_halted p' →
    eventually_bisimilar p q →
    step_star q la p'.
  Proof.
    intros.
    edestruct step_star_ebisim1 as [p''[q''[?[??]]]]; eauto.
    rewrite<- (List.app_nil_r la).
    eapply step_star_app; eauto.
    apply halted_ebisim1; auto.
    apply tstep_star_halted_resolve in H2; subst; auto.
  Qed.

  Lemma halted_converge_ebisim2: ∀ p q la q',
    step_star q la q' →
    is_halted q' →
    eventually_bisimilar p q →
    step_star p la q'.
  Proof.
    intros.
    edestruct step_star_ebisim2 as [q''[p''[?[??]]]]; eauto.
    rewrite<- (List.app_nil_r la).
    eapply step_star_app; eauto.
    apply halted_ebisim2; auto.
    apply tstep_star_halted_resolve in H3; subst; auto.
  Qed.

  Lemma esim_trans: ∀ p q r,
    eventually_similar p q →
    eventually_similar q r →
    eventually_similar p r.
  Proof.
    intros.
    ∃ (fun p r ⇒ ∃ q, eventually_similar p q ∧ eventually_similar q r).
    splits; eauto; clear p q r H H0; intros p r [q[??]]; intros.
    - change nil with (nil++(@nil lts_L)).
    eapply halted_converge_esim1; eauto.
    apply halted_esim1; auto.
    - change nil with (nil++(@nil lts_L)).
    eapply halted_converge_esim2; eauto.
    apply halted_esim2; auto.
    - split; intros.
    edestruct tstep_esim1 as [q'[??]]; eauto.
    edestruct step_star_esim1 with (p:=q) as [r'[??]]; eauto.
    edestruct lstep_esim1 as [q'[??]]; eauto.
    edestruct step_star_esim1 with (p:=q) as [r'[??]]; eauto.
    - edestruct step_star_esim2 as [q''[p''[?[??]]]]; eauto.
    edestruct step_star_esim2 with (q:=q) as [r'''[q'''[?[??]]]]; eauto.
    edestruct step_star_esim1 with (p:=q'') as [p'''[??]]; eauto.
    unfold inv; ∃ p''' r'''; splits; eauto.
    change nil with (nil++(@nil lts_L)).
    eapply step_star_app; eauto.
  Qed.


  Definition contrasimulation {lts: labeled_transition_system} (R:lts_S→lts_S→Prop) : Prop :=
    ∀ p q, R p q →
    (∀ la p',
      step_star p la p' →
      ∃ q',
        step_star q la q' ∧ R q' p').

  Definition partial_contrasimilar {lts: labeled_transition_system} p q := ∃ R,
    one_way_termination_sensitive R ∧ contrasimulation R ∧ R p q.
  Definition contrasimilar {lts: labeled_transition_system} p q := ∃ R,
    one_way_termination_sensitive R ∧
    contrasimulation R ∧
    R p q ∧ R q p.

  Lemma contrasimulation_step_star: ∀ R p q la p',
    contrasimulation R → R p q →
    step_star p la p' →
    ∃ q', step_star q la q' ∧ R q' p'.
  Proof. intros; eapply H; eauto. Qed.

  Lemma contrasimulation_tstep: ∀ R p q p',
    contrasimulation R → R p q →
    tstep p p' →
    ∃ q', step_star q nil q' ∧ R q' p'.
  Proof. intros; eapply H; eauto. apply single_tstep; auto. Qed.

  Lemma contrasimulation_lstep: ∀ R p q a p',
    contrasimulation R → R p q →
    lstep p a p' →
    ∃ q', step_star q [a] q' ∧ R q' p'.
  Proof. intros; eapply H; eauto. apply single_lstep; auto. Qed.

  Lemma contrasimulation_flip: ∀ R p q,
    contrasimulation R → R p q →
    ∃ q',
      step_star q nil q' ∧ R q' p.
  Proof.
    intros.
    edestruct contrasimulation_step_star as [q'[??]]; eauto.
    apply step_nil.
  Qed.

  Lemma contrasimulation_id: ∀ (R:lts_S→lts_S→Prop),
    (∀ p q, R p q ↔ p=q) → contrasimulation R.
  Proof.
    unfold contrasimulation; intros.
    apply H in H0; subst.
    ∃ p'; split; auto. apply H; auto.
  Qed.

  Lemma pcsim_refl: ∀ p,
    partial_contrasimilar p p.
  Proof.
    intros.
    ∃ (fun (p q:lts_S) ⇒ p=q); splits; auto.
    apply one_way_termination_sensitive_id; auto.
    apply contrasimulation_id; reflexivity.
  Qed.

  Lemma csim_refl: ∀ p,
    contrasimilar p p.
  Proof.
    intros.
    ∃ (fun (p q:lts_S) ⇒ p=q); splits; auto.
    apply one_way_termination_sensitive_id; auto.
    apply contrasimulation_id; reflexivity.
  Qed.

  Lemma step_star_pcsim: ∀ p q la p',
    step_star p la p' → partial_contrasimilar p q →
    ∃ q',
      step_star q la q' ∧ partial_contrasimilar q' p'.
  Proof.
    introv ? [R[?[??]]].
    edestruct contrasimulation_step_star as [q'[??]]; eauto.
    ∃ q'; split; auto. ∃ R; auto.
  Qed.

  Lemma tstep_pcsim: ∀ p q p',
    tstep p p' → partial_contrasimilar p q →
    ∃ q',
      step_star q nil q' ∧ partial_contrasimilar q' p'.
  Proof.
    intros.
    edestruct step_star_pcsim as [q'[??]]; eauto.
    apply single_tstep; auto.
  Qed.

  Lemma lstep_pcsim: ∀ p q a p',
    lstep p a p' → partial_contrasimilar p q →
    ∃ q',
      step_star q [a] q' ∧ partial_contrasimilar q' p'.
  Proof.
    intros.
    edestruct step_star_pcsim as [q'[??]]; eauto.
    apply single_lstep; auto.
  Qed.

  Lemma pcsim_contrasimulation: ∀ (R: lts_S→lts_S→Prop),
    (∀ p q, R p q ↔ partial_contrasimilar p q) → contrasimulation R.
  Proof.
    unfold contrasimulation; intros.
    apply H in H0.
    destruct H0 as [R'[?[??]]].
    edestruct contrasimulation_step_star with (R:=R') as [q'[??]]; eauto.
    ∃ q'; split; auto.
    apply H.
    ∃ R'; auto.
  Qed.

  Lemma flip_pcsim: ∀ p q,
    partial_contrasimilar p q →
    ∃ q',
      step_star q nil q' ∧ partial_contrasimilar q' p.
  Proof.
    intros; eapply contrasimulation_flip; eauto.
    apply pcsim_contrasimulation; reflexivity.
  Qed.

  Lemma halted_pcsim1: ∀ p q,
    is_halted p →
    partial_contrasimilar p q →
    step_star q nil p.
  Proof. introv ? [R[H0[??]]]; eapply H0; eauto. Qed.

  Lemma halted_pcsim2: ∀ p q,
    is_halted q →
    partial_contrasimilar p q →
    step_star p nil q.
  Proof.
    intros.
    edestruct flip_pcsim as [q'[??]]; eauto.
    apply tstep_star_halted_resolve in H1; auto. subst.
    eapply halted_pcsim1; auto.
  Qed.

  Lemma pcsim_one_way_termination_sensitive: ∀ (R: lts_S→lts_S→Prop),
    (∀ p q, R p q → partial_contrasimilar p q) → one_way_termination_sensitive R.
  Proof.
    red; intros; apply H in H0.
    apply halted_pcsim1; auto.
  Qed.

  Lemma pcsim_csim: ∀ p q,
    partial_contrasimilar p q → partial_contrasimilar q p → contrasimilar p q.
  Proof.
    intros.
    ∃ (fun p q ⇒ partial_contrasimilar p q).
    splits; eauto; clear p q H H0.
    apply pcsim_one_way_termination_sensitive; auto.
    apply pcsim_contrasimulation; reflexivity.
  Qed.

  Lemma csim_pcsim1: ∀ p q,
    contrasimilar p q → partial_contrasimilar p q.
  Proof. introv [R[?[?[??]]]]; ∃ R; auto. Qed.

  Lemma csim_pcsim2: ∀ p q,
    contrasimilar p q → partial_contrasimilar q p.
  Proof. introv [R[?[?[??]]]]; ∃ R; auto. Qed.

  Lemma halted_converge_pcsim: ∀ p q la p',
    step_star p la p' →
    is_halted p' →
    partial_contrasimilar p q →
    step_star q la p'.
  Proof.
    intros.
    edestruct step_star_pcsim as [q'[??]]; eauto.
    rewrite<- (app_nil_r la).
    eapply step_star_app; eauto.
    eapply halted_pcsim2; eauto.
  Qed.

  Lemma pcsim_trans: ∀ p q r,
    partial_contrasimilar p q →
    partial_contrasimilar q r →
    partial_contrasimilar p r.
  Proof.
    intros.
    ∃ (fun p r ⇒ ∃ q, partial_contrasimilar p q ∧ partial_contrasimilar q r).
    splits; jauto; clear p q r H H0; intros p r [q[??]]; intros.
    × change [] with ([]++@nil lts_L).
    eapply halted_converge_pcsim; eauto.
    eapply halted_pcsim1; auto.
    × edestruct step_star_pcsim as [q'[??]]; eauto.
    edestruct step_star_pcsim with (p:=q) as [r'[??]]; eauto.
  Qed.

  Lemma csim_trans: ∀ p q r,
    contrasimilar p q →
    contrasimilar q r →
    contrasimilar p r.
  Proof.
    intros.
    apply pcsim_csim.
    eapply pcsim_trans; apply csim_pcsim1; eauto.
    eapply pcsim_trans; apply csim_pcsim2; eauto.
  Qed.

  Lemma csim_symm: ∀ p q,
    contrasimilar p q →
    contrasimilar q p.
  Proof.
    intros p q [R[?[?[??]]]].
    ∃ R; auto.
  Qed.

  Lemma ebisim_csim: ∀ p q,
    eventually_bisimilar p q → contrasimilar p q.
  Proof.
    intros.
    ∃ (fun p q ⇒ (∃ q', step_star q nil q' ∧ eventually_bisimilar p q')).
    splits; auto.
    × clear p q H; intros p q [q'[??]]; intros.
    change [] with ([]++@nil lts_L).
    eapply step_star_app; eauto.
    apply halted_ebisim1; auto.
    × clear p q H; intros p q [q'[??]]; intros.
    edestruct step_star_ebisim1 as [p''[q''[?[??]]]]; eauto.
    ∃ q''; split; auto.
    change la with ([]++la).
    eapply step_star_app; eauto.
    ∃ p''; split; auto.
    apply ebisim_symm; auto.
    × ∃ q; split; auto; apply step_nil.
    × ∃ p; split. apply step_nil. apply ebisim_symm; auto.
  Qed.

  Lemma pbisim_csim: ∀ p q,
    par_bisimilar p q → contrasimilar p q.
  Proof. intros; apply ebisim_csim; apply pbisim_ebisim; auto. Qed.

  Lemma wbisim_csim: ∀ p q,
    wbisimilar p q → contrasimilar p q.
  Proof. intros; apply pbisim_csim; apply wbisim_pbisim; auto. Qed.

  Lemma wbisim_pcsim: ∀ p q,
    wbisimilar p q → partial_contrasimilar p q.
  Proof. intros; apply csim_pcsim1; apply wbisim_csim; auto. Qed.

  Lemma pcssim_pcsim: ∀ p q,
    partial_coupled_similar p q → partial_contrasimilar p q.
  Proof.
    intros.
    ∃ partial_coupled_similar.
    splits; auto; clear p q H.
    × apply pcssim_one_way_termination_sensitive; auto.
    × intros p q; intros.
    edestruct step_star_pcssim as [q'[??]]; eauto.
    edestruct flip_pcssim with (p:=p') as [q''[??]]; eauto.
    ∃ q''; split; auto.
    rewrite<- (app_nil_r la).
    eapply step_star_app; eauto.
  Qed.

  Lemma cssim_csim: ∀ p q,
    coupled_similar p q → contrasimilar p q.
  Proof.
    intros.
    apply pcsim_csim; apply pcssim_pcsim.
    apply cssim_pcssim1; auto.
    apply cssim_pcssim2; auto.
  Qed.

  Lemma contrasimulation_symm_weak_bisimulation: ∀ R,
    contrasimulation R →
    one_way_termination_sensitive R →
    (∀ p q, R p q → R q p) →
    weak_bisimulation R.
  Proof.
    intros.
    apply weak_bisimulation_symm; auto.
    intros p q; split; intros.
    × edestruct contrasimulation_tstep as [q'[??]]; eauto.
    × edestruct contrasimulation_lstep as [q'[??]]; eauto.
  Qed.

  Definition tstep_contrasimulation (R: lts_S→lts_S→Prop) : Prop :=
    one_way_termination_sensitive R ∧
    ∀ p q, R p q →
      (∀ p',
        tstep p p' →
        ∃ q',
          step_star q nil q' ∧ contrasimilar p' q') ∧
      (∀ a p',
        lstep p a p' →
        ∃ q',
          step_star q [a] q' ∧ R p' q') ∧
      R q p.

  Lemma pcsim_refl_step_star: ∀ p p',
    step_star p nil p' →
    partial_contrasimilar p' p.
  Proof.
    intros.
    ∃ (fun p q ⇒ step_star q nil p).
    splits; auto; clear p p' H; intros p q; intros; auto.
    ∃ p'; split.
    change la with ([]++la).
    eapply step_star_app; eauto.
    apply step_nil.
  Qed.

  Lemma pcsim_backward: ∀ q0 p q,
    step_star q0 nil q →
    partial_contrasimilar p q →
    partial_contrasimilar p q0.
  Proof.
    intros.
    eapply pcsim_trans; eauto.
    apply pcsim_refl_step_star; auto.
  Qed.

  Lemma pcsim_forward: ∀ p q p',
    step_star p nil p' →
    partial_contrasimilar p q →
    partial_contrasimilar p' q.
  Proof.
    intros.
    eapply pcsim_trans; eauto.
    apply pcsim_refl_step_star; auto.
  Qed.

  Lemma pcsim_tstep: ∀ R p q,
    tstep_contrasimulation R →
    R p q →
    partial_contrasimilar p q.
  Proof.
    unfold tstep_contrasimulation; intros.
    destruct H.
    ∃ (fun p q ⇒ R p q ∨ partial_contrasimilar p q).
    splits; auto; clear p q H0.
    × intros p q [?|?]; intros; auto.
    apply halted_pcsim1; auto.
    × intros p q [?|?]; intros.
    - revert q H H1 H0; induction H2; intros.
    + ∃ q; split; auto. apply step_nil.
    left; apply H1; auto.
    + edestruct H1 as [_[? _]]; eauto.
    edestruct H4 as [q'[??]]; eauto.
    edestruct IHstep_star as [q''[??]]; eauto.
    ∃ q''; split; auto.
    change (a::la) with ([a]++la).
    eapply step_star_app; eauto.
    + edestruct H1 as [? _]; eauto.
    edestruct H4 as [q'[??]]; eauto.
    clear IHstep_star H3.
    edestruct step_star_pcsim with (la:=la) as [q''[??]]; eauto.
    eapply pcsim_backward; eauto.
    apply csim_pcsim1; auto.
    - edestruct step_star_pcsim as [q'[??]]; eauto.
  Qed.

  Lemma strong_pcsim_symm: ∀ p q,
    (∀ p p', tstep p p' → False) →
    partial_contrasimilar p q → partial_contrasimilar q p.
  Proof.
    intros.
    edestruct flip_pcsim as [q'[??]]; eauto.
    inverts H1; auto.
    false; eapply H; eauto.
  Qed.

  Definition deterministic_internal_choice:=
    ∀ p p', tstep p p' → wbisimilar p p'.

  Lemma step_star_det_internal_choice: ∀ p p',
    deterministic_internal_choice →
    step_star p nil p' →
    wbisimilar p p'.
  Proof.
    intros.
    remember (@nil lts_L) as la.
    revert Heqla.
    induction H0; intros; subst.
    × apply wbisim_refl.
    × false.
    × eapply wbisim_trans; eauto.
  Qed.

  Lemma det_internal_choice_pcsim_symm: ∀ p q,
    deterministic_internal_choice →
    partial_contrasimilar p q → partial_contrasimilar q p.
  Proof.
    intros.
    edestruct flip_pcsim as [q'[??]]; eauto.
    eapply pcsim_trans; eauto.
    apply wbisim_pcsim.
    eapply step_star_det_internal_choice; eauto.
  Qed.

  Lemma pcsim_symm_wbisim: ∀ p q,
    (∀ p q, partial_contrasimilar p q → partial_contrasimilar q p) →
    partial_contrasimilar p q →
    wbisimilar p q.
  Proof.
    intros.
    ∃ partial_contrasimilar.
    split; auto.
    clear p q H0.
    apply weak_bisimulation_symm.
    × apply pcsim_one_way_termination_sensitive; auto.
    × intros p q; split; intros.
    - edestruct tstep_pcsim as [q'[??]]; eauto.
    - edestruct lstep_pcsim as [q'[??]]; eauto.
    × intros; auto.
  Qed.

  Lemma det_internal_choice_pcsim_wbisim: ∀ p q,
    deterministic_internal_choice →
    partial_contrasimilar p q → wbisimilar q p.
  Proof.
    intros.
    ∃ partial_contrasimilar.
    split.
    × clear p q H0.
    apply contrasimulation_symm_weak_bisimulation.
    - apply pcsim_contrasimulation; reflexivity.
    - apply pcsim_one_way_termination_sensitive; auto.
    - intros. apply det_internal_choice_pcsim_symm; auto.
    × apply det_internal_choice_pcsim_symm; auto.
  Qed.

  Lemma det_internal_choice_csim_wbisim: ∀ p q,
    deterministic_internal_choice →
    contrasimilar p q → wbisimilar q p.
  Proof.
    intros.
    apply det_internal_choice_pcsim_wbisim; auto.
    apply csim_pcsim1; auto.
  Qed.

  Lemma strong_csim_wbisim: ∀ p q,
    (∀ p p', tstep p p' → False) →
    contrasimilar p q → wbisimilar p q.
  Proof.
    intros.
    eapply det_internal_choice_pcsim_wbisim; eauto.
    clear p q H0.
    intros p q ?.
    false. eauto.
    apply csim_pcsim2; auto.
  Qed.


  Definition stable_bisimulation {lts: labeled_transition_system} (R: lts_S→lts_S→Prop) : Prop :=
    one_way_termination_sensitive R ∧ one_way_termination_sensitive (inv R) ∧
    ∀ p q, R p q →
    (∀ la p',
      step_star p la p' → stable lts p' → ∃ q', step_star q la q' ∧ R p' q') ∧
    (∀ la q',
      step_star q la q' → stable lts q' → ∃ p', step_star p la p' ∧ R p' q').

  Lemma csim_stable_bisim: ∀ p q,
    contrasimilar p q → ∃ R, stable_bisimulation R ∧ R p q.
  Proof.
    intros.
    ∃ contrasimilar.
    split; auto.
    clear p q H.
    splits.
    × apply pcsim_one_way_termination_sensitive.
    intros. apply csim_pcsim1; auto.
    × apply pcsim_one_way_termination_sensitive.
    unfold inv; intros. apply csim_pcsim2; auto.
    × intros p q ?.
    split; intros.
    - edestruct step_star_pcsim as [q'[??]]; eauto.
    apply csim_pcsim1; eauto.
    edestruct flip_pcsim with (p:=q') as [p''[??]]; eauto.
    inverts H4.
    ∃ q'; split; auto.
    apply pcsim_csim; auto.
    apply H1 in H6. false.
    - edestruct step_star_pcsim as [p'[??]]; eauto.
    apply csim_pcsim2; eauto.
    edestruct flip_pcsim with (p:=p') as [q''[??]]; eauto.
    inverts H4.
    ∃ p'; split; auto.
    apply pcsim_csim; auto.
    apply H1 in H6. false.
  Qed.

End Bisimulation.


Section TraceEquivalence.
  Variable lts: labeled_transition_system.
  Import Stepping.

  Definition trace_equivalent (p q: lts_S):=
    (∀ p' la, step_star p la p' → ∃ q', step_star q la q') ∧
    (∀ q' la, step_star q la q' → ∃ p', step_star p la p').

  Lemma csim_trace_equivalent: ∀ p q,
    contrasimilar p q → trace_equivalent p q.
  Proof.
    split; intros.
    × edestruct step_star_pcsim as [q'[??]]; eauto.
    apply csim_pcsim1; eauto.
    × edestruct step_star_pcsim as [p'[??]]; eauto.
    apply csim_pcsim2; eauto.
  Qed.

End TraceEquivalence.