proposition: Theorem Equiv3 : forall (Sini : S) (P : Stream S -> Prop), Always Sini P <-> ~ Posible Sini (fun s : Stream S => ~ P s).
proof: Proof. unfold iff, Always, not in |- *; intros; split. intros H H0; inversion_clear H0. generalize (H x H1); elim H2; intros. inversion_clear H3 in H0. apply (H0 H4). inversion_clear H4. apply (H3 H6). generalize Sini; cofix u. simple destruct x; intros; constructor. elim (classic (P (s ^ s0))); [ trivial | intros ]. absurd (Posible Sini0 (fun s : Stream S => ~ P s)). assumption. apply posible with (1 := H0). constructor 1; assumption. elim H0; simpl in |- *; intros. apply (u (hd s0)); intros. generalize H0; clear H0; generalize H3; clear H3. rewrite <- H1; case s0; simpl in |- *; intros. apply (notPosible (P:=fun s : Stream S => ~ P s) H H0); assumption. inversion_clear H2; simpl in |- *. unfold isTraceFrom in |- *; split; trivial. unfold isTraceFrom in |- *; split; trivial. Qed.
imports: Streams time_clocks Classical