Library tsimu

Require Import Setoid.
Require Import time.

Section TTS.
Variable Event: Type.

Inductive TLabel L: Type :=
  DLab: Time → TLabel L
| ELab: Event → TLabel L
| Tau: L → TLabel L.

Definition notDelay L (l: TLabel L): Prop :=
  match l with
    DLab _ ⇒ False
  | _ ⇒ True
  end.

Definition isDelay L (l: TLabel L): Prop :=
  match l with
    DLab _ ⇒ True
  | _ ⇒ False
  end.

Record TTS: Type := {
        State: Type;
        LEvent: Type;
        Init: State → Prop;
        Next: State → TLabel LEvent→ State → Prop;
        additivity: ∀ q d1 q' d2 q'', Next q (DLab _ d1) q' → Next q' (DLab _ d2) q'' → Next q (DLab _ (d1 @+ d2)) q'';
        zero_delay: ∀ q q', Next q (DLab _ Zero) q' ↔ q = q';
        continuity: ∀ q d' d'' q', Next q (DLab _ (d' @+ d'')) q' → ∃ r, Next q (DLab _ d') r ∧ Next r (DLab _ d'') q';
        determinism: ∀ q d q'1 q'2, Next q (DLab _ d) q'1 → Next q (DLab _ d) q'2 → q'1 = q'2

}.

Inductive DNext T st l st'': Prop :=
  DNprf: ∀ d st', Next T st (DLab _ d) st' → Next T st' l st'' → DNext T st l st''.

Inductive execFrom T s: list (Event + LEvent T) → State T → Prop :=
  Enil: ∀ s', s = s' → execFrom T s nil s'
| Etau: ∀ l e s' s'', execFrom T s l s' → DNext T s' (Tau _ e) s'' → execFrom T s ((inr _ e)::l) s''
| Eevt: ∀ l e s' s'', execFrom T s l s' → DNext T s' (ELab _ e) s'' → execFrom T s ((inl _ e)::l) s''.

Inductive exec T l: State T → Prop :=
  EE: ∀ s s', Init T s → execFrom T s l s' → exec T l s'.

Require lts.

Definition SSCG (T:TTS): lts.LTS Event := {|
        lts.State := list (Event + LEvent T);
        lts.LEvent := LEvent T;
        lts.Init lt := lt = nil;
        lts.Next lt t lt' := lt' = (t::lt)%list ∧ ∃ s, exec T lt' s
|}.

CoInductive Trace: Type :=
  TrEvent: Time → Event → Trace → Trace
| TrDiv: Trace.

Inductive skipTauWait (T: TTS): State T → Time → State T → Prop :=
  wtau: ∀ q q' d d' d'' q'' q''' l, Next T q (DLab _ d') q' → Next T q' (Tau _ l) q'' → skipTauWait T q'' d'' q''' → d = d' @+ d'' → skipTauWait T q d q'''
| wnop: ∀ q d q', Next T q (DLab _ d) q' → skipTauWait T q d q'.

Lemma DelaySkipTauWait: ∀ (T:TTS) q1 q2 q3 d d',
  Next T q1 (DLab _ d) q2 → skipTauWait T q2 d' q3 → skipTauWait T q1 (d @+ d') q3.
Proof.
  intros.
  inversion_clear H0.
  apply wtau with q' (d @+ d'0) d'' q'' l; auto.
  apply additivity with q2; auto.
  rewrite H4,tplus_assoc; tauto.
  apply wnop.
  apply additivity with q2; tauto.
Qed.

Lemma TauSkipTauWait: ∀ (T:TTS) q1 q2 q3 d l,
  Next T q1 (Tau _ l) q2 → skipTauWait T q2 d q3 → skipTauWait T q1 d q3.
Proof.
  intros.
  apply wtau with q1 Zero d q2 l; auto.
  apply zero_delay; auto.
  rewrite tplus_0_n; auto.
Qed.

Lemma wait_additivity: ∀ T q1 d1 q2 d2 q3,
  skipTauWait T q1 d1 q2 → skipTauWait T q2 d2 q3 →
    skipTauWait T q1 (d1 @+ d2) q3.
Proof.
  intros.
  induction H.
  rewrite H3 in *; clear H3 d.
  rewrite tplus_assoc.
  apply DelaySkipTauWait with q'; auto.
  apply TauSkipTauWait with q'' l; auto.

  apply DelaySkipTauWait with q'; auto.
Qed.

Inductive NextEvt T st d e st'': Prop :=
  NEprf: ∀ st', skipTauWait T st d st' → Next T st' (ELab _ e) st'' → NextEvt T st d e st''.

Definition deadlock (T: TTS) (q:State T): Prop :=
        ∀ d e q', ¬NextEvt T q d e q'.

Definition divergeFrom (T: TTS) (q:State T): Prop :=
        ∀ d, ∃ q', skipTauWait T q d q' ∧ deadlock T q'.

CoInductive acceptFrom (T:TTS) (s: State T): Trace → Prop :=
  accE: ∀ d e s'' tr, NextEvt T s d e s'' → acceptFrom T s'' tr → acceptFrom T s (TrEvent d e tr)
| accD: divergeFrom T s → acceptFrom T s TrDiv.

Inductive accept (T:TTS) (tr: Trace): Prop :=
  accPrf: ∀ s, Init T s → acceptFrom T s tr → accept T tr.

Definition refines (T1 T2: TTS): Prop :=
  ∀ tr, accept T1 tr → accept T2 tr.


CoInductive checkFrom (T1 T2: TTS): State T1 → State T2 → Prop :=
  CFE: ∀ s1 s2,
      (∀ e s'1, Next T1 s1 (ELab _ e) s'1 → ∃ s'2, ∃ s''2, skipTauWait T2 s2 Zero s'2 ∧ Next T2 s'2 (ELab _ e) s''2 ∧ checkFrom T1 T2 s'1 s''2)
  → (∀ e s'1, Next T1 s1 (Tau _ e) s'1 → checkFrom T1 T2 s'1 s2)
  → (∀ d s'1, Next T1 s1 (DLab _ d) s'1 → ∃ s'2, skipTauWait T2 s2 d s'2 ∧ checkFrom T1 T2 s'1 s'2)
  → (deadlock T1 s1 → ∃ s'2, skipTauWait T2 s2 Zero s'2 ∧ deadlock T2 s'2)
  → checkFrom T1 T2 s1 s2.

Definition check (T1 T2: TTS): Prop :=
  ∀ s1, Init T1 s1 → ∃ s2, Init T2 s2 ∧ checkFrom T1 T2 s1 s2.

Definition diverge T: Prop :=
  ∀ st d, ∃ st', skipTauWait T st d st'.

Definition isEvt L (l: TLabel L): Prop :=
  match l with
    Tau _ ⇒ True
  | ELab _ ⇒ True
  | _ ⇒ False
  end.

Lemma checkFrom_nextEvt:
  ∀ T1 T2 s1 s2 d l s''1, checkFrom T1 T2 s1 s2 → NextEvt T1 s1 d l s''1 → ∃ s''2, NextEvt T2 s2 d l s''2 ∧ checkFrom T1 T2 s''1 s''2.
Proof.
  intros.
  inversion_clear H0.
  revert H; revert s2; induction H1; intros.
  inversion_clear H4.
  elim (H7 d' _ H); clear H8 H7 H6 H5; intros.
  destruct H4.
  inversion_clear H5.
  generalize (H7 _ _ H0); clear H6 H7 H8 H9; intros.
  elim (IHskipTauWait H2 x H5); clear IHskipTauWait; intros.
  destruct H6.
  ∃ x0; split; try assumption.
  destruct H6.
  split with st'; try assumption.
  rewrite H3.
  apply wait_additivity with x; try assumption.

  inversion_clear H0.
  elim (H4 _ _ H); clear H1 H3 H4 H5; intros.
  destruct H0.
  inversion_clear H1.
  elim (H3 _ _ H2); clear H3 H4 H5 H6; intros.
  decompose record H1; clear H1.
  ∃ x1; split; try assumption.
  split with x0; try assumption.
  rewrite <- (tplus_n_0 d).
  apply wait_additivity with x; assumption.
Qed.

Lemma checkFrom_diverge:
  ∀ T1 T2 s1 s2, checkFrom T1 T2 s1 s2 → divergeFrom T1 s1 → divergeFrom T2 s2.
Proof.
  intros T1 T2; intros; intro; intros.
  elim (H0 d); clear H0; intros.
  destruct H0.
  revert H1 H; revert s2; induction H0; intros.
  inversion_clear H4.
  elim (H7 _ _ H); clear H5 H6 H7 H8; intros.
  destruct H4.
  inversion_clear H5.
  generalize (H7 _ _ H0); clear H6 H7 H8 H9; intros.
  elim (IHskipTauWait _ H3 H5); clear IHskipTauWait; intros.
  destruct H6.
  ∃ x0; split; intros.
  rewrite H2; apply wait_additivity with x; assumption.
  apply H7.

  inversion_clear H0.
  elim (H4 _ _ H); clear H2 H3 H4 H5; intros.
  destruct H0.
  inversion_clear H2.
  generalize (H6 H1); clear H3 H4 H5 H6; intros.
  decompose record H2; clear H2.
  ∃ x0; split; auto.
  rewrite <-(tplus_n_0 d).
  apply wait_additivity with x; auto.
Qed.

Lemma checkFrom_refines:
  ∀ T1 T2 s1 s2, checkFrom T1 T2 s1 s2 → (∀ tr, acceptFrom T1 s1 tr → acceptFrom T2 s2 tr).
Proof.
  intros T1 T2; intros.
  revert H0; revert tr; revert H; revert s2; revert s1; cofix; intros.
  revert H0; case tr; clear tr; intros.
  inversion_clear H0.
  elim (checkFrom_nextEvt _ _ _ _ _ _ _ H H1); intros.
  destruct H0.
  apply accE with x; try assumption.
  apply checkFrom_refines with s''; try assumption.

  inversion_clear H0.
  apply accD.
  apply checkFrom_diverge with T1 s1; auto.
Qed.

Lemma check_refines:
  ∀ T1 T2, check T1 T2 → refines T1 T2.
Proof.
  intros T1 T2; intros.
  intro; intros.
  inversion_clear H0.
  elim (H s H1); clear H; intros.
  destruct H.
  ∃ x; auto.
  apply checkFrom_refines with T1 s; auto.
Qed.

End TTS.

Variable Event: Type.

Inductive OState: Type :=
  OK: OState
| WAIT: Event → OState.

Inductive DState: Type := Devt0 | Ddly.

Definition preEvt dl :=
  match dl with
    Devt0 ⇒ True
  | Ddly ⇒ False
  end.

Definition preDly dl :=
  match dl with
  | Ddly ⇒ True
  | _ ⇒ False
  end.

Definition isDevt dl :=
  match dl with
    Devt0 ⇒ True
  | _ ⇒ False
  end.

Definition isDevt_dec: ∀ dl, {isDevt dl} + {¬isDevt dl}.
Proof.
  induction dl; simpl; try (left; apply I); right; intro H; elim H.
Defined.

Record PState (T1 T2:TTS Event): Type := mkPState {
        State1: State _ T1;
        State2: State _ T2;
        StateO: OState;
        StateD: DState
}.

Inductive LEvents T1 T2: Type :=
  Tau1: LEvent Event T1 → LEvents T1 T2
| Tau2: LEvent Event T2 → LEvents T1 T2
| Delay: LEvents T1 T2.

Definition DLabDly d dl :=
  if teq_0_dec d then dl else Ddly.

Lemma DLabDly0: ∀ dl, DLabDly Zero dl = dl.
Proof.
  intro; unfold DLabDly; case (teq_0_dec Zero); simpl; intros; auto.
  contradiction n; reflexivity.
Qed.

Lemma DLabDlyNZ:
  ∀ d, d ≠ Zero → ∀ dl, DLabDly d dl = Ddly.
Proof.
  intros.
  induction dl; unfold DLabDly; case (teq_0_dec d); simpl; intros; auto.
  elim (H e).
Qed.

Lemma pre_DLabDly_evt0: ∀ d, preEvt (DLabDly d Devt0) → d = Zero.
Proof.
  intro d.
  unfold DLabDly; case (teq_0_dec d); simpl; intros; auto.
  elim H.
Qed.

Lemma pre_DLabDly_cut: ∀ d1 d2 st,
  preEvt (DLabDly d1 (DLabDly d2 st)) → preEvt (DLabDly d1 st).
Proof.
  intros.
  case (teq_0_dec d2); intro.
  rewrite e, DLabDly0 in H; apply H.
  rewrite (DLabDlyNZ _ n) in H.
  revert H; unfold DLabDly; simpl; case (isDevt_dec st); simpl; intros; auto.
  revert H; case (teq_0_dec d1); simpl; intros; auto.
  revert H; case (teq_0_dec d1); simpl; intros; auto.
  elim H.
Qed.

Lemma pre_DLabDly_next: ∀ d1 d2 st,
  preEvt (DLabDly d1 (DLabDly d2 st)) → preEvt (DLabDly d2 st).
Proof.
  intros.
  case (teq_0_dec d1); intro.
  rewrite e, DLabDly0 in H; apply H.
  rewrite (DLabDlyNZ _ n) in H.
  revert H; unfold DLabDly; simpl; case (isDevt_dec st); simpl; intros; auto.
  elim H.
  elim H.
Qed.

Lemma DLabDly_additivity: ∀ d1 d2 st,
  DLabDly d2 (DLabDly d1 st) = DLabDly (d1 @+ d2) st.
Proof.
  intros.
  case (teq_0_dec d1); case (teq_0_dec d2); intros.
  rewrite e,e0,tplus_n_0; repeat (rewrite DLabDly0); reflexivity.
  rewrite e, tplus_0_n, DLabDly0; reflexivity.
  rewrite e, tplus_n_0, DLabDly0; reflexivity.
  assert (d1 @+ d2 ≠ Zero).
  intro; apply n; clear n.
  apply eq_sym in H; apply tplus_eq_0 in H; destruct H; assumption.
  induction st; unfold DLabDly; case (teq_0_dec d1); intro ee; try (elim (n0 ee)); clear ee;
    case (teq_0_dec d2); intro ee; try (elim (n ee)); clear ee;
      case (teq_0_dec (d1 @+ d2)); intro ee; try (elim (H ee)); clear ee; simpl; auto.
Qed.

Program Definition Compare (T1 T2: TTS Event): TTS (Event+Event) := {|
        State := PState T1 T2;
        LEvent := LEvents T1 T2;
        Init st := let (s1,s2,s,dl) := st in Init _ T1 s1 ∧ Init _ T2 s2 ∧ s=OK ∧ dl=Devt0;
        Next st l st' := let (s1,s2,s,dl) := st in let (s1',s2',s',dl') := st' in
                match l with
                  Tau (Tau1 e) ⇒ Next _ T1 s1 (Tau _ _ e) s1' ∧ s2' = s2 ∧ s = OK ∧ s'=s ∧ preEvt dl ∧ dl' = Devt0
                | Tau (Tau2 e) ⇒ Next _ T2 s2 (Tau _ _ e) s2' ∧ s1' = s1 ∧ s'=s ∧ preEvt dl ∧ dl' = Devt0
                | Tau Delay ⇒ s1' = s1 ∧ s2' = s2 ∧ s' = s ∧ preDly dl ∧ dl' = Devt0
                | ELab (inl e) ⇒ Next _ T1 s1 (ELab _ _ e) s1' ∧ s2' = s2 ∧ s=OK ∧ s'=WAIT e ∧ preEvt dl ∧ dl' = Devt0
                | ELab (inr e) ⇒ Next _ T2 s2 (ELab _ _ e) s2' ∧ s1' = s1 ∧ s=WAIT e ∧ s'=OK ∧ preEvt dl ∧ dl' = Devt0
                | DLab d ⇒ Next _ T1 s1 (DLab _ _ d) s1' ∧ Next _ T2 s2 (DLab _ _ d) s2' ∧ (s=OK ∨ d=Zero) ∧ s'=s ∧ dl' = DLabDly d dl
                end
|}.

Next Obligation.
  intros.
  induction q; induction q'; induction q''; simpl in ×.
  decompose record H; clear H.
  decompose record H0; clear H0.
  rewrite H4 in *; clear H4 StateO1.
  rewrite H8 in *; clear H8 StateO2.
  rewrite H10,H6 in *; clear H10 StateD2 H6 StateD1.
  repeat split; intros; auto.
  apply additivity with State5; assumption.
  apply additivity with State6; assumption.
  elim H2; intro; try (left; assumption).
  elim H5; intro; try (left; assumption).
  right; rewrite H0,H4; apply tplus_n_0.
  apply DLabDly_additivity.
Qed.

Next Obligation.
  intros.
  induction q; induction q'; simpl in ×.
  rewrite zero_delay.
  rewrite zero_delay.
  split; intros.
  decompose record H; clear H.
  clear H1; rewrite H0, H2, H3, H5, DLabDly0; auto.

  injection H; clear H; intros.
  rewrite <-H.
  repeat split; auto.
  case StateD0; simpl; auto.
  rewrite DLabDly0; auto.
  rewrite DLabDly0; auto.
Qed.

Next Obligation.
  induction q; induction q'; simpl in ×.
  decompose record H; clear H.
  rewrite H3 in *; clear H3 StateO1.
  elim (continuity _ _ _ _ _ _ H0); clear H0; intros.
  elim (continuity _ _ _ _ _ _ H2); clear H2; intros.
  destruct H; destruct H0.
  rewrite H5; clear H5 StateD1.
  elim (teq_0_dec d'); intro.
  rewrite a in *; clear a d'.
  rewrite tplus_0_n in ×.
  ∃ (mkPState _ _ x x0 StateO0 StateD0).
  repeat split; intros; trivial.
  destruct H1; [left|right]; trivial.
  case StateD0; simpl; auto.
  apply sym_eq; apply DLabDly0.
  apply sym_eq; apply DLabDly0.

  ∃ (mkPState _ _ x x0 StateO0 (DLabDly d' StateD0)).
  repeat split; intros; auto.
  left; destruct H1; try assumption.
  apply eq_sym in H1; apply tplus_eq_0 in H1; destruct H1.
  elim (b H1).
  left.
  destruct H1; try assumption.
  apply eq_sym in H1; apply tplus_eq_0 in H1; destruct H1.
  elim (b H1).
  apply eq_sym; apply DLabDly_additivity.
Qed.

Next Obligation.
  induction q; induction q'1; induction q'2; simpl in ×.
  decompose record H; clear H.
  decompose record H0; clear H0.
  rewrite (determinism _ _ _ _ _ _ H1 H).
  rewrite (determinism _ _ _ _ _ _ H3 H7).
  rewrite H4,H8, H10,H6.
  reflexivity.
Qed.

Definition isTau2 T1 T2 (l: TLabel (Event+Event) (LEvents T1 T2)): Prop :=
  match l with
    Tau (Tau2 _) ⇒ True
  | _ ⇒ False
  end.

Definition isEvt1 T1 T2 (l: TLabel (Event+Event) (LEvent _ (Compare T1 T2))): Prop :=
  match l with
    Tau (Tau1 _) ⇒ True
  | ELab (inl _) ⇒ True
  | _ ⇒ False
  end.

Definition isTauD T1 T2 (l: TLabel (Event+Event) (LEvent _ (Compare T1 T2))): Prop :=
  match l with
    Tau (Tau1 _) ⇒ True
  | Tau (Tau2 _) ⇒ True
  | Tau (Delay) ⇒ True
  | _ ⇒ False
  end.

Inductive EU T1 T2 (L: TLabel _ _ → Prop) (P U: PState T1 T2 → Prop): PState T1 T2 → Prop :=
  EU0: ∀ st, U st → EU T1 T2 L P U st
| EU1: ∀ st l st', P st → DNext _ (Compare T1 T2) st l st' → L l → EU T1 T2 L P U st' → EU T1 T2 L P U st.

Inductive EF T1 T2 (L: TLabel _ _ → Prop) (P: PState T1 T2 → Prop): PState T1 T2 → Prop :=
  EF0: ∀ st, P st → EF T1 T2 L P st
| EF1: ∀ st l st', DNext _ (Compare T1 T2) st l st' → L l → EF T1 T2 L P st' → EF T1 T2 L P st.

CoInductive AG T1 T2 (L: TLabel _ _ → Prop) (P: PState T1 T2 → Prop): PState T1 T2 → Prop :=
| AGprf: ∀ st, P st → (∀ l st', DNext _ (Compare T1 T2) st l st' → L l → AG T1 T2 L P st') → AG T1 T2 L P st.

Definition AX T1 T2 L (P: PState T1 T2 → Prop) (st: PState T1 T2): Prop :=
  ∀ l st', L l → DNext _ (Compare T1 T2) st l st' → P st'.

Definition AXE1 T1 T2 e (P: PState T1 T2 → Prop) (st: PState T1 T2): Prop :=
  ∀ st', DNext _ (Compare T1 T2) st (ELab _ _ (inl _ e)) st' → P st'.

Definition AXT1 T1 T2 e (P: PState T1 T2 → Prop) (st: PState T1 T2): Prop :=
  ∀ st', DNext _ (Compare T1 T2) st (Tau _ _ (Tau1 _ _ e)) st' → P st'.

Definition AXT2 T1 T2 e (P: PState T1 T2 → Prop) (st: PState T1 T2): Prop :=
  ∀ st', DNext _ (Compare T1 T2) st (Tau _ _ (Tau2 _ _ e)) st' → P st'.

Inductive EXT2 T1 T2 e (P: PState T1 T2 → Prop) (st: PState T1 T2): Prop :=
EXT2prf: ∀ st', DNext _ (Compare T1 T2) st (Tau _ _ (Tau2 _ _ e)) st' → P st' → EXT2 T1 T2 e P st.

Inductive EX T1 T2 L (P: PState T1 T2 → Prop) (st: PState T1 T2): Prop :=
EXprf: ∀ l st', L l → DNext _ (Compare T1 T2) st l st' → P st' → EX T1 T2 L P st.

Inductive EXE1 T1 T2 e (P: PState T1 T2 → Prop) (st: PState T1 T2): Prop :=
EXE1prf: ∀ st', DNext _ (Compare T1 T2) st (ELab _ _ (inl _ e)) st' → P st' → EXE1 T1 T2 e P st.

Inductive EXE2 T1 T2 e (P: PState T1 T2 → Prop) (st: PState T1 T2): Prop :=
EXE2prf: ∀ st', DNext _ (Compare T1 T2) st (ELab _ _ (inr _ e)) st' → P st' → EXE2 T1 T2 e P st.

Inductive AND T1 T2 (P Q: PState T1 T2 → Prop) (st: PState T1 T2): Prop :=
ANDprf: P st → Q st → AND T1 T2 P Q st.

Inductive IMP T1 T2 (P Q: PState T1 T2 → Prop) (st: PState T1 T2): Prop :=
IMPprf: (P st → Q st) → IMP T1 T2 P Q st.

Inductive AND3 T1 T2 (P Q R: PState T1 T2 → Prop) (st: PState T1 T2): Prop :=
AND3prf: P st → Q st → R st → AND3 T1 T2 P Q R st.

Inductive AND4 T1 T2 (P Q R S: PState T1 T2 → Prop) (st: PState T1 T2): Prop :=
AND4prf: P st → Q st → R st → S st → AND4 T1 T2 P Q R S st.

Inductive DIV T1 T2 (st: PState T1 T2): Prop :=
DIVprf: (∀ d, ∃ st', Next _ (Compare T1 T2) st (DLab _ _ d) st') → DIV T1 T2 st.

Definition ALLE T1 T2 (P: Event → PState T1 T2 → Prop) st: Prop :=
∀ e, P e st.

Definition ALL1 T1 T2 (P: LEvent _ T1 → PState T1 T2 → Prop) st: Prop :=
∀ e, P e st.

Definition ALL2 T1 T2 (P: LEvent _ T2 → PState T1 T2 → Prop) st: Prop :=
∀ e, P e st.

Definition EXE T1 T2 (P: Event → PState T1 T2 → Prop) st: Prop :=
∃ e, P e st.

Definition EX1 T1 T2 (P: LEvent _ T1 → PState T1 T2 → Prop) st: Prop :=
∃ e, P e st.

Definition EX2 T1 T2 (P: LEvent _ T2 → PState T1 T2 → Prop) st: Prop :=
∃ e, P e st.

Inductive ED T1 T2 (P: PState T1 T2 → Prop) (st: PState T1 T2): Prop :=
ED_intro: ∀ st', DNext _ (Compare T1 T2) st (Tau _ _ (Delay _ _)) st' → P st' → ED T1 T2 P st.

Definition AD T1 T2 (P: PState T1 T2 → Prop) (st: PState T1 T2): Prop :=
  ∀ st', DNext _ (Compare T1 T2) st (Tau _ _ (Delay _ _)) st' → P st'.


Definition nDL1 T1 T2 st :=
  (EF _ _ (isTauD _ _) (EXE T1 T2 (fun e ⇒ (EXE1 T1 T2 e (fun _ ⇒ True))))) st.

Definition nDL2 T1 T2 st :=
  (EF _ _ (isTauD _ _) (EXE T1 T2 (fun e ⇒ (EXE2 T1 T2 e (fun _ ⇒ True))))) st.

Lemma nDL1_ndeadlock: ∀ T1 T2 st,
  nDL1 T1 T2 st → ¬deadlock _ T1 (State1 _ _ st).
Proof.
  intros.
  induction H; intros.
  intro.
  inversion_clear H.
  inversion_clear H1.
  inversion_clear H; simpl in ×.
  induction st; induction st'; induction st'0; simpl in ×.
  decompose record H3; clear H3; subst.
  decompose record H1; clear H1; subst.
  unfold deadlock in H0.
  specialize H0 with d x State5.
  apply H0; clear H0.
  split with State7; auto.
  apply wnop; assumption.

  clear H1.
  intro; apply IHEF; clear IHEF; unfold deadlock in *; intros.
  intro.
  inversion_clear H.
  induction st; induction st'; induction st'0; simpl in ×.
  decompose record H3; clear H3; subst.
  specialize H1 with (d0 @+ d) e q'; apply H1; clear H1.
  induction l; simpl in *; try (elim H0).
  induction l; simpl in *; try (elim H0); clear H0;
    decompose record H4; clear H4; subst.
  inversion_clear H2.
  split with st'; auto.
  apply wait_additivity with State5; auto.
  rewrite <-(tplus_n_0 d0).
  apply DelaySkipTauWait with State7; auto.
  apply TauSkipTauWait with State5 l; auto.
  apply wnop; apply zero_delay; reflexivity.

  inversion_clear H2.
  split with st'; auto.
  apply wait_additivity with State7; auto.
  apply wnop.
  assumption.

  inversion_clear H2.

  split with st'; auto.
  apply DelaySkipTauWait with State7; auto.
Qed.

Lemma nDL2_ndeadlock: ∀ T1 T2 st,
  nDL2 T1 T2 st → ¬deadlock _ T2 (State2 _ _ st).
Proof.
  intros.
  induction H; intros.
  intro.
  inversion_clear H.
  inversion_clear H1.
  inversion_clear H; simpl in ×.
  induction st; induction st'; induction st'0; simpl in ×.
  decompose record H3; clear H3; subst.
  decompose record H1; clear H1; subst.
  unfold deadlock in H0.
  specialize H0 with d x State6.
  apply H0; clear H0.
  split with State8; auto.
  apply wnop; assumption.

  clear H1.
  intro; apply IHEF; clear IHEF; unfold deadlock in *; intros.
  intro.
  inversion_clear H.
  induction st; induction st'; induction st'0; simpl in ×.
  decompose record H3; clear H3; subst.
  specialize H1 with (d0 @+ d) e q'; apply H1; clear H1.
  induction l; simpl in *; try (elim H0).
  induction l; simpl in *; try (elim H0); clear H0;
    decompose record H4; clear H4; subst.
  inversion_clear H2.
  split with st'; auto.
  apply wait_additivity with State8; auto.
  rewrite <-(tplus_n_0 d0).
  apply DelaySkipTauWait with State8; auto.
  apply wnop; apply zero_delay; reflexivity.

  inversion_clear H2.
  split with st'; auto.
  apply wait_additivity with State8; auto.
  apply wnop.
  assumption.

  apply TauSkipTauWait with State6 l; auto.

  inversion_clear H2.
  split with st'; auto.
  apply DelaySkipTauWait with State8; auto.
Qed.

Require Import Coq.Logic.Classical_Pred_Type.
Require Import Coq.Logic.Classical_Prop.

Lemma ndeadlock_nDL2: ∀ T1 T2, diverge _ T1 → ∀ s1 s2,
  ¬deadlock _ T2 s2 → nDL2 T1 T2
  {| State1 := s1; State2 := s2; StateO := OK; StateD := Devt0 |}.
Proof.
  intros T1 T2 DV1; intros.
  unfold deadlock in H.
  apply not_all_ex_not in H; destruct H.
  apply not_all_ex_not in H; destruct H.
  apply not_all_not_ex in H; destruct H.
  destruct H.
  revert s1; induction H; intros.
  elim (DV1 s1 d'); intros.
  apply IHskipTauWait with (s1:=x) in H0; clear IHskipTauWait.
  clear H2 H3 d'' d.
  revert H; revert q; induction H4; intros.
  rewrite H3 in H5; clear H3 d.
  apply continuity in H5; destruct H5.
  destruct H3.
  case (teq_0_dec d'); intro.
  rewrite e in *; clear e d'.
  apply zero_delay in H3; rewrite H3 in *; clear H3 q0.
  apply zero_delay in H; rewrite H in *; clear H q.
  apply EF1 with (Tau _ _ (Tau1 _ _ l0)) (mkPState _ _ q''0 x OK Devt0); simpl; auto.
  split with Zero (mkPState _ _ q'0 x OK Devt0); simpl; intros; repeat split; auto.
  rewrite zero_delay; reflexivity.
  rewrite zero_delay; reflexivity.
  rewrite DLabDly0; auto.
  apply IHskipTauWait; auto.

  apply EF1 with (Tau _ _ (Delay _ _)) (mkPState _ _ q'0 x OK Devt0); simpl; auto.
  split with d' (mkPState _ _ q'0 x OK Ddly); simpl; intros; repeat split; auto.
  unfold DLabDly; case (teq_0_dec d'); tauto.
  apply EF1 with (Tau _ _ (Tau1 _ _ l0)) (mkPState _ _ q''0 x OK Devt0); simpl; auto.
  split with Zero (mkPState _ _ q'0 x OK Devt0); simpl; intros; repeat split; auto.
  apply zero_delay; reflexivity.
  apply zero_delay; reflexivity.
  rewrite DLabDly0; auto.
  apply IHskipTauWait; auto.

  case (teq_0_dec d); intro.
  rewrite e in *; clear e d.
  apply zero_delay in H2; rewrite H2 in *; clear H2 q0.
  apply zero_delay in H; rewrite H in *; clear H q.
  apply EF1 with (Tau _ _ (Tau2 _ _ l)) (mkPState _ _ q'0 q'' OK Devt0); simpl; repeat split; auto.
  split with Zero (mkPState _ _ q'0 q' OK Devt0); simpl; intros; repeat split; auto.
  rewrite zero_delay; reflexivity.
  rewrite zero_delay; reflexivity.
  rewrite DLabDly0; auto.

  apply EF1 with (Tau _ _ (Delay _ _)) (mkPState _ _ q'0 q' OK Devt0); simpl; auto.
  split with d (mkPState _ _ q'0 q' OK Ddly); simpl; intros; repeat split; auto.
  unfold DLabDly; case (teq_0_dec d); tauto.
  apply EF1 with (Tau _ _ (Tau2 _ _ l)) (mkPState _ _ q'0 q'' OK Devt0); simpl; repeat split; auto.
  split with Zero (mkPState _ _ q'0 q' OK Devt0); simpl; intros; repeat split; auto.
  rewrite zero_delay; reflexivity.
  rewrite zero_delay; reflexivity.
  rewrite DLabDly0; auto.

  elim (DV1 s1 d); intros.
  admit. Qed.

Lemma ndeadlock_nDL1: ∀ T1 T2, diverge _ T2 → ∀ s1 s2,
  ¬deadlock _ T1 s1 → nDL1 T1 T2 {| State1 := s1; State2 := s2; StateO := OK; StateD := Devt0 |}.
Proof.
  admit.
Qed.

CoInductive pCheckFrom T1 T2 (st: PState T1 T2): Prop :=
pCFprf:
      StateO _ _ st = OK → preEvt (StateD _ _ st)
  → AND4 T1 T2
        (ALLE T1 T2 (fun e ⇒ (AXE1 T1 T2 e (EF T1 T2 (isTau2 _ _)
                                                       (EXE2 T1 T2 e (pCheckFrom T1 T2))))))
        (ALL1 T1 T2 (fun e ⇒ AXT1 T1 T2 e (pCheckFrom T1 T2)))
        (IMP T1 T2
          (EF T1 T2 (isTau2 _ _) (ED T1 T2 (fun _ ⇒ True)))
          (EF T1 T2 (isTau2 _ _) (AND T1 T2 (ED T1 T2 (fun _ ⇒ True))
            (AD T1 T2 (pCheckFrom T1 T2)))))
        (IMP T1 T2 (AG T1 T2 (isTau2 _ _) (nDL2 _ _)) (nDL1 _ _))
      st
  → pCheckFrom T1 T2 st.
Definition pCheck T1 T2: Prop :=
  ∀ st, Init _ (Compare T1 T2) st → pCheckFrom T1 T2 st.

Lemma pCheckFrom_state: ∀ T1 T2 st, pCheckFrom T1 T2 st → StateO _ _ st = OK.
Proof.
  intros.
  inversion_clear H.
  auto.
Qed.

Lemma EF_tau2:
  ∀ T1 T2 P st, EF T1 T2 (isTau2 _ _) P st →
    ∃ d, ∃ st', skipTauWait _ T2 (State2 _ _ st) d (State2 _ _ st') ∧ P st'∧ Next _ T1 (State1 _ _ st) (DLab _ _ d) (State1 _ _ st').
Proof.
  intros.
  induction H.
  ∃ Zero.
  ∃ st.
  split; auto.
  apply wnop.
  rewrite zero_delay; auto.
  rewrite zero_delay; auto.

  destruct IHEF.
  destruct H2.
  destruct H2.
  destruct H3.
  induction l; try (elim H0).
  induction l; try (elim H0); clear H0.
  inversion_clear H; simpl in ×.
  induction st; induction st'; induction st'0; simpl in ×.
  decompose record H5; clear H5.
  rewrite <-H7,<-H6,H10 in *; clear H7 H6 StateO2 State7 H10 StateD1.
  decompose record H0; clear H0.
  rewrite H9 in *; clear H9 StateO1.
  ∃ (d @+ x).
  ∃ x0; simpl.

  split; auto.
  apply DelaySkipTauWait with State8; try trivial.
  apply TauSkipTauWait with State6 l; try trivial.
  split; try trivial.
  apply additivity with State5; trivial.
Qed.

Lemma DNext_tau2_evt0: ∀ T1 T2 st l st', (isTau2 _ _ l) →
  DNext (Event + Event) (Compare T1 T2) st l st' → StateD _ _ st' = Devt0.
Proof.
  intros.
  induction st; induction st'; simpl in ×.
  induction l; simpl in H; try (contradiction H; apply I).
  induction l; try (elim H); clear H.
  destruct H0; simpl in ×.
  induction st'; simpl in ×.
  decompose record H; clear H.
  rewrite H6,H4 in *; clear H6 StateD2 H4 StateO2.
  decompose record H0; clear H0.
  apply H8.
Qed.

Lemma DNext_tau2_evt: ∀ T1 T2 st l st', (isTau2 _ _ l) →
  DNext (Event + Event) (Compare T1 T2) st l st' → StateD _ _ st' = Devt0.
Proof.
  intros.
  induction st; induction st'; simpl in ×.
  induction l; simpl in H; try (contradiction H; apply I).
  induction l; try (elim H); clear H.
  destruct H0; simpl in ×.
  induction st'; simpl in ×.
  decompose record H; clear H.
  rewrite H6,H4 in *; clear H6 StateD2 H4 StateO2.
  decompose record H0; clear H0.
  apply H8.
Qed.

Lemma preevt0: ∀ d, preEvt (DLabDly d Devt0) → d = Zero.
Proof.
  intros.
  unfold DLabDly in H.
  revert H; case (teq_0_dec d); simpl; intros; auto.
  elim H.
Qed.

Lemma EF_tau2_evt0:
  ∀ T1 T2 P st, EF T1 T2 (isTau2 _ _) P st → StateD _ _ st = Devt0 →
    ∃ st', skipTauWait _ T2 (State2 _ _ st) Zero st' ∧ P (mkPState _ _ (State1 _ _ st) st' (StateO _ _ st) Devt0).
Proof.
  intros.
  revert H0; induction H; intro Hd.
  ∃ (State2 _ _ st).
  induction st; simpl in ×.
  split; auto.
  apply wnop.
  rewrite zero_delay; auto.
  rewrite Hd in H; assumption.
  generalize (DNext_tau2_evt0 _ _ _ _ _ H0 H); intro.
  elim (IHEF H2); clear IHEF H2; intros.
  destruct H2.
  induction l; try (elim H0).
  induction l; try (elim H0); clear H0.
  inversion_clear H; simpl in ×.
  induction st; induction st'; induction st'0; simpl in ×.
  decompose record H4; clear H4.
  rewrite H9,<-H5,<-H6 in *; clear H9 H5 H6 StateO2 State7 StateD1.
  decompose record H0; clear H0.
  rewrite H10,H8 in *; clear H10 H8 StateD2 StateO1.
  rewrite Hd in *; clear Hd StateD0.
  ∃ x; simpl.
  apply pre_DLabDly_evt0 in H7.
  rewrite H7 in *; clear H5 H7 d.
  apply zero_delay in H4; rewrite <-H4 in *; clear H4 State5.
  split; auto.
  apply zero_delay in H6; rewrite <-H6 in *; clear H6 State8.
  apply TauSkipTauWait with State6 l; assumption.
Qed.

Require Import Classical.

Lemma AX_EX: ∀ T1 T2 L P st,
  AX T1 T2 L P st ∨ EX T1 T2 L (fun st ⇒ ¬ P st) st.
Proof.
  intros.
  elim (classic (AX T1 T2 L P st)); intro.
  left; assumption.
  right.
  apply NNPP; intro.
  apply H; clear H; intro; intros.
  apply NNPP; intro.
  apply H0; clear H0.
  ∃ l st'; assumption.
Qed.

Definition isWait (T1 T2: TTS Event) (st: State _ (Compare T1 T2)): Prop :=
  match StateO _ _ st with
    OK ⇒ False
  | WAIT _ ⇒ True
  end.

Lemma EF_tau2_WAIT:
  ∀ T1 T2 P st, isWait T1 T2 st → EF T1 T2 (isTau2 _ _) P st →
    ∃ st', skipTauWait _ T2 (State2 _ _ st) Zero (State2 _ _ st') ∧ P st'∧ State1 _ _ st = State1 _ _ st'.
Proof.
  intros T1 T2 P st W; intros.
  induction H.
  ∃ st.
  split; auto.
  apply wnop.
  apply zero_delay; trivial.

  cut (isWait _ _ st'); intros.
  destruct (IHEF H2); clear H2.
  destruct H3.
  destruct H3.
  induction l; try (elim H0).
  induction l; try (elim H0); clear H0.
  inversion_clear H; simpl in ×.
  induction st; induction st'; induction st'0; simpl in ×.
  decompose record H5; clear H5.
  rewrite <-H7,<-H6,H10 in *; clear H6 H7 H10 StateO2 State7 StateD1.
  decompose record H0; clear H0.
  rewrite H9,H11 in *; clear H9 StateO1 H11 StateD2.
  ∃ x; simpl.
  induction StateO0; simpl in W; try (elim W).
  elim H6; clear H6; intro H6; try (discriminate H6); subst.
  rewrite zero_delay in H5,H7.
  rewrite H5,<-H7 in *; clear H5 H7 State3 State8.
  split; [idtac | split; trivial].
  apply TauSkipTauWait with State6 l; trivial.

  clear IHEF.
  induction l; try (elim H0).
  induction l; try (elim H0); clear H0.
  inversion_clear H; simpl in ×.
  induction st; induction st'; induction st'0; simpl in ×.
  decompose record H2; clear H2.
  rewrite H4,H7,<-H3 in *; clear H4 H7 State5 StateD1 H3 StateO2.
  decompose record H0; clear H0.
  rewrite H6; trivial.
Qed.

Lemma Tau2Obs:
  ∀ T1 T2 st l st', DNext (Event + Event) (Compare T1 T2) st l st' → isTau2 _ _ l → StateO _ _ st' = StateO _ _ st.
Proof.
  intros.
  induction l; try (elim H0).
  induction l; try (elim H0); clear H0.
  induction st; induction st'; simpl in H; simpl.
  destruct H; simpl in ×.
  induction st'; simpl in ×.
  intuition.
  rewrite H4; apply H5.
  rewrite H4; apply H5.
Qed.

Lemma Tau2Proj1:
  ∀ T1 T2 st l st', DNext (Event + Event) (Compare T1 T2) st l st'
    → isTau2 _ _ l → isWait T1 T2 st → State1 _ _ st' = State1 _ _ st.
Proof.
  intros.
  induction l; try (elim H0).
  induction l; try (elim H0); clear H0.
  destruct H.
  induction st; induction st'; induction st'0; simpl in *; try (elim H1); simpl in H1.
  intuition.
  rewrite H8 in H1; elim H1.
  rewrite H8 in *; clear H8 d.
  rewrite zero_delay in H2.
  rewrite <- H2 in H3; apply H3.
Qed.

Lemma EXE2_ex2:
  ∀ T1 T2 e P st, EXE2 T1 T2 e P st → ∃ s2, Next _ T2 (State2 _ _ st) (ELab _ _ e) s2 ∧ P (mkPState _ _ (State1 _ _ st) s2 OK Devt0).
Proof.
  intros.
  induction st; simpl in ×.
  inversion_clear H.
  induction st'; simpl in ×.
  inversion_clear H0.
  simpl in ×.
  induction st'; simpl in ×.
  decompose record H; clear H.
  decompose record H2; clear H2.
  rewrite H6,H9,H8,H12 in *; clear H9 StateO1 H6 StateO2 H8 State5 H12 StateD1.
  rewrite <- H5 in *; clear H5 StateO0.
  elim H3; clear H3; intro H3; try (discriminate H3).
  rewrite H7 in *; clear H7 StateD2.
  rewrite H3 in *; clear H3 d.
  rewrite zero_delay in H4,H0.
  rewrite H0,H4 in *; clear State3 State4 H0 H4.
  ∃ State6.
  repeat split; auto.
Qed.

Lemma EF_tau2Z_intro:
  ∀ T1 T2 (P: PState T1 T2 → Prop) (st st': PState T1 T2),
    StateD _ _ st = Devt0 → StateD _ _ st' = Devt0 →
    skipTauWait _ T2 (State2 _ _ st) Zero (State2 _ _ st') → P st'→ State1 _ _ st = State1 _ _ st' → StateO _ _ st = StateO _ _ st'
      → EF T1 T2 (isTau2 _ _) P st.
Proof.
  intros until st'; intros D1 D2 H; intros.
  induction st; induction st'; simpl in ×.
  rewrite D1,D2 in *; clear D1 D2 StateD0 StateD1.
  rewrite <-H1 in *; clear H1 State5.
  set (d := Zero).
  generalize (refl_equal d); intro.
  unfold d in H1 at 2.
  rewrite <- H1 in H.
  revert H0; revert H1; induction H; intros; auto.
  rewrite H4 in H3.
  apply tplus_eq_0 in H3.
  destruct H3.
  rewrite H3,H6,H2 in *; clear H2 StateO0 H3 d' H6 d'' H4 d.
  generalize (IHskipTauWait (refl_equal _) H5); clear IHskipTauWait; intro.
  apply EF1 with (Tau _ _ (Tau2 _ _ l)) (mkPState _ _ State3 q'' StateO1 Devt0); simpl; auto.
  split with Zero (mkPState _ _ State3 q' StateO1 Devt0); simpl.
  rewrite zero_delay.
  rewrite zero_delay.
  rewrite DLabDly0.
  repeat split; try trivial.
  rewrite zero_delay in H; trivial.
  right; trivial.
  repeat split; trivial.

  apply EF0; auto.
  rewrite H1 in H.
  apply zero_delay in H.
  rewrite H, H2.
  apply H0.
Qed.

Lemma pCheckFrom_NextEvt:
  ∀ T1 T2 st, pCheckFrom T1 T2 st →
    ∀ st1' e,
      Next _ T1 (State1 _ _ st) (ELab _ _ e) st1' →
        ∃ st2', ∃ st2'',
          skipTauWait _ T2 (State2 _ _ st) Zero st2' ∧
          Next _ T2 st2' (ELab _ _ e) st2'' ∧
          pCheckFrom T1 T2 (mkPState _ _ st1' st2'' OK Devt0).
Proof.
  intros T1 T2; intros.
  inversion_clear H.
  inversion_clear H3.
  rename H6 into dlp.
  induction st; simpl in ×.
  rewrite H1 in *; clear H1 StateO0.
  cut (DNext (Event + Event) (Compare T1 T2)
       {| State1 := State3; State2 := State4; StateO := OK; StateD := StateD0 |}
       (ELab (Event + Event) (LEvent (Event + Event) (Compare T1 T2))
          (inl Event e))
       {| State1 := st1'; State2 := State4; StateO := WAIT e; StateD := Devt0 |}); intros.
  generalize (H e (mkPState _ _ st1' State4 (WAIT e) Devt0) H1); clear H H4 H5; intros.
  apply EF_tau2_WAIT in H; simpl in ×.
  destruct H; destruct H.
  destruct H3.
  rewrite H4 in *; clear H4 st1'.
  inversion_clear H1; simpl in ×.
  induction st'; simpl in ×.
  decompose record H5; clear H5.
  rewrite <-H7,H6 in *; clear H7 H6 H8 H11 StateO0 State6.
  decompose record H4; clear H4.
  rewrite H11 in *; clear H11 H8 H6 StateD1.
  induction x; simpl in ×.
  inversion_clear H3.
  induction st'; simpl in ×.
  inversion_clear H4; simpl in ×.
  induction st'; simpl in ×.
  decompose record H8; clear H8.
  rewrite H15,<-H11,H12,H10 in *; clear H15 StateD2 H12 StateO1 H11 State10 H10 StateO2.
  decompose record H3; clear H3.
  rewrite <- H12 in *; clear H12 StateO0.
  elim H10; clear H10; intro H10; try (discriminate H10).
  rewrite H10,H15 in *; clear H10 d0 H15 StateD3.
  ∃ State11; ∃ State9.
  rewrite zero_delay in H8.
  rewrite <-H8 in *; clear H8 State8.
  split; [idtac|split]; try assumption.
  rewrite zero_delay in H11.
  rewrite <-H11; assumption.

  apply I.

  split with Zero (mkPState _ _ State3 State4 OK StateD0); simpl.
  repeat (rewrite zero_delay); repeat split; try reflexivity.
  left; reflexivity.
  revert H2; case StateD0; simpl; intros; auto.
  apply eq_sym; apply DLabDly0.
  repeat split; trivial.
  elim H2.
  repeat split; auto.
Qed.

Lemma pCheckFrom_NextTau:
  ∀ T1 T2 st, pCheckFrom T1 T2 st →
    ∀ e st1',
      Next _ T1 (State1 _ _ st) (Tau _ _ e) st1' →
        ∃ st2',
          skipTauWait _ T2 (State2 _ _ st) Zero st2' ∧
          pCheckFrom T1 T2 (mkPState _ _ st1' st2' OK Devt0).
Proof.
  intros T1 T2; intros.
  inversion_clear H.
  induction st; simpl in ×.
  rewrite H1 in *; clear H1 StateO0.
  destruct H3.
  rename H4 into dlp.
  cut (DNext (Event + Event) (Compare T1 T2)
   {| State1 := State3; State2 := State4; StateO := OK; StateD := StateD0 |}
   (Tau _ _ (Tau1 _ _ e))
   {| State1 := st1'; State2 := State4; StateO := OK; StateD := Devt0 |}); intros.
  generalize (H1 e (mkPState _ _ st1' State4 OK Devt0) H4); clear H H1 H2 H3; intros.
  ∃ State4.
  split; try assumption.
  apply wnop.
  rewrite zero_delay; reflexivity.
  split with Zero (mkPState _ _ State3 State4 OK StateD0); simpl.
  repeat (rewrite zero_delay); repeat split; try reflexivity.
  left; reflexivity.
  revert H2; case StateD0; simpl; intros; auto.
  apply eq_sym; apply DLabDly0.
  repeat split; trivial.
  elim H2.
  repeat split; auto.
Qed.


Lemma checkFrom_refl: ∀ L T s, checkFrom L T T s s.
Proof.
  admit.
Qed.

Inductive skipTauWaitAtl1Tau L T s d s': Prop :=
  stw1t: ∀ s'1 s'2 d' e d'',
    d = d' @+ d'' → skipTauWait L T s d' s'1 → Next L T s'1 (Tau _ _ e) s'2 → skipTauWait L T s'2 d'' s' → skipTauWaitAtl1Tau L T s d s'.

Inductive skipTauWaitNZ L T st d0: Time → State L T → Prop :=
  wtau1: ∀ d st', skipTauWaitAtl1Tau L T st d st' → skipTauWaitNZ L T st d0 d st'
| wdly1: ∀ d st', d = d0 → Next L T st (DLab _ _ d0) st' → skipTauWaitNZ L T st d0 d st'.

Lemma skipTauWaitNZ_max_intro: ∀ L T s d s',
  skipTauWait L T s d s' → skipTauWaitNZ L T s d d s'.
Proof.
  intros.
  inversion_clear H.
  apply wtau1.
  apply stw1t with q' q'' d' l d''; auto.
  apply wnop; assumption.
  apply wdly1; auto.
Qed.

Lemma skipTauWaitAtl1Tau_skipTauWait: ∀ L T st d st',
  skipTauWaitAtl1Tau L T st d st' → skipTauWait L T st d st'.
Proof.
  intros.
  inversion_clear H.
  subst.
  apply wait_additivity with s'1; auto.
  apply TauSkipTauWait with s'2 e; auto.
Qed.

CoInductive isTauZeno L T st d: Prop :=
  istz: ∀ st' d' d'', skipTauWaitAtl1Tau L T st d' st' → isTauZeno L T st' d'' → d' @+ d'' @<= d → isTauZeno L T st d.

Definition isTauNonZeno L T := ∀ st d, ¬isTauZeno L T st d.

Definition nonZenoTauPath L T: Prop :=
  ∀ (P: Time → State L T → Prop) d,
    (∀ st d1 d2, P d1 st → d2 ≠ Zero → d1 @+ d2 = d →
      ∃ d3, ∃ st',
        d3 @<= d2 ∧ skipTauWaitNZ L T st d2 d3 st' ∧ P (d1 @+ d3) st') →
    ∀ st, P Zero st → ∃ st', skipTauWait L T st d st' ∧ P d st'.

Lemma nonZenoTauPath_isTauNonZeno:
  ∀ L T, nonZenoTauPath L T → isTauNonZeno L T.
Proof.
  unfold isTauNonZeno; intros.
  intro.
  elim (tunb d); intros.
  generalize (H (fun t s ⇒ ∃ t', t @+ t' @<= d ∧ isTauZeno L T s t') x); clear H; intros.
  elim H with (st:=st); clear H; intros.
  decompose record H; clear H; intros.
  subst.
  rewrite tplus_assoc in H1.
  apply tlt_plus_nlt in H1; apply H1.
  destruct H as [t' [e H]]; subst.
  destruct H.
  ∃ d'; ∃ st'.
  repeat split.
  destruct H1.
  generalize (tle_trans _ _ _ e H1); intro.
  destruct H6.
  rewrite tplus_assoc in H6; apply tplus_opp_l in H6; subst.
  apply tle_trans with t'.
  destruct H4.
  ∃ (d''@+t0); subst.
  apply eq_sym; apply tplus_assoc.
  ∃ t; now auto.

  apply wtau1; auto.
  ∃ d''; split; auto.
  rewrite tplus_assoc.
  apply tle_trans with (d1 @+ t'); auto.
  destruct H4.
  ∃ t; subst.
  rewrite tplus_assoc; now auto.

  ∃ d; split; auto.
  ∃ Zero.
  rewrite tplus_0_n.
  apply tplus_n_0.
Qed.

Lemma isTauNonZeno_nonZenoTauPath:
  ∀ L T, isTauNonZeno L T → nonZenoTauPath L T.
Proof.
  intros.
  unfold isTauNonZeno in H.
  intro; intros.
  specialize H with st d.
  apply NNPP; intro.
  apply H; clear H.
  elim (teq_0_dec d); intros; subst.
  clear H0.
  apply False_ind; apply H2; clear H2.
  ∃ st; split; auto.
  apply wnop.
  apply zero_delay; now auto.
  assert (∃ st0, skipTauWait L T st0 Zero st).
  ∃ st; apply wnop; apply zero_delay; now auto.
  destruct H as [st0 H].
  assert (Zero @<= d) by (∃ d; apply tplus_0_n).
  destruct H3.
  assert (t = d) by (rewrite tplus_0_n in H3; auto).
  assert (¬ (∃ st' : State L T, skipTauWait L T st t st' ∧ P d st')).
  rewrite H4; apply H2.
  clear H2.
  rewrite <-H4 in b |- *; clear H4.
  revert H3 H H1; generalize Zero; intros.
  subst.
  revert dependent st; revert dependent t; revert t0; cofix; intros.
  elim (H0 st t0 t H1 b (refl_equal _)); intros.
  decompose record H2; clear H2; intros; subst.
  inversion_clear H4.
  apply istz with x0 x t1; intros; auto.
  apply isTauNonZeno_nonZenoTauPath with (t0 @+ x); clear isTauNonZeno_nonZenoTauPath; intros; auto.
  intro; subst; apply H5; clear H5.
  rewrite tplus_n_0.
  ∃ x0; split; auto.
  apply skipTauWaitAtl1Tau_skipTauWait; assumption.

  apply H0; intros; auto.
  rewrite tplus_assoc in H6; apply H6.

  apply wait_additivity with st; auto.
  apply skipTauWaitAtl1Tau_skipTauWait; assumption.

  intro; apply H5; clear H5.
  decompose record H3; clear H3.
  rewrite tplus_assoc in H6.
  ∃ x1; split; auto.
  apply wait_additivity with x0; auto.
  apply skipTauWaitAtl1Tau_skipTauWait; assumption.

  apply tle_refl.

  assert (x @+ Zero = x @+ t1) by (rewrite tplus_n_0; apply H2).
  apply tplus_opp_l in H4.
  clear H2; subst.
  rewrite tplus_n_0 in ×.
  apply False_ind; apply H5; clear H5.
  ∃ x0; split; auto.
  apply wnop; auto.
Qed.

Inductive skipTau2Wait (T1 T2: TTS Event) (st: State (Event+Event) (Compare T1 T2)) (d: Time) (st': State (Event+Event) (Compare T1 T2)): Prop :=
  st2we: ∀ e st1,
    Next (Event+Event) (Compare T1 T2) st (Tau (Event+Event) (LEvents T1 T2) (Tau2 T1 T2 e)) st1 →
    skipTau2Wait T1 T2 st1 d st' →
    skipTau2Wait T1 T2 st d st'
| st2wd: ∀ d' st1 st2 d'',
    Next (Event+Event) (Compare T1 T2) st (DLab _ _ d') st1 →
    Next _ (Compare T1 T2) st1 (Tau _ _ (Delay _ _)) st2 →
    skipTau2Wait T1 T2 st2 d'' st' →
    d = d' @+ d'' →
    skipTau2Wait T1 T2 st d st'
| st2wn: st' = st → d = Zero → skipTau2Wait T1 T2 st d st'.

Inductive timedPred T1 T2 d dl s1 s2 d' (s'2: State Event T2): Prop :=
  tpGt: ~(d' @<= d) → timedPred T1 T2 d dl s1 s2 d' s'2
| tpTau:
  ∀ st,
    skipTau2Wait T1 T2 (mkPState _ _ s1 s2 OK dl) d' st →
    pCheckFrom T1 T2 st →
    State2 _ _ st = s'2 →
    timedPred T1 T2 d dl s1 s2 d' s'2
| tpDly:
    d'=d → ∀ s'1,
    Next _ T1 s1 (DLab _ _ d') s'1 →
    Next _ T2 s2 (DLab _ _ d') s'2 →
    pCheckFrom T1 T2 (mkPState _ _ s'1 s'2 OK Devt0) →
    timedPred T1 T2 d dl s1 s2 d' s'2.

Lemma Devt0_exDelay: ∀ T1 T2 s1 d s2, Next _ (Compare T1 T2) s1 (DLab _ _ d) s2 → d ≠ Zero → preEvt (StateD _ _ s1) →
  ∃ s3, Next _ (Compare T1 T2) s2 (Tau _ _ (Delay _ _)) s3.
Proof.
  intros.
  induction s1; induction s2; simpl in ×.
  ∃ (mkPState _ _ State5 State6 StateO1 Devt0); simpl.
  repeat split; auto.
  decompose record H; clear H.
  rewrite H7; clear H7 StateD1.
  unfold DLabDly; simpl.
  induction StateD0; simpl in ×.
  case (teq_0_dec d); auto.
  elim H1.
Qed.

Lemma pCheckFrom_preEvt:
  ∀ T1 T2 st, pCheckFrom T1 T2 st → preEvt (StateD _ _ st).
Proof.
  intros.
  inversion_clear H.
  assumption.
Qed.

Lemma pCheckFrom_EFD:
  ∀ T1 T2 st, pCheckFrom T1 T2 st →
    (EF T1 T2 (isTau2 _ _) (ED T1 T2 (fun _ ⇒ True))) st →
    (EF T1 T2 (isTau2 _ _) (AND T1 T2 (ED T1 T2 (fun _ ⇒ True))
      (AD T1 T2 (pCheckFrom T1 T2))))
      st.
Proof.
  intros.
  inversion_clear H.
  inversion_clear H3.
  inversion_clear H5.
  apply (H3 H0).
Qed.

Lemma Tau2_proj1:
  ∀ T1 T2 st e st', Next _ (Compare T1 T2) st (Tau _ _ (Tau2 _ _ e)) st'
    → State1 _ _ st' = State1 _ _ st.
Proof.
  intros.
  induction st; induction st'; simpl in ×.
  decompose record H; assumption.
Qed.

Lemma Tau2_proj2:
  ∀ T1 T2 st e st', Next _ (Compare T1 T2) st (Tau _ _ (Tau2 _ _ e)) st'
    → Next _ T2 (State2 _ _ st) (Tau _ _ e) (State2 _ _ st').
Proof.
  intros.
  induction st; induction st'; simpl in ×.
  decompose record H; assumption.
Qed.

Lemma Tau2_StateD:
  ∀ T1 T2 st e st', Next _ (Compare T1 T2) st (Tau _ _ (Tau2 _ _ e)) st'
    → StateD _ _ st' = Devt0.
Proof.
  intros.
  induction st; induction st'; simpl in ×.
  decompose record H; assumption.
Qed.

Lemma Tau2_StateO:
  ∀ T1 T2 st e st', Next _ (Compare T1 T2) st (Tau _ _ (Tau2 _ _ e)) st'
    → StateO _ _ st' = StateO _ _ st.
Proof.
  intros.
  induction st; induction st'; simpl in ×.
  decompose record H; assumption.
Qed.

Lemma Delta_proj1: ∀ T1 T2 st d st',
  Next _ (Compare T1 T2) st (DLab _ _ d) st' →
    Next _ T1 (State1 _ _ st) (DLab _ _ d) (State1 _ _ st').
Proof.
  intros.
  induction st; induction st'; simpl in ×.
  decompose record H; assumption.
Qed.

Lemma Delta_proj2: ∀ T1 T2 st d st',
  Next _ (Compare T1 T2) st (DLab _ _ d) st' →
    skipTauWait _ T2 (State2 _ _ st) d (State2 _ _ st').
Proof.
  intros.
  apply wnop.
  induction st; induction st'; simpl in ×.
  decompose record H; assumption.
Qed.

Lemma Delta_StateO: ∀ T1 T2 st d st',
  Next _ (Compare T1 T2) st (DLab _ _ d) st' →
    StateO _ _ st' = StateO _ _ st.
Proof.
  intros.
  induction st; induction st'; simpl in ×.
  decompose record H; assumption.
Qed.

Lemma Delay_proj2: ∀ T1 T2 st st',
  Next _ (Compare T1 T2) st (Tau _ _ (Delay _ _)) st' →
    skipTauWait _ T2 (State2 _ _ st) Zero (State2 _ _ st').
Proof.
  intros.
  apply wnop.
  apply zero_delay.
  induction st; induction st'; simpl in ×.
  decompose record H; clear H.
  apply sym_eq; apply H2.
Qed.

Lemma Delay_State1:
  ∀ T1 T2 st st',
    Next _ (Compare T1 T2) st (Tau _ _ (Delay _ _)) st' →
      State1 _ _ st' = State1 _ _ st.
Proof.
  intros.
  induction st; induction st'; simpl in ×.
  decompose record H; auto.
Qed.

Lemma Delay_State2:
  ∀ T1 T2 st st',
    Next _ (Compare T1 T2) st (Tau _ _ (Delay _ _)) st' →
      State2 _ _ st' = State2 _ _ st.
Proof.
  intros.
  induction st; induction st'; simpl in ×.
  decompose record H; auto.
Qed.

Lemma Delay_StateD: ∀ T1 T2 st st',
  Next _ (Compare T1 T2) st (Tau _ _ (Delay _ _)) st' →
    StateD _ _ st' = Devt0.
Proof.
  intros.
  induction st; induction st'; simpl in ×.
  decompose record H; assumption.
Qed.

Lemma Delay_StateO: ∀ T1 T2 st st',
  Next _ (Compare T1 T2) st (Tau _ _ (Delay _ _)) st' →
    StateO _ _ st' = StateO _ _ st.
Proof.
  intros.
  induction st; induction st'; simpl in ×.
  decompose record H; assumption.
Qed.

Lemma DeltaEvtZ: ∀ T1 T2 st1 st2 st3 e d,
    Next _ (Compare T1 T2) st1 (DLab _ _ d) st2 →
      Next _ (Compare T1 T2) st2 (ELab _ _ e) st3 →
        d = Zero.
Proof.
  intros.
  induction e; induction st1; induction st2; induction st3; simpl in ×.
  decompose record H; clear H.
  decompose record H0; clear H0.
  induction StateD1; try (elim H9); clear H9.
  revert H6; unfold DLabDly.
  case (teq_0_dec d); intros; auto.
  discriminate H6.
  decompose record H; clear H.
  decompose record H0; clear H0.
  induction StateD1; try (elim H9); clear H9.
  revert H6; unfold DLabDly.
  case (teq_0_dec d); intros; auto.
  discriminate H6.
Qed.

Lemma DeltaTau1Z: ∀ T1 T2 st1 st2 st3 e d,
    Next _ (Compare T1 T2) st1 (DLab _ _ d) st2 →
      Next _ (Compare T1 T2) st2 (Tau _ _ (Tau1 _ _ e)) st3 →
        d = Zero.
Proof.
  intros.
  induction st1; induction st2; induction st3; simpl in ×.
  decompose record H; clear H.
  decompose record H0; clear H0.
  induction StateD1; try (elim H9); clear H9.
  revert H6; unfold DLabDly.
  case (teq_0_dec d); intros; auto.
  discriminate H6.
Qed.

Lemma DeltaTau2Z: ∀ T1 T2 st1 st2 st3 e d,
    Next _ (Compare T1 T2) st1 (DLab _ _ d) st2 →
      Next _ (Compare T1 T2) st2 (Tau _ _ (Tau2 _ _ e)) st3 →
        d = Zero.
Proof.
  intros.
  induction st1; induction st2; induction st3; simpl in ×.
  decompose record H; clear H.
  decompose record H0; clear H0.
  induction StateD1; try (elim H8); clear H8.
  revert H6; unfold DLabDly.
  case (teq_0_dec d); intros; auto.
  discriminate H6.
Qed.

Lemma DeltaDelay_NZ: ∀ T1 T2 st1 st2 st3 d,
  preEvt (StateD _ _ st1) →
    Next _ (Compare T1 T2) st1 (DLab _ _ d) st2 →
      Next _ (Compare T1 T2) st2 (Tau _ _ (Delay _ _)) st3 →
        d ≠ Zero.
Proof.
  intros.
  induction st1; induction st2; induction st3; simpl in ×.
  decompose record H1; clear H1.
  clear H2 H4 H3.
  decompose record H0; clear H0.
  clear H4 H2 H1 H3.
  induction StateD1; simpl in *; try (elim H5); clear H5.
  induction StateD0; simpl in *; try (elim H); clear H.
  revert H8; unfold DLabDly; simpl; case (teq_0_dec d); intros; auto.
  discriminate H8.
Qed.

Lemma Delay_Delta1:
  ∀ T1 T2 st d st' s'1,
    Next _ T1 (State1 _ _ st) (DLab _ _ d) s'1 → Next _ (Compare T1 T2) st (Tau _ _ (Delay _ _)) st' →
      Next _ T1 (State1 _ _ st') (DLab _ _ d) s'1.
Proof.
  intros.
  induction st; induction st'; simpl in ×.
  decompose record H0; auto.
  rewrite H1; auto.
Qed.

Lemma Delay_preEvt:
  ∀ T1 T2 st st',
    Next _ (Compare T1 T2) st (Tau _ _ (Delay _ _)) st' →
      preEvt (StateD _ _ st').
Proof.
  intros.
  induction st; induction st'; simpl in ×.
  decompose record H; auto.
  rewrite H5; simpl; auto.
Qed.

Lemma DeltaDelay_skipTau2Wait:
  ∀ T1 T2 st d st' st'',
    Next _ (Compare T1 T2) st (DLab _ _ d) st' →
    Next _ (Compare T1 T2) st' (Tau _ _ (Delay _ _)) st'' →
    skipTau2Wait T1 T2 st d st''.
Proof.
  intros.
  rewrite <-(tplus_n_0 d).
  apply st2wd with d st' st'' Zero; auto.
  apply st2wn; auto.
Qed.

Lemma Tau2_skipTau2Wait:
  ∀ T1 T2 st e st', Next _ (Compare T1 T2) st (Tau _ _ (Tau2 _ _ e)) st' →
    skipTau2Wait T1 T2 st Zero st'.
Proof.
  intros.
  apply st2we with e st'; try assumption.
  apply st2wn; auto.
Qed.

Lemma DeltaDelaySkipTau2Wait:
  ∀ T1 T2 st d' st1 st2 d'' st',
    Next _ (Compare T1 T2) st (DLab _ _ d') st1 →
    Next _ (Compare T1 T2) st1 (Tau _ _ (Delay _ _)) st2 →
    skipTau2Wait T1 T2 st2 d'' st' →
    skipTau2Wait T1 T2 st (d' @+ d'') st'.
Proof.
  intros.
  apply st2wd with d' st1 st2 d''; auto.
Qed.

Lemma DelaySkipTau2Wait:
  ∀ T1 T2 st st' d st'', Next _ (Compare T1 T2) st (Tau _ _ (Delay _ _)) st' →
    skipTau2Wait T1 T2 st' d st'' →
    skipTau2Wait T1 T2 st d st''.
Proof.
  intros.
  rewrite <-(tplus_0_n d).
  apply st2wd with Zero st st' d; auto.
  apply zero_delay; reflexivity.
Qed.

Lemma Tau2SkipTau2Wait:
  ∀ T1 T2 st e st' d st'', Next _ (Compare T1 T2) st (Tau _ _ (Tau2 _ _ e)) st' →
    skipTau2Wait T1 T2 st' d st'' →
    skipTau2Wait T1 T2 st d st''.
Proof.
  intros.
  apply st2we with e st'; assumption.
Qed.

Lemma wait2_additivity: ∀ T1 T2 st d1 st' d2 st'',
  skipTau2Wait T1 T2 st d1 st' → skipTau2Wait T1 T2 st' d2 st'' →
    skipTau2Wait T1 T2 st (d1 @+ d2) st''.
Proof.
  intros.
  revert H0; induction H; intros.
  apply Tau2SkipTau2Wait with e st1; try assumption.
  apply IHskipTau2Wait; assumption.

  rewrite H2, tplus_assoc.
  apply DeltaDelaySkipTau2Wait with st1 st2; try assumption.
  apply IHskipTau2Wait; assumption.

  rewrite H0, tplus_0_n,<-H; assumption.
Qed.

Lemma skipTau2Wait_Delta1: ∀ T1 T2 st d st',
  skipTau2Wait T1 T2 st d st' → Next _ T1 (State1 _ _ st) (DLab _ _ d) (State1 _ _ st').
Proof.
  intros.
  induction H.
  apply Tau2_proj1 in H.
  rewrite H in IHskipTau2Wait; assumption.

  apply Delay_State1 in H0.
  rewrite H2.
  rewrite H0 in IHskipTau2Wait.
  apply additivity with (State1 _ _ st1); try assumption.
  apply Delta_proj1; assumption.

  rewrite H,H0.
  apply zero_delay; reflexivity.
Qed.

Lemma skipTau2Wait_proj2: ∀ T1 T2 st d st',
  skipTau2Wait T1 T2 st d st' → skipTauWait _ T2 (State2 _ _ st) d (State2 _ _ st').
Proof.
  intros.
  induction H.
  apply Tau2_proj2 in H.
  apply TauSkipTauWait with (State2 _ _ st1) e; assumption.

  apply Delay_State2 in H0.
  apply Delta_proj2 in H.
  rewrite H2.
  apply wait_additivity with (State2 _ _ st1); try assumption.
  rewrite H0 in IHskipTau2Wait; assumption.

  rewrite H,H0.
  apply wnop; apply zero_delay; reflexivity.
Qed.

Lemma skipTau2Wait_StateO: ∀ T1 T2 st d st',
  skipTau2Wait T1 T2 st d st' → StateO _ _ st' = StateO _ _ st.
Proof.
  intros.
  induction H.
  apply Tau2_StateO in H.
  apply eq_trans with (StateO _ _ st1); assumption.

  apply Delay_StateO in H0.
  apply Delta_StateO in H.
  apply eq_trans with (StateO _ _ st2); try assumption.
  apply eq_trans with (StateO _ _ st1); assumption.

  f_equal; assumption.
Qed.

Lemma skipTau2Wait_cutDelta1:
  ∀ T1 T2 st d1 st' d2 s'1,
    Next _ T1 (State1 _ _ st) (DLab _ _ (d1 @+ d2)) s'1 → skipTau2Wait _ T2 st d1 st' →
      Next _ T1 (State1 _ _ st') (DLab _ _ d2) s'1.
Proof.
  intros.
  apply skipTau2Wait_Delta1 in H0.
  apply continuity in H; destruct H.
  destruct H.
  rewrite (determinism _ _ _ _ _ _ H H0) in H1; apply H1.
Qed.

Lemma skipTau2Z_preEvt: ∀ T1 T2 st st',
  preEvt (StateD _ _ st) → skipTau2Wait T1 T2 st Zero st' → preEvt (StateD _ _ st').
Proof.
  intros.
  set (d := Zero).
  fold d in H0.
  assert (d=Zero) by reflexivity.
  generalize dependent d; intros.
  revert H H1; induction H0; intros.

  apply IHskipTau2Wait; auto.
  rewrite (Tau2_StateD _ _ _ _ _ H).
  simpl; auto.

  rewrite H4 in H2.
  apply tplus_eq_0 in H2.
  destruct H2.
  apply IHskipTau2Wait; auto.
  rewrite (Delay_StateD _ _ _ _ H0).
  simpl; auto.

  rewrite H; auto.
Qed.

Lemma DNextTau2_preEvt: ∀ T1 T2 st st' l,
  preEvt (StateD _ _ st) → isTau2 _ _ l → DNext _ (Compare T1 T2) st l st' →
    Next _ (Compare T1 T2) st l st'.
Proof.
  intros.
  destruct H1.
  assert (st'0 = st).
  induction l; try (elim H0).
  induction l; try (elim H0).
  induction st; induction st'; induction st'0; simpl in ×.
  decompose record H1; clear H1.
  rewrite H8,H6 in *; clear H8 H6 StateD2 StateO2.
  decompose record H2; clear H2.
  rewrite <-H7 in *; clear H10 StateD1 H6 StateO1 H7 State7.
  induction StateD0; simpl in *; try (elim H).
  apply pre_DLabDly_evt0 in H8.
  rewrite H8 in *; clear H8 d.
  apply zero_delay in H3; apply zero_delay in H5.
  rewrite H3,H5,DLabDly0; reflexivity.
  rewrite H3 in H2; assumption.
Qed.

Lemma ADF_EDT_Atl1Tau:
  ∀ T1 T2 st st', preEvt (StateD _ _ st) → AD T1 T2 (fun _ ⇒ False) st → skipTau2Wait T1 T2 st Zero st' → ED T1 T2 (fun _ ⇒ True) st' →
    skipTauWaitAtl1Tau _ T2 (State2 _ _ st) Zero (State2 _ _ st').
Proof.
  intros T1 T2 st st' e0; intros.
  destruct H0.
  rewrite <-(tplus_0_n Zero).
  apply stw1t with (State2 _ _ st) (State2 _ _ st1) Zero e Zero; auto.
  apply wnop; apply zero_delay; reflexivity.
  apply Tau2_proj2 in H0; assumption.
  apply skipTau2Wait_proj2 in H2; assumption.
  apply tplus_eq_0 in H4.
  destruct H4.
  rewrite H4,H5 in *; clear H4 H5 d' d''.
  apply zero_delay in H0.
  rewrite <-H0 in *; clear H0 st1.
  induction st; induction st2; simpl in *; decompose record H2; clear H2.
  induction StateD0; [elim H6 | elim e0].
  rewrite H0 in *; clear H0 st' H2.
  destruct H1.
  elim (H _ H0).
Qed.

Lemma EF_tau2_elim: ∀ T1 T2 P st,
  EF T1 T2 (isTau2 _ _ ) P st → preEvt (StateD _ _ st) → ∃ st', skipTau2Wait T1 T2 st Zero st' ∧ P st'.
Proof.
  intros.
  induction H.
  ∃ st.
  split; try assumption.
  apply st2wn; auto.

  elim IHEF; intros.
  destruct H3.
  ∃ x; split; auto.
  apply DNextTau2_preEvt in H; try assumption.
  rewrite <-(tplus_0_n Zero).
  apply wait2_additivity with st'; try assumption.
  induction l; try (elim H1).
  induction l; try (elim H1).
  apply Tau2_skipTau2Wait with l; assumption.
  apply DNextTau2_preEvt in H; try assumption.
  clear IHEF.
  induction l; try (elim H1).
  induction l; try (elim H1).
  apply Tau2_StateD in H.
  rewrite H; simpl; auto.
Qed.

Inductive NextD_inf_t T1 T2 st t: Prop :=
  NextD_inf_t_ex: ∀ st' t' st'',
    t' @<= t → t' ≠ Zero → Next _ (Compare T1 T2) st (DLab _ _ t') st' →
      Next _ (Compare T1 T2) st' (Tau _ _ (Delay _ _)) st'' →
        NextD_inf_t T1 T2 st t.

Lemma EDT_inf_t: ∀ T1 T2 st t, ED T1 T2 (fun _ ⇒ True) st → preEvt (StateD T1 T2 st) → t ≠ Zero →
  NextD_inf_t T1 T2 st t.
Proof.
  intros.
  destruct H.
  clear H2.
  destruct H.
  case (tle_total t d); intro.
  destruct t0.
  rewrite <-H3 in *; clear H3 d.
  apply continuity in H; destruct H.
  destruct H.
  clear H2 H3.
  elim (Devt0_exDelay _ _ _ _ _ H H1); intros; auto.
  split with x t x0; auto.
  apply tle_refl.

  generalize (DeltaDelay_NZ _ _ _ _ _ _ H0 H H2); intro.
  split with st'0 d st'; auto.
Qed.

Lemma skipTauWaitAtl1TauLeft:
  ∀ L T s d1 s' d2 s'',
    skipTauWait L T s d1 s' → skipTauWaitAtl1Tau L T s' d2 s'' →
      skipTauWaitAtl1Tau L T s (d1 @+ d2) s''.
Proof.
  intros.
  destruct H0.
  split with s'1 s'2 (d1@+d') e d''; try assumption.
  rewrite H0; rewrite tplus_assoc; reflexivity.
  apply wait_additivity with s'; assumption.
Qed.

Lemma skipTauWaitAtl1TauRight:
  ∀ L T s d1 s' d2 s'',
    skipTauWaitAtl1Tau L T s d1 s' → skipTauWait L T s' d2 s'' →
      skipTauWaitAtl1Tau L T s (d1 @+ d2) s''.
Proof.
  intros.
  destruct H.
  split with s'1 s'2 d' e (d'' @+ d2); try assumption.
  rewrite H; rewrite tplus_assoc; reflexivity.
  apply wait_additivity with s'; assumption.
Qed.

Lemma skipTauWait_skipTauWaitNZ: ∀ L T d st1 d1 st2 d2 st3,
  skipTauWait L T st1 d1 st2 → skipTauWaitNZ L T st2 d d2 st3 →
    skipTauWaitNZ L T st1 (d1 @+ d) (d1 @+ d2) st3.
Proof.
  intros.
  destruct H0.
  apply wtau1.
  apply skipTauWaitAtl1TauLeft with st2; assumption.
  rewrite H0 in *; clear H0 d0.
  apply skipTauWaitNZ_max_intro.
  apply wait_additivity with st2; try assumption.
  apply wnop; assumption.
Qed.

Lemma DV_EF_Tau2_evt0_EDT:
  ∀ T1 T2, diverge _ T2 → ∀ st d s'1,
    d ≠ Zero →
    Next _ T1 (State1 _ _ st) (DLab _ _ d) s'1 →
    StateD _ _ st = Devt0 → StateO _ _ st = OK →
    EF T1 T2 (isTau2 T1 T2) (ED T1 T2 (fun _ : PState T1 T2 ⇒ True)) st.
Proof.
  intros T1 T2 DV st d s'1 dnz; intros.
  induction st; simpl in ×.
  elim (DV State4 d); intros.
  rewrite H1 in *; clear H1 StateO0.
  revert H0 H; revert StateD0 State3; induction H2; intros.
  case (teq_0_dec d'); intro.
  rewrite e in *; clear e d'.
  rewrite tplus_0_n in H1; rewrite <-H1 in *; clear H1 d''.
  apply zero_delay in H; rewrite <-H in *; clear q' H.
  apply EF1 with (Tau _ _ (Tau2 _ _ l))
    (mkPState _ _ State3 q'' OK Devt0); simpl; auto.
  split with Zero {| State1 := State3; State2 := q; StateO := OK; StateD := StateD0 |}.
  apply zero_delay; reflexivity.
  rewrite H3; simpl; repeat split; auto.

  apply EF0.
  rewrite H1 in H4; apply continuity in H4; destruct H4.
  destruct H4.
  split with {| State1 := x; State2 := q'; StateO := OK; StateD := Devt0 |}; simpl; repeat split; auto.
  split with d' {| State1 := x; State2 := q'; StateO := OK; StateD := Ddly |}; simpl; repeat split; auto.
  rewrite H3; unfold DLabDly; simpl; auto.
  case (teq_0_dec d'); simpl; intros; auto.
  elim (n e).

  apply EF0.
  split with {| State1 := s'1; State2 := q'; StateO := OK; StateD := Devt0 |}; simpl; repeat split; auto.
  split with d {| State1 := s'1; State2 := q'; StateO := OK; StateD := Ddly |}; simpl; repeat split; auto.
  rewrite H0; unfold DLabDly; simpl.
  case (teq_0_dec d); simpl; intros; auto.
  elim (dnz e).
Qed.

Lemma AD_ED_cases: ∀ T1 T2 st,
  AD T1 T2 (ED T1 T2 (fun _ ⇒ True)) st ∨ ED T1 T2 (AD T1 T2 (fun _ ⇒ False)) st.
Proof.
  intros.
  case (classic (AD T1 T2 (ED T1 T2 (fun _ : PState T1 T2 ⇒ True)) st)); intro; [left; assumption|right].
  apply NNPP; intro.
  apply H; clear H; unfold AD; simpl; intros.
  apply NNPP; intro.
  apply H0; clear H0.
  split with st'; try assumption.
  clear H.
  intro; intros.
  apply H1; clear H1.
  split with st'0; auto.
Qed.

Definition right_open L (T: TTS L) st: Prop :=
  ∀ d' st', Next L T st (DLab _ _ d') st' →
    ∃ d'', ∃ st'', d'' ≠ Zero ∧ Next L T st' (DLab _ _ d'') st''.

Definition right_closed L (T: TTS L) b st: Prop :=
  ∃ st', Next L T st (DLab _ _ b) st' ∧
    ∀ d st'', Next L T st (DLab _ _ d) st'' → d @<= b.

Lemma open_or_closed: ∀ L T st,
  right_open L T st ∨ ∃ b, right_closed L T b st.
Proof.
  intros.
  elim (classic (right_open L T st)); intro.
  left; assumption.
  right.
  unfold right_open in H.
  apply not_all_ex_not in H.
  destruct H.
  apply not_all_ex_not in H.
  destruct H.
  apply imply_to_and in H.
  destruct H.
  ∃ x.
  split with x0; repeat split; intros; auto.
  elim (tle_total d x); intro; auto.
  destruct b.
  rewrite <- H2 in *; clear H2 d.
  apply continuity in H1; destruct H1.
  destruct H1.
  rewrite (determinism _ _ _ _ _ _ H H1) in *; clear H x0.
  apply not_ex_all_not with (n:=t) in H0.
  apply not_ex_all_not with (n:=st'') in H0.
  apply not_and_or in H0.
  destruct H0.
  case (teq_0_dec t); intro.
  rewrite e.
  rewrite tplus_n_0.
  apply tle_refl.
  elim (H n).
  elim (H H2).
Qed.

Definition right_open_is_unb L (T: TTS L): Prop :=
  ∀ st, right_open L T st →
    ∀ d, ∃ st', Next L T st (DLab _ _ d) st'.

Lemma all_and: ∀ T (P Q: T → Prop), (∀ x, P x ∧ Q x) → (∀ x, P x) ∧ (∀ x, Q x).
Proof.
  intros.
  split; intros; elim (H x); intros; auto.
Qed.

Lemma EDT_prj1: ∀ T1 T2 st, isDevt (StateD _ _ st) → ED T1 T2 (fun _ ⇒ True) st →
  ∃ s'1, ∃ d, Next _ T1 (State1 _ _ st) (DLab _ _ d) s'1 ∧ d ≠ Zero.
Proof.
  intros T1 T2 st ev; intros.
  destruct H.
  clear H0.
  destruct H.
  induction st; induction st'0; induction st'; simpl in ×.
  decompose record H; clear H.
  decompose record H0; clear H0.
  ∃ State5; ∃ d; split; auto.
  rewrite H6 in H8.
  revert H8 ev; unfold DLabDly; induction StateD0; simpl; intros; auto.
  revert H8; case (teq_0_dec d); simpl; intros; auto.
Qed.

Definition atleast L T b s: Prop :=
  ∃ s', Next L T s (DLab _ _ b) s'.

Definition atmost L T b s: Prop := ∀ s', ¬Next L T s (DLab _ _ b) s'.

Inductive prod_closed_cases T1 T2 st:Prop :=
  PC1: ∀ b, right_closed _ T1 b (State1 _ _ st) → atleast _ T2 b (State2 _ _ st) → prod_closed_cases T1 T2 st
| PC2: ∀ b, right_closed _ T2 b (State2 _ _ st) → atleast _ T1 b (State1 _ _ st) → prod_closed_cases T1 T2 st.

Record prod_open_cond T1 T2 st: Prop := {
  PO1: ∀ b, right_closed _ T1 b (State1 _ _ st) → atmost _ T2 b (State2 _ _ st);
  PO2: ∀ b, right_closed _ T2 b (State2 _ _ st) → atmost _ T1 b (State1 _ _ st)
}.

Lemma prod_open_imp_proj_open: ∀ T1 T2 st,
  isDevt (StateD _ _ st) → ED T1 T2 (fun _ ⇒ True) st → AD T1 T2 (ED T1 T2 (fun _ ⇒ True)) st → prod_open_cond T1 T2 st.
Proof.
  intros T1 T2 st ev; intros.
  split; intros.
  assert (StateO _ _ st = OK) as ok.
  clear H1; induction st; inversion_clear H; simpl in ×.
  induction st'; simpl in *; destruct H1; simpl in ×.
  induction st'; simpl in ×.
  decompose record H1; clear H1 H2.
  clear H8 H3 H5.
  decompose record H; clear H.
  rewrite H8 in H6; clear H8 StateD2 H5 H3 H1.
  unfold DLabDly in H6.
  induction StateD0; try (elim ev).
  destruct H2; auto.
  revert H6; case (teq_0_dec d); simpl; intros; auto.
  elim H6.
  elim (n H).

  assert (b ≠ Zero) as nz.
  apply EDT_prj1 in H; auto.
  decompose record H; clear H.
  intro.
  rewrite H in *; clear H b.
  destruct H1.
  destruct H.
  generalize (H1 x0 x H2); clear H1; intro.
  apply tle_n_0 in H1.
  elim (H4 H1).

  intro; intro.
  destruct H1.
  destruct H1.
  assert (DNext _ (Compare T1 T2) st (Tau _ _ (Delay _ _)) (mkPState _ _ x s' OK Devt0)).
  split with b (mkPState _ _ x s' OK Ddly); induction st; simpl in *; repeat split; intros; auto.
  induction StateD0; try (elim ev); clear ev.
  unfold DLabDly.
  case (teq_0_dec b); intros; auto.
  elim (nz e).

  generalize (H0 _ H4); clear H0; intro.
  apply EDT_prj1 in H0; try (apply I).
  decompose record H0; clear H0; simpl in ×.
  generalize (additivity _ _ _ _ _ _ _ H1 H5); intro.
  generalize (H3 _ _ H0); intro.
  destruct H6.
  rewrite tplus_assoc in H6.
  revert H6; rewrite <-(tplus_n_0 b) at 2; intro.
  apply tplus_opp_l in H6.
  apply eq_sym in H6; apply tplus_eq_0 in H6.
  apply proj1 in H6.
  elim (H7 H6).

  admit. Qed.

Lemma right_open_prod: ∀ T1 T2,
  right_open_is_unb _ T1 → right_open_is_unb _ T2 →
    ∀ st, isDevt (StateD _ _ st) → StateO _ _ st = OK → ED T1 T2 (fun _ ⇒ True) st → AD T1 T2 (ED T1 T2 (fun _ ⇒ True)) st →
      ∀ d, ∃ st', Next _ (Compare T1 T2) st (DLab _ _ d) st'.
Proof.
  unfold right_open_is_unb; simpl; intros.
  rename H2 into ok.
  rename H3 into nz.
  rename H4 into H2.
  generalize (H (State1 _ _ st)); clear H; intros.
  generalize (H0 (State2 _ _ st)); clear H0; intros.
  case (teq_0_dec d); intro.
  ∃ st.
  rewrite e.
  clear H H0 H2.
  induction st; simpl in *; repeat split; try (apply zero_delay); auto.
  unfold DLabDly; induction StateD0; try (elim H1).
  case (teq_0_dec Zero); intro; auto.
  contradiction n; reflexivity.
  elim (prod_open_imp_proj_open _ _ _ H1 nz H2); intros.
  elim (open_or_closed _ _ (State1 _ _ st)); intro; elim (open_or_closed _ _ (State2 _ _ st)); intro.

  clear PO3 PO4.
  elim (H H3 d); clear H H3; intros.
  elim (H0 H4 d); clear H0 H4; intros.
  ∃ (mkPState _ _ x x0 OK (DLabDly d (StateD _ _ st))); induction st; simpl; repeat split; intros; auto.

  destruct H4.
  generalize (PO4 _ H4); clear PO3 PO4; intros.
  elim (H H3 x); clear H H3 H0; intros.
  elim (H5 x0 H).

  destruct H3.
  generalize (PO3 _ H3); clear PO3 PO4; intros.
  elim (H0 H4 x); clear H0 H4 H; intros.
  elim (H5 x0 H).

  destruct H3.
  destruct H4.
  elim (tle_total x x0); intro.
  generalize (PO3 _ H3); clear PO3 PO4; intros.
  destruct H4.
  destruct H4.
  destruct a.
  rewrite <-H7 in H4; apply continuity in H4; destruct H4.
  destruct H4.
  elim (H5 _ H4).

  generalize (PO4 _ H4); clear PO3 PO4; intros.
  destruct H3.
  destruct H3.
  destruct b.
  rewrite <-H7 in H3; apply continuity in H3; destruct H3.
  destruct H3.
  elim (H5 _ H3).
Qed.

Lemma one_step: ∀ T1 T2 s1 s2 st1 st2 st3 d1 d2 d dl,
  skipTau2Wait T1 T2 (mkPState _ _ s1 s2 OK dl) d1 st1 →
  preEvt (StateD _ _ st1) → d2 ≠ Zero →
  AD T1 T2 (pCheckFrom T1 T2) st1 →
    Next (Event + Event) (Compare T1 T2) st1 (DLab _ _ d) st2 →
      Next _ _ st2 (Tau _ _ (Delay T1 T2)) st3 → d2 @<= d →
   ∃ d3, ∃ st',
    d3 @<= d2 ∧
    skipTauWaitNZ Event T2 (State2 _ _ st1) d2 d3 st' ∧
    timedPred T1 T2 (d1 @+ d2) dl s1 s2 (d1 @+ d3) st'.
Proof.
  intros.
  destruct H5.
  rewrite <-H5 in *; clear H5 d.
  apply continuity in H3; destruct H3; destruct H3.
  clear H4 st3 st2 H5 t.
  elim (Devt0_exDelay _ _ _ _ _ H3 H1); try assumption; intros.
  generalize (H2 x0 (DNprf _ _ _ _ _ _ _ H3 H4)); intro.
  ∃ d2; ∃ (State2 _ _ x0).
  split; try (apply tle_refl).
  split.
  apply skipTauWaitNZ_max_intro.
  generalize (DeltaDelay_skipTau2Wait _ _ _ _ _ _ H3 H4); intro.
  rewrite <-(tplus_n_0 d2).
  apply wait_additivity with (State2 _ _ x0).
  apply skipTau2Wait_proj2 in H6; assumption.
  apply wnop.
  apply zero_delay; reflexivity.
  apply tpTau with x0; auto.
  apply wait2_additivity with st1; try assumption.
  rewrite <-(tplus_n_0 d2).
  apply wait2_additivity with x0; try assumption.
  apply (DeltaDelay_skipTau2Wait _ _ _ _ _ _ H3 H4).
  apply Delay_StateD in H4.
  apply st2wn; auto.
Qed.

Theorem pCheckFrom_check:
  ∀ T1 T2, diverge _ T1 → diverge _ T2 → nonZenoTauPath _ T2 →
    right_open_is_unb _ T1 → right_open_is_unb _ T2 →
    ∀ s1 s2 dl, preEvt dl → pCheckFrom T1 T2 (mkPState _ _ s1 s2 OK dl) → checkFrom _ T1 T2 s1 s2.
Proof.
  intros T1 T2 DV1 DV2 NZTP ro1 ro2.
  cofix; intros s1 s2 dl pdl; intros.
  apply CFE; intros.
  elim (pCheckFrom_NextEvt _ _ _ H _ _ H0); simpl; intros.
  destruct H1.
  destruct H1.
  destruct H2.
  ∃ x; ∃ x0; split; [idtac|split]; auto.

  inversion_clear H; simpl in ×.
  clear H4.
  inversion_clear H6.
  assert (DNext (Event + Event) (Compare T1 T2)
      {| State1 := s1; State2 := s2; StateO := OK; StateD := dl |}
      (ELab _ _ (inl _ e))
      {| State1 := s'1; State2 := s2; StateO := WAIT e; StateD := Devt0 |}); intros.
  split with Zero (mkPState _ _ s1 s2 OK dl); simpl; repeat split; trivial.
  apply zero_delay; reflexivity.
  apply zero_delay; reflexivity.
  left; reflexivity.
  revert pdl; case dl; simpl; intros; auto.
  apply eq_sym; apply DLabDly0.
  elim pdl.
  generalize (H e (mkPState _ _ s'1 s2 (WAIT e) Devt0) H6); clear H H4 H7 H6; intro.
  apply pCheckFrom_check with Devt0; simpl; trivial.

  inversion_clear H; simpl in ×.
  clear H1.
  inversion_clear H3.
  assert (DNext (Event + Event) (Compare T1 T2)
      {| State1 := s1; State2 := s2; StateO := OK; StateD := dl |}
      (Tau _ _ (Tau1 _ _ e))
      {| State1 := s'1; State2 := s2; StateO := OK; StateD := Devt0 |}); intros.
  split with Zero (mkPState _ _ s1 s2 OK dl); simpl; repeat split; trivial.
  apply zero_delay; reflexivity.
  apply zero_delay; reflexivity.
  left; reflexivity.
  revert pdl; case dl; simpl; intros; auto.
  apply eq_sym; apply DLabDly0.
  elim pdl.
  generalize (H1 e (mkPState _ _ s'1 s2 OK Devt0) H3); clear H H1 H4 H3; intro.
  apply pCheckFrom_check with Devt0; simpl; trivial.

  elim (teq_0_dec d); intro.
  rewrite a in *; clear a d.
  apply zero_delay in H0.
  rewrite <-H0 in *; clear H0 s'1.
  ∃ s2; split.
  apply wnop; apply zero_delay; reflexivity.
  apply pCheckFrom_check with dl; trivial.

  elim (NZTP (timedPred T1 T2 d dl s1 s2)) with d s2; intros; trivial.
  destruct H1.
  destruct H2.
  contradiction H2; apply tle_refl.

  ∃ x; split; try assumption.
  apply pCheckFrom_check with (StateD _ _ st); simpl; trivial.
  apply pCheckFrom_preEvt; assumption.

  induction st; simpl in ×.
  rewrite H4 in *; clear H4 State4.
  generalize (skipTau2Wait_Delta1 _ _ _ _ _ H2); simpl; intro.
  rewrite (determinism _ _ _ _ _ _ H0 H4); clear H4.
  generalize (skipTau2Wait_StateO _ _ _ _ _ H2); simpl; intro.
  rewrite H4 in H3; apply H3.

  ∃ x; split.
  apply wnop; assumption.
  rewrite (determinism _ _ _ _ _ _ H0 H3).
  apply pCheckFrom_check with Devt0; simpl; trivial.

  inversion_clear H1.
  contradiction H4.
  ∃ d2; assumption.

  clear pCheckFrom_check.
  rewrite <-H3 in *; clear H3 d.
  generalize (skipTau2Wait_Delta1 _ _ _ _ _ H4); simpl; intro.
  apply continuity in H0; destruct H0.
  destruct H0.
  rewrite (determinism _ _ _ _ _ _ H0 H1) in *; clear H0 x.
  generalize (pCheckFrom_preEvt _ _ _ H5); intro.
  generalize (pCheckFrom_state _ _ _ H5); intro.
  assert (StateD T1 T2 st0 = Devt0) by (
    revert H0; generalize (StateD _ _ st0); intro dd; induction dd; simpl; intro ff; auto; elim ff).
  generalize (DV_EF_Tau2_evt0_EDT _ _ DV2 st0 d2 _ H2 H3 H8 H7); intro.
  apply pCheckFrom_EFD in H5; try (apply H9); clear H9.
  apply EF_tau2_elim in H5; try assumption; destruct H5.
  destruct H5.
  destruct H9.
  elim (AD_ED_cases _ _ x); intro.

  rewrite <-H6.
  generalize (skipTau2Wait_StateO _ _ _ _ _ H5); intro.
  rewrite H7 in H12.
  generalize (skipTau2Z_preEvt _ _ _ _ H0 H5); intro.
  apply right_open_prod with (d:=d2) in H11; try assumption.
  destruct H11.
  elim (Devt0_exDelay _ _ _ _ _ H11 H2); try assumption; intros.
  assert (∃ d3 : Time,
    ∃ st'1 : State Event T2,
    d3 @<= d2 ∧
    skipTauWaitNZ Event T2 (State2 T1 T2 x) d2 d3 st'1 ∧
    timedPred T1 T2 (d1 @+ d2) dl s1 s2 (d1 @+ d3) st'1).
  apply one_step with x0 x1 d2; try assumption.
  rewrite <-(tplus_n_0 d1).
  apply wait2_additivity with st0; assumption.
  apply tle_refl.
  destruct H15.
  destruct H15.
  destruct H15.
  destruct H16.
  ∃ x2; ∃ x3; split; auto.
  split; auto.
  rewrite <-(tplus_0_n d2).
  apply skipTau2Wait_proj2 in H5.
  rewrite <-(tplus_0_n x2).
  apply skipTauWait_skipTauWaitNZ with (State2 _ _ x); assumption.

  clear H9.
  destruct H11.
  destruct H9.
  case (tle_lt_cases d2 d); intros.
  rewrite <-H6.
  assert (∃ d3 : Time,
    ∃ st'1 : State Event T2,
    d3 @<= d2 ∧
    skipTauWaitNZ Event T2 (State2 T1 T2 x) d2 d3 st'1 ∧
    timedPred T1 T2 (d1 @+ d2) dl s1 s2 (d1 @+ d3) st'1).
  apply one_step with st'0 st' d; try assumption.
  rewrite <-(tplus_n_0 d1).
  apply wait2_additivity with st0; assumption.
  apply skipTau2Z_preEvt in H5; assumption.
  destruct H14.
  destruct H14.
  destruct H14.
  destruct H15.
  ∃ x0; ∃ x1; split; auto.
  split; auto.
  rewrite <-(tplus_0_n d2).
  apply skipTau2Wait_proj2 in H5.
  rewrite <-(tplus_0_n x0).
  apply skipTauWait_skipTauWaitNZ with (State2 _ _ x); assumption.

  destruct H13.
  destruct H13.
  rewrite H13 in *; clear H13 d2.
  assert (DNext _ _ x (Tau _ _ (Delay _ _)) st') by (split with d st'0; assumption).
  generalize (H10 _ H13); clear H10; intro.
  apply pCheckFrom_EFD in H10.
  apply EF_tau2_elim in H10.
  destruct H10 as [st'2 [H15 [H16 H17]]].
  apply EDT_inf_t with (t:=x0) in H16; auto.
  inversion_clear H16.
  generalize (H17 _ (DNprf _ _ _ _ _ _ _ H19 H20)); clear H17; intro.
  ∃ (d@+t'); ∃ (State2 _ _ st'').
  split.
  apply tle_mono_l; assumption.
  split.
  apply wtau1.
  assert (DNext _ (Compare T1 T2) st'2 (Tau _ _ (Delay _ _)) st'') as exd by (split with t' st'1; assumption).
  apply skipTau2Wait_proj2 in H5.
  rewrite <-(tplus_0_n (d@+t')).
  rewrite <-H6.
  apply skipTauWaitAtl1TauLeft with (State2 _ _ x); try assumption.
  generalize (DeltaDelay_skipTau2Wait _ _ _ _ _ _ H9 H12); clear H9 H12; intro.
  apply skipTau2Wait_proj2 in H9.
  apply skipTauWaitAtl1TauLeft with (State2 _ _ st'); try assumption.
  rewrite <-(tplus_n_0 t').
  apply skipTauWaitAtl1TauRight with (State2 _ _ st''); try assumption.
  rewrite <-(tplus_0_n t').
  generalize (DeltaDelay_skipTau2Wait _ _ _ _ _ _ H19 H20); clear H20 H19; intro.
  apply skipTau2Wait_proj2 in H12.
  apply skipTauWaitAtl1TauRight with (State2 _ _ st'2); try assumption.
  assert (ED T1 T2 (fun _ ⇒ True) st'2) by (∃ st''; auto); clear exd.
  apply ADF_EDT_Atl1Tau; auto.
  destruct H13.
  apply Delay_preEvt in H19; assumption.
  apply wnop; apply zero_delay; reflexivity.

  apply tpTau with st''; auto.
  apply wait2_additivity with st0; try assumption.
  rewrite <-(tplus_0_n (d@+t')).
  apply wait2_additivity with x; try assumption.
  apply DeltaDelaySkipTau2Wait with st'0 st'; try assumption.
  rewrite <-(tplus_0_n t').
  apply wait2_additivity with st'2; try assumption.
  apply DeltaDelay_skipTau2Wait with st'1; assumption.
  apply skipTau2Z_preEvt with st'; try assumption.
  apply Delay_preEvt in H12; assumption.
  apply Delay_preEvt in H12; assumption.

  apply DV_EF_Tau2_evt0_EDT with x0 s'1; auto.
  apply skipTau2Wait_Delta1 in H5.
  apply zero_delay in H5.
  apply Delay_State1 in H12.
  rewrite H12.
  apply Delta_proj1 in H9.
  destruct H13.
  apply Delta_proj1 in H13.
  apply Delay_State1 in H15.
  rewrite <-H15 in H13; clear H15 st'1.
  rewrite <-H12 in *; clear H12 st'0.
  rewrite <- H5 in *; clear H5 x.
  apply skipTau2Wait_Delta1 in H4; simpl in H4.
  apply continuity in H3; destruct H3; destruct H3.
  rewrite <-(determinism _ _ _ _ _ _ H3 H9); assumption.
  apply pCheckFrom_preEvt in H10.
  revert H10; case (StateD _ _ st'); simpl; intros; auto.
  elim H10.
  apply pCheckFrom_state in H10; assumption.

  clear H7 H6 H5; apply False_ind.
  rewrite <- (tplus_n_0 d),H4 in H3.
  apply tplus_opp_l in H3.
  apply (H2 H3).

  apply tpTau with {| State1 := s1; State2 := s2; StateO := OK; StateD := dl |}.
  apply st2wn; auto.
  apply H.
  reflexivity.

  inversion_clear H.
  inversion_clear H3.
  clear H H1 H2 H4 H5.
  inversion_clear H6.
  apply NNPP; intro.
  generalize (not_ex_all_not _ _ H1); clear H1; intro.
  generalize (fun n ⇒ not_and_or _ _ (H1 n)); clear H1; intro.
  generalize (fun n ⇒ or_to_imply _ _ (H1 n)); clear H1; intro.
  assert (~~deadlock _ T1 s1) by tauto; clear H0.
  apply H2; clear H2.
  change s1 with (State1 _ _ {| State1 := s1; State2 := s2; StateO := OK; StateD := dl |}).
  apply nDL1_ndeadlock.
  apply H; clear H.
  induction dl; try (elim pdl); clear pdl.
  revert H1; revert s1 s2; cofix; simpl in *; intros.
  split; intros.
  generalize (H1 s2); clear H1; intro.
  assert (skipTauWait Event T2 s2 Zero s2) by (apply wnop; apply zero_delay; reflexivity).
  apply H in H0; clear H.
  apply ndeadlock_nDL2; auto.

  destruct H.
  induction st'0; induction st'; simpl in ×.
  destruct l; try (elim H0).
  destruct l; try (elim H0); clear H0.
  decompose record H2; clear H2; subst.
  decompose record H; clear H; subst.
  clear H3.
  apply pCheckFrom_check0; intros.
  apply H1.
  unfold DLabDly in H5.
  revert H5; case (teq_0_dec d); intros deq0 H5; try (elim H5); try tauto.
  rewrite deq0 in *; clear deq0 d.
  apply zero_delay in H4; rewrite <-H4 in *; clear H4 State4.
  apply TauSkipTauWait with State6 l; auto.
Qed.

Inductive hasInit E (T: TTS E): Prop :=
 exInit: ∀ st, Init E T st → hasInit E T.

Lemma pCheck_check:
  ∀ T1 T2, hasInit _ T2 → diverge _ T1 → diverge _ T2 → right_open_is_unb _ T1 → right_open_is_unb _ T2 → nonZenoTauPath Event T2 → pCheck T1 T2 → check _ T1 T2.
Proof.
  intros T1 T2 II DV1 DV2 ro1 ro2 NZTP H.
  intro; intros.
  unfold pCheck in H.
  inversion_clear II.
  ∃ st.
  split; auto.
  apply pCheckFrom_check with Devt0; simpl; auto.
  apply H.
  simpl; split; auto.
Qed.

Theorem pCheck_refines:
  ∀ T1 T2, diverge _ T1 → diverge _ T2 → hasInit _ T2 → nonZenoTauPath Event T2 → right_open_is_unb _ T1 → right_open_is_unb _ T2 → pCheck T1 T2 → refines _ T1 T2.
Proof.
  intros.
  apply check_refines; auto.
  apply pCheck_check; auto.
Qed.