let n be Element of NAT ; :: thesis: for V being CTLModelStr
for Kai being Function of atomic_WFF ,the BasicAssign of V
for f1, f2 being Function of CTL_WFF ,the Assignations of V st f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai holds
for H being CTL-formula st len H <= n holds
f1 . H = f2 . H
let V be CTLModelStr ; :: thesis: for Kai being Function of atomic_WFF ,the BasicAssign of V
for f1, f2 being Function of CTL_WFF ,the Assignations of V st f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai holds
for H being CTL-formula st len H <= n holds
f1 . H = f2 . H
let Kai be Function of atomic_WFF ,the BasicAssign of V; :: thesis: for f1, f2 being Function of CTL_WFF ,the Assignations of V st f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai holds
for H being CTL-formula st len H <= n holds
f1 . H = f2 . H
let f1, f2 be Function of CTL_WFF ,the Assignations of V; :: thesis: ( f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai implies for H being CTL-formula st len H <= n holds
f1 . H = f2 . H )
defpred S1[ Element of NAT ] means ( f1 is-PreEvaluation-for $1,Kai & f2 is-PreEvaluation-for $1,Kai implies for H being CTL-formula st len H <= $1 holds
f1 . H = f2 . H );
A1:
S1[ 0 ]
by Lm10;
A2:
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 A3:
S1[
k]
;
:: thesis: S1[k + 1]
assume that A4:
f1 is-PreEvaluation-for k + 1,
Kai
and A5:
f2 is-PreEvaluation-for k + 1,
Kai
;
:: thesis: for H being CTL-formula st len H <= k + 1 holds
f1 . H = f2 . H
let H be
CTL-formula;
:: thesis: ( len H <= k + 1 implies f1 . H = f2 . H )
assume A6:
len H <= k + 1
;
:: thesis: f1 . H = f2 . H
per cases
( H is atomic or H is negative or H is ExistNext or H is ExistGlobal or H is conjunctive or H is ExistUntill )
by Th2;
suppose A8:
H is
negative
;
:: thesis: f1 . H = f2 . Hthen
len (the_argument_of H) < len H
by Lm22;
then A9:
len (the_argument_of H) <= k
by A6, Lm1;
f2 . H =
the
Not of
V . (f2 . (the_argument_of H))
by A5, A6, A8, Def27
.=
the
Not of
V . (f1 . (the_argument_of H))
by A3, A4, A5, A9, Lm25
;
hence
f1 . H = f2 . H
by A4, A6, A8, Def27;
:: thesis: verum end; suppose A10:
H is
ExistNext
;
:: thesis: f1 . H = f2 . Hthen
len (the_argument_of H) < len H
by Lm22;
then A11:
len (the_argument_of H) <= k
by A6, Lm1;
f2 . H =
the
EneXt of
V . (f2 . (the_argument_of H))
by A5, A6, A10, Def27
.=
the
EneXt of
V . (f1 . (the_argument_of H))
by A3, A4, A5, A11, Lm25
;
hence
f1 . H = f2 . H
by A4, A6, A10, Def27;
:: thesis: verum end; suppose A12:
H is
ExistGlobal
;
:: thesis: f1 . H = f2 . Hthen
len (the_argument_of H) < len H
by Lm22;
then A13:
len (the_argument_of H) <= k
by A6, Lm1;
f2 . H =
the
EGlobal of
V . (f2 . (the_argument_of H))
by A5, A6, A12, Def27
.=
the
EGlobal of
V . (f1 . (the_argument_of H))
by A3, A4, A5, A13, Lm25
;
hence
f1 . H = f2 . H
by A4, A6, A12, Def27;
:: thesis: verum end; suppose A14:
H is
conjunctive
;
:: thesis: f1 . H = f2 . Hthen
len (the_left_argument_of H) < len H
by Lm23;
then
len (the_left_argument_of H) <= k
by A6, Lm1;
then A15:
f1 . (the_left_argument_of H) = f2 . (the_left_argument_of H)
by A3, A4, A5, Lm25;
len (the_right_argument_of H) < len H
by A14, Lm23;
then A16:
len (the_right_argument_of H) <= k
by A6, Lm1;
f2 . H =
the
And of
V . (f2 . (the_left_argument_of H)),
(f2 . (the_right_argument_of H))
by A5, A6, A14, Def27
.=
the
And of
V . (f1 . (the_left_argument_of H)),
(f1 . (the_right_argument_of H))
by A3, A4, A5, A15, A16, Lm25
;
hence
f1 . H = f2 . H
by A4, A6, A14, Def27;
:: thesis: verum end; suppose A17:
H is
ExistUntill
;
:: thesis: f1 . H = f2 . Hthen
len (the_left_argument_of H) < len H
by Lm23;
then
len (the_left_argument_of H) <= k
by A6, Lm1;
then A18:
f1 . (the_left_argument_of H) = f2 . (the_left_argument_of H)
by A3, A4, A5, Lm25;
len (the_right_argument_of H) < len H
by A17, Lm23;
then A19:
len (the_right_argument_of H) <= k
by A6, Lm1;
f2 . H =
the
EUntill of
V . (f2 . (the_left_argument_of H)),
(f2 . (the_right_argument_of H))
by A5, A6, A17, Def27
.=
the
EUntill of
V . (f1 . (the_left_argument_of H)),
(f1 . (the_right_argument_of H))
by A3, A4, A5, A18, A19, Lm25
;
hence
f1 . H = f2 . H
by A4, A6, A17, Def27;
:: thesis: verum end;
end;
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A1, A2);
hence
( f1 is-PreEvaluation-for n,Kai & f2 is-PreEvaluation-for n,Kai implies for H being CTL-formula st len H <= n holds
f1 . H = f2 . H )
; :: thesis: verum