let n be Element of NAT ; :: thesis: for V being CTLModelStr
for Kai being Function of atomic_WFF ,the BasicAssign of V
for f being Function of CTL_WFF ,the Assignations of V st f is-Evaluation-for Kai holds
f is-PreEvaluation-for n,Kai
let V be CTLModelStr ; :: thesis: for Kai being Function of atomic_WFF ,the BasicAssign of V
for f being Function of CTL_WFF ,the Assignations of V st f is-Evaluation-for Kai holds
f is-PreEvaluation-for n,Kai
let Kai be Function of atomic_WFF ,the BasicAssign of V; :: thesis: for f being Function of CTL_WFF ,the Assignations of V st f is-Evaluation-for Kai holds
f is-PreEvaluation-for n,Kai
let f be Function of CTL_WFF ,the Assignations of V; :: thesis: ( f is-Evaluation-for Kai implies f is-PreEvaluation-for n,Kai )
assume f is-Evaluation-for Kai ; :: thesis: f is-PreEvaluation-for n,Kai
then for H being CTL-formula st len H <= n holds
( ( H is atomic implies f . H = Kai . H ) & ( H is negative implies f . H = the Not of V . (f . (the_argument_of H)) ) & ( H is conjunctive implies f . H = the And of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) ) & ( H is ExistNext implies f . H = the EneXt of V . (f . (the_argument_of H)) ) & ( H is ExistGlobal implies f . H = the EGlobal of V . (f . (the_argument_of H)) ) & ( H is ExistUntill implies f . H = the EUntill of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) ) ) by Def26;
hence f is-PreEvaluation-for n,Kai by Def27; :: thesis: verum