let V be LTLModel; for Kai being Function of atomic_LTL, the BasicAssign of V
for f being Function of LTL_WFF, the carrier of V st ( for n being Nat holds f is-PreEvaluation-for n,Kai ) holds
f is-Evaluation-for Kai
let Kai be Function of atomic_LTL, the BasicAssign of V; for f being Function of LTL_WFF, the carrier of V st ( for n being Nat holds f is-PreEvaluation-for n,Kai ) holds
f is-Evaluation-for Kai
let f be Function of LTL_WFF, the carrier of V; ( ( for n being Nat holds f is-PreEvaluation-for n,Kai ) implies f is-Evaluation-for Kai )
assume A1:
for n being Nat holds f is-PreEvaluation-for n,Kai
; f is-Evaluation-for Kai
let H be LTL-formula; MODELC_2:def 27 ( ( 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 disjunctive implies f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is next implies f . H = the NEXT of V . (f . (the_argument_of H)) ) & ( H is Until implies f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is Release implies f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) )
set n = len H;
f is-PreEvaluation-for len H,Kai
by A1;
hence
( ( 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 disjunctive implies f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is next implies f . H = the NEXT of V . (f . (the_argument_of H)) ) & ( H is Until implies f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) & ( H is Release implies f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ) )
; verum