:: deftheorem defines FinalS_LTL MODELC_3:def 45 :
for v being neg-inner-most LTL-formula
for F being LTL-formula holds FinalS_LTL (F,v) = { x where x is Element of LTLStates v : ( not F in the LTLold of (CastNode (x,v)) or the_right_argument_of F in the LTLold of (CastNode (x,v)) ) } ;