let V be LTLModelStr ; for Kai being Function of atomic_LTL ,the BasicAssign of V ex f being Function of LTL_WFF ,the Assignations 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 Assignations of V st f is-Evaluation-for Kai
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 <> {}
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 H1( set ) -> 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 Assignations of V
proof
let n be
set ;
( n in NAT implies H1(n) is Function of LTL_WFF ,the Assignations of V )
assume A3:
n in NAT
;
H1(n) is Function of LTL_WFF ,the Assignations of V
set Y =
H1(
n);
reconsider n =
n as
Nat by A3;
set Z =
EvalSet V,
Kai,
n;
CastNat n = n
by Def1;
then
H1(
n)
in EvalSet V,
Kai,
n
by A1, Lm28;
then
ex
h being
Function of
LTL_WFF ,the
Assignations of
V st
(
H1(
n)
= h &
h is-PreEvaluation-for n,
Kai )
;
hence
H1(
n) is
Function of
LTL_WFF ,the
Assignations of
V
;
verum
end;
A4:
for n being set st n in NAT holds
H1(n) in Funcs LTL_WFF ,the Assignations of V
consider f1 being Function of NAT ,(Funcs LTL_WFF ,the Assignations of V) such that
A5:
for n being set st n in NAT holds
f1 . n = H1(n)
from FUNCT_2:sch 2(A4);
deffunc H2( set ) -> set = (CastEval V,(f1 . (len (CastLTL $1))),v0) . $1;
A6:
for H being set st H in LTL_WFF holds
H2(H) in the Assignations of V
by FUNCT_2:7;
consider f being Function of LTL_WFF ,the Assignations of V such that
A7:
for H being set 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
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
disjunctive implies
f . H = the
Or 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 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 disjunctive implies f . H = the Or 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 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 disjunctive implies f . H = the Or 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 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 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 disjunctive implies f . H = the Or 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))),
v0 = H1(
len H)
by Def31;
then reconsider f2 =
H1(
len H) as
Function of
LTL_WFF ,the
Assignations of
V ;
(
f2 = Choice . (EvalSet V,Kai,(len H)) &
Choice . (EvalSet V,Kai,(len H)) in EvalSet V,
Kai,
(len H) )
by A1, Def1, Lm28;
then A14:
ex
h being
Function of
LTL_WFF ,the
Assignations 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, Lm25;
f . H =
the
RELEASE of
V . (f2 . (the_left_argument_of H)),
(f2 . (the_right_argument_of H))
by A16, A14, A21, Def28
.=
the
RELEASE of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H))
by A9, A15, A23, A22, Lm25
;
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, Lm25;
f . H =
the
UNTIL of
V . (f2 . (the_left_argument_of H)),
(f2 . (the_right_argument_of H))
by A16, A14, A25, Def28
.=
the
UNTIL of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H))
by A9, A15, A27, A26, Lm25
;
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
Or of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H)) )
proof
assume A29:
H is
disjunctive
;
f . H = the Or 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, Lm25;
f . H =
the
Or of
V . (f2 . (the_left_argument_of H)),
(f2 . (the_right_argument_of H))
by A16, A14, A29, Def28
.=
the
Or of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H))
by A9, A15, A31, A30, Lm25
;
hence
f . H = the
Or of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H))
;
verum
end; A32:
(
H is
conjunctive implies
f . H = the
And of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H)) )
proof
assume A33:
H is
conjunctive
;
f . H = the And 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, Lm25;
f . H =
the
And of
V . (f2 . (the_left_argument_of H)),
(f2 . (the_right_argument_of H))
by A16, A14, A33, Def28
.=
the
And of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H))
by A9, A15, A35, A34, Lm25
;
hence
f . H = the
And of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H))
;
verum
end;
(
H is
negative implies
f . H = the
Not of
V . (f . (the_argument_of H)) )
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
disjunctive implies
f . H = the
Or 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, Def28;
verum 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
disjunctive implies
f . H = the
Or 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
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
disjunctive implies
f . H = the
Or 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 Lm27; verum