let V be CTLModelStr ; :: thesis: for Kai being Function of atomic_WFF ,the BasicAssign of V
for n being Element of NAT ex f being Function of CTL_WFF ,the Assignations of V st f is-PreEvaluation-for n,Kai
let Kai be Function of atomic_WFF ,the BasicAssign of V; :: thesis: for n being Element of NAT ex f being Function of CTL_WFF ,the Assignations of V st f is-PreEvaluation-for n,Kai
defpred S₁[ Element of NAT ] means ex f being Function of CTL_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 = CTL_WFF --> v0;
( dom (CTL_WFF --> v0) = CTL_WFF & rng (CTL_WFF --> v0) c= {v0} ) by FUNCOP_1:19;
then reconsider f = CTL_WFF --> v0 as Function of CTL_WFF ,the Assignations of V by A3, FUNCT_2:4, XBOOLE_1:1;
take f ; :: thesis: f is-PreEvaluation-for 0 ,Kai
thus f is-PreEvaluation-for 0 ,Kai by Lm24; :: thesis: verum

end;

A4: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
consider h being Function of CTL_WFF ,the Assignations of V such that
A6: h is-PreEvaluation-for k,Kai by A5;
S₁[k + 1]

proof

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

proof

let H be set ; :: thesis: ( H in CTL_WFF implies H₁(H) in the Assignations of V )
assume A8: H in CTL_WFF ; :: thesis: H₁(H) in the Assignations of V
reconsider H = H as CTL-formula by A8, Th1;
A9: H₁(H) = GraftEval V,Kai,h,h,k,H by A8, Def24;

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 ExistNext ) or ( len H = k + 1 & H is ExistGlobal ) or ( len H = k + 1 & H is ExistUntill ) or len H < k + 1 ) by Th2, XXREAL_0:1;

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

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

end;

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

then H in atomic_WFF ;
then Kai . H in the BasicAssign of V by FUNCT_2:7;
then Kai . H in the Assignations of V ;
hence H₁(H) in the Assignations of V by A9, A10, Def28; :: thesis: verum

end;

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

the_argument_of H in CTL_WFF by Th1;
then A12: 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 A11, Def28;
hence H₁(H) in the Assignations of V by A9, A12, FUNCT_2:7; :: thesis: verum

end;

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

the_left_argument_of H in CTL_WFF by Th1;
then A14: h . (the_left_argument_of H) in the Assignations of V by FUNCT_2:7;
the_right_argument_of H in CTL_WFF by Th1;
then h . (the_right_argument_of H) in the Assignations of V by FUNCT_2:7;
then A15: [(h . (the_left_argument_of H)),(h . (the_right_argument_of H))] in [:the Assignations of V,the Assignations of V:] by A14, 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 A13, Def28;
hence H₁(H) in the Assignations of V by A9, A15, FUNCT_2:7; :: thesis: verum

end;

suppose A16: ( len H = k + 1 & H is ExistNext ) ; :: thesis: H₁(H) in the Assignations of V

the_argument_of H in CTL_WFF by Th1;
then A17: h . (the_argument_of H) in the Assignations of V by FUNCT_2:7;
GraftEval V,Kai,h,h,k,H = the EneXt of V . (h . (the_argument_of H)) by A16, Def28;
hence H₁(H) in the Assignations of V by A9, A17, FUNCT_2:7; :: thesis: verum

end;

suppose A18: ( len H = k + 1 & H is ExistGlobal ) ; :: thesis: H₁(H) in the Assignations of V

the_argument_of H in CTL_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 EGlobal of V . (h . (the_argument_of H)) by A18, Def28;
hence H₁(H) in the Assignations of V by A9, A19, FUNCT_2:7; :: thesis: verum

end;

suppose A20: ( len H = k + 1 & H is ExistUntill ) ; :: thesis: H₁(H) in the Assignations of V

the_left_argument_of H in CTL_WFF by Th1;
then A21: h . (the_left_argument_of H) in the Assignations of V by FUNCT_2:7;
the_right_argument_of H in CTL_WFF by Th1;
then h . (the_right_argument_of H) in the Assignations of V by FUNCT_2:7;
then A22: [(h . (the_left_argument_of H)),(h . (the_right_argument_of H))] in [:the Assignations of V,the Assignations of V:] by A21, ZFMISC_1:def 2;
GraftEval V,Kai,h,h,k,H = the EUntill of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) by A20, Def28;
hence H₁(H) in the Assignations of V by A9, A22, FUNCT_2:7; :: thesis: verum

end;

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

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

end;

end;

end;

consider f being Function of CTL_WFF ,the Assignations of V such that
A23: for H being set st H in CTL_WFF holds
f . H = H₁(H) from FUNCT_2:sch 2(A7);
take f ; :: thesis: f is-PreEvaluation-for k + 1,Kai
A24: for H being CTL-formula st len H < k + 1 holds
f . H = h . H

proof

let H be CTL-formula; :: thesis: ( len H < k + 1 implies f . H = h . H )
assume A25: len H < k + 1 ; :: thesis: f . H = h . H
A26: H in CTL_WFF by Th1;
then f . H = H₁(H) by A23
.= GraftEval V,Kai,h,h,k,H by A26, Def24 ;
hence f . H = h . H by A25, Def28; :: thesis: verum

end;

f is-PreEvaluation-for k + 1,Kai

proof

for H being CTL-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 ExistNext implies f . H = the EneXt of V . (f . (the_argument_of H)) ) & ( H is ExistGlobal implies f . H = the EGlobal of V . (f . (the_argument_of H)) ) & ( H is ExistUntill implies f . H = the EUntill of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) ) )

proof

let H be CTL-formula; :: thesis: ( len H <= k + 1 implies ( ( 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 ExistNext implies f . H = the EneXt of V . (f . (the_argument_of H)) ) & ( H is ExistGlobal implies f . H = the EGlobal of V . (f . (the_argument_of H)) ) & ( H is ExistUntill implies f . H = the EUntill of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) ) ) )
assume A27: len H <= k + 1 ; :: thesis: ( ( 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 ExistNext implies f . H = the EneXt of V . (f . (the_argument_of H)) ) & ( H is ExistGlobal implies f . H = the EGlobal of V . (f . (the_argument_of H)) ) & ( H is ExistUntill implies f . H = the EUntill of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) ) )
A28: H in CTL_WFF by Th1;
then A29: f . H = H₁(H) by A23
.= GraftEval V,Kai,h,h,k,H by A28, Def24 ;
A30: ( H is atomic implies f . H = Kai . H )

proof

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

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

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

then len H < k + 1 by NAT_1:13;
then f . H = h . H by A24
.= Kai . H by A6, A31, A32, Def27 ;
hence f . H = Kai . H ; :: thesis: verum

end;

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

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

end;

end;

end;

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

proof

assume A34: H is negative ; :: thesis: f . H = the Not of V . (f . (the_argument_of H))
then len (the_argument_of H) < len H by Lm22;
then len (the_argument_of H) <= k by A27, Lm1;
then A35: len (the_argument_of H) < k + 1 by NAT_1:13;

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

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

then len H < k + 1 by NAT_1:13;
then f . H = h . H by A24
.= the Not of V . (h . (the_argument_of H)) by A6, A34, A36, Def27 ;
hence f . H = the Not of V . (f . (the_argument_of H)) by A24, A35; :: thesis: verum

end;

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

then GraftEval V,Kai,h,h,k,H = the Not of V . (h . (the_argument_of H)) by A34, Def28
.= the Not of V . (f . (the_argument_of H)) by A24, A35 ;
hence f . H = the Not of V . (f . (the_argument_of H)) by A29; :: thesis: verum

end;

end;

end;

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

proof

assume A38: H is conjunctive ; :: thesis: f . H = the And of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H))
then len (the_left_argument_of H) < len H by Lm23;
then len (the_left_argument_of H) <= k by A27, Lm1;
then len (the_left_argument_of H) < k + 1 by NAT_1:13;
then A39: h . (the_left_argument_of H) = f . (the_left_argument_of H) by A24;
len (the_right_argument_of H) < len H by A38, Lm23;
then len (the_right_argument_of H) <= k by A27, Lm1;
then A40: len (the_right_argument_of H) < k + 1 by NAT_1:13;

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

suppose A41: len H <= k ; :: thesis: f . H = the And 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 A24
.= the And of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) by A6, A38, A41, Def27 ;
hence f . H = the And of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A24, A39, A40; :: thesis: verum

end;

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

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 A38, Def28
.= the And of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A24, A39, A40 ;
hence f . H = the And of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A29; :: thesis: verum

end;

end;

end;

A42: ( H is ExistNext implies f . H = the EneXt of V . (f . (the_argument_of H)) )

proof

assume A43: H is ExistNext ; :: thesis: f . H = the EneXt of V . (f . (the_argument_of H))
then len (the_argument_of H) < len H by Lm22;
then len (the_argument_of H) <= k by A27, Lm1;
then A44: len (the_argument_of H) < k + 1 by NAT_1:13;

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

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

then len H < k + 1 by NAT_1:13;
then f . H = h . H by A24
.= the EneXt of V . (h . (the_argument_of H)) by A6, A43, A45, Def27 ;
hence f . H = the EneXt of V . (f . (the_argument_of H)) by A24, A44; :: thesis: verum

end;

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

then GraftEval V,Kai,h,h,k,H = the EneXt of V . (h . (the_argument_of H)) by A43, Def28
.= the EneXt of V . (f . (the_argument_of H)) by A24, A44 ;
hence f . H = the EneXt of V . (f . (the_argument_of H)) by A29; :: thesis: verum

end;

end;

end;

A46: ( H is ExistGlobal implies f . H = the EGlobal of V . (f . (the_argument_of H)) )

proof

assume A47: H is ExistGlobal ; :: thesis: f . H = the EGlobal of V . (f . (the_argument_of H))
then len (the_argument_of H) < len H by Lm22;
then len (the_argument_of H) <= k by A27, Lm1;
then A48: len (the_argument_of H) < k + 1 by NAT_1:13;

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

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

then len H < k + 1 by NAT_1:13;
then f . H = h . H by A24
.= the EGlobal of V . (h . (the_argument_of H)) by A6, A47, A49, Def27 ;
hence f . H = the EGlobal of V . (f . (the_argument_of H)) by A24, A48; :: thesis: verum

end;

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

then GraftEval V,Kai,h,h,k,H = the EGlobal of V . (h . (the_argument_of H)) by A47, Def28
.= the EGlobal of V . (f . (the_argument_of H)) by A24, A48 ;
hence f . H = the EGlobal of V . (f . (the_argument_of H)) by A29; :: thesis: verum

end;

end;

end;

( H is ExistUntill implies f . H = the EUntill of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) )

proof

assume A50: H is ExistUntill ; :: thesis: f . H = the EUntill of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H))
then len (the_left_argument_of H) < len H by Lm23;
then len (the_left_argument_of H) <= k by A27, Lm1;
then len (the_left_argument_of H) < k + 1 by NAT_1:13;
then A51: h . (the_left_argument_of H) = f . (the_left_argument_of H) by A24;
len (the_right_argument_of H) < len H by A50, Lm23;
then len (the_right_argument_of H) <= k by A27, Lm1;
then A52: len (the_right_argument_of H) < k + 1 by NAT_1:13;

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

suppose A53: len H <= k ; :: thesis: f . H = the EUntill 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 A24
.= the EUntill of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) by A6, A50, A53, Def27 ;
hence f . H = the EUntill of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A24, A51, A52; :: thesis: verum

end;

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

then GraftEval V,Kai,h,h,k,H = the EUntill of V . (h . (the_left_argument_of H)),(h . (the_right_argument_of H)) by A50, Def28
.= the EUntill of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A24, A51, A52 ;
hence f . H = the EUntill of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A29; :: thesis: verum

end;

end;

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 ExistNext implies f . H = the EneXt of V . (f . (the_argument_of H)) ) & ( H is ExistGlobal implies f . H = the EGlobal of V . (f . (the_argument_of H)) ) & ( H is ExistUntill implies f . H = the EUntill of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) ) ) by A30, A33, A37, A42, A46; :: thesis: verum

end;

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

end;

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

end;

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

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A1, A4);
hence for n being Element of NAT ex f being Function of CTL_WFF ,the Assignations of V st f is-PreEvaluation-for n,Kai ; :: thesis: verum