tt('thm/Omega_Automata/DET_OMEGA_EXISTS_FORALL_THEOREM_', ax, ![STATE : $t, INPUT : $t]: (![t0 : 'type/num/num', i : ('type/num/num' > INPUT), TransRel : (('type/pair/prod' INPUT STATE) > STATE), InitVal : STATE, Accept : (('type/pair/prod' ('type/num/num' > INPUT) ('type/num/num' > STATE)) > $o)]: ((?[q : ('type/num/num' > STATE)]: (((q t0) = InitVal) & ((![t : 'type/num/num']: ((q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = (TransRel (('const/pair/,' INPUT STATE) (i ('const/arithmetic/+' t t0)) (q ('const/arithmetic/+' t t0)))))) & (Accept (('const/pair/,' ('type/num/num' > INPUT) ('type/num/num' > STATE)) i (^[t : 'type/num/num']: (q ('const/arithmetic/+' t t0)))))))) = (![q : ('type/num/num' > STATE)]: ((((q t0) = InitVal) & (![t : 'type/num/num']: ((q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = (TransRel (('const/pair/,' INPUT STATE) (i ('const/arithmetic/+' t t0)) (q ('const/arithmetic/+' t t0))))))) => (Accept (('const/pair/,' ('type/num/num' > INPUT) ('type/num/num' > STATE)) i (^[t : 'type/num/num']: (q ('const/arithmetic/+' t t0)))))))))).
tt('thm/Omega_Automata/NEG_DET_AUTOMATA_', ax, ![STATE : $t, INPUT : $t]: (![t0 : 'type/num/num', i : ('type/num/num' > INPUT), TransRel : (('type/pair/prod' INPUT STATE) > STATE), InitVal : STATE, Accept : (('type/pair/prod' ('type/num/num' > INPUT) ('type/num/num' > STATE)) > $o)]: ((~ (?[q : ('type/num/num' > STATE)]: (((q t0) = InitVal) & ((![t : 'type/num/num']: ((q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = (TransRel (('const/pair/,' INPUT STATE) (i ('const/arithmetic/+' t t0)) (q ('const/arithmetic/+' t t0)))))) & (Accept (('const/pair/,' ('type/num/num' > INPUT) ('type/num/num' > STATE)) i (^[t : 'type/num/num']: (q ('const/arithmetic/+' t t0))))))))) = (?[q : ('type/num/num' > STATE)]: (((q t0) = InitVal) & ((![t : 'type/num/num']: ((q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = (TransRel (('const/pair/,' INPUT STATE) (i ('const/arithmetic/+' t t0)) (q ('const/arithmetic/+' t t0)))))) & (~ (Accept (('const/pair/,' ('type/num/num' > INPUT) ('type/num/num' > STATE)) i (^[t : 'type/num/num']: (q ('const/arithmetic/+' t t0)))))))))))).
tt('thm/Omega_Automata/OMEGA_CONJ_CLOSURE_', ax, ![B2 : $t, A : $t, B1 : $t]: (![t0 : 'type/num/num', i : ('type/num/num' > A), Psi2 : (('type/pair/prod' ('type/num/num' > A) ('type/num/num' > B2)) > $o), Psi1 : (('type/pair/prod' ('type/num/num' > A) ('type/num/num' > B1)) > $o), Phi_R2 : (('type/pair/prod' A B2) > $o), Phi_R1 : (('type/pair/prod' A B1) > $o), Phi_I2 : (B2 > $o), Phi_I1 : (B1 > $o)]: (((?[q1 : ('type/num/num' > B1)]: ((Phi_I1 (q1 t0)) & ((![t : 'type/num/num']: (Phi_R1 (('const/pair/,' A B1) (i ('const/arithmetic/+' t t0)) (q1 ('const/arithmetic/+' t t0))))) & (Psi1 (('const/pair/,' ('type/num/num' > A) ('type/num/num' > B1)) i q1))))) & (?[q2 : ('type/num/num' > B2)]: ((Phi_I2 (q2 t0)) & ((![t : 'type/num/num']: (Phi_R2 (('const/pair/,' A B2) (i ('const/arithmetic/+' t t0)) (q2 ('const/arithmetic/+' t t0))))) & (Psi2 (('const/pair/,' ('type/num/num' > A) ('type/num/num' > B2)) i q2)))))) = (?[q1 : ('type/num/num' > B1), q2 : ('type/num/num' > B2)]: (((Phi_I1 (q1 t0)) & (Phi_I2 (q2 t0))) & ((![t : 'type/num/num']: ((Phi_R1 (('const/pair/,' A B1) (i ('const/arithmetic/+' t t0)) (q1 ('const/arithmetic/+' t t0)))) & (Phi_R2 (('const/pair/,' A B2) (i ('const/arithmetic/+' t t0)) (q2 ('const/arithmetic/+' t t0)))))) & ((Psi1 (('const/pair/,' ('type/num/num' > A) ('type/num/num' > B1)) i q1)) & (Psi2 (('const/pair/,' ('type/num/num' > A) ('type/num/num' > B2)) i q2))))))))).
tt('thm/Omega_Automata/OMEGA_DISJ_CLOSURE_', ax, ![B2 : $t, A : $t, B1 : $t]: (![t0 : 'type/num/num', i : ('type/num/num' > A), Psi2 : (('type/pair/prod' ('type/num/num' > A) ('type/num/num' > B2)) > $o), Psi1 : (('type/pair/prod' ('type/num/num' > A) ('type/num/num' > B1)) > $o), Phi_R2 : (('type/pair/prod' A B2) > $o), Phi_R1 : (('type/pair/prod' A B1) > $o), Phi_I2 : (B2 > $o), Phi_I1 : (B1 > $o)]: (((?[q1 : ('type/num/num' > B1)]: ((Phi_I1 (q1 t0)) & ((![t : 'type/num/num']: (Phi_R1 (('const/pair/,' A B1) (i ('const/arithmetic/+' t t0)) (q1 ('const/arithmetic/+' t t0))))) & (Psi1 (('const/pair/,' ('type/num/num' > A) ('type/num/num' > B1)) i q1))))) | (?[q2 : ('type/num/num' > B2)]: ((Phi_I2 (q2 t0)) & ((![t : 'type/num/num']: (Phi_R2 (('const/pair/,' A B2) (i ('const/arithmetic/+' t t0)) (q2 ('const/arithmetic/+' t t0))))) & (Psi2 (('const/pair/,' ('type/num/num' > A) ('type/num/num' > B2)) i q2)))))) = (?[p : ('type/num/num' > $o), q1 : ('type/num/num' > B1), q2 : ('type/num/num' > B2)]: ((((~ (p t0)) & (Phi_I1 (q1 t0))) | ((p t0) & (Phi_I2 (q2 t0)))) & ((![t : 'type/num/num']: (((~ (p ('const/arithmetic/+' t t0))) & ((Phi_R1 (('const/pair/,' A B1) (i ('const/arithmetic/+' t t0)) (q1 ('const/arithmetic/+' t t0)))) & (~ (p ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))) | ((p ('const/arithmetic/+' t t0)) & ((Phi_R2 (('const/pair/,' A B2) (i ('const/arithmetic/+' t t0)) (q2 ('const/arithmetic/+' t t0)))) & (p ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))) & (((~ (p t0)) & (Psi1 (('const/pair/,' ('type/num/num' > A) ('type/num/num' > B1)) i q1))) | ((p t0) & (Psi2 (('const/pair/,' ('type/num/num' > A) ('type/num/num' > B2)) i q2)))))))))).
tt('thm/Omega_Automata/BOOLEAN_CLOSURE_G_0', ax, (![t0 : 'type/num/num', a : ('type/num/num' > $o)]: ((~ (![t : 'type/num/num']: (a ('const/arithmetic/+' t t0)))) = (?[t : 'type/num/num']: (~ (a ('const/arithmetic/+' t t0))))))).
tt('thm/Omega_Automata/BOOLEAN_CLOSURE_G_1', ax, (![t0 : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (((![t : 'type/num/num']: (a ('const/arithmetic/+' t t0))) & (![t : 'type/num/num']: (b ('const/arithmetic/+' t t0)))) = (![t : 'type/num/num']: ((a ('const/arithmetic/+' t t0)) & (b ('const/arithmetic/+' t t0))))))).
tt('thm/Omega_Automata/BOOLEAN_CLOSURE_G_e2', ax, (![t0 : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (((![t : 'type/num/num']: (a ('const/arithmetic/+' t t0))) | (![t : 'type/num/num']: (b ('const/arithmetic/+' t t0)))) = (?[p : ('type/num/num' > $o), q : ('type/num/num' > $o)]: (((~ (p t0)) & (~ (q t0))) & ((![t : 'type/num/num']: (((p ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = ((p ('const/arithmetic/+' t t0)) | (~ (a ('const/arithmetic/+' t t0))))) & ((q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = ((q ('const/arithmetic/+' t t0)) | (~ (b ('const/arithmetic/+' t t0))))))) & (![t : 'type/num/num']: ((~ (p ('const/arithmetic/+' t t0))) | (~ (q ('const/arithmetic/+' t t0))))))))))).
tt('thm/Omega_Automata/BOOLEAN_CLOSURE_F_0', ax, (![t0 : 'type/num/num', a : ('type/num/num' > $o)]: ((~ (?[t : 'type/num/num']: (a ('const/arithmetic/+' t t0)))) = (![t : 'type/num/num']: (~ (a ('const/arithmetic/+' t t0))))))).
tt('thm/Omega_Automata/BOOLEAN_CLOSURE_F_1', ax, (![t0 : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (((?[t : 'type/num/num']: (a ('const/arithmetic/+' t t0))) | (?[t : 'type/num/num']: (b ('const/arithmetic/+' t t0)))) = (?[t : 'type/num/num']: ((a ('const/arithmetic/+' t t0)) | (b ('const/arithmetic/+' t t0))))))).
tt('thm/Omega_Automata/BOOLEAN_CLOSURE_F_e2', ax, (![t0 : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (((?[t : 'type/num/num']: (a ('const/arithmetic/+' t t0))) & (?[t : 'type/num/num']: (b ('const/arithmetic/+' t t0)))) = (?[p : ('type/num/num' > $o), q : ('type/num/num' > $o)]: (((~ (p t0)) & (~ (q t0))) & ((![t : 'type/num/num']: (((p ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = ((p ('const/arithmetic/+' t t0)) | (a ('const/arithmetic/+' t t0)))) & ((q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = ((q ('const/arithmetic/+' t t0)) | (b ('const/arithmetic/+' t t0)))))) & (?[t : 'type/num/num']: ((p ('const/arithmetic/+' t t0)) & (q ('const/arithmetic/+' t t0)))))))))).
tt('thm/Omega_Automata/BOOLEAN_CLOSURE_FG_0', ax, (![t0 : 'type/num/num', a : ('type/num/num' > $o)]: ((~ (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (a ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))) = (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: (~ (a ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))))))).
tt('thm/Omega_Automata/BOOLEAN_CLOSURE_FG_1', ax, (![t0 : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (((?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (a ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (b ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))) = (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: ((a ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) & (b ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))))))).
tt('thm/Omega_Automata/BOOLEAN_CLOSURE_FG_e2', ax, (![t0 : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (((?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (a ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))) | (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (b ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))) = (?[q : ('type/num/num' > $o)]: ((~ (q t0)) & ((![t : 'type/num/num']: ((q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = (('const/bool/COND' $o) (q ('const/arithmetic/+' t t0)) (b ('const/arithmetic/+' t t0)) (~ (a ('const/arithmetic/+' t t0)))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: ((~ (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))) | (b ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))))))))).
tt('thm/Omega_Automata/BOOLEAN_CLOSURE_GF_0', ax, (![t0 : 'type/num/num', a : ('type/num/num' > $o)]: ((~ (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: (a ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))) = (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (~ (a ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))))))).
tt('thm/Omega_Automata/BOOLEAN_CLOSURE_GF_1', ax, (![t0 : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (((![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: (a ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))) | (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: (b ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))) = (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: ((a ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) | (b ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))))))).
tt('thm/Omega_Automata/BOOLEAN_CLOSURE_GF_e2', ax, (![t0 : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (((![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: (a ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))) & (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: (b ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))) = (?[q : ('type/num/num' > $o)]: ((~ (q t0)) & ((![t : 'type/num/num']: ((q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = (('const/bool/COND' $o) (q ('const/arithmetic/+' t t0)) (~ (b ('const/arithmetic/+' t t0))) (a ('const/arithmetic/+' t t0))))) & (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: ((q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) & (b ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))))))))).
tt('thm/Omega_Automata/BOREL_HIERARCHY_G_0', ax, (![t0 : 'type/num/num', a : ('type/num/num' > $o)]: ((![t : 'type/num/num']: (a ('const/arithmetic/+' t t0))) = (?[q : ('type/num/num' > $o)]: ((q t0) & ((![t : 'type/num/num']: ((q ('const/arithmetic/+' t t0)) & ((a ('const/arithmetic/+' t t0)) & (q ('const/num/SUC' ('const/arithmetic/+' t t0)))))) & (?[t : 'type/num/num']: (q ('const/arithmetic/+' t t0))))))))).
tt('thm/Omega_Automata/BOREL_HIERARCHY_G_1', ax, (![t0 : 'type/num/num', a : ('type/num/num' > $o)]: ((![t : 'type/num/num']: (a ('const/arithmetic/+' t t0))) = (?[q : ('type/num/num' > $o)]: ((q t0) & ((![t : 'type/num/num']: ((q ('const/num/SUC' ('const/arithmetic/+' t t0))) = ((q ('const/arithmetic/+' t t0)) & (a ('const/arithmetic/+' t t0))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))))))))).
tt('thm/Omega_Automata/BOREL_HIERARCHY_G_e2', ax, (![t0 : 'type/num/num', a : ('type/num/num' > $o)]: ((![t : 'type/num/num']: (a ('const/arithmetic/+' t t0))) = (?[q : ('type/num/num' > $o)]: ((q t0) & ((![t : 'type/num/num']: ((q ('const/num/SUC' ('const/arithmetic/+' t t0))) = ((q ('const/arithmetic/+' t t0)) & (a ('const/arithmetic/+' t t0))))) & (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))))))))).
tt('thm/Omega_Automata/BOREL_HIERARCHY_F_0', ax, (![t0 : 'type/num/num', a : ('type/num/num' > $o)]: ((?[t : 'type/num/num']: (a ('const/arithmetic/+' t t0))) = (?[q : ('type/num/num' > $o)]: ((~ (q t0)) & ((![t : 'type/num/num']: ((q ('const/num/SUC' ('const/arithmetic/+' t t0))) = ((q ('const/arithmetic/+' t t0)) | (a ('const/arithmetic/+' t t0))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))))))))).
tt('thm/Omega_Automata/BOREL_HIERARCHY_F_e1', ax, (![t0 : 'type/num/num', a : ('type/num/num' > $o)]: ((?[t : 'type/num/num']: (a ('const/arithmetic/+' t t0))) = (?[q : ('type/num/num' > $o)]: ((~ (q t0)) & ((![t : 'type/num/num']: ((q ('const/num/SUC' ('const/arithmetic/+' t t0))) = ((q ('const/arithmetic/+' t t0)) | (a ('const/arithmetic/+' t t0))))) & (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))))))))).
tt('thm/Omega_Automata/BOREL_HIERARCHY_FG_0', ax, (![t0 : 'type/num/num', a : ('type/num/num' > $o)]: ((?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (a ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))) = (?[q : ('type/num/num' > $o)]: ((~ (q t0)) & ((![t : 'type/num/num']: ((q ('const/arithmetic/+' t t0)) => ((a ('const/arithmetic/+' t t0)) & (q ('const/num/SUC' ('const/arithmetic/+' t t0)))))) & (?[t : 'type/num/num']: (q ('const/arithmetic/+' t t0))))))))).
tt('thm/Omega_Automata/BOREL_HIERARCHY_FG_e1', ax, (![t0 : 'type/num/num', a : ('type/num/num' > $o)]: ((?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (a ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))) = (?[p : ('type/num/num' > $o), q : ('type/num/num' > $o)]: (((~ (p t0)) & (~ (q t0))) & ((![t : 'type/num/num']: (((p ('const/arithmetic/+' t t0)) => (p ('const/num/SUC' ('const/arithmetic/+' t t0)))) & (((p ('const/num/SUC' ('const/arithmetic/+' t t0))) => ((p ('const/arithmetic/+' t t0)) | (~ (q ('const/arithmetic/+' t t0))))) & ((q ('const/num/SUC' ('const/arithmetic/+' t t0))) = (((p ('const/arithmetic/+' t t0)) & ((~ (q ('const/arithmetic/+' t t0))) & (~ (a ('const/arithmetic/+' t t0))))) | ((p ('const/arithmetic/+' t t0)) & (q ('const/arithmetic/+' t t0)))))))) & (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: ((p ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) & (~ (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))))))))))).
tt('thm/Omega_Automata/TEMP_OPS_DEFS_TO_OMEGA_0', ax, (![l : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((l = ('const/Temporal_Logic/NEXT' a)) = ($true & ((![t : 'type/num/num']: ((l t) = (a ('const/num/SUC' t)))) & $true))))).
tt('thm/Omega_Automata/TEMP_OPS_DEFS_TO_OMEGA_1', ax, (![l : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((l = ('const/Temporal_Logic/ALWAYS' a)) = ($true & ((![t : 'type/num/num']: ((l t) = ((a t) & (l ('const/num/SUC' t))))) & (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: ((a ('const/arithmetic/+' t1 t2)) => (l ('const/arithmetic/+' t1 t2)))))))))).
tt('thm/Omega_Automata/TEMP_OPS_DEFS_TO_OMEGA_2', ax, (![l : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((l = ('const/Temporal_Logic/EVENTUAL' a)) = ($true & ((![t : 'type/num/num']: ((l t) = ((a t) | (l ('const/num/SUC' t))))) & (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: ((l ('const/arithmetic/+' t1 t2)) => (a ('const/arithmetic/+' t1 t2)))))))))).
tt('thm/Omega_Automata/TEMP_OPS_DEFS_TO_OMEGA_3', ax, (![l : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((l = ('const/Temporal_Logic/SUNTIL' a b)) = ($true & ((![t : 'type/num/num']: ((l t) = ((~ (b t)) => ((a t) & (l ('const/num/SUC' t)))))) & (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: ((l ('const/arithmetic/+' t1 t2)) => ((~ (a ('const/arithmetic/+' t1 t2))) | (b ('const/arithmetic/+' t1 t2))))))))))).
tt('thm/Omega_Automata/TEMP_OPS_DEFS_TO_OMEGA_4', ax, (![l : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((l = ('const/Temporal_Logic/SWHEN' a b)) = ($true & ((![t : 'type/num/num']: ((l t) = (('const/bool/COND' $o) (b t) (a t) (l ('const/num/SUC' t))))) & (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: ((l ('const/arithmetic/+' t1 t2)) => (b ('const/arithmetic/+' t1 t2)))))))))).
tt('thm/Omega_Automata/TEMP_OPS_DEFS_TO_OMEGA_5', ax, (![l : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((l = ('const/Temporal_Logic/SBEFORE' a b)) = ($true & ((![t : 'type/num/num']: ((l t) = ((~ (b t)) & ((a t) | (l ('const/num/SUC' t)))))) & (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: ((l ('const/arithmetic/+' t1 t2)) => ((a ('const/arithmetic/+' t1 t2)) | (b ('const/arithmetic/+' t1 t2))))))))))).
tt('thm/Omega_Automata/TEMP_OPS_DEFS_TO_OMEGA_6', ax, (![l : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((l = ('const/Temporal_Logic/UNTIL' a b)) = ($true & ((![t : 'type/num/num']: ((l t) = ((~ (b t)) => ((a t) & (l ('const/num/SUC' t)))))) & (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: ((~ (l ('const/arithmetic/+' t1 t2))) => ((~ (a ('const/arithmetic/+' t1 t2))) | (b ('const/arithmetic/+' t1 t2))))))))))).
tt('thm/Omega_Automata/TEMP_OPS_DEFS_TO_OMEGA_7', ax, (![l : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((l = ('const/Temporal_Logic/WHEN' a b)) = ($true & ((![t : 'type/num/num']: ((l t) = (('const/bool/COND' $o) (b t) (a t) (l ('const/num/SUC' t))))) & (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: ((l ('const/arithmetic/+' t1 t2)) | (b ('const/arithmetic/+' t1 t2)))))))))).
tt('thm/Omega_Automata/TEMP_OPS_DEFS_TO_OMEGA_8', ax, (![l : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((l = ('const/Temporal_Logic/BEFORE' a b)) = ($true & ((![t : 'type/num/num']: ((l t) = ((~ (b t)) & ((a t) | (l ('const/num/SUC' t)))))) & (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: ((~ (l ('const/arithmetic/+' t1 t2))) => ((a ('const/arithmetic/+' t1 t2)) | (b ('const/arithmetic/+' t1 t2))))))))))).
tt('thm/Omega_Automata/TEMP_OPS_DEFS_TO_OMEGA_9', ax, (![l : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((l = ('const/Past_Temporal_Logic/PNEXT' a)) = (((l 'const/num/0') = $true) & ((![t : 'type/num/num']: ((l ('const/num/SUC' t)) = (a t))) & $true))))).
tt('thm/Omega_Automata/TEMP_OPS_DEFS_TO_OMEGA_10', ax, (![l : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((l = ('const/Past_Temporal_Logic/PSNEXT' a)) = (((l 'const/num/0') = $false) & ((![t : 'type/num/num']: ((l ('const/num/SUC' t)) = (a t))) & $true))))).
tt('thm/Omega_Automata/TEMP_OPS_DEFS_TO_OMEGA_11', ax, (![l : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((l = ('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PALWAYS' a))) = (((l 'const/num/0') = $true) & ((![t : 'type/num/num']: ((l ('const/num/SUC' t)) = ((a t) & (l t)))) & $true))))).
tt('thm/Omega_Automata/TEMP_OPS_DEFS_TO_OMEGA_12', ax, (![l : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((l = ('const/Past_Temporal_Logic/PSNEXT' ('const/Past_Temporal_Logic/PEVENTUAL' a))) = (((l 'const/num/0') = $false) & ((![t : 'type/num/num']: ((l ('const/num/SUC' t)) = ((a t) | (l t)))) & $true))))).
tt('thm/Omega_Automata/TEMP_OPS_DEFS_TO_OMEGA_13', ax, (![l : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((l = ('const/Past_Temporal_Logic/PSNEXT' ('const/Past_Temporal_Logic/PSUNTIL' a b))) = (((l 'const/num/0') = $false) & ((![t : 'type/num/num']: ((l ('const/num/SUC' t)) = ((b t) | ((a t) & (l t))))) & $true))))).
tt('thm/Omega_Automata/TEMP_OPS_DEFS_TO_OMEGA_14', ax, (![l : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((l = ('const/Past_Temporal_Logic/PSNEXT' ('const/Past_Temporal_Logic/PSWHEN' a b))) = (((l 'const/num/0') = $false) & ((![t : 'type/num/num']: ((l ('const/num/SUC' t)) = (((a t) & (b t)) | ((~ (b t)) & (l t))))) & $true))))).
tt('thm/Omega_Automata/TEMP_OPS_DEFS_TO_OMEGA_15', ax, (![l : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((l = ('const/Past_Temporal_Logic/PSNEXT' ('const/Past_Temporal_Logic/PSBEFORE' a b))) = (((l 'const/num/0') = $false) & ((![t : 'type/num/num']: ((l ('const/num/SUC' t)) = ((~ (b t)) & ((a t) | (l t))))) & $true))))).
tt('thm/Omega_Automata/TEMP_OPS_DEFS_TO_OMEGA_16', ax, (![l : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((l = ('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PUNTIL' a b))) = (((l 'const/num/0') = $true) & ((![t : 'type/num/num']: ((l ('const/num/SUC' t)) = ((b t) | ((a t) & (l t))))) & $true))))).
tt('thm/Omega_Automata/TEMP_OPS_DEFS_TO_OMEGA_17', ax, (![l : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((l = ('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PWHEN' a b))) = (((l 'const/num/0') = $true) & ((![t : 'type/num/num']: ((l ('const/num/SUC' t)) = (((a t) & (b t)) | ((~ (b t)) & (l t))))) & $true))))).
tt('thm/Omega_Automata/TEMP_OPS_DEFS_TO_OMEGA_e18', ax, (![l : ('type/num/num' > $o), b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: ((l = ('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PBEFORE' a b))) = (((l 'const/num/0') = $true) & ((![t : 'type/num/num']: ((l ('const/num/SUC' t)) = ((~ (b t)) & ((a t) | (l t))))) & $true))))).
tt('thm/Omega_Automata/AUTOMATON_TEMP_CLOSURE_0', ax, ![B : $t, A : $t]: (![Phi_R2 : (('type/pair/prod' ('type/num/num' > B) ('type/num/num' > A)) > $o), Phi_R1 : (('type/num/num' > A) > $o), Phi_I2 : (('type/num/num' > B) > $o), Phi_I1 : (('type/num/num' > A) > $o), Phi_F : (('type/pair/prod' ('type/num/num' > A) ('type/num/num' > B)) > $o)]: ((?[q1 : ('type/num/num' > A)]: ((Phi_I1 q1) & ((Phi_R1 q1) & (?[q2 : ('type/num/num' > B)]: ((Phi_I2 q2) & ((Phi_R2 (('const/pair/,' ('type/num/num' > B) ('type/num/num' > A)) q2 q1)) & (Phi_F (('const/pair/,' ('type/num/num' > A) ('type/num/num' > B)) q1 q2)))))))) = (?[q1 : ('type/num/num' > A), q2 : ('type/num/num' > B)]: (((Phi_I1 q1) & (Phi_I2 q2)) & (((Phi_R1 q1) & (Phi_R2 (('const/pair/,' ('type/num/num' > B) ('type/num/num' > A)) q2 q1))) & (Phi_F (('const/pair/,' ('type/num/num' > A) ('type/num/num' > B)) q1 q2)))))))).
tt('thm/Omega_Automata/AUTOMATON_TEMP_CLOSURE_1', ax, (![phi : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Temporal_Logic/NEXT' phi)) = (?[q0 : ('type/num/num' > $o), q1 : ('type/num/num' > $o)]: ($true & ((![t : 'type/num/num']: (((q0 t) = (phi t)) & ((q1 t) = (q0 ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))) & (Phi q1))))))).
tt('thm/Omega_Automata/AUTOMATON_TEMP_CLOSURE_2', ax, (![phi : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Past_Temporal_Logic/PNEXT' phi)) = (?[q : ('type/num/num' > $o)]: ((q 'const/num/0') & ((![t : 'type/num/num']: ((q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = (phi t))) & (Phi q))))))).
tt('thm/Omega_Automata/AUTOMATON_TEMP_CLOSURE_3', ax, (![phi : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Past_Temporal_Logic/PSNEXT' phi)) = (?[q : ('type/num/num' > $o)]: ((~ (q 'const/num/0')) & ((![t : 'type/num/num']: ((q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = (phi t))) & (Phi q))))))).
tt('thm/Omega_Automata/AUTOMATON_TEMP_CLOSURE_4', ax, (![a : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PALWAYS' a))) = (?[q : ('type/num/num' > $o)]: ((q 'const/num/0') & ((![t : 'type/num/num']: ((q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ((a t) & (q t)))) & (Phi q))))))).
tt('thm/Omega_Automata/AUTOMATON_TEMP_CLOSURE_5', ax, (![a : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Past_Temporal_Logic/PSNEXT' ('const/Past_Temporal_Logic/PEVENTUAL' a))) = (?[q : ('type/num/num' > $o)]: ((~ (q 'const/num/0')) & ((![t : 'type/num/num']: ((q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ((a t) | (q t)))) & (Phi q))))))).
tt('thm/Omega_Automata/AUTOMATON_TEMP_CLOSURE_6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Past_Temporal_Logic/PSNEXT' ('const/Past_Temporal_Logic/PSUNTIL' a b))) = (?[q : ('type/num/num' > $o)]: ((~ (q 'const/num/0')) & ((![t : 'type/num/num']: ((q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ((b t) | ((a t) & (q t))))) & (Phi q))))))).
tt('thm/Omega_Automata/AUTOMATON_TEMP_CLOSURE_7', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Past_Temporal_Logic/PSNEXT' ('const/Past_Temporal_Logic/PSWHEN' a b))) = (?[q : ('type/num/num' > $o)]: ((~ (q 'const/num/0')) & ((![t : 'type/num/num']: ((q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = (((a t) & (b t)) | ((~ (b t)) & (q t))))) & (Phi q))))))).
tt('thm/Omega_Automata/AUTOMATON_TEMP_CLOSURE_8', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Past_Temporal_Logic/PSNEXT' ('const/Past_Temporal_Logic/PSBEFORE' a b))) = (?[q : ('type/num/num' > $o)]: ((~ (q 'const/num/0')) & ((![t : 'type/num/num']: ((q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ((~ (b t)) & ((a t) | (q t))))) & (Phi q))))))).
tt('thm/Omega_Automata/AUTOMATON_TEMP_CLOSURE_9', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PUNTIL' a b))) = (?[q : ('type/num/num' > $o)]: ((q 'const/num/0') & ((![t : 'type/num/num']: ((q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ((b t) | ((a t) & (q t))))) & (Phi q))))))).
tt('thm/Omega_Automata/AUTOMATON_TEMP_CLOSURE_10', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PWHEN' a b))) = (?[q : ('type/num/num' > $o)]: ((q 'const/num/0') & ((![t : 'type/num/num']: ((q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = (((a t) & (b t)) | ((~ (b t)) & (q t))))) & (Phi q))))))).
tt('thm/Omega_Automata/AUTOMATON_TEMP_CLOSURE_e11', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Past_Temporal_Logic/PNEXT' ('const/Past_Temporal_Logic/PBEFORE' a b))) = (?[q : ('type/num/num' > $o)]: ((q 'const/num/0') & ((![t : 'type/num/num']: ((q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))) = ((~ (b t)) & ((a t) | (q t))))) & (Phi q))))))).
tt('thm/Omega_Automata/BUECHI_TRANSLATION_0', ax, (![phi : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Temporal_Logic/NEXT' phi)) = (?[q0 : ('type/num/num' > $o), q1 : ('type/num/num' > $o)]: ($true & ((![t : 'type/num/num']: (((q0 t) = (phi t)) & ((q1 t) = (q0 ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))) & (Phi q1))))))).
tt('thm/Omega_Automata/BUECHI_TRANSLATION_1', ax, (![a : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Temporal_Logic/ALWAYS' a)) = (?[q : ('type/num/num' > $o)]: ($true & ((![t : 'type/num/num']: ((q t) = ((a t) & (q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))) & ((![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: ((a ('const/arithmetic/+' t1 t2)) => (q ('const/arithmetic/+' t1 t2))))) & (Phi q)))))))).
tt('thm/Omega_Automata/BUECHI_TRANSLATION_2', ax, (![a : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Temporal_Logic/EVENTUAL' a)) = (?[q : ('type/num/num' > $o)]: ($true & ((![t : 'type/num/num']: ((q t) = ((a t) | (q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))) & ((![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: ((q ('const/arithmetic/+' t1 t2)) => (a ('const/arithmetic/+' t1 t2))))) & (Phi q)))))))).
tt('thm/Omega_Automata/BUECHI_TRANSLATION_3', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Temporal_Logic/SUNTIL' a b)) = (?[q : ('type/num/num' > $o)]: ($true & ((![t : 'type/num/num']: ((q t) = ((b t) | ((a t) & (q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))) & ((![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: ((q ('const/arithmetic/+' t1 t2)) => ((~ (a ('const/arithmetic/+' t1 t2))) | (b ('const/arithmetic/+' t1 t2)))))) & (Phi q)))))))).
tt('thm/Omega_Automata/BUECHI_TRANSLATION_4', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Temporal_Logic/UNTIL' a b)) = (?[q : ('type/num/num' > $o)]: ($true & ((![t : 'type/num/num']: ((q t) = ((b t) | ((a t) & (q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))) & ((![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: ((~ (q ('const/arithmetic/+' t1 t2))) => ((~ (a ('const/arithmetic/+' t1 t2))) | (b ('const/arithmetic/+' t1 t2)))))) & (Phi q)))))))).
tt('thm/Omega_Automata/BUECHI_TRANSLATION_5', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Temporal_Logic/SWHEN' a b)) = (?[q : ('type/num/num' > $o)]: ($true & ((![t : 'type/num/num']: ((q t) = (('const/bool/COND' $o) (b t) (a t) (q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))) & ((![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: ((q ('const/arithmetic/+' t1 t2)) => (b ('const/arithmetic/+' t1 t2))))) & (Phi q)))))))).
tt('thm/Omega_Automata/BUECHI_TRANSLATION_6', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Temporal_Logic/WHEN' a b)) = (?[q : ('type/num/num' > $o)]: ($true & ((![t : 'type/num/num']: ((q t) = (('const/bool/COND' $o) (b t) (a t) (q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))) & ((![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: ((q ('const/arithmetic/+' t1 t2)) | (b ('const/arithmetic/+' t1 t2))))) & (Phi q)))))))).
tt('thm/Omega_Automata/BUECHI_TRANSLATION_7', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Temporal_Logic/SBEFORE' a b)) = (?[q : ('type/num/num' > $o)]: ($true & ((![t : 'type/num/num']: ((q t) = ((~ (b t)) & ((a t) | (q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))) & ((![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: ((q ('const/arithmetic/+' t1 t2)) => ((a ('const/arithmetic/+' t1 t2)) | (b ('const/arithmetic/+' t1 t2)))))) & (Phi q)))))))).
tt('thm/Omega_Automata/BUECHI_TRANSLATION_e8', ax, (![b : ('type/num/num' > $o), a : ('type/num/num' > $o), Phi : (('type/num/num' > $o) > $o)]: ((Phi ('const/Temporal_Logic/BEFORE' a b)) = (?[q : ('type/num/num' > $o)]: ($true & ((![t : 'type/num/num']: ((q t) = ((~ (b t)) & ((a t) | (q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))) & ((![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: ((~ (q ('const/arithmetic/+' t1 t2))) => ((a ('const/arithmetic/+' t1 t2)) | (b ('const/arithmetic/+' t1 t2)))))) & (Phi q)))))))).
tt('thm/Omega_Automata/CO_BUECHI_CONJ_CLOSURE_', ax, ![B2 : $t, A : $t, B1 : $t]: (![t0 : 'type/num/num', i : ('type/num/num' > A), Psi2 : (('type/pair/prod' A B2) > $o), Psi1 : (('type/pair/prod' A B1) > $o), Phi_R2 : (('type/pair/prod' A B2) > $o), Phi_R1 : (('type/pair/prod' A B1) > $o), Phi_I2 : (B2 > $o), Phi_I1 : (B1 > $o)]: (((?[q1 : ('type/num/num' > B1)]: ((Phi_I1 (q1 t0)) & ((![t : 'type/num/num']: (Phi_R1 (('const/pair/,' A B1) (i ('const/arithmetic/+' t t0)) (q1 ('const/arithmetic/+' t t0))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (Psi1 (('const/pair/,' A B1) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) (q1 ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))))))) & (?[q2 : ('type/num/num' > B2)]: ((Phi_I2 (q2 t0)) & ((![t : 'type/num/num']: (Phi_R2 (('const/pair/,' A B2) (i ('const/arithmetic/+' t t0)) (q2 ('const/arithmetic/+' t t0))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (Psi2 (('const/pair/,' A B2) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) (q2 ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))))))))) = (?[q1 : ('type/num/num' > B1), q2 : ('type/num/num' > B2)]: (((Phi_I1 (q1 t0)) & (Phi_I2 (q2 t0))) & ((![t : 'type/num/num']: ((Phi_R1 (('const/pair/,' A B1) (i ('const/arithmetic/+' t t0)) (q1 ('const/arithmetic/+' t t0)))) & (Phi_R2 (('const/pair/,' A B2) (i ('const/arithmetic/+' t t0)) (q2 ('const/arithmetic/+' t t0)))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: ((Psi1 (('const/pair/,' A B1) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) (q1 ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))) & (Psi2 (('const/pair/,' A B2) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) (q2 ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))))))))))).
tt('thm/Omega_Automata/CO_BUECHI_DISJ_CLOSURE_', ax, ![B2 : $t, A : $t, B1 : $t]: (![t0 : 'type/num/num', t : 'type/num/num', i : ('type/num/num' > A), Psi2 : (('type/pair/prod' A B2) > $o), Psi1 : (('type/pair/prod' A B1) > $o), Phi_R2 : (('type/pair/prod' A B2) > $o), Phi_R1 : (('type/pair/prod' A B1) > $o), Phi_I2 : (B2 > $o), Phi_I1 : (B1 > $o)]: (((?[q1 : ('type/num/num' > B1)]: ((Phi_I1 (q1 t0)) & ((![t1 : 'type/num/num']: (Phi_R1 (('const/pair/,' A B1) (i ('const/arithmetic/+' t1 t0)) (q1 ('const/arithmetic/+' t1 t0))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (Psi1 (('const/pair/,' A B1) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) (q1 ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))))))) | (?[q2 : ('type/num/num' > B2)]: ((Phi_I2 (q2 t0)) & ((![t1 : 'type/num/num']: (Phi_R2 (('const/pair/,' A B2) (i ('const/arithmetic/+' t1 t0)) (q2 ('const/arithmetic/+' t1 t0))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (Psi2 (('const/pair/,' A B2) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) (q2 ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))))))))) = (?[p : ('type/num/num' > $o), q1 : ('type/num/num' > B1), q2 : ('type/num/num' > B2)]: ((((~ (p t0)) & (Phi_I1 (q1 t0))) | ((p t0) & (Phi_I2 (q2 t0)))) & ((![t1 : 'type/num/num']: (((~ (p ('const/arithmetic/+' t1 t0))) & ((Phi_R1 (('const/pair/,' A B1) (i ('const/arithmetic/+' t1 t0)) (q1 ('const/arithmetic/+' t1 t0)))) & (~ (p ('const/arithmetic/+' t1 ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))) | ((p ('const/arithmetic/+' t1 t0)) & ((Phi_R2 (('const/pair/,' A B2) (i ('const/arithmetic/+' t1 t0)) (q2 ('const/arithmetic/+' t1 t0)))) & (p ('const/arithmetic/+' t1 ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (((~ (p ('const/arithmetic/+' t t0))) & (Psi1 (('const/pair/,' A B1) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) (q1 ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))) | ((p ('const/arithmetic/+' t t0)) & (Psi2 (('const/pair/,' A B2) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) (q2 ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))))))))))))).
tt('thm/Omega_Automata/CO_BUECHI_NEXT_CLOSURE_', ax, ![B : $t, A : $t]: (![t0 : 'type/num/num', i : ('type/num/num' > A), c : B, Psi : (('type/pair/prod' A B) > $o), Phi_R : (('type/pair/prod' A B) > $o), Phi_I : (B > $o)]: (('const/Temporal_Logic/NEXT' (^[t00 : 'type/num/num']: (?[q : ('type/num/num' > B)]: ((Phi_I (q t00)) & ((![t : 'type/num/num']: (Phi_R (('const/pair/,' A B) (i ('const/arithmetic/+' t t00)) (q ('const/arithmetic/+' t t00))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (Psi (('const/pair/,' A B) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t00))) (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t00))))))))))) t0) = (?[p : ('type/num/num' > $o), q : ('type/num/num' > B)]: ((((p t0) = $false) & ((q t0) = c)) & ((![t : 'type/num/num']: (((~ (p ('const/arithmetic/+' t t0))) & (((q ('const/arithmetic/+' t t0)) = c) & ((p ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & (Phi_I (q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))) | ((p ('const/arithmetic/+' t t0)) & ((Phi_R (('const/pair/,' A B) (i ('const/arithmetic/+' t t0)) (q ('const/arithmetic/+' t t0)))) & (p ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (Psi (('const/pair/,' A B) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))))))))))).
tt('thm/Omega_Automata/CO_BUECHI_SUNTIL_CLOSURE_', ax, ![B : $t, A : $t]: (![t0 : 'type/num/num', phi : ('type/num/num' > $o), i : ('type/num/num' > A), c : B, Psi : (('type/pair/prod' A B) > $o), Phi_R : (('type/pair/prod' A B) > $o), Phi_I : (B > $o)]: (('const/Temporal_Logic/SUNTIL' phi (^[t00 : 'type/num/num']: (?[q : ('type/num/num' > B)]: ((Phi_I (q t00)) & ((![t : 'type/num/num']: (Phi_R (('const/pair/,' A B) (i ('const/arithmetic/+' t t00)) (q ('const/arithmetic/+' t t00))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (Psi (('const/pair/,' A B) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t00))) (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t00))))))))))) t0) = (?[p : ('type/num/num' > $o), q : ('type/num/num' > B)]: ((('const/bool/COND' $o) (p t0) (Phi_I (q t0)) ((q t0) = c)) & ((![t : 'type/num/num']: (((~ (p ('const/arithmetic/+' t t0))) & (((q ('const/arithmetic/+' t t0)) = c) & ((phi ('const/arithmetic/+' t t0)) & ((~ (p ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) & ((q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = c))))) | (((~ (p ('const/arithmetic/+' t t0))) & (((q ('const/arithmetic/+' t t0)) = c) & ((phi ('const/arithmetic/+' t t0)) & ((p ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & (Phi_I (q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))) | ((p ('const/arithmetic/+' t t0)) & ((Phi_R (('const/pair/,' A B) (i ('const/arithmetic/+' t t0)) (q ('const/arithmetic/+' t t0)))) & (p ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: ((p ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) & (Psi (('const/pair/,' A B) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))))))))))).
tt('thm/Omega_Automata/CO_BUECHI_UNTIL_CLOSURE_', ax, ![B : $t, A : $t]: (![t0 : 'type/num/num', phi : ('type/num/num' > $o), i : ('type/num/num' > A), c : B, Psi : (('type/pair/prod' A B) > $o), Phi_R : (('type/pair/prod' A B) > $o), Phi_I : (B > $o)]: (('const/Temporal_Logic/UNTIL' phi (^[t00 : 'type/num/num']: (?[q : ('type/num/num' > B)]: ((Phi_I (q t00)) & ((![t : 'type/num/num']: (Phi_R (('const/pair/,' A B) (i ('const/arithmetic/+' t t00)) (q ('const/arithmetic/+' t t00))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (Psi (('const/pair/,' A B) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t00))) (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t00))))))))))) t0) = (?[p : ('type/num/num' > $o), q : ('type/num/num' > B)]: ((('const/bool/COND' $o) (p t0) (Phi_I (q t0)) ((q t0) = c)) & ((![t : 'type/num/num']: (((~ (p ('const/arithmetic/+' t t0))) & (((q ('const/arithmetic/+' t t0)) = c) & ((phi ('const/arithmetic/+' t t0)) & ((~ (p ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) & ((q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = c))))) | (((~ (p ('const/arithmetic/+' t t0))) & (((q ('const/arithmetic/+' t t0)) = c) & ((phi ('const/arithmetic/+' t t0)) & ((p ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & (Phi_I (q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))) | ((p ('const/arithmetic/+' t t0)) & ((Phi_R (('const/pair/,' A B) (i ('const/arithmetic/+' t t0)) (q ('const/arithmetic/+' t t0)))) & (p ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: ((~ (p ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))) | (Psi (('const/pair/,' A B) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))))))))))).
tt('thm/Omega_Automata/CO_BUECHI_SBEFORE_CLOSURE_', ax, ![B : $t, A : $t]: (![t0 : 'type/num/num', phi : ('type/num/num' > $o), i : ('type/num/num' > A), c : B, Psi : (('type/pair/prod' A B) > $o), Phi_R : (('type/pair/prod' A B) > $o), Phi_I : (B > $o)]: (('const/Temporal_Logic/SBEFORE' (^[t00 : 'type/num/num']: (?[q : ('type/num/num' > B)]: ((Phi_I (q t00)) & ((![t : 'type/num/num']: (Phi_R (('const/pair/,' A B) (i ('const/arithmetic/+' t t00)) (q ('const/arithmetic/+' t t00))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (Psi (('const/pair/,' A B) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t00))) (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t00))))))))))) phi t0) = (?[p1 : ('type/num/num' > $o), p2 : ('type/num/num' > $o), q : ('type/num/num' > B)]: ((((~ (p1 t0)) & ((~ (p2 t0)) & ((q t0) = c))) | ((p1 t0) & ((~ (p2 t0)) & (Phi_I (q t0))))) & ((![t : 'type/num/num']: (((~ (p1 ('const/arithmetic/+' t t0))) & ((~ (p2 ('const/arithmetic/+' t t0))) & (((q ('const/arithmetic/+' t t0)) = c) & ((~ (phi ('const/arithmetic/+' t t0))) & ((~ (p1 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) & ((~ (p2 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) & ((q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = c))))))) | (((~ (p1 ('const/arithmetic/+' t t0))) & ((~ (p2 ('const/arithmetic/+' t t0))) & (((q ('const/arithmetic/+' t t0)) = c) & ((~ (phi ('const/arithmetic/+' t t0))) & ((p1 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & ((~ (p2 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) & (Phi_I (q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))))) | (((p1 ('const/arithmetic/+' t t0)) & ((~ (p2 ('const/arithmetic/+' t t0))) & ((~ (phi ('const/arithmetic/+' t t0))) & ((Phi_I (q ('const/arithmetic/+' t t0))) & ((Phi_R (('const/pair/,' A B) (i ('const/arithmetic/+' t t0)) (q ('const/arithmetic/+' t t0)))) & ((p1 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & (p2 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))) | ((p1 ('const/arithmetic/+' t t0)) & ((p2 ('const/arithmetic/+' t t0)) & ((Phi_R (('const/pair/,' A B) (i ('const/arithmetic/+' t t0)) (q ('const/arithmetic/+' t t0)))) & ((p1 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & (p2 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: ((p1 ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) & (Psi (('const/pair/,' A B) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))))))))))).
tt('thm/Omega_Automata/CO_BUECHI_BEFORE_CLOSURE_', ax, ![B : $t, A : $t]: (![t0 : 'type/num/num', phi : ('type/num/num' > $o), i : ('type/num/num' > A), c : B, Psi : (('type/pair/prod' A B) > $o), Phi_R : (('type/pair/prod' A B) > $o), Phi_I : (B > $o)]: (('const/Temporal_Logic/BEFORE' (^[t00 : 'type/num/num']: (?[q : ('type/num/num' > B)]: ((Phi_I (q t00)) & ((![t : 'type/num/num']: (Phi_R (('const/pair/,' A B) (i ('const/arithmetic/+' t t00)) (q ('const/arithmetic/+' t t00))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (Psi (('const/pair/,' A B) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t00))) (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t00))))))))))) phi t0) = (?[p1 : ('type/num/num' > $o), p2 : ('type/num/num' > $o), q : ('type/num/num' > B)]: ((((~ (p1 t0)) & ((~ (p2 t0)) & ((q t0) = c))) | ((p1 t0) & ((~ (p2 t0)) & (Phi_I (q t0))))) & ((![t : 'type/num/num']: (((~ (p1 ('const/arithmetic/+' t t0))) & ((~ (p2 ('const/arithmetic/+' t t0))) & (((q ('const/arithmetic/+' t t0)) = c) & ((~ (phi ('const/arithmetic/+' t t0))) & ((~ (p1 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) & ((~ (p2 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) & ((q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = c))))))) | (((~ (p1 ('const/arithmetic/+' t t0))) & ((~ (p2 ('const/arithmetic/+' t t0))) & (((q ('const/arithmetic/+' t t0)) = c) & ((~ (phi ('const/arithmetic/+' t t0))) & ((p1 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & ((~ (p2 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) & (Phi_I (q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))))) | (((p1 ('const/arithmetic/+' t t0)) & ((~ (p2 ('const/arithmetic/+' t t0))) & ((~ (phi ('const/arithmetic/+' t t0))) & ((Phi_I (q ('const/arithmetic/+' t t0))) & ((Phi_R (('const/pair/,' A B) (i ('const/arithmetic/+' t t0)) (q ('const/arithmetic/+' t t0)))) & ((p1 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & (p2 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))) | ((p1 ('const/arithmetic/+' t t0)) & ((p2 ('const/arithmetic/+' t t0)) & ((Phi_R (('const/pair/,' A B) (i ('const/arithmetic/+' t t0)) (q ('const/arithmetic/+' t t0)))) & ((p1 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & (p2 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: ((~ (p1 ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))) | (Psi (('const/pair/,' A B) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))))))))))).
tt('thm/Omega_Automata/CO_BUECHI_SWHEN_CLOSURE_', ax, ![B : $t, A : $t]: (![t0 : 'type/num/num', phi : ('type/num/num' > $o), i : ('type/num/num' > A), c : B, Psi : (('type/pair/prod' A B) > $o), Phi_R : (('type/pair/prod' A B) > $o), Phi_I : (B > $o)]: (('const/Temporal_Logic/SWHEN' (^[t00 : 'type/num/num']: (?[q : ('type/num/num' > B)]: ((Phi_I (q t00)) & ((![t : 'type/num/num']: (Phi_R (('const/pair/,' A B) (i ('const/arithmetic/+' t t00)) (q ('const/arithmetic/+' t t00))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (Psi (('const/pair/,' A B) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t00))) (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t00))))))))))) phi t0) = (?[p1 : ('type/num/num' > $o), p2 : ('type/num/num' > $o), q : ('type/num/num' > B)]: ((((~ (p1 t0)) & ((~ (p2 t0)) & ((q t0) = c))) | ((p1 t0) & ((~ (p2 t0)) & (Phi_I (q t0))))) & ((![t : 'type/num/num']: (((~ (p1 ('const/arithmetic/+' t t0))) & ((~ (p2 ('const/arithmetic/+' t t0))) & (((q ('const/arithmetic/+' t t0)) = c) & ((~ (phi ('const/arithmetic/+' t t0))) & ((~ (p1 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) & ((~ (p2 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) & ((q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = c))))))) | (((~ (p1 ('const/arithmetic/+' t t0))) & ((~ (p2 ('const/arithmetic/+' t t0))) & (((q ('const/arithmetic/+' t t0)) = c) & ((~ (phi ('const/arithmetic/+' t t0))) & ((p1 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & ((~ (p2 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) & (Phi_I (q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))))) | (((p1 ('const/arithmetic/+' t t0)) & ((~ (p2 ('const/arithmetic/+' t t0))) & ((phi ('const/arithmetic/+' t t0)) & ((Phi_I (q ('const/arithmetic/+' t t0))) & ((Phi_R (('const/pair/,' A B) (i ('const/arithmetic/+' t t0)) (q ('const/arithmetic/+' t t0)))) & ((p1 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & (p2 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))) | ((p1 ('const/arithmetic/+' t t0)) & ((p2 ('const/arithmetic/+' t t0)) & ((Phi_R (('const/pair/,' A B) (i ('const/arithmetic/+' t t0)) (q ('const/arithmetic/+' t t0)))) & ((p1 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & (p2 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: ((p1 ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) & (Psi (('const/pair/,' A B) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))))))))))).
tt('thm/Omega_Automata/CO_BUECHI_WHEN_CLOSURE_', ax, ![B : $t, A : $t]: (![t0 : 'type/num/num', phi : ('type/num/num' > $o), i : ('type/num/num' > A), c : B, Psi : (('type/pair/prod' A B) > $o), Phi_R : (('type/pair/prod' A B) > $o), Phi_I : (B > $o)]: (('const/Temporal_Logic/WHEN' (^[t00 : 'type/num/num']: (?[q : ('type/num/num' > B)]: ((Phi_I (q t00)) & ((![t : 'type/num/num']: (Phi_R (('const/pair/,' A B) (i ('const/arithmetic/+' t t00)) (q ('const/arithmetic/+' t t00))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (Psi (('const/pair/,' A B) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t00))) (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t00))))))))))) phi t0) = (?[p1 : ('type/num/num' > $o), p2 : ('type/num/num' > $o), q : ('type/num/num' > B)]: ((((~ (p1 t0)) & ((~ (p2 t0)) & ((q t0) = c))) | ((p1 t0) & ((~ (p2 t0)) & (Phi_I (q t0))))) & ((![t : 'type/num/num']: (((~ (p1 ('const/arithmetic/+' t t0))) & ((~ (p2 ('const/arithmetic/+' t t0))) & (((q ('const/arithmetic/+' t t0)) = c) & ((~ (phi ('const/arithmetic/+' t t0))) & ((~ (p1 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) & ((~ (p2 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) & ((q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) = c))))))) | (((~ (p1 ('const/arithmetic/+' t t0))) & ((~ (p2 ('const/arithmetic/+' t t0))) & (((q ('const/arithmetic/+' t t0)) = c) & ((~ (phi ('const/arithmetic/+' t t0))) & ((p1 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & ((~ (p2 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))) & (Phi_I (q ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))))))) | (((p1 ('const/arithmetic/+' t t0)) & ((~ (p2 ('const/arithmetic/+' t t0))) & ((phi ('const/arithmetic/+' t t0)) & ((Phi_I (q ('const/arithmetic/+' t t0))) & ((Phi_R (('const/pair/,' A B) (i ('const/arithmetic/+' t t0)) (q ('const/arithmetic/+' t t0)))) & ((p1 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & (p2 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))) | ((p1 ('const/arithmetic/+' t t0)) & ((p2 ('const/arithmetic/+' t t0)) & ((Phi_R (('const/pair/,' A B) (i ('const/arithmetic/+' t t0)) (q ('const/arithmetic/+' t t0)))) & ((p1 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))) & (p2 ('const/arithmetic/+' t ('const/arithmetic/+' t0 ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: ((~ (p1 ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))) | (Psi (('const/pair/,' A B) (i ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))) (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))))))))))).
tt('thm/Omega_Automata/NEXT_AS_CO_BUECHI_', ax, (![t0 : 'type/num/num', a : ('type/num/num' > $o)]: (('const/Temporal_Logic/NEXT' a t0) = (?[p : ('type/num/num' > $o), q : ('type/num/num' > $o)]: (((~ (p t0)) & (~ (q t0))) & ((![t : 'type/num/num']: (((~ (p ('const/arithmetic/+' t t0))) & ((~ (q ('const/arithmetic/+' t t0))) & ((p ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0))) & (~ (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0))))))) | (((p ('const/arithmetic/+' t t0)) & ((~ (q ('const/arithmetic/+' t t0))) & ((a ('const/arithmetic/+' t t0)) & ((p ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0))) & (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0))))))) | ((p ('const/arithmetic/+' t t0)) & ((q ('const/arithmetic/+' t t0)) & ((p ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0))) & (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0))))))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))))))))).
tt('thm/Omega_Automata/SUNTIL_AS_CO_BUECHI_', ax, (![t0 : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SUNTIL' a b t0) = (?[q : ('type/num/num' > $o)]: ((~ (q t0)) & ((![t : 'type/num/num']: (((~ (q ('const/arithmetic/+' t t0))) & ((a ('const/arithmetic/+' t t0)) & ((~ (b ('const/arithmetic/+' t t0))) & (~ (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0))))))) | (((~ (q ('const/arithmetic/+' t t0))) & ((b ('const/arithmetic/+' t t0)) & (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0))))) | ((q ('const/arithmetic/+' t t0)) & (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0))))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))))))))).
tt('thm/Omega_Automata/UNTIL_AS_CO_BUECHI_', ax, (![t0 : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/UNTIL' a b t0) = (?[q : ('type/num/num' > $o)]: ((~ (q t0)) & ((![t : 'type/num/num']: (((~ (q ('const/arithmetic/+' t t0))) & ((a ('const/arithmetic/+' t t0)) & ((~ (b ('const/arithmetic/+' t t0))) & (~ (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0))))))) | (((~ (q ('const/arithmetic/+' t t0))) & ((b ('const/arithmetic/+' t t0)) & (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0))))) | ((q ('const/arithmetic/+' t t0)) & (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0))))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: ((~ (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))) | (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))))))))).
tt('thm/Omega_Automata/SBEFORE_AS_CO_BUECHI_', ax, (![t0 : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SBEFORE' a b t0) = (?[q : ('type/num/num' > $o)]: ((~ (q t0)) & ((![t : 'type/num/num']: (((~ (q ('const/arithmetic/+' t t0))) & ((~ (a ('const/arithmetic/+' t t0))) & ((~ (b ('const/arithmetic/+' t t0))) & (~ (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0))))))) | (((~ (q ('const/arithmetic/+' t t0))) & ((a ('const/arithmetic/+' t t0)) & ((~ (b ('const/arithmetic/+' t t0))) & (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0)))))) | ((q ('const/arithmetic/+' t t0)) & (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0))))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))))))))).
tt('thm/Omega_Automata/BEFORE_AS_CO_BUECHI_', ax, (![t0 : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/BEFORE' a b t0) = (?[q : ('type/num/num' > $o)]: ((~ (q t0)) & ((![t : 'type/num/num']: (((~ (q ('const/arithmetic/+' t t0))) & ((~ (a ('const/arithmetic/+' t t0))) & ((~ (b ('const/arithmetic/+' t t0))) & (~ (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0))))))) | (((~ (q ('const/arithmetic/+' t t0))) & ((a ('const/arithmetic/+' t t0)) & ((~ (b ('const/arithmetic/+' t t0))) & (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0)))))) | ((q ('const/arithmetic/+' t t0)) & (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0))))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: ((~ (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))) | (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))))))))).
tt('thm/Omega_Automata/SWHEN_AS_CO_BUECHI_', ax, (![t0 : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/SWHEN' a b t0) = (?[q : ('type/num/num' > $o)]: ((~ (q t0)) & ((![t : 'type/num/num']: (((~ (q ('const/arithmetic/+' t t0))) & ((~ (b ('const/arithmetic/+' t t0))) & (~ (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0)))))) | (((~ (q ('const/arithmetic/+' t t0))) & ((a ('const/arithmetic/+' t t0)) & ((b ('const/arithmetic/+' t t0)) & (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0)))))) | ((q ('const/arithmetic/+' t t0)) & (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0))))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0))))))))))).
tt('thm/Omega_Automata/WHEN_AS_CO_BUECHI_', ax, (![t0 : 'type/num/num', b : ('type/num/num' > $o), a : ('type/num/num' > $o)]: (('const/Temporal_Logic/WHEN' a b t0) = (?[q : ('type/num/num' > $o)]: ((~ (q t0)) & ((![t : 'type/num/num']: (((~ (q ('const/arithmetic/+' t t0))) & ((~ (b ('const/arithmetic/+' t t0))) & (~ (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0)))))) | (((~ (q ('const/arithmetic/+' t t0))) & ((a ('const/arithmetic/+' t t0)) & ((b ('const/arithmetic/+' t t0)) & (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0)))))) | ((q ('const/arithmetic/+' t t0)) & (q ('const/arithmetic/+' t ('const/arithmetic/+' ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')) t0))))))) & (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: ((~ (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))) | (q ('const/arithmetic/+' t1 ('const/arithmetic/+' t2 t0)))))))))))).
tt('thm/Omega_Automata/BUECHI_PERIODIC_MODEL_', ax, ![STATE : $t, A : $t]: (![TransRel : (('type/pair/prod' A ('type/pair/prod' STATE STATE)) > $o), InitState : (STATE > $o), Accept : (STATE > $o)]: ((![s : ('type/num/num' > STATE)]: (?[x0 : 'type/num/num', l : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' l) & ((s x0) = (s ('const/arithmetic/+' x0 l)))))) => ((?[i : ('type/num/num' > A), q : ('type/num/num' > STATE)]: ((InitState (q 'const/num/0')) & ((![t : 'type/num/num']: (TransRel (('const/pair/,' A ('type/pair/prod' STATE STATE)) (i t) (('const/pair/,' STATE STATE) (q t) (q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))) & (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: (Accept (q ('const/arithmetic/+' t1 t2)))))))) = (?[x0 : 'type/num/num', l : 'type/num/num', j : ('type/num/num' > A), p : ('type/num/num' > STATE)]: (('const/prim_rec/<' 'const/num/0' l) & ((![t2 : 'type/num/num']: ((j ('const/arithmetic/+' x0 t2)) = (j ('const/arithmetic/+' x0 ('const/arithmetic/MOD' t2 l))))) & ((![t2 : 'type/num/num']: ((p ('const/arithmetic/+' x0 t2)) = (p ('const/arithmetic/+' x0 ('const/arithmetic/MOD' t2 l))))) & ((InitState (p 'const/num/0')) & ((![t : 'type/num/num']: (TransRel (('const/pair/,' A ('type/pair/prod' STATE STATE)) (j t) (('const/pair/,' STATE STATE) (p t) (p ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))) & (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: (Accept (p ('const/arithmetic/+' t1 t2))))))))))))))).
tt('thm/Omega_Automata/BUECHI_PERIODIC_REDUCTION_THM_', ax, ![STATE : $t, A : $t]: (![TransRel : (('type/pair/prod' A ('type/pair/prod' STATE STATE)) > $o), InitState : (STATE > $o), Accept : (STATE > $o)]: ((![s : ('type/num/num' > STATE)]: (?[x0 : 'type/num/num', l : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' l) & ((s x0) = (s ('const/arithmetic/+' x0 l)))))) => ((?[i : ('type/num/num' > A), q : ('type/num/num' > STATE)]: ((InitState (q 'const/num/0')) & ((![t : 'type/num/num']: (TransRel (('const/pair/,' A ('type/pair/prod' STATE STATE)) (i t) (('const/pair/,' STATE STATE) (q t) (q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))) & (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: (Accept (q ('const/arithmetic/+' t1 t2)))))))) = (?[x0 : 'type/num/num', l : 'type/num/num', j : ('type/num/num' > A), p : ('type/num/num' > STATE)]: (('const/prim_rec/<' 'const/num/0' l) & ((![t2 : 'type/num/num']: ((j ('const/arithmetic/+' x0 t2)) = (j ('const/arithmetic/+' x0 ('const/arithmetic/MOD' t2 l))))) & ((![t2 : 'type/num/num']: ((p ('const/arithmetic/+' x0 t2)) = (p ('const/arithmetic/+' x0 ('const/arithmetic/MOD' t2 l))))) & ((InitState (p 'const/num/0')) & ((![t : 'type/num/num']: (('const/prim_rec/<' t ('const/arithmetic/+' x0 l)) => (TransRel (('const/pair/,' A ('type/pair/prod' STATE STATE)) (j t) (('const/pair/,' STATE STATE) (p t) (p ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))) & (?[t : 'type/num/num']: (('const/prim_rec/<' t l) & (Accept (p ('const/arithmetic/+' x0 t))))))))))))))).
tt('thm/Omega_Automata/BUECHI_PROP_REDUCTION_', ax, ![STATE : $t, A : $t]: (![TransRel : (('type/pair/prod' A ('type/pair/prod' STATE STATE)) > $o), InitState : (STATE > $o), Accept : (STATE > $o)]: ((![s : ('type/num/num' > STATE)]: (?[x0 : 'type/num/num', l : 'type/num/num']: (('const/prim_rec/<' 'const/num/0' l) & ((s x0) = (s ('const/arithmetic/+' x0 l)))))) => ((?[i : ('type/num/num' > A), q : ('type/num/num' > STATE)]: ((InitState (q 'const/num/0')) & ((![t : 'type/num/num']: (TransRel (('const/pair/,' A ('type/pair/prod' STATE STATE)) (i t) (('const/pair/,' STATE STATE) (q t) (q ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO')))))))) & (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: (Accept (q ('const/arithmetic/+' t1 t2)))))))) = (?[x0 : 'type/num/num', l : 'type/num/num', j : ('type/num/num' > A), p : ('type/num/num' > STATE)]: (('const/prim_rec/<' 'const/num/0' l) & ((InitState (p 'const/num/0')) & ((![t : 'type/num/num']: (('const/prim_rec/<' t ('const/arithmetic/+' x0 l)) => (TransRel (('const/pair/,' A ('type/pair/prod' STATE STATE)) (j t) (('const/pair/,' STATE STATE) (p t) (p ('const/arithmetic/+' t ('const/arithmetic/NUMERAL' ('const/arithmetic/BIT1' 'const/arithmetic/ZERO'))))))))) & ((?[t : 'type/num/num']: (('const/prim_rec/<' t l) & (Accept (p ('const/arithmetic/+' x0 t))))) & ((p x0) = (p ('const/arithmetic/+' x0 l)))))))))))).
tt('thm/Omega_Automata/EQUALITY_THM_', ax, ![A : $t]: (![x : A, y : A]: ((x = y) = (![P : (A > $o)]: ((P x) = (P y)))))).
tt('thm/Omega_Automata/LESS_THM_', ax, (![x : 'type/num/num', y : 'type/num/num']: (('const/prim_rec/<' x y) = (?[P : ('type/num/num' > $o)]: ((P x) & ((~ (P y)) & (![z : 'type/num/num']: ((P ('const/num/SUC' z)) => (P z))))))))).
tt('thm/Omega_Automata/FORALL_EXISTS_THM_', ax, (![P : ('type/num/num' > $o)]: ((![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: (P ('const/arithmetic/+' t1 t2)))) = (![t1 : 'type/num/num']: (?[t2 : 'type/num/num']: (('const/prim_rec/<' t1 t2) & (P t2))))))).
tt('thm/Omega_Automata/EXISTS_FORALL_THM_', ax, (![P : ('type/num/num' > $o)]: ((?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (P ('const/arithmetic/+' t1 t2)))) = (?[t1 : 'type/num/num']: (![t2 : 'type/num/num']: (('const/prim_rec/<' t1 t2) => (P t2))))))).
tt('thm/Omega_Automata/ELGOT_LEMMA_', ax, ![A : $t]: (![PHI : ((A > $o) > (A > $o))]: ((?[x : A]: (![p : (A > $o)]: (PHI p x))) = (?[q : (A > $o)]: ((![x : A]: ((q x) => (![p : (A > $o)]: (PHI p x)))) & (?[z : A]: (q z))))))).
tt('thm/Omega_Automata/ELGOT1_THM_', ax, ![A : $t]: (![PHI : ((A > $o) > (A > $o))]: ((?[x : A]: (![p : (A > $o)]: (PHI p x))) = (?[q : (A > $o)]: (![p : (A > $o), x : A]: (?[z : A]: (((q x) => (PHI p x)) & (q z)))))))).
tt('thm/Omega_Automata/ELGOT2_THM_', ax, ![A : $t]: (![PHI : ((A > $o) > (A > $o))]: ((![x : A]: (?[p : (A > $o)]: (PHI p x))) = (![q : (A > $o)]: (?[p : (A > $o), x : A]: (![z : A]: ((q z) => ((PHI p x) & (q x))))))))).
