- DET_OMEGA_EXISTS_FORALL_THEOREM
-
⊢ (∃q.
q t0 = InitVal ∧
(∀t. q (t + (t0 + 1)) = TransRel (i (t + t0),q (t + t0))) ∧
Accept (i,(λt. q (t + t0)))) ⇔
∀q.
q t0 = InitVal ∧
(∀t. q (t + (t0 + 1)) = TransRel (i (t + t0),q (t + t0))) ⇒
Accept (i,(λt. q (t + t0)))
- NEG_DET_AUTOMATA
-
⊢ ¬(∃q.
q t0 = InitVal ∧
(∀t. q (t + (t0 + 1)) = TransRel (i (t + t0),q (t + t0))) ∧
Accept (i,(λt. q (t + t0)))) ⇔
∃q.
q t0 = InitVal ∧
(∀t. q (t + (t0 + 1)) = TransRel (i (t + t0),q (t + t0))) ∧
¬Accept (i,(λt. q (t + t0)))
- OMEGA_CONJ_CLOSURE
-
⊢ (∃q1. Phi_I1 (q1 t0) ∧ (∀t. Phi_R1 (i (t + t0),q1 (t + t0))) ∧ Psi1 (i,q1)) ∧
(∃q2. Phi_I2 (q2 t0) ∧ (∀t. Phi_R2 (i (t + t0),q2 (t + t0))) ∧ Psi2 (i,q2)) ⇔
∃q1 q2.
(Phi_I1 (q1 t0) ∧ Phi_I2 (q2 t0)) ∧
(∀t. Phi_R1 (i (t + t0),q1 (t + t0)) ∧ Phi_R2 (i (t + t0),q2 (t + t0))) ∧
Psi1 (i,q1) ∧ Psi2 (i,q2)
- OMEGA_DISJ_CLOSURE
-
⊢ (∃q1. Phi_I1 (q1 t0) ∧ (∀t. Phi_R1 (i (t + t0),q1 (t + t0))) ∧ Psi1 (i,q1)) ∨
(∃q2. Phi_I2 (q2 t0) ∧ (∀t. Phi_R2 (i (t + t0),q2 (t + t0))) ∧ Psi2 (i,q2)) ⇔
∃p q1 q2.
(¬p t0 ∧ Phi_I1 (q1 t0) ∨ p t0 ∧ Phi_I2 (q2 t0)) ∧
(∀t.
¬p (t + t0) ∧ Phi_R1 (i (t + t0),q1 (t + t0)) ∧ ¬p (t + (t0 + 1)) ∨
p (t + t0) ∧ Phi_R2 (i (t + t0),q2 (t + t0)) ∧ p (t + (t0 + 1))) ∧
(¬p t0 ∧ Psi1 (i,q1) ∨ p t0 ∧ Psi2 (i,q2))
- BOOLEAN_CLOSURE_G
-
⊢ (¬(∀t. a (t + t0)) ⇔ ∃t. ¬a (t + t0)) ∧
((∀t. a (t + t0)) ∧ (∀t. b (t + t0)) ⇔ ∀t. a (t + t0) ∧ b (t + t0)) ∧
((∀t. a (t + t0)) ∨ (∀t. b (t + t0)) ⇔
∃p q.
(¬p t0 ∧ ¬q t0) ∧
(∀t.
(p (t + (t0 + 1)) ⇔ p (t + t0) ∨ ¬a (t + t0)) ∧
(q (t + (t0 + 1)) ⇔ q (t + t0) ∨ ¬b (t + t0))) ∧
∀t. ¬p (t + t0) ∨ ¬q (t + t0))
- BOOLEAN_CLOSURE_F
-
⊢ (¬(∃t. a (t + t0)) ⇔ ∀t. ¬a (t + t0)) ∧
((∃t. a (t + t0)) ∨ (∃t. b (t + t0)) ⇔ ∃t. a (t + t0) ∨ b (t + t0)) ∧
((∃t. a (t + t0)) ∧ (∃t. b (t + t0)) ⇔
∃p q.
(¬p t0 ∧ ¬q t0) ∧
(∀t.
(p (t + (t0 + 1)) ⇔ p (t + t0) ∨ a (t + t0)) ∧
(q (t + (t0 + 1)) ⇔ q (t + t0) ∨ b (t + t0))) ∧
∃t. p (t + t0) ∧ q (t + t0))
- BOOLEAN_CLOSURE_FG
-
⊢ (¬(∃t1. ∀t2. a (t1 + (t2 + t0))) ⇔ ∀t1. ∃t2. ¬a (t1 + (t2 + t0))) ∧
((∃t1. ∀t2. a (t1 + (t2 + t0))) ∧ (∃t1. ∀t2. b (t1 + (t2 + t0))) ⇔
∃t1. ∀t2. a (t1 + (t2 + t0)) ∧ b (t1 + (t2 + t0))) ∧
((∃t1. ∀t2. a (t1 + (t2 + t0))) ∨ (∃t1. ∀t2. b (t1 + (t2 + t0))) ⇔
∃q.
¬q t0 ∧
(∀t. q (t + (t0 + 1)) ⇔ if q (t + t0) then b (t + t0) else ¬a (t + t0)) ∧
∃t1. ∀t2. ¬q (t1 + (t2 + t0)) ∨ b (t1 + (t2 + t0)))
- BOOLEAN_CLOSURE_GF
-
⊢ (¬(∀t1. ∃t2. a (t1 + (t2 + t0))) ⇔ ∃t1. ∀t2. ¬a (t1 + (t2 + t0))) ∧
((∀t1. ∃t2. a (t1 + (t2 + t0))) ∨ (∀t1. ∃t2. b (t1 + (t2 + t0))) ⇔
∀t1. ∃t2. a (t1 + (t2 + t0)) ∨ b (t1 + (t2 + t0))) ∧
((∀t1. ∃t2. a (t1 + (t2 + t0))) ∧ (∀t1. ∃t2. b (t1 + (t2 + t0))) ⇔
∃q.
¬q t0 ∧
(∀t. q (t + (t0 + 1)) ⇔ if q (t + t0) then ¬b (t + t0) else a (t + t0)) ∧
∀t1. ∃t2. q (t1 + (t2 + t0)) ∧ b (t1 + (t2 + t0)))
- BOREL_HIERARCHY_G
-
⊢ ((∀t. a (t + t0)) ⇔
∃q.
q t0 ∧ (∀t. q (t + t0) ∧ a (t + t0) ∧ q (SUC (t + t0))) ∧
∃t. q (t + t0)) ∧
((∀t. a (t + t0)) ⇔
∃q.
q t0 ∧ (∀t. q (SUC (t + t0)) ⇔ q (t + t0) ∧ a (t + t0)) ∧
∃t1. ∀t2. q (t1 + (t2 + t0))) ∧
((∀t. a (t + t0)) ⇔
∃q.
q t0 ∧ (∀t. q (SUC (t + t0)) ⇔ q (t + t0) ∧ a (t + t0)) ∧
∀t1. ∃t2. q (t1 + (t2 + t0)))
- BOREL_HIERARCHY_F
-
⊢ ((∃t. a (t + t0)) ⇔
∃q.
¬q t0 ∧ (∀t. q (SUC (t + t0)) ⇔ q (t + t0) ∨ a (t + t0)) ∧
∃t1. ∀t2. q (t1 + (t2 + t0))) ∧
((∃t. a (t + t0)) ⇔
∃q.
¬q t0 ∧ (∀t. q (SUC (t + t0)) ⇔ q (t + t0) ∨ a (t + t0)) ∧
∀t1. ∃t2. q (t1 + (t2 + t0)))
- BOREL_HIERARCHY_FG
-
⊢ ((∃t1. ∀t2. a (t1 + (t2 + t0))) ⇔
∃q.
¬q t0 ∧ (∀t. q (t + t0) ⇒ a (t + t0) ∧ q (SUC (t + t0))) ∧
∃t. q (t + t0)) ∧
((∃t1. ∀t2. a (t1 + (t2 + t0))) ⇔
∃p q.
(¬p t0 ∧ ¬q t0) ∧
(∀t.
(p (t + t0) ⇒ p (SUC (t + t0))) ∧
(p (SUC (t + t0)) ⇒ p (t + t0) ∨ ¬q (t + t0)) ∧
(q (SUC (t + t0)) ⇔
p (t + t0) ∧ ¬q (t + t0) ∧ ¬a (t + t0) ∨ p (t + t0) ∧ q (t + t0))) ∧
∀t1. ∃t2. p (t1 + (t2 + t0)) ∧ ¬q (t1 + (t2 + t0)))
- TEMP_OPS_DEFS_TO_OMEGA
-
⊢ (l = NEXT a ⇔ T ∧ (∀t. l t ⇔ a (SUC t)) ∧ T) ∧
(l = ALWAYS a ⇔
T ∧ (∀t. l t ⇔ a t ∧ l (SUC t)) ∧ ∀t1. ∃t2. a (t1 + t2) ⇒ l (t1 + t2)) ∧
(l = EVENTUAL a ⇔
T ∧ (∀t. l t ⇔ a t ∨ l (SUC t)) ∧ ∀t1. ∃t2. l (t1 + t2) ⇒ a (t1 + t2)) ∧
(l = (a SUNTIL b) ⇔
T ∧ (∀t. l t ⇔ ¬b t ⇒ a t ∧ l (SUC t)) ∧
∀t1. ∃t2. l (t1 + t2) ⇒ ¬a (t1 + t2) ∨ b (t1 + t2)) ∧
(l = (a SWHEN b) ⇔
T ∧ (∀t. l t ⇔ if b t then a t else l (SUC t)) ∧
∀t1. ∃t2. l (t1 + t2) ⇒ b (t1 + t2)) ∧
(l = (a SBEFORE b) ⇔
T ∧ (∀t. l t ⇔ ¬b t ∧ (a t ∨ l (SUC t))) ∧
∀t1. ∃t2. l (t1 + t2) ⇒ a (t1 + t2) ∨ b (t1 + t2)) ∧
(l = (a UNTIL b) ⇔
T ∧ (∀t. l t ⇔ ¬b t ⇒ a t ∧ l (SUC t)) ∧
∀t1. ∃t2. ¬l (t1 + t2) ⇒ ¬a (t1 + t2) ∨ b (t1 + t2)) ∧
(l = (a WHEN b) ⇔
T ∧ (∀t. l t ⇔ if b t then a t else l (SUC t)) ∧
∀t1. ∃t2. l (t1 + t2) ∨ b (t1 + t2)) ∧
(l = (a BEFORE b) ⇔
T ∧ (∀t. l t ⇔ ¬b t ∧ (a t ∨ l (SUC t))) ∧
∀t1. ∃t2. ¬l (t1 + t2) ⇒ a (t1 + t2) ∨ b (t1 + t2)) ∧
(l = PREV a ⇔ (l 0 ⇔ T) ∧ (∀t. l (SUC t) ⇔ a t) ∧ T) ∧
(l = PSNEXT a ⇔ (l 0 ⇔ F) ∧ (∀t. l (SUC t) ⇔ a t) ∧ T) ∧
(l = PREV (PALWAYS a) ⇔ (l 0 ⇔ T) ∧ (∀t. l (SUC t) ⇔ a t ∧ l t) ∧ T) ∧
(l = PSNEXT (ONCE a) ⇔ (l 0 ⇔ F) ∧ (∀t. l (SUC t) ⇔ a t ∨ l t) ∧ T) ∧
(l = PSNEXT (a PSUNTIL b) ⇔
(l 0 ⇔ F) ∧ (∀t. l (SUC t) ⇔ b t ∨ a t ∧ l t) ∧ T) ∧
(l = PSNEXT (a PSWHEN b) ⇔
(l 0 ⇔ F) ∧ (∀t. l (SUC t) ⇔ a t ∧ b t ∨ ¬b t ∧ l t) ∧ T) ∧
(l = PSNEXT (a PSBEFORE b) ⇔
(l 0 ⇔ F) ∧ (∀t. l (SUC t) ⇔ ¬b t ∧ (a t ∨ l t)) ∧ T) ∧
(l = PREV (a SINCE b) ⇔ (l 0 ⇔ T) ∧ (∀t. l (SUC t) ⇔ b t ∨ a t ∧ l t) ∧ T) ∧
(l = PREV (a PWHEN b) ⇔
(l 0 ⇔ T) ∧ (∀t. l (SUC t) ⇔ a t ∧ b t ∨ ¬b t ∧ l t) ∧ T) ∧
(l = PREV (a PBEFORE b) ⇔
(l 0 ⇔ T) ∧ (∀t. l (SUC t) ⇔ ¬b t ∧ (a t ∨ l t)) ∧ T)
- AUTOMATON_TEMP_CLOSURE
-
⊢ ((∃q1.
Phi_I1 q1 ∧ Phi_R1 q1 ∧
∃q2. Phi_I2 q2 ∧ Phi_R2 (q2,q1) ∧ Phi_F (q1,q2)) ⇔
∃q1 q2.
(Phi_I1 q1 ∧ Phi_I2 q2) ∧ (Phi_R1 q1 ∧ Phi_R2 (q2,q1)) ∧ Phi_F (q1,q2)) ∧
(Phi (NEXT phi) ⇔
∃q0 q1. T ∧ (∀t. (q0 t ⇔ phi t) ∧ (q1 t ⇔ q0 (t + 1))) ∧ Phi q1) ∧
(Phi (PREV phi) ⇔ ∃q. q 0 ∧ (∀t. q (t + 1) ⇔ phi t) ∧ Phi q) ∧
(Phi (PSNEXT phi) ⇔ ∃q. ¬q 0 ∧ (∀t. q (t + 1) ⇔ phi t) ∧ Phi q) ∧
(Phi (PREV (PALWAYS a)) ⇔ ∃q. q 0 ∧ (∀t. q (t + 1) ⇔ a t ∧ q t) ∧ Phi q) ∧
(Phi (PSNEXT (ONCE a)) ⇔ ∃q. ¬q 0 ∧ (∀t. q (t + 1) ⇔ a t ∨ q t) ∧ Phi q) ∧
(Phi (PSNEXT (a PSUNTIL b)) ⇔
∃q. ¬q 0 ∧ (∀t. q (t + 1) ⇔ b t ∨ a t ∧ q t) ∧ Phi q) ∧
(Phi (PSNEXT (a PSWHEN b)) ⇔
∃q. ¬q 0 ∧ (∀t. q (t + 1) ⇔ a t ∧ b t ∨ ¬b t ∧ q t) ∧ Phi q) ∧
(Phi (PSNEXT (a PSBEFORE b)) ⇔
∃q. ¬q 0 ∧ (∀t. q (t + 1) ⇔ ¬b t ∧ (a t ∨ q t)) ∧ Phi q) ∧
(Phi (PREV (a SINCE b)) ⇔
∃q. q 0 ∧ (∀t. q (t + 1) ⇔ b t ∨ a t ∧ q t) ∧ Phi q) ∧
(Phi (PREV (a PWHEN b)) ⇔
∃q. q 0 ∧ (∀t. q (t + 1) ⇔ a t ∧ b t ∨ ¬b t ∧ q t) ∧ Phi q) ∧
(Phi (PREV (a PBEFORE b)) ⇔
∃q. q 0 ∧ (∀t. q (t + 1) ⇔ ¬b t ∧ (a t ∨ q t)) ∧ Phi q)
- BUECHI_TRANSLATION
-
⊢ (Phi (NEXT phi) ⇔
∃q0 q1. T ∧ (∀t. (q0 t ⇔ phi t) ∧ (q1 t ⇔ q0 (t + 1))) ∧ Phi q1) ∧
(Phi (ALWAYS a) ⇔
∃q.
T ∧ (∀t. q t ⇔ a t ∧ q (t + 1)) ∧
(∀t1. ∃t2. a (t1 + t2) ⇒ q (t1 + t2)) ∧ Phi q) ∧
(Phi (EVENTUAL a) ⇔
∃q.
T ∧ (∀t. q t ⇔ a t ∨ q (t + 1)) ∧
(∀t1. ∃t2. q (t1 + t2) ⇒ a (t1 + t2)) ∧ Phi q) ∧
(Phi (a SUNTIL b) ⇔
∃q.
T ∧ (∀t. q t ⇔ b t ∨ a t ∧ q (t + 1)) ∧
(∀t1. ∃t2. q (t1 + t2) ⇒ ¬a (t1 + t2) ∨ b (t1 + t2)) ∧ Phi q) ∧
(Phi (a UNTIL b) ⇔
∃q.
T ∧ (∀t. q t ⇔ b t ∨ a t ∧ q (t + 1)) ∧
(∀t1. ∃t2. ¬q (t1 + t2) ⇒ ¬a (t1 + t2) ∨ b (t1 + t2)) ∧ Phi q) ∧
(Phi (a SWHEN b) ⇔
∃q.
T ∧ (∀t. q t ⇔ if b t then a t else q (t + 1)) ∧
(∀t1. ∃t2. q (t1 + t2) ⇒ b (t1 + t2)) ∧ Phi q) ∧
(Phi (a WHEN b) ⇔
∃q.
T ∧ (∀t. q t ⇔ if b t then a t else q (t + 1)) ∧
(∀t1. ∃t2. q (t1 + t2) ∨ b (t1 + t2)) ∧ Phi q) ∧
(Phi (a SBEFORE b) ⇔
∃q.
T ∧ (∀t. q t ⇔ ¬b t ∧ (a t ∨ q (t + 1))) ∧
(∀t1. ∃t2. q (t1 + t2) ⇒ a (t1 + t2) ∨ b (t1 + t2)) ∧ Phi q) ∧
(Phi (a BEFORE b) ⇔
∃q.
T ∧ (∀t. q t ⇔ ¬b t ∧ (a t ∨ q (t + 1))) ∧
(∀t1. ∃t2. ¬q (t1 + t2) ⇒ a (t1 + t2) ∨ b (t1 + t2)) ∧ Phi q)
- CO_BUECHI_CONJ_CLOSURE
-
⊢ (∃q1.
Phi_I1 (q1 t0) ∧ (∀t. Phi_R1 (i (t + t0),q1 (t + t0))) ∧
∃t1. ∀t2. Psi1 (i (t1 + (t2 + t0)),q1 (t1 + (t2 + t0)))) ∧
(∃q2.
Phi_I2 (q2 t0) ∧ (∀t. Phi_R2 (i (t + t0),q2 (t + t0))) ∧
∃t1. ∀t2. Psi2 (i (t1 + (t2 + t0)),q2 (t1 + (t2 + t0)))) ⇔
∃q1 q2.
(Phi_I1 (q1 t0) ∧ Phi_I2 (q2 t0)) ∧
(∀t. Phi_R1 (i (t + t0),q1 (t + t0)) ∧ Phi_R2 (i (t + t0),q2 (t + t0))) ∧
∃t1.
∀t2.
Psi1 (i (t1 + (t2 + t0)),q1 (t1 + (t2 + t0))) ∧
Psi2 (i (t1 + (t2 + t0)),q2 (t1 + (t2 + t0)))
- CO_BUECHI_DISJ_CLOSURE
-
⊢ (∃q1.
Phi_I1 (q1 t0) ∧ (∀t. Phi_R1 (i (t + t0),q1 (t + t0))) ∧
∃t1. ∀t2. Psi1 (i (t1 + (t2 + t0)),q1 (t1 + (t2 + t0)))) ∨
(∃q2.
Phi_I2 (q2 t0) ∧ (∀t. Phi_R2 (i (t + t0),q2 (t + t0))) ∧
∃t1. ∀t2. Psi2 (i (t1 + (t2 + t0)),q2 (t1 + (t2 + t0)))) ⇔
∃p q1 q2.
(¬p t0 ∧ Phi_I1 (q1 t0) ∨ p t0 ∧ Phi_I2 (q2 t0)) ∧
(∀t.
¬p (t + t0) ∧ Phi_R1 (i (t + t0),q1 (t + t0)) ∧ ¬p (t + (t0 + 1)) ∨
p (t + t0) ∧ Phi_R2 (i (t + t0),q2 (t + t0)) ∧ p (t + (t0 + 1))) ∧
∃t1.
∀t2.
¬p (t + t0) ∧ Psi1 (i (t1 + (t2 + t0)),q1 (t1 + (t2 + t0))) ∨
p (t + t0) ∧ Psi2 (i (t1 + (t2 + t0)),q2 (t1 + (t2 + t0)))
- CO_BUECHI_NEXT_CLOSURE
-
⊢ NEXT
(λt0.
∃q.
Phi_I (q t0) ∧ (∀t. Phi_R (i (t + t0),q (t + t0))) ∧
∃t1. ∀t2. Psi (i (t1 + (t2 + t0)),q (t1 + (t2 + t0)))) t0 ⇔
∃p q.
((p t0 ⇔ F) ∧ q t0 = c) ∧
(∀t.
¬p (t + t0) ∧ q (t + t0) = c ∧ p (t + (t0 + 1)) ∧
Phi_I (q (t + (t0 + 1))) ∨
p (t + t0) ∧ Phi_R (i (t + t0),q (t + t0)) ∧ p (t + (t0 + 1))) ∧
∃t1. ∀t2. Psi (i (t1 + (t2 + t0)),q (t1 + (t2 + t0)))
- CO_BUECHI_SUNTIL_CLOSURE
-
⊢ (phi SUNTIL
(λt0.
∃q.
Phi_I (q t0) ∧ (∀t. Phi_R (i (t + t0),q (t + t0))) ∧
∃t1. ∀t2. Psi (i (t1 + (t2 + t0)),q (t1 + (t2 + t0))))) t0 ⇔
∃p q.
(if p t0 then Phi_I (q t0) else q t0 = c) ∧
(∀t.
¬p (t + t0) ∧ q (t + t0) = c ∧ phi (t + t0) ∧ ¬p (t + (t0 + 1)) ∧
q (t + (t0 + 1)) = c ∨
¬p (t + t0) ∧ q (t + t0) = c ∧ phi (t + t0) ∧ p (t + (t0 + 1)) ∧
Phi_I (q (t + (t0 + 1))) ∨
p (t + t0) ∧ Phi_R (i (t + t0),q (t + t0)) ∧ p (t + (t0 + 1))) ∧
∃t1.
∀t2.
p (t1 + (t2 + t0)) ∧ Psi (i (t1 + (t2 + t0)),q (t1 + (t2 + t0)))
- CO_BUECHI_UNTIL_CLOSURE
-
⊢ (phi UNTIL
(λt0.
∃q.
Phi_I (q t0) ∧ (∀t. Phi_R (i (t + t0),q (t + t0))) ∧
∃t1. ∀t2. Psi (i (t1 + (t2 + t0)),q (t1 + (t2 + t0))))) t0 ⇔
∃p q.
(if p t0 then Phi_I (q t0) else q t0 = c) ∧
(∀t.
¬p (t + t0) ∧ q (t + t0) = c ∧ phi (t + t0) ∧ ¬p (t + (t0 + 1)) ∧
q (t + (t0 + 1)) = c ∨
¬p (t + t0) ∧ q (t + t0) = c ∧ phi (t + t0) ∧ p (t + (t0 + 1)) ∧
Phi_I (q (t + (t0 + 1))) ∨
p (t + t0) ∧ Phi_R (i (t + t0),q (t + t0)) ∧ p (t + (t0 + 1))) ∧
∃t1.
∀t2.
¬p (t1 + (t2 + t0)) ∨
Psi (i (t1 + (t2 + t0)),q (t1 + (t2 + t0)))
- CO_BUECHI_SBEFORE_CLOSURE
-
⊢ ((λt0.
∃q.
Phi_I (q t0) ∧ (∀t. Phi_R (i (t + t0),q (t + t0))) ∧
∃t1. ∀t2. Psi (i (t1 + (t2 + t0)),q (t1 + (t2 + t0)))) SBEFORE phi)
t0 ⇔
∃p1 p2 q.
(¬p1 t0 ∧ ¬p2 t0 ∧ q t0 = c ∨ p1 t0 ∧ ¬p2 t0 ∧ Phi_I (q t0)) ∧
(∀t.
¬p1 (t + t0) ∧ ¬p2 (t + t0) ∧ q (t + t0) = c ∧ ¬phi (t + t0) ∧
¬p1 (t + (t0 + 1)) ∧ ¬p2 (t + (t0 + 1)) ∧ q (t + (t0 + 1)) = c ∨
¬p1 (t + t0) ∧ ¬p2 (t + t0) ∧ q (t + t0) = c ∧ ¬phi (t + t0) ∧
p1 (t + (t0 + 1)) ∧ ¬p2 (t + (t0 + 1)) ∧ Phi_I (q (t + (t0 + 1))) ∨
p1 (t + t0) ∧ ¬p2 (t + t0) ∧ ¬phi (t + t0) ∧ Phi_I (q (t + t0)) ∧
Phi_R (i (t + t0),q (t + t0)) ∧ p1 (t + (t0 + 1)) ∧
p2 (t + (t0 + 1)) ∨
p1 (t + t0) ∧ p2 (t + t0) ∧ Phi_R (i (t + t0),q (t + t0)) ∧
p1 (t + (t0 + 1)) ∧ p2 (t + (t0 + 1))) ∧
∃t1.
∀t2.
p1 (t1 + (t2 + t0)) ∧
Psi (i (t1 + (t2 + t0)),q (t1 + (t2 + t0)))
- CO_BUECHI_BEFORE_CLOSURE
-
⊢ ((λt0.
∃q.
Phi_I (q t0) ∧ (∀t. Phi_R (i (t + t0),q (t + t0))) ∧
∃t1. ∀t2. Psi (i (t1 + (t2 + t0)),q (t1 + (t2 + t0)))) BEFORE phi)
t0 ⇔
∃p1 p2 q.
(¬p1 t0 ∧ ¬p2 t0 ∧ q t0 = c ∨ p1 t0 ∧ ¬p2 t0 ∧ Phi_I (q t0)) ∧
(∀t.
¬p1 (t + t0) ∧ ¬p2 (t + t0) ∧ q (t + t0) = c ∧ ¬phi (t + t0) ∧
¬p1 (t + (t0 + 1)) ∧ ¬p2 (t + (t0 + 1)) ∧ q (t + (t0 + 1)) = c ∨
¬p1 (t + t0) ∧ ¬p2 (t + t0) ∧ q (t + t0) = c ∧ ¬phi (t + t0) ∧
p1 (t + (t0 + 1)) ∧ ¬p2 (t + (t0 + 1)) ∧ Phi_I (q (t + (t0 + 1))) ∨
p1 (t + t0) ∧ ¬p2 (t + t0) ∧ ¬phi (t + t0) ∧ Phi_I (q (t + t0)) ∧
Phi_R (i (t + t0),q (t + t0)) ∧ p1 (t + (t0 + 1)) ∧
p2 (t + (t0 + 1)) ∨
p1 (t + t0) ∧ p2 (t + t0) ∧ Phi_R (i (t + t0),q (t + t0)) ∧
p1 (t + (t0 + 1)) ∧ p2 (t + (t0 + 1))) ∧
∃t1.
∀t2.
¬p1 (t1 + (t2 + t0)) ∨
Psi (i (t1 + (t2 + t0)),q (t1 + (t2 + t0)))
- CO_BUECHI_SWHEN_CLOSURE
-
⊢ ((λt0.
∃q.
Phi_I (q t0) ∧ (∀t. Phi_R (i (t + t0),q (t + t0))) ∧
∃t1. ∀t2. Psi (i (t1 + (t2 + t0)),q (t1 + (t2 + t0)))) SWHEN phi)
t0 ⇔
∃p1 p2 q.
(¬p1 t0 ∧ ¬p2 t0 ∧ q t0 = c ∨ p1 t0 ∧ ¬p2 t0 ∧ Phi_I (q t0)) ∧
(∀t.
¬p1 (t + t0) ∧ ¬p2 (t + t0) ∧ q (t + t0) = c ∧ ¬phi (t + t0) ∧
¬p1 (t + (t0 + 1)) ∧ ¬p2 (t + (t0 + 1)) ∧ q (t + (t0 + 1)) = c ∨
¬p1 (t + t0) ∧ ¬p2 (t + t0) ∧ q (t + t0) = c ∧ ¬phi (t + t0) ∧
p1 (t + (t0 + 1)) ∧ ¬p2 (t + (t0 + 1)) ∧ Phi_I (q (t + (t0 + 1))) ∨
p1 (t + t0) ∧ ¬p2 (t + t0) ∧ phi (t + t0) ∧ Phi_I (q (t + t0)) ∧
Phi_R (i (t + t0),q (t + t0)) ∧ p1 (t + (t0 + 1)) ∧
p2 (t + (t0 + 1)) ∨
p1 (t + t0) ∧ p2 (t + t0) ∧ Phi_R (i (t + t0),q (t + t0)) ∧
p1 (t + (t0 + 1)) ∧ p2 (t + (t0 + 1))) ∧
∃t1.
∀t2.
p1 (t1 + (t2 + t0)) ∧
Psi (i (t1 + (t2 + t0)),q (t1 + (t2 + t0)))
- CO_BUECHI_WHEN_CLOSURE
-
⊢ ((λt0.
∃q.
Phi_I (q t0) ∧ (∀t. Phi_R (i (t + t0),q (t + t0))) ∧
∃t1. ∀t2. Psi (i (t1 + (t2 + t0)),q (t1 + (t2 + t0)))) WHEN phi)
t0 ⇔
∃p1 p2 q.
(¬p1 t0 ∧ ¬p2 t0 ∧ q t0 = c ∨ p1 t0 ∧ ¬p2 t0 ∧ Phi_I (q t0)) ∧
(∀t.
¬p1 (t + t0) ∧ ¬p2 (t + t0) ∧ q (t + t0) = c ∧ ¬phi (t + t0) ∧
¬p1 (t + (t0 + 1)) ∧ ¬p2 (t + (t0 + 1)) ∧ q (t + (t0 + 1)) = c ∨
¬p1 (t + t0) ∧ ¬p2 (t + t0) ∧ q (t + t0) = c ∧ ¬phi (t + t0) ∧
p1 (t + (t0 + 1)) ∧ ¬p2 (t + (t0 + 1)) ∧ Phi_I (q (t + (t0 + 1))) ∨
p1 (t + t0) ∧ ¬p2 (t + t0) ∧ phi (t + t0) ∧ Phi_I (q (t + t0)) ∧
Phi_R (i (t + t0),q (t + t0)) ∧ p1 (t + (t0 + 1)) ∧
p2 (t + (t0 + 1)) ∨
p1 (t + t0) ∧ p2 (t + t0) ∧ Phi_R (i (t + t0),q (t + t0)) ∧
p1 (t + (t0 + 1)) ∧ p2 (t + (t0 + 1))) ∧
∃t1.
∀t2.
¬p1 (t1 + (t2 + t0)) ∨
Psi (i (t1 + (t2 + t0)),q (t1 + (t2 + t0)))
- NEXT_AS_CO_BUECHI
-
⊢ NEXT a t0 ⇔
∃p q.
(¬p t0 ∧ ¬q t0) ∧
(∀t.
¬p (t + t0) ∧ ¬q (t + t0) ∧ p (t + (1 + t0)) ∧ ¬q (t + (1 + t0)) ∨
p (t + t0) ∧ ¬q (t + t0) ∧ a (t + t0) ∧ p (t + (1 + t0)) ∧
q (t + (1 + t0)) ∨
p (t + t0) ∧ q (t + t0) ∧ p (t + (1 + t0)) ∧ q (t + (1 + t0))) ∧
∃t1. ∀t2. q (t1 + (t2 + t0))
- SUNTIL_AS_CO_BUECHI
-
⊢ (a SUNTIL b) t0 ⇔
∃q.
¬q t0 ∧
(∀t.
¬q (t + t0) ∧ a (t + t0) ∧ ¬b (t + t0) ∧ ¬q (t + (1 + t0)) ∨
¬q (t + t0) ∧ b (t + t0) ∧ q (t + (1 + t0)) ∨
q (t + t0) ∧ q (t + (1 + t0))) ∧ ∃t1. ∀t2. q (t1 + (t2 + t0))
- UNTIL_AS_CO_BUECHI
-
⊢ (a UNTIL b) t0 ⇔
∃q.
¬q t0 ∧
(∀t.
¬q (t + t0) ∧ a (t + t0) ∧ ¬b (t + t0) ∧ ¬q (t + (1 + t0)) ∨
¬q (t + t0) ∧ b (t + t0) ∧ q (t + (1 + t0)) ∨
q (t + t0) ∧ q (t + (1 + t0))) ∧
∃t1. ∀t2. ¬q (t1 + (t2 + t0)) ∨ q (t1 + (t2 + t0))
- SBEFORE_AS_CO_BUECHI
-
⊢ (a SBEFORE b) t0 ⇔
∃q.
¬q t0 ∧
(∀t.
¬q (t + t0) ∧ ¬a (t + t0) ∧ ¬b (t + t0) ∧ ¬q (t + (1 + t0)) ∨
¬q (t + t0) ∧ a (t + t0) ∧ ¬b (t + t0) ∧ q (t + (1 + t0)) ∨
q (t + t0) ∧ q (t + (1 + t0))) ∧ ∃t1. ∀t2. q (t1 + (t2 + t0))
- BEFORE_AS_CO_BUECHI
-
⊢ (a BEFORE b) t0 ⇔
∃q.
¬q t0 ∧
(∀t.
¬q (t + t0) ∧ ¬a (t + t0) ∧ ¬b (t + t0) ∧ ¬q (t + (1 + t0)) ∨
¬q (t + t0) ∧ a (t + t0) ∧ ¬b (t + t0) ∧ q (t + (1 + t0)) ∨
q (t + t0) ∧ q (t + (1 + t0))) ∧
∃t1. ∀t2. ¬q (t1 + (t2 + t0)) ∨ q (t1 + (t2 + t0))
- SWHEN_AS_CO_BUECHI
-
⊢ (a SWHEN b) t0 ⇔
∃q.
¬q t0 ∧
(∀t.
¬q (t + t0) ∧ ¬b (t + t0) ∧ ¬q (t + (1 + t0)) ∨
¬q (t + t0) ∧ a (t + t0) ∧ b (t + t0) ∧ q (t + (1 + t0)) ∨
q (t + t0) ∧ q (t + (1 + t0))) ∧ ∃t1. ∀t2. q (t1 + (t2 + t0))
- WHEN_AS_CO_BUECHI
-
⊢ (a WHEN b) t0 ⇔
∃q.
¬q t0 ∧
(∀t.
¬q (t + t0) ∧ ¬b (t + t0) ∧ ¬q (t + (1 + t0)) ∨
¬q (t + t0) ∧ a (t + t0) ∧ b (t + t0) ∧ q (t + (1 + t0)) ∨
q (t + t0) ∧ q (t + (1 + t0))) ∧
∃t1. ∀t2. ¬q (t1 + (t2 + t0)) ∨ q (t1 + (t2 + t0))
- BUECHI_PERIODIC_MODEL
-
⊢ (∀s. ∃x0 l. 0 < l ∧ s x0 = s (x0 + l)) ⇒
((∃i q.
InitState (q 0) ∧ (∀t. TransRel (i t,q t,q (t + 1))) ∧
∀t1. ∃t2. Accept (q (t1 + t2))) ⇔
∃x0 l j p.
0 < l ∧ (∀t2. j (x0 + t2) = j (x0 + t2 MOD l)) ∧
(∀t2. p (x0 + t2) = p (x0 + t2 MOD l)) ∧ InitState (p 0) ∧
(∀t. TransRel (j t,p t,p (t + 1))) ∧ ∀t1. ∃t2. Accept (p (t1 + t2)))
- BUECHI_PERIODIC_REDUCTION_THM
-
⊢ (∀s. ∃x0 l. 0 < l ∧ s x0 = s (x0 + l)) ⇒
((∃i q.
InitState (q 0) ∧ (∀t. TransRel (i t,q t,q (t + 1))) ∧
∀t1. ∃t2. Accept (q (t1 + t2))) ⇔
∃x0 l j p.
0 < l ∧ (∀t2. j (x0 + t2) = j (x0 + t2 MOD l)) ∧
(∀t2. p (x0 + t2) = p (x0 + t2 MOD l)) ∧ InitState (p 0) ∧
(∀t. t < x0 + l ⇒ TransRel (j t,p t,p (t + 1))) ∧
∃t. t < l ∧ Accept (p (x0 + t)))
- BUECHI_PROP_REDUCTION
-
⊢ (∀s. ∃x0 l. 0 < l ∧ s x0 = s (x0 + l)) ⇒
((∃i q.
InitState (q 0) ∧ (∀t. TransRel (i t,q t,q (t + 1))) ∧
∀t1. ∃t2. Accept (q (t1 + t2))) ⇔
∃x0 l j p.
0 < l ∧ InitState (p 0) ∧
(∀t. t < x0 + l ⇒ TransRel (j t,p t,p (t + 1))) ∧
(∃t. t < l ∧ Accept (p (x0 + t))) ∧ p x0 = p (x0 + l))
- EQUALITY_THM
-
⊢ ∀x y. x = y ⇔ ∀P. P x ⇔ P y
- LESS_THM
-
⊢ ∀x y. x < y ⇔ ∃P. P x ∧ ¬P y ∧ ∀z. P (SUC z) ⇒ P z
- FORALL_EXISTS_THM
-
⊢ ∀P. (∀t1. ∃t2. P (t1 + t2)) ⇔ ∀t1. ∃t2. t1 < t2 ∧ P t2
- EXISTS_FORALL_THM
-
⊢ ∀P. (∃t1. ∀t2. P (t1 + t2)) ⇔ ∃t1. ∀t2. t1 < t2 ⇒ P t2
- ELGOT_LEMMA
-
⊢ ∀PHI. (∃x. ∀p. PHI p x) ⇔ ∃q. (∀x. q x ⇒ ∀p. PHI p x) ∧ ∃z. q z
- ELGOT1_THM
-
⊢ ∀PHI. (∃x. ∀p. PHI p x) ⇔ ∃q. ∀p x. ∃z. (q x ⇒ PHI p x) ∧ q z
- ELGOT2_THM
-
⊢ ∀PHI. (∀x. ∃p. PHI p x) ⇔ ∀q. ∃p x. ∀z. q z ⇒ PHI p x ∧ q x