proposition: Theorem Equiv1_T : forall (Sini : S * Instant) (P : Stream (S * Instant) -> Prop), Posible_T Sini P <-> EX_Until_bound Sini (fun _ : Stream (S * Instant) => True) P.
proof: Proof. unfold iff in |- *; intros; split; intro. inversion_clear H. apply ExUntil_bound with (P := fun _ : Stream (S * Instant) => True) (1 := H0). elim H1. simple destruct x0; simpl in |- *. simple destruct p; simple destruct 1; simpl in |- *; intros. constructor 2; assumption. simple destruct s; intros. constructor 1; trivial. inversion_clear H. apply posible_T with (1 := H0). elim H1. simple destruct s; intros. constructor 2; assumption. intros; constructor 1; simpl in |- *; split; assumption. Qed.
imports: time_clocks ctl