Structure Omega_AutomataTheory
signature Omega_AutomataTheory =
sig
type thm = Thm.thm
(* Theorems *)
val AUTOMATON_TEMP_CLOSURE : thm
val BEFORE_AS_CO_BUECHI : thm
val BOOLEAN_CLOSURE_F : thm
val BOOLEAN_CLOSURE_FG : thm
val BOOLEAN_CLOSURE_G : thm
val BOOLEAN_CLOSURE_GF : thm
val BOREL_HIERARCHY_F : thm
val BOREL_HIERARCHY_FG : thm
val BOREL_HIERARCHY_G : thm
val BUECHI_PERIODIC_MODEL : thm
val BUECHI_PERIODIC_REDUCTION_THM : thm
val BUECHI_PROP_REDUCTION : thm
val BUECHI_TRANSLATION : thm
val CO_BUECHI_BEFORE_CLOSURE : thm
val CO_BUECHI_CONJ_CLOSURE : thm
val CO_BUECHI_DISJ_CLOSURE : thm
val CO_BUECHI_NEXT_CLOSURE : thm
val CO_BUECHI_SBEFORE_CLOSURE : thm
val CO_BUECHI_SUNTIL_CLOSURE : thm
val CO_BUECHI_SWHEN_CLOSURE : thm
val CO_BUECHI_UNTIL_CLOSURE : thm
val CO_BUECHI_WHEN_CLOSURE : thm
val DET_OMEGA_EXISTS_FORALL_THEOREM : thm
val ELGOT1_THM : thm
val ELGOT2_THM : thm
val ELGOT_LEMMA : thm
val EQUALITY_THM : thm
val EXISTS_FORALL_THM : thm
val FORALL_EXISTS_THM : thm
val LESS_THM : thm
val NEG_DET_AUTOMATA : thm
val NEXT_AS_CO_BUECHI : thm
val OMEGA_CONJ_CLOSURE : thm
val OMEGA_DISJ_CLOSURE : thm
val SBEFORE_AS_CO_BUECHI : thm
val SUNTIL_AS_CO_BUECHI : thm
val SWHEN_AS_CO_BUECHI : thm
val TEMP_OPS_DEFS_TO_OMEGA : thm
val UNTIL_AS_CO_BUECHI : thm
val WHEN_AS_CO_BUECHI : thm
val Omega_Automata_grammars : type_grammar.grammar * term_grammar.grammar
(*
[Past_Temporal_Logic] Parent theory of "Omega_Automata"
[AUTOMATON_TEMP_CLOSURE] Theorem
|- ((∃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 (PNEXT 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 (PNEXT (PALWAYS a)) ⇔
∃q. q 0 ∧ (∀t. q (t + 1) ⇔ a t ∧ q t) ∧ Phi q) ∧
(Phi (PSNEXT (PEVENTUAL 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 (PNEXT (a PUNTIL b)) ⇔
∃q. q 0 ∧ (∀t. q (t + 1) ⇔ b t ∨ a t ∧ q t) ∧ Phi q) ∧
(Phi (PNEXT (a PWHEN b)) ⇔
∃q. q 0 ∧ (∀t. q (t + 1) ⇔ a t ∧ b t ∨ ¬b t ∧ q t) ∧ Phi q) ∧
(Phi (PNEXT (a PBEFORE b)) ⇔
∃q. q 0 ∧ (∀t. q (t + 1) ⇔ ¬b t ∧ (a t ∨ q t)) ∧ Phi q)
[BEFORE_AS_CO_BUECHI] Theorem
|- (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))
[BOOLEAN_CLOSURE_F] Theorem
|- (¬(∃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] Theorem
|- (¬(∃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_G] Theorem
|- (¬(∀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_GF] Theorem
|- (¬(∀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_F] Theorem
|- ((∃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] Theorem
|- ((∃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)))
[BOREL_HIERARCHY_G] Theorem
|- ((∀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)))
[BUECHI_PERIODIC_MODEL] Theorem
|- (∀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] Theorem
|- (∀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] Theorem
|- (∀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)))
[BUECHI_TRANSLATION] Theorem
|- (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_BEFORE_CLOSURE] Theorem
|- ((λ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_CONJ_CLOSURE] Theorem
|- (∃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] Theorem
|- (∃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] Theorem
|- 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_SBEFORE_CLOSURE] Theorem
|- ((λ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_SUNTIL_CLOSURE] Theorem
|- (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_SWHEN_CLOSURE] Theorem
|- ((λ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_UNTIL_CLOSURE] Theorem
|- (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_WHEN_CLOSURE] Theorem
|- ((λ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)))
[DET_OMEGA_EXISTS_FORALL_THEOREM] 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)))
[ELGOT1_THM] Theorem
|- ∀PHI. (∃x. ∀p. PHI p x) ⇔ ∃q. ∀p x. ∃z. (q x ⇒ PHI p x) ∧ q z
[ELGOT2_THM] Theorem
|- ∀PHI. (∀x. ∃p. PHI p x) ⇔ ∀q. ∃p x. ∀z. q z ⇒ PHI p x ∧ q x
[ELGOT_LEMMA] Theorem
|- ∀PHI. (∃x. ∀p. PHI p x) ⇔ ∃q. (∀x. q x ⇒ ∀p. PHI p x) ∧ ∃z. q z
[EQUALITY_THM] Theorem
|- ∀x y. (x = y) ⇔ ∀P. P x ⇔ P y
[EXISTS_FORALL_THM] Theorem
|- ∀P. (∃t1. ∀t2. P (t1 + t2)) ⇔ ∃t1. ∀t2. t1 < t2 ⇒ P t2
[FORALL_EXISTS_THM] Theorem
|- ∀P. (∀t1. ∃t2. P (t1 + t2)) ⇔ ∀t1. ∃t2. t1 < t2 ∧ P t2
[LESS_THM] Theorem
|- ∀x y. x < y ⇔ ∃P. P x ∧ ¬P y ∧ ∀z. P (SUC z) ⇒ P z
[NEG_DET_AUTOMATA] 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)))
[NEXT_AS_CO_BUECHI] Theorem
|- 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))
[OMEGA_CONJ_CLOSURE] Theorem
|- (∃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] Theorem
|- (∃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))
[SBEFORE_AS_CO_BUECHI] Theorem
|- (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))
[SUNTIL_AS_CO_BUECHI] Theorem
|- (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))
[SWHEN_AS_CO_BUECHI] Theorem
|- (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))
[TEMP_OPS_DEFS_TO_OMEGA] Theorem
|- ((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 = PNEXT 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 = PNEXT (PALWAYS a)) ⇔
(l 0 ⇔ T) ∧ (∀t. l (SUC t) ⇔ a t ∧ l t) ∧ T) ∧
((l = PSNEXT (PEVENTUAL 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 = PNEXT (a PUNTIL b)) ⇔
(l 0 ⇔ T) ∧ (∀t. l (SUC t) ⇔ b t ∨ a t ∧ l t) ∧ T) ∧
((l = PNEXT (a PWHEN b)) ⇔
(l 0 ⇔ T) ∧ (∀t. l (SUC t) ⇔ a t ∧ b t ∨ ¬b t ∧ l t) ∧ T) ∧
((l = PNEXT (a PBEFORE b)) ⇔
(l 0 ⇔ T) ∧ (∀t. l (SUC t) ⇔ ¬b t ∧ (a t ∨ l t)) ∧ T)
[UNTIL_AS_CO_BUECHI] Theorem
|- (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))
[WHEN_AS_CO_BUECHI] Theorem
|- (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))
*)
end
HOL 4, Kananaskis-10