let V be LTLModelStr ; :: thesis:
let Kai be Function of atomic_LTL ,the BasicAssign of V; :: thesis:
defpred S₁[ Nat] means ex f being Function of LTL_WFF ,the Assignations of V st f is-PreEvaluation-for $1,Kai;
A1: S₁[ 0 ]

proof

consider v0 being set such that
A2: v0 in the Assignations of V by XBOOLE_0:def 1;
A3: {v0} c= the Assignations of V by A2, ZFMISC_1:37;
set f = LTL_WFF --> v0;
( dom (LTL_WFF --> v0) = LTL_WFF & rng (LTL_WFF --> v0) c= {v0} ) by FUNCOP_1:19;
then reconsider f = LTL_WFF --> v0 as Function of LTL_WFF ,the Assignations of V by A3, FUNCT_2:4, XBOOLE_1:1;
take f ; :: thesis:
thus f is-PreEvaluation-for 0 ,Kai by Lm24; :: thesis:

end;

A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A6: S₁[k] ; :: thesis:
consider h being Function of LTL_WFF ,the Assignations of V such that
A7: h is-PreEvaluation-for k,Kai by A6;
S₁[k + 1]

proof

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

proof

let H be set ; :: thesis:
assume A9: H in LTL_WFF ; :: thesis:
reconsider H = H as LTL-formula by Th1, A9;
A10: H₁(H) = GraftEval V,Kai,h,h,k,H by A9, Def24;

per cases by Th2, XXREAL_0:1;

suppose len H > k + 1 ; :: thesis:

then GraftEval V,Kai,h,h,k,H = h . H by Def28;
hence H₁(H) in the Assignations of V by A9, A10, FUNCT_2:7; :: thesis:

end;

suppose A11: ( len H = k + 1 & H is atomic ) ; :: thesis:

then A12: H in atomic_LTL ;
Kai . H in the BasicAssign of V by A12, FUNCT_2:7;
then Kai . H in the Assignations of V ;
hence H₁(H) in the Assignations of V by A11, Def28, A10; :: thesis:

end;

suppose A13: ( len H = k + 1 & H is negative ) ; :: thesis:

the_argument_of H in LTL_WFF by Th1;
then A14: h . (the_argument_of H) in the Assignations of V by FUNCT_2:7;
GraftEval V,Kai,h,h,k,H = the Not of V . (h . (the_argument_of H)) by A13, Def28;
hence H₁(H) in the Assignations of V by A14, A10, FUNCT_2:7; :: thesis:

end;

suppose A15: ( len H = k + 1 & H is conjunctive ) ; :: thesis:

the_left_argument_of H in LTL_WFF by Th1;
then A16: h . (the_left_argument_of H) in the Assignations of V by FUNCT_2:7;
the_right_argument_of H in LTL_WFF by Th1;
then h . (the_right_argument_of H) in the Assignations of V by FUNCT_2:7;
then A17: [(h . (the_left_argument_of H)),(h . (the_right_argument_of H))] in [:the Assignations of V,the Assignations of V:] by A16, ZFMISC_1:def 2;
GraftEval V,Kai,h,h,k,H = the And of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) by A15, Def28;
hence H₁(H) in the Assignations of V by A17, A10, FUNCT_2:7; :: thesis:

end;

suppose A1501: ( len H = k + 1 & H is disjunctive ) ; :: thesis:

the_left_argument_of H in LTL_WFF by Th1;
then A1601: h . (the_left_argument_of H) in the Assignations of V by FUNCT_2:7;
the_right_argument_of H in LTL_WFF by Th1;
then h . (the_right_argument_of H) in the Assignations of V by FUNCT_2:7;
then A1701: [(h . (the_left_argument_of H)),(h . (the_right_argument_of H))] in [:the Assignations of V,the Assignations of V:] by A1601, ZFMISC_1:def 2;
GraftEval V,Kai,h,h,k,H = the Or of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) by A1501, Def28;
hence H₁(H) in the Assignations of V by A1701, A10, FUNCT_2:7; :: thesis:

end;

suppose A18: ( len H = k + 1 & H is next ) ; :: thesis:

the_argument_of H in LTL_WFF by Th1;
then A19: h . (the_argument_of H) in the Assignations of V by FUNCT_2:7;
GraftEval V,Kai,h,h,k,H = the NEXT of V . (h . (the_argument_of H)) by A18, Def28;
hence H₁(H) in the Assignations of V by A19, A10, FUNCT_2:7; :: thesis:

end;

suppose A22: ( len H = k + 1 & H is Until ) ; :: thesis:

the_left_argument_of H in LTL_WFF by Th1;
then A23: h . (the_left_argument_of H) in the Assignations of V by FUNCT_2:7;
the_right_argument_of H in LTL_WFF by Th1;
then h . (the_right_argument_of H) in the Assignations of V by FUNCT_2:7;
then A24: [(h . (the_left_argument_of H)),(h . (the_right_argument_of H))] in [:the Assignations of V,the Assignations of V:] by A23, ZFMISC_1:def 2;
GraftEval V,Kai,h,h,k,H = the UNTIL of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) by A22, Def28;
hence H₁(H) in the Assignations of V by A24, A10, FUNCT_2:7; :: thesis:

end;

suppose A2201: ( len H = k + 1 & H is Release ) ; :: thesis:

the_left_argument_of H in LTL_WFF by Th1;
then A2301: h . (the_left_argument_of H) in the Assignations of V by FUNCT_2:7;
the_right_argument_of H in LTL_WFF by Th1;
then h . (the_right_argument_of H) in the Assignations of V by FUNCT_2:7;
then A2401: [(h . (the_left_argument_of H)),(h . (the_right_argument_of H))] in [:the Assignations of V,the Assignations of V:] by A2301, ZFMISC_1:def 2;
GraftEval V,Kai,h,h,k,H = the RELEASE of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) by A2201, Def28;
hence H₁(H) in the Assignations of V by A2401, A10, FUNCT_2:7; :: thesis:

end;

suppose len H < k + 1 ; :: thesis:

then GraftEval V,Kai,h,h,k,H = h . H by Def28;
hence H₁(H) in the Assignations of V by A9, A10, FUNCT_2:7; :: thesis:

end;

consider f being Function of LTL_WFF ,the Assignations of V such that
A25: for H being set st H in LTL_WFF holds
f . H = H₁(H) from FUNCT_2:sch 2(A8);
take f ; :: thesis:
A26: for H being LTL-formula st len H < k + 1 holds
f . H = h . H

proof

let H be LTL-formula; :: thesis:
assume A27: len H < k + 1 ; :: thesis:
A28: H in LTL_WFF by Th1;
f . H = H₁(H) by A28, A25
.= GraftEval V,Kai,h,h,k,H by A28, Def24 ;
hence f . H = h . H by Def28, A27; :: thesis:

end;

f is-PreEvaluation-for k + 1,Kai

proof

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 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)) ) )

proof

let H be LTL-formula; :: thesis:
assume A29: len H <= k + 1 ; :: thesis:
A30: H in LTL_WFF by Th1;
A31: f . H = H₁(H) by A30, A25
.= GraftEval V,Kai,h,h,k,H by A30, Def24 ;
A32: ( H is atomic implies f . H = Kai . H )

proof

assume A33: H is atomic ; :: thesis:

per cases by A29, NAT_1:8;

suppose A34: len H <= k ; :: thesis:

then len H < k + 1 by NAT_1:13;
then f . H = h . H by A26
.= Kai . H by A7, A33, A34, Def27 ;
hence f . H = Kai . H ; :: thesis:

end;

suppose len H = k + 1 ; :: thesis:

hence f . H = Kai . H by A33, Def28, A31; :: thesis:

end;

A35: ( H is negative implies f . H = the Not of V . (f . (the_argument_of H)) )

proof

assume A36: H is negative ; :: thesis:
then len (the_argument_of H) < len H by ThArg7;
then len (the_argument_of H) <= k by A29, Lm1;
then A37: len (the_argument_of H) < k + 1 by NAT_1:13;

per cases by A29, NAT_1:8;

suppose A38: len H <= k ; :: thesis:

then len H < k + 1 by NAT_1:13;
then f . H = h . H by A26
.= the Not of V . (h . (the_argument_of H)) by A7, A36, A38, Def27 ;
hence f . H = the Not of V . (f . (the_argument_of H)) by A37, A26; :: thesis:

end;

suppose len H = k + 1 ; :: thesis:

then GraftEval V,Kai,h,h,k,H = the Not of V . (h . (the_argument_of H)) by Def28, A36
.= the Not of V . (f . (the_argument_of H)) by A37, A26 ;
hence f . H = the Not of V . (f . (the_argument_of H)) by A31; :: thesis:

end;

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

proof

assume A40: H is conjunctive ; :: thesis:
then len (the_left_argument_of H) < len H by ThArg8;
then len (the_left_argument_of H) <= k by A29, Lm1;
then len (the_left_argument_of H) < k + 1 by NAT_1:13;
then A41: h . (the_left_argument_of H) = f . (the_left_argument_of H) by A26;
len (the_right_argument_of H) < len H by A40, ThArg8;
then len (the_right_argument_of H) <= k by A29, Lm1;
then A42: len (the_right_argument_of H) < k + 1 by NAT_1:13;

per cases by A29, NAT_1:8;

suppose A43: len H <= k ; :: thesis:

then len H < k + 1 by NAT_1:13;
then f . H = h . H by A26
.= the And of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) by A7, A40, A43, Def27 ;
hence f . H = the And of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A41, A42, A26; :: thesis:

end;

suppose len H = k + 1 ; :: thesis:

then GraftEval V,Kai,h,h,k,H = the And of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) by Def28, A40
.= the And of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A41, A42, A26 ;
hence f . H = the And of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A31; :: thesis:

end;

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

proof

assume A4001: H is disjunctive ; :: thesis:
then len (the_left_argument_of H) < len H by ThArg8;
then len (the_left_argument_of H) <= k by A29, Lm1;
then len (the_left_argument_of H) < k + 1 by NAT_1:13;
then A4101: h . (the_left_argument_of H) = f . (the_left_argument_of H) by A26;
len (the_right_argument_of H) < len H by A4001, ThArg8;
then len (the_right_argument_of H) <= k by A29, Lm1;
then A4201: len (the_right_argument_of H) < k + 1 by NAT_1:13;

per cases by A29, NAT_1:8;

suppose A4301: len H <= k ; :: thesis:

then len H < k + 1 by NAT_1:13;
then f . H = h . H by A26
.= the Or of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) by A7, A4001, A4301, Def27 ;
hence f . H = the Or of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A4101, A4201, A26; :: thesis:

end;

suppose len H = k + 1 ; :: thesis:

then GraftEval V,Kai,h,h,k,H = the Or of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) by Def28, A4001
.= the Or of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A4101, A4201, A26 ;
hence f . H = the Or of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A31; :: thesis:

end;

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

proof

assume A45: H is next ; :: thesis:
then len (the_argument_of H) < len H by ThArg7;
then len (the_argument_of H) <= k by A29, Lm1;
then A46: len (the_argument_of H) < k + 1 by NAT_1:13;

per cases by A29, NAT_1:8;

suppose A47: len H <= k ; :: thesis:

then len H < k + 1 by NAT_1:13;
then f . H = h . H by A26
.= the NEXT of V . (h . (the_argument_of H)) by A7, A45, A47, Def27 ;
hence f . H = the NEXT of V . (f . (the_argument_of H)) by A46, A26; :: thesis:

end;

suppose len H = k + 1 ; :: thesis:

then GraftEval V,Kai,h,h,k,H = the NEXT of V . (h . (the_argument_of H)) by Def28, A45
.= the NEXT of V . (f . (the_argument_of H)) by A46, A26 ;
hence f . H = the NEXT of V . (f . (the_argument_of H)) by A31; :: thesis:

end;

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

proof

assume A52: H is Until ; :: thesis:
then len (the_left_argument_of H) < len H by ThArg8;
then len (the_left_argument_of H) <= k by A29, Lm1;
then len (the_left_argument_of H) < k + 1 by NAT_1:13;
then A53: h . (the_left_argument_of H) = f . (the_left_argument_of H) by A26;
len (the_right_argument_of H) < len H by ThArg8, A52;
then len (the_right_argument_of H) <= k by A29, Lm1;
then A54: len (the_right_argument_of H) < k + 1 by NAT_1:13;

per cases by A29, NAT_1:8;

suppose A55: len H <= k ; :: thesis:

then len H < k + 1 by NAT_1:13;
then f . H = h . H by A26
.= the UNTIL of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) by A7, A52, A55, Def27 ;
hence f . H = the UNTIL of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A53, A54, A26; :: thesis:

end;

suppose len H = k + 1 ; :: thesis:

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 Def28, A52
.= the UNTIL of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A53, A54, A26 ;
hence f . H = the UNTIL of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A31; :: thesis:

end;

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

proof

assume A5201: H is Release ; :: thesis:
then len (the_left_argument_of H) < len H by ThArg8;
then len (the_left_argument_of H) <= k by A29, Lm1;
then len (the_left_argument_of H) < k + 1 by NAT_1:13;
then A5301: h . (the_left_argument_of H) = f . (the_left_argument_of H) by A26;
len (the_right_argument_of H) < len H by ThArg8, A5201;
then len (the_right_argument_of H) <= k by A29, Lm1;
then A5401: len (the_right_argument_of H) < k + 1 by NAT_1:13;

per cases by A29, NAT_1:8;

suppose A5501: len H <= k ; :: thesis:

then len H < k + 1 by NAT_1:13;
then f . H = h . H by A26
.= the RELEASE of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) by A7, A5201, A5501, Def27 ;
hence f . H = the RELEASE of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A5301, A5401, A26; :: thesis:

end;

suppose len H = k + 1 ; :: thesis:

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 Def28, A5201
.= the RELEASE of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A5301, A5401, A26 ;
hence f . H = the RELEASE of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A31; :: thesis:

end;

hence ( ( 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 A32, A35, A39, A3901, A44, A50; :: thesis:

end;

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

end;

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

end;

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

end;

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