:: deftheorem Def34 defines Evaluate MODELC_1:def 34 :
for V being CTLModel
for Kai being Function of atomic_WFF, the BasicAssign of V
for H being CTL-formula
for b₄ being Assign of V holds
( b₄ = Evaluate (H,Kai) iff ex f being Function of CTL_WFF, the carrier of V st
( f is-Evaluation-for Kai & b₄ = f . H ) );