proposition: Theorem Equiv4_T : forall (Sini : S * Instant) (P : Stream (S * Instant) -> Prop), SafePath_T Sini P <-> ~ Inevitable_T Sini (fun s : Stream (S * Instant) => ~ P s).
proof: Proof. unfold iff, Inevitable_T, not in |- *; intros; split. intro sp; inversion sp; intros. generalize H0; elim (H1 x H); intros. inversion_clear H3 in H2. elim H2; intros. apply (H6 (H4 H3)). apply H3; inversion_clear H4; assumption. intro H; elim (not_all_ex_not (Stream (S * Instant)) (fun x : Stream (S * Instant) => isTraceFrom_T Sini x -> ExistsS (fun s : Stream (S * Instant) => bound (snd (hd s)) /\ (P s -> False)) x) H). intros. generalize (not_imply_elim2 (isTraceFrom_T Sini x) (ExistsS (fun s : Stream (S * Instant) => bound (snd (hd s)) /\ (P s -> False)) x) H0). generalize (not_imply_elim (isTraceFrom_T Sini x) (ExistsS (fun s : Stream (S * Instant) => bound (snd (hd s)) /\ (P s -> False)) x) H0); intros. apply safePath_T with (1 := H1). generalize H1; clear H1; generalize H2; clear H2. generalize x; generalize Sini; cofix u. simple destruct x0; intros; constructor. elim (classic (P (p ^ s))); [ trivial | intros ]. cut (ExistsS (fun s0 : Stream (S * Instant) => bound (snd (hd s0)) /\ (P s0 -> False)) (p ^ s)). intro ex; elim (H2 ex). apply Here with (P := fun s : Stream (S * Instant) => bound (snd (hd s)) /\ (P s -> False)). split; assumption. apply u with (Sini := hd s). generalize H2; clear H2; case s; unfold not in |- *; intros. apply (not_EX H2 H3). unfold isTraceFrom_T in |- *; elim H1; intros ig trace; inversion_clear trace. split; trivial. split; trivial. Qed.
imports: time_clocks ctl Classical