let n be Nat; :: thesis: for V being LTLModel
for Kai being Function of atomic_LTL, the BasicAssign of V
for f being Function of LTL_WFF, the carrier of V st f is-PreEvaluation-for n + 1,Kai holds
f is-PreEvaluation-for n,Kai
let V be LTLModel; :: thesis: for Kai being Function of atomic_LTL, the BasicAssign of V
for f being Function of LTL_WFF, the carrier of V st f is-PreEvaluation-for n + 1,Kai holds
f is-PreEvaluation-for n,Kai
let Kai be Function of atomic_LTL, the BasicAssign of V; :: thesis: for f being Function of LTL_WFF, the carrier of V st f is-PreEvaluation-for n + 1,Kai holds
f is-PreEvaluation-for n,Kai
let f be Function of LTL_WFF, the carrier of V; :: thesis: ( f is-PreEvaluation-for n + 1,Kai implies f is-PreEvaluation-for n,Kai )
assume A1: f is-PreEvaluation-for n + 1,Kai ; :: thesis: f is-PreEvaluation-for n,Kai
for H being LTL-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 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))) ) )

proof

let H be LTL-formula; :: thesis: ( len H <= n implies ( ( 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))) ) ) )
assume len H <= n ; :: thesis: ( ( 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))) ) )
then len H < n + 1 by NAT_1:13;
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))) ) ) by A1; :: thesis: verum

end;

hence f is-PreEvaluation-for n,Kai ; :: thesis: verum