let V be CTLModelStr ; :: thesis:
let Kai be Function of atomic_WFF ,the BasicAssign of V; :: thesis:
set M = EvalFamily V,Kai;
consider v0 being Element of the Assignations of V;
for X being set st X in EvalFamily V,Kai holds
X <> {}

proof

let X be set ; :: thesis:
assume X in EvalFamily V,Kai ; :: thesis:
then ex n being Element of NAT st X = EvalSet V,Kai,n by Def31;
hence X <> {} ; :: thesis:

end;

then consider Choice being Function such that
dom Choice = EvalFamily V,Kai and
A1: for X being set st X in EvalFamily V,Kai holds
Choice . X in X by WELLORD2:28;
deffunc H₁( set ) -> set = Choice . (EvalSet V,Kai,(k_nat $1));
A2: for n being set st n in NAT holds
H₁(n) is Function of CTL_WFF ,the Assignations of V

proof

let n be set ; :: thesis:
assume A3: n in NAT ; :: thesis:
A4: k_nat n = n by A3, Def2;
set Y = H₁(n);
reconsider n = n as Element of NAT by A3;
H₁(n) in EvalSet V,Kai,n by A1, A4, Lm30;
then ex h being Function of CTL_WFF ,the Assignations of V st
( H₁(n) = h & h is-PreEvaluation-for n,Kai ) ;
hence H₁(n) is Function of CTL_WFF ,the Assignations of V ; :: thesis:

end;

A5: for n being set st n in NAT holds
H₁(n) in Funcs CTL_WFF ,the Assignations of V

proof

let n be set ; :: thesis:
assume n in NAT ; :: thesis:
then H₁(n) is Function of CTL_WFF ,the Assignations of V by A2;
hence H₁(n) in Funcs CTL_WFF ,the Assignations of V by FUNCT_2:11; :: thesis:

end;

consider f1 being Function of NAT ,(Funcs CTL_WFF ,the Assignations of V) such that
A6: for n being set st n in NAT holds
f1 . n = H₁(n) from FUNCT_2:sch 2(A5);
deffunc H₂( set ) -> set = (CastEval V,(f1 . (len (CastCTLformula $1))),v0) . $1;
A7: for H being set st H in CTL_WFF holds
H₂(H) in the Assignations of V by FUNCT_2:7;
consider f being Function of CTL_WFF ,the Assignations of V such that
A8: for H being set st H in CTL_WFF holds
f . H = H₂(H) from FUNCT_2:sch 2(A7);
take f ; :: thesis:
for n being Element of NAT holds f is-PreEvaluation-for n,Kai

proof

defpred S₁[ Element of NAT ] means f is-PreEvaluation-for $1,Kai;
A9: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis:
assume A10: S₁[k] ; :: thesis:
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:
assume A11: len H <= k + 1 ; :: thesis:

now

per cases by A11, NAT_1:8;

case len H <= k ; :: thesis:

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 A10, Def27; :: thesis:

end;

case A12: len H = k + 1 ; :: thesis:

set f2 = H₁( len H);
A13: H in CTL_WFF by Th1;
then f1 . (len (CastCTLformula H)) = f1 . (len H) by Def24
.= H₁( len H) by A6 ;
then A14: CastEval V,(f1 . (len (CastCTLformula H))),v0 = H₁( len H) by Def30;
then reconsider f2 = H₁( len H) as Function of CTL_WFF ,the Assignations of V ;
A15: f2 = Choice . (EvalSet V,Kai,(len H)) by Def2;
Choice . (EvalSet V,Kai,(len H)) in EvalSet V,Kai,(len H) by A1, Lm30;
then A16: ex h being Function of CTL_WFF ,the Assignations of V st
( f2 = h & h is-PreEvaluation-for len H,Kai ) by A15;
then A17: f2 is-PreEvaluation-for k,Kai by A12, Lm25;
A18: f . H = f2 . H by A8, A13, A14;
A19: ( H is ExistNext implies f . H = the EneXt of V . (f . (the_argument_of H)) )

proof

assume A20: H is ExistNext ; :: thesis:
then len (the_argument_of H) < len H by Lm22;
then A21: len (the_argument_of H) <= k by A12, NAT_1:13;
f . H = the EneXt of V . (f2 . (the_argument_of H)) by A18, A16, A20, Def27
.= the EneXt of V . (f . (the_argument_of H)) by A10, A17, A21, Lm27 ;
hence f . H = the EneXt of V . (f . (the_argument_of H)) ; :: thesis:

end;

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

proof

assume A23: H is ExistUntill ; :: thesis:
then len (the_right_argument_of H) < len H by Lm23;
then A24: len (the_right_argument_of H) <= k by A12, NAT_1:13;
len (the_left_argument_of H) < len H by A23, Lm23;
then len (the_left_argument_of H) <= k by A12, NAT_1:13;
then A25: f . (the_left_argument_of H) = f2 . (the_left_argument_of H) by A10, A17, Lm27;
f . H = the EUntill of V . (f2 . (the_left_argument_of H)),(f2 . (the_right_argument_of H)) by A18, A16, A23, Def27
.= the EUntill of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A10, A17, A25, A24, Lm27 ;
hence f . H = the EUntill of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) ; :: thesis:

end;

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

proof

assume A27: H is conjunctive ; :: thesis:
then len (the_right_argument_of H) < len H by Lm23;
then A28: len (the_right_argument_of H) <= k by A12, NAT_1:13;
len (the_left_argument_of H) < len H by A27, Lm23;
then len (the_left_argument_of H) <= k by A12, NAT_1:13;
then A29: f . (the_left_argument_of H) = f2 . (the_left_argument_of H) by A10, A17, Lm27;
f . H = the And of V . (f2 . (the_left_argument_of H)),(f2 . (the_right_argument_of H)) by A18, A16, A27, Def27
.= the And of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) by A10, A17, A29, A28, Lm27 ;
hence f . H = the And of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H)) ; :: thesis:

end;

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

proof

assume A31: H is ExistGlobal ; :: thesis:
then len (the_argument_of H) < len H by Lm22;
then A32: len (the_argument_of H) <= k by A12, NAT_1:13;
f . H = the EGlobal of V . (f2 . (the_argument_of H)) by A18, A16, A31, Def27
.= the EGlobal of V . (f . (the_argument_of H)) by A10, A17, A32, Lm27 ;
hence f . H = the EGlobal of V . (f . (the_argument_of H)) ; :: thesis:

end;

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

proof

assume A33: H is negative ; :: thesis:
then len (the_argument_of H) < len H by Lm22;
then A34: len (the_argument_of H) <= k by A12, NAT_1:13;
f . H = the Not of V . (f2 . (the_argument_of H)) by A18, A16, A33, Def27
.= the Not of V . (f . (the_argument_of H)) by A10, A17, A34, Lm27 ;
hence f . H = the Not of V . (f . (the_argument_of H)) ; :: thesis:

end;

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

end;

for H being CTL-formula st len H <= 0 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)) ) ) by Lm10;
then A35: S₁[ 0 ] by Def27;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A35, A9);
hence for n being Element of NAT holds f is-PreEvaluation-for n,Kai ; :: thesis:

end;

hence f is-Evaluation-for Kai by Lm29; :: thesis: