let V be CTLModel; for Kai being Function of atomic_WFF, the BasicAssign of V
for f being Function of CTL_WFF, the carrier of V
for n being Nat st f is-PreEvaluation-for n + 1,Kai holds
f is-PreEvaluation-for n,Kai
let Kai be Function of atomic_WFF, the BasicAssign of V; for f being Function of CTL_WFF, the carrier of V
for n being Nat st f is-PreEvaluation-for n + 1,Kai holds
f is-PreEvaluation-for n,Kai
let f be Function of CTL_WFF, the carrier of V; for n being Nat st f is-PreEvaluation-for n + 1,Kai holds
f is-PreEvaluation-for n,Kai
let n be Nat; ( f is-PreEvaluation-for n + 1,Kai implies f is-PreEvaluation-for n,Kai )
assume A1:
f is-PreEvaluation-for n + 1,Kai
; f is-PreEvaluation-for n,Kai
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 Compl of V . (f . (the_argument_of H)) ) & ( H is conjunctive implies f . H = the L_meet 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))) ) )
hence
f is-PreEvaluation-for n,Kai
; verum