:: deftheorem defines BAutomaton MODELC_3:def 47 :
for v being neg-inner-most LTL-formula holds BAutomaton v = BuchiAutomaton(# (LTLStates v),(Tran_LTL v),(InitS_LTL v),(FinalS_LTL v) #);