:: deftheorem defines FinalS_LTL MODELC_3:def 46 :
for v being neg-inner-most LTL-formula holds FinalS_LTL v = { x where x is Element of bool (LTLStates v) : ex F being LTL-formula st
( F is_subformula_of v & F is Until & x = FinalS_LTL (F,v) ) } ;