Theory "Temporal_Logic"

Signature

Definitions

NEXT

⊢ ∀P. NEXT P = (λt. P (SUC t))

ALWAYS

⊢ ∀P t0. ALWAYS P t0 ⇔ ∀t. P (t + t0)

EVENTUAL

⊢ ∀P t0. EVENTUAL P t0 ⇔ ∃t. P (t + t0)

WATCH

⊢ ∀q b t0.
      (q WATCH b) t0 ⇔
      ∀t. (q t0 ⇔ F) ∧ (q (SUC (t + t0)) ⇔ q (t + t0) ∨ b (t + t0))

UPTO

⊢ ∀t0 t1 a. UPTO (t0,t1,a) ⇔ ∀t2. t0 ≤ t2 ∧ t2 < t1 ⇒ a t2

WHEN

⊢ ∀a b t0.
      (a WHEN 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)

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

SWHEN

⊢ ∀a b t0.
      (a SWHEN 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)

SBEFORE

⊢ ∀a b t0.
      (a SBEFORE b) t0 ⇔
      ∃q. (q WATCH b) t0 ∧ ∃t. ¬q (t + t0) ∧ ¬b (t + t0) ∧ a (t + t0)

Theorems

WATCH_EXISTS

⊢ ∀b t0. ∃q. (q WATCH b) 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

DELTA_CASES

⊢ (∃d. (∀t. t < d ⇒ ¬b (t + t0)) ∧ b (d + t0)) ∨ ∀d. ¬b (d + t0)

WHEN_IMP

⊢ (a WHEN b) t0 ⇔
  ∀q. (q WATCH b) t0 ⇒ ∀t. q (t + t0) ∨ (b (t + t0) ⇒ a (t + t0))

UNTIL_IMP

⊢ (a UNTIL b) t0 ⇔
  ∀q. (q WATCH b) t0 ⇒ ∀t. q (t + t0) ∨ b (t + t0) ∨ a (t + t0)

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)

SWHEN_IMP

⊢ (a SWHEN b) t0 ⇔
  ∀q. (q WATCH b) t0 ⇒ ∃t. ¬q (t + t0) ∧ b (t + t0) ∧ a (t + t0)

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)

SBEFORE_IMP

⊢ (a SBEFORE b) t0 ⇔
  ∀q. (q WATCH b) t0 ⇒ ∃t. ¬q (t + t0) ∧ ¬b (t + t0) ∧ a (t + t0)

ALWAYS_SIGNAL

⊢ ALWAYS a t0 ⇔ ∀t. a (t + t0)

EVENTUAL_SIGNAL

⊢ EVENTUAL a t0 ⇔ ∃t. a (t + 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)))

WHEN_SIGNAL

⊢ (a WHEN b) t0 ⇔
  ∀delta. (∀t. t < delta ⇒ ¬b (t + t0)) ∧ b (delta + t0) ⇒ a (delta + 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)

BEFORE_SIGNAL

⊢ (a BEFORE b) t0 ⇔
  ∀delta.
      (∀t. t < delta ⇒ ¬b (t + t0)) ∧ b (delta + t0) ⇒
      ∃t. t < delta ∧ a (t + t0)

SWHEN_SIGNAL

⊢ (a SWHEN b) t0 ⇔
  ∃delta. (∀t. t < delta ⇒ ¬b (t + t0)) ∧ b (delta + t0) ∧ a (delta + t0)

SUNTIL_SIGNAL

⊢ (a SUNTIL b) t0 ⇔
  ∃delta. (∀t. t < delta ⇒ a (t + t0) ∧ ¬b (t + t0)) ∧ b (delta + t0)

SBEFORE_SIGNAL

⊢ (a SBEFORE b) t0 ⇔ ∃delta. a (delta + t0) ∧ ∀t. t ≤ delta ⇒ ¬b (t + t0)

NEXT_LINORD

⊢ NEXT a t0 ⇔ ∃t1. t0 < t1 ∧ (∀t3. t0 < t3 ⇒ t1 ≤ t3) ∧ a t1

ALWAYS_LINORD

⊢ ALWAYS a t0 ⇔ ∀t1. t0 ≤ t1 ⇒ a t1

EVENTUAL_LINORD

⊢ EVENTUAL a t0 ⇔ ∃t1. t0 ≤ t1 ∧ a t1

SUNTIL_LINORD

⊢ (a SUNTIL b) t0 ⇔ ∃t1. t0 ≤ t1 ∧ b t1 ∧ UPTO (t0,t1,a)

UNTIL_LINORD

⊢ (a UNTIL b) t0 ⇔ ∀t1. t0 ≤ t1 ∧ ¬b t1 ∧ UPTO (t0,t1,(λt. ¬b t)) ⇒ a t1

SBEFORE_LINORD

⊢ (a SBEFORE b) t0 ⇔ ∃t1. t0 ≤ t1 ∧ a t1 ∧ ¬b t1 ∧ UPTO (t0,t1,(λt. ¬b t))

BEFORE_LINORD

⊢ (a BEFORE b) t0 ⇔ ∀t1. t0 ≤ t1 ∧ UPTO (t0,t1,(λt. ¬a t)) ⇒ ¬b t1

SWHEN_LINORD

⊢ (a SWHEN b) t0 ⇔ ∃t1. t0 ≤ t1 ∧ a t1 ∧ b t1 ∧ UPTO (t0,t1,(λt. ¬b t))

WHEN_LINORD

⊢ (a WHEN b) t0 ⇔ ∀t1. t0 ≤ t1 ∧ b t1 ∧ UPTO (t0,t1,(λt. ¬b t)) ⇒ a t1

ALWAYS_AS_WHEN

⊢ ALWAYS a = ((λt. F) WHEN (λt. ¬a t))

EVENTUAL_AS_WHEN

⊢ EVENTUAL a = (λt. ¬((λt. F) WHEN a) t)

UNTIL_AS_WHEN

⊢ (a UNTIL b) = (b WHEN (λt. a t ⇒ b t))

BEFORE_AS_WHEN

⊢ (a BEFORE b) = ((λt. ¬b t) WHEN (λt. a t ∨ b t))

SWHEN_AS_WHEN

⊢ (a SWHEN b) = (λt0. (a WHEN b) t0 ∧ EVENTUAL b t0)

SWHEN_AS_NOT_WHEN

⊢ (a SWHEN b) t0 ⇔ ¬((λt. ¬a t) WHEN b) t0

SUNTIL_AS_WHEN

⊢ (a SUNTIL b) = (λt. (b WHEN (λt. a t ⇒ b t)) t ∧ EVENTUAL b t)

SBEFORE_AS_WHEN

⊢ (a SBEFORE b) = (λt0. ((λt. ¬b t) WHEN (λt. a t ∨ b t)) t0 ∧ EVENTUAL a t0)

BEFORE_AS_WHEN_UNTIL

⊢ (a BEFORE b) = (λt. ((λt. ¬b t) UNTIL a) t ∧ ((λt. ¬b t) WHEN a) t)

BEFORE_HW

⊢ (a BEFORE b) t0 ⇔ ∃q. (q WATCH a) t0 ∧ ∀t. q (t + t0) ∨ ¬b (t + t0)

ALWAYS_AS_UNTIL

⊢ ALWAYS a = (a UNTIL (λt. F))

EVENTUAL_AS_UNTIL

⊢ EVENTUAL a = (λt. ¬((λt. ¬a t) UNTIL (λt. F)) t)

WHEN_AS_UNTIL

⊢ (a WHEN b) = ((λt. ¬b t) UNTIL (λt. a t ∧ b t))

BEFORE_AS_UNTIL

⊢ (a BEFORE b) = (λt0. ¬((λt. ¬a t) UNTIL b) t0 ∨ ALWAYS (λt. ¬b t) t0)

SWHEN_AS_UNTIL

⊢ (a SWHEN b) = (λt. ((λt. ¬b t) UNTIL (λt. a t ∧ b t)) t ∧ EVENTUAL b t)

SUNTIL_AS_UNTIL

⊢ (a SUNTIL b) = (λt0. (a UNTIL b) t0 ∧ EVENTUAL b t0)

SBEFORE_AS_UNTIL

⊢ (a SBEFORE b) = (λt0. ¬((λt. ¬a t) UNTIL b) t0)

ALWAYS_AS_BEFORE

⊢ ALWAYS b = ((λt. F) BEFORE (λt. ¬b t))

EVENTUAL_AS_BEFORE

⊢ EVENTUAL b = (λt0. ¬((λt. F) BEFORE b) t0)

WHEN_AS_BEFORE

⊢ (a WHEN b) = (λt0. ¬(b BEFORE (λt. a t ∧ b t)) t0 ∨ ALWAYS (λt. ¬b t) t0)

UNTIL_AS_BEFORE

⊢ (a UNTIL b) = (λt0. ¬((λt. ¬a t) BEFORE b) t0 ∨ ALWAYS a t0)

SWHEN_AS_BEFORE

⊢ (a SWHEN b) = (λt0. ¬(b BEFORE (λt. a t ∧ b t)) t0)

SUNTIL_AS_BEFORE

⊢ (a SUNTIL b) = (λt0. ¬((λt. ¬a t) BEFORE b) t0)

SBEFORE_AS_BEFORE

⊢ (a SBEFORE b) = (λt0. (a BEFORE b) t0 ∧ EVENTUAL a t0)

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)

ALWAYS_AS_SWHEN

⊢ ALWAYS a = (λt. ¬((λt. T) SWHEN (λt. ¬a t)) t)

EVENTUAL_AS_SWHEN

⊢ EVENTUAL a = ((λt. T) SWHEN a)

WHEN_AS_SWHEN

⊢ (a WHEN b) = (λt. (a SWHEN b) t ∨ ALWAYS (λt. ¬b t) t)

WHEN_AS_NOT_SWHEN

⊢ (a WHEN b) t0 ⇔ ¬((λt. ¬a t) SWHEN b) t0

UNTIL_AS_SWHEN

⊢ (a UNTIL b) = (λt. (b SWHEN (λt. a t ⇒ b t)) t ∨ ALWAYS a 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_NOT_SWHEN

⊢ (a BEFORE b) = (λt0. ¬(b SWHEN (λt. a t ∨ b t)) t0)

SUNTIL_AS_SWHEN

⊢ (a SUNTIL b) = (b SWHEN (λt. a t ⇒ b t))

SBEFORE_AS_SWHEN

⊢ (a SBEFORE b) = ((λt. ¬b t) SWHEN (λt. a t ∨ b t))

ALWAYS_AS_SUNTIL

⊢ ALWAYS a = (λt. ¬((λt. T) SUNTIL (λt. ¬a t)) t)

EVENTUAL_AS_SUNTIL

⊢ EVENTUAL a = ((λt. T) SUNTIL a)

WHEN_AS_SUNTIL

⊢ (a WHEN b) =
  (λt. ((λt. ¬b t) SUNTIL (λt. a t ∧ b t)) t ∨ ALWAYS (λt. ¬b t) t)

UNTIL_AS_SUNTIL

⊢ (a UNTIL b) = (λt. (a SUNTIL b) t ∨ ALWAYS a t)

BEFORE_AS_SUNTIL

⊢ (a BEFORE b) = (λt. ¬((λt. ¬a t) SUNTIL b) t)

SWHEN_AS_SUNTIL

⊢ (a SWHEN b) = ((λt. ¬b t) SUNTIL (λt. a t ∧ b t))

SBEFORE_AS_SUNTIL

⊢ (a SBEFORE b) = (λt0. ¬((λt. ¬a t) SUNTIL b) t0 ∧ EVENTUAL a t0)

ALWAYS_AS_SBEFORE

⊢ ALWAYS b = (λt0. ¬((λt. ¬b t) SBEFORE (λt. F)) t0)

EVENTUAL_AS_SBEFORE

⊢ EVENTUAL b = (b SBEFORE (λt. F))

WHEN_AS_SBEFORE

⊢ (a WHEN b) = (λt0. (b SBEFORE (λt. ¬a t ∧ b t)) t0 ∨ ALWAYS (λt. ¬b t) t0)

UNTIL_AS_SBEFORE

⊢ (a UNTIL b) = (λt0. ¬((λt. ¬a t) SBEFORE b) t0)

SWHEN_AS_SBEFORE

⊢ (a SWHEN b) = (b SBEFORE (λt. ¬a t ∧ b t))

SUNTIL_AS_SBEFORE

⊢ (a SUNTIL b) = (λt0. ¬((λt. ¬a t) SBEFORE b) t0 ∧ EVENTUAL b t0)

BEFORE_AS_SBEFORE

⊢ (a BEFORE b) = (λt0. (a SBEFORE b) t0 ∨ ALWAYS (λt. ¬b t) 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)

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)

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)

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

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)

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)

WHEN_EVENT

⊢ (a WHEN b) = ((λt. a t ∧ b t) WHEN b)

UNTIL_EVENT

⊢ (a UNTIL b) = ((λt. a t ∧ ¬b t) UNTIL b)

BEFORE_EVENT

⊢ (a BEFORE b) = ((λt. a t ∧ ¬b t) BEFORE b)

SWHEN_EVENT

⊢ (a SWHEN b) = ((λt. a t ∧ b t) SWHEN b)

SUNTIL_EVENT

⊢ (a SUNTIL b) = ((λt. a t ∧ ¬b t) SUNTIL b)

SBEFORE_EVENT

⊢ (a SBEFORE b) = ((λt. a t ∧ ¬b t) SBEFORE b)

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

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

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)

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)

NOT_NEXT

⊢ ∀P. NEXT (λt. ¬P t) = (λt. ¬NEXT P t)

AND_NEXT

⊢ ∀Q P. NEXT (λt. P t ∧ Q t) = (λt. NEXT P t ∧ NEXT Q t)

OR_NEXT

⊢ ∀Q P. NEXT (λt. P t ∨ Q t) = (λt. NEXT P t ∨ NEXT Q t)

IMP_NEXT

⊢ ∀Q P. NEXT (λt. P t ⇒ Q t) = (λt. NEXT P t ⇒ NEXT Q t)

EQUIV_NEXT

⊢ ∀Q P. NEXT (λt. P t ⇔ Q t) = (λt. NEXT P t ⇔ NEXT Q t)

ALWAYS_NEXT

⊢ ∀a. NEXT (ALWAYS a) = ALWAYS (NEXT a)

EVENTUAL_NEXT

⊢ ∀a. NEXT (EVENTUAL a) = EVENTUAL (NEXT a)

WHEN_NEXT

⊢ ∀a b. NEXT (a WHEN b) = (NEXT a WHEN NEXT b)

UNTIL_NEXT

⊢ ∀a b. NEXT (a UNTIL b) = (NEXT a UNTIL NEXT b)

BEFORE_NEXT

⊢ ∀a b. NEXT (a BEFORE b) = (NEXT a BEFORE NEXT b)

SWHEN_NEXT

⊢ ∀a b. NEXT (a SWHEN b) = (NEXT a SWHEN NEXT b)

SUNTIL_NEXT

⊢ ∀a b. NEXT (a SUNTIL b) = (NEXT a SUNTIL NEXT b)

SBEFORE_NEXT

⊢ ∀a b. NEXT (a SBEFORE b) = (NEXT a SBEFORE NEXT b)

ALWAYS_REC

⊢ ALWAYS P t0 ⇔ P t0 ∧ NEXT (ALWAYS P) t0

EVENTUAL_REC

⊢ EVENTUAL P t0 ⇔ P t0 ∨ NEXT (EVENTUAL P) t0

WATCH_REC

⊢ (q WATCH b) t0 ⇔
  ¬q t0 ∧ if b t0 then NEXT (ALWAYS q) t0 else NEXT (q WATCH b) t0

WHEN_REC

⊢ (a WHEN b) t0 ⇔ if b t0 then a t0 else NEXT (a WHEN b) t0

UNTIL_REC

⊢ (a UNTIL b) t0 ⇔ ¬b t0 ⇒ a t0 ∧ NEXT (a UNTIL b) t0

BEFORE_REC

⊢ (a BEFORE b) t0 ⇔ ¬b t0 ∧ (a t0 ∨ NEXT (a BEFORE b) t0)

SWHEN_REC

⊢ (a SWHEN b) t0 ⇔ if b t0 then a t0 else NEXT (a SWHEN b) t0

SUNTIL_REC

⊢ (a SUNTIL b) t0 ⇔ ¬b t0 ⇒ a t0 ∧ NEXT (a SUNTIL b) t0

SBEFORE_REC

⊢ (a SBEFORE b) t0 ⇔ ¬b t0 ∧ (a t0 ∨ NEXT (a SBEFORE b) t0)

ALWAYS_FIX

⊢ y = (λt. a t ∧ y (t + 1)) ⇔ y = ALWAYS a ∨ y = (λt. F)

EVENTUAL_FIX

⊢ y = (λt. a t ∨ y (t + 1)) ⇔ y = EVENTUAL a ∨ y = (λt. T)

WHEN_FIX

⊢ y = (λt. if b t then a t else y (t + 1)) ⇔ y = (a WHEN b) ∨ y = (a SWHEN b)

UNTIL_FIX

⊢ y = (λt. ¬b t ⇒ a t ∧ y (t + 1)) ⇔ y = (a UNTIL b) ∨ y = (a SUNTIL b)

BEFORE_FIX

⊢ ∀y.
      y = (λt. ¬b t ∧ (a t ∨ y (t + 1))) ⇔
      y = (a BEFORE b) ∨ y = (a SBEFORE b)

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)

UNTIL_INVARIANT

⊢ ∀t0.
      (a UNTIL b) t0 ⇔
      ∃J. J t0 ∧ ∀t. J (t + t0) ∧ ¬b (t + t0) ⇒ a (t + t0) ∧ J (SUC (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)

ALWAYS_INVARIANT

⊢ ALWAYS a t0 ⇔ ∃J. J t0 ∧ ∀t. J (t + t0) ⇒ a (t + t0) ∧ J (t + (t0 + 1))

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)

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)

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)

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)

ALWAYS_IDEM

⊢ ALWAYS a = ALWAYS (ALWAYS a)

EVENTUAL_IDEM

⊢ EVENTUAL a = EVENTUAL (EVENTUAL a)

WHEN_IDEM

⊢ (a WHEN b) = ((a WHEN b) WHEN b)

UNTIL_IDEM

⊢ (a UNTIL b) = ((a UNTIL b) UNTIL b)

BEFORE_IDEM

⊢ (a BEFORE b) = ((a BEFORE b) BEFORE b)

SWHEN_IDEM

⊢ (a SWHEN b) = ((a SWHEN b) SWHEN b)

SUNTIL_IDEM

⊢ (a SUNTIL b) = ((a SUNTIL b) SUNTIL b)

SBEFORE_IDEM

⊢ (a SBEFORE b) = ((a SBEFORE b) SBEFORE b)

NOT_ALWAYS

⊢ ¬ALWAYS a t0 ⇔ EVENTUAL (λt. ¬a t) t0

NOT_EVENTUAL

⊢ ¬EVENTUAL a t0 ⇔ ALWAYS (λt. ¬a t) t0

NOT_WHEN

⊢ ¬(a WHEN b) t0 ⇔ ((λt. ¬a t) SWHEN b) t0

NOT_UNTIL

⊢ ¬(a UNTIL b) t0 ⇔ ((λt. ¬a t) SBEFORE b) t0

NOT_BEFORE

⊢ ¬(a BEFORE b) t0 ⇔ ((λt. ¬a t) SUNTIL b) t0

NOT_SWHEN

⊢ ¬(a SWHEN b) t0 ⇔ ((λt. ¬a t) WHEN b) t0

NOT_SUNTIL

⊢ ¬(a SUNTIL b) t0 ⇔ ((λt. ¬a t) BEFORE b) t0

NOT_SBEFORE

⊢ ¬(a SBEFORE b) t0 ⇔ ((λt. ¬a t) UNTIL b) t0