let V be CTLModelStr ; :: thesis: for Kai being Function of atomic_WFF ,the BasicAssign of V ex f being Function of CTL_WFF ,the Assignations of V st f is-Evaluation-for Kai
let Kai be Function of atomic_WFF ,the BasicAssign of V; :: thesis: ex f being Function of CTL_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,(k_nat $1));
A4:
for n being set st n in NAT holds
H1(n) is Function of CTL_WFF ,the Assignations of V
proof
let n be
set ;
:: thesis: ( n in NAT implies H1(n) is Function of CTL_WFF ,the Assignations of V )
assume A5:
n in NAT
;
:: thesis: H1(n) is Function of CTL_WFF ,the Assignations of V
set Y =
H1(
n);
A6:
k_nat n = n
by A5, Def2;
reconsider n =
n as
Element of
NAT by A5;
H1(
n)
in EvalSet V,
Kai,
n
by A3, A6, Lm30;
then consider h being
Function of
CTL_WFF ,the
Assignations of
V such that A7:
H1(
n)
= h
and
h is-PreEvaluation-for n,
Kai
;
thus
H1(
n) is
Function of
CTL_WFF ,the
Assignations of
V
by A7;
:: thesis: verum
end;
A8:
for n being set st n in NAT holds
H1(n) in Funcs CTL_WFF ,the Assignations of V
consider f1 being Function of NAT ,(Funcs CTL_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 (CastCTLformula $1))),v0) . $1;
A11:
for H being set st H in CTL_WFF holds
H2(H) in the Assignations of V
by FUNCT_2:7;
consider f being Function of CTL_WFF ,the Assignations of V such that
A12:
for H being set st H in CTL_WFF holds
f . H = H2(H)
from FUNCT_2:sch 2(A11);
take
f
; :: thesis: f is-Evaluation-for Kai
for n being Element of NAT holds f is-PreEvaluation-for n,Kai
proof
defpred S1[
Element of
NAT ]
means f is-PreEvaluation-for $1,
Kai;
A13:
S1[
0 ]
A14:
for
k being
Element of
NAT st
S1[
k] holds
S1[
k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A15:
S1[
k]
;
:: thesis: S1[k + 1]
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: ( 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 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)) ) ) )
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 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)) ) )
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 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)) ) )A18:
H in CTL_WFF
by Th1;
then f1 . (len (CastCTLformula H)) =
f1 . (len H)
by Def24
.=
H1(
len H)
by A10
;
then A19:
CastEval V,
(f1 . (len (CastCTLformula H))),
v0 = H1(
len H)
by Def30;
set f2 =
H1(
len H);
reconsider f2 =
H1(
len H) as
Function of
CTL_WFF ,the
Assignations of
V by A19;
A20:
f . H = f2 . H
by A12, A18, A19;
A21:
f2 = Choice . (EvalSet V,Kai,(len H))
by Def2;
Choice . (EvalSet V,Kai,(len H)) in EvalSet V,
Kai,
(len H)
by A3, Lm30;
then consider h being
Function of
CTL_WFF ,the
Assignations of
V such that A22:
f2 = h
and A23:
h is-PreEvaluation-for len H,
Kai
by A21;
A24:
f2 is-PreEvaluation-for k,
Kai
by A17, A22, A23, Lm25;
A25:
(
H is
negative implies
f . H = the
Not of
V . (f . (the_argument_of H)) )
A28:
(
H is
ExistNext implies
f . H = the
EneXt of
V . (f . (the_argument_of H)) )
A31:
(
H is
ExistGlobal implies
f . H = the
EGlobal of
V . (f . (the_argument_of H)) )
A34:
(
H is
conjunctive implies
f . H = the
And of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H)) )
proof
assume A35:
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 Lm23;
then
len (the_left_argument_of H) <= k
by A17, NAT_1:13;
then A36:
f . (the_left_argument_of H) = f2 . (the_left_argument_of H)
by A15, A24, Lm27;
len (the_right_argument_of H) < len H
by A35, Lm23;
then A37:
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 A20, A22, A23, A35, Def27
.=
the
And of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H))
by A15, A24, A36, A37, Lm27
;
hence
f . H = the
And of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H))
;
:: thesis: verum
end;
(
H is
ExistUntill implies
f . H = the
EUntill of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H)) )
proof
assume A38:
H is
ExistUntill
;
:: thesis: f . H = the EUntill of V . (f . (the_left_argument_of H)),(f . (the_right_argument_of H))
then
len (the_left_argument_of H) < len H
by Lm23;
then
len (the_left_argument_of H) <= k
by A17, NAT_1:13;
then A39:
f . (the_left_argument_of H) = f2 . (the_left_argument_of H)
by A15, A24, Lm27;
len (the_right_argument_of H) < len H
by A38, Lm23;
then A40:
len (the_right_argument_of H) <= k
by A17, NAT_1:13;
f . H =
the
EUntill of
V . (f2 . (the_left_argument_of H)),
(f2 . (the_right_argument_of H))
by A20, A22, A23, A38, Def27
.=
the
EUntill of
V . (f . (the_left_argument_of H)),
(f . (the_right_argument_of H))
by A15, A24, A39, A40, Lm27
;
hence
f . H = the
EUntill 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
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 A20, A22, A23, A25, A28, A31, A34, Def27;
:: 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
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)) ) )
;
:: thesis: verum
end;
hence
S1[
k + 1]
by Def27;
:: thesis: verum
end;
for
n being
Element of
NAT holds
S1[
n]
from NAT_1:sch 1(A13, A14);
hence
for
n being
Element of
NAT holds
f is-PreEvaluation-for n,
Kai
;
:: thesis: verum
end;
hence
f is-Evaluation-for Kai
by Lm29; :: thesis: verum