let V be LTLModel; for Kai being Function of atomic_LTL, the BasicAssign of V ex f being Function of LTL_WFF, the carrier of V st f is-Evaluation-for Kai
let Kai be Function of atomic_LTL, the BasicAssign of V; ex f being Function of LTL_WFF, the carrier of V st f is-Evaluation-for Kai
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 <> {}
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 H1( object ) -> set = Choice . (EvalSet (V,Kai,(CastNat $1)));
A2:
for n being set st n in NAT holds
H1(n) is Function of LTL_WFF, the carrier of V
A4:
for n being object st n in NAT holds
H1(n) in Funcs (LTL_WFF, the carrier of V)
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 = H1(n)
from FUNCT_2:sch 2(A4);
deffunc H2( 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
H2(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 = H2(H)
from FUNCT_2:sch 2(A6);
take
f
; f is-Evaluation-for Kai
for n being Nat holds f is-PreEvaluation-for n,Kai
proof
defpred S1[
Nat]
means f is-PreEvaluation-for $1,
Kai;
A8:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A9:
S1[
k]
;
S1[k + 1]
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;
( 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 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))) ) ) )
assume A10:
len H <= k + 1
;
( ( 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))) ) )
now ( ( len H <= k & ( 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))) ) ) or ( len H = k + 1 & ( 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))) ) ) )per cases
( len H <= k or len H = k + 1 )
by A10, NAT_1:8;
case A11:
len H = k + 1
;
( ( 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))) ) )set f2 =
H1(
len H);
A12:
H in LTL_WFF
by Th1;
then f1 . (len (CastLTL H)) =
f1 . (len H)
by Def25
.=
H1(
len H)
by A5
;
then A13:
CastEval (
V,
(f1 . (len (CastLTL H))), the
Element of the
carrier of
V)
= H1(
len H)
by Def33;
then reconsider f2 =
H1(
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)) )
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
;
f . H = the RELEASE of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H)))
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)))
;
verum
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
;
f . H = the UNTIL of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H)))
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)))
;
verum
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
;
f . H = the L_join of V . ((f . (the_left_argument_of H)),(f . (the_right_argument_of H)))
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)))
;
verum
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
;
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 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)))
;
verum
end;
(
H is
negative implies
f . H = the
Compl of
V . (f . (the_argument_of H)) )
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 A16, A14, A17, A32, A28, A24, A20;
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
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))) ) )
;
verum
end;
hence
S1[
k + 1]
by Def28;
verum
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:
S1[
0 ]
by Def28;
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(A38, A8);
hence
for
n being
Nat holds
f is-PreEvaluation-for n,
Kai
;
verum
end;
hence
f is-Evaluation-for Kai
by Lm26; verum