- 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