let V be LTLModel; :: thesis: for Kai being Function of atomic_LTL, the BasicAssign of V
for n being Nat ex f being Function of LTL_WFF, the carrier of V st f is-PreEvaluation-for n,Kai
let Kai be Function of atomic_LTL, the BasicAssign of V; :: thesis: for n being Nat ex f being Function of LTL_WFF, the carrier of V st f is-PreEvaluation-for n,Kai
defpred S₁[ Nat] means ex f being Function of LTL_WFF, the carrier of V st f is-PreEvaluation-for $1,Kai;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then consider h being Function of LTL_WFF, the carrier of V such that
A2: h is-PreEvaluation-for k,Kai ;
S₁[k + 1]

proof

deffunc H₁( object ) -> set = GraftEval (V,Kai,h,h,k,(CastLTL $1));
A3: for H being object st H in LTL_WFF holds
H₁(H) in the carrier of V

proof

let H be object ; :: thesis: ( H in LTL_WFF implies H₁(H) in the carrier of V )
assume A4: H in LTL_WFF ; :: thesis: H₁(H) in the carrier of V
reconsider H = H as LTL-formula by A4, Th1;
A5: H₁(H) = GraftEval (V,Kai,h,h,k,H) by A4, Def25;

per cases ( len H > k + 1 or ( len H = k + 1 & H is atomic ) or ( len H = k + 1 & H is negative ) or ( len H = k + 1 & H is conjunctive ) or ( len H = k + 1 & H is disjunctive ) or ( len H = k + 1 & H is next ) or ( len H = k + 1 & H is Until ) or ( len H = k + 1 & H is Release ) or len H < k + 1 ) by Th2, XXREAL_0:1;

suppose len H > k + 1 ; :: thesis: H₁(H) in the carrier of V

then GraftEval (V,Kai,h,h,k,H) = h . H by Def29;
hence H₁(H) in the carrier of V by A4, A5, FUNCT_2:5; :: thesis: verum

end;

suppose A6: ( len H = k + 1 & H is atomic ) ; :: thesis: H₁(H) in the carrier of V

then H in atomic_LTL ;
then Kai . H in the BasicAssign of V by FUNCT_2:5;
then Kai . H in the carrier of V ;
hence H₁(H) in the carrier of V by A5, A6, Def29; :: thesis: verum

end;

suppose A7: ( len H = k + 1 & H is negative ) ; :: thesis: H₁(H) in the carrier of V

the_argument_of H in LTL_WFF by Th1;
then A8: h . (the_argument_of H) in the carrier of V by FUNCT_2:5;
GraftEval (V,Kai,h,h,k,H) = the Compl of V . (h . (the_argument_of H)) by A7, Def29;
hence H₁(H) in the carrier of V by A5, A8, FUNCT_2:5; :: thesis: verum

end;

suppose ( len H = k + 1 & H is conjunctive ) ; :: thesis: H₁(H) in the carrier of V

then A9: GraftEval (V,Kai,h,h,k,H) = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) by Def29;
the_right_argument_of H in LTL_WFF by Th1;
then A10: h . (the_right_argument_of H) in the carrier of V by FUNCT_2:5;
the_left_argument_of H in LTL_WFF by Th1;
then h . (the_left_argument_of H) in the carrier of V by FUNCT_2:5;
then [(h . (the_left_argument_of H)),(h . (the_right_argument_of H))] in [: the carrier of V, the carrier of V:] by A10, ZFMISC_1:def 2;
hence H₁(H) in the carrier of V by A5, A9, FUNCT_2:5; :: thesis: verum

end;

suppose ( len H = k + 1 & H is disjunctive ) ; :: thesis: H₁(H) in the carrier of V

then A11: GraftEval (V,Kai,h,h,k,H) = the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) by Def29;
the_right_argument_of H in LTL_WFF by Th1;
then A12: h . (the_right_argument_of H) in the carrier of V by FUNCT_2:5;
the_left_argument_of H in LTL_WFF by Th1;
then h . (the_left_argument_of H) in the carrier of V by FUNCT_2:5;
then [(h . (the_left_argument_of H)),(h . (the_right_argument_of H))] in [: the carrier of V, the carrier of V:] by A12, ZFMISC_1:def 2;
hence H₁(H) in the carrier of V by A5, A11, FUNCT_2:5; :: thesis: verum

end;

suppose A13: ( len H = k + 1 & H is next ) ; :: thesis: H₁(H) in the carrier of V

the_argument_of H in LTL_WFF by Th1;
then A14: h . (the_argument_of H) in the carrier of V by FUNCT_2:5;
GraftEval (V,Kai,h,h,k,H) = the NEXT of V . (h . (the_argument_of H)) by A13, Def29;
hence H₁(H) in the carrier of V by A5, A14, FUNCT_2:5; :: thesis: verum

end;

suppose ( len H = k + 1 & H is Until ) ; :: thesis: H₁(H) in the carrier of V

then A15: GraftEval (V,Kai,h,h,k,H) = the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) by Def29;
the_right_argument_of H in LTL_WFF by Th1;
then A16: h . (the_right_argument_of H) in the carrier of V by FUNCT_2:5;
the_left_argument_of H in LTL_WFF by Th1;
then h . (the_left_argument_of H) in the carrier of V by FUNCT_2:5;
then [(h . (the_left_argument_of H)),(h . (the_right_argument_of H))] in [: the carrier of V, the carrier of V:] by A16, ZFMISC_1:def 2;
hence H₁(H) in the carrier of V by A5, A15, FUNCT_2:5; :: thesis: verum

end;

suppose ( len H = k + 1 & H is Release ) ; :: thesis: H₁(H) in the carrier of V

then A17: GraftEval (V,Kai,h,h,k,H) = the RELEASE of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) by Def29;
the_right_argument_of H in LTL_WFF by Th1;
then A18: h . (the_right_argument_of H) in the carrier of V by FUNCT_2:5;
the_left_argument_of H in LTL_WFF by Th1;
then h . (the_left_argument_of H) in the carrier of V by FUNCT_2:5;
then [(h . (the_left_argument_of H)),(h . (the_right_argument_of H))] in [: the carrier of V, the carrier of V:] by A18, ZFMISC_1:def 2;
hence H₁(H) in the carrier of V by A5, A17, FUNCT_2:5; :: thesis: verum

end;

suppose len H < k + 1 ; :: thesis: H₁(H) in the carrier of V

then GraftEval (V,Kai,h,h,k,H) = h . H by Def29;
hence H₁(H) in the carrier of V by A4, A5, FUNCT_2:5; :: thesis: verum

end;

end;

end;

consider f being Function of LTL_WFF, the carrier of V such that
A19: for H being object st H in LTL_WFF holds
f . H = H₁(H) from FUNCT_2:sch 2(A3);
take f ; :: thesis: f is-PreEvaluation-for k + 1,Kai
A20: for H being LTL-formula st len H < k + 1 holds
f . H = h . H

proof

let H be LTL-formula; :: thesis: ( len H < k + 1 implies f . H = h . H )
assume A21: len H < k + 1 ; :: thesis: f . H = h . H
A22: H in LTL_WFF by Th1;
then f . H = H₁(H) by A19
.= GraftEval (V,Kai,h,h,k,H) by A22, Def25 ;
hence f . H = h . H by A21, Def29; :: thesis: verum

end;

for H being LTL-formula st len H <= k + 1 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 <= k + 1 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 A23: len H <= k + 1 ; :: 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))) ) )
A24: H in LTL_WFF by Th1;
then A25: f . H = H₁(H) by A19
.= GraftEval (V,Kai,h,h,k,H) by A24, Def25 ;
A26: ( H is negative implies f . H = the Compl of V . (f . (the_argument_of H)) )

proof

assume A27: H is negative ; :: thesis: f . H = the Compl of V . (f . (the_argument_of H))
then len (the_argument_of H) < len H by Th10;
then len (the_argument_of H) <= k by A23, Lm1;
then A28: len (the_argument_of H) < k + 1 by NAT_1:13;

per cases ( len H <= k or len H = k + 1 ) by A23, NAT_1:8;

suppose A29: len H <= k ; :: thesis: f . H = the Compl of V . (f . (the_argument_of H))

then len H < k + 1 by NAT_1:13;
then f . H = h . H by A20
.= the Compl of V . (h . (the_argument_of H)) by A2, A27, A29 ;
hence f . H = the Compl of V . (f . (the_argument_of H)) by A20, A28; :: thesis: verum

end;

suppose len H = k + 1 ; :: thesis: f . H = the Compl of V . (f . (the_argument_of H))

then GraftEval (V,Kai,h,h,k,H) = the Compl of V . (h . (the_argument_of H)) by A27, Def29
.= the Compl of V . (f . (the_argument_of H)) by A20, A28 ;
hence f . H = the Compl of V . (f . (the_argument_of H)) by A25; :: thesis: verum

end;

end;

end;

A30: ( H is Release implies f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) )

proof

assume A31: H is Release ; :: thesis: f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H)))
then len (the_right_argument_of H) < len H by Th11;
then len (the_right_argument_of H) <= k by A23, Lm1;
then A32: len (the_right_argument_of H) < k + 1 by NAT_1:13;
len (the_left_argument_of H) < len H by A31, Th11;
then len (the_left_argument_of H) <= k by A23, Lm1;
then len (the_left_argument_of H) < k + 1 by NAT_1:13;
then A33: h . (the_left_argument_of H) = f . (the_left_argument_of H) by A20;

per cases ( len H <= k or len H = k + 1 ) by A23, NAT_1:8;

suppose A34: len H <= k ; :: thesis: f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H)))

then len H < k + 1 by NAT_1:13;
then f . H = h . H by A20
.= the RELEASE of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) by A2, A31, A34 ;
hence f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A20, A33, A32; :: thesis: verum

end;

suppose len H = k + 1 ; :: thesis: f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H)))

then GraftEval (V,Kai,h,h,k,H) = the RELEASE of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) by A31, Def29
.= the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A20, A33, A32 ;
hence f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A25; :: thesis: verum

end;

end;

end;

A35: ( H is Until implies f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) )

proof

assume A36: H is Until ; :: thesis: f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H)))
then len (the_right_argument_of H) < len H by Th11;
then len (the_right_argument_of H) <= k by A23, Lm1;
then A37: len (the_right_argument_of H) < k + 1 by NAT_1:13;
len (the_left_argument_of H) < len H by A36, Th11;
then len (the_left_argument_of H) <= k by A23, Lm1;
then len (the_left_argument_of H) < k + 1 by NAT_1:13;
then A38: h . (the_left_argument_of H) = f . (the_left_argument_of H) by A20;

per cases ( len H <= k or len H = k + 1 ) by A23, NAT_1:8;

suppose A39: len H <= k ; :: thesis: f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H)))

then len H < k + 1 by NAT_1:13;
then f . H = h . H by A20
.= the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) by A2, A36, A39 ;
hence f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A20, A38, A37; :: thesis: verum

end;

suppose len H = k + 1 ; :: thesis: f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H)))

then GraftEval (V,Kai,h,h,k,H) = the UNTIL of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) by A36, Def29
.= the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A20, A38, A37 ;
hence f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A25; :: thesis: verum

end;

end;

end;

A40: ( H is disjunctive implies f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) )

proof

assume A41: H is disjunctive ; :: thesis: f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H)))
then len (the_right_argument_of H) < len H by Th11;
then len (the_right_argument_of H) <= k by A23, Lm1;
then A42: len (the_right_argument_of H) < k + 1 by NAT_1:13;
len (the_left_argument_of H) < len H by A41, Th11;
then len (the_left_argument_of H) <= k by A23, Lm1;
then len (the_left_argument_of H) < k + 1 by NAT_1:13;
then A43: h . (the_left_argument_of H) = f . (the_left_argument_of H) by A20;

per cases ( len H <= k or len H = k + 1 ) by A23, NAT_1:8;

suppose A44: len H <= k ; :: thesis: f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H)))

then len H < k + 1 by NAT_1:13;
then f . H = h . H by A20
.= the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) by A2, A41, A44 ;
hence f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A20, A43, A42; :: thesis: verum

end;

suppose len H = k + 1 ; :: thesis: f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H)))

then GraftEval (V,Kai,h,h,k,H) = the L_join of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) by A41, Def29
.= the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A20, A43, A42 ;
hence f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A25; :: thesis: verum

end;

end;

end;

A45: ( H is conjunctive implies f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) )

proof

assume A46: H is conjunctive ; :: thesis: f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H)))
then len (the_right_argument_of H) < len H by Th11;
then len (the_right_argument_of H) <= k by A23, Lm1;
then A47: len (the_right_argument_of H) < k + 1 by NAT_1:13;
len (the_left_argument_of H) < len H by A46, Th11;
then len (the_left_argument_of H) <= k by A23, Lm1;
then len (the_left_argument_of H) < k + 1 by NAT_1:13;
then A48: h . (the_left_argument_of H) = f . (the_left_argument_of H) by A20;

per cases ( len H <= k or len H = k + 1 ) by A23, NAT_1:8;

suppose A49: len H <= k ; :: thesis: f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H)))

then len H < k + 1 by NAT_1:13;
then f . H = h . H by A20
.= the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) by A2, A46, A49 ;
hence f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A20, A48, A47; :: thesis: verum

end;

suppose len H = k + 1 ; :: thesis: f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H)))

then GraftEval (V,Kai,h,h,k,H) = the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) by A46, Def29
.= the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A20, A48, A47 ;
hence f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A25; :: thesis: verum

end;

end;

end;

A50: ( H is next implies f . H = the NEXT of V . (f . (the_argument_of H)) )

proof

assume A51: H is next ; :: thesis: f . H = the NEXT of V . (f . (the_argument_of H))
then len (the_argument_of H) < len H by Th10;
then len (the_argument_of H) <= k by A23, Lm1;
then A52: len (the_argument_of H) < k + 1 by NAT_1:13;

per cases ( len H <= k or len H = k + 1 ) by A23, NAT_1:8;

suppose A53: len H <= k ; :: thesis: f . H = the NEXT of V . (f . (the_argument_of H))

then len H < k + 1 by NAT_1:13;
then f . H = h . H by A20
.= the NEXT of V . (h . (the_argument_of H)) by A2, A51, A53 ;
hence f . H = the NEXT of V . (f . (the_argument_of H)) by A20, A52; :: thesis: verum

end;

suppose len H = k + 1 ; :: thesis: f . H = the NEXT of V . (f . (the_argument_of H))

then GraftEval (V,Kai,h,h,k,H) = the NEXT of V . (h . (the_argument_of H)) by A51, Def29
.= the NEXT of V . (f . (the_argument_of H)) by A20, A52 ;
hence f . H = the NEXT of V . (f . (the_argument_of H)) by A25; :: thesis: verum

end;

end;

end;

( H is atomic implies f . H = Kai . H )

proof

assume A54: H is atomic ; :: thesis: f . H = Kai . H

per cases ( len H <= k or len H = k + 1 ) by A23, NAT_1:8;

suppose A55: len H <= k ; :: thesis: f . H = Kai . H

then len H < k + 1 by NAT_1:13;
then f . H = h . H by A20
.= Kai . H by A2, A54, A55 ;
hence f . H = Kai . H ; :: thesis: verum

end;

suppose len H = k + 1 ; :: thesis: f . H = Kai . H

hence f . H = Kai . H by A25, A54, Def29; :: thesis: verum

end;

end;

end;

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 A26, A45, A40, A50, A35, A30; :: thesis: verum

end;

hence f is-PreEvaluation-for k + 1,Kai ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A56: S₁[ 0 ]

proof

consider v0 being object such that
A57: v0 in the carrier of V by XBOOLE_0:def 1;
set f = LTL_WFF --> v0;
A58: ( dom (LTL_WFF --> v0) = LTL_WFF & rng (LTL_WFF --> v0) c= {v0} ) by FUNCOP_1:13;
{v0} c= the carrier of V by A57, ZFMISC_1:31;
then reconsider f = LTL_WFF --> v0 as Function of LTL_WFF, the carrier of V by A58, FUNCT_2:2, XBOOLE_1:1;
take f ; :: thesis: f is-PreEvaluation-for 0 ,Kai
thus f is-PreEvaluation-for 0 ,Kai by Lm22; :: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A56, A1);
hence for n being Nat ex f being Function of LTL_WFF, the carrier of V st f is-PreEvaluation-for n,Kai ; :: thesis: verum