modelc_1.miz
begin
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;
let a be
Element of S;
::
MODELC_1:def1
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;
::
MODELC_1:def2
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;
::
MODELC_1:def3
func
UnivF (x,f,a) ->
set equals
:
Def3: (f
. x) if x
in (
dom f)
otherwise a;
correctness ;
end
definition
let a be
set;
::
MODELC_1:def4
func
Castboolean (a) ->
boolean
object equals
:
Def4: a if a is
boolean
otherwise
FALSE ;
correctness ;
end
definition
let X be
set, a be
object;
::
MODELC_1:def5
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 ;
definition
let n;
::
MODELC_1:def6
func
atom. n ->
FinSequence of
NAT equals
<*(5
+ n)*>;
coherence ;
end
definition
let p;
::
MODELC_1:def7
func
'not' p ->
FinSequence of
NAT equals (
<*
0 *>
^ p);
coherence ;
let q;
::
MODELC_1:def8
func p
'&' q ->
FinSequence of
NAT equals ((
<*1*>
^ p)
^ q);
coherence ;
end
definition
let p;
::
MODELC_1:def9
func
EX p ->
FinSequence of
NAT equals (
<*2*>
^ p);
coherence ;
::
MODELC_1:def10
func
EG p ->
FinSequence of
NAT equals (
<*3*>
^ p);
coherence ;
let q;
::
MODELC_1:def11
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;
definition
::
MODELC_1:def12
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 be
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 ;
::
MODELC_1:def13
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 ::
MODELC_1:1
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;
::
MODELC_1:def14
attr H is
atomic means ex n st H
= (
atom. n);
::
MODELC_1:def15
attr H is
negative means ex H1 st H
= (
'not' H1);
::
MODELC_1:def16
attr H is
conjunctive means ex F, G st H
= (F
'&' G);
::
MODELC_1:def17
attr H is
ExistNext means ex H1 st H
= (
EX H1);
::
MODELC_1:def18
attr H is
ExistGlobal means ex H1 st H
= (
EG H1);
::
MODELC_1:def19
attr H is
ExistUntill means ex F, G st H
= (F
EU G);
end
definition
let F, G;
::
MODELC_1:def20
func F
'or' G ->
CTL-formula equals (
'not' ((
'not' F)
'&' (
'not' G)));
coherence ;
end
theorem ::
MODELC_1:2
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 be
Nat st (for k be
Nat st k
< n holds for H, F, sq st (
len H)
= k & H
= (F
^ sq) holds H
= F) holds 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 holds 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,
FINSEQ_1: 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,
FINSEQ_1: 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 be
Nat st for n be
Nat st n
< k holds
P[n] holds
P[k];
A72: for n be
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;
::
MODELC_1:def21
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;
::
MODELC_1:def22
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 ;
::
MODELC_1:def23
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;
::
MODELC_1:def24
func
CastCTLformula (x) ->
CTL-formula equals
:
Def24: x if x
in
CTL_WFF
otherwise (
atom.
0 );
correctness by
Th1;
end
definition
let Prop be
set;
struct (
RelStr)
KripkeStr over Prop
(# the
carrier ->
set,
the
Starts ->
Subset of the carrier,
the
InternalRel ->
Relation of the carrier, the carrier,
the
Label ->
Function of the carrier, (
bool Prop) #)
attr strict
strict;
end
definition
struct (
ComplULattStr)
CTLModelStr
(# the
carrier ->
set,
the
BasicAssign ->
Subset of the carrier,
the
L_meet ->
BinOp of the carrier,
the
Compl ->
UnOp of the carrier,
the
EneXt ->
UnOp of the carrier,
the
EGlobal ->
UnOp of the carrier,
the
EUntill ->
BinOp of the carrier #)
attr strict
strict;
end
definition
let V be
CTLModelStr;
mode
Assign of V is
Element of the
carrier of V;
end
definition
::
MODELC_1:def25
func
atomic_WFF ->
Subset of
CTL_WFF equals { x where x be
CTL-formula : x is
atomic };
correctness
proof
set X = { x where x be
CTL-formula : x is
atomic };
X
c=
CTL_WFF
proof
let y be
object;
assume y
in X;
then ex x be
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;
::
MODELC_1:def26
pred f
is-Evaluation-for Kai means for H be
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;
::
MODELC_1:def27
pred f
is-PreEvaluation-for n,Kai means
:
Def27: for H be
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;
::
MODELC_1:def28
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;
::
MODELC_1:def29
attr C is
with_basic means
:
Def29: the
BasicAssign of C is non
empty;
end
definition
::
MODELC_1:def30
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 be
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 be
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 be
Nat holds f1
is-PreEvaluation-for (n,Kai) & f2
is-PreEvaluation-for (n,Kai) implies for H be
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 be
CTL-formula st (
len H)
<= $1 holds (f1
. H)
= (f2
. H));
A1: for k be
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 be
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 be
Function of
CTL_WFF , the
carrier of V st f
is-PreEvaluation-for ($1,Kai);
A1: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat;
assume
P[k];
then
consider h be
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 be
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 be
object st H
in
CTL_WFF holds (f
. H)
=
F(H) from
FUNCT_2:sch 2(
A3);
take f;
A18: for H be
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 be
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 be
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 ;
::
MODELC_1:def31
func
EvalSet (V,Kai,n) -> non
empty
set equals { h where h be
Function of
CTL_WFF , the
carrier of V : h
is-PreEvaluation-for (n,Kai) };
correctness
proof
set X = { h where h be
Function of
CTL_WFF , the
carrier of V : h
is-PreEvaluation-for (n,Kai) };
consider h be
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;
::
MODELC_1:def32
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;
::
MODELC_1:def33
func
EvalFamily (V,Kai) -> non
empty
set means
:
Def33: for p be
set holds p
in it iff p
in (
bool (
Funcs (
CTL_WFF ,the
carrier of V))) & ex n be
Element of
NAT st p
= (
EvalSet (V,Kai,n));
existence
proof
defpred
Q[
set] means ex n be
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 be
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 be
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 be
Element of
NAT st $1
= (
EvalSet (V,Kai,n));
for X1,X2 be
set st (for x be
set holds x
in X1 iff
P[x]) & (for x be
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 be
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 ::
MODELC_1:3
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 be
set st X
in M holds X
<>
{}
proof
let X be
set;
assume X
in M;
then ex n be
Element of
NAT st X
= (
EvalSet (V,Kai,n)) by
Def33;
hence thesis;
end;
then
consider Choice be
Function such that (
dom Choice)
= M and
A1: for X be
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 be
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 be
Function of
CTL_WFF , the
carrier of V st Y
= h & h
is-PreEvaluation-for (n,Kai);
hence thesis;
end;
A5: for n be
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 be
sequence of (
Funcs (
CTL_WFF ,the
carrier of V)) such that
A6: for n be
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 be
object st H
in
CTL_WFF holds
G(H)
in the
carrier of V by
FUNCT_2: 5;
consider f be
Function of
CTL_WFF , the
carrier of V such that
A8: for H be
object st H
in
CTL_WFF holds (f
. H)
=
G(H) from
FUNCT_2:sch 2(
A7);
take f;
for n be
Element of
NAT holds f
is-PreEvaluation-for (n,Kai)
proof
defpred
P[
Nat] means f
is-PreEvaluation-for ($1,Kai);
A9: for k be
Nat st
P[k] holds
P[(k
+ 1)]
proof
let k be
Nat such that
A10:
P[k];
for H be
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);
A13: H
in
CTL_WFF by
Th1;
then (f1
. (
len (
CastCTLformula H)))
= (f1
. (
len H)) by
Def24
.=
F(len) by
A6;
then
A14: (
CastEval (V,(f1
. (
len (
CastCTLformula H))),v0))
=
F(len) 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 be
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 be
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 be
Nat holds
P[n] from
NAT_1:sch 2(
A35,
A9);
hence thesis;
end;
hence thesis by
Lm28;
end;
theorem ::
MODELC_1:4
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 be
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;
::
MODELC_1:def34
func
Evaluate (H,Kai) ->
Assign of V means
:
Def34: ex f be
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;
::
MODELC_1:def35
func
EX (f) ->
Assign of V equals (the
EneXt of V
. f);
correctness ;
::
MODELC_1:def36
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;
::
MODELC_1:def37
func f
EU g ->
Assign of V equals (the
EUntill of V
. (f,g));
correctness ;
::
MODELC_1:def38
func f
'or' g ->
Assign of V equals (
'not' ((
'not' f)
'&' (
'not' g)));
correctness ;
end
theorem ::
MODELC_1:5
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 ::
MODELC_1:6
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 ::
MODELC_1:7
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 ::
MODELC_1:8
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 ::
MODELC_1:9
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 ::
MODELC_1:10
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;
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;
:: original:
|**
redefine
func f
|** n ->
Function of S, S ;
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
Lm30: for S be
set, R be
Relation of S, S holds R is
total implies for x be
set st x
in S holds ex y be
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 be
set st x
in S holds ex y be
set st y
in S &
[x, y]
in R
proof
assume
A1: R is
total;
for x be
set st x
in S holds ex y be
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 be
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 be
set, R be
Relation of S, S holds (for x be
set st x
in S holds ex y be
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 be
set st x
in S holds ex y be
set st y
in S &
[x, y]
in R) implies R is
total
proof
assume
A1: for x be
set st x
in S holds ex y be
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 be
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;
Lm32: (R
.:
{s}) is non
empty
proof
A1: s
in
{s} by
TARSKI:def 1;
ex p be
set st p
in S &
[s, p]
in R by
Lm30;
hence thesis by
A1,
RELAT_1:def 13;
end;
scheme ::
MODELC_1:sch1
ExistPath { S() -> non
empty
set , R() ->
total
Relation of S(), S() , s0() ->
Element of S() , F(
Element of S()) ->
set } :
ex f be
sequence of S() st (f
.
0 )
= s0() & for n be
Element of
NAT holds
[(f
. n), (f
. (n
+ 1))]
in R() & (f
. (n
+ 1))
in F(.)
provided
A1: for s be
Element of S() holds ((
Im (R(),s))
/\ F(s)) is non
empty
Subset of S();
for p be
set st p
in (
BOOL S()) holds p
<>
{} by
ORDERS_1: 1;
then
consider Choice be
Function such that (
dom Choice)
= (
BOOL S()) and
A2: for p be
set st p
in (
BOOL S()) holds (Choice
. p)
in p by
FUNCT_1: 111;
A3: s0()
in S();
ex g be
sequence of S() st (g
.
0 )
= s0() & for n be
Element of
NAT holds (g
. (n
+ 1))
= (Choice
. ((R()
.:
{(g
. n)})
/\ F(.)))
proof
deffunc
G(
object) = (Choice
. ((R()
.:
{(
k_id ($1,S(),s0()))})
/\ F(k_id)));
A4: for x be
object st x
in S() holds
G(x)
in S()
proof
let x be
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 be
Function of S(), S() such that
A9: for x be
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 be
object st m
in
NAT holds
H(m)
in S();
consider g be
sequence of S() such that
A11: for m be
object st m
in
NAT holds (g
. m)
=
H(m) from
FUNCT_2:sch 2(
A10);
A12: for n be
Element of
NAT holds (g
. (n
+ 1))
= (Choice
. ((R()
.:
{(g
. n)})
/\ F(.)))
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(+) 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(.))) 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 be
sequence of S() such that
A15: (g
.
0 )
= s0() and
A16: for n be
Element of
NAT holds (g
. (n
+ 1))
= (Choice
. ((R()
.:
{(g
. n)})
/\ F(.)));
take g;
A17: for n be
Element of
NAT holds (g
. (n
+ 1))
in ((R()
.:
{(g
. n)})
/\ F(.))
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 be
Element of
NAT holds
[(g
. n), (g
. (n
+ 1))]
in R() & (g
. (n
+ 1))
in F(.)
proof
let n be
Element of
NAT ;
A18: (g
. (n
+ 1))
in ((
Im (R(),(g
. n)))
/\ F(.)) 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 be
sequence of S st (f
.
0 )
= s0 & for n be
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,
XBOOLE_1: 28;
hence thesis by
A3,
A2,
Lm32,
XBOOLE_1: 1;
end;
consider f be
sequence of S such that
A4: (f
.
0 )
= s0 & for n holds
[(f
. n), (f
. (n
+ 1))]
in R & (f
. (n
+ 1))
in
F(.) 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
let S be non
empty
set;
let R be
total
Relation of S, S;
::
MODELC_1:def39
mode
inf_path of R ->
sequence of S means
:
Def39: for n be
Nat holds
[(it
. n), (it
. (n
+ 1))]
in R;
existence
proof
set b = the
Element of S;
consider IT be
sequence of S such that (IT
.
0 )
= b and
A1: for n be
Nat holds
[(IT
. n), (IT
. (n
+ 1))]
in R by
Lm33;
take IT;
thus thesis by
A1;
end;
end
definition
let S be non
empty
set;
::
MODELC_1:def40
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
let S be non
empty
set;
let f be
object;
::
MODELC_1:def41
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 be
set holds ((
Fid (f,S))
. s)
<>
TRUE implies ((
Fid (f,S))
. s)
=
FALSE by
TARSKI:def 2;
scheme ::
MODELC_1:sch2
Func1EX { S() -> non
empty
set , f() ->
Function of S(),
BOOLEAN , F(
object,
Function of S(),
BOOLEAN ) ->
boolean
object } :
ex g be
set st g
in (
ModelSP S()) & for s be
set st s
in S() holds F(s,f)
=
TRUE iff ((
Fid (g,S()))
. s)
=
TRUE ;
deffunc
G(
object) = F($1,f);
A1: for s be
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 be
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 ::
MODELC_1:sch3
Func1Unique { S() -> non
empty
set , f() ->
Function of S(),
BOOLEAN , F(
object,
Function of S(),
BOOLEAN ) ->
boolean
object } :
for g1,g2 be
set st g1
in (
ModelSP S()) & (for s be
set st s
in S() holds F(s,f)
=
TRUE iff ((
Fid (g1,S()))
. s)
=
TRUE ) & g2
in (
ModelSP S()) & (for s be
set st s
in S() holds F(s,f)
=
TRUE iff ((
Fid (g2,S()))
. s)
=
TRUE ) holds g1
= g2;
let g1,g2 be
set such that
A1: g1
in (
ModelSP S()) and
A2: for s be
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 be
set st s
in S() holds F(s,f)
=
TRUE iff ((
Fid (g2,S()))
. s)
=
TRUE ;
A5: for s be
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;
scheme ::
MODELC_1:sch4
UnOpEX { M() -> non
empty
set , F(
object) ->
Element of M() } :
ex o be
UnOp of M() st for f be
object st f
in M() holds (o
. f)
= F(f);
A1: for f be
object st f
in M() holds F(f)
in M();
ex o be
Function of M(), M() st for f be
object st f
in M() holds (o
. f)
= F(f) from
FUNCT_2:sch 2(
A1);
hence thesis;
end;
scheme ::
MODELC_1:sch5
UnOpUnique { S,M() -> non
empty
set , F(
object) ->
Element of M() } :
for o1,o2 be
UnOp of M() st (for f be
object st f
in M() holds (o1
. f)
= F(f)) & (for f be
object st f
in M() holds (o2
. f)
= F(f)) holds o1
= o2;
let o1,o2 be
UnOp of M() such that
A1: for f be
object st f
in M() holds (o1
. f)
= F(f) and
A2: for f be
object st f
in M() holds (o2
. f)
= F(f);
for f be
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;
scheme ::
MODELC_1:sch6
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 be
set st h
in (
ModelSP S()) & for s be
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 be
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 be
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 ::
MODELC_1:sch7
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 be
set st h1
in (
ModelSP S()) & (for s be
set st s
in S() holds F(s,f,g)
=
TRUE iff ((
Fid (h1,S()))
. s)
=
TRUE ) & h2
in (
ModelSP S()) & (for s be
set st s
in S() holds F(s,f,g)
=
TRUE iff ((
Fid (h2,S()))
. s)
=
TRUE ) holds h1
= h2;
let h1,h2 be
set such that
A1: h1
in (
ModelSP S()) and
A2: for s be
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 be
set st s
in S() holds F(s,f,g)
=
TRUE iff ((
Fid (h2,S()))
. s)
=
TRUE ;
A5: for s be
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
let S be non
empty
set;
let f be
object;
::
MODELC_1:def42
func
Not_0 (f,S) ->
Element of (
ModelSP S) means
:
Def42: for s be
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 be
set such that
A1: IT
in (
ModelSP S) and
A2: for s be
set st s
in S holds
F(s,Fid)
=
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 be
set st g1
in (
ModelSP S) & (for s be
set st s
in S holds
F(s,Fid)
=
TRUE iff ((
Fid (g1,S))
. s)
=
TRUE ) & g2
in (
ModelSP S) & (for s be
set st s
in S holds
F(s,Fid)
=
TRUE iff ((
Fid (g2,S))
. s)
=
TRUE ) holds g1
= g2 from
Func1Unique;
hence thesis;
end;
end
Lm35: for o1,o2 be
UnOp of (
ModelSP S) st (for f be
object st f
in (
ModelSP S) holds (o1
. f)
= (
Not_0 (f,S))) & (for f be
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 be
UnOp of M st (for f be
object st f
in M holds (o1
. f)
=
F(f)) & (for f be
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;
::
MODELC_1:def43
func
Not_ (S) ->
UnOp of (
ModelSP S) means
:
Def43: for f be
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 be
UnOp of M st for f be
object st f
in M holds (o
. f)
=
F(f) from
UnOpEX;
hence thesis;
end;
uniqueness by
Lm35;
end
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;
::
MODELC_1:def44
func
EneXt_univ (x,f,R) ->
Element of
BOOLEAN equals
:
Def44:
TRUE if x
in S & ex pai be
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;
::
MODELC_1:def45
func
EneXt_0 (f,R) ->
Element of (
ModelSP S) means
:
Def45: for s be
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 be
set such that
A1: IT
in (
ModelSP S) and
A2: for s be
set st s
in S holds
F(s,Fid)
=
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 be
set st g1
in (
ModelSP S) & (for s be
set st s
in S holds
F(s,Fid)
=
TRUE iff ((
Fid (g1,S))
. s)
=
TRUE ) & g2
in (
ModelSP S) & (for s be
set st s
in S holds
F(s,Fid)
=
TRUE iff ((
Fid (g2,S))
. s)
=
TRUE ) holds g1
= g2 from
Func1Unique;
hence thesis;
end;
end
Lm36: for o1,o2 be
UnOp of (
ModelSP S) st (for f be
object st f
in (
ModelSP S) holds (o1
. f)
= (
EneXt_0 (f,R))) & (for f be
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 be
UnOp of M st (for f be
object st f
in M holds (o1
. f)
=
F(f)) & (for f be
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;
::
MODELC_1:def46
func
EneXt_ (R) ->
UnOp of (
ModelSP S) means
:
Def46: for f be
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 be
UnOp of M st for f be
object st f
in M holds (o
. f)
=
F(f) from
UnOpEX;
hence thesis;
end;
uniqueness by
Lm36;
end
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;
::
MODELC_1:def47
func
EGlobal_univ (x,f,R) ->
Element of
BOOLEAN equals
:
Def47:
TRUE if x
in S & ex pai be
inf_path of R st ((pai
.
0 )
= x & for n be
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;
::
MODELC_1:def48
func
EGlobal_0 (f,R) ->
Element of (
ModelSP S) means
:
Def48: for s be
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 be
set such that
A1: IT
in (
ModelSP S) and
A2: for s be
set st s
in S holds
F(s,Fid)
=
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 be
set st g1
in (
ModelSP S) & (for s be
set st s
in S holds
F(s,Fid)
=
TRUE iff ((
Fid (g1,S))
. s)
=
TRUE ) & g2
in (
ModelSP S) & (for s be
set st s
in S holds
F(s,Fid)
=
TRUE iff ((
Fid (g2,S))
. s)
=
TRUE ) holds g1
= g2 from
Func1Unique;
hence thesis;
end;
end
Lm37: for o1,o2 be
UnOp of (
ModelSP S) st (for f be
object st f
in (
ModelSP S) holds (o1
. f)
= (
EGlobal_0 (f,R))) & (for f be
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 be
UnOp of M st (for f be
object st f
in M holds (o1
. f)
=
F(f)) & (for f be
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;
::
MODELC_1:def49
func
EGlobal_ (R) ->
UnOp of (
ModelSP S) means
:
Def49: for f be
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 be
UnOp of M st for f be
object st f
in M holds (o
. f)
=
F(f) from
UnOpEX;
hence thesis;
end;
uniqueness by
Lm37;
end
definition
let S be non
empty
set;
let f,g be
set;
::
MODELC_1:def50
func
And_0 (f,g,S) ->
Element of (
ModelSP S) means
:
Def50: for s be
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 be
set such that
A1: IT
in (
ModelSP S) and
A2: for s be
set st s
in S holds
F(s,Fid,Fid)
=
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 be
set st h1
in (
ModelSP S) & (for s be
set st s
in S holds
F(s,Fid,Fid)
=
TRUE iff ((
Fid (h1,S))
. s)
=
TRUE ) & h2
in (
ModelSP S) & (for s be
set st s
in S holds
F(s,Fid,Fid)
=
TRUE iff ((
Fid (h2,S))
. s)
=
TRUE ) holds h1
= h2 from
Func2Unique;
hence thesis;
end;
end
Lm38: for o1,o2 be
BinOp of (
ModelSP S) st (for f,g be
set st (f
in (
ModelSP S)) & (g
in (
ModelSP S)) holds (o1
. (f,g))
= (
And_0 (f,g,S))) & (for f,g be
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 be
BinOp of M st (for f,g be
Element of M holds (o1
. (f,g))
=
O(f,g)) & (for f,g be
Element of M holds (o2
. (f,g))
=
O(f,g)) holds o1
= o2 from
BINOP_2:sch 2;
for o1,o2 be
BinOp of M st (for f,g be
set st (f
in M) & (g
in M) holds (o1
. (f,g))
= (
And_0 (f,g,S))) & (for f,g be
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 be
set st f
in M & g
in M holds (o1
. (f,g))
= (
And_0 (f,g,S)) and
A3: for f,g be
set st f
in M & g
in M holds (o2
. (f,g))
= (
And_0 (f,g,S));
A4: for f,g be
Element of M holds (o2
. (f,g))
=
O(f,g) by
A3;
for f,g be
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;
::
MODELC_1:def51
func
And_ (S) ->
BinOp of (
ModelSP S) means
:
Def51: for f,g be
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 be
BinOp of M such that
A1: for f,g be
Element of M holds (o
. (f,g))
=
O(f,g) from
BINOP_1:sch 4;
for f,g be
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
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;
::
MODELC_1:def52
func
EUntill_univ (x,f,g,R) ->
Element of
BOOLEAN equals
:
Def52:
TRUE if x
in S & ex pai be
inf_path of R st ((pai
.
0 )
= x & ex m be
Element of
NAT st (for j be
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;
::
MODELC_1:def53
func
EUntill_0 (f,g,R) ->
Element of (
ModelSP S) means
:
Def53: for s be
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 be
set such that
A1: IT
in (
ModelSP S) and
A2: for s be
set st s
in S holds
F(s,Fid,Fid)
=
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 be
set st h1
in (
ModelSP S) & (for s be
set st s
in S holds
F(s,Fid,Fid)
=
TRUE iff ((
Fid (h1,S))
. s)
=
TRUE ) & h2
in (
ModelSP S) & (for s be
set st s
in S holds
F(s,Fid,Fid)
=
TRUE iff ((
Fid (h2,S))
. s)
=
TRUE ) holds h1
= h2 from
Func2Unique;
hence thesis;
end;
end
Lm39: for o1,o2 be
BinOp of (
ModelSP S) st (for f,g be
set st (f
in (
ModelSP S)) & (g
in (
ModelSP S)) holds (o1
. (f,g))
= (
EUntill_0 (f,g,R))) & (for f,g be
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 be
BinOp of M st (for f,g be
Element of M holds (o1
. (f,g))
=
O(f,g)) & (for f,g be
Element of M holds (o2
. (f,g))
=
O(f,g)) holds o1
= o2 from
BINOP_2:sch 2;
for o1,o2 be
BinOp of M st (for f,g be
set st f
in M & g
in M holds (o1
. (f,g))
= (
EUntill_0 (f,g,R))) & (for f,g be
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 be
set st f
in M & g
in M holds (o1
. (f,g))
= (
EUntill_0 (f,g,R)) and
A3: for f,g be
set st f
in M & g
in M holds (o2
. (f,g))
= (
EUntill_0 (f,g,R));
A4: for f,g be
Element of M holds (o2
. (f,g))
=
O(f,g) by
A3;
for f,g be
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;
::
MODELC_1:def54
func
EUntill_ (R) ->
BinOp of (
ModelSP S) means
:
Def54: for f,g be
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 be
BinOp of M such that
A1: for f,g be
Element of M holds (o
. (f,g))
=
O(f,g) from
BINOP_1:sch 4;
for f,g be
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
let S be non
empty
set;
let X be non
empty
Subset of (
ModelSP S);
let s be
object;
::
MODELC_1:def55
func
F_LABEL (s,X) ->
Subset of X means
:
Def55: for x be
object holds x
in it iff x
in X & ex f be
Function of S,
BOOLEAN st f
= x & (f
. s)
=
TRUE ;
existence
proof
defpred
P[
object] means ex f be
Function of S,
BOOLEAN st f
= $1 & (f
. s)
=
TRUE ;
consider IT be
set such that
A1: for x be
object holds x
in IT iff x
in X &
P[x] from
XBOOLE_0:sch 1;
for x be
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 be
Function of S,
BOOLEAN st f
= $1 & (f
. s)
=
TRUE ;
for X1,X2 be
set st (for x be
object holds x
in X1 iff
P[x]) & (for x be
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);
::
MODELC_1:def56
func
Label_ (X) ->
Function of S, (
bool X) means
:
Def56: for x be
object st x
in S holds (it
. x)
= (
F_LABEL (x,X));
existence
proof
deffunc
F(
object) = (
F_LABEL ($1,X));
A1: for x be
object st x
in S holds
F(x)
in (
bool X);
consider IT be
Function of S, (
bool X) such that
A2: for x be
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 be
object st x
in S holds (G
. x)
= (
F_LABEL (x,X)) and
A4: for x be
object st x
in S holds (H
. x)
= (
F_LABEL (x,X));
for x be
object st x
in S holds (G
. x)
= (H
. x)
proof
let x be
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);
::
MODELC_1:def57
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;
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);
::
MODELC_1:def58
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
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));
::
MODELC_1:def59
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 ::
MODELC_1:11
Th11: for a be
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 be
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 ::
MODELC_1:12
Th12: for f be
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 ::
MODELC_1:13
Th13: for f,g be
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 ::
MODELC_1:14
Th14: for f be
Assign of (
BASSModel (R,BASSIGN)) holds s
|= (
EX f) iff ex pai be
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 be
inf_path of R st (pai
.
0 )
= s & (pai
. 1)
|= f) implies s
|= (
EX f)
proof
assume
A3: ex pai be
inf_path of R st (pai
.
0 )
= s & (pai
. 1)
|= f;
ex pai be
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 be
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 be
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 ::
MODELC_1:15
Th15: for f be
Assign of (
BASSModel (R,BASSIGN)) holds s
|= (
EG f) iff ex pai be
inf_path of R st (pai
.
0 )
= s & for n be
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 be
inf_path of R st (pai
.
0 )
= s & for n be
Element of
NAT holds (pai
. n)
|= f) implies s
|= (
EG f)
proof
assume
A3: ex pai be
inf_path of R st (pai
.
0 )
= s & for n be
Element of
NAT holds (pai
. n)
|= f;
ex pai be
inf_path of R st (pai
.
0 )
= s & for n be
Element of
NAT holds ((
Fid (f,S))
. (pai
. n))
=
TRUE
proof
consider pai be
inf_path of R such that
A4: (pai
.
0 )
= s and
A5: for n be
Element of
NAT holds (pai
. n)
|= f by
A3;
take pai;
for n be
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 be
inf_path of R st (pai
.
0 )
= s & for n be
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 be
inf_path of R such that
A6: (pai
.
0 )
= s and
A7: for n be
Element of
NAT holds ((
Fid (f,S))
. (pai
. n))
=
TRUE by
Def47;
take pai;
for n be
Element of
NAT holds (pai
. n)
|= f by
A7;
hence thesis by
A6;
end;
hence thesis by
A2;
end;
theorem ::
MODELC_1:16
Th16: for f,g be
Assign of (
BASSModel (R,BASSIGN)) holds s
|= (f
EU g) iff ex pai be
inf_path of R st (pai
.
0 )
= s & ex m be
Element of
NAT st (for j be
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 be
inf_path of R st (pai
.
0 )
= s & ex m be
Element of
NAT st (for j be
Element of
NAT st j
< m holds (pai
. j)
|= f) & (pai
. m)
|= g) implies s
|= (f
EU g)
proof
assume
A3: ex pai be
inf_path of R st (pai
.
0 )
= s & ex m be
Element of
NAT st (for j be
Element of
NAT st j
< m holds (pai
. j)
|= f) & (pai
. m)
|= g;
ex pai be
inf_path of R st (pai
.
0 )
= s & ex m be
Element of
NAT st (for j be
Element of
NAT st j
< m holds ((
Fid (f,S))
. (pai
. j))
=
TRUE ) & ((
Fid (g,S))
. (pai
. m))
=
TRUE
proof
consider pai be
inf_path of R such that
A4: (pai
.
0 )
= s and
A5: ex m be
Element of
NAT st (for j be
Element of
NAT st j
< m holds (pai
. j)
|= f) & (pai
. m)
|= g by
A3;
take pai;
ex m be
Element of
NAT st (for j be
Element of
NAT st j
< m holds ((
Fid (f,S))
. (pai
. j))
=
TRUE ) & ((
Fid (g,S))
. (pai
. m))
=
TRUE
proof
consider m be
Element of
NAT such that
A6: for j be
Element of
NAT st j
< m holds (pai
. j)
|= f and
A7: (pai
. m)
|= g by
A5;
take m;
for j be
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 be
inf_path of R st (pai
.
0 )
= s & ex m be
Element of
NAT st (for j be
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 be
inf_path of R such that
A8: (pai
.
0 )
= s and
A9: ex m be
Element of
NAT st (for j be
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 be
Element of
NAT st (for j be
Element of
NAT st j
< m holds (pai
. j)
|= f) & (pai
. m)
|= g
proof
consider m be
Element of
NAT such that
A10: for j be
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 be
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 ::
MODELC_1:17
Th17: for f,g be
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
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 be
Function of
atomic_WFF , the
BasicAssign of (
BASSModel (R,BASSIGN));
let s be
Element of S;
let H be
CTL-formula;
::
MODELC_1:def60
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 be
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 ::
MODELC_1:18
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 ::
MODELC_1:19
(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 ::
MODELC_1:20
(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 ::
MODELC_1:21
(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 ::
MODELC_1:22
(s,kai)
|= (
EX H) iff ex pai be
inf_path of R st (pai
.
0 )
= s & ((pai
. 1),kai)
|= H
proof
A1: (ex pai be
inf_path of R st (pai
.
0 )
= s & (pai
. 1)
|= (
Evaluate (H,kai))) implies ex pai be
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 ::
MODELC_1:23
(s,kai)
|= (
EG H) iff ex pai be
inf_path of R st (pai
.
0 )
= s & for n be
Element of
NAT holds ((pai
. n),kai)
|= H
proof
A1: (ex pai be
inf_path of R st (pai
.
0 )
= s & for n be
Element of
NAT holds (pai
. n)
|= (
Evaluate (H,kai))) implies ex pai be
inf_path of R st (pai
.
0 )
= s & for n be
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 be
Element of
NAT holds (pai
. n)
|= (
Evaluate (H,kai));
take pai;
for n be
Element of
NAT holds ((pai
. n),kai)
|= H by
A3;
hence thesis by
A2;
end;
A4: (ex pai be
inf_path of R st (pai
.
0 )
= s & for n be
Element of
NAT holds ((pai
. n),kai)
|= H) implies ex pai be
inf_path of R st (pai
.
0 )
= s & for n be
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 be
Element of
NAT holds ((pai
. n),kai)
|= H;
take pai;
for n be
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 ::
MODELC_1:24
(s,kai)
|= (H1
EU H2) iff ex pai be
inf_path of R st (pai
.
0 )
= s & ex m be
Element of
NAT st (for j be
Element of
NAT st j
< m holds ((pai
. j),kai)
|= H1) & ((pai
. m),kai)
|= H2
proof
A1: (ex pai be
inf_path of R st (pai
.
0 )
= s & ex m be
Element of
NAT st (for j be
Element of
NAT st j
< m holds (pai
. j)
|= (
Evaluate (H1,kai))) & ((pai
. m)
|= (
Evaluate (H2,kai)))) implies ex pai be
inf_path of R st (pai
.
0 )
= s & ex m be
Element of
NAT st (for j be
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 be
Element of
NAT st (for j be
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 be
Element of
NAT st j
< m holds (pai
. j)
|= (
Evaluate (H1,kai)) and
A5: (pai
. m)
|= (
Evaluate (H2,kai)) by
A3;
A6: for j be
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 be
inf_path of R st (pai
.
0 )
= s & ex m be
Element of
NAT st (for j be
Element of
NAT st j
< m holds ((pai
. j),kai)
|= H1) & (((pai
. m),kai)
|= H2)) implies ex pai be
inf_path of R st (pai
.
0 )
= s & ex m be
Element of
NAT st (for j be
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 be
Element of
NAT st (for j be
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 be
Element of
NAT st j
< m holds ((pai
. j),kai)
|= H1 and
A11: ((pai
. m),kai)
|= H2 by
A9;
A12: for j be
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;
theorem ::
MODELC_1:25
Th25: for s0 holds ex pai be
inf_path of R st (pai
.
0 )
= s0
proof
let s0;
consider pai be
sequence of S such that
A1: (pai
.
0 )
= s0 and
A2: for n be
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 ::
MODELC_1:26
for R be
Relation of S, S holds R is
total iff for x be
set st x
in S holds ex y be
set st y
in S &
[x, y]
in R by
Lm30,
Lm31;
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;
::
MODELC_1:def61
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 ::
MODELC_1:27
Th27:
[s0, s1]
in R implies ex pai be
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 be
object st x
in
NAT holds
F(x)
in S;
consider pai be
sequence of S such that
A3: for n be
object st n
in
NAT holds (pai
. n)
=
F(n) from
FUNCT_2:sch 2(
A2);
assume
A4:
[s0, s1]
in R;
for n be
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() 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 ::
MODELC_1:28
Th28: for f be
Assign of (
BASSModel (R,BASSIGN)) holds s
|= (
EX f) iff ex s1 be
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 be
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 be
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
let S be non
empty
set;
let R be
total
Relation of S, S;
let H be
Subset of S;
::
MODELC_1:def62
func
Pred (H,R) ->
Subset of S equals { s where s be
Element of S : ex t be
Element of S st t
in H &
[s, t]
in R };
coherence
proof
set P = { s where s be
Element of S : ex t be
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 be
Element of S st t
in H &
[s, t]
in R;
hence thesis;
end;
hence thesis;
end;
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);
let f be
Assign of (
BASSModel (R,BASSIGN));
::
MODELC_1:def63
func
SIGMA (f) ->
Subset of S equals { s where s be
Element of S : s
|= f };
correctness
proof
set P = { s where s be
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 be
Assign of (
BASSModel (R,BASSIGN)) holds (
SIGMA f)
= { s where s be
Element of S : ((
Fid (f,S))
. s)
=
TRUE }
proof
let f be
Assign of (
BASSModel (R,BASSIGN));
A1: for x be
object holds x
in { s where s be
Element of S : ((
Fid (f,S))
. s)
=
TRUE } implies x
in (
SIGMA f)
proof
let x be
object;
assume x
in { s where s be
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 be
object holds x
in (
SIGMA f) implies x
in { s where s be
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 be non
empty
set, f,g be
Function of X,
BOOLEAN holds { x where x be
Element of X : (f
. x)
=
TRUE }
= { x where x be
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 be
Element of X : (f
. x)
=
TRUE };
set G = { x where x be
Element of X : (g
. x)
=
TRUE };
assume that
A1: F
= G;
for p be
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 be
Element of X st x1
= p & (f
. x1)
=
TRUE ;
ex x2 be
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 be
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;
theorem ::
MODELC_1:29
for f,g be
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 be
Element of S : ((
Fid (f,S))
. s)
=
TRUE } by
Lm40;
then { s where s be
Element of S : ((
Fid (f,S))
. s)
=
TRUE }
= { s where s be
Element of S : ((
Fid (g,S))
. s)
=
TRUE } by
A1,
Lm40;
hence thesis by
Lm41,
Lm42;
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);
let T be
Subset of S;
::
MODELC_1:def64
func
Tau (T,R,BASSIGN) ->
Assign of (
BASSModel (R,BASSIGN)) means
:
Def64: for s be
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 be
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 be
Function of S,
BOOLEAN such that
A3: for x be
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 be
set st s
in S holds ((
Fid (f1,S))
. s)
= ((
chi (T,S))
. s) and
A5: for s be
set st s
in S holds ((
Fid (f2,S))
. s)
= ((
chi (T,S))
. s);
for s be
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
theorem ::
MODELC_1:30
for T1,T2 be
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 be
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 be
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;
theorem ::
MODELC_1:31
Th31: for f be
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 be
Element of S : ((
Fid (f,S))
. s)
=
TRUE } by
Lm40;
for s be
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 be
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;
theorem ::
MODELC_1:32
Th32: for T be
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 be
Element of S : ((
Fid (f,S))
. s)
=
TRUE } by
Lm40;
for s be
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 be
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;
theorem ::
MODELC_1:33
Th33: for f,g be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
Element of S st x
= s & x
|= f;
reconsider s as
Element of S by
A18;
ex y be
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;
theorem ::
MODELC_1:34
Th34: for G1,G2 be
Subset of S holds G1
c= G2 implies for s be
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;
theorem ::
MODELC_1:35
Th35: for f1,f2 be
Assign of (
BASSModel (R,BASSIGN)) holds (for s be
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 be
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;
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));
::
MODELC_1:def65
func
Fax (f,g) ->
Assign of (
BASSModel (R,BASSIGN)) equals (f
'&' (
EX g));
correctness ;
end
theorem ::
MODELC_1:36
Th36: for f,g1,g2 be
Assign of (
BASSModel (R,BASSIGN)) holds (for s be
Element of S holds s
|= g1 implies s
|= g2) implies for s be
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 be
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;
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;
::
MODELC_1:def66
func
SigFaxTau (f,G,R,BASSIGN) ->
Subset of S equals (
SIGMA (
Fax (f,(
Tau (G,R,BASSIGN)))));
coherence ;
end
theorem ::
MODELC_1:37
Th37: for f be
Assign of (
BASSModel (R,BASSIGN)), G1,G2 be
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 be
Element of S holds s
|= (
Tau (G1,R,BASSIGN)) implies s
|= (
Tau (G2,R,BASSIGN)) by
Th34;
then for s be
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;
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 ;
::
MODELC_1:def67
func
PathShift (pai,k) ->
inf_path of R means
:
Def67: for n be
Element of
NAT holds (it
. n)
= (pai
. (n
+ k));
existence
proof
deffunc
PAI1(
object) = (pai
. ((
k_nat $1)
+ k));
A1: for x be
object st x
in
NAT holds
PAI1(x)
in S;
consider IT be
sequence of S such that
A2: for n be
object st n
in
NAT holds (IT
. n)
=
PAI1(n) from
FUNCT_2:sch 2(
A1);
A3: for n be
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 be
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 be
inf_path of R st (for n be
Element of
NAT holds (pai1
. n)
= (pai
. (n
+ k))) & (for n be
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 be
Element of
NAT holds (pai1
. n)
= (pai
. (n
+ k)) and
A7: for n be
Element of
NAT holds (pai2
. n)
= (pai
. (n
+ k));
for x be
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;
::
MODELC_1:def68
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;
::
MODELC_1:def69
func
PathConc (pai1,pai2,k) ->
sequence of S means
:
Def69: for n be
Nat holds (it
. n)
= (
PathChange (pai1,pai2,k,n));
existence
proof
deffunc
F1(
object) = (
PathChange (pai1,pai2,k,(
k_nat $1)));
A1: for n be
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 be
sequence of S such that
A4: for n be
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 be
Nat holds (f1
. n)
= (
PathChange (pai1,pai2,k,n)) and
A6: for n be
Nat holds (f2
. n)
= (
PathChange (pai1,pai2,k,n));
for x be
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 ::
MODELC_1:38
Th38: for pai1,pai2 be
inf_path of R, k be
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 be
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;
theorem ::
MODELC_1:39
Th39: for f be
Assign of (
BASSModel (R,BASSIGN)), s be
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 be
Element of
NAT holds (pai
. n)
|= f by
Th15;
set pai1 = (
PathShift (pai,1));
A3: for n be
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 be
inf_path of R such that
A8: (pai2
.
0 )
= (pai1
. 1) and
A9: for n be
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 be
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;
theorem ::
MODELC_1:40
Th40: for g be
Assign of (
BASSModel (R,BASSIGN)), s0 be
Element of S st s0
|= g holds (for s be
Element of S holds s
|= g implies s
|= (
EX g)) implies ex pai be
inf_path of R st (pai
.
0 )
= s0 & for n be
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 be
Element of S :
[$1, x]
in R };
assume
A2: for s be
Element of S holds s
|= g implies s
|= (
EX g);
for p be
set st p
in (
BOOL S) holds p
<>
{} by
ORDERS_1: 1;
then
consider Choice be
Function such that
A3: (
dom Choice)
= (
BOOL S) and
A4: for p be
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 be
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 be
Function of S, S such that
A7: for x be
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 be
object st n
in
NAT holds
PAI(n)
in S;
consider pai be
sequence of S such that
A9: for n be
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 be
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 be
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() 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 be
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;
theorem ::
MODELC_1:41
Th41: for f,g be
Assign of (
BASSModel (R,BASSIGN)) holds (for s be
Element of S holds s
|= g iff s
|= (
Fax (f,g))) implies for s be
Element of S holds s
|= g implies s
|= (
EG f)
proof
let f,g be
Assign of (
BASSModel (R,BASSIGN));
assume
A1: for s be
Element of S holds s
|= g iff s
|= (
Fax (f,g));
A2: for s be
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 be
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 be
Nat holds (pai
. (
In (n,
NAT )))
|= g by
A2,
Th40;
for n be
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
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));
::
MODELC_1:def70
func
TransEG (f) ->
c=-monotone
Function of (
bool S), (
bool S) means
:
Def70: for G be
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 be
object st G
in (
bool S) holds
F(G)
in (
bool S);
consider IT be
Function of (
bool S), (
bool S) such that
A2: for G be
object st G
in (
bool S) holds (IT
. G)
=
F(G) from
FUNCT_2:sch 2(
A1);
A3: for G be
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 be
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 be
Subset of S holds (F1
. G)
= (
SigFaxTau (f,G,R,BASSIGN)) and
A7: for G be
Subset of S holds (F2
. G)
= (
SigFaxTau (f,G,R,BASSIGN));
for G be
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
theorem ::
MODELC_1:42
Th42: for f,g be
Assign of (
BASSModel (R,BASSIGN)) holds (for s be
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 be
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 be
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 be
Element of S holds s
|= g iff s
|= (
Fax (f,g))) implies G
is_a_fixpoint_of (
TransEG f)
proof
assume
A4: for s be
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 ::
MODELC_1:43
for f be
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 be
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 be
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
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));
::
MODELC_1:def71
func
Foax (g,f,h) ->
Assign of (
BASSModel (R,BASSIGN)) equals (g
'or' (
Fax (f,h)));
coherence ;
end
theorem ::
MODELC_1:44
Th44: for f,g,h1,h2 be
Assign of (
BASSModel (R,BASSIGN)) holds (for s be
Element of S holds s
|= h1 implies s
|= h2) implies for s be
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 be
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;
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;
::
MODELC_1:def72
func
SigFoaxTau (g,f,H,R,BASSIGN) ->
Subset of S equals (
SIGMA (
Foax (g,f,(
Tau (H,R,BASSIGN)))));
coherence ;
end
theorem ::
MODELC_1:45
Th45: for f,g be
Assign of (
BASSModel (R,BASSIGN)), H1,H2 be
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 be
Element of S holds s
|= (
Tau (H1,R,BASSIGN)) implies s
|= (
Tau (H2,R,BASSIGN)) by
Th34;
then for s be
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;
theorem ::
MODELC_1:46
Th46: for f,g be
Assign of (
BASSModel (R,BASSIGN)), s be
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 be
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 be
Element of
NAT st (for j be
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 be
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 be
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 be
Element of
NAT st (for j be
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 be
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 be
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;
theorem ::
MODELC_1:47
Th47: for f,g,h be
Assign of (
BASSModel (R,BASSIGN)) holds (for s be
Element of S holds s
|= h iff s
|= (
Foax (g,f,h))) implies for s be
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 be
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 be
inf_path of R such that
A2: (pai
.
0 )
= s0 and
A3: ex m be
Element of
NAT st (for j be
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 be
Element of
NAT st j
< m holds (pai
. j)
|= f and
A5: (pai
. m)
|= g by
A3;
for j be
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 be
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 be
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
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));
::
MODELC_1:def73
func
TransEU (f,g) ->
c=-monotone
Function of (
bool S), (
bool S) means
:
Def73: for H be
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 be
object st H
in (
bool S) holds
F(H)
in (
bool S);
consider IT be
Function of (
bool S), (
bool S) such that
A2: for H be
object st H
in (
bool S) holds (IT
. H)
=
F(H) from
FUNCT_2:sch 2(
A1);
A3: for H be
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 be
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 be
Subset of S holds (F1
. H)
= (
SigFoaxTau (g,f,H,R,BASSIGN)) and
A7: for H be
Subset of S holds (F2
. H)
= (
SigFoaxTau (g,f,H,R,BASSIGN));
for H be
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
theorem ::
MODELC_1:48
Th48: for f,g,h be
Assign of (
BASSModel (R,BASSIGN)) holds (for s be
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 be
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 be
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 be
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 be
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 ::
MODELC_1:49
for f,g be
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 be
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 be
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;
theorem ::
MODELC_1:50
Th50: for f be
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 be
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 be
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 be
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 be
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 ::
MODELC_1:51
for f be
Assign of (
BASSModel (R,BASSIGN)), X be
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 ::
MODELC_1:52
for f,g be
Assign of (
BASSModel (R,BASSIGN)), X be
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;