:: deftheorem Def32 defines CastEval MODELC_1:def 32 :
for V being CTLModel
for v0 being Element of the carrier of V
for x being set holds
( ( x in Funcs (CTL_WFF, the carrier of V) implies CastEval (V,x,v0) = x ) & ( not x in Funcs (CTL_WFF, the carrier of V) implies CastEval (V,x,v0) = CTL_WFF --> v0 ) );