:: deftheorem Def33 defines CastEval MODELC_2:def 33 :
for V being LTLModel
for v0 being Element of the carrier of V
for x being set holds
( ( x in Funcs (LTL_WFF, the carrier of V) implies CastEval (V,x,v0) = x ) & ( not x in Funcs (LTL_WFF, the carrier of V) implies CastEval (V,x,v0) = LTL_WFF --> v0 ) );