Theory: Temporal_Logic

Parents

• numeral
• pair

Types

Constants

• WATCH  :(num -> bool) -> (num -> bool) -> num -> bool
• SWHEN  :(num -> bool) -> (num -> bool) -> num -> bool
• UNTIL  :(num -> bool) -> (num -> bool) -> num -> bool
• NEXT  :(num -> bool) -> num -> bool
• WHEN  :(num -> bool) -> (num -> bool) -> num -> bool
• ALWAYS  :(num -> bool) -> num -> bool
• UPTO  :num # num # (num -> bool) -> bool
• EVENTUAL  :(num -> bool) -> num -> bool
• BEFORE  :(num -> bool) -> (num -> bool) -> num -> bool
• SUNTIL  :(num -> bool) -> (num -> bool) -> num -> bool
• SBEFORE  :(num -> bool) -> (num -> bool) -> num -> bool

Definitions

ALWAYS

|- !P t0. ALWAYS P t0 = !t. P (t + t0)

BEFORE

|- !a b t0.
     (a BEFORE b) t0 =
     ?q.
       (q WATCH b) t0 /\
       ((?t. ~q (t + t0) /\ ~b (t + t0) /\ a (t + t0)) \/ !t. ~b (t + t0))

EVENTUAL

|- !P t0. EVENTUAL P t0 = ?t. P (t + t0)

NEXT

|- !P. NEXT P = (\t. P (SUC t))

SBEFORE

|- !a b t0.
     (a SBEFORE b) t0 =
     ?q. (q WATCH b) t0 /\ ?t. ~q (t + t0) /\ ~b (t + t0) /\ a (t + t0)

SUNTIL

|- !a b t0.
     (a SUNTIL b) t0 =
     ?q.
       (q WATCH b) t0 /\ (!t. q (t + t0) \/ b (t + t0) \/ a (t + t0)) /\
       ?t. b (t + t0)

SWHEN

|- !a b t0.
     (a SWHEN b) t0 =
     ?q. (q WATCH b) t0 /\ ?t. ~q (t + t0) /\ b (t + t0) /\ a (t + t0)

UNTIL

|- !a b t0.
     (a UNTIL b) t0 =
     ?q. (q WATCH b) t0 /\ !t. q (t + t0) \/ b (t + t0) \/ a (t + t0)

UPTO

|- !t0 t1 a. UPTO (t0,t1,a) = !t2. t0 <= t2 /\ t2 < t1 ==> a t2

WATCH

|- !q b t0.
     (q WATCH b) t0 =
     !t. (q t0 = F) /\ (q (SUC (t + t0)) = q (t + t0) \/ b (t + t0))

WHEN

|- !a b t0.
     (a WHEN b) t0 =
     ?q. (q WATCH b) t0 /\ !t. q (t + t0) \/ (b (t + t0) ==> a (t + t0))

Theorems

ALWAYS_AS_BEFORE

|- ALWAYS b = (\t. F) BEFORE (\t. ~b t)

ALWAYS_AS_SBEFORE

|- ALWAYS b = (\t0. ~((\t. ~b t) SBEFORE (\t. F)) t0)

ALWAYS_AS_SUNTIL

|- ALWAYS a = (\t. ~((\t. T) SUNTIL (\t. ~a t)) t)

ALWAYS_AS_SWHEN

|- ALWAYS a = (\t. ~((\t. T) SWHEN (\t. ~a t)) t)

ALWAYS_AS_UNTIL

|- ALWAYS a = a UNTIL (\t. F)

ALWAYS_AS_WHEN

|- ALWAYS a = (\t. F) WHEN (\t. ~a t)

ALWAYS_FIX

|- (y = (\t. a t /\ y (t + 1))) = (y = ALWAYS a) \/ (y = (\t. F))

ALWAYS_IDEM

|- ALWAYS a = ALWAYS (ALWAYS a)

ALWAYS_INVARIANT

|- ALWAYS a t0 = ?J. J t0 /\ !t. J (t + t0) ==> a (t + t0) /\ J (t + (t0 + 1))

ALWAYS_LINORD

|- ALWAYS a t0 = !t1. t0 <= t1 ==> a t1

ALWAYS_NEXT

|- !a. NEXT (ALWAYS a) = ALWAYS (NEXT a)

ALWAYS_REC

|- ALWAYS P t0 = P t0 /\ NEXT (ALWAYS P) t0

ALWAYS_SIGNAL

|- ALWAYS a t0 = !t. a (t + t0)

AND_NEXT

|- !Q P. NEXT (\t. P t /\ Q t) = (\t. NEXT P t /\ NEXT Q t)

BEFORE_AS_NOT_SWHEN

|- a BEFORE b = (\t0. ~(b SWHEN (\t. a t \/ b t)) t0)

BEFORE_AS_SBEFORE

|- a BEFORE b = (\t0. (a SBEFORE b) t0 \/ ALWAYS (\t. ~b t) t0)

BEFORE_AS_SUNTIL

|- a BEFORE b = (\t. ~((\t. ~a t) SUNTIL b) t)

BEFORE_AS_SWHEN

|- a BEFORE b =
   (\t0.
      ((\t. ~b t) SWHEN (\t. a t \/ b t)) t0 \/ ALWAYS (\t. ~a t /\ ~b t) t0)

BEFORE_AS_UNTIL

|- a BEFORE b = (\t0. ~((\t. ~a t) UNTIL b) t0 \/ ALWAYS (\t. ~b t) t0)

BEFORE_AS_WHEN

|- a BEFORE b = (\t. ~b t) WHEN (\t. a t \/ b t)

BEFORE_AS_WHEN_UNTIL

|- a BEFORE b = (\t. ((\t. ~b t) UNTIL a) t /\ ((\t. ~b t) WHEN a) t)

BEFORE_EVENT

|- a BEFORE b = (\t. a t /\ ~b t) BEFORE b

BEFORE_FIX

|- !y.
     (y = (\t. ~b t /\ (a t \/ y (t + 1)))) =
     (y = a BEFORE b) \/ (y = a SBEFORE b)

BEFORE_HW

|- (a BEFORE b) t0 = ?q. (q WATCH a) t0 /\ !t. q (t + t0) \/ ~b (t + t0)

BEFORE_IDEM

|- a BEFORE b = (a BEFORE b) BEFORE b

BEFORE_IMP

|- (a BEFORE b) t0 =
   !q.
     (q WATCH b) t0 ==>
     (?t. ~q (t + t0) /\ ~b (t + t0) /\ a (t + t0)) \/ !t. ~b (t + t0)

BEFORE_INVARIANT

|- (a BEFORE b) t0 =
   ?J.
     J t0 /\ (!t. J (t + t0) /\ ~a (t + t0) ==> J (SUC (t + t0))) /\
     !d. J (d + t0) ==> ~b (d + t0)

BEFORE_LINORD

|- (a BEFORE b) t0 = !t1. t0 <= t1 /\ UPTO (t0,t1,(\t. ~a t)) ==> ~b t1

BEFORE_NEXT

|- !a b. NEXT (a BEFORE b) = NEXT a BEFORE NEXT b

BEFORE_REC

|- (a BEFORE b) t0 = ~b t0 /\ (a t0 \/ NEXT (a BEFORE b) t0)

BEFORE_SIGNAL

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

BEFORE_SIMP

|- ((\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))

DELTA_CASES

|- (?d. (!t. t < d ==> ~b (t + t0)) /\ b (d + t0)) \/ !d. ~b (d + t0)

EQUIV_NEXT

|- !Q P. NEXT (\t. P t = Q t) = (\t. NEXT P t = NEXT Q t)

EVENTUAL_AS_BEFORE

|- EVENTUAL b = (\t0. ~((\t. F) BEFORE b) t0)

EVENTUAL_AS_SBEFORE

|- EVENTUAL b = b SBEFORE (\t. F)

EVENTUAL_AS_SUNTIL

|- EVENTUAL a = (\t. T) SUNTIL a

EVENTUAL_AS_SWHEN

|- EVENTUAL a = (\t. T) SWHEN a

EVENTUAL_AS_UNTIL

|- EVENTUAL a = (\t. ~((\t. ~a t) UNTIL (\t. F)) t)

EVENTUAL_AS_WHEN

|- EVENTUAL a = (\t. ~((\t. F) WHEN a) t)

EVENTUAL_FIX

|- (y = (\t. a t \/ y (t + 1))) = (y = EVENTUAL a) \/ (y = (\t. T))

EVENTUAL_IDEM

|- EVENTUAL a = EVENTUAL (EVENTUAL a)

EVENTUAL_INVARIANT

|- EVENTUAL b t0 =
   ?J.
     0 < J t0 /\
     (!t. J (SUC (t + t0)) < J (t + t0) \/ (J (SUC (t + t0)) = 0)) /\
     !t. 0 < J (t + t0) /\ (J (SUC (t + t0)) = 0) ==> b (t + t0)

EVENTUAL_LINORD

|- EVENTUAL a t0 = ?t1. t0 <= t1 /\ a t1

EVENTUAL_NEXT

|- !a. NEXT (EVENTUAL a) = EVENTUAL (NEXT a)

EVENTUAL_REC

|- EVENTUAL P t0 = P t0 \/ NEXT (EVENTUAL P) t0

EVENTUAL_SIGNAL

|- EVENTUAL a t0 = ?t. a (t + t0)

IMMEDIATE_EVENT

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

IMP_NEXT

|- !Q P. NEXT (\t. P t ==> Q t) = (\t. NEXT P t ==> NEXT Q t)

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)

NEXT_LINORD

|- NEXT a t0 = ?t1. t0 < t1 /\ (!t3. t0 < t3 ==> t1 <= t3) /\ a t1

NO_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

NOT_ALWAYS

|- ~ALWAYS a t0 = EVENTUAL (\t. ~a t) t0

NOT_BEFORE

|- ~(a BEFORE b) t0 = ((\t. ~a t) SUNTIL b) t0

NOT_EVENTUAL

|- ~EVENTUAL a t0 = ALWAYS (\t. ~a t) t0

NOT_NEXT

|- !P. NEXT (\t. ~P t) = (\t. ~NEXT P t)

NOT_SBEFORE

|- ~(a SBEFORE b) t0 = ((\t. ~a t) UNTIL b) t0

NOT_SUNTIL

|- ~(a SUNTIL b) t0 = ((\t. ~a t) BEFORE b) t0

NOT_SWHEN

|- ~(a SWHEN b) t0 = ((\t. ~a t) WHEN b) t0

NOT_UNTIL

|- ~(a UNTIL b) t0 = ((\t. ~a t) SBEFORE b) t0

NOT_WHEN

|- ~(a WHEN b) t0 = ((\t. ~a t) SWHEN b) t0

OR_NEXT

|- !Q P. NEXT (\t. P t \/ Q t) = (\t. NEXT P t \/ NEXT Q t)

SBEFORE_AS_BEFORE

|- a SBEFORE b = (\t0. (a BEFORE b) t0 /\ EVENTUAL a t0)

SBEFORE_AS_SUNTIL

|- a SBEFORE b = (\t0. ~((\t. ~a t) SUNTIL b) t0 /\ EVENTUAL a t0)

SBEFORE_AS_SWHEN

|- a SBEFORE b = (\t. ~b t) SWHEN (\t. a t \/ b t)

SBEFORE_AS_UNTIL

|- a SBEFORE b = (\t0. ~((\t. ~a t) UNTIL b) t0)

SBEFORE_AS_WHEN

|- a SBEFORE b = (\t0. ((\t. ~b t) WHEN (\t. a t \/ b t)) t0 /\ EVENTUAL a t0)

SBEFORE_EVENT

|- a SBEFORE b = (\t. a t /\ ~b t) SBEFORE b

SBEFORE_IDEM

|- a SBEFORE b = (a SBEFORE b) SBEFORE b

SBEFORE_IMP

|- (a SBEFORE b) t0 =
   !q. (q WATCH b) t0 ==> ?t. ~q (t + t0) /\ ~b (t + t0) /\ a (t + t0)

SBEFORE_INVARIANT

|- (a SBEFORE b) t0 =
   (?J1.
      J1 t0 /\ (!t. J1 (t + t0) /\ ~a (t + t0) ==> J1 (SUC (t + t0))) /\
      !d. J1 (d + t0) ==> ~b (d + t0)) /\
   ?J2.
     0 < J2 t0 /\
     (!t. J2 (SUC (t + t0)) < J2 (t + t0) \/ (J2 (SUC (t + t0)) = 0)) /\
     !t. 0 < J2 (t + t0) /\ (J2 (SUC (t + t0)) = 0) ==> a (t + t0)

SBEFORE_LINORD

|- (a SBEFORE b) t0 =
   ?t1. t0 <= t1 /\ a t1 /\ ~b t1 /\ UPTO (t0,t1,(\t. ~b t))

SBEFORE_NEXT

|- !a b. NEXT (a SBEFORE b) = NEXT a SBEFORE NEXT b

SBEFORE_REC

|- (a SBEFORE b) t0 = ~b t0 /\ (a t0 \/ NEXT (a SBEFORE b) t0)

SBEFORE_SIGNAL

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

SBEFORE_SIMP

|- ((\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))

SOME_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)

SUNTIL_AS_BEFORE

|- a SUNTIL b = (\t0. ~((\t. ~a t) BEFORE b) t0)

SUNTIL_AS_SBEFORE

|- a SUNTIL b = (\t0. ~((\t. ~a t) SBEFORE b) t0 /\ EVENTUAL b t0)

SUNTIL_AS_SWHEN

|- a SUNTIL b = b SWHEN (\t. a t ==> b t)

SUNTIL_AS_UNTIL

|- a SUNTIL b = (\t0. (a UNTIL b) t0 /\ EVENTUAL b t0)

SUNTIL_AS_WHEN

|- a SUNTIL b = (\t. (b WHEN (\t. a t ==> b t)) t /\ EVENTUAL b t)

SUNTIL_EVENT

|- a SUNTIL b = (\t. a t /\ ~b t) SUNTIL b

SUNTIL_IDEM

|- a SUNTIL b = (a SUNTIL b) SUNTIL b

SUNTIL_IMP

|- (a SUNTIL b) t0 =
   !q.
     (q WATCH b) t0 ==>
     (!t. q (t + t0) \/ b (t + t0) \/ a (t + t0)) /\ ?t. b (t + t0)

SUNTIL_INVARIANT

|- (a SUNTIL b) t0 =
   (?J1.
      J1 t0 /\
      !t. J1 (t + t0) /\ ~b (t + t0) ==> a (t + t0) /\ J1 (SUC (t + t0))) /\
   ?J2.
     0 < J2 t0 /\
     (!t. J2 (SUC (t + t0)) < J2 (t + t0) \/ (J2 (SUC (t + t0)) = 0)) /\
     !t. 0 < J2 (t + t0) /\ (J2 (SUC (t + t0)) = 0) ==> b (t + t0)

SUNTIL_LINORD

|- (a SUNTIL b) t0 = ?t1. t0 <= t1 /\ b t1 /\ UPTO (t0,t1,a)

SUNTIL_NEXT

|- !a b. NEXT (a SUNTIL b) = NEXT a SUNTIL NEXT b

SUNTIL_REC

|- (a SUNTIL b) t0 = ~b t0 ==> a t0 /\ NEXT (a SUNTIL b) t0

SUNTIL_SIGNAL

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

SUNTIL_SIMP

|- ((\t. F) SUNTIL b = (\t. b t)) /\ ((\t. T) SUNTIL b = EVENTUAL b) /\
   (a SUNTIL (\t. F) = (\t. F)) /\ (a SUNTIL (\t. T) = (\t. T)) /\
   (a SUNTIL a = (\t. a t))

SWHEN_AS_BEFORE

|- a SWHEN b = (\t0. ~(b BEFORE (\t. a t /\ b t)) t0)

SWHEN_AS_NOT_WHEN

|- (a SWHEN b) t0 = ~((\t. ~a t) WHEN b) t0

SWHEN_AS_SBEFORE

|- a SWHEN b = b SBEFORE (\t. ~a t /\ b t)

SWHEN_AS_SUNTIL

|- a SWHEN b = (\t. ~b t) SUNTIL (\t. a t /\ b t)

SWHEN_AS_UNTIL

|- a SWHEN b = (\t. ((\t. ~b t) UNTIL (\t. a t /\ b t)) t /\ EVENTUAL b t)

SWHEN_AS_WHEN

|- a SWHEN b = (\t0. (a WHEN b) t0 /\ EVENTUAL b t0)

SWHEN_EVENT

|- a SWHEN b = (\t. a t /\ b t) SWHEN b

SWHEN_IDEM

|- a SWHEN b = (a SWHEN b) SWHEN b

SWHEN_IMP

|- (a SWHEN b) t0 =
   !q. (q WATCH b) t0 ==> ?t. ~q (t + t0) /\ b (t + t0) /\ a (t + t0)

SWHEN_INVARIANT

|- (a SWHEN b) t0 =
   (?J1.
      J1 t0 /\ (!t. ~b (t + t0) /\ J1 (t + t0) ==> J1 (SUC (t + t0))) /\
      !d. b (d + t0) /\ J1 (d + t0) ==> a (d + t0)) /\
   ?J2.
     0 < J2 t0 /\
     (!t. J2 (SUC (t + t0)) < J2 (t + t0) \/ (J2 (SUC (t + t0)) = 0)) /\
     !t. 0 < J2 (t + t0) /\ (J2 (SUC (t + t0)) = 0) ==> b (t + t0)

SWHEN_LINORD

|- (a SWHEN b) t0 = ?t1. t0 <= t1 /\ a t1 /\ b t1 /\ UPTO (t0,t1,(\t. ~b t))

SWHEN_NEXT

|- !a b. NEXT (a SWHEN b) = NEXT a SWHEN NEXT b

SWHEN_REC

|- (a SWHEN b) t0 = (if b t0 then a t0 else NEXT (a SWHEN b) t0)

SWHEN_SIGNAL

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

SWHEN_SIMP

|- ((\t. F) SWHEN b = (\t. F)) /\ ((\t. T) SWHEN b = EVENTUAL b) /\
   (a SWHEN (\t. F) = (\t. F)) /\ (a SWHEN (\t. T) = (\t. a t)) /\
   (a SWHEN a = EVENTUAL a)

UNTIL_AS_BEFORE

|- a UNTIL b = (\t0. ~((\t. ~a t) BEFORE b) t0 \/ ALWAYS a t0)

UNTIL_AS_SBEFORE

|- a UNTIL b = (\t0. ~((\t. ~a t) SBEFORE b) t0)

UNTIL_AS_SUNTIL

|- a UNTIL b = (\t. (a SUNTIL b) t \/ ALWAYS a t)

UNTIL_AS_SWHEN

|- a UNTIL b = (\t. (b SWHEN (\t. a t ==> b t)) t \/ ALWAYS a t)

UNTIL_AS_WHEN

|- a UNTIL b = b WHEN (\t. a t ==> b t)

UNTIL_EVENT

|- a UNTIL b = (\t. a t /\ ~b t) UNTIL b

UNTIL_FIX

|- (y = (\t. ~b t ==> a t /\ y (t + 1))) = (y = a UNTIL b) \/ (y = a SUNTIL b)

UNTIL_IDEM

|- a UNTIL b = (a UNTIL b) UNTIL b

UNTIL_IMP

|- (a UNTIL b) t0 =
   !q. (q WATCH b) t0 ==> !t. q (t + t0) \/ b (t + t0) \/ a (t + t0)

UNTIL_INVARIANT

|- !t0.
     (a UNTIL b) t0 =
     ?J.
       J t0 /\
       !t. J (t + t0) /\ ~b (t + t0) ==> a (t + t0) /\ J (SUC (t + t0))

UNTIL_LINORD

|- (a UNTIL b) t0 = !t1. t0 <= t1 /\ ~b t1 /\ UPTO (t0,t1,(\t. ~b t)) ==> a t1

UNTIL_NEXT

|- !a b. NEXT (a UNTIL b) = NEXT a UNTIL NEXT b

UNTIL_REC

|- (a UNTIL b) t0 = ~b t0 ==> a t0 /\ NEXT (a UNTIL b) t0

UNTIL_SIGNAL

|- (a UNTIL b) t0 =
   ((!t. ~b (t + t0)) ==> !t. a (t + t0)) /\
   !d. (!t. t < d ==> ~b (t + t0)) /\ b (d + t0) ==> !t. t < d ==> a (t + t0)

UNTIL_SIMP

|- ((\t. F) UNTIL b = (\t. b t)) /\ ((\t. T) UNTIL b = (\t. T)) /\
   (a UNTIL (\t. F) = ALWAYS a) /\ (a UNTIL (\t. T) = (\t. T)) /\
   (a UNTIL a = (\t. a t))

WATCH_EXISTS

|- !b t0. ?q. (q WATCH b) t0

WATCH_REC

|- (q WATCH b) t0 =
   ~q t0 /\ (if b t0 then NEXT (ALWAYS q) t0 else NEXT (q WATCH b) t0)

WATCH_SIGNAL

|- (q WATCH b) t0 =
   ((!t. ~b (t + t0)) ==> !t. ~q (t + t0)) /\
   !d.
     b (d + t0) /\ (!t. t < d ==> ~b (t + t0)) ==>
     (!t. t <= d ==> ~q (t + t0)) /\ !t. q (SUC (t + (d + t0)))

WELL_ORDER

|- (?n. P n) = ?m. P m /\ !n. n < m ==> ~P n

WELL_ORDER_UNIQUE

|- !m2 m1 P.
     (P m1 /\ !n. n < m1 ==> ~P n) /\ P m2 /\ (!n. n < m2 ==> ~P n) ==>
     (m1 = m2)

WHEN_AS_BEFORE

|- a WHEN b = (\t0. ~(b BEFORE (\t. a t /\ b t)) t0 \/ ALWAYS (\t. ~b t) t0)

WHEN_AS_NOT_SWHEN

|- (a WHEN b) t0 = ~((\t. ~a t) SWHEN b) t0

WHEN_AS_SBEFORE

|- a WHEN b = (\t0. (b SBEFORE (\t. ~a t /\ b t)) t0 \/ ALWAYS (\t. ~b t) t0)

WHEN_AS_SUNTIL

|- a WHEN b =
   (\t. ((\t. ~b t) SUNTIL (\t. a t /\ b t)) t \/ ALWAYS (\t. ~b t) t)

WHEN_AS_SWHEN

|- a WHEN b = (\t. (a SWHEN b) t \/ ALWAYS (\t. ~b t) t)

WHEN_AS_UNTIL

|- a WHEN b = (\t. ~b t) UNTIL (\t. a t /\ b t)

WHEN_EVENT

|- a WHEN b = (\t. a t /\ b t) WHEN b

WHEN_FIX

|- (y = (\t. (if b t then a t else y (t + 1)))) =
   (y = a WHEN b) \/ (y = a SWHEN b)

WHEN_IDEM

|- a WHEN b = (a WHEN b) WHEN b

WHEN_IMP

|- (a WHEN b) t0 =
   !q. (q WATCH b) t0 ==> !t. q (t + t0) \/ (b (t + t0) ==> a (t + t0))

WHEN_INVARIANT

|- (a WHEN b) t0 =
   ?J.
     J t0 /\ (!t. ~b (t + t0) /\ J (t + t0) ==> J (SUC (t + t0))) /\
     !d. b (d + t0) /\ J (d + t0) ==> a (d + t0)

WHEN_LINORD

|- (a WHEN b) t0 = !t1. t0 <= t1 /\ b t1 /\ UPTO (t0,t1,(\t. ~b t)) ==> a t1

WHEN_NEXT

|- !a b. NEXT (a WHEN b) = NEXT a WHEN NEXT b

WHEN_REC

|- (a WHEN b) t0 = (if b t0 then a t0 else NEXT (a WHEN b) t0)

WHEN_SIGNAL

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

WHEN_SIMP

|- ((\t. F) WHEN b = ALWAYS (\t. ~b t)) /\ ((\t. T) WHEN b = (\t. T)) /\
   (a WHEN (\t. F) = (\t. T)) /\ (a WHEN (\t. T) = (\t. a t)) /\
   (a WHEN a = (\t. T))

WHEN_SWHEN_LEMMA

|- (if !t1. ?t2. b (t2 + t1) then
      !t0. (a WHEN b) t0 = (a SWHEN b) t0
    else
      ?t1. !t2. (a WHEN b) (t2 + t1) /\ ~(a SWHEN b) (t2 + t1))