Theory: Past_Temporal_Logic

Parents

• Temporal_Logic

Types

Constants

• PSWHEN  :(num -> bool) -> (num -> bool) -> num -> bool
• PUNTIL  :(num -> bool) -> (num -> bool) -> num -> bool
• InitPoint  :num -> bool
• PEVENTUAL  :(num -> bool) -> num -> bool
• PSBEFORE  :(num -> bool) -> (num -> bool) -> num -> bool
• PALWAYS  :(num -> bool) -> num -> bool
• PNEXT  :(num -> bool) -> num -> bool
• PBEFORE  :(num -> bool) -> (num -> bool) -> num -> bool
• PSUNTIL  :(num -> bool) -> (num -> bool) -> num -> bool
• PWHEN  :(num -> bool) -> (num -> bool) -> num -> bool
• PSNEXT  :(num -> bool) -> num -> bool

Definitions

InitPoint

|- InitPoint = (\t. t = 0)

PALWAYS

|- !a t0. PALWAYS a t0 = !t. t <= t0 ==> a t

PBEFORE

|- !a b t0.
     (a PBEFORE b) t0 =
     (!t. t <= t0 ==> ~b t) \/
     ?delta. delta <= t0 /\ a delta /\ !t. delta <= t /\ t <= t0 ==> ~b t

PEVENTUAL

|- !a t0. PEVENTUAL a t0 = ?t. t <= t0 /\ a t

PNEXT

|- !a t0. PNEXT a t0 = (t0 = 0) \/ a (PRE t0)

PSBEFORE

|- !a b t0.
     (a PSBEFORE b) t0 =
     ?delta. delta <= t0 /\ a delta /\ !t. delta <= t /\ t <= t0 ==> ~b t

PSNEXT

|- !a t0. PSNEXT a t0 = 0 < t0 /\ a (PRE t0)

PSUNTIL

|- !a b t0.
     (a PSUNTIL b) t0 =
     ?delta.
       delta <= t0 /\ b delta /\ !t. delta < t /\ t <= t0 ==> a t /\ ~b t

PSWHEN

|- !a b t0.
     (a PSWHEN b) t0 =
     ?delta.
       delta <= t0 /\ a delta /\ b delta /\ !t. delta < t /\ t <= t0 ==> ~b t

PUNTIL

|- !a b t0.
     (a PUNTIL b) t0 =
     (!t. t <= t0 ==> a t) \/
     ?delta.
       delta <= t0 /\ b delta /\ !t. delta < t /\ t <= t0 ==> a t /\ ~b t

PWHEN

|- !a b t0.
     (a PWHEN b) t0 =
     (!t. t <= t0 ==> ~b t) \/
     ?delta.
       delta <= t0 /\ a delta /\ b delta /\ !t. delta < t /\ t <= t0 ==> ~b t

Theorems

BEFORE_EXPRESSIVE

|- (ALWAYS a = (\t. ((\t. F) BEFORE (\t. ~a t)) t)) /\
   (EVENTUAL a = (\t. ~((\t. F) BEFORE a) t)) /\
   (a SUNTIL b = (\t. ~((\t. ~a t) BEFORE b) t)) /\
   (a UNTIL b = (\t. (b BEFORE (\t. ~a t /\ ~b t)) t)) /\
   (a SWHEN b = (\t. ~(b BEFORE (\t. a t /\ b t)) t)) /\
   (a WHEN b = (\t. ((\t. a t /\ b t) BEFORE (\t. ~a t /\ b t)) t)) /\
   (a SBEFORE b = (\t. ~(b BEFORE (\t. a t /\ ~b t)) t))

CONJUNCTIVE_NORMAL_FORM

|- (NEXT (\t. a t /\ b t) = (\t. NEXT a t /\ NEXT b t)) /\
   (ALWAYS (\t. a t /\ b t) = (\t. ALWAYS a t /\ ALWAYS b t)) /\
   ((\t. a t /\ b t) WHEN c = (\t. (a WHEN c) t /\ (b WHEN c) t)) /\
   ((\t. a t /\ b t) SWHEN c = (\t. (a SWHEN c) t /\ (b SWHEN c) t)) /\
   ((\t. a t /\ b t) UNTIL c = (\t. (a UNTIL c) t /\ (b UNTIL c) t)) /\
   ((\t. a t /\ b t) SUNTIL c = (\t. (a SUNTIL c) t /\ (b SUNTIL c) t)) /\
   (c BEFORE (\t. a t \/ b t) = (\t. (c BEFORE a) t /\ (c BEFORE b) t)) /\
   (c SBEFORE (\t. a t \/ b t) = (\t. (c SBEFORE a) t /\ (c SBEFORE b) t)) /\
   (PNEXT (\t. a t /\ b t) = (\t. PNEXT a t /\ PNEXT b t)) /\
   (PSNEXT (\t. a t /\ b t) = (\t. PSNEXT a t /\ PSNEXT b t)) /\
   (PALWAYS (\t. a t /\ b t) = (\t. PALWAYS a t /\ PALWAYS b t)) /\
   ((\t. a t /\ b t) PWHEN c = (\t. (a PWHEN c) t /\ (b PWHEN c) t)) /\
   ((\t. a t /\ b t) PSWHEN c = (\t. (a PSWHEN c) t /\ (b PSWHEN c) t)) /\
   ((\t. a t /\ b t) PUNTIL c = (\t. (a PUNTIL c) t /\ (b PUNTIL c) t)) /\
   ((\t. a t /\ b t) PSUNTIL c = (\t. (a PSUNTIL c) t /\ (b PSUNTIL c) t)) /\
   (c PBEFORE (\t. a t \/ b t) = (\t. (c PBEFORE a) t /\ (c PBEFORE b) t)) /\
   (c PSBEFORE (\t. a t \/ b t) = (\t. (c PSBEFORE a) t /\ (c PSBEFORE b) t))

DISJUNCTIVE_NORMAL_FORM

|- (NEXT (\t. a t \/ b t) = (\t. NEXT a t \/ NEXT b t)) /\
   (EVENTUAL (\t. a t \/ b t) = (\t. EVENTUAL a t \/ EVENTUAL b t)) /\
   ((\t. a t \/ b t) WHEN c = (\t. (a WHEN c) t \/ (b WHEN c) t)) /\
   ((\t. a t \/ b t) SWHEN c = (\t. (a SWHEN c) t \/ (b SWHEN c) t)) /\
   (a UNTIL (\t. b t \/ c t) = (\t. (a UNTIL b) t \/ (a UNTIL c) t)) /\
   (a SUNTIL (\t. b t \/ c t) = (\t. (a SUNTIL b) t \/ (a SUNTIL c) t)) /\
   ((\t. a t \/ b t) BEFORE c = (\t. (a BEFORE c) t \/ (b BEFORE c) t)) /\
   ((\t. a t \/ b t) SBEFORE c = (\t. (a SBEFORE c) t \/ (b SBEFORE c) t)) /\
   (PNEXT (\t. a t \/ b t) = (\t. PNEXT a t \/ PNEXT b t)) /\
   (PEVENTUAL (\t. a t \/ b t) = (\t. PEVENTUAL a t \/ PEVENTUAL b t)) /\
   ((\t. a t \/ b t) PWHEN c = (\t. (a PWHEN c) t \/ (b PWHEN c) t)) /\
   ((\t. a t \/ b t) PSWHEN c = (\t. (a PSWHEN c) t \/ (b PSWHEN c) t)) /\
   (a PUNTIL (\t. b t \/ c t) = (\t. (a PUNTIL b) t \/ (a PUNTIL c) t)) /\
   (a PSUNTIL (\t. b t \/ c t) = (\t. (a PSUNTIL b) t \/ (a PSUNTIL c) t)) /\
   ((\t. a t \/ b t) PBEFORE c = (\t. (a PBEFORE c) t \/ (b PBEFORE c) t)) /\
   ((\t. a t \/ b t) PSBEFORE c = (\t. (a PSBEFORE c) t \/ (b PSBEFORE c) t))

FIXPOINTS

|- ((y = (\t. a t /\ NEXT y t)) = (y = ALWAYS a) \/ (y = (\t. F))) /\
   ((y = (\t. a t \/ NEXT y t)) = (y = EVENTUAL a) \/ (y = (\t. T))) /\
   ((y = (\t. ~b t ==> a t /\ NEXT y t)) =
    (y = a UNTIL b) \/ (y = a SUNTIL b)) /\
   ((y = (\t. (if b t then a t else NEXT y t))) =
    (y = a WHEN b) \/ (y = a SWHEN b)) /\
   ((y = (\t. ~b t /\ (a t \/ NEXT y t))) =
    (y = a BEFORE b) \/ (y = a SBEFORE b)) /\
   ((y = (\t. a t /\ PNEXT y t)) = (y = PALWAYS a)) /\
   ((y = (\t. a t \/ PSNEXT y t)) = (y = PEVENTUAL a)) /\
   ((y = (\t. b t \/ a t /\ PSNEXT y t)) = (y = a PSUNTIL b)) /\
   ((y = (\t. a t /\ b t \/ ~b t /\ PSNEXT y t)) = (y = a PSWHEN b)) /\
   ((y = (\t. ~b t /\ (a t \/ PSNEXT y t))) = (y = a PSBEFORE b)) /\
   ((y = (\t. b t \/ a t /\ PNEXT y t)) = (y = a PUNTIL b)) /\
   ((y = (\t. a t /\ b t \/ ~b t /\ PNEXT y t)) = (y = a PWHEN b)) /\
   ((y = (\t. ~b t /\ (a t \/ PNEXT y t))) = (y = a PBEFORE b))

IMMEDIATE_EVENT

|- b t ==>
   ((a WHEN b) t = a t) /\ ((a UNTIL b) t = T) /\ ((a BEFORE b) t = F) /\
   ((b BEFORE a) t = ~a t) /\ ((a SWHEN b) t = a t) /\ ((a SUNTIL b) t = T) /\
   ((a SBEFORE b) t = F) /\ ((b SBEFORE a) t = ~a t) /\
   ((a PWHEN b) t = a t) /\ ((a PUNTIL b) t = T) /\ ((a PBEFORE b) t = F) /\
   ((b PBEFORE a) t = ~a t) /\ ((a PSWHEN b) t = a t) /\
   ((a PSUNTIL b) t = T) /\ ((a PSBEFORE b) t = F) /\
   ((b PSBEFORE a) t = ~a t)

INITIALISATION

|- (PNEXT a 0 = T) /\ (PSNEXT a 0 = F) /\ (PALWAYS a 0 = a 0) /\
   (PEVENTUAL a 0 = a 0) /\ ((a PSUNTIL b) 0 = b 0) /\
   ((a PSWHEN b) 0 = a 0 /\ b 0) /\ ((a PSBEFORE b) 0 = a 0 /\ ~b 0) /\
   ((a PUNTIL b) 0 = a 0 \/ b 0) /\ ((a PWHEN b) 0 = a 0 \/ ~b 0) /\
   ((a PBEFORE b) 0 = ~b 0)

MORE_EVENT

|- (a WHEN b = (\t. a t /\ b t) WHEN b) /\
   (a UNTIL b = (\t. a t /\ ~b t) UNTIL b) /\
   (a BEFORE b = (\t. a t /\ ~b t) BEFORE b) /\
   (a SWHEN b = (\t. a t /\ b t) SWHEN b) /\
   (a SUNTIL b = (\t. a t /\ ~b t) SUNTIL b) /\
   (a SBEFORE b = (\t. a t /\ ~b t) SBEFORE b) /\
   (a PWHEN b = (\t. a t /\ b t) PWHEN b) /\
   (a PUNTIL b = (\t. a t /\ ~b t) PUNTIL b) /\
   (a PBEFORE b = (\t. a t /\ ~b t) PBEFORE b) /\
   (a PSWHEN b = (\t. a t /\ b t) PSWHEN b) /\
   (a PSUNTIL b = (\t. a t /\ ~b t) PSUNTIL b) /\
   (a PSBEFORE b = (\t. a t /\ ~b t) PSBEFORE b)

NEGATION_NORMAL_FORM

|- (~NEXT a t = NEXT (\t. ~a t) t) /\ (~ALWAYS a t = EVENTUAL (\t. ~a t) t) /\
   (~EVENTUAL a t = ALWAYS (\t. ~a t) t) /\
   (~(a WHEN b) t = ((\t. ~a t) SWHEN b) t) /\
   (~(a UNTIL b) t = ((\t. ~a t) SBEFORE b) t) /\
   (~(a BEFORE b) t = ((\t. ~a t) SUNTIL b) t) /\
   (~(a SWHEN b) t = ((\t. ~a t) WHEN b) t) /\
   (~(a SUNTIL b) t = ((\t. ~a t) BEFORE b) t) /\
   (~(a SBEFORE b) t = ((\t. ~a t) UNTIL b) t) /\
   (~PNEXT a t = PSNEXT (\t. ~a t) t) /\ (~PSNEXT a t = PNEXT (\t. ~a t) t) /\
   (~PALWAYS a t = PEVENTUAL (\t. ~a t) t) /\
   (~PEVENTUAL a t = PALWAYS (\t. ~a t) t) /\
   (~(a PWHEN b) t = ((\t. ~a t) PSWHEN b) t) /\
   (~(a PUNTIL b) t = ((\t. ~a t) PSBEFORE b) t) /\
   (~(a PBEFORE b) t = ((\t. ~a t) PSUNTIL b) t) /\
   (~(a PSWHEN b) t = ((\t. ~a t) PWHEN b) t) /\
   (~(a PSUNTIL b) t = ((\t. ~a t) PBEFORE b) t) /\
   (~(a PSBEFORE b) t = ((\t. ~a t) PUNTIL b) t)

NEXT_INWARDS_NORMAL_FORM

|- (NEXT (\t. ~a t) = (\t. ~NEXT a t)) /\
   (NEXT (\t. a t /\ b t) = (\t. NEXT a t /\ NEXT b t)) /\
   (NEXT (\t. a t \/ b t) = (\t. NEXT a t \/ NEXT b t)) /\
   (NEXT (ALWAYS a) = ALWAYS (NEXT a)) /\
   (NEXT (EVENTUAL a) = EVENTUAL (NEXT a)) /\
   (NEXT (a SUNTIL b) = NEXT a SUNTIL NEXT b) /\
   (NEXT (a SWHEN b) = NEXT a SWHEN NEXT b) /\
   (NEXT (a SBEFORE b) = NEXT a SBEFORE NEXT b) /\
   (NEXT (a UNTIL b) = NEXT a UNTIL NEXT b) /\
   (NEXT (a WHEN b) = NEXT a WHEN NEXT b) /\
   (NEXT (a BEFORE b) = NEXT a BEFORE NEXT b) /\ (NEXT (PNEXT a) = a) /\
   (NEXT (PSNEXT a) = a) /\
   (NEXT (PALWAYS a) = (\t. PALWAYS a t /\ NEXT a t)) /\
   (NEXT (PEVENTUAL a) = (\t. PEVENTUAL a t \/ NEXT a t)) /\
   (NEXT (a PSUNTIL b) = (\t. NEXT b t \/ NEXT a t /\ (a PSUNTIL b) t)) /\
   (NEXT (a PSWHEN b) =
    (\t. (if NEXT b t then NEXT a t else (a PSWHEN b) t))) /\
   (NEXT (a PSBEFORE b) =
    (\t. ~NEXT b t /\ (NEXT a t \/ (a PSBEFORE b) t))) /\
   (NEXT (a PUNTIL b) = (\t. NEXT b t \/ NEXT a t /\ (a PUNTIL b) t)) /\
   (NEXT (a PWHEN b) =
    (\t. (if NEXT b t then NEXT a t else (a PWHEN b) t))) /\
   (NEXT (a PBEFORE b) = (\t. ~NEXT b t /\ (NEXT a t \/ (a PBEFORE b) t)))

NO_FUTURE_EVENT

|- ALWAYS (\t. ~b t) t0 ==>
   (!a. (a WHEN b) t0 = T) /\ (!a. (a UNTIL b) t0 = ALWAYS a t0) /\
   (!a. (a BEFORE b) t0 = T) /\ (!a. (a SWHEN b) t0 = F) /\
   (!a. (a SUNTIL b) t0 = F) /\ !a. (a SBEFORE b) t0 = EVENTUAL a t0

NO_PAST_EVENT

|- PALWAYS (\t. ~b t) t ==>
   ((a PWHEN b) t = T) /\ ((a PUNTIL b) t = PALWAYS a t) /\
   ((a PBEFORE b) t = T) /\ ((b PBEFORE a) t = PALWAYS (\t. ~a t) t) /\
   ((a PSWHEN b) t = F) /\ ((a PSUNTIL b) t = F) /\
   ((a PSBEFORE b) t = PEVENTUAL a t) /\ ((b PSBEFORE a) t = F)

PBEFORE_EXPRESSIVE

|- (PALWAYS a = (\t. ((\t. F) PBEFORE (\t. ~a t)) t)) /\
   (PEVENTUAL a = (\t. ~((\t. F) PBEFORE a) t)) /\
   (a PSUNTIL b = (\t. ~((\t. ~a t) PBEFORE b) t)) /\
   (a PUNTIL b = (\t. (b PBEFORE (\t. ~a t /\ ~b t)) t)) /\
   (a PSWHEN b = (\t. ~(b PBEFORE (\t. a t /\ b t)) t)) /\
   (a PWHEN b = (\t. ((\t. a t /\ b t) PBEFORE (\t. ~a t /\ b t)) t)) /\
   (a PSBEFORE b = (\t. ~(b PBEFORE (\t. a t /\ ~b t)) t))

PNEXT_INWARDS_NORMAL_FORM

|- (PNEXT (\t. ~a t) = (\t. ~PSNEXT a t)) /\
   (PNEXT (\t. a t /\ b t) = (\t. PNEXT a t /\ PNEXT b t)) /\
   (PNEXT (\t. a t \/ b t) = (\t. PNEXT a t \/ PNEXT b t)) /\
   (PNEXT (NEXT a) = (\t. InitPoint t \/ a t)) /\
   (PNEXT (ALWAYS a) = (\t. InitPoint t \/ ALWAYS (PNEXT a) t)) /\
   (PNEXT (EVENTUAL a) = (\t. InitPoint t \/ EVENTUAL (PNEXT a) t)) /\
   (PNEXT (a SUNTIL b) = PNEXT a SUNTIL PNEXT b) /\
   (PNEXT (a SWHEN b) = PNEXT a SWHEN PNEXT b) /\
   (PNEXT (a SBEFORE b) = PNEXT a SBEFORE PSNEXT b) /\
   (PNEXT (a UNTIL b) = PNEXT a UNTIL PNEXT b) /\
   (PNEXT (a WHEN b) = PNEXT a WHEN PNEXT b) /\
   (PNEXT (a BEFORE b) = PNEXT a BEFORE PSNEXT b) /\
   (PNEXT (PALWAYS a) = PALWAYS (PNEXT a)) /\
   (PNEXT (PEVENTUAL a) = (\t. InitPoint t \/ PEVENTUAL (PSNEXT a) t)) /\
   (PNEXT (a PSUNTIL b) =
    (\t. InitPoint t \/ (PNEXT a PSUNTIL PSNEXT b) t)) /\
   (PNEXT (a PSWHEN b) = (\t. InitPoint t \/ (PNEXT a PSWHEN PSNEXT b) t)) /\
   (PNEXT (a PSBEFORE b) =
    (\t. InitPoint t \/ (PSNEXT a PSBEFORE PNEXT b) t)) /\
   (PNEXT (a PUNTIL b) = PNEXT a PUNTIL PNEXT b) /\
   (PNEXT (a PWHEN b) = PNEXT a PWHEN PNEXT b) /\
   (PNEXT (a PBEFORE b) = PNEXT a PBEFORE PSNEXT b)

PRENEX_NEXT_NORMAL_FORM

|- (~NEXT a t = NEXT (\t. ~a t) t) /\
   (a t /\ NEXT b t = NEXT (\t. PNEXT a t /\ b t) t) /\
   (a t \/ NEXT b t = NEXT (\t. PNEXT a t \/ b t) t) /\
   (ALWAYS (NEXT a) = NEXT (ALWAYS a)) /\
   (EVENTUAL (NEXT a) = NEXT (EVENTUAL a)) /\
   (a SUNTIL NEXT b = NEXT (PNEXT a SUNTIL b)) /\
   (a SWHEN NEXT b = NEXT (PNEXT a SWHEN b)) /\
   (a SBEFORE NEXT b = NEXT (PNEXT a SBEFORE b)) /\
   (a UNTIL NEXT b = NEXT (PNEXT a UNTIL b)) /\
   (a WHEN NEXT b = NEXT (PNEXT a WHEN b)) /\
   (a BEFORE NEXT b = NEXT (PNEXT a BEFORE b)) /\
   (NEXT a SUNTIL b = NEXT (a SUNTIL PNEXT b)) /\
   (NEXT a SWHEN b = NEXT (a SWHEN PNEXT b)) /\
   (NEXT a SBEFORE b = NEXT (a SBEFORE PNEXT b)) /\
   (NEXT a UNTIL b = NEXT (a UNTIL PNEXT b)) /\
   (NEXT a WHEN b = NEXT (a WHEN PNEXT b)) /\
   (NEXT a BEFORE b = NEXT (a BEFORE PNEXT b)) /\
   (PNEXT (NEXT a) = (\t. InitPoint t \/ a t)) /\
   (PSNEXT (NEXT a) = (\t. ~InitPoint t /\ a t)) /\
   (PALWAYS (NEXT a) = NEXT (PALWAYS (\t. InitPoint t \/ a t))) /\
   (PEVENTUAL (NEXT a) = NEXT (PEVENTUAL (\t. ~InitPoint t /\ a t))) /\
   (a PSUNTIL NEXT b = NEXT (PNEXT a PSUNTIL (\t. ~InitPoint t /\ b t))) /\
   (a PSWHEN NEXT b = NEXT (PNEXT a PSWHEN (\t. ~InitPoint t /\ b t))) /\
   (a PSBEFORE NEXT b = NEXT (PSNEXT a PSBEFORE b)) /\
   (a PUNTIL NEXT b = NEXT (PNEXT a PUNTIL b)) /\
   (a PWHEN NEXT b = NEXT (PNEXT a PWHEN (\t. ~InitPoint t /\ b t))) /\
   (a PBEFORE NEXT b = NEXT (PNEXT a PBEFORE (\t. ~InitPoint t /\ b t))) /\
   (NEXT a PSUNTIL b = NEXT (a PSUNTIL PSNEXT b)) /\
   (NEXT a PSWHEN b = NEXT (a PSWHEN PSNEXT b)) /\
   (NEXT a PSBEFORE b = NEXT ((\t. ~InitPoint t /\ a t) PSBEFORE PNEXT b)) /\
   (NEXT a PUNTIL b = NEXT ((\t. InitPoint t \/ a t) PUNTIL PNEXT b)) /\
   (NEXT a PWHEN b = NEXT (a PWHEN PSNEXT b)) /\
   (NEXT a PBEFORE b = NEXT (a PBEFORE PSNEXT b))

PSBEFORE_EXPRESSIVE

|- (PALWAYS a = (\t. ~((\t. ~a t) PSBEFORE (\t. F)) t)) /\
   (PEVENTUAL a = (\t. (a PSBEFORE (\t. F)) t)) /\
   (a PSUNTIL b = (\t. (b PSBEFORE (\t. ~a t /\ ~b t)) t)) /\
   (a PUNTIL b = (\t. ~((\t. ~a t) PSBEFORE b) t)) /\
   (a PSWHEN b = (\t. (b PSBEFORE (\t. ~a t /\ b t)) t)) /\
   (a PWHEN b = (\t. ~(b PSBEFORE (\t. a t /\ b t)) t)) /\
   (a PBEFORE b = (\t. ~(b PSBEFORE (\t. a t /\ ~b t)) t))

PSUNTIL_EXPRESSIVE

|- (PALWAYS a = (\t. ~((\t. T) PSUNTIL (\t. ~a t)) t)) /\
   (PEVENTUAL a = (\t. ((\t. T) PSUNTIL a) t)) /\
   (a PUNTIL b = (\t. ~((\t. ~b t) PSUNTIL (\t. ~a t /\ ~b t)) t)) /\
   (a PWHEN b = (\t. ~((\t. ~a t \/ ~b t) PSUNTIL (\t. ~a t /\ b t)) t)) /\
   (a PBEFORE b = (\t. ~((\t. ~a t) PSUNTIL b) t)) /\
   (a PSWHEN b = (\t. ((\t. ~b t) PSUNTIL (\t. a t /\ b t)) t)) /\
   (a PSBEFORE b = (\t. ((\t. ~b t) PSUNTIL (\t. a t /\ ~b t)) t))

PSWHEN_EXPRESSIVE

|- (PALWAYS a = (\t. ~((\t. T) PSWHEN (\t. ~a t)) t)) /\
   (PEVENTUAL a = (\t. ((\t. T) PSWHEN a) t)) /\
   (a PSUNTIL b = (\t. (b PSWHEN (\t. a t ==> b t)) t)) /\
   (a PUNTIL b = (\t. ~((\t. ~b t) PSWHEN (\t. a t ==> b t)) t)) /\
   (a PWHEN b = (\t. ~((\t. ~a t) PSWHEN b) t)) /\
   (a PBEFORE b = (\t. ~(b PSWHEN (\t. a t \/ b t)) t)) /\
   (a PSBEFORE b = (\t. ((\t. ~b t) PSWHEN (\t. a t \/ b t)) t))

PUNTIL_EXPRESSIVE

|- (PALWAYS a = (\t. (a PUNTIL (\t. F)) t)) /\
   (PEVENTUAL a = (\t. ~((\t. ~a t) PUNTIL (\t. F)) t)) /\
   (a PSUNTIL b = (\t. ~((\t. ~b t) PUNTIL (\t. ~a t /\ ~b t)) t)) /\
   (a PWHEN b = (\t. ((\t. ~b t) PUNTIL (\t. a t /\ b t)) t)) /\
   (a PSWHEN b = (\t. ~((\t. ~a t \/ ~b t) PUNTIL (\t. ~a t /\ b t)) t)) /\
   (a PBEFORE b = (\t. ((\t. ~b t) PUNTIL (\t. a t /\ ~b t)) t)) /\
   (a PSBEFORE b = (\t. ~((\t. ~a t) PUNTIL b) t))

PWHEN_EXPRESSIVE

|- (PALWAYS a = (\t. ((\t. F) PWHEN (\t. ~a t)) t)) /\
   (PEVENTUAL a = (\t. ~((\t. F) PWHEN a) t)) /\
   (a PSUNTIL b = (\t. ~((\t. ~b t) PWHEN (\t. a t ==> b t)) t)) /\
   (a PUNTIL b = (\t. (b PWHEN (\t. a t ==> b t)) t)) /\
   (a PSWHEN b = (\t. ~((\t. ~a t) PWHEN b) t)) /\
   (a PBEFORE b = (\t. ((\t. ~b t) PWHEN (\t. a t \/ b t)) t)) /\
   (a PSBEFORE b = (\t. ~(b PWHEN (\t. a t \/ b t)) t))

RECURSION

|- (ALWAYS a = (\t. a t /\ NEXT (ALWAYS a) t)) /\
   (EVENTUAL a = (\t. a t \/ NEXT (EVENTUAL a) t)) /\
   (a SUNTIL b = (\t. ~b t ==> a t /\ NEXT (a SUNTIL b) t)) /\
   (a SWHEN b = (\t. (if b t then a t else NEXT (a SWHEN b) t))) /\
   (a SBEFORE b = (\t. ~b t /\ (a t \/ NEXT (a SBEFORE b) t))) /\
   (a UNTIL b = (\t. ~b t ==> a t /\ NEXT (a UNTIL b) t)) /\
   (a WHEN b = (\t. (if b t then a t else NEXT (a WHEN b) t))) /\
   (a BEFORE b = (\t. ~b t /\ (a t \/ NEXT (a BEFORE b) t))) /\
   (PALWAYS a = (\t. a t /\ PNEXT (PALWAYS a) t)) /\
   (PEVENTUAL a = (\t. a t \/ PSNEXT (PEVENTUAL a) t)) /\
   (a PSUNTIL b = (\t. b t \/ a t /\ PSNEXT (a PSUNTIL b) t)) /\
   (a PSWHEN b = (\t. a t /\ b t \/ ~b t /\ PSNEXT (a PSWHEN b) t)) /\
   (a PSBEFORE b = (\t. ~b t /\ (a t \/ PSNEXT (a PSBEFORE b) t))) /\
   (a PUNTIL b = (\t. b t \/ a t /\ PNEXT (a PUNTIL b) t)) /\
   (a PWHEN b = (\t. a t /\ b t \/ ~b t /\ PNEXT (a PWHEN b) t)) /\
   (a PBEFORE b = (\t. ~b t /\ (a t \/ PNEXT (a PBEFORE b) t)))

SBEFORE_EXPRESSIVE

|- (ALWAYS a = (\t. ~((\t. ~a t) SBEFORE (\t. F)) t)) /\
   (EVENTUAL a = (\t. (a SBEFORE (\t. F)) t)) /\
   (a SUNTIL b = (\t. (b SBEFORE (\t. ~a t /\ ~b t)) t)) /\
   (a UNTIL b = (\t. ~((\t. ~a t) SBEFORE b) t)) /\
   (a SWHEN b = (\t. (b SBEFORE (\t. ~a t /\ b t)) t)) /\
   (a WHEN b = (\t. ~(b SBEFORE (\t. a t /\ b t)) t)) /\
   (a BEFORE b = (\t. ~(b SBEFORE (\t. a t /\ ~b t)) t))

SEPARATE_BEFORE_THM

|- (a BEFORE (\t. b t \/ c t) = (\t. (a BEFORE b) t /\ (a BEFORE c) t)) /\
   ((\t. a t \/ b t) BEFORE c = (\t. (a BEFORE c) t \/ (b BEFORE c) t)) /\
   (a BEFORE (\t. b t /\ PNEXT c t) =
    (\t.
       ~(b t /\ PNEXT c t) /\
       (a t \/ (NEXT a BEFORE (\t. c t /\ NEXT b t)) t))) /\
   (a BEFORE (\t. b t /\ PSNEXT c t) =
    (\t.
       ~(b t /\ PSNEXT c t) /\
       (a t \/ (NEXT a BEFORE (\t. c t /\ NEXT b t)) t))) /\
   (a BEFORE (\t. b t /\ (c PSUNTIL d) t) =
    (\t.
       (((\t. ~c t) PBEFORE d) t \/ ((\t. a t \/ ~NEXT c t) BEFORE b) t) /\
       (a BEFORE (\t. d t /\ ((\t. ~a t /\ NEXT c t) SUNTIL b) t)) t)) /\
   (a BEFORE (\t. b t /\ (c PBEFORE d) t) =
    (\t.
       (((\t. ~c t) PSUNTIL d) t \/ ((\t. a t \/ NEXT d t) BEFORE b) t) /\
       (a BEFORE (\t. c t /\ ~d t /\ ((\t. ~a t /\ ~NEXT d t) SUNTIL b) t))
         t)) /\
   ((\t. a t /\ PNEXT b t) BEFORE c =
    (\t.
       ~c t /\ a t /\ PNEXT b t \/
       ~c t /\ ((\t. b t /\ NEXT a t) BEFORE NEXT c) t)) /\
   ((\t. a t /\ PSNEXT b t) BEFORE c =
    (\t.
       ~c t /\ a t /\ PSNEXT b t \/
       ~c t /\ ((\t. b t /\ NEXT a t) BEFORE NEXT c) t)) /\
   ((\t. a t /\ (b PBEFORE c) t) BEFORE d =
    (\t.
       (b PBEFORE c) t /\
       ((\t. ~d t /\ ~NEXT c t) SUNTIL (\t. a t /\ ~d t)) t \/
       ((\t.
           b t /\ ~c t /\
           ((\t. ~d t /\ ~NEXT c t) SUNTIL (\t. a t /\ ~d t)) t) BEFORE d)
         t)) /\
   ((\t. a t /\ (b PSUNTIL c) t) BEFORE d =
    (\t.
       (b PSUNTIL c) t /\
       ((\t. ~d t /\ NEXT b t) SUNTIL (\t. a t /\ ~d t)) t \/
       ((\t.
           c t /\ ((\t. ~d t /\ NEXT b t) SUNTIL (\t. a t /\ ~d t)) t) BEFORE
        d) t))

SEPARATE_NEXT_THM

|- (NEXT (\t. a t /\ PNEXT b t) = (\t. b t /\ NEXT a t)) /\
   (NEXT (\t. a t /\ PSNEXT b t) = (\t. b t /\ NEXT a t)) /\
   (NEXT (\t. a t /\ (b PSUNTIL c) t) =
    (\t.
       NEXT (\t. a t /\ c t) t \/
       (b PSUNTIL c) t /\ NEXT (\t. a t /\ b t) t)) /\
   (NEXT (\t. a t /\ (b PBEFORE c) t) =
    (\t.
       NEXT (\t. a t /\ b t /\ ~c t) t \/
       (b PBEFORE c) t /\ NEXT (\t. a t /\ ~c t) t)) /\
   (NEXT (\t. a t \/ PNEXT b t) = (\t. b t \/ NEXT a t)) /\
   (NEXT (\t. a t \/ PSNEXT b t) = (\t. b t \/ NEXT a t)) /\
   (NEXT (\t. a t \/ (b PSUNTIL c) t) =
    (\t. NEXT (\t. a t \/ c t) t \/ (b PSUNTIL c) t /\ NEXT b t)) /\
   (NEXT (\t. a t \/ (b PBEFORE c) t) =
    (\t.
       NEXT (\t. a t \/ ~c t) t /\
       ((b PBEFORE c) t \/ NEXT (\t. a t \/ b t) t)))

SEPARATE_PNEXT_THM

|- (PNEXT (\t. a t /\ NEXT b t) = (\t. InitPoint t \/ b t /\ PNEXT a t)) /\
   (PNEXT (\t. a t /\ (b SUNTIL c) t) =
    (\t.
       PNEXT (\t. a t /\ c t) t \/
       (b SUNTIL c) t /\ PNEXT (\t. a t /\ b t) t)) /\
   (PNEXT (\t. a t /\ (b BEFORE c) t) =
    (\t.
       PNEXT (\t. a t /\ b t /\ ~c t) t \/
       (b BEFORE c) t /\ PNEXT (\t. a t /\ ~c t) t)) /\
   (PNEXT (\t. a t \/ NEXT b t) = (\t. b t \/ PNEXT a t)) /\
   (PNEXT (\t. a t \/ (b SUNTIL c) t) =
    (\t. PNEXT (\t. a t \/ c t) t \/ (b SUNTIL c) t /\ PNEXT b t)) /\
   (PNEXT (\t. a t \/ (b BEFORE c) t) =
    (\t.
       PNEXT (\t. a t \/ ~c t) t /\
       ((b BEFORE c) t \/ PNEXT (\t. a t \/ b t) t)))

SEPARATE_PSUNTIL_THM

|- (a PSUNTIL (\t. b t \/ c t) = (\t. (a PSUNTIL b) t \/ (a PSUNTIL c) t)) /\
   (a PSUNTIL (\t. b t /\ NEXT c t) =
    (\t. b t /\ NEXT c t \/ (a PSUNTIL (\t. a t /\ c t /\ PSNEXT b t)) t)) /\
   (a PSUNTIL (\t. b t /\ (c SUNTIL d) t) =
    (\t.
       (c SUNTIL d) t /\ ((\t. a t /\ PNEXT c t) PSUNTIL b) t \/
       (a PSUNTIL (\t. d t /\ ((\t. a t /\ PNEXT c t) PSUNTIL b) t)) t)) /\
   (a PSUNTIL (\t. b t /\ (c BEFORE d) t) =
    (\t.
       (c BEFORE d) t /\ ((\t. a t /\ ~PNEXT d t) PSUNTIL b) t \/
       (a PSUNTIL (\t. c t /\ ~d t /\ ((\t. a t /\ ~PNEXT d t) PSUNTIL b) t))
         t)) /\
   ((\t. a t /\ b t) PSUNTIL c = (\t. (a PSUNTIL c) t /\ (b PSUNTIL c) t)) /\
   ((\t. a t \/ NEXT b t) PSUNTIL c =
    (\t.
       c t \/
       (a t \/ NEXT b t) /\ ((\t. b t \/ PNEXT a t) PSUNTIL PSNEXT c) t)) /\
   ((\t. a t \/ (b SUNTIL c) t) PSUNTIL d =
    (\t.
       ((b SUNTIL c) t \/
        ((\t. d t \/ PNEXT c t) PBEFORE (\t. ~a t /\ ~d t)) t) /\
       ((\t.
           b t \/ c t \/
           ((\t. d t \/ PNEXT c t) PBEFORE (\t. ~a t /\ ~d t)) t) PSUNTIL d)
         t)) /\
   ((\t. a t \/ (b BEFORE c) t) PSUNTIL d =
    (\t.
       ((b BEFORE c) t \/
        ((\t. d t \/ PSNEXT b t) PBEFORE (\t. ~a t /\ ~d t)) t) /\
       ((\t.
           ~c t \/
           ((\t. d t \/ PSNEXT b t) PBEFORE (\t. ~a t /\ ~d t)) t) PSUNTIL d)
         t))

SEPARATE_SUNTIL_THM

|- (a SUNTIL (\t. b t \/ c t) = (\t. (a SUNTIL b) t \/ (a SUNTIL c) t)) /\
   (a SUNTIL (\t. b t /\ PNEXT c t) =
    (\t. b t /\ PNEXT c t \/ (a SUNTIL (\t. a t /\ c t /\ NEXT b t)) t)) /\
   (a SUNTIL (\t. b t /\ PSNEXT c t) =
    (\t. b t /\ PSNEXT c t \/ (a SUNTIL (\t. a t /\ c t /\ NEXT b t)) t)) /\
   (a SUNTIL (\t. b t /\ (c PSUNTIL d) t) =
    (\t.
       (c PSUNTIL d) t /\ ((\t. a t /\ NEXT c t) SUNTIL b) t \/
       (a SUNTIL (\t. d t /\ ((\t. a t /\ NEXT c t) SUNTIL b) t)) t)) /\
   (a SUNTIL (\t. b t /\ (c PBEFORE d) t) =
    (\t.
       (c PBEFORE d) t /\ ((\t. a t /\ ~NEXT d t) SUNTIL b) t \/
       (a SUNTIL (\t. c t /\ ~d t /\ ((\t. a t /\ ~NEXT d t) SUNTIL b) t))
         t)) /\
   ((\t. a t /\ b t) SUNTIL c = (\t. (a SUNTIL c) t /\ (b SUNTIL c) t)) /\
   ((\t. a t \/ PNEXT b t) SUNTIL c =
    (\t.
       c t \/
       (a t \/ PNEXT b t) /\ ((\t. b t \/ NEXT a t) SUNTIL NEXT c) t)) /\
   ((\t. a t \/ PSNEXT b t) SUNTIL c =
    (\t.
       c t \/
       (a t \/ PSNEXT b t) /\ ((\t. b t \/ NEXT a t) SUNTIL NEXT c) t)) /\
   ((\t. a t \/ (b PSUNTIL c) t) SUNTIL d =
    (\t.
       ((b PSUNTIL c) t \/
        ((\t. d t \/ NEXT c t) BEFORE (\t. ~a t /\ ~d t)) t) /\
       ((\t.
           b t \/ c t \/
           ((\t. d t \/ NEXT c t) BEFORE (\t. ~a t /\ ~d t)) t) SUNTIL d)
         t)) /\
   ((\t. a t \/ (b PBEFORE c) t) SUNTIL d =
    (\t.
       ((b PBEFORE c) t \/
        ((\t. d t \/ NEXT b t) BEFORE (\t. ~a t /\ ~d t)) t) /\
       ((\t.
           ~c t \/ ((\t. d t \/ NEXT b t) BEFORE (\t. ~a t /\ ~d t)) t) SUNTIL
        d) t))

SIMPLIFY

|- (NEXT (\t. F) = (\t. F)) /\ (NEXT (\t. T) = (\t. T)) /\
   (ALWAYS (\t. T) = (\t. T)) /\ (ALWAYS (\t. F) = (\t. F)) /\
   (EVENTUAL (\t. T) = (\t. T)) /\ (EVENTUAL (\t. F) = (\t. F)) /\
   ((\t. F) SUNTIL b = b) /\ ((\t. T) SUNTIL b = EVENTUAL b) /\
   (a SUNTIL (\t. F) = (\t. F)) /\ (a SUNTIL (\t. T) = (\t. T)) /\
   (a SUNTIL a = a) /\ ((\t. F) UNTIL b = b) /\ ((\t. T) UNTIL b = (\t. T)) /\
   (a UNTIL (\t. F) = ALWAYS a) /\ (a UNTIL (\t. T) = (\t. T)) /\
   (a UNTIL a = a) /\ ((\t. F) SWHEN b = (\t. F)) /\
   ((\t. T) SWHEN b = EVENTUAL b) /\ (a SWHEN (\t. F) = (\t. F)) /\
   (a SWHEN (\t. T) = a) /\ (a SWHEN a = EVENTUAL a) /\
   ((\t. F) WHEN b = ALWAYS (\t. ~b t)) /\ ((\t. T) WHEN b = (\t. T)) /\
   (a WHEN (\t. F) = (\t. T)) /\ (a WHEN (\t. T) = a) /\
   (a WHEN a = (\t. T)) /\ ((\t. F) SBEFORE b = (\t. F)) /\
   ((\t. T) SBEFORE b = (\t. ~b t)) /\ (a SBEFORE (\t. F) = EVENTUAL a) /\
   (a SBEFORE (\t. T) = (\t. F)) /\ (a SBEFORE a = (\t. F)) /\
   ((\t. F) BEFORE b = ALWAYS (\t. ~b t)) /\
   ((\t. T) BEFORE b = (\t. ~b t)) /\ (a BEFORE (\t. F) = (\t. T)) /\
   (a BEFORE (\t. T) = (\t. F)) /\ (a BEFORE a = ALWAYS (\t. ~a t)) /\
   (PNEXT (\t. F) = InitPoint) /\ (PNEXT (\t. T) = (\t. T)) /\
   (PSNEXT (\t. F) = (\t. F)) /\ (PSNEXT (\t. T) = (\t. ~InitPoint t)) /\
   (PALWAYS (\t. T) = (\t. T)) /\ (PALWAYS (\t. F) = (\t. F)) /\
   (PEVENTUAL (\t. T) = (\t. T)) /\ (PEVENTUAL (\t. F) = (\t. F)) /\
   ((\t. F) PSUNTIL b = b) /\ ((\t. T) PSUNTIL b = PEVENTUAL b) /\
   (a PSUNTIL (\t. F) = (\t. F)) /\ (a PSUNTIL (\t. T) = (\t. T)) /\
   (a PSUNTIL a = a) /\ ((\t. F) PUNTIL b = b) /\
   ((\t. T) PUNTIL b = (\t. T)) /\ (a PUNTIL (\t. F) = PALWAYS a) /\
   (a PUNTIL (\t. T) = (\t. T)) /\ (a PUNTIL a = a) /\
   ((\t. F) PSWHEN b = (\t. F)) /\ ((\t. T) PSWHEN b = PEVENTUAL b) /\
   (a PSWHEN (\t. F) = (\t. F)) /\ (a PSWHEN (\t. T) = a) /\
   (a PSWHEN a = PEVENTUAL a) /\ ((\t. F) PWHEN b = PALWAYS (\t. ~b t)) /\
   ((\t. T) PWHEN b = (\t. T)) /\ (a PWHEN (\t. F) = (\t. T)) /\
   (a PWHEN (\t. T) = a) /\ (a PWHEN a = (\t. T)) /\
   ((\t. F) PSBEFORE b = (\t. F)) /\ ((\t. T) PSBEFORE b = (\t. ~b t)) /\
   (a PSBEFORE (\t. F) = PEVENTUAL a) /\ (a PSBEFORE (\t. T) = (\t. F)) /\
   (a PSBEFORE a = (\t. F)) /\ ((\t. F) PBEFORE b = PALWAYS (\t. ~b t)) /\
   ((\t. T) PBEFORE b = (\t. ~b t)) /\ (a PBEFORE (\t. F) = (\t. T)) /\
   (a PBEFORE (\t. T) = (\t. F)) /\ (a PBEFORE a = PALWAYS (\t. ~a t))

SOME_FUTURE_EVENT

|- (EVENTUAL b t0 = !a. (a WHEN b) t0 = (a SWHEN b) t0) /\
   (EVENTUAL b t0 = !a. (a UNTIL b) t0 = (a SUNTIL b) t0) /\
   (EVENTUAL b t0 = !a. (a BEFORE b) t0 = (a SBEFORE b) t0)

SOME_PAST_EVENT

|- PEVENTUAL b t ==>
   ((a PWHEN b) t = (a PSWHEN b) t) /\ ((a PUNTIL b) t = (a PSUNTIL b) t) /\
   ((a PBEFORE b) t = (a PSBEFORE b) t) /\
   ((b PBEFORE a) t = (b PSBEFORE a) t)

SUNTIL_EXPRESSIVE

|- (ALWAYS a = (\t. ~((\t. T) SUNTIL (\t. ~a t)) t)) /\
   (EVENTUAL a = (\t. ((\t. T) SUNTIL a) t)) /\
   (a UNTIL b = (\t. ~((\t. ~b t) SUNTIL (\t. ~a t /\ ~b t)) t)) /\
   (a WHEN b = (\t. ~((\t. ~a t \/ ~b t) SUNTIL (\t. ~a t /\ b t)) t)) /\
   (a BEFORE b = (\t. ~((\t. ~a t) SUNTIL b) t)) /\
   (a SWHEN b = (\t. ((\t. ~b t) SUNTIL (\t. a t /\ b t)) t)) /\
   (a SBEFORE b = (\t. ((\t. ~b t) SUNTIL (\t. a t /\ ~b t)) t))

SWHEN_EXPRESSIVE

|- (ALWAYS a = (\t. ~((\t. T) SWHEN (\t. ~a t)) t)) /\
   (EVENTUAL a = (\t. ((\t. T) SWHEN a) t)) /\
   (a SUNTIL b = (\t. (b SWHEN (\t. a t ==> b t)) t)) /\
   (a UNTIL b = (\t. ~((\t. ~b t) SWHEN (\t. a t ==> b t)) t)) /\
   (a WHEN b = (\t. ~((\t. ~a t) SWHEN b) t)) /\
   (a BEFORE b = (\t. ~(b SWHEN (\t. a t \/ b t)) t)) /\
   (a SBEFORE b = (\t. ((\t. ~b t) SWHEN (\t. a t \/ b t)) t))

UNTIL_EXPRESSIVE

|- (ALWAYS a = (\t. (a UNTIL (\t. F)) t)) /\
   (EVENTUAL a = (\t. ~((\t. ~a t) UNTIL (\t. F)) t)) /\
   (a SUNTIL b = (\t. ~((\t. ~b t) UNTIL (\t. ~a t /\ ~b t)) t)) /\
   (a WHEN b = (\t. ((\t. ~b t) UNTIL (\t. a t /\ b t)) t)) /\
   (a SWHEN b = (\t. ~((\t. ~a t \/ ~b t) UNTIL (\t. ~a t /\ b t)) t)) /\
   (a BEFORE b = (\t. ((\t. ~b t) UNTIL (\t. a t /\ ~b t)) t)) /\
   (a SBEFORE b = (\t. ~((\t. ~a t) UNTIL b) t))

WHEN_EXPRESSIVE

|- (ALWAYS a = (\t. ((\t. F) WHEN (\t. ~a t)) t)) /\
   (EVENTUAL a = (\t. ~((\t. F) WHEN a) t)) /\
   (a SUNTIL b = (\t. ~((\t. ~b t) WHEN (\t. a t ==> b t)) t)) /\
   (a UNTIL b = (\t. (b WHEN (\t. a t ==> b t)) t)) /\
   (a SWHEN b = (\t. ~((\t. ~a t) WHEN b) t)) /\
   (a BEFORE b = (\t. ((\t. ~b t) WHEN (\t. a t \/ b t)) t)) /\
   (a SBEFORE b = (\t. ~(b WHEN (\t. a t \/ b t)) t))