Structure Omega_AutomataTheory


Source File Identifier index Theory binding index

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 (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)
   
   [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 = 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)
   
   [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


Source File Identifier index Theory binding index

HOL 4, Kananaskis-13