:: Model Checking, Part {I}
:: by Kazuhisa Ishida
::
:: Received November 14, 2006
:: Copyright (c) 2006-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, NAT_1, ARYTM_3, XXREAL_0, SUBSET_1, CARD_1, FUNCT_1,
RELAT_1, XBOOLEAN, TARSKI, XBOOLE_0, FINSEQ_1, ZF_LANG, ORDINAL4,
PARTFUN1, ZFMISC_1, BINOP_1, FUNCOP_1, FUNCT_2, FUNCT_7, ORDERS_1,
MARGREL1, ZF_MODEL, ARYTM_1, FUNCT_3, COHSP_1, ABIAN, KNASTER, MODELC_1,
STRUCT_0, ORDERS_2, FUNCT_5, ROBBINS1, LATTICES;
notations RELSET_1, RELAT_1, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1,
NUMBERS, XCMPLX_0, NAT_1, FUNCT_1, FUNCT_2, FUNCT_3, FUNCT_7, BINOP_1,
FINSEQ_1, PARTFUN1, KNASTER, XXREAL_0, ABIAN, ORDERS_1, FUNCOP_1,
MARGREL1, FUNCT_5, STRUCT_0, ORDERS_2, LATTICES, ROBBINS1;
constructors BINOP_1, FUNCT_3, REAL_1, NAT_1, MARGREL1, ABIAN, KNASTER,
RELSET_1, FUNCT_5, ROBBINS1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, ORDINAL1, PARTFUN1, XXREAL_0,
XREAL_0, NAT_1, INT_1, XBOOLEAN, MARGREL1, KNASTER, CARD_1, RELSET_1,
STRUCT_0;
requirements REAL, NUMERALS, ARITHM, SUBSET, BOOLE;
definitions TARSKI;
equalities RELAT_1, BINOP_1, MARGREL1, XBOOLEAN, ROBBINS1, LATTICES;
expansions TARSKI;
theorems RELSET_1, XBOOLE_0, ZFMISC_1, XBOOLE_1, TARSKI, FUNCT_1, FUNCT_2,
FUNCT_3, FUNCT_7, PARTFUN1, RELAT_1, NAT_1, INT_1, KNASTER, XREAL_1,
ABIAN, FINSEQ_1, ORDERS_1, FUNCOP_1, XXREAL_0, RELSET_2, MARGREL1,
FINSEQ_5, XBOOLEAN, ORDINAL1, XTUPLE_0;
schemes NAT_1, FUNCT_2, XBOOLE_0, BINOP_1, BINOP_2, XFAMILY;
begin
:: definition of CTL(Computation Tree Logic) language.
:: refer to (reuse) construction & proof of ZF_LANG
Lm1: for m,n,k be Nat st m < n & n <= k+1 holds m <= k
proof
let m,n,k be Nat;
assume that
A1: m < n and
A2: n <= k+1;
m+1 <= n by A1,NAT_1:13;
then m+1<=k+1 by A2,XXREAL_0:2;
hence thesis by XREAL_1:6;
end;
definition
let x be object, S be set; :: !!! zastapic przez In(.,.)
let a be Element of S;
func k_id(x,S,a) -> Element of S equals
:Def1:
x if x in S otherwise a;
correctness;
end;
definition
let x be object;
func k_nat(x) -> Element of NAT equals
:Def2:
x if x in NAT otherwise 0;
correctness;
end;
definition
let f be Function;
let x,a be set;
func UnivF(x,f,a) -> set equals
:Def3:
f.x if x in dom f otherwise a;
correctness;
end;
definition
let a be set;
func Castboolean(a) -> boolean object equals
:Def4:
a if a is boolean
otherwise FALSE;
correctness;
end;
definition
let X be set, a be object; :: zastapic przez In(.,.) !!!
func CastBool(a,X) -> Subset of X equals
:Def5:
a if a in bool X otherwise {};
correctness by XBOOLE_1:2;
end;
reserve k,n for Element of NAT,
a,Y for set,
D,D1,D2 for non empty set,
p,q for FinSequence of NAT;
:: The operations to make CTL-formulae
definition
let n;
func atom.n -> FinSequence of NAT equals
<* (5 + n) *>;
coherence;
end;
definition
let p;
func 'not' p -> FinSequence of NAT equals
<*0*>^p;
coherence;
let q;
func p '&' q -> FinSequence of NAT equals
<*1*>^p^q;
coherence;
end;
definition
let p;
func EX p -> FinSequence of NAT equals
<*2*>^p;
coherence;
func EG p -> FinSequence of NAT equals
<*3*>^p;
coherence;
let q;
func p EU q -> FinSequence of NAT equals
<*4*>^p^q;
coherence;
end;
Lm2: len(<*n*>^p^q) = 1+len(p)+len(q)
proof
len(p^q) = len(p)+len(q) by FINSEQ_1:22;
then
A1: len(<*n*>)+len(p^q) = len(<*n*>)+len(p)+len(q);
len(<*n*>^p^q) = len(<*n*>^(p^q)) by FINSEQ_1:32
.= len(<*n*>)+len(p^q) by FINSEQ_1:22;
hence thesis by A1,FINSEQ_1:40;
end;
:: The set of all well formed formulae of CTL-language
definition
func CTL_WFF -> non empty set means
:Def12:
(for a st a in it holds a is
FinSequence of NAT ) & (for n holds atom.n in it ) & (for p st p in it holds
'not' p in it ) & (for p,q st p in it & q in it holds p '&' q in it ) & (for p
st p in it holds EX p in it ) & (for p st p in it holds EG p in it ) & (for p,q
st p in it & q in it holds p EU q in it ) & for D st (for a st a in D holds a
is FinSequence of NAT ) & (for n holds atom.n in D ) & (for p st p in D holds
'not' p in D ) & (for p,q st p in D & q in D holds p '&' q in D ) & (for p st p
in D holds EX p in D ) & (for p st p in D holds EG p in D ) & (for p,q st p in
D & q in D holds p EU q in D ) holds it c= D;
existence
proof
defpred P[set] means (for a st a in $1 holds a is FinSequence of NAT ) & (
for n holds atom.n in $1 ) & (for p st p in $1 holds 'not' p in $1 ) & (for p,q
st p in $1 & q in $1 holds p '&' q in $1 ) & (for p st p in $1 holds EX p in $1
) & (for p st p in $1 holds EG p in $1 ) & (for p,q st p in $1 & q in $1 holds
p EU q in $1 );
defpred Q[object] means for D st P[D] holds $1 in D;
consider Y such that
A1: for a being object holds a in Y iff a in NAT* & Q[a] from XBOOLE_0:sch 1;
now
set a = atom.0;
A2: for D st P[D] holds a in D;
take b = a;
a in NAT* by FINSEQ_1:def 11;
hence b in Y by A1,A2;
end;
then reconsider Y as non empty set;
take Y;
thus a in Y implies a is FinSequence of NAT
proof
assume a in Y;
then a in NAT* by A1;
hence thesis by FINSEQ_1:def 11;
end;
thus atom.n in Y
proof
A3: for D st P[D] holds atom.n in D;
atom.n in NAT* by FINSEQ_1:def 11;
hence thesis by A1,A3;
end;
thus p in Y implies 'not' p in Y
proof
assume
A4: p in Y;
A5: for D st P[D] holds 'not' p in D
proof
let D;
assume
A6: P[D];
then p in D by A1,A4;
hence thesis by A6;
end;
'not' p in NAT* by FINSEQ_1:def 11;
hence thesis by A1,A5;
end;
thus for q,p holds q in Y & p in Y implies q '&' p in Y
proof
let q,p;
assume that
A7: q in Y and
A8: p in Y;
A9: for D st P[D] holds q '&' p in D
proof
let D;
assume
A10: P[D];
then
A11: q in D by A1,A7;
p in D by A1,A8,A10;
hence thesis by A10,A11;
end;
q '&' p in NAT* by FINSEQ_1:def 11;
hence thesis by A1,A9;
end;
thus p in Y implies EX p in Y
proof
assume
A12: p in Y;
A13: for D st P[D] holds EX p in D
proof
let D;
assume
A14: P[D];
then p in D by A1,A12;
hence thesis by A14;
end;
EX p in NAT* by FINSEQ_1:def 11;
hence thesis by A1,A13;
end;
thus p in Y implies EG p in Y
proof
assume
A15: p in Y;
A16: for D st P[D] holds EG p in D
proof
let D;
assume
A17: P[D];
then p in D by A1,A15;
hence thesis by A17;
end;
EG p in NAT* by FINSEQ_1:def 11;
hence thesis by A1,A16;
end;
thus for q,p holds q in Y & p in Y implies q EU p in Y
proof
let q,p;
assume that
A18: q in Y and
A19: p in Y;
A20: for D st P[D] holds q EU p in D
proof
let D;
assume
A21: P[D];
then
A22: q in D by A1,A18;
p in D by A1,A19,A21;
hence thesis by A21,A22;
end;
q EU p in NAT* by FINSEQ_1:def 11;
hence thesis by A1,A20;
end;
let D such that
A23: P[D];
let a be object;
assume a in Y;
hence thesis by A1,A23;
end;
uniqueness
proof
let D1,D2 such that
A24: for a st a in D1 holds a is FinSequence of NAT and
A25: for n holds atom.n in D1 and
A26: for p st p in D1 holds 'not' p in D1 and
A27: for p,q st p in D1 & q in D1 holds p '&' q in D1 and
A28: for p st p in D1 holds EX p in D1 and
A29: for p st p in D1 holds EG p in D1 and
A30: for p,q st p in D1 & q in D1 holds p EU q in D1 and
A31: for D st (for a st a in D holds a is FinSequence of NAT ) & (for
n holds atom.n in D ) & (for p st p in D holds 'not' p in D ) & (for p,q st p
in D & q in D holds p '&' q in D ) & (for p st p in D holds EX p in D ) & (for
p st p in D holds EG p in D ) & (for p,q st p in D & q in D holds p EU q in D )
holds D1 c= D and
A32: for a st a in D2 holds a is FinSequence of NAT and
A33: for n holds atom.n in D2 and
A34: for p st p in D2 holds 'not' p in D2 and
A35: for p,q st p in D2 & q in D2 holds p '&' q in D2 and
A36: for p st p in D2 holds EX p in D2 and
A37: for p st p in D2 holds EG p in D2 and
A38: for p,q st p in D2 & q in D2 holds p EU q in D2 and
A39: for D st (for a st a in D holds a is FinSequence of NAT ) & (for
n holds atom.n in D ) & (for p st p in D holds 'not' p in D ) & (for p,q st p
in D & q in D holds p '&' q in D ) & (for p st p in D holds EX p in D ) & (for
p st p in D holds EG p in D ) & (for p,q st p in D & q in D holds p EU q in D )
holds D2 c= D;
A40: D2 c= D1 by A24,A25,A26,A27,A28,A29,A30,A39;
D1 c= D2 by A31,A32,A33,A34,A35,A36,A37,A38;
hence thesis by A40,XBOOLE_0:def 10;
end;
end;
definition
let IT be FinSequence of NAT;
attr IT is CTL-formula-like means
:Def13:
IT is Element of CTL_WFF;
end;
registration
cluster CTL-formula-like for FinSequence of NAT;
existence
proof
set x = the Element of CTL_WFF;
reconsider x as FinSequence of NAT by Def12;
take x;
thus x is Element of CTL_WFF;
end;
end;
definition
mode CTL-formula is CTL-formula-like FinSequence of NAT;
end;
theorem Th1:
a is CTL-formula iff a in CTL_WFF
proof
thus a is CTL-formula implies a in CTL_WFF
proof
assume a is CTL-formula;
then a is Element of CTL_WFF by Def13;
hence thesis;
end;
assume a in CTL_WFF;
hence thesis by Def12,Def13;
end;
reserve F,F1,G,G1,H,H1,H2 for CTL-formula;
registration
let n;
cluster atom.n -> CTL-formula-like;
coherence
by Def12;
end;
registration
let H;
cluster 'not' H -> CTL-formula-like;
coherence
proof
H is Element of CTL_WFF by Def13;
then 'not' H is Element of CTL_WFF by Def12;
hence thesis;
end;
cluster EX H -> CTL-formula-like;
coherence
proof
H is Element of CTL_WFF by Def13;
then EX H is Element of CTL_WFF by Def12;
hence thesis;
end;
cluster EG H -> CTL-formula-like;
coherence
proof
H is Element of CTL_WFF by Def13;
then EG H is Element of CTL_WFF by Def12;
hence thesis;
end;
let G;
cluster H '&' G -> CTL-formula-like;
coherence
proof
A1: G is Element of CTL_WFF by Def13;
H is Element of CTL_WFF by Def13;
then H '&' G is Element of CTL_WFF by A1,Def12;
hence thesis;
end;
cluster H EU G -> CTL-formula-like;
coherence
proof
A2: G is Element of CTL_WFF by Def13;
H is Element of CTL_WFF by Def13;
then H EU G is Element of CTL_WFF by A2,Def12;
hence thesis;
end;
end;
definition
let H;
attr H is atomic means
ex n st H = atom.n;
attr H is negative means
ex H1 st H = 'not' H1;
attr H is conjunctive means
ex F,G st H = F '&' G;
attr H is ExistNext means
ex H1 st H = EX H1;
attr H is ExistGlobal means
ex H1 st H = EG H1;
attr H is ExistUntill means
ex F,G st H = F EU G;
end;
definition
let F,G;
func F 'or' G -> CTL-formula equals
'not'('not' F '&' 'not' G);
coherence;
end;
theorem Th2:
H is atomic or H is negative or H is conjunctive or H is
ExistNext or H is ExistGlobal or H is ExistUntill
proof
A1: H is Element of CTL_WFF by Def13;
assume
A2: not thesis;
then atom.0 <> H;
then
A3: not atom.0 in { H } by TARSKI:def 1;
A4: now
let p;
assume
A5: p in CTL_WFF \ { H };
then reconsider H1 = p as CTL-formula by Def13;
EG H1 <> H by A2;
then
A6: not EG p in { H } by TARSKI:def 1;
EG p in CTL_WFF by A5,Def12;
hence EG p in CTL_WFF \ { H } by A6,XBOOLE_0:def 5;
end;
A7: now
let p;
assume
A8: p in CTL_WFF \ { H };
then reconsider H1 = p as CTL-formula by Def13;
EX H1 <> H by A2;
then
A9: not EX p in { H } by TARSKI:def 1;
EX p in CTL_WFF by A8,Def12;
hence EX p in CTL_WFF \ { H } by A9,XBOOLE_0:def 5;
end;
A10: now
let p,q;
assume that
A11: p in CTL_WFF \ { H } and
A12: q in CTL_WFF \ { H };
reconsider F = p, G = q as CTL-formula by A11,A12,Def13;
F '&' G <> H by A2;
then
A13: not p '&' q in { H } by TARSKI:def 1;
p '&' q in CTL_WFF by A11,A12,Def12;
hence p '&' q in CTL_WFF \ { H } by A13,XBOOLE_0:def 5;
end;
A14: now
let p;
assume
A15: p in CTL_WFF \ { H };
then reconsider H1 = p as CTL-formula by Def13;
'not' H1 <> H by A2;
then
A16: not 'not' p in { H } by TARSKI:def 1;
'not' p in CTL_WFF by A15,Def12;
hence 'not' p in CTL_WFF \ { H } by A16,XBOOLE_0:def 5;
end;
A17: now
let p,q;
assume that
A18: p in CTL_WFF \ { H } and
A19: q in CTL_WFF \ { H };
reconsider F = p, G = q as CTL-formula by A18,A19,Def13;
F EU G <> H by A2;
then
A20: not p EU q in { H } by TARSKI:def 1;
p EU q in CTL_WFF by A18,A19,Def12;
hence p EU q in CTL_WFF \ { H } by A20,XBOOLE_0:def 5;
end;
A21: now
let n;
atom.n <> H by A2;
then
A22: not atom.n in { H } by TARSKI:def 1;
atom.n in CTL_WFF by Def12;
hence atom.n in CTL_WFF \ { H } by A22,XBOOLE_0:def 5;
end;
atom.0 in CTL_WFF by Def12;
then
A23: CTL_WFF \ { H } is non empty by A3,XBOOLE_0:def 5;
for a st a in CTL_WFF \ { H } holds a is FinSequence of NAT by Def12;
then CTL_WFF c= CTL_WFF \ { H } by A23,A21,A14,A10,A7,A4,A17,Def12;
then H in CTL_WFF \ { H } by A1;
then not H in { H } by XBOOLE_0:def 5;
hence contradiction by TARSKI:def 1;
end;
Lm3: H is negative implies H.1 = 0
by FINSEQ_1:41;
Lm4: H is conjunctive implies H.1 = 1
proof
assume H is conjunctive;
then consider F,G such that
A1: H = F '&' G;
<*1*>^F^G = <*1*>^(F^G) by FINSEQ_1:32;
hence thesis by A1,FINSEQ_1:41;
end;
Lm5: H is ExistNext implies H.1 = 2
by FINSEQ_1:41;
Lm6: H is ExistGlobal implies H.1 = 3
by FINSEQ_1:41;
Lm7: H is ExistUntill implies H.1 = 4
proof
assume H is ExistUntill;
then consider F,G such that
A1: H = F EU G;
<*4*>^F^G = <*4*>^(F^G) by FINSEQ_1:32;
hence thesis by A1,FINSEQ_1:41;
end;
Lm8: H is atomic implies not H.1 = 0 & not H.1 = 1 & not H.1 = 2 & not H.1 = 3
& not H.1 = 4
proof
assume H is atomic;
then consider n such that
A1: H = atom.n;
A2: 2+0<2+(3+n) by XREAL_1:8;
A3: 4+0<4+(1+n) by XREAL_1:8;
A4: 3+0<3+(2+n) by XREAL_1:8;
1+0<1+(4+n) by XREAL_1:8;
hence thesis by A1,A2,A4,A3,FINSEQ_1:40;
end;
Lm9: H is atomic & H.1 <> 0 & H.1 <> 1 & H.1 <> 2 & H.1 <> 3 & H.1 <> 4 or H
is negative & H.1 = 0 or H is conjunctive & H.1 = 1 or H is ExistNext & H.1 = 2
or H is ExistGlobal & H.1 = 3 or H is ExistUntill & H.1 = 4
proof
per cases by Th2;
case
H is atomic;
hence thesis by Lm8;
end;
case
H is negative;
hence thesis by Lm3;
end;
case
H is conjunctive;
hence thesis by Lm4;
end;
case
H is ExistNext;
hence thesis by Lm5;
end;
case
H is ExistGlobal;
hence thesis by Lm6;
end;
case
H is ExistUntill;
hence thesis by Lm7;
end;
end;
Lm10: 1<= len H
proof
per cases by Th2;
suppose
H is atomic;
then ex n st H = atom.n;
hence thesis by FINSEQ_1:40;
end;
suppose
H is negative;
then consider H1 such that
A1: H = 'not' H1;
len(H) = 1+len(H1) by A1,FINSEQ_5:8;
hence thesis by NAT_1:11;
end;
suppose
H is conjunctive;
then consider F,G such that
A2: H = F '&' G;
A3: 1 <= 1+len(F) by NAT_1:11;
A4: 1+len(F) <= 1+len(F)+len(G) by NAT_1:11;
len(H) = 1+len(F)+len(G) by A2,Lm2;
hence thesis by A3,A4,XXREAL_0:2;
end;
suppose
H is ExistNext;
then consider H1 such that
A5: H = EX H1;
len(H) = 1+len(H1) by A5,FINSEQ_5:8;
hence thesis by NAT_1:11;
end;
suppose
H is ExistGlobal;
then consider H1 such that
A6: H = EG H1;
len(H) = 1+len(H1) by A6,FINSEQ_5:8;
hence thesis by NAT_1:11;
end;
suppose
H is ExistUntill;
then consider F,G such that
A7: H = F EU G;
A8: 1 <= 1+len(F) by NAT_1:11;
A9: 1+len(F) <= 1+len(F)+len(G) by NAT_1:11;
len(H) = 1+len(F)+len(G) by A7,Lm2;
hence thesis by A8,A9,XXREAL_0:2;
end;
end;
reserve sq,sq9 for FinSequence;
Lm11: H = F^sq implies H = F
proof
defpred P[Nat] means for H,F,sq st len H = $1 & H = F^sq holds H = F;
for n being Nat st (for k being Nat st k < n for H,F,sq st len H = k & H
= F^sq holds H = F) for H,F,sq st len H = n & H = F^sq holds H = F
proof
let n be Nat such that
A1: for k be Nat st k < n for H,F,sq st len H = k & H = F^sq holds H = F;
let H,F,sq such that
A2: len H = n and
A3: H = F^sq;
A4: dom F = Seg len F by FINSEQ_1:def 3;
1 <= len F by Lm10;
then
A5: 1 in dom F by A4,FINSEQ_1:1;
A6: now
A7: len <*0*>= 1 by FINSEQ_1:40;
assume
A8: H is negative;
then consider H1 such that
A9: H = 'not' H1;
(F^sq).1 = 0 by A3,A8,Lm3;
then F.1 = 0 by A5,FINSEQ_1:def 7;
then F is negative by Lm9;
then consider F1 such that
A10: F = 'not' F1;
len <*0*> + len H1 = len H by A9,FINSEQ_1:22;
then
A11: len H1 < len H by A7,NAT_1:13;
<*0*>^F1^sq = <*0*>^(F1^sq) by FINSEQ_1:32;
then H1 = F1^sq by A3,A9,A10,FINSEQ_1:33;
hence thesis by A1,A2,A9,A10,A11;
end;
A12: now
A13: len <*4*> = 1 by FINSEQ_1:40;
assume
A14: H is ExistUntill;
then consider G1,G such that
A15: H = G1 EU G;
(F^sq).1 = 4 by A3,A14,Lm7;
then F.1 = 4 by A5,FINSEQ_1:def 7;
then F is ExistUntill by Lm9;
then consider F1,H1 such that
A16: F = F1 EU H1;
A17: len G + (1 + len G1) = len G + 1 + len G1;
A18: len(<*4*>^G1) = len <*4*> + len G1 by FINSEQ_1:22;
len(<*4*>^G1) + len G = len H by A15,FINSEQ_1:22;
then len G + 1 <= len H by A18,A13,A17,NAT_1:11;
then
A19: len G < len H by NAT_1:13;
A20: F1^H1^sq = F1^(H1^sq) by FINSEQ_1:32;
A21: now
A22: len <*4*> = 1 by FINSEQ_1:40;
given sq9 such that
A23: G1 = F1^sq9;
A24: len(<*4*>^G1) = len <*4*> + len G1 by FINSEQ_1:22;
len(<*4*>^G1) + len G = len H by A15,FINSEQ_1:22;
then len G1 + 1 <= len H by A24,A22,NAT_1:11;
then len G1 < len H by NAT_1:13;
hence G1 = F1 by A1,A2,A23;
end;
A25: <*4*>^(F1^H1)^sq = <*4*>^(F1^H1^sq) by FINSEQ_1:32;
A26: now
A27: len <*4*> = 1 by FINSEQ_1:40;
A28: len(<*4*>^F1) = len <*4*> + len F1 by FINSEQ_1:22;
A29: len F1 + 1 + len H1 + len sq = len F1 + 1 + (len H1 + len sq);
given sq9 such that
A30: F1 = G1^sq9;
A31: len(F^sq) = len F + len sq by FINSEQ_1:22;
len F = len(<*4*>^F1) + len H1 by A16,FINSEQ_1:22;
then len F1 + 1 <= len H by A3,A31,A28,A27,A29,NAT_1:11;
then len F1 < len H by NAT_1:13;
hence F1 = G1 by A1,A2,A30;
end;
A32: <*4*>^F1^H1 = <*4*>^(F1^H1) by FINSEQ_1:32;
<*4*>^G1^G = <*4*>^(G1^G) by FINSEQ_1:32;
then
A33: G1^G = F1^(H1^sq) by A3,A15,A16,A32,A25,A20,FINSEQ_1:33;
then len F1 <= len G1 implies ex sq9 st G1 = F1^sq9 by FINSEQ_1:47;
then G = H1^sq by A33,A21,A26,FINSEQ_1:33,47;
hence thesis by A1,A2,A3,A16,A32,A25,A20,A19;
end;
A34: now
A35: len <*1*> = 1 by FINSEQ_1:40;
assume
A36: H is conjunctive;
then consider G1,G such that
A37: H = G1 '&' G;
(F^sq).1 = 1 by A3,A36,Lm4;
then F.1 = 1 by A5,FINSEQ_1:def 7;
then F is conjunctive by Lm9;
then consider F1,H1 such that
A38: F = F1 '&' H1;
A39: len G + (1 + len G1) = len G + 1 + len G1;
A40: len(<*1*>^G1) = len <*1*> + len G1 by FINSEQ_1:22;
len(<*1*>^G1) + len G = len H by A37,FINSEQ_1:22;
then len G + 1 <= len H by A40,A35,A39,NAT_1:11;
then
A41: len G < len H by NAT_1:13;
A42: F1^H1^sq = F1^(H1^sq) by FINSEQ_1:32;
A43: now
A44: len <*1*> = 1 by FINSEQ_1:40;
given sq9 such that
A45: G1 = F1^sq9;
A46: len(<*1*>^G1) = len <*1*> + len G1 by FINSEQ_1:22;
len(<*1*>^G1) + len G = len H by A37,FINSEQ_1:22;
then len G1 + 1 <= len H by A46,A44,NAT_1:11;
then len G1 < len H by NAT_1:13;
hence G1 = F1 by A1,A2,A45;
end;
A47: <*1*>^(F1^H1)^sq = <*1*>^(F1^H1^sq) by FINSEQ_1:32;
A48: now
A49: len(<*1*>^F1) = len <*1*> + len F1 by FINSEQ_1:22;
A50: len <*1*> = 1 by FINSEQ_1:40;
A51: len F1 + 1 + len H1 + len sq = len F1 + 1 + (len H1 + len sq);
given sq9 such that
A52: F1 = G1^sq9;
A53: len(F^sq) = len F + len sq by FINSEQ_1:22;
len F = len(<*1*>^F1) + len H1 by A38,FINSEQ_1:22;
then len F1 + 1 <= len H by A3,A53,A50,A49,A51,NAT_1:11;
then len F1 < len H by NAT_1:13;
hence F1 = G1 by A1,A2,A52;
end;
A54: <*1*>^F1^H1 = <*1*>^(F1^H1) by FINSEQ_1:32;
<*1*>^G1^G = <*1*>^(G1^G) by FINSEQ_1:32;
then
A55: G1^G = F1^(H1^sq) by A3,A37,A38,A54,A47,A42,FINSEQ_1:33;
then len F1 <= len G1 implies ex sq9 st G1 = F1^sq9 by FINSEQ_1:47;
then G = H1^sq by A55,A43,A48,FINSEQ_1:33,47;
hence thesis by A1,A2,A3,A38,A54,A47,A42,A41;
end;
A56: now
A57: len <*3*>= 1 by FINSEQ_1:40;
assume
A58: H is ExistGlobal;
then consider H1 such that
A59: H = EG H1;
(F^sq).1 = 3 by A3,A58,Lm6;
then F.1 = 3 by A5,FINSEQ_1:def 7;
then F is ExistGlobal by Lm9;
then consider F1 such that
A60: F = EG F1;
len <*3*> + len H1 = len H by A59,FINSEQ_1:22;
then
A61: len H1 < len H by A57,NAT_1:13;
<*3*>^F1^sq = <*3*>^(F1^sq) by FINSEQ_1:32;
then H1 = F1^sq by A3,A59,A60,FINSEQ_1:33;
hence thesis by A1,A2,A59,A60,A61;
end;
A62: now
A63: len <*2*>= 1 by FINSEQ_1:40;
assume
A64: H is ExistNext;
then consider H1 such that
A65: H = EX H1;
(F^sq).1 = 2 by A3,A64,Lm5;
then F.1 = 2 by A5,FINSEQ_1:def 7;
then F is ExistNext by Lm9;
then consider F1 such that
A66: F = EX F1;
len <*2*> + len H1 = len H by A65,FINSEQ_1:22;
then
A67: len H1 < len H by A63,NAT_1:13;
<*2*>^F1^sq = <*2*>^(F1^sq) by FINSEQ_1:32;
then H1 = F1^sq by A3,A65,A66,FINSEQ_1:33;
hence thesis by A1,A2,A65,A66,A67;
end;
A68: len F + len sq = len(F^sq) by FINSEQ_1:22;
now
A69: 1 <= len F by Lm10;
assume H is atomic;
then ex k st H = atom.k;
then
A70: len(H) = 1 by FINSEQ_1:40;
then len F <= 1 by A3,A68,NAT_1:11;
then 1 + len sq = 1 + 0 by A3,A68,A70,A69,XXREAL_0:1;
then sq = {};
hence thesis by A3,FINSEQ_1:34;
end;
hence thesis by A6,A34,A62,A56,A12,Th2;
end;
then
A71: for k being Nat st for n being Nat st n < k holds P[n] holds P[k];
A72: for n being Nat holds P[n] from NAT_1:sch 4(A71);
len H = len H;
hence thesis by A72;
end;
Lm12: H '&' G = H1 '&' G1 implies H = H1 & G = G1
proof
assume
A1: H '&' G = H1 '&' G1;
A2: <*1*>^H1^G1 = <*1*>^(H1^G1) by FINSEQ_1:32;
<*1*>^H^G = <*1*>^(H^G) by FINSEQ_1:32;
then
A3: H^G = H1^G1 by A1,A2,FINSEQ_1:33;
then
A4: len H1 <= len H implies ex sq st H = H1^sq by FINSEQ_1:47;
A5: len H <= len H1 implies ex sq st H1 = H^sq by A3,FINSEQ_1:47;
hence H = H1 by A4,Lm11;
(ex sq st H1 = H^sq) implies H1 = H by Lm11;
hence thesis by A1,A4,A5,Lm11,FINSEQ_1:33;
end;
Lm13: H EU G = H1 EU G1 implies H = H1 & G = G1
proof
assume
A1: H EU G = H1 EU G1;
A2: <*4*>^H1^G1 = <*4*>^(H1^G1) by FINSEQ_1:32;
<*4*>^H^G = <*4*>^(H^G) by FINSEQ_1:32;
then
A3: H^G = H1^G1 by A1,A2,FINSEQ_1:33;
then
A4: len H1 <= len H implies ex sq st H = H1^sq by FINSEQ_1:47;
A5: len H <= len H1 implies ex sq st H1 = H^sq by A3,FINSEQ_1:47;
hence H = H1 by A4,Lm11;
(ex sq st H1 = H^sq) implies H1 = H by Lm11;
hence thesis by A1,A4,A5,Lm11,FINSEQ_1:33;
end;
Lm14: H is atomic implies (not H is negative) & (not H is conjunctive) & (not
H is ExistNext) & (not H is ExistGlobal) & not H is ExistUntill
proof
assume
A1: H is atomic;
then
A2: not H.1 = 1 by Lm8;
A3: not H.1 = 3 by A1,Lm8;
A4: not H.1 = 2 by A1,Lm8;
A5: not H.1 = 4 by A1,Lm8;
not H.1 = 0 by A1,Lm8;
hence thesis by A2,A4,A3,A5,Lm3,Lm4,Lm5,Lm6,Lm7;
end;
Lm15: H is negative implies (not H is atomic) & (not H is conjunctive) & (not
H is ExistNext) & (not H is ExistGlobal) & not H is ExistUntill
proof
assume H is negative;
then H.1=0 by Lm3;
hence thesis by Lm4,Lm5,Lm6,Lm7,Lm8;
end;
Lm16: H is conjunctive implies (not H is atomic) & (not H is negative) & (not
H is ExistNext) & (not H is ExistGlobal) & not H is ExistUntill
proof
assume H is conjunctive;
then H.1=1 by Lm4;
hence thesis by Lm3,Lm5,Lm6,Lm7,Lm8;
end;
Lm17: H is ExistNext implies (not H is atomic) & (not H is conjunctive) & (not
H is negative) & (not H is ExistGlobal) & not H is ExistUntill
proof
assume H is ExistNext;
then H.1=2 by Lm5;
hence thesis by Lm3,Lm4,Lm6,Lm7,Lm8;
end;
Lm18: H is ExistGlobal implies (not H is atomic) & (not H is conjunctive) & (
not H is negative) & (not H is ExistNext) & not H is ExistUntill
proof
assume H is ExistGlobal;
then H.1=3 by Lm6;
hence thesis by Lm3,Lm4,Lm5,Lm7,Lm8;
end;
definition
let H;
assume
A1: H is negative or H is ExistNext or H is ExistGlobal;
func the_argument_of H -> CTL-formula means
:Def21:
'not' it = H if H is
negative, EX it = H if H is ExistNext otherwise EG it = H;
existence by A1;
uniqueness by FINSEQ_1:33;
consistency by Lm15;
end;
definition
let H;
assume
A1: H is conjunctive or H is ExistUntill;
func the_left_argument_of H -> CTL-formula means
:Def22:
ex H1 st it '&' H1 = H if H is conjunctive otherwise ex H1 st it EU H1 = H;
existence by A1;
uniqueness by Lm12,Lm13;
consistency;
func the_right_argument_of H -> CTL-formula means
:Def23:
ex H1 st H1 '&' it = H if H is conjunctive otherwise ex H1 st H1 EU it = H;
existence
by A1;
uniqueness by Lm12,Lm13;
consistency;
end;
Lm19: H is ExistGlobal implies H = EG the_argument_of H
proof
assume
A1: H is ExistGlobal;
then
A2: not H is ExistNext by Lm18;
not H is negative by A1,Lm18;
hence thesis by A1,A2,Def21;
end;
Lm20: H is conjunctive implies H =(the_left_argument_of H) '&' (
the_right_argument_of H)
proof
assume
A1: H is conjunctive;
then ex H1 st H = H1 '&' the_right_argument_of H by Def23;
hence thesis by A1,Def22;
end;
Lm21: H is ExistUntill implies H = (the_left_argument_of H) EU (
the_right_argument_of H)
proof
assume
A1: H is ExistUntill;
then H.1 = 4 by Lm7;
then
A2: not H is conjunctive by Lm4;
then ex H1 st H = H1 EU the_right_argument_of H by A1,Def23;
hence thesis by A1,A2,Def22;
end;
Lm22: H is negative or H is ExistNext or H is ExistGlobal implies len(
the_argument_of H) < len(H)
proof
assume
A1: H is negative or H is ExistNext or H is ExistGlobal;
per cases by A1;
suppose
H is negative;
then H = 'not' the_argument_of H by Def21;
then len(H) = 1+len(the_argument_of H) by FINSEQ_5:8;
hence thesis by NAT_1:19;
end;
suppose
H is ExistNext;
then H = EX the_argument_of H by Def21;
then len(H) = 1+len(the_argument_of H) by FINSEQ_5:8;
hence thesis by NAT_1:19;
end;
suppose
H is ExistGlobal;
then H = EG the_argument_of H by Lm19;
then len(H) = 1+len(the_argument_of H) by FINSEQ_5:8;
hence thesis by NAT_1:19;
end;
end;
Lm23: H is conjunctive or H is ExistUntill implies len(the_left_argument_of H)
< len(H) & len(the_right_argument_of H) < len(H)
proof
set iL=len(the_left_argument_of H);
set iR=len(the_right_argument_of H);
set iR1=iR+1;
assume
A1: H is conjunctive or H is ExistUntill;
per cases by A1;
suppose
H is conjunctive;
then H = (the_left_argument_of H) '&' (the_right_argument_of H) by Lm20;
then
A2: len(H) = 1+iL+iR by Lm2;
1<=iR1 by NAT_1:11;
then
A3: iL < iL +iR1 by NAT_1:19;
1<=1+iL by NAT_1:11;
hence thesis by A2,A3,NAT_1:19;
end;
suppose
H is ExistUntill;
then H = the_left_argument_of H EU the_right_argument_of H by Lm21;
then
A4: len(H) = 1+iL+iR by Lm2;
1<=iR1 by NAT_1:11;
then
A5: iL < iL +iR1 by NAT_1:19;
1<=1+iL by NAT_1:11;
hence thesis by A4,A5,NAT_1:19;
end;
end;
definition
let x be object;
func CastCTLformula(x) -> CTL-formula equals
:Def24:
x if x in CTL_WFF
otherwise atom.0;
correctness by Th1;
end;
::***************************************************
::**
::** definition of Kripke structure & CTL model structure.
::**
::****************************************************
definition
let Prop be set;
struct(RelStr) KripkeStr over Prop (# carrier -> set,
Starts -> Subset of the carrier,
InternalRel -> Relation of the carrier, the carrier,
Label -> Function of the carrier, bool Prop #);
end;
definition
struct(ComplULattStr) CTLModelStr (# carrier -> set, BasicAssign ->
Subset of the carrier, L_meet -> BinOp of the carrier, Compl -> UnOp
of the carrier, EneXt -> UnOp of the carrier, EGlobal -> UnOp of the
carrier, EUntill -> BinOp of the carrier #);
end;
definition
let V be CTLModelStr;
mode Assign of V is Element of the carrier of V;
end;
:: Preparation to define semantics for CTL-language
:: definition of evaluate function of CTL
definition
func atomic_WFF -> Subset of CTL_WFF equals
{x where x is CTL-formula:x is atomic};
correctness
proof
set X = {x where x is CTL-formula:x is atomic};
X c= CTL_WFF
proof
let y be object;
assume y in X;
then ex x being CTL-formula st y=x & x is atomic;
hence thesis by Th1;
end;
hence thesis;
end;
end;
definition
let V be CTLModelStr;
let Kai be Function of atomic_WFF,the BasicAssign of V;
let f be Function of CTL_WFF,the carrier of V;
pred f is-Evaluation-for Kai means
for H being CTL-formula 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 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)));
end;
definition
let V be CTLModelStr;
let Kai be Function of atomic_WFF,the BasicAssign of V;
let f be Function of CTL_WFF,the carrier of V;
let n be Nat;
pred f is-PreEvaluation-for n,Kai means
:Def27:
for H being CTL-formula st
len(H) <= n 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 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)));
end;
definition
let V be CTLModelStr;
let Kai be Function of atomic_WFF,the BasicAssign of V;
let f,h be Function of CTL_WFF,the carrier of V;
let n be Nat;
let H be CTL-formula;
func GraftEval(V,Kai,f,h,n,H) -> set equals
:Def28:
f.H if len(H) > n+1, Kai
.H if len(H)=n+1 & H is atomic, (the Compl of V).(h.(the_argument_of H))
if len(H
)=n+1 & H is negative, (the L_meet of V).(h.(the_left_argument_of H), h.(
the_right_argument_of H)) if len(H)=n+1 & H is conjunctive, (the EneXt of V).(h
.(the_argument_of H)) if len(H)=n+1 & H is ExistNext , (the EGlobal of V).(h.(
the_argument_of H)) if len(H)=n+1 & H is ExistGlobal, (the EUntill of V).(h.(
the_left_argument_of H), h.(the_right_argument_of H)) if len(H)=n+1 & H is
ExistUntill, h.H if len(H)<n+1 otherwise {};
coherence;
consistency by Lm14,Lm15,Lm16,Lm17,Lm18;
end;
definition let C be CTLModelStr;
attr C is with_basic means
:Def29: the BasicAssign of C is non empty;
end;
definition
func TrivialCTLModel -> CTLModelStr equals
CTLModelStr(# {0}, [#]{0}, op2, op1, op1, op1, op2#);
coherence;
end;
registration
cluster TrivialCTLModel -> with_basic strict non empty;
coherence;
end;
registration
cluster non empty for CTLModelStr;
existence
proof
take TrivialCTLModel;
thus thesis;
end;
end;
registration
cluster with_basic for non empty CTLModelStr;
existence
proof
take TrivialCTLModel;
thus thesis;
end;
end;
definition
mode CTLModel is with_basic non empty CTLModelStr;
end;
registration let C be CTLModel;
cluster the BasicAssign of C -> non empty;
coherence by Def29;
end;
reserve V for CTLModel;
reserve Kai for Function of atomic_WFF,the BasicAssign of V;
reserve f,f1,f2 for Function of CTL_WFF,the carrier of V;
Lm24: f is-PreEvaluation-for 0,Kai
by Lm10;
Lm25:
for n being Nat holds
f is-PreEvaluation-for n+1,Kai implies f is-PreEvaluation-for n,Kai
proof let n be Nat;
assume
A1: f is-PreEvaluation-for n+1,Kai;
for H being CTL-formula st len(H) <= n 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 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;
assume len(H) <= n;
then len(H) < n+1 by NAT_1:13;
hence thesis by A1;
end;
hence thesis;
end;
Lm26:
for n being Nat holds
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
proof let n be Nat;
defpred P[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: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat such that
A2: P[k];
assume that
A3: f1 is-PreEvaluation-for k+1,Kai and
A4: f2 is-PreEvaluation-for k+1,Kai;
let H be CTL-formula such that
A5: len(H)<= k+1;
per cases by Th2;
suppose
A6: H is atomic;
then f1.H = Kai.H by A3,A5;
hence thesis by A4,A5,A6;
end;
suppose
A7: H is negative;
then len the_argument_of H < len(H) by Lm22;
then
A8: len the_argument_of H <= k by A5,Lm1;
f2.H = (the Compl of V).(f2.(the_argument_of H)) by A4,A5,A7
.= (the Compl of V).(f1.(the_argument_of H)) by A2,A3,A4,A8,Lm25;
hence thesis by A3,A5,A7;
end;
suppose
A9: H is ExistNext;
then len(the_argument_of H) < len(H) by Lm22;
then
A10: len(the_argument_of H) <= k by A5,Lm1;
f2.H = (the EneXt of V).(f2.(the_argument_of H)) by A4,A5,A9
.= (the EneXt of V).(f1.(the_argument_of H)) by A2,A3,A4,A10,Lm25;
hence thesis by A3,A5,A9;
end;
suppose
A11: H is ExistGlobal;
then len(the_argument_of H) < len(H) by Lm22;
then
A12: len(the_argument_of H) <= k by A5,Lm1;
f2.H = (the EGlobal of V).(f2.(the_argument_of H)) by A4,A5,A11
.= (the EGlobal of V).(f1.(the_argument_of H)) by A2,A3,A4,A12,Lm25;
hence thesis by A3,A5,A11;
end;
suppose
A13: H is conjunctive;
then len(the_left_argument_of H) < len(H) by Lm23;
then len(the_left_argument_of H) <= k by A5,Lm1;
then
A14: f1.(the_left_argument_of H) = f2.(the_left_argument_of H) by A2,A3,A4
,Lm25;
len(the_right_argument_of H) < len(H) by A13,Lm23;
then
A15: len(the_right_argument_of H) <= k by A5,Lm1;
f2.H = (the L_meet of V).(f2.(the_left_argument_of H), f2.(
the_right_argument_of H)) by A4,A5,A13
.= (the L_meet of V).(f1.(the_left_argument_of H), f1.(
the_right_argument_of H)) by A2,A3,A4,A14,A15,Lm25;
hence thesis by A3,A5,A13;
end;
suppose
A16: H is ExistUntill;
then len(the_left_argument_of H) < len(H) by Lm23;
then len(the_left_argument_of H) <= k by A5,Lm1;
then
A17: f1.(the_left_argument_of H) = f2.(the_left_argument_of H) by A2,A3,A4
,Lm25;
len(the_right_argument_of H) < len(H) by A16,Lm23;
then
A18: len(the_right_argument_of H) <= k by A5,Lm1;
f2.H = (the EUntill of V).(f2.(the_left_argument_of H), f2.(
the_right_argument_of H)) by A4,A5,A16
.= (the EUntill of V).(f1.(the_left_argument_of H), f1.(
the_right_argument_of H)) by A2,A3,A4,A17,A18,Lm25;
hence thesis by A3,A5,A16;
end;
end;
A19: P[0] by Lm10;
for n being Nat holds P[n] from NAT_1:sch 2(A19,A1);
hence thesis;
end;
Lm27: for n holds ex f st f is-PreEvaluation-for n,Kai
proof
defpred P[Nat] means ex f being Function of CTL_WFF,the
carrier of V st f is-PreEvaluation-for $1,Kai;
A1: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume P[k];
then consider h being Function of CTL_WFF,the carrier of V such that
A2: h is-PreEvaluation-for k,Kai;
P[k+1]
proof
deffunc F(object) =GraftEval(V,Kai,h,h,k,CastCTLformula($1));
A3: for H being object st H in CTL_WFF holds F(H) in the carrier of V
proof
let H be object such that
A4: H in CTL_WFF;
reconsider H as CTL-formula by A4,Th1;
A5: F(H)=GraftEval(V,Kai,h,h,k,H) by A4,Def24;
per cases by Th2,XXREAL_0:1;
suppose
len(H) > k+1;
then GraftEval(V,Kai,h,h,k,H)=h.H by Def28;
hence thesis by A4,A5,FUNCT_2:5;
end;
suppose
A6: len(H)=k+1 & H is atomic;
then H in atomic_WFF;
then Kai.H in the BasicAssign of V by FUNCT_2:5;
then Kai.H in the carrier of V;
hence thesis by A5,A6,Def28;
end;
suppose
A7: len(H)=k+1 & H is negative;
the_argument_of H in CTL_WFF by Th1;
then
A8: h.(the_argument_of H) in the carrier of V by FUNCT_2:5;
GraftEval(V,Kai,h,h,k,H) = (the Compl of V).(h.(the_argument_of H
)) by A7,Def28;
hence thesis by A5,A8,FUNCT_2:5;
end;
suppose
len(H)=k+1 & H is conjunctive;
then
A9: GraftEval(V,Kai,h,h,k,H) = (the L_meet of V).(h.(
the_left_argument_of H), h.(the_right_argument_of H)) by Def28;
the_right_argument_of H in CTL_WFF by Th1;
then
A10: h.(the_right_argument_of H) in the carrier of V by FUNCT_2:5;
the_left_argument_of H in CTL_WFF by Th1;
then h.(the_left_argument_of H) in the carrier of V by FUNCT_2:5;
then
[h.(the_left_argument_of H),h.(the_right_argument_of H )] in [:
the carrier of V,the carrier of V:] by A10,ZFMISC_1:def 2;
hence thesis by A5,A9,FUNCT_2:5;
end;
suppose
A11: len(H)=k+1 & H is ExistNext;
the_argument_of H in CTL_WFF by Th1;
then
A12: h.(the_argument_of H) in the carrier of V by FUNCT_2:5;
GraftEval(V,Kai,h,h,k,H) = (the EneXt of V).(h.(the_argument_of
H)) by A11,Def28;
hence thesis by A5,A12,FUNCT_2:5;
end;
suppose
A13: len(H)=k+1 & H is ExistGlobal;
the_argument_of H in CTL_WFF by Th1;
then
A14: h.(the_argument_of H) in the carrier of V by FUNCT_2:5;
GraftEval(V,Kai,h,h,k,H) = (the EGlobal of V).(h.(
the_argument_of H)) by A13,Def28;
hence thesis by A5,A14,FUNCT_2:5;
end;
suppose
len(H)=k+1 & H is ExistUntill;
then
A15: GraftEval(V,Kai,h,h,k,H) = (the EUntill of V).(h.(
the_left_argument_of H), h.(the_right_argument_of H)) by Def28;
the_right_argument_of H in CTL_WFF by Th1;
then
A16: h.(the_right_argument_of H) in the carrier of V by FUNCT_2:5;
the_left_argument_of H in CTL_WFF by Th1;
then h.(the_left_argument_of H) in the carrier of V by FUNCT_2:5;
then
[h.(the_left_argument_of H),h.(the_right_argument_of H )] in [:
the carrier of V,the carrier of V:] by A16,ZFMISC_1:def 2;
hence thesis by A5,A15,FUNCT_2:5;
end;
suppose
len(H) < k+1;
then GraftEval(V,Kai,h,h,k,H)=h.H by Def28;
hence thesis by A4,A5,FUNCT_2:5;
end;
end;
consider f be Function of CTL_WFF,the carrier of V such that
A17: for H being object st H in CTL_WFF holds f.H =F(H) from FUNCT_2:
sch 2(A3 );
take f;
A18: for H being CTL-formula st len(H) <k+1 holds f.H =h.H
proof
let H be CTL-formula such that
A19: len(H) < k+1;
A20: H in CTL_WFF by Th1;
then f.H = F(H) by A17
.=GraftEval(V,Kai,h,h,k,H) by A20,Def24;
hence thesis by A19,Def28;
end;
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 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 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 such that
A21: len(H) <= k+1;
A22: H in CTL_WFF by Th1;
then
A23: f.H = F(H) by A17
.=GraftEval(V,Kai,h,h,k,H) by A22,Def24;
A24: H is negative implies f.H = (the Compl of V).(f.(the_argument_of H) )
proof
assume
A25: H is negative;
then len(the_argument_of H) < len(H) by Lm22;
then len(the_argument_of H) <=k by A21,Lm1;
then
A26: len(the_argument_of H) < k+1 by NAT_1:13;
per cases by A21,NAT_1:8;
suppose
A27: len(H) <= k;
then len(H) < k+1 by NAT_1:13;
then f.H = h.H by A18
.= (the Compl of V).(h.(the_argument_of H)) by A2,A25,A27;
hence thesis by A18,A26;
end;
suppose
len(H) = k+1;
then
GraftEval(V,Kai,h,h,k,H) = (the Compl of V).(h.(the_argument_of
H)) by A25,Def28
.= (the Compl of V).(f.(the_argument_of H)) by A18,A26;
hence thesis by A23;
end;
end;
A28: H is ExistUntill implies f.H = (the EUntill of V).(f.(
the_left_argument_of H), f.(the_right_argument_of H))
proof
assume
A29: H is ExistUntill;
then len(the_right_argument_of H) < len(H) by Lm23;
then len(the_right_argument_of H) <=k by A21,Lm1;
then
A30: len(the_right_argument_of H) < k+1 by NAT_1:13;
len(the_left_argument_of H) < len(H) by A29,Lm23;
then len(the_left_argument_of H) <=k by A21,Lm1;
then len(the_left_argument_of H) < k+1 by NAT_1:13;
then
A31: h.(the_left_argument_of H) =f.( the_left_argument_of H) by A18;
per cases by A21,NAT_1:8;
suppose
A32: len(H) <= k;
then len(H) < k+1 by NAT_1:13;
then f.H = h.H by A18
.= (the EUntill of V).(h.(the_left_argument_of H), h.(
the_right_argument_of H)) by A2,A29,A32;
hence thesis by A18,A31,A30;
end;
suppose
len(H) = k+1;
then GraftEval(V,Kai,h,h,k,H) = (the EUntill of V).(h.(
the_left_argument_of H), h.(the_right_argument_of H)) by A29,Def28
.= (the EUntill of V).(f.(the_left_argument_of H), f.(
the_right_argument_of H)) by A18,A31,A30;
hence thesis by A23;
end;
end;
A33: 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
A34: H is conjunctive;
then len(the_right_argument_of H) < len(H) by Lm23;
then len(the_right_argument_of H) <=k by A21,Lm1;
then
A35: len(the_right_argument_of H) < k+1 by NAT_1:13;
len(the_left_argument_of H) < len(H) by A34,Lm23;
then len(the_left_argument_of H) <=k by A21,Lm1;
then len(the_left_argument_of H) < k+1 by NAT_1:13;
then
A36: h.(the_left_argument_of H) =f.( the_left_argument_of H) by A18;
per cases by A21,NAT_1:8;
suppose
A37: len(H) <= k;
then len(H) < k+1 by NAT_1:13;
then f.H = h.H by A18
.= (the L_meet of V).(h.(the_left_argument_of H), h.(
the_right_argument_of H)) by A2,A34,A37;
hence thesis by A18,A36,A35;
end;
suppose
len(H) = k+1;
then GraftEval(V,Kai,h,h,k,H) = (the L_meet of V).(h.(
the_left_argument_of H), h.(the_right_argument_of H)) by A34,Def28
.= (the L_meet of V).(f.(the_left_argument_of H), f.(
the_right_argument_of H)) by A18,A36,A35;
hence thesis by A23;
end;
end;
A38: H is ExistGlobal implies f.H = (the EGlobal of V).(f.(
the_argument_of H))
proof
assume
A39: H is ExistGlobal;
then len(the_argument_of H) < len(H) by Lm22;
then len(the_argument_of H) <=k by A21,Lm1;
then
A40: len(the_argument_of H) < k+1 by NAT_1:13;
per cases by A21,NAT_1:8;
suppose
A41: len(H) <= k;
then len(H) < k+1 by NAT_1:13;
then f.H = h.H by A18
.= (the EGlobal of V).(h.(the_argument_of H)) by A2,A39,A41;
hence thesis by A18,A40;
end;
suppose
len(H) = k+1;
then GraftEval(V,Kai,h,h,k,H) = (the EGlobal of V).(h.(
the_argument_of H)) by A39,Def28
.= (the EGlobal of V).(f.(the_argument_of H)) by A18,A40;
hence thesis by A23;
end;
end;
A42: H is ExistNext implies f.H = (the EneXt of V).(f.(the_argument_of H))
proof
assume
A43: H is ExistNext;
then len(the_argument_of H) < len(H) by Lm22;
then len(the_argument_of H) <=k by A21,Lm1;
then
A44: len(the_argument_of H) < k+1 by NAT_1:13;
per cases by A21,NAT_1:8;
suppose
A45: len(H) <= k;
then len(H) < k+1 by NAT_1:13;
then f.H = h.H by A18
.= (the EneXt of V).(h.(the_argument_of H)) by A2,A43,A45;
hence thesis by A18,A44;
end;
suppose
len(H) = k+1;
then GraftEval(V,Kai,h,h,k,H) = (the EneXt of V).(h.(
the_argument_of H)) by A43,Def28
.= (the EneXt of V).(f.(the_argument_of H)) by A18,A44;
hence thesis by A23;
end;
end;
H is atomic implies f.H = Kai.H
proof
assume
A46: H is atomic;
per cases by A21,NAT_1:8;
suppose
A47: len(H) <= k;
then len(H) < k+1 by NAT_1:13;
then f.H = h.H by A18
.= Kai.H by A2,A46,A47;
hence thesis;
end;
suppose
len(H) = k+1;
hence thesis by A23,A46,Def28;
end;
end;
hence thesis by A24,A33,A42,A38,A28;
end;
hence thesis;
end;
hence thesis;
end;
A48: P[0]
proof
consider v0 be object such that
A49: v0 in the carrier of V by XBOOLE_0:def 1;
set f = CTL_WFF --> v0;
A50: dom f = CTL_WFF by FUNCOP_1:13;
A51: rng f c= {v0} by FUNCOP_1:13;
{v0} c= the carrier of V by A49,ZFMISC_1:31;
then reconsider f as Function of CTL_WFF,the carrier of V by A50,A51,
FUNCT_2:2,XBOOLE_1:1;
take f;
thus thesis by Lm24;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A48,A1);
hence thesis;
end;
Lm28: (for n holds f is-PreEvaluation-for n,Kai) implies f is-Evaluation-for
Kai
proof
assume
A1: for n holds f is-PreEvaluation-for n,Kai;
let H be CTL-formula;
set n = len(H);
f is-PreEvaluation-for n,Kai by A1;
hence thesis;
end;
definition
let V be CTLModel;
let Kai be Function of atomic_WFF,the BasicAssign of V;
let n be Element of NAT;
func EvalSet(V,Kai,n) ->non empty set equals
{h where h is Function of
CTL_WFF,the carrier of V : h is-PreEvaluation-for n,Kai};
correctness
proof
set X = {h where h is Function of CTL_WFF,the carrier of V : h
is-PreEvaluation-for n,Kai};
consider h being Function of CTL_WFF,the carrier of V such that
A1: h is-PreEvaluation-for n,Kai by Lm27;
h in X by A1;
hence thesis;
end;
end;
definition
let V be CTLModel;
let v0 be Element of the carrier of V;
let x be set;
func CastEval(V,x,v0) ->Function of CTL_WFF,the carrier of V equals
:
Def32: x
if x in Funcs(CTL_WFF,the carrier of V) otherwise CTL_WFF --> v0;
correctness by FUNCT_2:66;
end;
definition
let V be CTLModel;
let Kai be Function of atomic_WFF,the BasicAssign of V;
func EvalFamily(V,Kai) -> non empty set means
:Def33:
for p being set holds
p in it iff p in bool Funcs(CTL_WFF,the carrier of V) & ex n being Element
of NAT st p=EvalSet(V,Kai,n);
existence
proof
defpred Q[set] means ex n being Element of NAT st $1=EvalSet(V,Kai,n);
set X = bool Funcs(CTL_WFF,the carrier of V);
consider IT be set such that
A1: for p being set holds p in IT iff p in X & Q[p] from XFAMILY:sch
1;
IT is non empty
proof
set p = EvalSet(V,Kai,0);
p c= Funcs(CTL_WFF,the carrier of V)
proof
let x be object;
assume x in p;
then
ex h being Function of CTL_WFF,the carrier of V st x =h & h
is-PreEvaluation-for 0,Kai;
hence thesis by FUNCT_2:8;
end;
hence thesis by A1;
end;
then reconsider IT as non empty set;
take IT;
thus thesis by A1;
end;
uniqueness
proof
defpred P[set] means $1 in bool Funcs(CTL_WFF,the carrier of V) & ex
n being Element of NAT st $1=EvalSet(V,Kai,n);
for X1,X2 being set st (for x being set holds x in X1 iff P[x]) & (for
x being set holds x in X2 iff P[x]) holds X1 = X2 from XFAMILY:sch 3;
hence thesis;
end;
end;
Lm29: EvalSet(V,Kai,n) in EvalFamily(V,Kai)
proof
set p1 = EvalSet(V,Kai,n);
p1 c= Funcs(CTL_WFF,the carrier of V)
proof
let x be object;
assume x in p1;
then ex h being Function of CTL_WFF,the carrier of V st x = h & h
is-PreEvaluation-for n,Kai;
hence thesis by FUNCT_2:8;
end;
hence thesis by Def33;
end;
theorem Th3:
ex f st f is-Evaluation-for Kai
proof
set M = EvalFamily(V,Kai);
set v0 = the Element of the carrier of V;
for X being set st X in M holds X <> {}
proof
let X being set;
assume X in M;
then ex n being Element of NAT st X = EvalSet(V,Kai,n) by Def33;
hence thesis;
end;
then consider Choice being Function such that
dom Choice = M and
A1: for X being set st X in M holds Choice.X in X by FUNCT_1:111;
deffunc F(object) = Choice.EvalSet(V,Kai,k_nat($1));
A2: for n being set st n in NAT holds F(n) is Function of CTL_WFF,the
carrier of V
proof
let n be set such that
A3: n in NAT;
A4: k_nat(n) = n by A3,Def2;
set Y = F(n);
reconsider n as Element of NAT by A3;
Y in EvalSet(V,Kai,n) by A1,A4,Lm29;
then ex h being Function of CTL_WFF,the carrier of V st Y =h & h
is-PreEvaluation-for n,Kai;
hence thesis;
end;
A5: for n being object st n in NAT
holds F(n) in Funcs(CTL_WFF,the carrier of V)
proof
let n be object;
assume n in NAT;
then F(n) is Function of CTL_WFF,the carrier of V by A2;
hence thesis by FUNCT_2:8;
end;
consider f1 being sequence of Funcs(CTL_WFF,the carrier of V) such
that
A6: for n being object st n in NAT holds f1.n = F(n) from FUNCT_2:sch 2(
A5);
deffunc G(object) = CastEval(V,f1.len(CastCTLformula($1)),v0).$1;
A7: for H being object st H in CTL_WFF
holds G(H) in the carrier of V by FUNCT_2:5;
consider f being Function of CTL_WFF,the carrier of V such that
A8: for H being object st H in CTL_WFF holds f.H = G(H) from FUNCT_2:sch 2
(A7 );
take f;
for n being Element of NAT holds f is-PreEvaluation-for n,Kai
proof
defpred P[Nat] means f is-PreEvaluation-for $1,Kai;
A9: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat such that
A10: P[k];
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 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 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 such that
A11: len(H) <= k+1;
now
per cases by A11,NAT_1:8;
case
len(H) <= k;
hence thesis by A10,Def27;
end;
case
A12: len(H) = k+1;
set f2 = F(len H);
A13: H in CTL_WFF by Th1;
then f1.len(CastCTLformula(H)) = f1.len(H) by Def24
.= F(len(H)) by A6;
then
A14: CastEval(V,f1.len(CastCTLformula(H)),v0) = F(len H ) by Def32;
then reconsider f2 as Function of CTL_WFF,the carrier of V;
A15: f2 = Choice.EvalSet(V,Kai,len(H)) by Def2;
Choice.EvalSet(V,Kai,len(H)) in EvalSet(V,Kai,len(H)) by A1,Lm29;
then
A16: ex h being Function of CTL_WFF,the carrier of V st f2=h
& h is-PreEvaluation-for len(H),Kai by A15;
then
A17: f2 is-PreEvaluation-for k,Kai by A12,Lm25;
A18: f.H = f2.H by A8,A13,A14;
A19: H is ExistNext implies f.H = (the EneXt of V).(f.(
the_argument_of H))
proof
assume
A20: H is ExistNext;
then len(the_argument_of H) < len(H) by Lm22;
then
A21: len(the_argument_of H) <= k by A12,NAT_1:13;
f.H = (the EneXt of V).(f2.(the_argument_of H)) by A18,A16,A20
.= (the EneXt of V).(f.(the_argument_of H)) by A10,A17,A21,Lm26
;
hence thesis;
end;
A22: H is ExistUntill implies f.H = (the EUntill of V).(f.(
the_left_argument_of H), f.(the_right_argument_of H))
proof
assume
A23: H is ExistUntill;
then len(the_right_argument_of H) < len(H) by Lm23;
then
A24: len(the_right_argument_of H) <= k by A12,NAT_1:13;
len(the_left_argument_of H) < len(H) by A23,Lm23;
then len(the_left_argument_of H) <= k by A12,NAT_1:13;
then
A25: f.(the_left_argument_of H) = f2.( the_left_argument_of H)
by A10,A17,Lm26;
f.H = (the EUntill of V).(f2.(the_left_argument_of H), f2.(
the_right_argument_of H)) by A18,A16,A23
.= (the EUntill of V).(f.(the_left_argument_of H), f.(
the_right_argument_of H)) by A10,A17,A25,A24,Lm26;
hence thesis;
end;
A26: 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
A27: H is conjunctive;
then len(the_right_argument_of H) < len(H) by Lm23;
then
A28: len(the_right_argument_of H) <= k by A12,NAT_1:13;
len(the_left_argument_of H) < len(H) by A27,Lm23;
then len(the_left_argument_of H) <= k by A12,NAT_1:13;
then
A29: f.(the_left_argument_of H) = f2.( the_left_argument_of H)
by A10,A17,Lm26;
f.H = (the L_meet of V).(f2.(the_left_argument_of H), f2.(
the_right_argument_of H)) by A18,A16,A27
.= (the L_meet of V).(f.(the_left_argument_of H), f.(
the_right_argument_of H)) by A10,A17,A29,A28,Lm26;
hence thesis;
end;
A30: H is ExistGlobal implies f.H = (the EGlobal of V).(f.(
the_argument_of H))
proof
assume
A31: H is ExistGlobal;
then len(the_argument_of H) < len(H) by Lm22;
then
A32: len(the_argument_of H) <= k by A12,NAT_1:13;
f.H = (the EGlobal of V).(f2.(the_argument_of H)) by A18,A16,A31
.= (the EGlobal of V).(f.(the_argument_of H)) by A10,A17,A32
,Lm26;
hence thesis;
end;
H is negative implies f.H = (the Compl of V).(f.(
the_argument_of H))
proof
assume
A33: H is negative;
then len(the_argument_of H) < len(H) by Lm22;
then
A34: len(the_argument_of H) <= k by A12,NAT_1:13;
f.H = (the Compl of V).(f2.(the_argument_of H)) by A18,A16,A33
.= (the Compl of V).(f.(the_argument_of H)) by A10,A17,A34,Lm26
;
hence thesis;
end;
hence thesis by A18,A16,A19,A30,A26,A22;
end;
end;
hence thesis;
end;
hence thesis by Def27;
end;
for H being CTL-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 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 Lm10;
then
A35: P[0] by Def27;
for n being Nat holds P[n] from NAT_1:sch 2(A35,A9);
hence thesis;
end;
hence thesis by Lm28;
end;
theorem Th4:
f1 is-Evaluation-for Kai & f2 is-Evaluation-for Kai implies f1 = f2
proof
assume that
A1: f1 is-Evaluation-for Kai and
A2: f2 is-Evaluation-for Kai;
for H being object st H in CTL_WFF holds f1.H=f2.H
proof
let H be object;
assume H in CTL_WFF;
then reconsider H as CTL-formula by Th1;
set n=len(H);
A3: f2 is-PreEvaluation-for n, Kai by A2;
f1 is-PreEvaluation-for n, Kai by A1;
hence thesis by A3,Lm26;
end;
hence thesis by FUNCT_2:12;
end;
definition
let V be CTLModel;
let Kai be Function of atomic_WFF,the BasicAssign of V;
let H be CTL-formula;
func Evaluate(H,Kai) -> Assign of V means
:Def34:
ex f being Function of
CTL_WFF,the carrier of V st f is-Evaluation-for Kai & it = f.H;
existence
proof
consider f be Function of CTL_WFF,the carrier of V such that
A1: f is-Evaluation-for Kai by Th3;
set IT=f.H;
H in CTL_WFF by Th1;
then reconsider IT as Assign of V by FUNCT_2:5;
take IT;
thus thesis by A1;
end;
uniqueness by Th4;
end;
notation
let V be CTLModel;
let f be Assign of V;
synonym 'not' f for f`;
let g be Assign of V;
synonym f '&' g for f "/\" g;
end;
definition
let V be CTLModel;
let f be Assign of V;
func EX(f) -> Assign of V equals
(the EneXt of V).f;
correctness;
func EG(f) -> Assign of V equals
(the EGlobal of V).f;
correctness;
end;
definition
let V be CTLModel;
let f,g be Assign of V;
func f EU g -> Assign of V equals
(the EUntill of V).(f,g);
correctness;
func f 'or' g -> Assign of V equals
'not'('not'(f) '&' 'not'(g));
correctness;
end;
::Some properties of evaluate function of CTL
theorem Th5:
Evaluate('not' H,Kai) = 'not' Evaluate(H,Kai)
proof
consider f1 be Function of CTL_WFF,the carrier of V such that
A1: f1 is-Evaluation-for Kai and
A2: Evaluate('not' H,Kai) = f1.('not' H) by Def34;
A3: ex f2 be Function of CTL_WFF,the carrier of V st f2
is-Evaluation-for Kai & Evaluate(H,Kai) = f2.H by Def34;
A4: 'not' H is negative;
then
Evaluate('not' H,Kai) = (the Compl of V).(f1.(the_argument_of('not' H)) )
by A1,A2
.= (the Compl of V).(f1.H ) by A4,Def21
.= 'not' Evaluate(H,Kai) by A1,A3,Th4;
hence thesis;
end;
theorem Th6:
Evaluate(H1 '&' H2,Kai) = Evaluate(H1,Kai) '&' Evaluate(H2,Kai)
proof
consider f0 be Function of CTL_WFF,the carrier of V such that
A1: f0 is-Evaluation-for Kai and
A2: Evaluate(H1 '&' H2,Kai) = f0.(H1 '&' H2) by Def34;
consider f1 be Function of CTL_WFF,the carrier of V such that
A3: f1 is-Evaluation-for Kai and
A4: Evaluate(H1,Kai) = f1.H1 by Def34;
consider f2 be Function of CTL_WFF,the carrier of V such that
A5: f2 is-Evaluation-for Kai and
A6: Evaluate(H2,Kai) = f2.H2 by Def34;
A7: f0=f2 by A1,A5,Th4;
A8: H1 '&' H2 is conjunctive;
then
A9: the_left_argument_of(H1 '&' H2) = H1 by Def22;
A10: the_right_argument_of(H1 '&' H2)= H2 by A8,Def23;
f0=f1 by A1,A3,Th4;
hence thesis by A1,A2,A4,A6,A7,A8,A9,A10;
end;
theorem Th7:
Evaluate(EX H,Kai) = EX Evaluate(H,Kai)
proof
consider f1 be Function of CTL_WFF,the carrier of V such that
A1: f1 is-Evaluation-for Kai and
A2: Evaluate(EX H,Kai) = f1.(EX H) by Def34;
A3: ex f2 be Function of CTL_WFF,the carrier of V st f2
is-Evaluation-for Kai & Evaluate(H,Kai) = f2.H by Def34;
A4: EX H is ExistNext;
then Evaluate(EX H,Kai) = (the EneXt of V).(f1.(the_argument_of(EX H)) ) by
A1,A2
.= (the EneXt of V).(f1.H ) by A4,Def21
.= EX Evaluate(H,Kai) by A1,A3,Th4;
hence thesis;
end;
theorem Th8:
Evaluate(EG H,Kai) = EG Evaluate(H,Kai)
proof
consider f1 be Function of CTL_WFF,the carrier of V such that
A1: f1 is-Evaluation-for Kai and
A2: Evaluate(EG H,Kai) = f1.(EG H) by Def34;
A3: ex f2 be Function of CTL_WFF,the carrier of V st f2
is-Evaluation-for Kai & Evaluate(H,Kai) = f2.H by Def34;
A4: EG H is ExistGlobal;
then
A5: not EG H is negative by Lm18;
A6: not EG H is ExistNext by A4,Lm18;
Evaluate(EG H,Kai) = (the EGlobal of V).(f1.(the_argument_of(EG H)) ) by A1
,A2,A4
.= (the EGlobal of V).(f1.H ) by A4,A5,A6,Def21
.= EG Evaluate(H,Kai) by A1,A3,Th4;
hence thesis;
end;
theorem Th9:
Evaluate(H1 EU H2,Kai) = Evaluate(H1,Kai) EU Evaluate(H2,Kai)
proof
consider f0 be Function of CTL_WFF,the carrier of V such that
A1: f0 is-Evaluation-for Kai and
A2: Evaluate(H1 EU H2,Kai) = f0.(H1 EU H2) by Def34;
consider f1 be Function of CTL_WFF,the carrier of V such that
A3: f1 is-Evaluation-for Kai and
A4: Evaluate(H1,Kai) = f1.H1 by Def34;
consider f2 be Function of CTL_WFF,the carrier of V such that
A5: f2 is-Evaluation-for Kai and
A6: Evaluate(H2,Kai) = f2.H2 by Def34;
A7: f0=f2 by A1,A5,Th4;
A8: H1 EU H2 is ExistUntill;
then (H1 EU H2).1 = 4 by Lm7;
then
A9: not H1 EU H2 is conjunctive by Lm4;
then
A10: the_left_argument_of(H1 EU H2) = H1 by A8,Def22;
A11: the_right_argument_of(H1 EU H2) = H2 by A8,A9,Def23;
f0=f1 by A1,A3,Th4;
hence thesis by A1,A2,A4,A6,A7,A8,A10,A11;
end;
theorem Th10:
Evaluate(H1 'or' H2,Kai) = Evaluate(H1,Kai) 'or' Evaluate(H2,Kai )
proof
Evaluate(H1 'or' H2,Kai) = 'not' Evaluate('not' H1 '&' 'not' H2,Kai) by Th5
.= 'not' (Evaluate('not' H1,Kai) '&' Evaluate('not' H2,Kai)) by Th6
.= 'not' (('not' Evaluate(H1,Kai)) '&' Evaluate('not' H2,Kai)) by Th5;
hence thesis by Th5;
end;
:: definition of iteration of function: f|**n
notation
let f be Function;
let n be Nat;
synonym f|**n for iter (f,n);
end;
definition
let S be set;
let f be Function of S,S;
let n be Nat;
redefine func f|**n -> Function of S,S; :: redefines |** (MODELC_1, synonym) → iter (FUNCT_7, definition)
coherence
proof
reconsider n9=n as Element of NAT by ORDINAL1:def 12;
iter(f,n9) is Function of S,S;
hence thesis;
end;
end;
:: Lemma of total Relation
Lm30: for S being set, R being Relation of S,S holds R is total implies for x
being set st x in S holds ex y being set st y in S & [x,y] in R
proof
let S be set;
let R be Relation of S,S;
R is total implies for x being set st x in S holds ex y being set st y
in S & [x,y] in R
proof
assume
A1: R is total;
for x being set st x in S holds ex y being set st y in S & [x,y] in R
proof
let x be set such that
A2: x in S;
dom R = S by A1,PARTFUN1:def 2;
then consider y being Element of S such that
A3: [x,y] in R by A2,RELSET_1:24;
take y;
thus thesis by A2,A3;
end;
hence thesis;
end;
hence thesis;
end;
Lm31: for S being set, R being Relation of S,S holds (for x being set st x in
S holds ex y being set st y in S & [x,y] in R) implies R is total
proof
let S be set;
let R be Relation of S,S;
(for x being set st x in S holds ex y being set st y in S & [x,y] in R)
implies R is total
proof
assume
A1: for x being set st x in S holds ex y being set st y in S & [x,y] in R;
A2: S c= dom R
proof
let x be object;
assume x in S;
then ex y being set st y in S & [x,y] in R by A1;
hence thesis by XTUPLE_0:def 12;
end;
dom R c= S by RELAT_1:def 18;
then dom R = S by A2,XBOOLE_0:def 10;
hence thesis by PARTFUN1:def 2;
end;
hence thesis;
end;
reserve S for non empty set;
reserve R for total Relation of S,S;
reserve s,s0,s1 for Element of S;
:: existence of (infinite) path for total Relation
Lm32: R.:{s} is non empty
proof
A1: s in {s} by TARSKI:def 1;
ex p being set st p in S & [s,p] in R by Lm30;
hence thesis by A1,RELAT_1:def 13;
end;
:: scheme for path with condition F
scheme
ExistPath{ S()-> non empty set, R()-> total Relation of S(),S(), s0()->
Element of S(), F(Element of S())-> set}: ex f being sequence of S() st f.0
=s0() & for n being Element of NAT holds [f.n,f.(n+1)] in R() & f.(n+1) in F(f.
n)
provided
A1: for s being Element of S() holds Im(R(),s) /\ F(s) is non empty
Subset of S()
proof
for p being set st p in BOOL S() holds p<>{} by ORDERS_1:1;
then consider Choice being Function such that
dom Choice = BOOL S() and
A2: for p being set st p in BOOL S() holds Choice.p in p by FUNCT_1:111;
A3: s0() in S();
ex g being sequence of S() st g.0=s0() & for n being Element of NAT
holds g.(n+1) = Choice.(R().:{g.n} /\ F(g.n))
proof
deffunc G(object)
= Choice.(R().:{k_id($1,S(),s0())} /\ F(k_id($1,S(),s0())));
A4: for x being object st x in S() holds G(x) in S()
proof
let x being object such that
A5: x in S();
A6: k_id(x,S(),s0()) = x by A5,Def1;
reconsider x as Element of S() by A5;
set X = Im(R(),x)/\ F(x);
X is non empty Subset of S() by A1;
then X in BOOL S() by ORDERS_1:2;
then Choice.X in X by A2;
then
A7: G(x) in R().:{x} by A6,XBOOLE_0:def 4;
A8: rng R() c= S() by RELAT_1:def 19;
R().:{x} c= rng R() by RELAT_1:111;
then R().:{x} c= S() by A8;
hence thesis by A7;
end;
consider f being Function of S(),S() such that
A9: for x being object st x in S() holds f.x= G(x) from FUNCT_2:sch 2(A4
);
deffunc H(object) = (f|**k_nat($1)).s0();
A10: for m being object st m in NAT holds H(m) in S();
consider g being sequence of S() such that
A11: for m being object st m in NAT holds g.m= H(m) from FUNCT_2:sch 2(
A10);
A12: for n being Element of NAT holds g.(n+1) = Choice.(R().:{g.n} /\ F(g. n))
proof
let n be Element of NAT;
A13: s0() in dom (f|**n) by A3,FUNCT_2:def 1;
A14: k_id(g.n,S(),s0())=g.n by Def1;
g.(n+1) = H(n+1) by A11
.= (f|**(n+1)).s0() by Def2
.=(f*(f|**n)).s0() by FUNCT_7:71
.=f.((f|**n).s0()) by A13,FUNCT_1:13
.=f.((f|**k_nat(n)).s0()) by Def2
.=f.(g.n) by A11
.=Choice.(R().:{g.n}/\ F(g.n)) by A9,A14;
hence thesis;
end;
take g;
g.0 = H(0) by A11
.=(f|**0).s0() by Def2
.= (id S()).s0() by FUNCT_7:84
.=s0();
hence thesis by A12;
end;
then consider g being sequence of S() such that
A15: g.0=s0() and
A16: for n being Element of NAT holds g.(n+1) = Choice.(R().:{g.n}/\ F(g .n));
take g;
A17: for n being Element of NAT holds g.(n+1) in R().:{g.n}/\ F(g.n)
proof
let n be Element of NAT;
set s = g.n;
set X = Im(R(),s)/\ F(s);
X is non empty Subset of S() by A1;
then X in BOOL S() by ORDERS_1:2;
then Choice.X in X by A2;
hence thesis by A16;
end;
for n being Element of NAT holds [g.n,g.(n+1)] in R() & g.(n+1) in F(g. n)
proof
let n be Element of NAT;
A18: g.(n+1) in Im(R(),g.n) /\ F(g.n) by A17;
then g.(n+1) in Im(R(),g.n) by XBOOLE_0:def 4;
hence thesis by A18,RELSET_2:9,XBOOLE_0:def 4;
end;
hence thesis by A15;
end;
Lm33: for s0 holds ex f being sequence of S st f.0=s0 &
for n being Nat holds [f.n,f.(n+1)] in R
proof
let s0;
deffunc F(Element of S) = S;
A1: for s holds Im(R,s) /\ F(s) is non empty Subset of S
proof
let s;
set X = R.:{s};
A2: rng R c= S by RELAT_1:def 19;
A3: X c= rng R by RELAT_1:111;
then R.:{s} /\ F(s) = X by A2,XBOOLE_1:1,28;
hence thesis by A3,A2,Lm32,XBOOLE_1:1;
end;
consider f being sequence of S such that
A4: f.0=s0 & for n holds [f.n,f.(n+1)] in R & f.(n+1) in F(f.n) from
ExistPath(A1);
take f;
thus f.0 = s0 by A4;
let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A4;
end;
:: definition of infinity path
definition
let S be non empty set;
let R be total Relation of S,S;
mode inf_path of R -> sequence of S means
:Def39:
for n being Nat holds [it.n,it.(n+1)] in R;
existence
proof
set b = the Element of S;
consider IT being sequence of S such that
IT.0=b and
A1: for n being Nat holds [IT.n,IT.(n+1)] in R by Lm33;
take IT;
thus thesis by A1;
end;
end;
::definition of concrete object of CTL model
definition
let S be non empty set;
func ModelSP(S) -> set equals
Funcs(S,BOOLEAN);
correctness;
end;
registration
let S be non empty set;
cluster ModelSP(S) -> non empty;
coherence;
end;
:: definition Fid:ModelSP(S) -> Function of S,BOOLEAN
definition
let S be non empty set;
let f be object; :: zastapic przez In(.,.) ??? !!!
func Fid(f,S) -> Function of S,BOOLEAN equals
:Def41:
f if f in ModelSP(S)
otherwise S --> FALSE;
correctness by FUNCT_2:66;
end;
Lm34: for f being set holds (Fid(f,S)).s <> TRUE implies (Fid(f,S)).s = FALSE
by TARSKI:def 2;
::schemes for existence & uniqueness of 1 Operand functor
scheme
Func1EX{S()->non empty set, f()->Function of S(),BOOLEAN,
F(object,Function of S(),BOOLEAN) -> boolean object}:
ex g being set st g in ModelSP(S()) & for s being
set st s in S() holds F(s,f()) =TRUE iff (Fid(g,S())).s=TRUE proof
deffunc G(object) = F($1,f());
A1: for s being object st s in S() holds G(s) in BOOLEAN by MARGREL1:def 12;
consider IT be Function of S(),BOOLEAN such that
A2: for s being object st s in S() holds IT.s =G(s) from FUNCT_2:sch 2(A1);
take IT;
IT in ModelSP(S()) by FUNCT_2:8;
then Fid(IT,S()) = IT by Def41;
hence thesis by A2,FUNCT_2:8;
end;
scheme
Func1Unique{S()->non empty set, f()->Function of S(),BOOLEAN,
F(object,Function of S(),BOOLEAN) -> boolean object}:
for g1,g2 being set st g1 in ModelSP(S()) & (
for s being set st s in S() holds F(s,f()) =TRUE iff (Fid(g1,S())).s=TRUE ) &
g2 in ModelSP(S()) & (for s being set st s in S() holds F(s,f()) =TRUE iff (Fid
(g2,S())).s=TRUE ) holds g1 = g2 proof
let g1,g2 be set such that
A1: g1 in ModelSP(S()) and
A2: for s being set st s in S() holds F(s,f()) =TRUE iff (Fid(g1,S())).s
=TRUE and
A3: g2 in ModelSP(S()) and
A4: for s being set st s in S() holds F(s,f()) =TRUE iff (Fid(g2,S())).s =TRUE;
A5: for s being object st s in S() holds Fid(g1,S()).s= (Fid(g2,S())).s
proof
let s be object such that
A6: s in S();
set F1 = F(s,f());
set f1 = (Fid(g1,S())).s;
A7: F1 =TRUE iff f1 =TRUE by A2,A6;
set f2 = (Fid(g2,S())).s;
A8: F1 =TRUE iff f2 =TRUE by A4,A6;
per cases;
suppose
F1=TRUE;
hence thesis by A4,A6,A7;
end;
suppose
A9: F1<>TRUE;
then f1 = FALSE by A6,A7,Lm34;
hence thesis by A6,A8,A9,Lm34;
end;
end;
g1 = Fid(g1,S()) by A1,Def41
.= Fid(g2,S()) by A5,FUNCT_2:12
.= g2 by A3,Def41;
hence thesis;
end;
::schemes for existence & uniqueness of Unary Operation
scheme
UnOpEX{M()->non empty set, F(object)->Element of M()}:
ex o being UnOp of M()
st for f being object st f in M() holds o.(f) = F(f);
A1: for f being object st f in M() holds F(f) in M();
ex o being Function of M(),M() st
for f being object st f in M() holds o.f
= F(f) from FUNCT_2:sch 2(A1);
hence thesis;
end;
scheme
UnOpUnique{S,M()->non empty set, F(object)->Element of M()}:
for o1,o2 being UnOp of M() st
(for f being object st f in M() holds o1.f = F(f))
& (for f being object st f in M() holds o2.f = F(f)) holds o1=o2;
let o1,o2 being UnOp of M() such that
A1: for f being object st f in M() holds o1.f = F(f) and
A2: for f being object st f in M() holds o2.f = F(f);
for f being Element of M() holds o1.f = o2.f
proof
let f be Element of M();
o1.f = F(f) by A1
.= o2.f by A2;
hence thesis;
end;
hence thesis by FUNCT_2:63;
end;
::schemes for existence & uniqueness of 2 Operands functor .
scheme
Func2EX{S()->non empty set, f()->Function of S(),BOOLEAN, g()->Function of S
(),BOOLEAN, F(object,Function of S(),BOOLEAN, Function of S(),BOOLEAN)
-> boolean object}:
ex h being set st h in ModelSP(S()) & for s being set st s in S() holds F
(s,f(),g()) =TRUE iff (Fid(h,S())).s=TRUE;
deffunc G(object) = F($1,f(),g());
A1: for s being object st s in S() holds G(s) in BOOLEAN by MARGREL1:def 12;
consider IT be Function of S(),BOOLEAN such that
A2: for s being object st s in S() holds IT.s =G(s) from FUNCT_2:sch 2(A1);
take IT;
IT in ModelSP(S()) by FUNCT_2:8;
then Fid(IT,S()) = IT by Def41;
hence thesis by A2,FUNCT_2:8;
end;
scheme
Func2Unique{S()->non empty set, f()->Function of S(),BOOLEAN, g()->Function
of S(),BOOLEAN,
F(object,Function of S(),BOOLEAN, Function of S(),BOOLEAN) ->
boolean object}:
for h1,h2 being set st h1 in ModelSP(S()) & (for s being set st s
in S() holds F(s,f(),g()) =TRUE iff (Fid(h1,S())).s=TRUE) & h2 in ModelSP(S())
& (for s being set st s in S() holds F(s,f(),g()) =TRUE iff (Fid(h2,S())).s=
TRUE) holds h1 = h2 proof
let h1,h2 be set such that
A1: h1 in ModelSP(S()) and
A2: for s being set st s in S() holds F(s,f(),g()) =TRUE iff (Fid(h1,S()
)).s=TRUE and
A3: h2 in ModelSP(S()) and
A4: for s being set st s in S() holds F(s,f(),g()) =TRUE iff (Fid(h2,S()
)).s=TRUE;
A5: for s being object st s in S() holds (Fid(h1,S())).s = (Fid(h2,S())).s
proof
let s be object such that
A6: s in S();
set F1 = F(s,f(),g());
set f1 = (Fid(h1,S())).s;
A7: F1 =TRUE iff f1 =TRUE by A2,A6;
set f2 = (Fid(h2,S())).s;
A8: F1 =TRUE iff f2 =TRUE by A4,A6;
per cases;
suppose
F1=TRUE;
hence thesis by A4,A6,A7;
end;
suppose
A9: F1<>TRUE;
then f1 = FALSE by A6,A7,Lm34;
hence thesis by A6,A8,A9,Lm34;
end;
end;
h1 = Fid(h1,S()) by A1,Def41
.= Fid(h2,S()) by A5,FUNCT_2:12
.= h2 by A3,Def41;
hence thesis;
end;
:: definition of Not_ unary operation of Model Space.
definition
let S be non empty set;
let f be object;
func Not_0(f,S) -> Element of ModelSP(S) means
:Def42:
for s being set st s
in S holds 'not' (Castboolean (Fid(f,S)).s) = TRUE iff (Fid(it,S)).s = TRUE;
existence
proof
deffunc F(set,Function of S,BOOLEAN) ='not' Castboolean($2.$1);
consider IT being set such that
A1: IT in ModelSP(S) and
A2: for s being set st s in S holds F(s,Fid(f,S)) = TRUE iff (Fid(IT,S
)).s=TRUE from Func1EX;
take IT;
thus thesis by A1,A2;
end;
uniqueness
proof
deffunc F(set,Function of S,BOOLEAN) ='not' Castboolean($2.$1);
for g1,g2 being set st g1 in ModelSP(S) & (for s being set st s in S
holds F(s,Fid(f,S)) =TRUE iff (Fid(g1,S)).s=TRUE) & g2 in ModelSP(S) & (for s
being set st s in S holds F(s,Fid(f,S)) =TRUE iff (Fid(g2,S)).s=TRUE) holds g1
= g2 from Func1Unique;
hence thesis;
end;
end;
Lm35: for o1,o2 being UnOp of ModelSP(S) st
(for f being object st f in ModelSP(S
) holds o1.f = Not_0(f,S)) &
(for f being object st f in ModelSP(S) holds o2.f =
Not_0(f,S)) holds o1=o2
proof
set M = ModelSP(S);
deffunc F(object) = Not_0($1,S);
for o1,o2 being UnOp of M st
(for f being object st f in M holds o1.f = F(f
)) & (for f being object st f in M holds o2.f = F(f)) holds o1=o2
from UnOpUnique;
hence thesis;
end;
definition
let S be non empty set;
func Not_(S) -> UnOp of ModelSP(S) means
:Def43:
for f being object st f in ModelSP(S) holds it.f = Not_0(f,S);
existence
proof
set M = ModelSP(S);
deffunc F(object) = Not_0($1,S);
ex o being UnOp of M st for f being object st f in M holds o.(f) = F(f)
from UnOpEX;
hence thesis;
end;
uniqueness by Lm35;
end;
:: definition of EneXt_ unary operation of Model Space.
definition
let S be non empty set;
let R be total Relation of S,S;
let f be Function of S,BOOLEAN;
let x be object;
func EneXt_univ(x,f,R) -> Element of BOOLEAN equals
:Def44:
TRUE if x in S &
ex pai being inf_path of R st pai.0 = x & f.(pai.1) =TRUE otherwise FALSE;
correctness;
end;
definition
let S be non empty set;
let R be total Relation of S,S;
let f be object;
func EneXt_0(f,R) -> Element of ModelSP(S) means
:Def45:
for s being set st
s in S holds EneXt_univ(s,Fid(f,S),R)=TRUE iff (Fid(it,S)).s=TRUE;
existence
proof
deffunc F(set,Function of S,BOOLEAN) =EneXt_univ($1,$2,R);
consider IT being set such that
A1: IT in ModelSP(S) and
A2: for s being set st s in S holds F(s,Fid(f,S)) =TRUE iff (Fid(IT,S)
).s=TRUE from Func1EX;
take IT;
thus thesis by A1,A2;
end;
uniqueness
proof
deffunc F(set,Function of S,BOOLEAN) =EneXt_univ($1,$2,R);
for g1,g2 being set st g1 in ModelSP(S) & (for s being set st s in S
holds F(s,Fid(f,S)) =TRUE iff (Fid(g1,S)).s=TRUE) & g2 in ModelSP(S) & (for s
being set st s in S holds F(s,Fid(f,S)) =TRUE iff (Fid(g2,S)).s=TRUE) holds g1
= g2 from Func1Unique;
hence thesis;
end;
end;
Lm36: for o1,o2 being UnOp of ModelSP(S) st
(for f being object st f in ModelSP(S
) holds o1.f = EneXt_0(f,R)) &
(for f being object st f in ModelSP(S) holds o2.f =
EneXt_0(f,R)) holds o1=o2
proof
set M = ModelSP(S);
deffunc F(object) = EneXt_0($1,R);
for o1,o2 being UnOp of M st
(for f being object st f in M holds o1.f = F(f
)) & (for f being object st f in M holds o2.f = F(f)) holds o1=o2
from UnOpUnique;
hence thesis;
end;
definition
let S be non empty set;
let R be total Relation of S,S;
func EneXt_(R) -> UnOp of ModelSP(S) means
:Def46:
for f being object st f in ModelSP(S) holds it.f = EneXt_0(f,R);
existence
proof
set M = ModelSP(S);
deffunc F(object) = EneXt_0($1,R);
ex o being UnOp of M st for f being object st f in M holds o.(f) = F(f)
from UnOpEX;
hence thesis;
end;
uniqueness by Lm36;
end;
:: definition of EGlobal_ unary operation of Model Space.
definition
let S be non empty set;
let R be total Relation of S,S;
let f be Function of S,BOOLEAN;
let x be set;
func EGlobal_univ(x,f,R) -> Element of BOOLEAN equals
:Def47:
TRUE if x in S
& ex pai being inf_path of R st (pai.0 = x & for n being Element of NAT holds f
.(pai.n) =TRUE) otherwise FALSE;
correctness;
end;
definition
let S be non empty set;
let R be total Relation of S,S;
let f be object;
func EGlobal_0(f,R) -> Element of ModelSP(S) means
:Def48:
for s being set
st s in S holds EGlobal_univ(s,Fid(f,S),R)=TRUE iff (Fid(it,S)).s=TRUE;
existence
proof
deffunc F(set,Function of S,BOOLEAN) =EGlobal_univ($1,$2,R);
consider IT being set such that
A1: IT in ModelSP(S) and
A2: for s being set st s in S holds F(s,Fid(f,S)) =TRUE iff (Fid(IT,S)
).s=TRUE from Func1EX;
take IT;
thus thesis by A1,A2;
end;
uniqueness
proof
deffunc F(set,Function of S,BOOLEAN) =EGlobal_univ($1,$2,R);
for g1,g2 being set st g1 in ModelSP(S) & (for s being set st s in S
holds F(s,Fid(f,S)) =TRUE iff (Fid(g1,S)).s=TRUE) & g2 in ModelSP(S) & (for s
being set st s in S holds F(s,Fid(f,S)) =TRUE iff (Fid(g2,S)).s=TRUE) holds g1
= g2 from Func1Unique;
hence thesis;
end;
end;
Lm37: for o1,o2 being UnOp of ModelSP(S) st
(for f being object st f in ModelSP(S
) holds o1.f = EGlobal_0(f,R)) &
(for f being object st f in ModelSP(S) holds o2.f
= EGlobal_0(f,R)) holds o1=o2
proof
set M = ModelSP(S);
deffunc F(object) = EGlobal_0($1,R);
for o1,o2 being UnOp of M st
(for f being object st f in M holds o1.f = F(f
)) & (for f being object st f in M holds o2.f = F(f)) holds o1=o2
from UnOpUnique;
hence thesis;
end;
definition
let S be non empty set;
let R be total Relation of S,S;
func EGlobal_(R) -> UnOp of ModelSP(S) means
:Def49:
for f being object st f in ModelSP(S) holds it.f = EGlobal_0(f,R);
existence
proof
set M = ModelSP(S);
deffunc F(object) = EGlobal_0($1,R);
ex o being UnOp of M st for f being object st f in M holds o.(f) = F(f)
from UnOpEX;
hence thesis;
end;
uniqueness by Lm37;
end;
:: definition of And_ Binary Operation of Model Space.
definition
let S be non empty set;
let f,g be set;
func And_0(f,g,S) -> Element of ModelSP(S) means
:Def50:
for s being set st
s in S holds (Castboolean (Fid(f,S)).s ) '&' (Castboolean (Fid(g,S)).s ) =TRUE
iff (Fid(it,S)).s=TRUE;
existence
proof
deffunc F(set,Function of S,BOOLEAN,Function of S,BOOLEAN) = (Castboolean
$2.$1 ) '&' (Castboolean $3.$1 );
consider IT being set such that
A1: IT in ModelSP(S) and
A2: for s being set st s in S holds F(s,Fid(f,S),Fid(g,S)) =TRUE iff (
Fid(IT,S)).s=TRUE from Func2EX;
take IT;
thus thesis by A1,A2;
end;
uniqueness
proof
deffunc F(set,Function of S,BOOLEAN,Function of S,BOOLEAN) =(Castboolean
$2.$1 ) '&' (Castboolean $3.$1 );
for h1,h2 being set st h1 in ModelSP(S) & (for s being set st s in S
holds F(s,Fid(f,S),Fid(g,S)) =TRUE iff (Fid(h1,S)).s=TRUE) & h2 in ModelSP(S) &
(for s being set st s in S holds F(s,Fid(f,S),Fid(g,S)) =TRUE iff (Fid(h2,S)).s
=TRUE) holds h1 = h2 from Func2Unique;
hence thesis;
end;
end;
Lm38: for o1,o2 being BinOp of ModelSP(S) st (for f,g being set st (f in
ModelSP(S)) & (g in ModelSP(S)) holds o1.(f,g) = And_0(f,g,S)) & (for f,g being
set st (f in ModelSP(S)) & (g in ModelSP(S)) holds o2.(f,g) = And_0(f,g,S))
holds o1=o2
proof
set M = ModelSP(S);
deffunc O(Element of M,Element of M) = And_0($1,$2,S);
A1: for o1,o2 being BinOp of M st (for f,g being Element of M holds o1.(f,g)
= O(f,g)) & (for f,g being Element of M holds o2.(f,g) = O(f,g)) holds o1=o2
from BINOP_2:sch 2;
for o1,o2 being BinOp of M st (for f,g being set st (f in M ) & (g in M
) holds o1.(f,g) = And_0(f,g,S)) & (for f,g being set st (f in M) & (g in M)
holds o2.(f,g) = And_0(f,g,S)) holds o1=o2
proof
let o1,o2 be BinOp of M such that
A2: for f,g being set st f in M & g in M holds o1.(f,g) = And_0(f,g,S) and
A3: for f,g being set st f in M & g in M holds o2.(f,g) = And_0(f,g,S);
A4: for f,g being Element of M holds o2.(f,g) = O(f,g) by A3;
for f,g being Element of M holds o1.(f,g) = O(f,g) by A2;
hence thesis by A1,A4;
end;
hence thesis;
end;
definition
let S be non empty set;
func And_(S) -> BinOp of ModelSP(S) means
:Def51:
for f,g being set st f in
ModelSP(S) & g in ModelSP(S) holds it.(f,g) = And_0(f,g,S);
existence
proof
set M = ModelSP(S);
deffunc O(Element of M,Element of M) = And_0($1,$2,S);
consider o being BinOp of M such that
A1: for f,g being Element of M holds o.(f,g) = O(f,g) from BINOP_1:sch 4;
for f,g being set st f in M & g in M holds o.(f,g) = And_0(f,g,S) by A1;
hence thesis;
end;
uniqueness by Lm38;
end;
:: definition of EUntill_ Binary Operation of Model Space.
definition
let S be non empty set;
let R be total Relation of S,S;
let f,g be Function of S,BOOLEAN;
let x be set;
func EUntill_univ(x,f,g,R) -> Element of BOOLEAN equals
:Def52:
TRUE if x in
S & ex pai being inf_path of R st (pai.0 = x & ex m being Element of NAT st (
for j being Element of NAT st j<m holds f.(pai.j) =TRUE ) & g.(pai.m) = TRUE )
otherwise FALSE;
correctness;
end;
definition
let S be non empty set;
let R be total Relation of S,S;
let f,g be set;
func EUntill_0(f,g,R) -> Element of ModelSP(S) means
:Def53:
for s being set
st s in S holds EUntill_univ(s,Fid(f,S),Fid(g,S),R)=TRUE iff (Fid(it,S)).s=TRUE
;
existence
proof
deffunc F(set,Function of S,BOOLEAN, Function of S,BOOLEAN) =EUntill_univ(
$1,$2,$3,R);
consider IT being set such that
A1: IT in ModelSP(S) and
A2: for s being set st s in S holds F(s,Fid(f,S),Fid(g,S)) =TRUE iff (
Fid(IT,S)).s=TRUE from Func2EX;
take IT;
thus thesis by A1,A2;
end;
uniqueness
proof
deffunc F(set,Function of S,BOOLEAN, Function of S,BOOLEAN) =EUntill_univ(
$1,$2,$3,R);
for h1,h2 being set st h1 in ModelSP(S) & (for s being set st s in S
holds F(s,Fid(f,S),Fid(g,S)) = TRUE iff (Fid(h1,S)).s=TRUE) & h2 in ModelSP(S)
& (for s being set st s in S holds F(s,Fid(f,S),Fid(g,S)) = TRUE iff (Fid(h2,S)
).s=TRUE) holds h1 = h2 from Func2Unique;
hence thesis;
end;
end;
Lm39: for o1,o2 being BinOp of ModelSP(S) st (for f,g being set st (f in
ModelSP(S)) & (g in ModelSP(S)) holds o1.(f,g) = EUntill_0(f,g,R)) & (for f,g
being set st (f in ModelSP(S)) & (g in ModelSP(S)) holds o2.(f,g) = EUntill_0(f
,g,R)) holds o1=o2
proof
set M = ModelSP(S);
deffunc O(Element of M,Element of M) = EUntill_0($1,$2,R);
A1: for o1,o2 being BinOp of M st (for f,g being Element of M holds o1.(f,g)
= O(f,g)) & (for f,g being Element of M holds o2.(f,g) = O(f,g)) holds o1=o2
from BINOP_2:sch 2;
for o1,o2 being BinOp of M st (for f,g being set st f in M & g in M
holds o1.(f,g) = EUntill_0(f,g,R)) & (for f,g being set st f in M & g in M
holds o2.(f,g) = EUntill_0(f,g,R)) holds o1=o2
proof
let o1,o2 be BinOp of M such that
A2: for f,g being set st f in M & g in M holds o1.(f,g) = EUntill_0(f, g,R) and
A3: for f,g being set st f in M & g in M holds o2.(f,g) = EUntill_0(f, g,R);
A4: for f,g being Element of M holds o2.(f,g) = O(f,g) by A3;
for f,g being Element of M holds o1.(f,g) = O(f,g) by A2;
hence thesis by A1,A4;
end;
hence thesis;
end;
definition
let S be non empty set;
let R be total Relation of S,S;
func EUntill_(R) -> BinOp of ModelSP(S) means
:Def54:
for f,g being set st f
in ModelSP(S) & g in ModelSP(S) holds it.(f,g) = EUntill_0(f,g,R);
existence
proof
set M = ModelSP(S);
deffunc O(Element of M,Element of M) = EUntill_0($1,$2,R);
consider o being BinOp of M such that
A1: for f,g being Element of M holds o.(f,g) = O(f,g) from BINOP_1:sch 4;
for f,g being set st f in M & g in M holds o.(f,g) = EUntill_0(f,g,R) by A1;
hence thesis;
end;
uniqueness by Lm39;
end;
:: definition of concrete object of CTL model by ModelSP
definition
let S be non empty set;
let X be non empty Subset of ModelSP(S);
let s be object;
func F_LABEL(s,X) -> Subset of X means
:Def55:
for x being object holds x in it
iff x in X & ex f being Function of S,BOOLEAN st f=x & f.s=TRUE;
existence
proof
defpred P[object] means
ex f being Function of S,BOOLEAN st f=$1 & f.s=TRUE;
consider IT being set such that
A1: for x being object holds x in IT iff x in X & P[x] from XBOOLE_0:sch
1;
for x being object holds x in IT implies x in X by A1;
then reconsider IT as Subset of X by TARSKI:def 3;
take IT;
thus thesis by A1;
end;
uniqueness
proof
defpred P[object] means
$1 in X & ex f being Function of S,BOOLEAN st f=$1 &
f.s=TRUE;
for X1,X2 being set st (for x being object holds x in X1 iff P[x]) &
(for
x being object holds x in X2 iff P[x]) holds X1 = X2 from XBOOLE_0:sch 3;
hence thesis;
end;
end;
definition
let S be non empty set;
let X be non empty Subset of ModelSP(S);
func Label_(X) -> Function of S,bool X means
:Def56:
for x being object st x in S holds it.x = F_LABEL(x,X);
existence
proof
deffunc F(object)=F_LABEL($1,X);
A1: for x being object st x in S holds F(x) in bool X;
consider IT be Function of S,bool X such that
A2: for x being object st x in S holds IT.x = F(x) from FUNCT_2:sch 2(A1);
take IT;
thus thesis by A2;
end;
uniqueness
proof
let G,H be Function of S,bool X such that
A3: for x being object st x in S holds G.x = F_LABEL(x,X) and
A4: for x being object st x in S holds H.x = F_LABEL(x,X);
for x being object st x in S holds G.x = H.x
proof
let x being object such that
A5: x in S;
G.x = F_LABEL(x,X) by A3,A5
.=H.x by A4,A5;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
end;
definition
let S be non empty set;
let S0 be Subset of S;
let R be total Relation of S,S;
let Prop be non empty Subset of ModelSP(S);
func KModel(R,S0,Prop) -> KripkeStr over Prop equals
KripkeStr (# S, S0, R,
Label_(Prop) #);
coherence;
end;
registration
let S be non empty set;
let S0 be Subset of S;
let R be total Relation of S,S;
let Prop be non empty Subset of ModelSP(S);
cluster the carrier of KModel(R,S0,Prop) -> non empty;
coherence;
end;
registration
let S be non empty set;
let S0 be Subset of S;
let R be total Relation of S,S;
let Prop be non empty Subset of ModelSP(S);
cluster ModelSP(the carrier of KModel(R,S0,Prop)) -> non empty for Subset of
Funcs(the carrier of KModel(R,S0,Prop),BOOLEAN);
coherence;
end;
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
func BASSModel(R,BASSIGN) -> CTLModelStr equals
CTLModelStr(# ModelSP(S),
BASSIGN, And_(S), Not_(S), EneXt_(R), EGlobal_(R), EUntill_(R) #);
coherence;
end;
registration
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
cluster BASSModel(R,BASSIGN) -> with_basic non empty;
coherence;
end;
reserve BASSIGN for non empty Subset of ModelSP(S);
reserve kai for Function of atomic_WFF,the BasicAssign of BASSModel(R,BASSIGN);
:: definition of correctness of Assign of BASSModel(R,BASSIGN)
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let s be Element of S;
let f be Assign of BASSModel(R,BASSIGN);
pred s |= f means
:Def59:
(Fid(f,S)).s=TRUE;
end;
notation
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let s be Element of S;
let f be Assign of BASSModel(R,BASSIGN);
antonym s |/= f for s |= f;
end;
theorem Th11:
for a being Assign of BASSModel(R,BASSIGN) st a in BASSIGN holds
s |= a iff a in (Label_(BASSIGN)).s
proof
let a be Assign of BASSModel(R,BASSIGN) such that
A1: a in BASSIGN;
thus s |= a implies a in (Label_(BASSIGN)).s
proof
set f = Fid(a,S);
assume s |= a;
then
A2: f.s=TRUE;
a= f by Def41;
then a in F_LABEL(s,BASSIGN) by A1,A2,Def55;
hence thesis by Def56;
end;
assume a in (Label_(BASSIGN)).s;
then a in F_LABEL(s,BASSIGN) by Def56;
then consider f being Function of S,BOOLEAN such that
A3: f =a and
A4: f.s=TRUE by Def55;
Fid(a,S)=f by A3,Def41;
hence thesis by A4;
end;
theorem Th12:
for f being Assign of BASSModel(R,BASSIGN) holds s |= 'not'(f) iff s |/= f
proof
let f be Assign of BASSModel(R,BASSIGN);
A1: 'not' f = Not_0(f,S) by Def43;
A2: s |/= f implies s |= ('not' f)
proof
assume s |/= f;
then not (Fid(f,S)).s =TRUE;
then not Castboolean (Fid(f,S)).s = TRUE by Def4;
then Castboolean (Fid(f,S)).s = FALSE by XBOOLEAN:def 3;
then 'not' (Castboolean (Fid(f,S)).s) =TRUE;
then (Fid('not'(f),S)).s =TRUE by A1,Def42;
hence thesis;
end;
s |= 'not'(f) implies s |/= f
proof
assume s |= ('not' f);
then (Fid(Not_0(f,S),S)).s = TRUE by A1;
then 'not' (Castboolean (Fid(f,S)).s) =TRUE by Def42;
then (Fid(f,S)).s = FALSE by Def4;
hence thesis;
end;
hence thesis by A2;
end;
theorem Th13:
for f,g being Assign of BASSModel(R,BASSIGN) holds s |= f '&' g
iff s|=f & s|=g
proof
let f,g be Assign of BASSModel(R,BASSIGN);
A1: f '&' g = And_0(f,g,S) by Def51;
A2: s |= f '&' g implies s|= f & s|= g
proof
assume s|= f '&' g;
then (Fid(And_0(f,g,S),S)).s=TRUE by A1;
then
A3: (Castboolean (Fid(f,S)).s) '&' (Castboolean (Fid(g,S)).s) =TRUE by Def50;
then Castboolean (Fid(g,S)).s=TRUE by XBOOLEAN:101;
then
A4: (Fid(g,S)).s=TRUE by Def4;
Castboolean (Fid(f,S)).s =TRUE by A3,XBOOLEAN:101;
then (Fid(f,S)).s =TRUE by Def4;
hence thesis by A4;
end;
s|= f & s|= g implies s |= f '&' g
proof
assume that
A5: s|= f and
A6: s|= g;
A7: (Fid(g,S)).s=TRUE by A6;
(Fid(f,S)).s=TRUE by A5;
then (Castboolean (Fid(f,S)).s) '&' (Castboolean (Fid(g,S)).s) =TRUE by A7
,Def4;
then (Fid(f '&' g,S)).s=TRUE by A1,Def50;
hence thesis;
end;
hence thesis by A2;
end;
theorem Th14:
for f being Assign of BASSModel(R,BASSIGN) holds s |= EX(f) iff
ex pai being inf_path of R st pai.0 = s & (pai.1) |= f
proof
let f be Assign of BASSModel(R,BASSIGN);
A1: EX(f) = EneXt_0(f,R) by Def46;
A2: (ex pai being inf_path of R st pai.0 = s & (pai.1) |= f) implies s |= EX
(f)
proof
assume
A3: ex pai being inf_path of R st pai.0 = s & (pai.1) |= f;
ex pai being inf_path of R st pai.0 = s & (Fid(f,S)).(pai.1) =TRUE
by A3;
then EneXt_univ(s,Fid(f,S),R)=TRUE by Def44;
then (Fid(EX(f),S)).s=TRUE by A1,Def45;
hence thesis;
end;
s |= EX(f) implies ex pai being inf_path of R st pai.0 = s & (pai.1) |= f
proof
assume s|= EX(f);
then (Fid(EneXt_0(f,R),S)).s=TRUE by A1;
then EneXt_univ(s,Fid(f,S),R)=TRUE by Def45;
then consider pai being inf_path of R such that
A4: pai.0 = s and
A5: (Fid(f,S)).(pai.1) =TRUE by Def44;
take pai;
thus thesis by A4,A5;
end;
hence thesis by A2;
end;
theorem Th15:
for f being Assign of BASSModel(R,BASSIGN) holds s |= EG(f) iff
ex pai being inf_path of R st pai.0 = s & for n being Element of NAT holds (pai
.n) |= f
proof
let f be Assign of BASSModel(R,BASSIGN);
A1: EG(f) = EGlobal_0(f,R) by Def49;
A2: (ex pai being inf_path of R st pai.0 = s & for n being Element of NAT
holds (pai.n) |= f) implies s |= EG(f)
proof
assume
A3: ex pai being inf_path of R st pai.0 = s & for n being Element of
NAT holds (pai.n) |= f;
ex pai being inf_path of R st pai.0 = s & for n being Element of NAT
holds (Fid(f,S)).(pai.n) =TRUE
proof
consider pai being inf_path of R such that
A4: pai.0 = s and
A5: for n being Element of NAT holds (pai.n) |= f by A3;
take pai;
for n being Element of NAT holds (Fid(f,S)).(pai.n) =TRUE
by A5,Def59;
hence thesis by A4;
end;
then EGlobal_univ(s,Fid(f,S),R)=TRUE by Def47;
then (Fid(EG(f),S)).s=TRUE by A1,Def48;
hence thesis;
end;
s |= EG(f) implies ex pai being inf_path of R st pai.0 = s & for n being
Element of NAT holds (pai.n) |= f
proof
assume s|= EG(f);
then (Fid(EGlobal_0(f,R),S)).s=TRUE by A1;
then EGlobal_univ(s,Fid(f,S),R)=TRUE by Def48;
then consider pai being inf_path of R such that
A6: pai.0 = s and
A7: for n being Element of NAT holds (Fid(f,S)).(pai.n) =TRUE by Def47;
take pai;
for n being Element of NAT holds (pai.n) |= f
by A7;
hence thesis by A6;
end;
hence thesis by A2;
end;
theorem Th16:
for f,g being Assign of BASSModel(R,BASSIGN) holds s |= f EU g
iff ex pai being inf_path of R st pai.0 = s & ex m being Element of NAT st (for
j being Element of NAT st j<m holds pai.j |= f) & pai.m |= g
proof
let f,g be Assign of BASSModel(R,BASSIGN);
A1: f EU g = EUntill_0(f,g,R) by Def54;
A2: (ex pai being inf_path of R st pai.0 = s & ex m being Element of NAT st
(for j being Element of NAT st j<m holds (pai.j) |= f) & (pai.m) |= g) implies
s |= f EU g
proof
assume
A3: ex pai being inf_path of R st pai.0 = s & ex m being Element of
NAT st (for j being Element of NAT st j<m holds (pai.j) |= f) & (pai.m) |= g;
ex pai being inf_path of R st pai.0 = s & ex m being Element of NAT
st (for j being Element of NAT st j<m holds (Fid(f,S)).(pai.j) =TRUE) & (Fid(g,
S)).(pai.m) =TRUE
proof
consider pai being inf_path of R such that
A4: pai.0 = s and
A5: ex m being Element of NAT st (for j being Element of NAT st j<m
holds (pai.j) |= f) & (pai.m) |= g by A3;
take pai;
ex m being Element of NAT st (for j being Element of NAT st j<m
holds (Fid(f,S)).(pai.j) =TRUE) & (Fid(g,S)).(pai.m) =TRUE
proof
consider m being Element of NAT such that
A6: for j being Element of NAT st j<m holds (pai.j) |= f and
A7: (pai.m) |= g by A5;
take m;
for j being Element of NAT st j<m holds (Fid(f,S)).(pai.j) =TRUE
by A6,Def59;
hence thesis by A7;
end;
hence thesis by A4;
end;
then EUntill_univ(s,Fid(f,S),Fid(g,S),R)=TRUE by Def52;
then (Fid(f EU g,S)).s=TRUE by A1,Def53;
hence thesis;
end;
s |= f EU g implies ex pai being inf_path of R st pai.0 = s & ex m being
Element of NAT st (for j being Element of NAT st j<m holds pai.j |= f) & pai.m
|= g
proof
assume s|= f EU g;
then (Fid(EUntill_0(f,g,R),S)).s=TRUE by A1;
then EUntill_univ(s,Fid(f,S),Fid(g,S),R)=TRUE by Def53;
then consider pai being inf_path of R such that
A8: pai.0 = s and
A9: ex m being Element of NAT st (for j being Element of NAT st j<m
holds (Fid(f,S)).(pai.j) =TRUE ) & (Fid(g,S)).(pai.m) =TRUE by Def52;
take pai;
ex m being Element of NAT st (for j being Element of NAT st j<m holds
(pai.j) |= f ) & (pai.m) |= g
proof
consider m being Element of NAT such that
A10: for j being Element of NAT st j<m holds (Fid(f,S)).(pai.j) =TRUE and
A11: (Fid(g,S)).(pai.m) =TRUE by A9;
take m;
for j being Element of NAT st j<m holds (pai.j) |= f
by A10;
hence thesis by A11;
end;
hence thesis by A8;
end;
hence thesis by A2;
end;
theorem Th17:
for f,g being Assign of BASSModel(R,BASSIGN) holds s |= f 'or' g
iff (s|= f or s|= g)
proof
let f,g be Assign of BASSModel(R,BASSIGN);
s |= f 'or' g iff not s|= 'not'(f) '&' 'not'(g) by Th12;
then s |= f 'or' g iff not s|= 'not'(f) or not s|= 'not'(g) by Th13;
hence thesis by Th12;
end;
:: definition of correctness of CTL-formula & its basic properties.
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let kai being Function of atomic_WFF,the BasicAssign of BASSModel(R,BASSIGN);
let s be Element of S;
let H be CTL-formula;
pred s,kai|= H means
:Def60:
s|= Evaluate(H,kai);
end;
notation
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let kai being Function of atomic_WFF,the BasicAssign of BASSModel(R,BASSIGN);
let s be Element of S;
let H be CTL-formula;
antonym s,kai|/= H for s,kai|= H;
end;
theorem
H is atomic implies (s,kai |= H iff kai.H in (Label_(BASSIGN)).s)
proof
assume
A1: H is atomic;
ex f be Function of CTL_WFF,the carrier of BASSModel(R, BASSIGN) st
f is-Evaluation-for kai & Evaluate(H,kai) = f.H by Def34;
then
A2: Evaluate(H,kai) = kai.H by A1;
H in atomic_WFF by A1;
then Evaluate(H,kai) in BASSIGN by A2,FUNCT_2:5;
hence thesis by A2,Th11;
end;
theorem
s,kai|= 'not' H iff s,kai|/= H
proof
s,kai|= 'not' H iff s|= 'not' Evaluate(H,kai) by Th5;
then s,kai|= 'not' H iff s|/= Evaluate(H,kai) by Th12;
hence thesis;
end;
theorem
s,kai|= H1 '&' H2 iff s,kai|= H1 & s,kai|= H2
proof
s,kai|= H1 '&' H2 iff s|= Evaluate(H1,kai) '&' Evaluate(H2,kai) by Th6;
then s,kai|= H1 '&' H2 iff s|= Evaluate(H1,kai) & s|= Evaluate(H2,kai) by
Th13;
hence thesis;
end;
theorem
s,kai|= H1 'or' H2 iff s,kai|= H1 or s,kai|= H2
proof
s,kai|= H1 'or' H2 iff s|= Evaluate(H1,kai) 'or' Evaluate(H2,kai) by
Th10;
then s,kai|= H1 'or' H2 iff s|= Evaluate(H1,kai) or s|= Evaluate(H2,kai) by
Th17;
hence thesis;
end;
theorem
s,kai|= EX H iff ex pai being inf_path of R st pai.0 = s & (pai.1),kai |= H
proof
A1: (ex pai being inf_path of R st pai.0 = s & (pai.1) |= Evaluate(H,kai) )
implies ex pai being inf_path of R st pai.0 = s & (pai.1),kai|= H
by Def60;
s,kai|= EX H iff s|= EX Evaluate(H,kai) by Th7;
hence thesis by A1,Th14;
end;
theorem
s,kai|= EG H iff ex pai being inf_path of R st pai.0 = s & for n being
Element of NAT holds (pai.n),kai|= H
proof
A1: (ex pai being inf_path of R st pai.0 = s & for n being Element of NAT
holds (pai.n)|= Evaluate(H,kai) ) implies ex pai being inf_path of R st pai.0 =
s & for n being Element of NAT holds (pai.n),kai|= H
proof
given pai be inf_path of R such that
A2: pai.0 = s and
A3: for n being Element of NAT holds (pai.n)|= Evaluate(H,kai);
take pai;
for n being Element of NAT holds (pai.n),kai|= H
by A3;
hence thesis by A2;
end;
A4: (ex pai being inf_path of R st pai.0 = s & for n being Element of NAT
holds (pai.n),kai|= H ) implies ex pai being inf_path of R st pai.0 = s & for n
being Element of NAT holds (pai.n)|= Evaluate(H,kai)
proof
given pai be inf_path of R such that
A5: pai.0 = s and
A6: for n being Element of NAT holds (pai.n),kai|= H;
take pai;
for n being Element of NAT holds (pai.n)|= Evaluate(H,kai)
by A6,Def60;
hence thesis by A5;
end;
s,kai|= EG H iff s|= EG Evaluate(H,kai) by Th8;
hence thesis by A1,A4,Th15;
end;
theorem
s,kai|= H1 EU H2 iff ex pai being inf_path of R st pai.0 = s & ex m
being Element of NAT st (for j being Element of NAT st j<m holds pai.j,kai|= H1
) & pai.m,kai|= H2
proof
A1: (ex pai being inf_path of R st pai.0 = s & ex m being Element of NAT st
(for j being Element of NAT st j<m holds pai.j |= Evaluate(H1,kai)) & (pai.m |=
Evaluate(H2,kai)) ) implies ex pai being inf_path of R st pai.0 = s & ex m
being Element of NAT st (for j being Element of NAT st j<m holds pai.j,kai|= H1
) & pai.m,kai|= H2
proof
given pai be inf_path of R such that
A2: pai.0 = s and
A3: ex m being Element of NAT st (for j being Element of NAT st j<m
holds pai.j |= Evaluate(H1,kai)) & pai.m |= Evaluate(H2,kai);
take pai;
consider m be Element of NAT such that
A4: for j being Element of NAT st j<m holds pai.j |= Evaluate(H1,kai) and
A5: pai.m |= Evaluate(H2,kai) by A3;
A6: for j being Element of NAT st j<m holds pai.j,kai|= H1
by A4;
pai.m |= Evaluate(H2,kai) iff pai.m,kai|= H2;
hence thesis by A2,A5,A6;
end;
A7: (ex pai being inf_path of R st pai.0 = s & ex m being Element of NAT st
(for j being Element of NAT st j<m holds pai.j,kai|= H1) & (pai.m,kai|= H2) )
implies ex pai being inf_path of R st pai.0 = s & ex m being Element of NAT st
(for j being Element of NAT st j<m holds pai.j |= Evaluate(H1,kai)) & pai.m |=
Evaluate(H2,kai)
proof
given pai be inf_path of R such that
A8: pai.0 = s and
A9: ex m being Element of NAT st (for j being Element of NAT st j<m
holds pai.j,kai|= H1) & pai.m,kai|= H2;
take pai;
consider m be Element of NAT such that
A10: for j being Element of NAT st j<m holds pai.j,kai|= H1 and
A11: pai.m,kai|= H2 by A9;
A12: for j being Element of NAT st j<m holds pai.j |= Evaluate(H1,kai)
by A10,Def60;
thus thesis by A8,A11,A12;
end;
s,kai|= H1 EU H2 iff s|= Evaluate(H1,kai) EU Evaluate(H2,kai) by Th9;
hence thesis by A1,A7,Th16;
end;
::Some basic theorems for external Mizar files.
theorem Th25:
for s0 holds ex pai being inf_path of R st pai.0 = s0
proof
let s0;
consider pai being sequence of S such that
A1: pai.0=s0 and
A2: for n being Nat holds [pai.n,pai.(n+1)] in R by Lm33;
reconsider pai as inf_path of R by A2,Def39;
take pai;
thus thesis by A1;
end;
theorem
for R being Relation of S,S holds R is total iff for x being set st x
in S holds ex y being set st y in S & [x,y] in R by Lm30,Lm31;
::*************
::
::Verification of the basic algorithm
:: for Model checking based on CTL.
::
::the basic algorithm is solver to get
:: {s where s is Element of S: s,kai|=H}
::
::*************
definition
let S be non empty set;
let R be total Relation of S,S;
let s0 be Element of S;
let pai be inf_path of R;
let n be object;
func PrePath(n,s0,pai) -> Element of S equals
:Def61:
s0 if n=0 otherwise
pai.(k_nat(k_nat(n)-1));
correctness;
end;
theorem Th27:
[s0,s1] in R implies ex pai being inf_path of R st pai.0 = s0 & pai.1=s1
proof
consider pai1 be inf_path of R such that
A1: pai1.0 = s1 by Th25;
deffunc F(object) = PrePath($1,s0,pai1);
A2: for x being object st x in NAT holds F(x) in S;
consider pai be sequence of S such that
A3: for n being object st n in NAT holds pai.n= F(n) from FUNCT_2:sch 2(A2);
assume
A4: [s0,s1] in R;
for n being Nat holds [pai.n,pai.(n+1)] in R
proof
let n be Nat;
set n1=n+1;
set n0=n-1;
per cases;
suppose
A5: n = 0;
then
A6: k_nat(k_nat(n1)-1) = k_nat(1-1) by Def2
.= 0 by Def2;
A7: pai.n = F(n) by A3,A5
.= s0 by A5,Def61;
pai.n1 = F(n1) by A3
.= s1 by A1,A6,Def61;
hence thesis by A4,A7;
end;
suppose
A8: n<>0;
then reconsider n0 as Element of NAT by NAT_1:20;
A9: pai.n1 = F(n1) by A3
.= pai1.(k_nat(k_nat(n1)-1)) by Def61
.= pai1.(k_nat(n1-1)) by Def2
.= pai1.(n0+1) by Def2;
A10: n in NAT by ORDINAL1:def 12;
then
pai.n = F(n) by A3
.= pai1.(k_nat(k_nat(n)-1)) by A8,Def61
.= pai1.(k_nat(n-1)) by Def2,A10
.= pai1.n0 by Def2;
hence thesis by A9,Def39;
end;
end;
then reconsider pai as inf_path of R by Def39;
A11: pai.0= F(0) by A3
.= s0 by Def61;
take pai;
pai.1 = F(1) by A3
.= pai1.(k_nat(k_nat(1)-1)) by Def61
.= pai1.(k_nat(1-1)) by Def2
.= s1 by A1,Def2;
hence thesis by A11;
end;
theorem Th28:
for f being Assign of BASSModel(R,BASSIGN) holds s |= EX(f) iff
ex s1 being Element of S st [s,s1] in R & s1 |= f
proof
let f be Assign of BASSModel(R,BASSIGN);
A1: s |= EX(f) implies ex s1 being Element of S st [s,s1] in R & s1 |= f
proof
assume s |= EX(f);
then consider pai be inf_path of R such that
A2: pai.0 = s and
A3: (pai.1) |= f by Th14;
[pai.0,pai.(0+1)] in R by Def39;
hence thesis by A2,A3;
end;
(ex s1 being Element of S st [s,s1] in R & s1 |= f ) implies s |= EX(f)
proof
given s1 be Element of S such that
A4: [s,s1] in R and
A5: s1 |= f;
ex pai be inf_path of R st pai.0 = s & pai.1 = s1 by A4,Th27;
hence thesis by A5,Th14;
end;
hence thesis by A1;
end;
:: definition of predecessor
definition
let S be non empty set;
let R be total Relation of S,S;
let H be Subset of S;
func Pred(H,R) -> Subset of S equals
{ s where s is Element of S : ex t
being Element of S st t in H & [s,t] in R };
coherence
proof
set P = { s where s is Element of S : ex t being Element of S st t in H &
[s,t] in R };
P c= S
proof
let x be object;
assume x in P;
then
ex s be Element of S st x=s & ex t being Element of S st t in H &
[s,t] in R;
hence thesis;
end;
hence thesis;
end;
end;
:: definition of SIGMA
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let f be Assign of BASSModel(R,BASSIGN);
func SIGMA(f) -> Subset of S equals
{ s where s is Element of S : s|= f };
correctness
proof
set P = { s where s is Element of S : s|= f };
P c= S
proof
let x be object;
assume x in P;
then ex s be Element of S st x=s & s|= f;
hence thesis;
end;
hence thesis;
end;
end;
Lm40: for f being Assign of BASSModel(R,BASSIGN) holds SIGMA(f) = { s where s
is Element of S : (Fid(f,S)).s=TRUE }
proof
let f be Assign of BASSModel(R,BASSIGN);
A1: for x being object holds x in { s where s is Element of S : (Fid(f,S)).s=
TRUE } implies x in SIGMA(f)
proof
let x be object;
assume x in { s where s is Element of S : (Fid(f,S)).s=TRUE };
then consider s be Element of S such that
A2: x=s and
A3: (Fid(f,S)).s=TRUE;
s|= f by A3;
hence thesis by A2;
end;
for x being object holds x in SIGMA(f) implies x in { s where s is Element
of S : (Fid(f,S)).s=TRUE }
proof
let x be object;
assume x in SIGMA(f);
then consider s be Element of S such that
A4: x=s and
A5: s|= f;
(Fid(f,S)).s=TRUE by A5;
hence thesis by A4;
end;
hence thesis by A1,TARSKI:2;
end;
Lm41: for X being non empty set, f,g being Function of X, BOOLEAN holds { x
where x is Element of X : f.x=TRUE } = { x where x is Element of X : g.x=TRUE }
implies f =g
proof
let X be non empty set;
let f,g be Function of X, BOOLEAN;
set F = { x where x is Element of X : f.x=TRUE };
set G = { x where x is Element of X : g.x=TRUE };
assume that
A1: F = G;
for p being object st p in X holds f.p = g.p
proof
let p be object such that
A2: p in X;
per cases;
suppose
A3: p in F;
then
A4: ex x1 being Element of X st x1=p & f.x1=TRUE;
ex x2 being Element of X st x2=p & g.x2=TRUE by A1,A3;
hence thesis by A4;
end;
suppose
A5: not p in F;
A6: f.p = FALSE
proof
assume
A7: f.p <> FALSE;
f.p in BOOLEAN by A2,FUNCT_2:5;
then f.p=TRUE by A7,TARSKI:def 2;
hence contradiction by A2,A5;
end;
g.p = FALSE
proof
assume
A8: g.p <> FALSE;
g.p in BOOLEAN by A2,FUNCT_2:5;
then g.p=TRUE by A8,TARSKI:def 2;
hence contradiction by A1,A2,A5;
end;
hence thesis by A6;
end;
end;
hence thesis by FUNCT_2:12;
end;
Lm42: for f, g being Assign of BASSModel(R,BASSIGN) holds Fid(f,S) = Fid(g,S)
implies f =g
proof
let f,g be Assign of BASSModel(R,BASSIGN);
Fid(f,S) = f by Def41;
hence thesis by Def41;
end;
:: SIGMA is one to one.
theorem
for f, g being Assign of BASSModel(R,BASSIGN) holds SIGMA(f) = SIGMA(g)
implies f=g
proof
let f,g be Assign of BASSModel(R,BASSIGN);
assume
A1: SIGMA(f) = SIGMA(g);
SIGMA(f) = { s where s is Element of S : (Fid(f,S)).s=TRUE } by Lm40;
then { s where s is Element of S : (Fid(f,S)).s=TRUE } = { s where s is
Element of S : (Fid(g,S)).s=TRUE } by A1,Lm40;
hence thesis by Lm41,Lm42;
end;
:: definition of Tau (inverse of SIGMA).
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let T be Subset of S;
func Tau(T,R,BASSIGN) -> Assign of BASSModel(R,BASSIGN) means
:Def64:
for s being set st s in S holds (Fid(it,S)).s = chi(T,S).s;
existence
proof
deffunc F(object) = chi(T,S).$1;
A1: for x being object st x in S holds F(x) in BOOLEAN
proof
let x be object such that
A2: x in S;
per cases;
suppose
x in T;
then F(x) = 1 by FUNCT_3:def 3;
hence thesis by TARSKI:def 2;
end;
suppose
not x in T;
then F(x) = 0 by A2,FUNCT_3:def 3;
hence thesis by TARSKI:def 2;
end;
end;
consider IT being Function of S,BOOLEAN such that
A3: for x being object st x in S holds IT.x = F(x) from FUNCT_2:sch 2(A1);
reconsider IT as Assign of BASSModel(R,BASSIGN) by FUNCT_2:8;
take IT;
Fid(IT,S) = IT by Def41;
hence thesis by A3;
end;
uniqueness
proof
let f1,f2 be Assign of BASSModel(R,BASSIGN) such that
A4: for s being set st s in S holds (Fid(f1,S)).s = chi(T,S).s and
A5: for s being set st s in S holds (Fid(f2,S)).s = chi(T,S).s;
for s being object st s in S holds (Fid(f1,S)).s = (Fid(f2,S)).s
proof
let s be object such that
A6: s in S;
(Fid(f1,S)).s = chi(T,S).s by A4,A6
.= (Fid(f2,S)).s by A5,A6;
hence thesis;
end;
hence thesis by Lm42,FUNCT_2:12;
end;
end;
:: Tau is one to one.
theorem
for T1,T2 being Subset of S holds Tau(T1,R,BASSIGN) = Tau(T2,R,BASSIGN
) implies T1=T2
proof
let T1,T2 be Subset of S;
set h1 = Tau(T1,R,BASSIGN);
set h2 = Tau(T2,R,BASSIGN);
assume
A1: h1 = h2;
A2: for s being object holds s in T2 implies s in T1
proof
let s be object;
assume
A3: s in T2;
then chi(T2,S).s =1 by FUNCT_3:def 3;
then (Fid(h2,S)).s =TRUE by A3,Def64;
then chi(T1,S).s = 1 by A1,A3,Def64;
hence thesis by FUNCT_3:36;
end;
for s being object holds s in T1 implies s in T2
proof
let s be object;
assume
A4: s in T1;
then chi(T1,S).s =1 by FUNCT_3:def 3;
then (Fid(h1,S)).s =TRUE by A4,Def64;
then chi(T2,S).s = 1 by A1,A4,Def64;
hence thesis by FUNCT_3:36;
end;
hence thesis by A2,TARSKI:2;
end;
:: Tau is on to.
theorem Th31:
for f being Assign of BASSModel(R,BASSIGN) holds Tau(SIGMA(f),R, BASSIGN) = f
proof
let f be Assign of BASSModel(R,BASSIGN);
set T = SIGMA(f);
set g = Tau(T,R,BASSIGN);
A1: T = { s where s is Element of S : (Fid(f,S)).s=TRUE } by Lm40;
for s being object st s in S holds Fid(f,S).s= Fid(g,S).s
proof
let s be object;
assume s in S;
then reconsider s as Element of S;
per cases;
suppose
A2: s in T;
A3: Fid(g,S).s = chi(T,S).s by Def64
.= 1 by A2,FUNCT_3:def 3;
ex x being Element of S st x=s & (Fid(f,S)).x=TRUE by A1,A2;
hence thesis by A3;
end;
suppose
A4: not s in T;
A5: (Fid(f,S)).s=FALSE
proof
assume (Fid(f,S)).s <> FALSE;
then (Fid(f,S)).s= TRUE by TARSKI:def 2;
hence contradiction by A1,A4;
end;
Fid(g,S).s = chi(T,S).s by Def64
.=0 by A4,FUNCT_3:def 3;
hence thesis by A5;
end;
end;
hence thesis by Lm42,FUNCT_2:12;
end;
:: SIGMA is on to.
theorem Th32:
for T being Subset of S holds SIGMA(Tau(T,R,BASSIGN)) = T
proof
let T be Subset of S;
set f = Tau(T,R,BASSIGN);
set U = SIGMA(f);
A1: U = { s where s is Element of S : (Fid(f,S)).s=TRUE } by Lm40;
for s being object holds s in U iff s in T
proof
let s be object;
thus s in U implies s in T
proof
assume s in U;
then ex t being Element of S st s = t & (Fid(f,S)).t=TRUE by A1;
then chi(T,S).s =TRUE by Def64;
hence thesis by FUNCT_3:36;
end;
assume
A2: s in T;
then (Fid(f,S)).s = chi(T,S).s by Def64
.= 1 by A2,FUNCT_3:def 3;
hence thesis by A1,A2;
end;
hence thesis by TARSKI:2;
end;
:: SIGMA is homomorphism .
theorem Th33:
for f,g being Assign of BASSModel(R,BASSIGN) holds SIGMA('not' f)
= S \ SIGMA(f) & SIGMA(f '&' g) = SIGMA(f) /\ SIGMA(g) & SIGMA(f 'or' g) =
SIGMA(f) \/ SIGMA(g)
proof
let f,g be Assign of BASSModel(R,BASSIGN);
A1: for s being object holds s in SIGMA('not' f) iff s in S \ SIGMA(f)
proof
let s be object;
A2: s in SIGMA('not' f) implies s in S \ SIGMA(f)
proof
assume
A3: s in SIGMA('not' f);
then
A4: ex x being Element of S st x = s & x |= 'not' f;
reconsider s as Element of S by A3;
not s in SIGMA(f)
proof
assume s in SIGMA(f);
then ex y being Element of S st y = s & y |= f;
hence contradiction by A4,Th12;
end;
hence thesis by XBOOLE_0:def 5;
end;
s in S \ SIGMA(f) implies s in SIGMA('not' f)
proof
assume
A5: s in S \ SIGMA(f);
then reconsider s as Element of S;
not s in SIGMA(f) by A5,XBOOLE_0:def 5;
then s |/= f;
then s |= 'not' f by Th12;
hence thesis;
end;
hence thesis by A2;
end;
A6: for s being object
holds s in SIGMA(f 'or' g) iff s in SIGMA(f) \/ SIGMA(g )
proof
let s be object;
A7: s in SIGMA(f) \/ SIGMA(g) implies s in SIGMA(f 'or' g)
proof
assume
A8: s in SIGMA(f) \/ SIGMA(g);
per cases by A8,XBOOLE_0:def 3;
suppose
A9: s in SIGMA(f);
then
A10: ex x being Element of S st x = s & x |= f;
reconsider s as Element of S by A9;
s |= f 'or' g by A10,Th17;
hence thesis;
end;
suppose
A11: s in SIGMA(g);
then
A12: ex x being Element of S st x = s & x |= g;
reconsider s as Element of S by A11;
s |= f 'or' g by A12,Th17;
hence thesis;
end;
end;
s in SIGMA(f 'or' g) implies s in SIGMA(f) \/ SIGMA(g)
proof
assume
A13: s in SIGMA(f 'or' g);
then
A14: ex x being Element of S st x = s & x |= f 'or' g;
reconsider s as Element of S by A13;
per cases by A14,Th17;
suppose
s|= f;
then s in SIGMA(f);
hence thesis by XBOOLE_0:def 3;
end;
suppose
s|= g;
then s in SIGMA(g);
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis by A7;
end;
for s being object holds s in SIGMA(f '&' g) iff s in SIGMA(f) /\ SIGMA(g)
proof
let s be object;
thus s in SIGMA(f '&' g) implies s in SIGMA(f) /\ SIGMA(g)
proof
assume
A15: s in SIGMA(f '&' g);
then
A16: ex x being Element of S st x = s & x |= f '&' g;
reconsider s as Element of S by A15;
s|= g by A16,Th13;
then
A17: s in SIGMA(g);
s|= f by A16,Th13;
then s in SIGMA(f);
hence thesis by A17,XBOOLE_0:def 4;
end;
assume
A18: s in SIGMA(f) /\ SIGMA(g);
then
A19: s in SIGMA(g) by XBOOLE_0:def 4;
s in SIGMA(f) by A18,XBOOLE_0:def 4;
then
A20: ex x being Element of S st x = s & x |= f;
reconsider s as Element of S by A18;
ex y being Element of S st y = s & y |= g by A19;
then s |= f '&' g by A20,Th13;
hence thesis;
end;
hence thesis by A1,A6,TARSKI:2;
end;
:: Tau is monotonic.
theorem Th34:
for G1,G2 being Subset of S holds G1 c= G2 implies for s being
Element of S holds s|= Tau(G1,R,BASSIGN) implies s|= Tau(G2,R,BASSIGN)
proof
let G1,G2 be Subset of S;
set Tau1 = Tau(G1,R,BASSIGN);
set Tau2 = Tau(G2,R,BASSIGN);
assume
A1: G1 c= G2;
let s be Element of S;
assume s|= Tau1;
then (Fid(Tau1,S)).s = TRUE;
then chi(G1,S).s =1 by Def64;
then s in G1 by FUNCT_3:def 3;
then chi(G2,S).s =1 by A1,FUNCT_3:def 3;
then (Fid(Tau2,S)).s = TRUE by Def64;
hence thesis;
end;
:: SIGMA is monotonic.
theorem Th35:
for f1,f2 being Assign of BASSModel(R,BASSIGN) holds (for s being
Element of S holds s|= f1 implies s|= f2) implies SIGMA(f1) c= SIGMA(f2)
proof
let f1,f2 be Assign of BASSModel(R,BASSIGN);
assume
A1: for s being Element of S holds s|= f1 implies s|= f2;
let x be object;
assume x in SIGMA(f1);
then consider s be Element of S such that
A2: x=s and
A3: s|= f1;
s|= f2 by A1,A3;
hence thesis by A2;
end;
:: theorems for translation
:: problem of
:: (1)find status s st s |= EG(f)
:: (2)find status s st s |= f EU g
:: to "find fixpoint of some function of bool S -> bool S".
:: definition Fax(f,*):carrier ->carrier
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let f,g be Assign of BASSModel(R,BASSIGN);
func Fax(f,g) -> Assign of BASSModel(R,BASSIGN) equals
f '&' EX(g);
correctness;
end;
:: Fax(f,*) is monotonic.
theorem Th36:
for f,g1,g2 being Assign of BASSModel(R,BASSIGN) holds (for s
being Element of S holds s|= g1 implies s|= g2) implies for s being Element of
S holds s|= Fax(f,g1) implies s|= Fax(f,g2)
proof
let f,g1,g2 be Assign of BASSModel(R,BASSIGN);
assume
A1: for s being Element of S holds s|= g1 implies s|= g2;
let s be Element of S;
assume
A2: s|= Fax(f,g1);
then s|= EX(g1) by Th13;
then consider pai be inf_path of R such that
A3: pai.0 = s and
A4: (pai.1) |= g1 by Th14;
(pai.1) |= g2 by A1,A4;
then
A5: s|= EX(g2) by A3,Th14;
s|= f by A2,Th13;
hence thesis by A5,Th13;
end;
::commutative
:: Fax(f,*)
:: Assigns ------> Assigns
:: | |
:: SIGMA | | Tau
:: v v
:: bool S -------> bool S
:: SigFaxTau(f,*)
::
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let f be Assign of BASSModel(R,BASSIGN);
let G be Subset of S;
func SigFaxTau(f,G,R,BASSIGN) -> Subset of S equals
SIGMA(Fax(f,Tau(G,R,
BASSIGN)));
coherence;
end;
:: SigFaxTau(f,*) is monotonic.
theorem Th37:
for f being Assign of BASSModel(R,BASSIGN), G1,G2 being Subset of
S holds G1 c= G2 implies SigFaxTau(f,G1,R,BASSIGN) c= SigFaxTau(f,G2,R,BASSIGN)
proof
let f be Assign of BASSModel(R,BASSIGN);
let G1,G2 be Subset of S;
assume G1 c= G2;
then
for s being Element of S holds s|= Tau(G1,R,BASSIGN) implies s|= Tau(G2,
R,BASSIGN) by Th34;
then
for s being Element of S holds s|= Fax(f,Tau(G1,R,BASSIGN)) implies s|=
Fax(f,Tau(G2,R,BASSIGN)) by Th36;
hence thesis by Th35;
end;
:: Some tools to treat path.
definition
let S be non empty set;
let R be total Relation of S,S;
let pai be inf_path of R;
let k be Element of NAT;
func PathShift(pai,k) -> inf_path of R means
:Def67:
for n being Element of NAT holds it.n = pai.(n+k);
existence
proof
deffunc PAI1(object) = pai.(k_nat($1)+k);
A1: for x being object st x in NAT holds PAI1(x) in S;
consider IT being sequence of S such that
A2: for n being object st n in NAT holds IT.n= PAI1(n) from FUNCT_2:sch 2
(A1 );
A3: for n being Nat holds IT.n = pai.(n+k)
proof
let n be Nat;
A4: n in NAT by ORDINAL1:def 12;
then PAI1(n) = pai.(n+k) by Def2;
hence thesis by A2,A4;
end;
for n being Nat holds [IT.n,IT.(n+1)] in R
proof
let n be Nat;
set n1 = n+1;
set n2 = n+k;
A5: IT.(n+1) = pai.(n1+k) by A3
.= pai.(n2+1);
IT.n = pai.n2 by A3;
hence thesis by A5,Def39;
end;
then reconsider IT as inf_path of R by Def39;
take IT;
thus thesis by A3;
end;
uniqueness
proof
for pai1,pai2 being inf_path of R st (for n being Element of NAT holds
pai1.n = pai.(n+k)) & (for n being Element of NAT holds pai2.n = pai.(n+k))
holds pai1 = pai2
proof
let pai1,pai2 be inf_path of R such that
A6: for n being Element of NAT holds pai1.n = pai.(n+k) and
A7: for n being Element of NAT holds pai2.n = pai.(n+k);
for x being object st x in NAT holds pai1.x = pai2.x
proof
let x be object;
assume x in NAT;
then reconsider x as Element of NAT;
pai1.x = pai.(x+k) by A6
.= pai2.x by A7;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
hence thesis;
end;
end;
definition
let S be non empty set;
let R be total Relation of S,S;
let pai1,pai2 be inf_path of R;
let n,k be Nat;
func PathChange(pai1,pai2,k,n) -> set equals
:Def68:
pai1.n if n<k otherwise
pai2.(n-k);
correctness;
end;
definition
let S be non empty set;
let R be total Relation of S,S;
let pai1,pai2 be inf_path of R;
let k be Nat;
func PathConc(pai1,pai2,k) -> sequence of S means
:Def69:
for n being Nat holds it.n = PathChange(pai1,pai2,k,n);
existence
proof
deffunc F1(object) = PathChange(pai1,pai2,k,k_nat($1));
A1: for n being object st n in NAT holds F1(n) in S
proof
let n be object;
assume n in NAT;
then reconsider n as Element of NAT;
set x = PathChange(pai1,pai2,k,n);
A2: F1(n) = PathChange(pai1,pai2,k,n) by Def2;
per cases;
suppose
n < k;
then x = pai1.n by Def68;
hence thesis by A2;
end;
suppose
A3: not n < k;
set m = n - k;
reconsider m as Element of NAT by A3,NAT_1:21;
x = pai2.m by A3,Def68;
hence thesis by A2;
end;
end;
consider IT being sequence of S such that
A4: for n being object st n in NAT holds IT.n= F1(n) from FUNCT_2:sch 2(
A1);
take IT;
let n be Nat;
n in NAT by ORDINAL1:def 12;
then k_nat(n) = n by Def2;
hence thesis by A4;
end;
uniqueness
proof
let f1,f2 be sequence of S such that
A5: for n being Nat holds f1.n = PathChange(pai1,pai2,k,n) and
A6: for n being Nat holds f2.n = PathChange(pai1,pai2,k,n);
for x being object st x in NAT holds f1.x = f2.x
proof
let x be object;
assume x in NAT;
then reconsider x as Element of NAT;
f1.x = PathChange(pai1,pai2,k,x) by A5
.= f2.x by A6;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
end;
theorem Th38:
for pai1,pai2 being inf_path of R, k being Element of NAT holds
pai1.k = pai2.0 implies PathConc(pai1,pai2,k) is inf_path of R
proof
let pai1,pai2 be inf_path of R;
let k be Element of NAT;
set pai = PathConc(pai1,pai2,k);
assume
A1: pai1.k = pai2.0;
for n being Nat holds [pai.n,pai.(n+1)] in R
proof
let n be Nat;
set n1=n+1;
per cases by XXREAL_0:1;
suppose
A2: n1 < k;
then
A3: n < k by NAT_1:13;
A4: pai.n = PathChange(pai1,pai2,k,n) by Def69
.= pai1.n by A3,Def68;
pai.n1 = PathChange(pai1,pai2,k,n1) by Def69
.=pai1.n1 by A2,Def68;
hence thesis by A4,Def39;
end;
suppose
A5: n1 = k;
then
A6: n < k by NAT_1:13;
A7: pai.n = PathChange(pai1,pai2,k,n) by Def69
.= pai1.n by A6,Def68;
pai.n1 = PathChange(pai1,pai2,k,n1) by Def69
.= pai2.(n1-k) by A5,Def68
.= pai1.n1 by A1,A5;
hence thesis by A7,Def39;
end;
suppose
A8: k < n1;
then
A9: k <= n by NAT_1:13;
then reconsider m = n - k as Element of NAT by NAT_1:21;
A10: pai.n1 = PathChange(pai1,pai2,k,n1) by Def69
.= pai2.(n1-k) by A8,Def68
.= pai2.(m+1);
pai.n = PathChange(pai1,pai2,k,n) by Def69
.= pai2.m by A9,Def68;
hence thesis by A10,Def39;
end;
end;
hence thesis by Def39;
end;
:: EG(f) is fixpoint of Fax(f,*).
theorem Th39:
for f being Assign of BASSModel(R,BASSIGN), s being Element of S
holds s|= EG(f) iff s|= Fax(f,EG(f))
proof
let f be Assign of BASSModel(R,BASSIGN);
let s be Element of S;
set g = EG(f);
thus s|= EG(f) implies s|= Fax(f,EG(f))
proof
set g = EG(f);
assume s|= EG(f);
then consider pai be inf_path of R such that
A1: pai.0 = s and
A2: for n being Element of NAT holds pai.n |= f by Th15;
set pai1 = PathShift(pai,1);
A3: for n being Element of NAT holds pai1.n |= f
proof
let n be Element of NAT;
set n1 = n+1;
pai1.n = pai.n1 by Def67;
hence thesis by A2;
end;
pai.(0+1) = pai1.0 by Def67;
then pai.1 |= g by A3,Th15;
then
A4: s |= EX(g) by A1,Th14;
s |= f by A1,A2;
hence thesis by A4,Th13;
end;
assume
A5: s|= Fax(f,g);
then s|= EX(g) by Th13;
then consider pai1 be inf_path of R such that
A6: pai1.0 = s and
A7: (pai1.1) |= g by Th14;
consider pai2 being inf_path of R such that
A8: pai2.0 = pai1.1 and
A9: for n being Element of NAT holds (pai2.n) |= f by A7,Th15;
set pai = PathConc(pai1,pai2,1);
reconsider pai as inf_path of R by A8,Th38;
A10: pai.0 = PathChange(pai1,pai2,1,0) by Def69
.= s by A6,Def68;
for n being Element of NAT holds pai.n |= f
proof
let n be Element of NAT;
per cases;
suppose
A11: n < 1;
n=0
proof
assume
A12: n <> 0;
n<0+1 by A11;
hence contradiction by A12,NAT_1:22;
end;
hence thesis by A5,A10,Th13;
end;
suppose
A13: not n < 1;
then reconsider m = n-1 as Element of NAT by NAT_1:21;
pai.n = PathChange(pai1,pai2,1,n) by Def69
.= pai2.m by A13,Def68;
hence thesis by A9;
end;
end;
hence thesis by A10,Th15;
end;
:: Existence path for fixpoint of Fax(f,*).
theorem Th40:
for g being Assign of BASSModel(R,BASSIGN), s0 being Element of S
st s0 |= g holds (for s being Element of S holds s|= g implies s|= EX(g))
implies ex pai being inf_path of R st pai.0= s0 & for n being Nat
holds pai.In(n,NAT) |= g
proof
let g be Assign of BASSModel(R,BASSIGN);
let s0 be Element of S such that
A1: s0 |= g;
deffunc Next(object) = {x where x is Element of S : [$1,x] in R};
assume
A2: for s being Element of S holds s|= g implies s|= EX(g);
for p being set st p in BOOL S holds p<>{} by ORDERS_1:1;
then consider Choice being Function such that
A3: dom Choice = BOOL S and
A4: for p being set st p in BOOL S holds Choice.p in p by FUNCT_1:111;
deffunc H(object) = UnivF((Next($1) /\ SIGMA(g)),Choice,s0);
A5: for x being object st x in S holds H(x) in S
proof
let x be object such that
x in S;
set Y = Next(x) /\ SIGMA(g);
per cases;
suppose
A6: Y in dom Choice;
then H(x)= Choice.Y by Def3;
then H(x) in Y by A3,A4,A6;
then H(x) in Next(x) by XBOOLE_0:def 4;
then ex z be Element of S st z=H(x) & [x,z] in R;
hence thesis;
end;
suppose
not Y in dom Choice;
then H(x)= s0 by Def3;
hence thesis;
end;
end;
consider h being Function of S,S such that
A7: for x being object st x in S holds h.x= H(x) from FUNCT_2:sch 2(A5);
deffunc PAI(object) = (h|**(k_nat($1))).s0;
A8: for n being object st n in NAT holds PAI(n) in S;
consider pai being sequence of S such that
A9: for n being object st n in NAT holds pai.n= PAI(n) from FUNCT_2:sch 2(
A8 );
A10: pai.0 = PAI(0) by A9
.= (h|**0).s0 by Def2
.= (id S).s0 by FUNCT_7:84
.= s0;
A11: s0 in S;
A12: for n being Nat holds [pai.n,pai.(n+1)] in R & pai.In(n,NAT) |= g
proof
defpred P[Nat] means [pai.$1,pai.($1+1)] in R & pai.In($1,NAT) |= g;
A13: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
set k1=k+1;
set k2=k1+1;
set p0 = pai.In(k,NAT);
set p1 = pai.k1;
set p2 = pai.k2;
set Y1 = Next(p0) /\ SIGMA(g);
set Y2 = Next(p1) /\ SIGMA(g);
A14: s0 in dom (h|**k) by A11,FUNCT_2:def 1;
assume P[k];
then p0 |= EX(g) by A2;
then consider pai01 be inf_path of R such that
A15: pai01.0 = p0 and
A16: (pai01.1) |= g by Th14;
set x1 = pai01.1;
[pai01.0,pai01.(0+1)] in R by Def39;
then
A17: x1 in Next(p0) by A15;
x1 in SIGMA(g) by A16;
then Y1 <> {} by A17,XBOOLE_0:def 4;
then not Y1 in {{}} by TARSKI:def 1;
then
A18: Y1 in bool S \ {{}} by XBOOLE_0:def 5;
then
A19: Y1 in BOOL S by ORDERS_1:def 3;
A20: Y1 in dom Choice by A3,A18,ORDERS_1:def 3;
A21: k in NAT by ORDINAL1:def 12;
p1 = PAI(k1) by A9
.= (h|**k1).s0 by Def2
.= (h*(h|**k)).s0 by FUNCT_7:71
.= h.((h|**k).s0) by A14,FUNCT_1:13
.= h.(PAI(k)) by Def2,A21
.= h.p0 by A9
.= H(p0) by A7
.= Choice.Y1 by A20,Def3;
then p1 in Y1 by A4,A19;
then p1 in SIGMA(g) by XBOOLE_0:def 4;
then
A22: ex q1 be Element of S st q1=p1 & q1|= g;
then p1 |= EX(g) by A2;
then consider pai02 be inf_path of R such that
A23: pai02.0 = p1 and
A24: (pai02.1) |= g by Th14;
set x2 = pai02.1;
[pai02.0,pai02.(0+1)] in R by Def39;
then
A25: x2 in Next(p1) by A23;
x2 in SIGMA(g) by A24;
then x2 in Y2 by A25,XBOOLE_0:def 4;
then not Y2 in {{}} by TARSKI:def 1;
then
A26: Y2 in bool S \ {{}} by XBOOLE_0:def 5;
then
A27: Y2 in BOOL S by ORDERS_1:def 3;
A28: s0 in dom (h|**k1) by A11,FUNCT_2:def 1;
A29: Y2 in dom Choice by A3,A26,ORDERS_1:def 3;
p2 = PAI(k2) by A9
.= (h|**k2).s0 by Def2
.= (h*(h|**k1)).s0 by FUNCT_7:71
.= h.((h|**k1).s0) by A28,FUNCT_1:13
.= h.(PAI(k1)) by Def2
.= h.p1 by A9
.= H(p1) by A7
.= Choice.Y2 by A29,Def3;
then p2 in Y2 by A4,A27;
then p2 in Next(p1) by XBOOLE_0:def 4;
then ex q2 be Element of S st q2=p2 & [p1,q2] in R;
hence thesis by A22;
end;
A30: P[0]
proof
set Y = Next(s0) /\ SIGMA(g);
set y = Choice.Y;
s0 |= EX(g) by A1,A2;
then consider pai01 be inf_path of R such that
A31: pai01.0 = s0 and
A32: (pai01.1) |= g by Th14;
set x = pai01.1;
[pai01.0,pai01.(0+1)] in R by Def39;
then
A33: x in Next(s0) by A31;
x in SIGMA(g) by A32;
then Y <> {} by A33,XBOOLE_0:def 4;
then not Y in {{}} by TARSKI:def 1;
then
A34: Y in bool S \ {{}} by XBOOLE_0:def 5;
then
A35: Y in dom Choice by A3,ORDERS_1:def 3;
Y in BOOL S by A34,ORDERS_1:def 3;
then
A36: y in Y by A4;
then y in Next(s0) by XBOOLE_0:def 4;
then consider t be Element of S such that
A37: y = t and
A38: [s0,t] in R;
t in SIGMA(g) by A36,A37,XBOOLE_0:def 4;
then consider s1 be Element of S such that
A39: t = s1 and
s1 |= g;
pai.1 = PAI(1) by A9
.= (h|**1).s0 by Def2
.= h.s0 by FUNCT_7:70
.=H(s0) by A7
.=s1 by A35,A37,A39,Def3;
hence thesis by A1,A10,A38,A39;
end;
for k being Nat holds P[k] from NAT_1:sch 2(A30,A13);
hence thesis;
end;
then reconsider pai as inf_path of R by Def39;
take pai;
thus thesis by A10,A12;
end;
:: EG(f) is the maximum fixpoint of Fax(f,*)
theorem Th41:
for f,g being Assign of BASSModel(R,BASSIGN) holds (for s being
Element of S holds s|= g iff s|= Fax(f,g)) implies for s being Element of S
holds s|= g implies s|= EG(f)
proof
let f,g be Assign of BASSModel(R,BASSIGN);
assume
A1: for s being Element of S holds s|= g iff s|= Fax(f,g);
A2: for s being Element of S holds s|= g implies s|= EX g
proof
let s be Element of S;
assume s|= g;
then s|= f '&' EX(g) by A1;
hence thesis by Th13;
end;
for s0 being Element of S holds s0|= g implies s0|= EG(f)
proof
let s0 be Element of S;
assume s0|= g;
then consider pai be inf_path of R such that
A3: pai.0= s0 and
A4: for n being Nat holds pai.In(n,NAT) |= g by A2,Th40;
for n being Element of NAT holds pai.n |= f
proof
let n be Element of NAT;
pai.In(n,NAT) |= g by A4;
then pai.n |= f '&' EX(g) by A1;
hence thesis by Th13;
end;
hence thesis by A3,Th15;
end;
hence thesis;
end;
:: definition of TransEG(f)::translated function for EG(f)
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let f be Assign of BASSModel(R,BASSIGN);
func TransEG(f) -> c=-monotone Function of bool S, bool S means
:Def70:
for G being Subset of S holds it.G = SigFaxTau(f,G,R,BASSIGN);
existence
proof
deffunc F(object) = SigFaxTau(f,CastBool($1,S),R,BASSIGN);
A1: for G being object st G in bool S holds F(G) in bool S;
consider IT being Function of bool S, bool S such that
A2: for G being object st G in bool S holds IT.G= F(G) from FUNCT_2:sch 2
(A1 );
A3: for G being Subset of S holds IT.G = SigFaxTau(f,G,R,BASSIGN)
proof
let G be Subset of S;
F(G) = SigFaxTau(f,G,R,BASSIGN) by Def5;
hence thesis by A2;
end;
for G1, G2 being Subset of S st G1 c= G2 holds IT.G1 c= IT.G2
proof
let G1,G2 be Subset of S such that
A4: G1 c= G2;
A5: IT.G2 = SigFaxTau(f,G2,R,BASSIGN) by A3;
IT.G1 = SigFaxTau(f,G1,R,BASSIGN) by A3;
hence thesis by A4,A5,Th37;
end;
then reconsider IT as c=-monotone Function of bool S,bool S by
KNASTER:def 1;
take IT;
thus thesis by A3;
end;
uniqueness
proof
let F1,F2 be c=-monotone Function of bool S, bool S such that
A6: for G being Subset of S holds F1.G = SigFaxTau(f,G,R,BASSIGN) and
A7: for G being Subset of S holds F2.G = SigFaxTau(f,G,R,BASSIGN);
for G being object st G in bool S holds F1.G = F2.G
proof
let G be object;
assume G in bool S;
then reconsider G as Subset of S;
F1.G = SigFaxTau(f,G,R,BASSIGN) by A6
.= F2.G by A7;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
end;
:: fixpoint of TransEG(f)
theorem Th42:
for f,g being Assign of BASSModel(R,BASSIGN) holds (for s being
Element of S holds s|= g iff s|= Fax(f,g)) iff SIGMA(g) is_a_fixpoint_of
TransEG(f)
proof
let f,g be Assign of BASSModel(R,BASSIGN);
set G = SIGMA(g);
set Q = SIGMA(Fax(f,g));
A1: (TransEG(f)).G = SigFaxTau(f,G,R,BASSIGN) by Def70
.= Q by Th31;
A2: G is_a_fixpoint_of TransEG(f) implies for s being Element of S holds s
|= g iff s|= Fax(f,g)
proof
assume G is_a_fixpoint_of TransEG(f);
then
A3: G = Q by A1,ABIAN:def 4;
for s being Element of S holds s|= g iff s|= Fax(f,g)
proof
let s be Element of S;
thus s|= g implies s|= Fax(f,g)
proof
assume s|= g;
then s in Q by A3;
then ex t be Element of S st s=t & t|= Fax(f,g);
hence thesis;
end;
assume s|= Fax(f,g);
then s in G by A3;
then ex t be Element of S st s = t & t|= g;
hence thesis;
end;
hence thesis;
end;
(for s being Element of S holds s|= g iff s|= Fax(f,g)) implies G
is_a_fixpoint_of TransEG(f)
proof
assume
A4: for s being Element of S holds s|= g iff s|= Fax(f,g);
A5: for s be object st s in Q holds s in G
proof
let x be object;
assume x in Q;
then consider s be Element of S such that
A6: x=s and
A7: s|= Fax(f,g);
s|= g by A4,A7;
hence thesis by A6;
end;
for x be object st x in G holds x in Q
proof
let x be object;
assume x in G;
then consider s be Element of S such that
A8: x=s and
A9: s|= g;
s|= Fax(f,g) by A4,A9;
hence thesis by A8;
end;
then G = (TransEG(f)).G by A1,A5,TARSKI:2;
hence thesis by ABIAN:def 4;
end;
hence thesis by A2;
end;
theorem
for f being Assign of BASSModel(R,BASSIGN) holds SIGMA(EG(f)) = gfp(S,
TransEG(f))
proof
let f be Assign of BASSModel(R,BASSIGN);
set g = EG(f);
set h = Tau(gfp(S,TransEG(f)),R,BASSIGN);
A1: SIGMA(h) = gfp(S,TransEG(f)) by Th32;
then SIGMA(h) is_a_fixpoint_of TransEG(f) by KNASTER:5;
then
A2: for s being Element of S holds s|= h iff s|= Fax(f,h) by Th42;
A3: SIGMA(h) c= SIGMA(g)
proof
let x be object;
assume x in SIGMA(h);
then consider s be Element of S such that
A4: x=s and
A5: s|= h;
s|= g by A2,A5,Th41;
hence thesis by A4;
end;
for s being Element of S holds s|= g iff s|= Fax(f,g) by Th39;
then SIGMA(g) is_a_fixpoint_of TransEG(f) by Th42;
then SIGMA(g) c= gfp(S,TransEG(f)) by KNASTER:8;
hence thesis by A1,A3,XBOOLE_0:def 10;
end;
:: definition Foax(g,f,*):carrier ->carrier
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let f,g,h be Assign of BASSModel(R,BASSIGN);
func Foax(g,f,h) -> Assign of BASSModel(R,BASSIGN) equals
g 'or' Fax(f,h);
coherence;
end;
:: Foax(g,f,*) is monotonic.
theorem Th44:
for f,g,h1,h2 being Assign of BASSModel(R,BASSIGN) holds (for s
being Element of S holds s|= h1 implies s|= h2) implies for s being Element of
S holds s|= Foax(g,f,h1) implies s|= Foax(g,f,h2)
proof
let f,g,h1,h2 be Assign of BASSModel(R,BASSIGN);
assume
A1: for s being Element of S holds s|= h1 implies s|= h2;
let s be Element of S;
assume
A2: s|= Foax(g,f,h1);
per cases by A2,Th17;
suppose
s|= g;
hence thesis by Th17;
end;
suppose
A3: s|= Fax(f,h1);
then s|= EX(h1) by Th13;
then consider pai be inf_path of R such that
A4: pai.0 = s and
A5: (pai.1) |= h1 by Th14;
(pai.1) |= h2 by A1,A5;
then
A6: s|= EX(h2) by A4,Th14;
s|= f by A3,Th13;
then s|= f '&' EX(h2) by A6,Th13;
hence thesis by Th17;
end;
end;
::commutative
:: Foax(g,f,*)
:: Assigns ------> Assigns
:: | |
:: SIGMA | | Tau
:: v v
:: bool S -------> bool S
:: SigFoaxTau(g,f,*)
::
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let f,g be Assign of BASSModel(R,BASSIGN);
let H be Subset of S;
func SigFoaxTau(g,f,H,R,BASSIGN) -> Subset of S equals
SIGMA(Foax(g,f,Tau(H,
R,BASSIGN)));
coherence;
end;
:: SigFoaxTau(g,f,*) is monotonic.
theorem Th45:
for f,g being Assign of BASSModel(R,BASSIGN), H1,H2 being Subset
of S holds H1 c= H2 implies SigFoaxTau(g,f,H1,R,BASSIGN) c= SigFoaxTau(g,f,H2,R
,BASSIGN)
proof
let f,g be Assign of BASSModel(R,BASSIGN);
let H1,H2 be Subset of S;
assume H1 c= H2;
then
for s being Element of S holds s|= Tau(H1,R,BASSIGN) implies s|= Tau(H2,
R,BASSIGN) by Th34;
then
for s being Element of S holds s|= Foax(g,f,Tau(H1,R,BASSIGN)) implies s
|= Foax(g,f,Tau(H2,R,BASSIGN)) by Th44;
hence thesis by Th35;
end;
:: f EU g is fixpoint of Foax(g,f,*).
theorem Th46:
for f,g being Assign of BASSModel(R,BASSIGN), s being Element of
S holds s|= f EU g iff s|= Foax(g,f,f EU g)
proof
let f,g be Assign of BASSModel(R,BASSIGN);
let s be Element of S;
A1: s|= Foax(g,f,f EU g) implies s|= f EU g
proof
assume
A2: s|= Foax(g,f,f EU g);
per cases by A2,Th17;
suppose
A3: s |= g;
set m = 0;
consider pai be inf_path of R such that
A4: pai.0 = s by Th25;
for j being Element of NAT st j<m holds pai.j |= f;
hence thesis by A3,A4,Th16;
end;
suppose
A5: s |= Fax(f,f EU g);
set h = f EU g;
s |= EX h by A5,Th13;
then consider pai be inf_path of R such that
A6: pai.0 = s and
A7: (pai.1) |= h by Th14;
consider pai1 be inf_path of R such that
A8: pai1.0 = pai.1 and
A9: ex m being Element of NAT st (for j being Element of NAT st j<m
holds pai1.j |= f) & pai1.m |= g by A7,Th16;
set PAI = PathConc(pai,pai1,1);
reconsider PAI as inf_path of R by A8,Th38;
A10: PAI.0 = PathChange(pai,pai1,1,0) by Def69
.= s by A6,Def68;
consider m be Element of NAT such that
A11: for j being Element of NAT st j<m holds pai1.j |= f and
A12: pai1.m |= g by A9;
set m1 = m + 1;
A13: not m1 < 1 by NAT_1:11;
A14: s |= f by A5,Th13;
A15: for k being Element of NAT st k<m1 holds PAI.k |= f
proof
let k be Element of NAT such that
A16: k < m1;
per cases;
suppose
k < 1;
hence thesis by A14,A10,NAT_1:14;
end;
suppose
A17: not k < 1;
set k0 = k-1;
reconsider k0 as Element of NAT by A17,NAT_1:21;
(k-1) +1 <= m by A16,INT_1:7;
then
A18: k0 < m by NAT_1:13;
PAI.k = PathChange(pai,pai1,1,k) by Def69
.= pai1.k0 by A17,Def68;
hence thesis by A11,A18;
end;
end;
PAI.m1 = PathChange(pai,pai1,1,m1) by Def69
.= pai1.(m1-1) by A13,Def68
.= pai1.m;
hence thesis by A12,A10,A15,Th16;
end;
end;
s|= f EU g implies s|= Foax(g,f,f EU g)
proof
assume s|= f EU g;
then consider pai be inf_path of R such that
A19: pai.0 = s and
A20: ex m being Element of NAT st (for j being Element of NAT st j<m
holds pai.j |= f) & pai.m |= g by Th16;
consider m be Element of NAT such that
A21: for j being Element of NAT st j<m holds pai.j |= f and
A22: pai.m |= g by A20;
per cases;
suppose
m = 0;
hence thesis by A19,A22,Th17;
end;
suppose
A23: m >0;
set k = m-1;
reconsider k as Element of NAT by A23,NAT_1:20;
set h = f EU g;
set pai1 = PathShift(pai,1);
A24: pai1.k = pai.(k+1) by Def67
.= pai.m;
A25: for j being Element of NAT st j<k holds pai1.j |= f
proof
let j be Element of NAT;
assume j<k;
then j +1 <= k by INT_1:7;
then j+1 < k+1 by NAT_1:13;
then pai.(j+1) |= f by A21;
hence thesis by Def67;
end;
pai1.0 = pai.(0+1) by Def67
.= pai.1;
then pai.1 |= h by A22,A24,A25,Th16;
then
A26: s |= EX h by A19,Th14;
s |= f by A19,A21,A23;
then s |= Fax(f,h) by A26,Th13;
hence thesis by Th17;
end;
end;
hence thesis by A1;
end;
:: f EU g is the minimum fixpoint of Foax(g,f,*)
theorem Th47:
for f,g,h being Assign of BASSModel(R,BASSIGN) holds (for s being
Element of S holds s|= h iff s|= Foax(g,f,h)) implies for s being Element of S
holds s|= f EU g implies s|= h
proof
let f,g,h be Assign of BASSModel(R,BASSIGN);
assume
A1: for s being Element of S holds s|= h iff s|= Foax(g,f,h);
let s0 be Element of S;
assume s0|= f EU g;
then consider pai being inf_path of R such that
A2: pai.0 = s0 and
A3: ex m being Element of NAT st (for j being Element of NAT st j<m
holds pai.j |= f) & pai.m |= g by Th16;
consider m be Element of NAT such that
A4: for j being Element of NAT st j<m holds pai.j |= f and
A5: pai.m |= g by A3;
for j being Element of NAT holds j<= m implies pai.k_nat(m-j) |= h
proof
defpred P[Nat] means $1 <= m implies pai.k_nat(m-$1) |= h;
A6: for j being Nat st P[j] holds P[j+1]
proof
let j be Nat such that
A7: P[j];
set j1 = j+1;
j1 <= m implies pai.k_nat(m-j1) |= h
proof
set k =m-j1;
assume
A8: j1 <=m;
then reconsider k as Element of NAT by NAT_1:21;
set pai1 = PathShift(pai,k);
A9: pai1.0 = pai.(k+0) by Def67
.= pai.k;
k<= k+j by NAT_1:12;
then k < (k+j) +1 by NAT_1:13;
then
A10: pai.k |= f by A4;
A11: pai1.1 = pai.(k+1) by Def67;
pai.(k+1) |= h by A7,A8,Def2,NAT_1:13;
then pai.k |= EX(h) by A9,A11,Th14;
then pai.k |= Fax(f,h) by A10,Th13;
then
A12: pai.k |= Foax(g,f,h) by Th17;
k_nat(k) = k by Def2;
hence thesis by A1,A12;
end;
hence thesis;
end;
A13: P[0]
proof
assume 0 <= m;
A14: k_nat(m-0) = m by Def2;
pai.m |= Foax(g,f,h) by A5,Th17;
hence thesis by A1,A14;
end;
for j being Nat holds P[j] from NAT_1:sch 2(A13,A6);
hence thesis;
end;
then pai.k_nat(m-m) |= h;
hence thesis by A2,Def2;
end;
:: definition of TransEU(f,g)::translated function for f EU g
definition
let S be non empty set;
let R be total Relation of S,S;
let BASSIGN be non empty Subset of ModelSP(S);
let f,g be Assign of BASSModel(R,BASSIGN);
func TransEU(f,g) -> c=-monotone Function of bool S, bool S means
:Def73:
for H being Subset of S holds it.H = SigFoaxTau(g,f,H,R,BASSIGN);
existence
proof
deffunc F(object) = SigFoaxTau(g,f,CastBool($1,S),R,BASSIGN);
A1: for H being object st H in bool S holds F(H) in bool S;
consider IT being Function of bool S, bool S such that
A2: for H being object st H in bool S holds IT.H= F(H) from FUNCT_2:sch 2
(A1 );
A3: for H being Subset of S holds IT.H = SigFoaxTau(g,f,H,R,BASSIGN)
proof
let H be Subset of S;
CastBool(H,S) = H by Def5;
hence thesis by A2;
end;
for H1, H2 being Subset of S st H1 c= H2 holds IT.H1 c= IT.H2
proof
let H1,H2 be Subset of S such that
A4: H1 c= H2;
A5: IT.H2 = SigFoaxTau(g,f,H2,R,BASSIGN) by A3;
IT.H1 = SigFoaxTau(g,f,H1,R,BASSIGN) by A3;
hence thesis by A4,A5,Th45;
end;
then reconsider IT as c=-monotone Function of bool S,bool S by
KNASTER:def 1;
take IT;
thus thesis by A3;
end;
uniqueness
proof
let F1,F2 be c=-monotone Function of bool S, bool S such that
A6: for H being Subset of S holds F1.H = SigFoaxTau(g,f,H,R,BASSIGN) and
A7: for H being Subset of S holds F2.H = SigFoaxTau(g,f,H,R,BASSIGN);
for H being object st H in bool S holds F1.H = F2.H
proof
let H be object;
assume H in bool S;
then reconsider H as Subset of S;
F1.H = SigFoaxTau(g,f,H,R,BASSIGN) by A6
.= F2.H by A7;
hence thesis;
end;
hence thesis by FUNCT_2:12;
end;
end;
:: fixpoint of TransEU(f,g)
theorem Th48:
for f,g,h being Assign of BASSModel(R,BASSIGN) holds (for s being
Element of S holds s|= h iff s|= Foax(g,f,h)) iff SIGMA(h) is_a_fixpoint_of
TransEU(f,g)
proof
let f,g,h be Assign of BASSModel(R,BASSIGN);
set H = SIGMA(h);
set Q = SIGMA(Foax(g,f,h));
A1: (TransEU(f,g)).H = SigFoaxTau(g,f,H,R,BASSIGN) by Def73
.= Q by Th31;
A2: H is_a_fixpoint_of TransEU(f,g) implies for s being Element of S holds
s|= h iff s|= Foax(g,f,h)
proof
assume H is_a_fixpoint_of TransEU(f,g);
then
A3: H = Q by A1,ABIAN:def 4;
for s being Element of S holds s|= h iff s|= Foax(g,f,h)
proof
let s be Element of S;
thus s|= h implies s|= Foax(g,f,h)
proof
assume s|= h;
then s in H;
then ex t be Element of S st s=t & t|= Foax(g,f,h) by A3;
hence thesis;
end;
assume s|= Foax(g,f,h);
then s in Q;
then ex t be Element of S st s =t & t|= h by A3;
hence thesis;
end;
hence thesis;
end;
(for s being Element of S holds s|= h iff s|= Foax(g,f,h)) implies H
is_a_fixpoint_of TransEU(f,g)
proof
assume
A4: for s being Element of S holds s|= h iff s|= Foax(g,f,h);
A5: for s be object st s in Q holds s in H
proof
let x be object;
assume x in Q;
then consider s be Element of S such that
A6: x=s and
A7: s|= Foax(g,f,h);
s|= h by A4,A7;
hence thesis by A6;
end;
for x be object st x in H holds x in Q
proof
let x be object;
assume x in H;
then consider s be Element of S such that
A8: x=s and
A9: s|= h;
s|= Foax(g,f,h) by A4,A9;
hence thesis by A8;
end;
then H = Q by A5,TARSKI:2;
hence thesis by A1,ABIAN:def 4;
end;
hence thesis by A2;
end;
theorem
for f,g being Assign of BASSModel(R,BASSIGN) holds SIGMA(f EU g) = lfp(
S,TransEU(f,g))
proof
let f,g be Assign of BASSModel(R,BASSIGN);
set h = f EU g;
set p = Tau(lfp(S,TransEU(f,g)),R,BASSIGN);
A1: SIGMA(p) = lfp(S,TransEU(f,g)) by Th32;
lfp(S,TransEU(f,g)) is_a_fixpoint_of TransEU(f,g) by KNASTER:4;
then
A2: for s being Element of S holds s|= p iff s|= Foax(g,f,p) by A1,Th48;
A3: SIGMA(h) c= SIGMA(p)
proof
let x be object;
assume x in SIGMA(h);
then consider s be Element of S such that
A4: x=s and
A5: s|= h;
s|= p by A2,A5,Th47;
hence thesis by A4;
end;
for s being Element of S holds s|= h iff s|= Foax(g,f,h) by Th46;
then SIGMA(h) is_a_fixpoint_of TransEU(f,g) by Th48;
then lfp(S,TransEU(f,g)) c= SIGMA(h) by KNASTER:8;
hence thesis by A1,A3,XBOOLE_0:def 10;
end;
:: Solver for EX and TransEG,TransEU
theorem Th50:
for f being Assign of BASSModel(R,BASSIGN) holds SIGMA(EX(f)) =
Pred(SIGMA(f),R)
proof
let f be Assign of BASSModel(R,BASSIGN);
set g = EX(f);
set H = SIGMA(f);
A1: for x being object holds x in Pred(H,R) implies x in SIGMA(g)
proof
let x be object;
assume x in Pred(H,R);
then consider s be Element of S such that
A2: x = s and
A3: ex s1 being Element of S st s1 in H & [s,s1] in R;
consider s1 be Element of S such that
A4: s1 in H and
A5: [s,s1] in R by A3;
ex s2 be Element of S st s1 = s2 & s2 |= f by A4;
then s |= g by A5,Th28;
hence thesis by A2;
end;
for x being object holds x in SIGMA(g) implies x in Pred(H,R)
proof
let x be object;
assume x in SIGMA(g);
then consider s be Element of S such that
A6: x=s and
A7: s|= g;
consider s1 being Element of S such that
A8: [s,s1] in R and
A9: s1 |= f by A7,Th28;
s1 in H by A9;
hence thesis by A6,A8;
end;
hence thesis by A1,TARSKI:2;
end;
theorem
for f being Assign of BASSModel(R,BASSIGN), X being Subset of S holds (
TransEG(f)).X = SIGMA(f) /\ Pred(X,R)
proof
let f be Assign of BASSModel(R,BASSIGN);
let X be Subset of S;
set g = Tau(X,R,BASSIGN);
(TransEG(f)).X = SigFaxTau(f,X,R,BASSIGN) by Def70
.= SIGMA(f) /\ SIGMA(EX(g)) by Th33
.= SIGMA(f) /\ Pred(SIGMA(g),R) by Th50;
hence thesis by Th32;
end;
theorem
for f,g being Assign of BASSModel(R,BASSIGN), X being Subset of S holds
(TransEU(f,g)).X = SIGMA(g) \/ (SIGMA(f) /\ Pred(X,R))
proof
let f,g be Assign of BASSModel(R,BASSIGN);
let X be Subset of S;
set h = Tau(X,R,BASSIGN);
(TransEU(f,g)).X = SigFoaxTau(g,f,X,R,BASSIGN) by Def73
.= SIGMA(g) \/ SIGMA(Fax(f,h)) by Th33
.= SIGMA(g) \/ (SIGMA(f) /\ SIGMA(EX(h))) by Th33
.= SIGMA(g) \/ (SIGMA(f) /\ Pred(SIGMA(h),R)) by Th50;
hence thesis by Th32;
end;