proposition: Theorem Equiv4 : forall (Sini : S) (P : Stream S -> Prop), SafePath Sini P <-> ~ Inevitable Sini (fun s : Stream S => ~ P s).
proof: Proof. unfold iff, Inevitable, not in |- *; intros; split. intro sp; inversion sp; intros. generalize H0; elim (H1 x H); intros. inversion_clear H3 in H2. apply (H2 H4). apply H3; inversion_clear H4; assumption. intro H; elim (not_all_ex_not (Stream S) (fun x : Stream S => isTraceFrom Sini x -> ExistsS (fun s : Stream S => P s -> False) x) H). intros. generalize (not_imply_elim2 (isTraceFrom Sini x) (ExistsS (fun s : Stream S => ~ P s) x) H0). generalize (not_imply_elim (isTraceFrom Sini x) (ExistsS (fun s : Stream S => ~ P s) x) H0); intros. apply safePath 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 (s ^ s0))); [ trivial | intro ]. elim (H2 (Here (P:=fun s : Stream S => ~ P s) H3)). apply u with (Sini := hd s0). generalize H2; clear H2; case s0; unfold not in |- *; intros. apply (not_EX H2 H3). elim H1; intros ig trace; inversion_clear trace. unfold isTraceFrom in |- *; split; trivial. unfold isTraceFrom in |- *; split; trivial. Qed.
imports: Streams time_clocks Classical