let V be LTLModel; :: thesis:
let Kai be Function of atomic_LTL, the BasicAssign of V; :: thesis:
set M = EvalFamily (V,Kai);
set v0 = the Element of the carrier 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 Nat st X = EvalSet (V,Kai,n) by Def34;
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 FUNCT_1:111;
deffunc H₁( object ) -> set = Choice . (EvalSet (V,Kai,(CastNat $1)));
A2: for n being set st n in NAT holds
H₁(n) is Function of LTL_WFF, the carrier of V

proof

let n be set ; :: thesis:
assume A3: n in NAT ; :: thesis:
set Y = H₁(n);
reconsider n = n as Nat by A3;
CastNat n = n by Def1;
then H₁(n) in EvalSet (V,Kai,n) by A1, Lm27;
then ex h being Function of LTL_WFF, the carrier of V st
( H₁(n) = h & h is-PreEvaluation-for n,Kai ) ;
hence H₁(n) is Function of LTL_WFF, the carrier of V ; :: thesis:

end;

A4: for n being object st n in NAT holds
H₁(n) in Funcs (LTL_WFF, the carrier of V)

proof

let n be object ; :: thesis:
assume n in NAT ; :: thesis:
then H₁(n) is Function of LTL_WFF, the carrier of V by A2;
hence H₁(n) in Funcs (LTL_WFF, the carrier of V) by FUNCT_2:8; :: thesis:

end;

consider f1 being sequence of (Funcs (LTL_WFF, the carrier of V)) such that
A5: for n being object st n in NAT holds
f1 . n = H₁(n) from FUNCT_2:sch 2(A4);
deffunc H₂( object ) -> set = (CastEval (V,(f1 . (len (CastLTL $1))), the Element of the carrier of V)) . $1;
A6: for H being object st H in LTL_WFF holds
H₂(H) in the carrier of V by FUNCT_2:5;
consider f being Function of LTL_WFF, the carrier of V such that
A7: for H being object st H in LTL_WFF holds
f . H = H₂(H) from FUNCT_2:sch 2(A6);
take f ; :: thesis:
for n being Nat holds f is-PreEvaluation-for n,Kai

proof

defpred S₁[ Nat] means f is-PreEvaluation-for $1,Kai;
A8: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

now :: thesis:

per cases by A10, NAT_1:8;

case len H <= k ; :: thesis:

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 A9, Def28; :: thesis:

end;

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

set f2 = H₁( len H);
A12: H in LTL_WFF by Th1;
then f1 . (len (CastLTL H)) = f1 . (len H) by Def25
.= H₁( len H) by A5 ;
then A13: CastEval (V,(f1 . (len (CastLTL H))), the Element of the carrier of V) = H₁( len H) by Def33;
then reconsider f2 = H₁( len H) as Function of LTL_WFF, the carrier of V ;
( f2 = Choice . (EvalSet (V,Kai,(len H))) & Choice . (EvalSet (V,Kai,(len H))) in EvalSet (V,Kai,(len H)) ) by A1, Def1, Lm27;
then A14: ex h being Function of LTL_WFF, the carrier of V st
( f2 = h & h is-PreEvaluation-for len H,Kai ) ;
then A15: f2 is-PreEvaluation-for k,Kai by A11, Lm23;
A16: f . H = f2 . H by A7, A12, A13;
A17: ( H is next implies f . H = the NEXT of V . (f . (the_argument_of H)) )

proof

assume A18: H is next ; :: thesis:
then len (the_argument_of H) < len H by Th10;
then A19: len (the_argument_of H) <= k by A11, NAT_1:13;
f . H = the NEXT of V . (f2 . (the_argument_of H)) by A16, A14, A18
.= the NEXT of V . (f . (the_argument_of H)) by A9, A15, A19, Lm24 ;
hence f . H = the NEXT of V . (f . (the_argument_of H)) ; :: thesis:

end;

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

proof

assume A21: H is Release ; :: thesis:
then len (the_right_argument_of H) < len H by Th11;
then A22: len (the_right_argument_of H) <= k by A11, NAT_1:13;
len (the_left_argument_of H) < len H by A21, Th11;
then len (the_left_argument_of H) <= k by A11, NAT_1:13;
then A23: f . (the_left_argument_of H) = f2 . (the_left_argument_of H) by A9, A15, Lm24;
f . H = the RELEASE of V . ((f2 . (the_left_argument_of H)),(f2 . (the_right_argument_of H))) by A16, A14, A21
.= the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A9, A15, A23, A22, Lm24 ;
hence f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ; :: thesis:

end;

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

proof

assume A25: H is Until ; :: thesis:
then len (the_right_argument_of H) < len H by Th11;
then A26: len (the_right_argument_of H) <= k by A11, NAT_1:13;
len (the_left_argument_of H) < len H by A25, Th11;
then len (the_left_argument_of H) <= k by A11, NAT_1:13;
then A27: f . (the_left_argument_of H) = f2 . (the_left_argument_of H) by A9, A15, Lm24;
f . H = the UNTIL of V . ((f2 . (the_left_argument_of H)),(f2 . (the_right_argument_of H))) by A16, A14, A25
.= the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A9, A15, A27, A26, Lm24 ;
hence f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ; :: thesis:

end;

A28: ( 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 A29: H is disjunctive ; :: thesis:
then len (the_right_argument_of H) < len H by Th11;
then A30: len (the_right_argument_of H) <= k by A11, NAT_1:13;
len (the_left_argument_of H) < len H by A29, Th11;
then len (the_left_argument_of H) <= k by A11, NAT_1:13;
then A31: f . (the_left_argument_of H) = f2 . (the_left_argument_of H) by A9, A15, Lm24;
f . H = the L_join of V . ((f2 . (the_left_argument_of H)),(f2 . (the_right_argument_of H))) by A16, A14, A29
.= the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A9, A15, A31, A30, Lm24 ;
hence f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ; :: thesis:

end;

A32: ( 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 A33: H is conjunctive ; :: thesis:
then len (the_right_argument_of H) < len H by Th11;
then A34: len (the_right_argument_of H) <= k by A11, NAT_1:13;
len (the_left_argument_of H) < len H by A33, Th11;
then len (the_left_argument_of H) <= k by A11, NAT_1:13;
then A35: f . (the_left_argument_of H) = f2 . (the_left_argument_of H) by A9, A15, Lm24;
f . H = the L_meet of V . ((f2 . (the_left_argument_of H)),(f2 . (the_right_argument_of H))) by A16, A14, A33
.= the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) by A9, A15, A35, A34, Lm24 ;
hence f . H = the L_meet of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H))) ; :: thesis:

end;

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

proof

assume A36: H is negative ; :: thesis:
then len (the_argument_of H) < len H by Th10;
then A37: len (the_argument_of H) <= k by A11, NAT_1:13;
f . H = the Compl of V . (f2 . (the_argument_of H)) by A16, A14, A36
.= the Compl of V . (f . (the_argument_of H)) by A9, A15, A37, Lm24 ;
hence f . H = the Compl of V . (f . (the_argument_of H)) ; :: thesis:

end;

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

end;

for H being LTL-formula st len H <= 0 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))) ) ) by Th3;
then A38: S₁[ 0 ] by Def28;
for n being Nat holds S₁[n] from NAT_1:sch 2(A38, A8);
hence for n being Nat holds f is-PreEvaluation-for n,Kai ; :: thesis:

end;

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