let V be LTLModelStr ; :: thesis: 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; :: thesis: ex f being Function of LTL_WFF ,the Assignations of V st f is-Evaluation-for Kai
set M = EvalFamily V,Kai;
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
A3:
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));
A4:
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 ;
:: thesis: ( n in NAT implies H1(n) is Function of LTL_WFF ,the Assignations of V )
assume A5:
n in NAT
;
:: thesis: H1(n) is Function of LTL_WFF ,the Assignations of V
set Y =
H1(
n);
n is
Element of
NAT
by A5;
then reconsider n =
n as
Nat ;
A6:
CastNat n = n
by DefCastNat;
set Z =
EvalSet V,
Kai,
n;
H1(
n)
in EvalSet V,
Kai,
n
by A6, A3, Lm30;
then consider h being
Function of
LTL_WFF ,the
Assignations of
V such that A7:
H1(
n)
= h
and
h is-PreEvaluation-for n,
Kai
;
thus
H1(
n) is
Function of
LTL_WFF ,the
Assignations of
V
by A7;
:: thesis: verum
end;
A8:
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
A10:
for n being set st n in NAT holds
f1 . n = H1(n)
from FUNCT_2:sch 2(A8);
consider v0 being Element of the Assignations of V;
deffunc H2( set ) -> set = (CastEval V,(f1 . (len (CastLTL $1))),v0) . $1;
A11:
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
A12:
for H being set st H in LTL_WFF holds
f . H = H2(H)
from FUNCT_2:sch 2(A11);
take
f
; :: thesis: 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;
A13:
S1[
0 ]
A14:
for
k being
Nat st
S1[
k] holds
S1[
k + 1]
proof
let k be
Nat;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A15:
S1[
k]
;
:: thesis: 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;
:: thesis: ( 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 A16:
len H <= k + 1
;
:: thesis: ( ( 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 A16, NAT_1:8;
case A17:
len H = k + 1
;
:: thesis: ( ( 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)) ) )A18:
H in LTL_WFF
by Th1;
A19:
f1 . (len (CastLTL H)) =
f1 . (len H)
by A18, Def24
.=
H1(
len H)
by A10
;
A20:
CastEval V,
(f1 . (len (CastLTL H))),
v0 = H1(
len H)
by Def30, A19;
set f2 =
H1(
len H);
reconsider f2 =
H1(
len H) as
Function of
LTL_WFF ,the
Assignations of
V by A20;
A21:
f . H = f2 . H
by A12, A18, A20;
A22:
f2 = Choice . (EvalSet V,Kai,(len H))
by DefCastNat;
Choice . (EvalSet V,Kai,(len H)) in EvalSet V,
Kai,
(len H)
by A3, Lm30;
then consider h being
Function of
LTL_WFF ,the
Assignations of
V such that A23:
f2 = h
and A24:
h is-PreEvaluation-for len H,
Kai
by A22;
A25:
f2 is-PreEvaluation-for k,
Kai
by A23, A24, A17, Lm25;
A26:
(
H is
negative implies
f . H = the
Not of
V . (f . (the_argument_of H)) )
A29:
(
H is
next implies
f . H = the
NEXT of
V . (f . (the_argument_of H)) )
A35:
(
H is
conjunctive implies
f . H = the
And of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H)) )
proof
assume A36:
H is
conjunctive
;
:: thesis: f . H = the And of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H))
then
len (the_left_argument_of H) < len H
by ThArg8;
then
len (the_left_argument_of H) <= k
by A17, NAT_1:13;
then A37:
f . (the_left_argument_of H) = f2 . (the_left_argument_of H)
by A25, A15, Lm27;
len (the_right_argument_of H) < len H
by A36, ThArg8;
then A38:
len (the_right_argument_of H) <= k
by A17, NAT_1:13;
f . H =
the
And of
V . (f2 . (the_left_argument_of H)),
(f2 . (the_right_argument_of H))
by A21, A23, A24, A36, Def27
.=
the
And of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H))
by A37, A38, A25, A15, Lm27
;
hence
f . H = the
And of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H))
;
:: thesis: verum
end; A3501:
(
H is
disjunctive implies
f . H = the
Or of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H)) )
proof
assume A3601:
H is
disjunctive
;
:: thesis: f . H = the Or of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H))
then
len (the_left_argument_of H) < len H
by ThArg8;
then
len (the_left_argument_of H) <= k
by A17, NAT_1:13;
then A3701:
f . (the_left_argument_of H) = f2 . (the_left_argument_of H)
by A25, A15, Lm27;
len (the_right_argument_of H) < len H
by A3601, ThArg8;
then A3801:
len (the_right_argument_of H) <= k
by A17, NAT_1:13;
f . H =
the
Or of
V . (f2 . (the_left_argument_of H)),
(f2 . (the_right_argument_of H))
by A21, A23, A24, A3601, Def27
.=
the
Or of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H))
by A3701, A3801, A25, A15, Lm27
;
hence
f . H = the
Or of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H))
;
:: thesis: verum
end; A3900:
(
H is
Until implies
f . H = the
UNTIL of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H)) )
proof
assume A39:
H is
Until
;
:: thesis: f . H = the UNTIL of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H))
then
len (the_left_argument_of H) < len H
by ThArg8;
then
len (the_left_argument_of H) <= k
by A17, NAT_1:13;
then A40:
f . (the_left_argument_of H) = f2 . (the_left_argument_of H)
by A25, A15, Lm27;
len (the_right_argument_of H) < len H
by A39, ThArg8;
then A41:
len (the_right_argument_of H) <= k
by A17, NAT_1:13;
f . H =
the
UNTIL of
V . (f2 . (the_left_argument_of H)),
(f2 . (the_right_argument_of H))
by A21, A23, A24, A39, Def27
.=
the
UNTIL of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H))
by A40, A41, A25, A15, Lm27
;
hence
f . H = the
UNTIL of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H))
;
:: thesis: verum
end;
(
H is
Release implies
f . H = the
RELEASE of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H)) )
proof
assume A3901:
H is
Release
;
:: thesis: f . H = the RELEASE of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H))
then
len (the_left_argument_of H) < len H
by ThArg8;
then
len (the_left_argument_of H) <= k
by A17, NAT_1:13;
then A4001:
f . (the_left_argument_of H) = f2 . (the_left_argument_of H)
by A25, A15, Lm27;
len (the_right_argument_of H) < len H
by A3901, ThArg8;
then A4101:
len (the_right_argument_of H) <= k
by A17, NAT_1:13;
f . H =
the
RELEASE of
V . (f2 . (the_left_argument_of H)),
(f2 . (the_right_argument_of H))
by A21, A23, A24, A3901, Def27
.=
the
RELEASE of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H))
by A4001, A4101, A25, A15, Lm27
;
hence
f . H = the
RELEASE of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H))
;
:: thesis: 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)) ) )
by A21, A23, A24, Def27, A26, A29, A35, A3501, A3900;
:: thesis: 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)) ) )
;
:: thesis: verum
end;
hence
S1[
k + 1]
by Def27;
:: thesis: verum
end;
for
n being
Nat holds
S1[
n]
from NAT_1:sch 2(A13, A14);
hence
for
n being
Nat holds
f is-PreEvaluation-for n,
Kai
;
:: thesis: verum
end;
hence
f is-Evaluation-for Kai
by Lm29; :: thesis: verum