proposition: Theorem Equiv3_T : forall (Sini : S * Instant) (P : Stream (S * Instant) -> Prop), Always_T Sini P <-> ~ Posible_T Sini (fun s : Stream (S * Instant) => ~ P s).
proof: Proof. unfold iff, Always_T, not in |- *; intros; split. intros H H0; inversion_clear H0. generalize (H x H1); elim H2; intros. inversion_clear H3 in H0. elim H0; intros. elim (H6 (H4 H3)). inversion_clear H4. apply (H3 H6). generalize Sini; cofix u. simple destruct x; intros; constructor. intro; elim (classic (P (p ^ s))); [ trivial | intros ]. absurd (Posible_T Sini0 (fun s : Stream (S * Instant) => ~ P s)). assumption. apply posible_T with (1 := H0). constructor 1; split; assumption. elim H0; simpl in |- *; intros. apply (u (hd s)); intros. generalize H0; clear H0; generalize H3; clear H3. rewrite <- H1; case s; simpl in |- *; intros. apply (notPosible_T (P:=fun s : Stream (S * Instant) => ~ P s) H H0); assumption. unfold isTraceFrom_T in |- *; inversion_clear H2; simpl in |- *. split; trivial. split; trivial. Qed.
imports: time_clocks ctl Classical