let V be CTLModel; :: 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 carrier 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 carrier of V st f is-PreEvaluation-for n,Kai
defpred S1[ Nat] means ex f being Function of CTL_WFF, the carrier of V st f is-PreEvaluation-for $1,Kai;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; :: thesis: S1[k + 1]
then consider h being Function of CTL_WFF, the carrier of V such that
A2: h is-PreEvaluation-for k,Kai ;
S1[k + 1]
proof
deffunc H1( object ) -> set = GraftEval (V,Kai,h,h,k,(CastCTLformula $1));
A3: for H being object st H in CTL_WFF holds
H1(H) in the carrier of V
proof
let H be object ; :: thesis: ( H in CTL_WFF implies H1(H) in the carrier of V )
assume A4: H in CTL_WFF ; :: thesis: H1(H) in the carrier of V
reconsider H = H as CTL-formula by A4, Th1;
A5: H1(H) = GraftEval (V,Kai,h,h,k,H) by A4, 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: H1(H) in the carrier of V
then GraftEval (V,Kai,h,h,k,H) = h . H by Def28;
hence H1(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: H1(H) in the carrier of V
then H in atomic_WFF ;
then Kai . H in the BasicAssign of V by FUNCT_2:5;
then Kai . H in the carrier of V ;
hence H1(H) in the carrier of V by A5, A6, Def28; :: thesis: verum
end;
suppose A7: ( len H = k + 1 & H is negative ) ; :: thesis: H1(H) in the carrier of V
the_argument_of H in CTL_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, Def28;
hence H1(H) in the carrier of V by A5, A8, FUNCT_2:5; :: thesis: verum
end;
suppose A11: ( len H = k + 1 & H is ExistNext ) ; :: thesis: H1(H) in the carrier of V
the_argument_of H in CTL_WFF by Th1;
then A12: h . (the_argument_of H) in the carrier of V by FUNCT_2:5;
GraftEval (V,Kai,h,h,k,H) = the EneXt of V . (h . (the_argument_of H)) by A11, Def28;
hence H1(H) in the carrier of V by A5, A12, FUNCT_2:5; :: thesis: verum
end;
suppose A13: ( len H = k + 1 & H is ExistGlobal ) ; :: thesis: H1(H) in the carrier of V
the_argument_of H in CTL_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 EGlobal of V . (h . (the_argument_of H)) by A13, Def28;
hence H1(H) in the carrier of V by A5, A14, FUNCT_2:5; :: thesis: verum
end;
suppose len H < k + 1 ; :: thesis: H1(H) in the carrier of V
then GraftEval (V,Kai,h,h,k,H) = h . H by Def28;
hence H1(H) in the carrier of V by A4, A5, FUNCT_2:5; :: thesis: verum
end;
end;
end;
consider f being Function of CTL_WFF, the carrier of V such that
A17: for H being object st H in CTL_WFF holds
f . H = H1(H) from FUNCT_2:sch 2(A3);
 take f ; :: thesis: f is-PreEvaluation-for k + 1,Kai
A18: 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 A19: len H < k + 1 ; :: thesis: f . H = h . H
A20: H in CTL_WFF by Th1;
then f . H = H1(H) by A17
.= GraftEval (V,Kai,h,h,k,H) by A20, Def24 ;
hence f . H = h . H by A19, Def28; :: thesis: verum
end;
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 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 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 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 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 A21: 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 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))) ) )
A22: H in CTL_WFF by Th1;
then A23: f . H = H1(H) by A17
.= GraftEval (V,Kai,h,h,k,H) by A22, Def24 ;
A24: ( H is negative implies f . H = the Compl of V . (f . (the_argument_of H)) )
proof
assume A25: H is negative ; :: thesis: f . H = the Compl 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 A21, Lm1;
then A26: len (the_argument_of H) < k + 1 by NAT_1:13;
per cases ( len H <= k or len H = k + 1 ) by A21, NAT_1:8;
suppose A27: 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 A18
.= the Compl of V . (h . (the_argument_of H)) by A2, A25, A27 ;
hence f . H = the Compl of V . (f . (the_argument_of H)) by A18, A26; :: 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 A25, Def28
.= the Compl of V . (f . (the_argument_of H)) by A18, A26 ;
hence f . H = the Compl of V . (f . (the_argument_of H)) by A23; :: thesis: verum
end;
end;
end;
A28: ( H is ExistUntill implies f . H = the EUntill of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) )
proof
assume A29: 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_right_argument_of H) < len H by Lm23;
then len (the_right_argument_of H) <= k by A21, Lm1;
then A30: len (the_right_argument_of H) < k + 1 by NAT_1:13;
len (the_left_argument_of H) < len H by A29, Lm23;
then len (the_left_argument_of H) <= k by A21, Lm1;
then len (the_left_argument_of H) < k + 1 by NAT_1:13;
then A31: h . (the_left_argument_of H) = f . (the_left_argument_of H) by A18;
per cases ( len H <= k or len H = k + 1 ) by A21, NAT_1:8;
suppose A32: 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 A18
.= the EUntill of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) by A2, A29, A32 ;
hence f . H = the EUntill of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A18, A31, A30; :: 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 A29, Def28
.= the EUntill of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A18, A31, A30 ;
hence f . H = the EUntill of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A23; :: thesis: verum
end;
end;
end;
A33: ( 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 A34: 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 Lm23;
then len (the_right_argument_of H) <= k by A21, Lm1;
then A35: len (the_right_argument_of H) < k + 1 by NAT_1:13;
len (the_left_argument_of H) < len H by A34, Lm23;
then len (the_left_argument_of H) <= k by A21, Lm1;
then len (the_left_argument_of H) < k + 1 by NAT_1:13;
then A36: h . (the_left_argument_of H) = f . (the_left_argument_of H) by A18;
per cases ( len H <= k or len H = k + 1 ) by A21, NAT_1:8;
suppose A37: 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 A18
.= the L_meet of V . ((h . (the_left_argument_of H)),(h . (the_right_argument_of H))) by A2, A34, A37 ;
hence f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A18, A36, A35; :: 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 A34, Def28
.= the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A18, A36, A35 ;
hence f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A23; :: thesis: verum
end;
end;
end;
A38: ( H is ExistGlobal implies f . H = the EGlobal of V . (f . (the_argument_of H)) )
proof
assume A39: 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 A21, Lm1;
then A40: len (the_argument_of H) < k + 1 by NAT_1:13;
per cases ( len H <= k or len H = k + 1 ) by A21, NAT_1:8;
suppose A41: 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 A18
.= the EGlobal of V . (h . (the_argument_of H)) by A2, A39, A41 ;
hence f . H = the EGlobal of V . (f . (the_argument_of H)) by A18, A40; :: 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 A39, Def28
.= the EGlobal of V . (f . (the_argument_of H)) by A18, A40 ;
hence f . H = the EGlobal of V . (f . (the_argument_of H)) by A23; :: 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 A21, 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 A21, 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 A18
.= the EneXt of V . (h . (the_argument_of H)) by A2, A43, A45 ;
hence f . H = the EneXt of V . (f . (the_argument_of H)) by A18, 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 A18, A44 ;
hence f . H = the EneXt of V . (f . (the_argument_of H)) by A23; :: thesis: verum
end;
end;
end;
( H is atomic implies f . H = Kai . H )
proof
assume A46: H is atomic ; :: thesis: f . H = Kai . H
per cases ( len H <= k or len H = k + 1 ) by A21, NAT_1:8;
suppose A47: len H <= k ; :: thesis: f . H = Kai . H
then len H < k + 1 by NAT_1:13;
then f . H = h . H by A18
.= Kai . H by A2, A46, A47 ;
hence f . H = Kai . H ; :: thesis: verum
end;
suppose len H = k + 1 ; :: thesis: f . H = Kai . H
hence f . H = Kai . H by A23, A46, Def28; :: 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 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 A24, A33, A42, A38, A28; :: thesis: verum
end;
hence f is-PreEvaluation-for k + 1,Kai ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
A48: S1[ 0 ]
proof
consider v0 being object such that
A49: v0 in the carrier of V by XBOOLE_0:def 1;
set f = CTL_WFF --> v0;
A50: dom (CTL_WFF --> v0) = CTL_WFF by FUNCOP_1:13;
A51: rng (CTL_WFF --> v0) c= {v0} by FUNCOP_1:13;
{v0} c= the carrier of V by A49, ZFMISC_1:31;
then reconsider f = CTL_WFF --> v0 as Function of CTL_WFF, the carrier of V by A50, A51, FUNCT_2:2, XBOOLE_1:1;
take f ; :: thesis: f is-PreEvaluation-for 0 ,Kai
thus f is-PreEvaluation-for 0 ,Kai by Lm24; :: thesis: verum
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A48, A1);
 hence for n being Element of NAT ex f being Function of CTL_WFF, the carrier of V st f is-PreEvaluation-for n,Kai ; :: thesis: verum