(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Set Implicit Arguments.
Unset Strict Implicit.

Require Import time_clocks. (* Temporal notions for discrete time *)
Require Import ctl.

Infix "^" := Cons.

Section TemporalOperators_TCTL.

(*** operators TCTL with co-inductives types: definitions and properties ***)
  Variable Label : Set.               (* labels: dicrete transitions *) 
  Variable S : Set.               (* states                      *) 
  Variable tr : S -> Label -> S -> Prop. (* transitions                 *)
  Variable inv : S -> Prop.         (* location invariants         *)
  Variable inc : S -> Instant -> S. (* increase clocks of states   *)  
  Variable bound : Instant -> Prop.     (* Belonging to temporal intervals *)
 
  Notation State_T := (S * Instant)%type (only parsing).
  Notation SPath_T := (Stream (S * Instant)) (only parsing).


  (* Ejecution traces *)

  CoInductive isTrace_T : Stream (S * Instant) -> Prop :=
    | isTraceTick_T :
        forall (x : Stream (S * Instant)) (s : S) (t : Instant),
        inv (inc s tick) ->
        isTrace_T ((inc s tick, Inc t) ^ x) ->
        isTrace_T ((s, t) ^ (inc s tick, Inc t) ^ x)
    | isTraceDisc_T :
        forall (x : Stream (S * Instant)) (s1 s2 : S) 
          (t : Instant) (l : Label),
        tr s1 l s2 ->
        inv s2 ->
        isTrace_T ((s2, t) ^ x) -> isTrace_T ((s1, t) ^ (s2, t) ^ x). 

  Definition isTraceFrom_T (Sini : S * Instant) (x : Stream (S * Instant)) :=
    Sini = hd x /\ isTrace_T x.
 
 
  (* operator Until *)

  Inductive Until_bound (P Q : Stream (S * Instant) -> Prop) :
  Stream (S * Instant) -> Prop :=
    | UntilFurther_bound :
        forall (s : S * Instant) (x : Stream (S * Instant)),
        P (s ^ x) -> Until_bound P Q x -> Until_bound P Q (s ^ x)
    | UntilHere_bound :
        forall (s : S) (t : Instant) (x : Stream (S * Instant)),
        bound t -> Q ((s, t) ^ x) -> Until_bound P Q ((s, t) ^ x).

  Inductive EX_Until_bound (Sini : S * Instant)
  (P Q : Stream (S * Instant) -> Prop) : Prop :=
      ExUntil_bound :
        forall x : Stream (S * Instant),
        isTraceFrom_T Sini x -> Until_bound P Q x -> EX_Until_bound Sini P Q.

  Definition FA_Until_bound (Sini : S * Instant)
    (P Q : Stream (S * Instant) -> Prop) :=
    forall x : Stream (S * Instant),
    isTraceFrom_T Sini x -> Until_bound P Q x.


  (* Init => FA[](bound t) P *)

  Definition Always_T (Sini : S * Instant)
    (P : Stream (S * Instant) -> Prop) :=
    forall x : Stream (S * Instant),
    isTraceFrom_T Sini x ->
    ForAllS (fun s : Stream (S * Instant) => bound (snd (hd s)) -> P s) x.


  (* Init => FA<>(bound t) P *)

  Definition Inevitable_T (Sini : S * Instant)
    (P : Stream (S * Instant) -> Prop) :=
    forall x : Stream (S * Instant),
    isTraceFrom_T Sini x ->
    ExistsS (fun s : Stream (S * Instant) => bound (snd (hd s)) /\ P s) x.


  (* Init => EX<>(bound t) P *)

  Inductive Posible_T (Sini : S * Instant) (P : Stream (S * Instant) -> Prop)
  : Prop :=
      posible_T :
        forall x : Stream (S * Instant),
        isTraceFrom_T Sini x ->
        ExistsS (fun s : Stream (S * Instant) => bound (snd (hd s)) /\ P s) x ->
        Posible_T Sini P.


  (* Init => EX[](bound t) P *)

  Inductive SafePath_T (Sini : S * Instant)
  (P : Stream (S * Instant) -> Prop) : Prop :=
      safePath_T :
        forall x : Stream (S * Instant),
        isTraceFrom_T Sini x ->
        ForAllS (fun s : Stream (S * Instant) => bound (snd (hd s)) -> P s) x ->
        SafePath_T Sini P.

 
  (**************************************************************************)
  (*                            Some Properties                             *)
  (**************************************************************************)

  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.
(* Goal: forall (Sini : prod S Instant) (P : forall _ : Stream (prod S Instant), Prop), iff (Posible_T Sini P) (EX_Until_bound Sini (fun _ : Stream (prod S Instant) => True) P) *)
    unfold iff in |- *; intros; split; intro.
(* Goal: Posible_T Sini P *)
    inversion_clear H.
    apply
     ExUntil_bound with (P := fun _ : Stream (S * Instant) => True) (1 := H0).
(* Goal: @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (P s)) x *)
    elim H1.
(* Goal: forall (x : Stream (prod S Instant)) (_ : and (bound (@snd S Instant (@hd (prod S Instant) x))) (P x)), Until_bound (fun _ : Stream (prod S Instant) => True) P x *)
(* Goal: forall (x : Stream (prod S Instant)) (s : prod S Instant) (_ : @ExistsS (prod S Instant) (fun s0 : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s0))) (P s0)) x) (_ : Until_bound (fun _ : Stream (prod S Instant) => True) P x), Until_bound (fun _ : Stream (prod S Instant) => True) P (@Cons (prod S Instant) s x) *)
(* Goal: Posible_T Sini P *)
    simple destruct x0; simpl in |- *.
(* Goal: forall (p : prod S Instant) (s : Stream (prod S Instant)) (_ : and (bound (@snd S Instant p)) (P (@Cons (prod S Instant) p s))), Until_bound (fun _ : Stream (prod S Instant) => True) P (@Cons (prod S Instant) p s) *)
(* Goal: forall (x : Stream (prod S Instant)) (s : prod S Instant) (_ : @ExistsS (prod S Instant) (fun s0 : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s0))) (P s0)) x) (_ : Until_bound (fun _ : Stream (prod S Instant) => True) P x), Until_bound (fun _ : Stream (prod S Instant) => True) P (@Cons (prod S Instant) s x) *)
(* Goal: Posible_T Sini P *)
    simple destruct p; simple destruct 1; simpl in |- *; intros.
(* Goal: @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (P s)) (@Cons (prod S Instant) s x0) *)
(* Goal: @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (P s)) (@Cons (prod S Instant) (@pair S Instant s t) x0) *)
    constructor 2; assumption.
(* Goal: forall (s : prod S Instant) (x : Stream (prod S Instant)) (_ : True) (_ : Until_bound (fun _ : Stream (prod S Instant) => True) P x) (_ : @ExistsS (prod S Instant) (fun s0 : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s0))) (P s0)) x), @ExistsS (prod S Instant) (fun s0 : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s0))) (P s0)) (@Cons (prod S Instant) s x) *)
(* Goal: forall (s : S) (t : Instant) (x : Stream (prod S Instant)) (_ : bound t) (_ : P (@Cons (prod S Instant) (@pair S Instant s t) x)), @ExistsS (prod S Instant) (fun s0 : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s0))) (P s0)) (@Cons (prod S Instant) (@pair S Instant s t) x) *)
    simple destruct s; intros.
(* Goal: forall (p : prod S Instant) (s : Stream (prod S Instant)) (s0 : prod S Instant) (_ : @ExistsS (prod S Instant) (fun s1 : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s1))) (P s1)) (@Cons (prod S Instant) p s)) (_ : Until_bound (fun _ : Stream (prod S Instant) => True) P (@Cons (prod S Instant) p s)), Until_bound (fun _ : Stream (prod S Instant) => True) P (@Cons (prod S Instant) s0 (@Cons (prod S Instant) p s)) *)
(* Goal: @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (P s)) x *)
    constructor 1; trivial.
(* Goal: Posible_T Sini P *)
    inversion_clear H.
(* Goal: Posible_T Sini0 (fun s : Stream (prod S Instant) => not (P s)) *)
(* Goal: @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) s *)
    apply posible_T with (1 := H0).
(* Goal: @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (P s)) x *)
    elim H1.
(* Goal: forall (s : prod S Instant) (x : Stream (prod S Instant)) (_ : True) (_ : Until_bound (fun _ : Stream (prod S Instant) => True) P x) (_ : @ExistsS (prod S Instant) (fun s0 : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s0))) (P s0)) x), @ExistsS (prod S Instant) (fun s0 : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s0))) (P s0)) (@Cons (prod S Instant) s x) *)
(* Goal: forall (s : S) (t : Instant) (x : Stream (prod S Instant)) (_ : bound t) (_ : P (@Cons (prod S Instant) (@pair S Instant s t) x)), @ExistsS (prod S Instant) (fun s0 : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s0))) (P s0)) (@Cons (prod S Instant) (@pair S Instant s t) x) *)
    simple destruct s; intros.
(* Goal: @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (P s)) (@Cons (prod S Instant) s x0) *)
(* Goal: @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (P s)) (@Cons (prod S Instant) (@pair S Instant s t) x0) *)
    constructor 2; assumption.
(* Goal: forall (s : S) (t : Instant) (x : Stream (prod S Instant)) (_ : bound t) (_ : P (@Cons (prod S Instant) (@pair S Instant s t) x)), @ExistsS (prod S Instant) (fun s0 : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s0))) (P s0)) (@Cons (prod S Instant) (@pair S Instant s t) x) *)
    intros; constructor 1; simpl in |- *; split; assumption.
  Qed.


  Theorem Equiv2_T :
   forall (Sini : S * Instant) (P : Stream (S * Instant) -> Prop),
   Inevitable_T Sini P <->
   FA_Until_bound Sini (fun _ : Stream (S * Instant) => True) P.
  Proof.
(* Goal: forall (Sini : prod S Instant) (P : forall _ : Stream (prod S Instant), Prop), iff (Inevitable_T Sini P) (FA_Until_bound Sini (fun _ : Stream (prod S Instant) => True) P) *)
    unfold iff, Inevitable_T, FA_Until_bound in |- *; intros; split; intros.
(* Goal: Until_bound (fun _ : Stream (prod S Instant) => True) P x *)
(* Goal: @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (P s)) x *)
    elim (H x H0); simple destruct x0.
(* Goal: forall (p : prod S Instant) (s : Stream (prod S Instant)) (_ : and (bound (@snd S Instant (@hd (prod S Instant) (@Cons (prod S Instant) p s)))) (P (@Cons (prod S Instant) p s))), Until_bound (fun _ : Stream (prod S Instant) => True) P (@Cons (prod S Instant) p s) *)
(* Goal: forall (p : prod S Instant) (s : Stream (prod S Instant)) (s0 : prod S Instant) (_ : @ExistsS (prod S Instant) (fun s1 : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s1))) (P s1)) (@Cons (prod S Instant) p s)) (_ : Until_bound (fun _ : Stream (prod S Instant) => True) P (@Cons (prod S Instant) p s)), Until_bound (fun _ : Stream (prod S Instant) => True) P (@Cons (prod S Instant) s0 (@Cons (prod S Instant) p s)) *)
(* Goal: @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (P s)) x *)
    simple destruct p; intros.
(* Goal: False *)
    elim H1; intros.
(* Goal: @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (P s)) (@Cons (prod S Instant) s x0) *)
(* Goal: @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (P s)) (@Cons (prod S Instant) (@pair S Instant s t) x0) *)
    constructor 2; assumption.
(* Goal: forall (p : prod S Instant) (s : Stream (prod S Instant)) (s0 : prod S Instant) (_ : @ExistsS (prod S Instant) (fun s1 : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s1))) (P s1)) (@Cons (prod S Instant) p s)) (_ : Until_bound (fun _ : Stream (prod S Instant) => True) P (@Cons (prod S Instant) p s)), Until_bound (fun _ : Stream (prod S Instant) => True) P (@Cons (prod S Instant) s0 (@Cons (prod S Instant) p s)) *)
(* Goal: @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (P s)) x *)
    constructor 1; trivial.
(* Goal: @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (P s)) x *)
    elim (H x H0); intros.
(* Goal: @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (P s)) (@Cons (prod S Instant) s x0) *)
(* Goal: @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (P s)) (@Cons (prod S Instant) (@pair S Instant s t) x0) *)
    constructor 2; assumption.
(* Goal: @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (not (P s))) (@Cons (prod S Instant) p s) *)
(* Goal: @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) s *)
    constructor 1; split; assumption.
  Qed.

  Lemma ConsTrace_T :
   forall (s1 s2 : S * Instant) (x z : Stream (S * Instant)),
   isTraceFrom_T s2 z ->
   isTraceFrom_T s1 (s1 ^ s2 ^ x) -> isTraceFrom_T s1 (s1 ^ z).
  Proof.
(* Goal: forall (s1 s2 : prod S Instant) (x z : Stream (prod S Instant)) (_ : isTraceFrom_T s2 z) (_ : isTraceFrom_T s1 (@Cons (prod S Instant) s1 (@Cons (prod S Instant) s2 x))), isTraceFrom_T s1 (@Cons (prod S Instant) s1 z) *)
    unfold isTraceFrom_T in |- *; simpl in |- *.
    simple destruct z; simple destruct 1; simple destruct 3; simpl in |- *;
(* Goal: forall (x : Stream (prod S Instant)) (_ : not (forall _ : isTraceFrom_T Sini x, @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (forall _ : P s, False)) x)), SafePath_T Sini P *)
     intros.
(* Goal: and (@eq (prod S Instant) s1 s1) (isTrace_T (@Cons (prod S Instant) s1 (@Cons (prod S Instant) p s))) *)
    compute in H0; rewrite H0 in H4.
(* Goal: and (@eq (prod S Instant) s1 s1) (isTrace_T (@Cons (prod S Instant) s1 (@Cons (prod S Instant) p s))) *)
    inversion_clear H4 in H1.
(* Goal: and (@eq (prod S Instant) (@pair S Instant s0 t) (@pair S Instant s0 t)) (isTrace_T (@Cons (prod S Instant) (@pair S Instant s0 t) (@Cons (prod S Instant) (@pair S nat (inc s0 tick) (Inc t)) s))) *)
(* Goal: and (@eq (prod S Instant) (@pair S Instant s0 t) (@pair S Instant s0 t)) (isTrace_T (@Cons (prod S Instant) (@pair S Instant s0 t) (@Cons (prod S Instant) (@pair S Instant s3 t) s))) *)
    split; [ trivial | apply (isTraceTick_T H5 H1) ].
(* Goal: and (@eq (prod S Instant) (@pair S Instant s0 t) (@pair S Instant s0 t)) (isTrace_T (@Cons (prod S Instant) (@pair S Instant s0 t) (@Cons (prod S Instant) (@pair S Instant s3 t) s))) *)
    split; [ trivial | apply (isTraceDisc_T H5 H6 H1) ].
  Qed.


  Lemma notPosible_T :
   forall (P : Stream (S * Instant) -> Prop) (s1 : S * Instant),
   ~ Posible_T s1 P ->
   forall (z : Stream (S * Instant)) (s2 : S * Instant),
   isTraceFrom_T s1 (s1 ^ s2 ^ z) -> ~ Posible_T s2 P.
  Proof.
(* Goal: forall (P : forall _ : Stream (prod S Instant), Prop) (s1 : prod S Instant) (_ : not (Posible_T s1 P)) (z : Stream (prod S Instant)) (s2 : prod S Instant) (_ : isTraceFrom_T s1 (@Cons (prod S Instant) s1 (@Cons (prod S Instant) s2 z))), not (Posible_T s2 P) *)
    unfold not at 2 in |- *; intros.
(* Goal: False *)
    elim H1; intros.
(* Goal: False *)
    apply H; cut (isTraceFrom_T s1 (s1 ^ x)).
(* Goal: forall _ : isTraceFrom_T s1 (@Cons (prod S Instant) s1 x), Posible_T s1 P *)
(* Goal: isTraceFrom_T s1 (@Cons (prod S Instant) s1 x) *)
    intro H4; apply (posible_T (P:=P) H4).
(* Goal: @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (P s)) (@Cons (prod S Instant) s1 x) *)
(* Goal: isTraceFrom_T s1 (@Cons (prod S Instant) s1 x) *)
    apply Further; assumption.
(* Goal: isTraceFrom_T s1 (@Cons (prod S Instant) s1 x) *)
    apply ConsTrace_T with (1 := H2) (2 := H0); assumption.
  Qed.

  Require Import Classical.

  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.
(* Goal: forall (Sini : prod S Instant) (P : forall _ : Stream (prod S Instant), Prop), iff (Always_T Sini P) (not (Posible_T Sini (fun s : Stream (prod S Instant) => not (P s)))) *)
    unfold iff, Always_T, not in |- *; intros; split.
(* Goal: forall (_ : forall (x : Stream (prod S Instant)) (_ : isTraceFrom_T Sini x), @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) x) (_ : Posible_T Sini (fun s : Stream (prod S Instant) => forall _ : P s, False)), False *)
(* Goal: forall (_ : forall _ : Posible_T Sini (fun s : Stream (prod S Instant) => forall _ : P s, False), False) (x : Stream (prod S Instant)) (_ : isTraceFrom_T Sini x), @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) x *)
    intros H H0; inversion_clear H0.
(* Goal: False *)
(* Goal: forall (_ : forall _ : Posible_T Sini (fun s : Stream (prod S Instant) => forall _ : P s, False), False) (x : Stream (prod S Instant)) (_ : isTraceFrom_T Sini x), @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) x *)
    generalize (H x H1); elim H2; intros.
(* Goal: False *)
(* Goal: False *)
(* Goal: forall (_ : forall _ : Posible_T Sini (fun s : Stream (prod S Instant) => forall _ : P s, False), False) (x : Stream (prod S Instant)) (_ : isTraceFrom_T Sini x), @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) x *)
    inversion_clear H3 in H0.
(* Goal: False *)
(* Goal: False *)
(* Goal: forall (_ : forall _ : Posible_T Sini (fun s : Stream (prod S Instant) => forall _ : P s, False), False) (x : Stream (prod S Instant)) (_ : isTraceFrom_T Sini x), @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) x *)
    elim H0; intros.
(* Goal: False *)
(* Goal: False *)
(* Goal: forall (_ : forall _ : Posible_T Sini (fun s : Stream (prod S Instant) => forall _ : P s, False), False) (x : Stream (prod S Instant)) (_ : isTraceFrom_T Sini x), @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) x *)
    elim (H6 (H4 H3)).
(* Goal: False *)
(* Goal: forall (_ : forall _ : Posible_T Sini (fun s : Stream (prod S Instant) => forall _ : P s, False), False) (x : Stream (prod S Instant)) (_ : isTraceFrom_T Sini x), @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) x *)
    inversion_clear H4.
(* Goal: False *)
(* Goal: forall (_ : forall _ : Posible_T Sini (fun s : Stream (prod S Instant) => forall _ : P s, False), False) (x : Stream (prod S Instant)) (_ : isTraceFrom_T Sini x), @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) x *)
    apply (H3 H6).
(* Goal: forall (_ : forall _ : Posible_T Sini (fun s : Stream (prod S Instant) => forall _ : P s, False), False) (x : Stream (prod S Instant)) (_ : isTraceFrom_T Sini x), @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) x *)
    generalize Sini; cofix u.
(* Goal: forall (Sini : prod S Instant) (_ : forall _ : Posible_T Sini (fun s : Stream (prod S Instant) => forall _ : P s, False), False) (x : Stream (prod S Instant)) (_ : isTraceFrom_T Sini x), @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) x *)
    simple destruct x; intros; constructor.
(* Goal: forall _ : bound (@snd S Instant (@hd (prod S Instant) (@Cons (prod S Instant) p s))), P (@Cons (prod S Instant) p s) *)
(* Goal: @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) s *)
    intro; elim (classic (P (p ^ s))); [ trivial | intros ].
(* Goal: P (@Cons (prod S Instant) p s) *)
(* Goal: @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) s *)
    absurd (Posible_T Sini0 (fun s : Stream (S * Instant) => ~ P s)).
(* Goal: not (Posible_T Sini0 (fun s : Stream (prod S Instant) => not (P s))) *)
(* Goal: Posible_T Sini0 (fun s : Stream (prod S Instant) => not (P s)) *)
(* Goal: @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) s *)
    assumption.
(* Goal: Posible_T Sini0 (fun s : Stream (prod S Instant) => not (P s)) *)
(* Goal: @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) s *)
    apply posible_T with (1 := H0).
(* Goal: @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (not (P s))) (@Cons (prod S Instant) p s) *)
(* Goal: @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) s *)
    constructor 1; split; assumption.
(* Goal: @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) s *)
    elim H0; simpl in |- *; intros.
(* Goal: @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) s *)
    apply (u (hd s)); intros.
(* Goal: False *)
(* Goal: isTraceFrom_T (@hd (prod S Instant) s) s *)
    generalize H0; clear H0; generalize H3; clear H3.
(* Goal: forall (_ : Posible_T (@hd (prod S Instant) s) (fun s : Stream (prod S Instant) => forall _ : P s, False)) (_ : isTraceFrom_T Sini0 (@Cons (prod S Instant) p s)), False *)
(* Goal: isTraceFrom_T (@hd (prod S Instant) s) s *)
    rewrite <- H1; case s; simpl in |- *; intros.
    apply (notPosible_T (P:=fun s : Stream (S * Instant) => ~ P s) H H0);
(* Goal: not (Posible_T Sini0 (fun s : Stream (prod S Instant) => not (P s))) *)
(* Goal: Posible_T Sini0 (fun s : Stream (prod S Instant) => not (P s)) *)
(* Goal: @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) s *)
     assumption.
(* Goal: isTraceFrom_T (@hd (prod S Instant) s) s *)
    unfold isTraceFrom_T in |- *; inversion_clear H2; simpl in |- *.
(* Goal: and (@eq (prod S Instant) (@hd (prod S Instant) (@Cons (prod S Instant) (@pair S Instant s2 t) x1)) (@hd (prod S Instant) (@Cons (prod S Instant) (@pair S Instant s2 t) x1))) (isTrace_T (@Cons (prod S Instant) (@pair S Instant s2 t) x1)) *)
    split; trivial.
(* Goal: and (@eq (prod S Instant) (@hd (prod S Instant) (@Cons (prod S Instant) (@pair S Instant s2 t) x1)) (@hd (prod S Instant) (@Cons (prod S Instant) (@pair S Instant s2 t) x1))) (isTrace_T (@Cons (prod S Instant) (@pair S Instant s2 t) x1)) *)
    split; trivial.
  Qed.


  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.
(* Goal: forall (Sini : prod S Instant) (P : forall _ : Stream (prod S Instant), Prop), iff (SafePath_T Sini P) (not (Inevitable_T Sini (fun s : Stream (prod S Instant) => not (P s)))) *)
    unfold iff, Inevitable_T, not in |- *; intros; split.
(* Goal: forall (_ : SafePath_T Sini P) (_ : forall (x : Stream (prod S Instant)) (_ : isTraceFrom_T Sini x), @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (forall _ : P s, False)) x), False *)
(* Goal: forall _ : forall _ : forall (x : Stream (prod S Instant)) (_ : isTraceFrom_T Sini x), @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (forall _ : P s, False)) x, False, SafePath_T Sini P *)
    intro sp; inversion sp; intros.
(* Goal: False *)
(* Goal: forall _ : forall _ : forall (x : Stream (prod S Instant)) (_ : isTraceFrom_T Sini x), @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (forall _ : P s, False)) x, False, SafePath_T Sini P *)
    generalize H0; elim (H1 x H); intros.
(* Goal: False *)
(* Goal: False *)
(* Goal: forall _ : forall _ : forall (x : Stream (prod S Instant)) (_ : isTraceFrom_T Sini x), @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (forall _ : P s, False)) x, False, SafePath_T Sini P *)
    inversion_clear H3 in H2.
(* Goal: False *)
(* Goal: False *)
(* Goal: forall _ : forall _ : forall (x : Stream (prod S Instant)) (_ : isTraceFrom_T Sini x), @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (forall _ : P s, False)) x, False, SafePath_T Sini P *)
    elim H2; intros.
(* Goal: False *)
(* Goal: False *)
(* Goal: forall _ : forall _ : forall (x : Stream (prod S Instant)) (_ : isTraceFrom_T Sini x), @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (forall _ : P s, False)) x, False, SafePath_T Sini P *)
    apply (H6 (H4 H3)).
(* Goal: not (Posible_T Sini0 (fun s : Stream (prod S Instant) => not (P s))) *)
(* Goal: Posible_T Sini0 (fun s : Stream (prod S Instant) => not (P s)) *)
(* Goal: @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) s *)
    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).
(* Goal: forall (x : Stream (prod S Instant)) (_ : not (forall _ : isTraceFrom_T Sini x, @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (forall _ : P s, False)) x)), SafePath_T Sini P *)
    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); 
(* Goal: forall (x : Stream (prod S Instant)) (_ : not (forall _ : isTraceFrom_T Sini x, @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (forall _ : P s, False)) x)), SafePath_T Sini P *)
     intros.
(* Goal: SafePath_T Sini P *)
    apply safePath_T with (1 := H1).
(* Goal: @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) x *)
    generalize H1; clear H1; generalize H2; clear H2.
(* Goal: forall (_ : forall _ : Posible_T Sini (fun s : Stream (prod S Instant) => forall _ : P s, False), False) (x : Stream (prod S Instant)) (_ : isTraceFrom_T Sini x), @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) x *)
    generalize x; generalize Sini; cofix u.
(* Goal: forall (Sini : prod S Instant) (x : Stream (prod S Instant)) (_ : not (@ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (forall _ : P s, False)) x)) (_ : isTraceFrom_T Sini x), @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) x *)
    simple destruct x0; intros; constructor.
(* Goal: forall _ : bound (@snd S Instant (@hd (prod S Instant) (@Cons (prod S Instant) p s))), P (@Cons (prod S Instant) p s) *)
(* Goal: @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) s *)
    elim (classic (P (p ^ s))); [ trivial | intros ].
    cut
     (ExistsS
        (fun s0 : Stream (S * Instant) =>
         bound (snd (hd s0)) /\ (P s0 -> False)) (p ^ s)).
(* Goal: forall _ : @ExistsS (prod S Instant) (fun s0 : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s0))) (forall _ : P s0, False)) (@Cons (prod S Instant) p s), P (@Cons (prod S Instant) p s) *)
(* Goal: @ExistsS (prod S Instant) (fun s0 : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s0))) (forall _ : P s0, False)) (@Cons (prod S Instant) p s) *)
(* Goal: @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) s *)
    intro ex; elim (H2 ex).
    apply
     Here
      with
        (P := fun s : Stream (S * Instant) =>
              bound (snd (hd s)) /\ (P s -> False)).
(* Goal: not (Posible_T Sini0 (fun s : Stream (prod S Instant) => not (P s))) *)
(* Goal: Posible_T Sini0 (fun s : Stream (prod S Instant) => not (P s)) *)
(* Goal: @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) s *)
    split; assumption.
(* Goal: @ForAllS (prod S Instant) (fun s : Stream (prod S Instant) => forall _ : bound (@snd S Instant (@hd (prod S Instant) s)), P s) s *)
    apply u with (Sini := hd s).
(* Goal: forall (x : Stream (prod S Instant)) (_ : not (forall _ : isTraceFrom_T Sini x, @ExistsS (prod S Instant) (fun s : Stream (prod S Instant) => and (bound (@snd S Instant (@hd (prod S Instant) s))) (forall _ : P s, False)) x)), SafePath_T Sini P *)
    generalize H2; clear H2; case s; unfold not in |- *; intros.
(* Goal: False *)
(* Goal: isTraceFrom_T (@hd (prod S Instant) s) s *)
    apply (not_EX H2 H3).
    unfold isTraceFrom_T in |- *; elim H1; intros ig trace;
     inversion_clear trace.
(* Goal: and (@eq (prod S Instant) (@hd (prod S Instant) (@Cons (prod S Instant) (@pair S Instant s2 t) x1)) (@hd (prod S Instant) (@Cons (prod S Instant) (@pair S Instant s2 t) x1))) (isTrace_T (@Cons (prod S Instant) (@pair S Instant s2 t) x1)) *)
    split; trivial.
(* Goal: and (@eq (prod S Instant) (@hd (prod S Instant) (@Cons (prod S Instant) (@pair S Instant s2 t) x1)) (@hd (prod S Instant) (@Cons (prod S Instant) (@pair S Instant s2 t) x1))) (isTrace_T (@Cons (prod S Instant) (@pair S Instant s2 t) x1)) *)
    split; trivial.
  Qed.


End TemporalOperators_TCTL.

