let V be LTLModelStr ; :: thesis: for Kai being Function of atomic_LTL ,the BasicAssign of V
for f being Function of LTL_WFF ,the Assignations of V holds f is-PreEvaluation-for 0 ,Kai
let Kai be Function of atomic_LTL ,the BasicAssign of V; :: thesis: for f being Function of LTL_WFF ,the Assignations of V holds f is-PreEvaluation-for 0 ,Kai
let f be Function of LTL_WFF ,the Assignations of V; :: thesis: f is-PreEvaluation-for 0 ,Kai
for H being LTL-formula st len H <= 0 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 disjunctive implies f . H = the Or 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)) ) ) by Thlen01;
hence f is-PreEvaluation-for 0 ,Kai by Def27; :: thesis: verum