:: deftheorem Def28 defines GraftEval MODELC_1:def 28 :
for V being CTLModelStr
for Kai being Function of atomic_WFF, the BasicAssign of V
for f, h being Function of CTL_WFF, the carrier of V
for n being Nat
for H being CTL-formula holds
( ( len H > n + 1 implies GraftEval (V,Kai,f,h,n,H) = f . H ) & ( len H = n + 1 & H is atomic implies GraftEval (V,Kai,f,h,n,H) = Kai . H ) & ( len H = n + 1 & H is negative implies GraftEval (V,Kai,f,h,n,H) = the Compl of V . (h . (the_argument_of H)) ) & ( len H = n + 1 & H is conjunctive implies GraftEval (V,Kai,f,h,n,H) = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) & ( len H = n + 1 & H is ExistNext implies GraftEval (V,Kai,f,h,n,H) = the EneXt of V . (h . (the_argument_of H)) ) & ( len H = n + 1 & H is ExistGlobal implies GraftEval (V,Kai,f,h,n,H) = the EGlobal of V . (h . (the_argument_of H)) ) & ( len H = n + 1 & H is ExistUntill implies GraftEval (V,Kai,f,h,n,H) = the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) ) & ( len H < n + 1 implies GraftEval (V,Kai,f,h,n,H) = h . H ) & ( not len H > n + 1 & ( not len H = n + 1 or not H is atomic ) & ( not len H = n + 1 or not H is negative ) & ( not len H = n + 1 or not H is conjunctive ) & ( not len H = n + 1 or not H is ExistNext ) & ( not len H = n + 1 or not H is ExistGlobal ) & ( not len H = n + 1 or not H is ExistUntill ) & not len H < n + 1 implies GraftEval (V,Kai,f,h,n,H) = {} ) );