Section TS.

Variable process action : Set.
Variable T : action.
Variable transition : process → action → process → Prop.
Hypothesis eqT_dec : ∀ a : action, a = T ∨ a ≠ T.


Inductive weak_derivative : process → action → process → Prop :=
  | eps : ∀ p : process, weak_derivative p T p
  | w_single :
      ∀ (a : action) (p q : process),
      transition p a q → weak_derivative p a q
  | w_tau_left :
      ∀ (a : action) (p p' q : process),
      transition p T p' → weak_derivative p' a q → weak_derivative p a q
  | w_tau_right :
      ∀ (a : action) (p q q' : process),
      transition q' T q → weak_derivative p a q' → weak_derivative p a q.
Hint Resolve w_single eps.

Inductive derivative : process → action → process → Prop :=
  | single :
      ∀ (a : action) (p q : process),
      transition p a q → derivative p a q
  | tau_left :
      ∀ (a : action) (p p' q : process),
      transition p T p' → derivative p' a q → derivative p a q
  | tau_right :
      ∀ (a : action) (p q q' : process),
      transition q' T q → derivative p a q' → derivative p a q.

Hint Resolve single.

Lemma deriv_weak_deriv :
 ∀ (p p' : process) (a : action),
 derivative p a p' → weak_derivative p a p'.

intros p p' a H; elim H; clear H; auto with v62.
clear p p' a.
intros a p p' q tr de we.
apply w_tau_left with p'; try trivial with v62.

clear p p' a; intros a p q q' tr de we.
apply w_tau_right with q'; try trivial with v62.

Qed.

Hint Resolve deriv_weak_deriv.

Lemma weak_deriv_deriv :
 ∀ (p p' : process) (a : action),
 weak_derivative p a p' → a ≠ T → derivative p a p'.
intros p p' a H; elim H; clear H p p' a.
unfold not in |- ×.
intros p H; cut False; auto with v62.
intros H1; elim H1.

intros a p q tr H; auto with v62.

intros a p p' q tr we H_ind not_eq.
apply tau_left with p'; auto with v62.

intros a p q q' tr we H_ind notEq.
apply tau_right with q'; auto with v62.
Qed.

Hint Resolve weak_deriv_deriv.

Lemma weak_deriv_tau_left :
 ∀ (p p' p'' : process) (a : action),
 weak_derivative p T p' →
 weak_derivative p' a p'' → weak_derivative p a p''.

cut
 (∀ (p : process) (a : action) (p' : process),
  weak_derivative p a p' →
  a = T →
  ∀ (p'' : process) (b : action),
  weak_derivative p' b p'' → weak_derivative p b p'').
intros H p p' p'' a we we'; apply (H p T p'); auto with v62.

simple induction 1.
simple induction 1; auto with v62.

clear H p' a p.
intros a p q Tpq eqT p'' b we.
rewrite eqT in Tpq.
apply w_tau_left with q; auto with v62.

clear H p p' a.
intros a p p' q Tpq we H_rec eqT p'' b we'.
apply w_tau_left with p'; auto with v62.

clear H p a p'.
intros a p q q' Tr we H_rec eqT p'' b we'.
apply (H_rec eqT).
apply w_tau_left with q; auto with v62.

Qed.

Lemma weak_deriv_tau_right :
 ∀ (p p' p'' : process) (a : action),
 weak_derivative p a p' →
 weak_derivative p' T p'' → weak_derivative p a p''.

cut
 (∀ (p' : process) (a : action) (p'' : process),
  weak_derivative p' a p'' →
  a = T →
  ∀ (p : process) (b : action),
  weak_derivative p b p' → weak_derivative p b p'').
intros H p p' p'' a we we1; apply (H p' T p''); auto with v62.

intros p' a p'' H; elim H; clear H a p' p''; auto with v62.
intros a p q tr eqT p0 b we.
apply w_tau_right with p; auto with v62.
rewrite eqT in tr; auto with v62.

intros a p q q' tr we H_rec eqT p0 b we'.
apply (H_rec eqT).
apply w_tau_right with p; auto with v62.

intros a p q q' tr we H_rec eqT p0 b we'.
apply w_tau_right with q'; auto with v62.

Qed.

Lemma w_deriv_tau_left :
 ∀ (p p' p'' : process) (a : action),
 weak_derivative p T p' → derivative p' a p'' → derivative p a p''.

cut
 (∀ (p : process) (a : action) (p' : process),
  weak_derivative p a p' →
  a = T →
  ∀ (p'' : process) (b : action),
  derivative p' b p'' → derivative p b p'').
intros H p p' p'' a de de1; apply (H p T p'); auto with v62.

intros p a p' H; elim H; clear H a p p'; auto with v62.
intros a p q Tpq eqT p'' b de.
rewrite eqT in Tpq.
apply tau_left with q; auto with v62.

intros a p p' q tr de H_ind eqT p'' d de'.
apply tau_left with p'; auto with v62.

intros a p q q' Tr de H_ind eqT p'' b de'.
apply (H_ind eqT).
apply tau_left with q; auto with v62.

Qed.

Lemma w_deriv_tau_right :
 ∀ (p p' p'' : process) (a : action),
 derivative p a p' → weak_derivative p' T p'' → derivative p a p''.

cut
 (∀ (p' : process) (a : action) (p'' : process),
  weak_derivative p' a p'' →
  a = T →
  ∀ (p : process) (b : action), derivative p b p' → derivative p b p'').
intros H p p' p'' a de de1; apply (H p' T p''); auto with v62.

intros p' a p'' H; elim H; clear H a p' p''.
auto with v62.

intros a p q tr eqT p0 b we.
apply tau_right with p; auto with v62.
rewrite eqT in tr; auto with v62.

intros a p q q' tr we H_rec eqT p0 b we'.
apply (H_rec eqT).
apply tau_right with p; auto with v62.

intros a p q q' tr we H_rec eqT p0 b we'.
apply tau_right with q'; auto with v62.

Qed.

Lemma deriv_tau_left :
 ∀ (p p' p'' : process) (a : action),
 derivative p T p' → derivative p' a p'' → derivative p a p''.

intros p p' p'' a pp' p_p''.
apply w_deriv_tau_left with p'; auto with v62.
Qed.

Lemma deriv_tau_right :
 ∀ (p p' p'' : process) (a : action),
 derivative p a p' → derivative p' T p'' → derivative p a p''.

intros p p' p'' a de1 de2.
apply w_deriv_tau_right with p'; auto with v62.
Qed.


CoInductive strong_eq : process → process → Prop :=
    str_eq :
      ∀ p q : process,
      (∀ (a : action) (p' : process),
       transition p a p' →
       ∃ q' : process, transition q a q' ∧ strong_eq p' q') →
      (∀ (a : action) (q' : process),
       transition q a q' →
       ∃ p' : process, transition p a p' ∧ strong_eq p' q') →
      strong_eq p q.


Lemma refl_strong_eq : ∀ p : process, strong_eq p p.
cofix.
intros p; apply str_eq.
intros a p' trans; ∃ p'; split; auto with v62.
intros a p' trans; ∃ p'; split; auto with v62.
Qed.

Hint Resolve refl_strong_eq.

Lemma sym_strong_eq : ∀ p q : process, strong_eq p q → strong_eq q p.
cofix.
intros p q H; inversion_clear H.
apply str_eq.
intros a q'.
intros trans.
elim (H1 a q' trans); clear H1.
intros p' H; elim H; ∃ p'; split; auto with v62.
intros a p' trans.
elim (H0 a p' trans); clear H0.
intros q' H; elim H; clear H.
intros trans1 str.
∃ q'; split; auto with v62.
Qed.

Hint Immediate sym_strong_eq.

Lemma trans_strong_eq :
 ∀ p q r : process, strong_eq p q → strong_eq q r → strong_eq p r.

cofix.
intros p q r pq qr.
inversion_clear pq; inversion_clear qr.
apply str_eq.
intros a p' tp.
cut (∃ q' : process, transition q a q' ∧ strong_eq p' q').
intros G; elim G; clear G.
intros q' G; elim G.
intros tq pq'; elim (H1 a q' tq).
clear G.
intros r' G; elim G; clear G.
intros tr qr'; ∃ r'; split; auto with v62.
apply trans_strong_eq with q'; auto with v62.
elim (H a p' tp).
intros q' G; elim G; clear G.
intros tq pq'.
∃ q'; split; auto with v62.
intros a r' tr.
cut (∃ q' : process, transition q a q' ∧ strong_eq q' r').
intros G; elim G; clear G.
intros q' G; elim G; clear G.
intros tq qr'.
elim (H0 a q' tq).
intros p' G; elim G; clear G.
intros tp pq'; ∃ p'; split; auto with v62.
apply trans_strong_eq with q'; auto with v62.
elim (H2 a r' tr).
intros q' G; elim G; clear G.
intros tq qr'; ∃ q'; split; auto with v62.
Qed.


CoInductive weak_eq : process → process → Prop :=
    w_eq :
      ∀ p q : process,
      (∀ (a : action) (p' : process),
       transition p a p' →
       ∃ q' : process, weak_derivative q a q' ∧ weak_eq p' q') →
      (∀ (a : action) (q' : process),
       transition q a q' →
       ∃ p' : process, weak_derivative p a p' ∧ weak_eq p' q') →
      weak_eq p q.


Lemma refl_weak_eq : ∀ p : process, weak_eq p p.
cofix.
intros p; apply w_eq.
intros a p' trans; ∃ p'; split; auto with v62.
intros a p' trans; ∃ p'; split; auto with v62.
Qed.

Hint Resolve refl_weak_eq.

Lemma sym_weak_eq : ∀ p q : process, weak_eq p q → weak_eq q p.
cofix.
intros p q H; inversion_clear H.
apply w_eq.
intros a q'.
intros trans.
elim (H1 a q' trans); clear H1.
intros p' H; elim H; ∃ p'; split; auto with v62.
intros a p' trans.
elim (H0 a p' trans); clear H0.
intros q' H; elim H; clear H.
intros trans1 str.
∃ q'; split; auto with v62.
Qed.

Hint Immediate sym_weak_eq.


Remark Hint_Trans :
 ∀ (q q' r : process) (a : action),
 weak_derivative q a q' →
 weak_eq q r → ∃ r' : process, weak_derivative r a r' ∧ weak_eq q' r'.

intros q q' r a H.
generalize r; clear r.
elim H; clear H.
intros p r we; ∃ r; split; auto with v62.

clear a q q'; intros a p q tr r we.
inversion_clear we.
apply (H a q tr).

clear q q' a; intros a p p' q tr wd H_ind r we.
cut (∃ r'' : process, weak_derivative r T r'' ∧ weak_eq p' r'').
intros H.
elim H; clear H.
intros r'' Hr''; elim Hr''; clear Hr''; intros rTr'' we'.
cut (∃ r' : process, weak_derivative r'' a r' ∧ weak_eq q r').
intros H; elim H; clear H.
intros r' Hr'; elim Hr'; clear Hr'; intros wde we''.
∃ r'; split; auto with v62.
apply (weak_deriv_tau_left r r'' r' a); auto with v62.

apply (H_ind r''); auto with v62.

inversion_clear we.
apply (H T p' tr); auto with v62.

clear q q' a; intros a p q q' tr wd H_ind r we.
cut (∃ r'' : process, weak_derivative r a r'' ∧ weak_eq q' r'').
intros H; elim H; clear H.
intros r'' Hr''; elim Hr''; clear Hr''; intros wd' we'.
cut (∃ r' : process, weak_derivative r'' T r' ∧ weak_eq q r').
intros H; elim H; clear H.
intros r' Hr'; elim Hr'; intros wd'' we''.
∃ r'; split; auto with v62.
apply (weak_deriv_tau_right r r'' r' a); auto with v62.

inversion_clear we'; auto with v62.

apply (H_ind r we); auto with v62.

Qed.

Lemma trans_weak_eq :
 ∀ p q r : process, weak_eq p q → weak_eq q r → weak_eq p r.
cofix.
intros p q r pq qr.
apply w_eq.

intros a p' tr.
cut (∃ q' : process, weak_derivative q a q' ∧ weak_eq p' q').
intros H; elim H; clear H; intros q' Hq'; elim Hq'; clear Hq'; intros wd we.
cut (∃ r' : process, weak_derivative r a r' ∧ weak_eq q' r').
intros Hr'; elim Hr'; clear Hr'; intros r' Hr'; elim Hr'; clear Hr';
 intros wd' we'.
∃ r'; split; auto with v62.
apply trans_weak_eq with q'; auto with v62.
apply (Hint_Trans q q' r); auto with v62.
inversion_clear pq; auto with v62.

intros a r' tr.
cut (∃ q' : process, weak_derivative q a q' ∧ weak_eq q' r').
intros H; elim H; clear H; intros q' Hq'; elim Hq'; clear Hq'; intros wd we.
cut (∃ p' : process, weak_derivative p a p' ∧ weak_eq q' p').
intros H; elim H; clear H; intros p' Hp'; elim Hp'; clear Hp'; intros wd' we'.
∃ p'; split; auto with v62.
apply trans_weak_eq with q'; auto with v62.
apply (Hint_Trans q q' p a); auto with v62.
inversion_clear qr; auto with v62.
Qed.


CoInductive weak_eq1 : process → process → Prop :=
    w_eq1 :
      ∀ p q : process,
      (∀ (a : action) (p' : process),
       derivative p a p' →
       ∃ q' : process, weak_derivative q a q' ∧ weak_eq1 p' q') →
      (∀ (a : action) (q' : process),
       derivative q a q' →
       ∃ p' : process, weak_derivative p a p' ∧ weak_eq1 p' q') →
      weak_eq1 p q.

Lemma weak_eq_deriv :
 ∀ p q : process,
 weak_eq p q →
 ∀ (a : action) (p' : process),
 derivative p a p' →
 ∃ q' : process, weak_derivative q a q' ∧ weak_eq p' q'.

intros p q we a p' de.
generalize we.
generalize q.
elim de; clear de we a p p' q.
intros a p p' tr q we.
inversion we.
elim (H a p' tr); clear H H0.
intros q' H; elim H; clear H; intros wde we'.
∃ q'; split; assumption.

intros a p p1 p' tr de H_ind q we.
cut (∃ q1 : process, weak_derivative q T q1 ∧ weak_eq p1 q1).
intros H; elim H; clear H.
intros q1 H; elim H; clear H; intros wde we'.
cut (∃ q' : process, weak_derivative q1 a q' ∧ weak_eq p' q').
intros H; elim H; clear H.
intros q' H; elim H; clear H; intros wde1 we1.
∃ q'; split; try try try trivial with v62.
apply weak_deriv_tau_left with q1; try try trivial with v62.

apply (H_ind q1); try try trivial with v62.

inversion_clear we.
apply (H T p1); try try trivial with v62.

intros a p p' p1 tr de H_ind q we.
cut (∃ q1 : process, weak_derivative q a q1 ∧ weak_eq p1 q1).
intros H; elim H; clear H.
intros q1 H; elim H; clear H; intros wde we1.
cut (∃ q' : process, weak_derivative q1 T q' ∧ weak_eq p' q').
intros H; elim H; clear H.
intros q' H; elim H; clear H; intros wde1 we'.
∃ q'; split; try try try trivial with v62.
apply weak_deriv_tau_right with q1; try try trivial with v62.

inversion_clear we1.
apply (H T p'); try try trivial with v62.

apply (H_ind q we).
Qed.

Lemma weak_eq_deriv_sym :
 ∀ p q : process,
 weak_eq p q →
 ∀ (a : action) (q' : process),
 derivative q a q' →
 ∃ p' : process, weak_derivative p a p' ∧ weak_eq p' q'.

intros p q we a q' de.
cut (weak_eq q p); auto with v62.
intros we'.
elim (weak_eq_deriv q p we' a q' de).
intros p' H; elim H; intros w_de we''.
∃ p'; split; auto with v62.

Qed.

Lemma weak_eq1_weak_eq : ∀ p q : process, weak_eq1 p q → weak_eq p q.
cofix.
intros p q we1.
apply w_eq.
intros a p' tr.
inversion we1.
elim (H a p').
intros q' G; elim G; clear G; intros wde we1'.
∃ q'; split; try try try trivial with v62.
apply weak_eq1_weak_eq; assumption.

apply single; assumption.

intros a q' tr.
inversion we1.
elim (H0 a q').
intros p' G; elim G; intros wde we1'.
∃ p'; split; try try try trivial with v62.
apply weak_eq1_weak_eq; assumption.

apply single; try try trivial with v62.
Qed.

Hint Immediate weak_eq1_weak_eq.

Lemma weak_eq_weak_eq1 : ∀ p q : process, weak_eq p q → weak_eq1 p q.

cofix.
intros p q we.
apply w_eq1.
intros a p' de.
cut (∃ q' : process, weak_derivative q a q' ∧ weak_eq p' q').
intros H; elim H; clear H.
intros q' H; elim H; clear H; intros wde we'.
∃ q'; split; try try try trivial with v62.
apply weak_eq_weak_eq1; try try trivial with v62.

elim (weak_eq_deriv p q we a p' de).
intros q' H; ∃ q'; assumption.

intros a q' de.
cut (∃ p' : process, weak_derivative p a p' ∧ weak_eq p' q').
intros H; elim H; clear H.
intros p' H; elim H; clear H; intros wde we'.
∃ p'; split; try try try try trivial with v62.
apply weak_eq_weak_eq1; try try try trivial with v62.

elim (weak_eq_deriv_sym p q we a q' de).
intros p' H; ∃ p'; assumption.

Qed.

Hint Immediate weak_eq_weak_eq1.


Lemma refl_weak_eq1 : ∀ p : process, weak_eq1 p p.

auto with v62.
Qed.

Lemma sym_weak_eq1 : ∀ p q : process, weak_eq1 p q → weak_eq1 q p.

intros.
apply weak_eq_weak_eq1.
apply sym_weak_eq; auto with v62.

Qed.

Lemma trans_weak_eq1 :
 ∀ p q r : process, weak_eq1 p q → weak_eq1 q r → weak_eq1 p r.

intros p q r pq qr.
apply weak_eq_weak_eq1.
apply trans_weak_eq with q; auto with v62.

Qed.


Definition obs_eq (p q : process) : Prop :=
  (∀ (a : action) (p' : process),
   transition p a p' →
   ∃ q' : process, derivative q a q' ∧ weak_eq p' q') ∧
  (∀ (a : action) (q' : process),
   transition q a q' →
   ∃ p' : process, derivative p a p' ∧ weak_eq p' q').

Lemma refl_obs_eq : ∀ p : process, obs_eq p p.
unfold obs_eq in |- ×.
split; intros a p' trans; ∃ p'; split; auto with v62.
Qed.

Hint Immediate refl_obs_eq.

Lemma sym_obs_eq : ∀ p q : process, obs_eq p q → obs_eq q p.
unfold obs_eq in |- ×.
intros p q.
intros H; elim H; clear H; intros Hp Hq.
split.
auto with v62.
intros a q' tr.
elim (Hq a q' tr); clear Hq.
intros p' H; elim H; clear H; intros de we; ∃ p'; split; auto with v62.
intros a p' tr.
elim (Hp a p' tr); clear Hp.
intros q' H; elim H; clear H; intros de we; ∃ q'; split; auto with v62.
Qed.

Hint Immediate sym_obs_eq.


Definition obs_eq1 (p q : process) : Prop :=
  (∀ (a : action) (p' : process),
   derivative p a p' →
   ∃ q' : process, derivative q a q' ∧ weak_eq p' q') ∧
  (∀ (a : action) (q' : process),
   derivative q a q' →
   ∃ p' : process, derivative p a p' ∧ weak_eq p' q').

Lemma obs_eq1_obs_eq : ∀ p q : process, obs_eq1 p q → obs_eq p q.
intros p q oe.
unfold obs_eq in |- *; split; elim oe; auto with v62.
Qed.

Hint Resolve obs_eq1_obs_eq.

Remark half_obs_eq_obs_eq1 :
 ∀ p q : process,
 obs_eq p q →
 ∀ (a : action) (p' : process),
 derivative p a p' → ∃ q' : process, derivative q a q' ∧ weak_eq p' q'.

intros p q oe a p' de; generalize oe; generalize q; clear oe q.
elim de; clear de a p p'.
intros a p p' tr q oe.
unfold obs_eq in oe; elim oe; clear oe; intros oe_l oe_r; clear oe_r.
auto with v62.

intros a p p1 p' tr de H_ind q oe.
cut (∃ q1 : process, derivative q T q1 ∧ weak_eq p1 q1).
intros H; elim H; clear H.
intros q1 H; elim H; clear H; intros de' we.
cut (∃ q' : process, weak_derivative q1 a q' ∧ weak_eq p' q').
intros H; elim H; clear H.
intros q' H; elim H; intros de'' we'.
∃ q'; split; auto with v62.
elim eqT_dec with a.
intros a_T.
rewrite a_T in de''.
rewrite a_T.
apply w_deriv_tau_right with q1; auto with v62.

intros dif_a_T.
apply weak_deriv_deriv.
apply weak_deriv_tau_left with q1; auto with v62.

auto with v62.

cut (weak_eq1 p1 q1); auto with v62.
intros we1.
cut (∃ q' : process, weak_derivative q1 a q' ∧ weak_eq1 p' q').
intros H; elim H; clear H; intros q' H; elim H; intros de'' we1'; ∃ q';
 split; auto with v62.

inversion_clear we1; auto with v62.

unfold obs_eq in oe; elim oe; auto with v62.

intros a p p' p1 tr de H_ind q oe.
cut (∃ q1 : process, derivative q a q1 ∧ weak_eq p1 q1).
intros H; elim H; clear H.
intros q1 H; elim H; clear H; intros de1 we1.
cut (∃ q' : process, weak_derivative q1 T q' ∧ weak_eq p' q').
intros H; elim H; clear H; intros q' H; elim H; intros de2 we.
∃ q'; split; auto with v62.
apply w_deriv_tau_right with q1; auto with v62.

inversion_clear we1; auto with v62.

apply (H_ind q); auto with v62.

Qed.

Lemma obs_eq_obs_eq1 : ∀ p q : process, obs_eq p q → obs_eq1 p q.

intros p q oe.
unfold obs_eq1 in |- *; split.
exact (half_obs_eq_obs_eq1 p q oe).

cut
 (∀ (a : action) (q' : process),
  derivative q a q' →
  ∃ p' : process, derivative p a p' ∧ weak_eq q' p').
intros H a q' de.
elim (H a q' de); clear H.
intros p' H; elim H; clear H; intros; ∃ p'; split; auto with v62.

cut (obs_eq q p); auto with v62.
exact (half_obs_eq_obs_eq1 q p).

Qed.

Hint Resolve obs_eq_obs_eq1.


Lemma refl_obs_eq1 : ∀ p : process, obs_eq1 p p.

auto with v62.
Qed.

Hint Immediate refl_obs_eq1.

Lemma sym_obs_eq1 : ∀ p q : process, obs_eq1 p q → obs_eq1 q p.
intros.
apply obs_eq_obs_eq1.
apply sym_obs_eq.
auto with v62.
Qed.

Hint Immediate sym_obs_eq1.

Remark half_trans_obs_eq1 :
 ∀ p q r : process,
 obs_eq1 p q →
 obs_eq1 q r →
 ∀ (a : action) (p' : process),
 derivative p a p' → ∃ r' : process, derivative r a r' ∧ weak_eq p' r'.

intros p q r pq qr a p' de.
cut (∃ q' : process, derivative q a q' ∧ weak_eq p' q').
intros H; elim H; clear H; intros q' H; elim H; intros de' we; clear H.
elim qr; clear qr; intros qr_l qr_r; clear qr_r.
elim (qr_l a q' de').
intros r' H; elim H; clear H; intros de'' we'; ∃ r'; split;
 auto with v62.
apply trans_weak_eq with q'; auto with v62.

elim pq; intros pq_l pq_r; clear pq_r; auto with v62.

Qed.

Lemma trans_obs_eq1 :
 ∀ p q r : process, obs_eq1 p q → obs_eq1 q r → obs_eq1 p r.

intros p q r pq qr; unfold obs_eq in |- *; split.
exact (half_trans_obs_eq1 p q r pq qr).

cut
 (∀ (a : action) (r' : process),
  derivative r a r' →
  ∃ p' : process, derivative p a p' ∧ weak_eq r' p').
intros H a r' de.
elim (H a r' de); clear H; intros p' H; elim H; clear H; intros; ∃ p';
 split; auto with v62.

cut (obs_eq1 q p); auto with v62.
cut (obs_eq1 r q); auto with v62.
exact (half_trans_obs_eq1 r q p).
Qed.

Lemma trans_obs_eq :
 ∀ p q r : process, obs_eq p q → obs_eq q r → obs_eq p r.
intros p q r pq qr.
apply obs_eq1_obs_eq.
apply trans_obs_eq1 with q; auto with v62.

Qed.


Lemma strong_weak : ∀ p q : process, strong_eq p q → weak_eq p q.
cofix.
intros p q.
intros H.
inversion_clear H.
apply w_eq.
intros a p' trans.
elim (H0 a p' trans).
clear H0.
intros q' H; elim H; clear H.
intros trans1 Str.
∃ q'.
split.
apply w_single.
try try trivial with v62.

apply strong_weak; try try trivial with v62.

clear H0.
intros a q' trans.
elim (H1 a q' trans); clear H1.
intros p' H; elim H; clear H.
intros trans1 Str; ∃ p'; split.
apply w_single; try try trivial with v62.

apply strong_weak; try try trivial with v62.
Qed.

Hint Resolve strong_weak.

Lemma strong_obs : ∀ p q : process, strong_eq p q → obs_eq p q.

intros p q H.
inversion_clear H.
unfold obs_eq in |- *; split.
clear H1; intros a p' trans.
elim (H0 a p' trans); clear H0.
intros q' H; elim H; clear H.
intros trans1 Str; ∃ q'; auto with v62.
clear H0; intros a q' trans.
elim (H1 a q' trans); clear H1.
intros p' H; elim H; clear H.
intros trans1 Str; ∃ p'; split; auto with v62.
Qed.

Hint Resolve strong_obs.

Lemma obs_weak : ∀ p q : process, obs_eq p q → weak_eq p q.

unfold obs_eq in |- ×.
intros p q H; elim H; clear H; intros H1 H2.
apply w_eq.
intros a p' tr.
elim (H1 a p' tr).
intros q' H; elim H; clear H; intros de we.
∃ q'; split; auto with v62.
intros a q' tr.
elim (H2 a q' tr).
intros p' H; elim H; clear H; intros de we.
∃ p'; split; auto with v62.
Qed.

End TS.