Copyright (c) 1992 Association of Mizar Users
environ
vocabulary NET_1, BOOLE, RELAT_1, FF_SIEC, FUNCT_1;
notation TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, NET_1;
constructors TARSKI, NET_1, XBOOLE_0;
clusters RELAT_1, NET_1, SYSREL, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;
theorems ZFMISC_1, RELAT_1, SYSREL, TARSKI, RELSET_1, NET_1, XBOOLE_0,
XBOOLE_1;
begin :: F - Nets
reserve x,y,X,Y for set;
definition
let N be Net;
canceled;
func chaos(N) -> set equals
:Def2: Elements(N) \/ {Elements(N)};
correctness;
end;
reserve M for Pnet;
definition let X,Y;
assume A1: X misses Y;
canceled;
func PTempty_f_net(X,Y) -> strict Pnet equals
:Def4: Net (# X, Y, {} #);
correctness
proof
set M = Net (# X, Y, {} #);
(the Places of M) misses (the Transitions of M) &
(the Flow of M) c= [:the Places of M, the Transitions of M:] \/
[:the Transitions of M, the Places of M:] by A1,XBOOLE_1:2;
hence thesis by NET_1:def 1;
end;
end;
definition let X;
func Tempty_f_net(X) -> strict Pnet equals
:Def5: PTempty_f_net(X,{});
correctness;
func Pempty_f_net(X) -> strict Pnet equals
:Def6: PTempty_f_net({},X);
correctness;
end;
definition let x;
func Tsingle_f_net(x) -> strict Pnet equals
:Def7: PTempty_f_net({},{x});
correctness;
func Psingle_f_net(x) -> strict Pnet equals
:Def8: PTempty_f_net({x},{});
correctness;
end;
definition
func empty_f_net -> strict Pnet equals
:Def9: PTempty_f_net({},{});
correctness;
end;
canceled;
theorem
X misses Y implies the Places of PTempty_f_net(X,Y) = X &
the Transitions of PTempty_f_net(X,Y) = Y &
the Flow of PTempty_f_net(X,Y) = {}
proof
assume X misses Y;
then PTempty_f_net(X,Y) = Net (# X, Y, {} #) by Def4;
hence thesis;
end;
theorem
the Places of Tempty_f_net(X) = X &
the Transitions of Tempty_f_net(X) = {} &
the Flow of Tempty_f_net(X) = {}
proof
A1:X misses {} by XBOOLE_1:65;
Tempty_f_net(X) = PTempty_f_net(X,{}) by Def5
.= Net (# X, {}, {} #) by A1,Def4;
hence thesis;
end;
theorem
for X holds the Places of Pempty_f_net(X) = {} &
the Transitions of Pempty_f_net(X) = X &
the Flow of Pempty_f_net(X) = {}
proof
let X;
A1: {} misses X by XBOOLE_1:65;
Pempty_f_net(X) = PTempty_f_net({},X) by Def6
.= Net (# {}, X, {} #) by A1,Def4;
hence thesis;
end;
theorem
for x holds the Places of (Tsingle_f_net(x)) = {} &
the Transitions of (Tsingle_f_net(x)) = {x} &
the Flow of (Tsingle_f_net(x)) = {}
proof
let x;
A1: {} misses {x} by XBOOLE_1:65;
Tsingle_f_net(x) = PTempty_f_net({},{x}) by Def7
.= Net (# {}, {x}, {} #) by A1,Def4;
hence thesis;
end;
theorem
for x holds the Places of (Psingle_f_net(x)) = {x} &
the Transitions of (Psingle_f_net(x)) = {} &
the Flow of (Psingle_f_net(x)) = {}
proof
let x;
A1:{x} misses {} by XBOOLE_1:65;
Psingle_f_net(x) = PTempty_f_net({x},{}) by Def8
.= Net (# {x}, {}, {} #) by A1,Def4;
hence thesis;
end;
theorem
the Places of empty_f_net = {} &
the Transitions of empty_f_net = {} &
the Flow of empty_f_net = {}
proof
{} misses {} by XBOOLE_1:65;
then empty_f_net = Net (# {}, {}, {} #) by Def4,Def9;
hence thesis;
end;
theorem
the Places of M c= Elements M & the Transitions of M c= Elements M
by NET_1:4,5;
canceled 2;
theorem Th11:
(([x,y] in the Flow of M & x in the Transitions of M) implies
not x in the Places of M & not y in the Transitions of M &
y in the Places of M) &
(([x,y] in the Flow of M & y in the Transitions of M) implies
not y in the Places of M & not x in the Transitions of M &
x in the Places of M) &
(([x,y] in the Flow of M & x in the Places of M) implies
not y in the Places of M & not x in the Transitions of M &
y in the Transitions of M) &
(([x,y] in the Flow of M & y in the Places of M) implies
not x in the Places of M & not y in the Transitions of M &
x in the Transitions of M)
proof
(the Places of M) misses (the Transitions of M) &
((the Flow of M) c= [:the Places of M, the Transitions of M:] \/
[:the Transitions of M, the Places of M:]) by NET_1:def 1;
hence thesis by SYSREL:22;
end;
theorem
chaos(M) <> {}
proof
A1:chaos(M) = Elements(M) \/ {Elements(M)} by Def2;
Elements(M) in {Elements(M)} by TARSKI:def 1;
hence thesis by A1,XBOOLE_0:def 2;
end;
theorem Th13:
(the Flow of M) c= [:Elements(M), Elements(M):] &
(the Flow of M)~ c= [:Elements(M), Elements(M):]
proof
(the Flow of M) c= [:Elements(M), Elements(M):]
proof
A1: the Places of M c= Elements(M) by NET_1:4;
A2:the Transitions of M c= Elements(M) by NET_1:5;
then A3:[:the Places of M, the Transitions of M:] c=
[:Elements(M), Elements(M):] by A1,ZFMISC_1:119;
[:the Transitions of M, the Places of M:] c=
[:Elements(M), Elements(M):] by A1,A2,ZFMISC_1:119;
then A4:[:the Places of M, the Transitions of M:] \/
[:the Transitions of M, the Places of M:] c=
[:Elements(M), Elements(M):] by A3,XBOOLE_1:8;
the Flow of M c= [:the Places of M, the Transitions of M:] \/
[:the Transitions of M, the Places of M:] by NET_1:def 1;
hence thesis by A4,XBOOLE_1:1;
end;
hence thesis by SYSREL:16;
end;
theorem Th14:
rng ((the Flow of M)|(the Transitions of M)) c= (the Places of M) &
rng ((the Flow of M)~|(the Transitions of M)) c= (the Places of M) &
dom ((the Flow of M)|(the Transitions of M)) c=
(the Transitions of M) &
dom ((the Flow of M)~|(the Transitions of M)) c=
(the Transitions of M) &
rng ((the Flow of M)|(the Places of M)) c= (the Transitions of M) &
rng ((the Flow of M)~|(the Places of M)) c= (the Transitions of M) &
dom ((the Flow of M)|(the Places of M)) c= (the Places of M) &
dom ((the Flow of M)~|(the Places of M)) c= (the Places of M) &
rng id(the Transitions of M) c= (the Transitions of M) &
dom id(the Transitions of M) c= (the Transitions of M) &
rng id(the Places of M) c= (the Places of M) &
dom id(the Places of M) c= (the Places of M)
proof
A1:rng ((the Flow of M)|(the Transitions of M)) c= (the Places of M)
proof
for x holds x in rng ((the Flow of M)|(the Transitions of M)) implies
x in (the Places of M)
proof
let x;
assume x in rng ((the Flow of M)|(the Transitions of M));
then consider y such that A2:[y,x] in
(the Flow of M)|(the Transitions of M) by RELAT_1:def 5;
y in (the Transitions of M) & [y,x] in (the Flow of M) by A2,RELAT_1:def
11
;
hence thesis by Th11;
end;
hence thesis by TARSKI:def 3;
end;
A3: rng ((the Flow of M)~|(the Transitions of M)) c= (the Places of M)
proof
for x holds x in rng ((the Flow of M)~|(the Transitions of M)) implies
x in (the Places of M)
proof
let x;
assume x in rng ((the Flow of M)~|(the Transitions of M));
then consider y such that
A4: [y,x] in (the Flow of M)~|(the Transitions of M) by RELAT_1:def 5;
y in (the Transitions of M) & [y,x] in (the Flow of M)~ by A4,RELAT_1:def
11
;
then y in (the Transitions of M) & [x,y] in (the Flow of M) by RELAT_1:def 7
;
hence thesis by Th11;
end;
hence thesis by TARSKI:def 3;
end;
A5:rng ((the Flow of M)|(the Places of M)) c= (the Transitions of M)
proof
for x holds x in rng ((the Flow of M)|(the Places of M)) implies
x in (the Transitions of M)
proof
let x;
assume x in rng ((the Flow of M)|(the Places of M));
then consider y such that A6:[y,x] in (the Flow of M)|(the Places of M) by
RELAT_1:def 5;
y in (the Places of M) & [y,x] in (the Flow of M) by A6,RELAT_1:def 11;
hence thesis by Th11;
end;
hence thesis by TARSKI:def 3;
end;
rng ((the Flow of M)~|(the Places of M)) c= (the Transitions of M)
proof
for x holds x in rng ((the Flow of M)~|(the Places of M)) implies
x in (the Transitions of M)
proof
let x;
assume x in rng ((the Flow of M)~|(the Places of M));
then consider y such that A7:
[y,x] in (the Flow of M)~|(the Places of M) by RELAT_1:def 5;
y in (the Places of M) & [y,x] in (the Flow of M)~ by A7,RELAT_1:def 11;
then y in (the Places of M) & [x,y] in (the Flow of M) by RELAT_1:def 7;
hence thesis by Th11;
end;
hence thesis by TARSKI:def 3;
end;
hence thesis by A1,A3,A5,RELAT_1:71,87;
end;
Lm1:
for A,B,C,D being set st B misses D & A c= B & C c= D holds
A misses C
proof
let A,B,C,D be set; assume A1: B misses D & A c= B & C c= D;
assume A meets C;
then consider x be set such that
A2: x in A /\ C by XBOOLE_0:4;
A /\ C c= B /\ D by A1,XBOOLE_1:27;
hence thesis by A1,A2,XBOOLE_0:4;
end;
theorem Th15:
rng ((the Flow of M)|(the Transitions of M)) misses
dom((the Flow of M)|(the Transitions of M)) &
rng ((the Flow of M)|(the Transitions of M)) misses
dom((the Flow of M)~|(the Transitions of M)) &
rng ((the Flow of M)|(the Transitions of M)) misses
dom(id(the Transitions of M)) &
rng ((the Flow of M)~|(the Transitions of M)) misses
dom((the Flow of M)|(the Transitions of M)) &
rng ((the Flow of M)~|(the Transitions of M)) misses
dom((the Flow of M)~|(the Transitions of M)) &
rng ((the Flow of M)~|(the Transitions of M)) misses
dom(id(the Transitions of M)) &
dom ((the Flow of M)|(the Transitions of M)) misses
rng((the Flow of M)|(the Transitions of M)) &
dom ((the Flow of M)|(the Transitions of M)) misses
rng((the Flow of M)~|(the Transitions of M)) &
dom ((the Flow of M)|(the Transitions of M)) misses
rng(id(the Places of M)) &
dom ((the Flow of M)~|(the Transitions of M)) misses
rng((the Flow of M)|(the Transitions of M)) &
dom ((the Flow of M)~|(the Transitions of M)) misses
rng((the Flow of M)~|(the Transitions of M)) &
dom ((the Flow of M)~|(the Transitions of M)) misses
rng(id(the Places of M)) &
rng ((the Flow of M)|(the Places of M)) misses
dom((the Flow of M)|(the Places of M)) &
rng ((the Flow of M)|(the Places of M)) misses
dom((the Flow of M)~|(the Places of M)) &
rng ((the Flow of M)|(the Places of M)) misses
dom(id(the Places of M)) &
rng ((the Flow of M)~|(the Places of M)) misses
dom((the Flow of M)|(the Places of M)) &
rng ((the Flow of M)~|(the Places of M)) misses
dom((the Flow of M)~|(the Places of M)) &
rng ((the Flow of M)~|(the Places of M)) misses
dom(id(the Places of M)) &
dom ((the Flow of M)|(the Places of M)) misses
rng((the Flow of M)|(the Places of M)) &
dom ((the Flow of M)|(the Places of M)) misses
rng((the Flow of M)~|(the Places of M)) &
dom ((the Flow of M)|(the Places of M)) misses
rng(id(the Transitions of M)) &
dom ((the Flow of M)~|(the Places of M)) misses
rng((the Flow of M)|(the Places of M)) &
dom ((the Flow of M)~|(the Places of M)) misses
rng((the Flow of M)~|(the Places of M)) &
dom ((the Flow of M)~|(the Places of M)) misses
rng(id(the Transitions of M))
proof
set R = (the Flow of M)|(the Transitions of M);
set S = (the Flow of M)~|(the Transitions of M);
set T = id(the Transitions of M);
set R1 = (the Flow of M)|(the Places of M);
set S1 = (the Flow of M)~|(the Places of M);
set T1 = id(the Places of M);
A1:dom R c= the Transitions of M & rng R c= the Places of M by Th14;
A2:dom S c= the Transitions of M & rng S c= the Places of M by Th14;
A3:dom T c= the Transitions of M & rng T c= the Transitions of M by Th14;
A4:dom R1 c= the Places of M & rng R1 c= the Transitions of M by Th14;
A5:dom S1 c= the Places of M & rng S1 c= the Transitions of M by Th14;
A6:dom T1 c= the Places of M & rng T1 c= the Places of M by Th14;
(the Places of M) misses (the Transitions of M) by NET_1:def 1;
hence thesis by A1,A2,A3,A4,A5,A6,Lm1;
end;
theorem Th16:
(((the Flow of M)|(the Transitions of M)) *
((the Flow of M)|(the Transitions of M)) = {}) &
(((the Flow of M)~|(the Transitions of M)) *
((the Flow of M)~|(the Transitions of M)) = {}) &
(((the Flow of M)|(the Transitions of M)) *
((the Flow of M)~|(the Transitions of M)) = {}) &
(((the Flow of M)~|(the Transitions of M)) *
((the Flow of M)|(the Transitions of M)) = {}) &
(((the Flow of M)|(the Places of M)) *
((the Flow of M)|(the Places of M)) = {}) &
(((the Flow of M)~|(the Places of M)) *
((the Flow of M)~|(the Places of M)) = {}) &
(((the Flow of M)|(the Places of M)) *
((the Flow of M)~|(the Places of M)) = {}) &
(((the Flow of M)~|(the Places of M)) *
((the Flow of M)|(the Places of M)) = {})
proof
A1:(((the Flow of M)|(the Transitions of M)) *
((the Flow of M)|(the Transitions of M)) = {})
proof
rng ((the Flow of M)|(the Transitions of M)) misses
dom ((the Flow of M)|(the Transitions of M)) by Th15;
hence thesis by RELAT_1:67;
end;
A2:((the Flow of M)~|(the Transitions of M)) *
((the Flow of M)~|(the Transitions of M)) = {}
proof
rng ((the Flow of M)~|(the Transitions of M)) misses
dom ((the Flow of M)~|(the Transitions of M)) by Th15;
hence thesis by RELAT_1:67;
end;
A3:((the Flow of M)|(the Transitions of M)) *
((the Flow of M)~|(the Transitions of M)) = {}
proof
rng ((the Flow of M)|(the Transitions of M)) misses
dom ((the Flow of M)~|(the Transitions of M)) by Th15;
hence thesis by RELAT_1:67;
end;
A4:((the Flow of M)~|(the Transitions of M)) *
((the Flow of M)|(the Transitions of M)) = {}
proof
rng ((the Flow of M)~|(the Transitions of M)) misses
dom ((the Flow of M)|(the Transitions of M)) by Th15;
hence thesis by RELAT_1:67;
end;
A5:(((the Flow of M)|(the Places of M)) *
((the Flow of M)|(the Places of M)) = {})
proof
rng ((the Flow of M)|(the Places of M)) misses
dom ((the Flow of M)|(the Places of M)) by Th15;
hence thesis by RELAT_1:67;
end;
A6:((the Flow of M)~|(the Places of M)) *
((the Flow of M)~|(the Places of M)) = {}
proof
rng ((the Flow of M)~|(the Places of M)) misses
dom ((the Flow of M)~|(the Places of M)) by Th15;
hence thesis by RELAT_1:67;
end;
A7:((the Flow of M)|(the Places of M)) *
((the Flow of M)~|(the Places of M)) = {}
proof
rng ((the Flow of M)|(the Places of M)) misses
dom ((the Flow of M)~|(the Places of M)) by Th15;
hence thesis by RELAT_1:67;
end;
((the Flow of M)~|(the Places of M)) *
((the Flow of M)|(the Places of M)) = {}
proof
rng ((the Flow of M)~|(the Places of M)) misses
dom ((the Flow of M)|(the Places of M)) by Th15;
hence thesis by RELAT_1:67;
end;
hence thesis by A1,A2,A3,A4,A5,A6,A7;
end;
theorem Th17:
(((the Flow of M)|(the Transitions of M)) *
id(the Places of M) = (the Flow of M)|(the Transitions of M)) &
(((the Flow of M)~|(the Transitions of M)) *
id(the Places of M) = (the Flow of M)~|(the Transitions of M)) &
((id(the Transitions of M) *
((the Flow of M)|(the Transitions of M))) =
(the Flow of M)|(the Transitions of M)) &
((id(the Transitions of M) *
((the Flow of M)~|(the Transitions of M))) =
(the Flow of M)~|(the Transitions of M)) &
(((the Flow of M)|(the Places of M)) *
id(the Transitions of M) = (the Flow of M)|(the Places of M)) &
(((the Flow of M)~|(the Places of M)) *
id(the Transitions of M) = (the Flow of M)~|(the Places of M)) &
(id(the Places of M)) *
((the Flow of M)|(the Places of M)) =
(the Flow of M)|(the Places of M) &
(id(the Places of M)) * ((the Flow of M)~|(the Places of M)) =
(the Flow of M)~|(the Places of M) &
((the Flow of M)|(the Places of M)) * id(the Transitions of M) =
(the Flow of M)|(the Places of M) &
((the Flow of M)~|(the Places of M)) * id(the Transitions of M) =
(the Flow of M)~|(the Places of M) &
(id(the Transitions of M) * ((the Flow of M)|(the Places of M))) = {} &
(id(the Transitions of M) *
((the Flow of M)~|(the Places of M))) = {} &
((the Flow of M)|(the Places of M)) * id(the Places of M) = {} &
((the Flow of M)~|(the Places of M)) * id(the Places of M) = {} &
(id(the Places of M)) *
((the Flow of M)|(the Transitions of M)) = {} &
(id(the Places of M)) *
((the Flow of M)~|(the Transitions of M)) = {} &
((the Flow of M)|(the Transitions of M)) *
(id(the Transitions of M)) = {} &
((the Flow of M)~|(the Transitions of M)) *
(id(the Transitions of M)) = {}
proof
A1: ((the Flow of M)|(the Transitions of M)) *
id(the Places of M) = (the Flow of M)|(the Transitions of M)
proof
rng ((the Flow of M)|(the Transitions of M)) c= the Places of M by Th14;
hence thesis by RELAT_1:79;
end;
A2:((the Flow of M)~|(the Transitions of M)) *
id(the Places of M) = (the Flow of M)~|(the Transitions of M)
proof
rng ((the Flow of M)~|(the Transitions of M)) c= the Places of M by Th14;
hence thesis by RELAT_1:79;
end;
A3:(id(the Transitions of M) *
((the Flow of M)|(the Transitions of M))) =
(the Flow of M)|(the Transitions of M)
proof
dom ((the Flow of M)|(the Transitions of M)) c= the Transitions of M
by Th14;
hence thesis by RELAT_1:77;
end;
A4:(id(the Transitions of M) *
((the Flow of M)~|(the Transitions of M))) =
(the Flow of M)~|(the Transitions of M)
proof
dom ((the Flow of M)~|(the Transitions of M)) c= (the Transitions of M)
by Th14;
hence thesis by RELAT_1:77;
end;
A5: ((the Flow of M)|(the Places of M)) *
id(the Transitions of M) = (the Flow of M)|(the Places of M)
proof
rng ((the Flow of M)|(the Places of M)) c= the Transitions of M by Th14;
hence thesis by RELAT_1:79;
end;
A6:((the Flow of M)~|(the Places of M)) *
id(the Transitions of M) = (the Flow of M)~|(the Places of M)
proof
rng ((the Flow of M)~|(the Places of M)) c= the Transitions of M by Th14;
hence thesis by RELAT_1:79;
end;
A7:(id(the Places of M) *
((the Flow of M)|(the Places of M))) =
(the Flow of M)|(the Places of M)
proof
dom ((the Flow of M)|(the Places of M)) c= the Places of M by Th14;
hence thesis by RELAT_1:77;
end;
A8:(id(the Places of M) *
((the Flow of M)~|(the Places of M))) =
(the Flow of M)~|(the Places of M)
proof
dom ((the Flow of M)~|(the Places of M)) c= the Places of M by Th14;
hence thesis by RELAT_1:77;
end;
A9:(id(the Transitions of M) *
((the Flow of M)|(the Places of M))) = {}
proof
dom ((the Flow of M)|(the Places of M)) misses
rng (id(the Transitions of M)) by Th15;
hence thesis by RELAT_1:67;
end;
A10:(id(the Transitions of M) *
((the Flow of M)~|(the Places of M))) = {}
proof
dom ((the Flow of M)~|(the Places of M)) misses
rng (id(the Transitions of M)) by Th15;
hence thesis by RELAT_1:67;
end;
A11: ((the Flow of M)|(the Places of M)) *
id(the Places of M) = {}
proof
rng ((the Flow of M)|(the Places of M)) misses
dom (id(the Places of M)) by Th15;
hence thesis by RELAT_1:67;
end;
A12:((the Flow of M)~|(the Places of M)) *
id(the Places of M) = {}
proof
rng ((the Flow of M)~|(the Places of M)) misses
dom (id(the Places of M)) by Th15;
hence thesis by RELAT_1:67;
end;
A13:(id(the Places of M) *
((the Flow of M)|(the Transitions of M))) = {}
proof
rng id(the Places of M) misses
dom ((the Flow of M)|(the Transitions of M)) by Th15;
hence thesis by RELAT_1:67;
end;
A14:(id(the Places of M) *
((the Flow of M)~|(the Transitions of M))) = {}
proof
rng id(the Places of M) misses
dom ((the Flow of M)~|(the Transitions of M)) by Th15;
hence thesis by RELAT_1:67;
end;
A15:((the Flow of M)|(the Transitions of M)) *
id(the Transitions of M) = {}
proof
rng ((the Flow of M)|(the Transitions of M)) misses
dom id(the Transitions of M) by Th15;
hence thesis by RELAT_1:67;
end;
((the Flow of M)~|(the Transitions of M)) *
id(the Transitions of M) = {}
proof
rng ((the Flow of M)~|(the Transitions of M)) misses
dom id(the Transitions of M) by Th15;
hence thesis by RELAT_1:67;
end;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,A12,A13,A14,A15;
end;
theorem Th18:
(((the Flow of M)~|(the Transitions of M)) misses (id(Elements(M)))) &
(((the Flow of M)|(the Transitions of M)) misses (id(Elements(M)))) &
(((the Flow of M)~|(the Places of M)) misses (id(Elements(M)))) &
(((the Flow of M)|(the Places of M)) misses (id(Elements(M))))
proof
set T = id(Elements(M));
thus ((the Flow of M)~|(the Transitions of M)) misses (id(Elements(M)))
proof
set R = (the Flow of M)~|(the Transitions of M);
for x,y holds not [x,y] in R /\ T
proof
let x,y;
assume [x,y] in R /\ T;
then A1:[x,y] in R & [x,y] in T by XBOOLE_0:def 3;
then x in (the Transitions of M) & [x,y] in (the Flow of M)~ by RELAT_1:def
11;
then x in (the Transitions of M) & [y,x] in (the Flow of M) by RELAT_1:def 7
;
then x <> y by Th11;
hence thesis by A1,RELAT_1:def 10;
end;
then R /\ T = {} by RELAT_1:56;
hence thesis by XBOOLE_0:def 7;
end;
thus ((the Flow of M)|(the Transitions of M)) misses (id(Elements(M)))
proof
set R = (the Flow of M)|(the Transitions of M);
for x,y holds not [x,y] in R /\ T
proof
let x,y;
assume [x,y] in R /\ T;
then A2:[x,y] in R & [x,y] in T by XBOOLE_0:def 3;
then x in (the Transitions of M) & [x,y] in (the Flow of M) by RELAT_1:def
11;
then x <> y by Th11;
hence thesis by A2,RELAT_1:def 10;
end; then R /\ T = {} by RELAT_1:56;
hence thesis by XBOOLE_0:def 7;
end;
thus ((the Flow of M)~|(the Places of M)) misses (id(Elements(M)))
proof
set R = (the Flow of M)~|(the Places of M);
for x,y holds not [x,y] in R /\ T
proof
let x,y;
assume [x,y] in R /\ T;
then A3:[x,y] in R & [x,y] in T by XBOOLE_0:def 3;
then x in the Places of M & [x,y] in (the Flow of M)~ by RELAT_1:def 11;
then x in the Places of M & [y,x] in the Flow of M by RELAT_1:def 7;
then x <> y by Th11;
hence thesis by A3,RELAT_1:def 10;
end;
then R /\ T = {} by RELAT_1:56;
hence thesis by XBOOLE_0:def 7;
end;
set R = (the Flow of M)|(the Places of M);
for x,y holds not [x,y] in R /\ T
proof
let x,y;
assume [x,y] in R /\ T;
then A4:[x,y] in R & [x,y] in T by XBOOLE_0:def 3;
then x in the Places of M & [x,y] in the Flow of M by RELAT_1:def 11;
then x <> y by Th11;
hence thesis by A4,RELAT_1:def 10;
end;
then R /\ T = {} by RELAT_1:56;
hence thesis by XBOOLE_0:def 7;
end;
theorem Th19:
((the Flow of M)~|(the Transitions of M)) \/
(id(the Places of M)) \ id(Elements(M)) =
(the Flow of M)~|(the Transitions of M) &
((the Flow of M)|(the Transitions of M)) \/
(id(the Places of M)) \ id(Elements(M)) =
(the Flow of M)|(the Transitions of M) &
(((the Flow of M)~|(the Places of M)) \/
(id(the Places of M))) \ id(Elements(M)) =
(the Flow of M)~|(the Places of M) &
(((the Flow of M)|(the Places of M)) \/
(id(the Places of M))) \ id(Elements(M)) =
(the Flow of M)|(the Places of M) &
((the Flow of M)~|(the Places of M)) \/
(id(the Transitions of M)) \ id(Elements(M)) =
(the Flow of M)~|(the Places of M) &
((the Flow of M)|(the Places of M)) \/
(id(the Transitions of M)) \ id(Elements(M)) =
(the Flow of M)|(the Places of M) &
(((the Flow of M)~|(the Transitions of M)) \/
(id(the Transitions of M))) \ id(Elements(M)) =
(the Flow of M)~|(the Transitions of M) &
(((the Flow of M)|(the Transitions of M)) \/
(id(the Transitions of M))) \ id(Elements(M)) =
(the Flow of M)|(the Transitions of M)
proof
A1:((the Flow of M)~|(the Transitions of M)) \/
(id(the Places of M)) \ id(Elements(M)) =
(the Flow of M)~|(the Transitions of M)
proof
set R = (the Flow of M)~|(the Transitions of M);
set S = id(the Places of M);
set T = id(Elements(M));
the Places of M c= Elements(M) by NET_1:4;
then A2: S c= T by SYSREL:33;
A3: R misses T by Th18;
(R \/ S) \ T = (R \ T) \/ (S \ T) by XBOOLE_1:42
.= (R \ T) \/ {} by A2,XBOOLE_1:37
.= R by A3,XBOOLE_1:83;
hence thesis;
end;
A4:((the Flow of M)|(the Transitions of M)) \/
(id(the Places of M)) \ id(Elements(M)) =
(the Flow of M)|(the Transitions of M)
proof
set R = (the Flow of M)|(the Transitions of M);
set S = id(the Places of M);
set T = id(Elements(M));
the Places of M c= Elements(M) by NET_1:4;
then A5: S c= T by SYSREL:33;
A6: R misses T by Th18;
(R \/ S) \ T = (R \ T) \/ (S \ T) by XBOOLE_1:42
.= (R \ T) \/ {} by A5,XBOOLE_1:37
.= R by A6,XBOOLE_1:83;
hence thesis;
end;
A7:((the Flow of M)~|(the Places of M)) \/
(id(the Places of M)) \ id(Elements(M)) =
(the Flow of M)~|(the Places of M)
proof
set R = (the Flow of M)~|(the Places of M);
set S = id(the Places of M);
set T = id(Elements(M));
the Places of M c= Elements(M) by NET_1:4;
then A8: S c= T by SYSREL:33;
A9: R misses T by Th18;
(R \/ S) \ T = (R \ T) \/ (S \ T) by XBOOLE_1:42
.= (R \ T) \/ {} by A8,XBOOLE_1:37
.= R by A9,XBOOLE_1:83;
hence thesis;
end;
A10:((the Flow of M)|(the Places of M)) \/
(id(the Places of M)) \ id(Elements(M)) =
(the Flow of M)|(the Places of M)
proof
set R = (the Flow of M)|(the Places of M);
set S = id(the Places of M);
set T = id(Elements(M));
the Places of M c= Elements(M) by NET_1:4;
then A11: S c= T by SYSREL:33;
A12: R misses T by Th18;
(R \/ S) \ T = (R \ T) \/ (S \ T) by XBOOLE_1:42
.= (R \ T) \/ {} by A11,XBOOLE_1:37
.= R by A12,XBOOLE_1:83;
hence thesis;
end;
A13:((the Flow of M)~|(the Places of M)) \/
(id(the Transitions of M)) \ id(Elements(M)) =
(the Flow of M)~|(the Places of M)
proof
set R = (the Flow of M)~|(the Places of M);
set S = id(the Transitions of M);
set T = id(Elements(M));
the Transitions of M c= Elements(M) by NET_1:5;
then A14: S c= T by SYSREL:33;
A15: R misses T by Th18;
(R \/ S) \ T = (R \ T) \/ (S \ T) by XBOOLE_1:42
.= (R \ T) \/ {} by A14,XBOOLE_1:37
.= R by A15,XBOOLE_1:83;
hence thesis;
end;
A16:((the Flow of M)|(the Places of M)) \/
(id(the Transitions of M)) \ id(Elements(M)) =
(the Flow of M)|(the Places of M)
proof
set R = (the Flow of M)|(the Places of M);
set S = id(the Transitions of M);
set T = id(Elements(M));
the Transitions of M c= Elements(M) by NET_1:5;
then A17: S c= T by SYSREL:33;
A18: R misses T by Th18;
(R \/ S) \ T = (R \ T) \/ (S \ T) by XBOOLE_1:42
.= (R \ T) \/ {} by A17,XBOOLE_1:37
.= R by A18,XBOOLE_1:83;
hence thesis;
end;
A19:((the Flow of M)~|(the Transitions of M)) \/
(id(the Transitions of M)) \ id(Elements(M)) =
(the Flow of M)~|(the Transitions of M)
proof
set R = (the Flow of M)~|(the Transitions of M);
set S = id(the Transitions of M);
set T = id(Elements(M));
the Transitions of M c= Elements(M) by NET_1:5;
then A20: S c= T by SYSREL:33;
A21: R misses T by Th18;
(R \/ S) \ T = (R \ T) \/ (S \ T) by XBOOLE_1:42
.= (R \ T) \/ {} by A20,XBOOLE_1:37
.= R by A21,XBOOLE_1:83;
hence thesis;
end;
((the Flow of M)|(the Transitions of M)) \/
(id(the Transitions of M)) \ id(Elements(M)) =
(the Flow of M)|(the Transitions of M)
proof
set R = (the Flow of M)|(the Transitions of M);
set S = id(the Transitions of M);
set T = id(Elements(M));
the Transitions of M c= Elements(M) by NET_1:5;
then A22: S c= T by SYSREL:33;
A23: R misses T by Th18;
(R \/ S) \ T = (R \ T) \/ (S \ T) by XBOOLE_1:42
.= (R \ T) \/ {} by A22,XBOOLE_1:37
.= R by A23,XBOOLE_1:83;
hence thesis;
end;
hence thesis by A1,A4,A7,A10,A13,A16,A19;
end;
theorem Th20:
((the Flow of M)|(the Places of M))~ =
((the Flow of M)~)|(the Transitions of M) &
((the Flow of M)|(the Transitions of M))~ =
((the Flow of M)~)|(the Places of M)
proof
set R = the Flow of M;
set X = the Places of M;
set Y = the Transitions of M;
A1:((R|X)~) c= ((R~)|Y)
proof
for x,y holds [x,y] in (R|X)~ implies [x,y] in (R~)|Y
proof
let x,y;
assume [x,y] in (R|X)~;
then [y,x] in R|X by RELAT_1:def 7;
then [y,x] in R & y in X by RELAT_1:def 11;
then [x,y] in R~ & x in Y by Th11,RELAT_1:def 7;
hence thesis by RELAT_1:def 11;
end;
hence thesis by RELAT_1:def 3;
end;
A2: ((R~)|Y) c= ((R|X)~)
proof
for x,y holds [x,y] in (R~)|Y implies [x,y] in (R|X)~
proof
let x,y;
assume [x,y] in (R~)|Y;
then [x,y] in R~ & x in Y by RELAT_1:def 11;
then [y,x] in R & x in Y by RELAT_1:def 7;
then [y,x] in R & y in X by Th11;
then [y,x] in R|X by RELAT_1:def 11;
hence thesis by RELAT_1:def 7;
end;
hence thesis by RELAT_1:def 3;
end;
A3:((R|Y)~) c= ((R~)|X)
proof
for x,y holds [x,y] in (R|Y)~ implies [x,y] in (R~)|X
proof
let x,y;
assume [x,y] in (R|Y)~;
then [y,x] in R|Y by RELAT_1:def 7;
then [y,x] in R & y in Y by RELAT_1:def 11;
then [x,y] in R~ & x in X by Th11,RELAT_1:def 7;
hence thesis by RELAT_1:def 11;
end;
hence thesis by RELAT_1:def 3;
end;
((R~)|X) c= ((R|Y)~)
proof
for x,y holds [x,y] in (R~)|X implies [x,y] in (R|Y)~
proof
let x,y;
assume [x,y] in (R~)|X;
then [x,y] in R~ & x in X by RELAT_1:def 11;
then [y,x] in R & x in X by RELAT_1:def 7;
then [y,x] in R & y in Y by Th11;
then [y,x] in R|Y by RELAT_1:def 11;
hence thesis by RELAT_1:def 7;
end;
hence thesis by RELAT_1:def 3;
end;
hence thesis by A1,A2,A3,XBOOLE_0:def 10;
end;
theorem Th21:
((the Flow of M)|(the Places of M)) \/
((the Flow of M)|(the Transitions of M)) = (the Flow of M) &
((the Flow of M)|(the Transitions of M)) \/
((the Flow of M)|(the Places of M)) = (the Flow of M) &
(((the Flow of M)|(the Places of M))~) \/
(((the Flow of M)|(the Transitions of M))~) = (the Flow of M)~ &
(((the Flow of M)|(the Transitions of M))~) \/
(((the Flow of M)|(the Places of M))~) = (the Flow of M)~
proof
set R = the Flow of M;
A1:the Flow of M c= [:Elements(M),Elements(M):] by Th13;
Elements(M) = (the Places of M) \/ (the Transitions of M) by NET_1:def 2;
then (R|the Places of M) \/ (R|the Transitions of M) = R by A1,SYSREL:25;
hence thesis by RELAT_1:40;
end;
:: T R A N S F O R M A T I O N S
:: A [F -> E]
definition
let M;
func f_enter(M) -> Relation equals :Def10:
((the Flow of M)~|(the Transitions of M)) \/ id(the Places of M);
correctness;
func f_exit(M) -> Relation equals :Def11:
((the Flow of M)|(the Transitions of M)) \/ id(the Places of M);
correctness;
end;
theorem
f_exit(M) c= [:Elements(M),Elements(M):] &
f_enter(M) c= [:Elements(M),Elements(M):]
proof
thus f_exit(M) c= [:Elements(M),Elements(M):]
proof
A1:id(the Places of M) c= [:Elements(M),Elements(M):]
proof
(the Places of M) c= Elements(M) by NET_1:4;
then A2: id(the Places of M) c= id(Elements(M)) by SYSREL:33;
id(Elements(M)) c= [:Elements(M),Elements(M):] by RELSET_1:28;
hence thesis by A2,XBOOLE_1:1;
end;
A3:(the Flow of M)|(the Transitions of M) c= (the Flow of M) by RELAT_1:88;
(the Flow of M) c= [:Elements(M),Elements(M):] by Th13;
then (the Flow of M)|(the Transitions of M) c= [:Elements(M),Elements(M):]
by A3,XBOOLE_1:1;
then ((the Flow of M)|(the Transitions of M)) \/
id(the Places of M) c= [:Elements(M),Elements(M):] by A1,XBOOLE_1:8;
hence thesis by Def11;
end;
A4:id(the Places of M) c= [:Elements(M),Elements(M):]
proof
(the Places of M) c= Elements(M) by NET_1:4;
then A5: id(the Places of M) c= id(Elements(M)) by SYSREL:33;
id(Elements(M)) c= [:Elements(M),Elements(M):] by RELSET_1:28;
hence thesis by A5,XBOOLE_1:1;
end;
A6:(the Flow of M)~|(the Transitions of M) c=
(the Flow of M)~ by RELAT_1:88;
(the Flow of M)~ c= [:Elements(M),Elements(M):] by Th13;
then (the Flow of M)~|(the Transitions of M) c= [:Elements(M),Elements(M):]
by A6,XBOOLE_1:1;
then ((the Flow of M)~|(the Transitions of M)) \/
id(the Places of M) c= [:Elements(M),Elements(M):]
by A4,XBOOLE_1:8;
hence thesis by Def10;
end;
theorem
dom(f_exit(M)) c= Elements(M) & rng(f_exit(M)) c= Elements(M) &
dom(f_enter(M)) c= Elements(M) & rng(f_enter(M)) c= Elements(M)
proof
A1: for x holds x in dom(f_exit(M)) implies x in Elements(M)
proof
let x;
assume x in dom(f_exit(M));
then x in dom(((the Flow of M)|(the Transitions of M)) \/
id(the Places of M)) by Def11;
then x in dom((the Flow of M)|(the Transitions of M)) \/
dom(id(the Places of M)) by RELAT_1:13;
then x in dom((the Flow of M)|(the Transitions of M)) or
x in dom(id(the Places of M)) by XBOOLE_0:def 2;
then x in (the Transitions of M) or x in the Places of M by RELAT_1:71,86;
then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
hence thesis by NET_1:def 2;
end;
A2: for x holds x in rng(f_exit(M)) implies x in Elements(M)
proof
let x;
assume x in rng(f_exit(M));
then x in rng(((the Flow of M)|(the Transitions of M)) \/
id(the Places of M)) by Def11;
then A3: x in rng((the Flow of M)|(the Transitions of M)) \/
rng(id(the Places of M)) by RELAT_1:26;
A4:x in rng((the Flow of M)|(the Transitions of M)) implies thesis
proof
assume x in rng((the Flow of M)|(the Transitions of M));
then consider y such that A5:
[y,x] in (the Flow of M)|(the Transitions of M) by
RELAT_1:def 5;
y in (the Transitions of M) & [y,x] in (the Flow of M) by A5,RELAT_1:def
11
;
then x in (the Transitions of M) or x in the Places of M by Th11;
then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
hence thesis by NET_1:def 2;
end;
x in rng(id(the Places of M)) implies thesis
proof
assume x in rng(id(the Places of M));
then x in (the Transitions of M) or x in the Places of M by RELAT_1:71;
then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
hence thesis by NET_1:def 2;
end;
hence thesis by A3,A4,XBOOLE_0:def 2;
end;
A6: for x holds x in dom(f_enter(M)) implies x in Elements(M)
proof
let x;
assume x in dom(f_enter(M));
then x in dom(((the Flow of M)~|(the Transitions of M)) \/
id(the Places of M)) by Def10;
then x in dom((the Flow of M)~|(the Transitions of M)) \/
dom(id(the Places of M)) by RELAT_1:13;
then x in dom((the Flow of M)~|(the Transitions of M)) or
x in dom(id(the Places of M)) by XBOOLE_0:def 2;
then x in (the Transitions of M) or x in the Places of M by RELAT_1:71,86;
then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
hence thesis by NET_1:def 2;
end;
for x holds x in rng(f_enter(M)) implies x in Elements(M)
proof
let x;
assume x in rng(f_enter(M));
then x in rng(((the Flow of M)~|(the Transitions of M)) \/
id(the Places of M)) by Def10;
then A7: x in rng((the Flow of M)~|(the Transitions of M)) \/
rng(id(the Places of M)) by RELAT_1:26;
A8:x in rng((the Flow of M)~|(the Transitions of M)) implies thesis
proof
assume x in rng((the Flow of M)~|(the Transitions of M));
then consider y such that A9:
[y,x] in (the Flow of M)~|(the Transitions of M) by
RELAT_1:def 5;
y in (the Transitions of M) & [y,x] in (the Flow of M)~ by A9,RELAT_1:def
11
;
then y in (the Transitions of M) & [x,y] in (the Flow of M) by RELAT_1:def 7
;
then x in (the Transitions of M) or x in the Places of M by Th11;
then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
hence thesis by NET_1:def 2;
end;
x in rng(id(the Places of M)) implies thesis
proof
assume x in rng(id(the Places of M));
then x in (the Transitions of M) or x in the Places of M by RELAT_1:71;
then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
hence thesis by NET_1:def 2;
end;
hence thesis by A7,A8,XBOOLE_0:def 2;
end;
hence thesis by A1,A2,A6,TARSKI:def 3;
end;
theorem
(f_exit(M)) * (f_exit(M)) = f_exit(M) &
(f_exit(M)) * (f_enter(M)) = f_exit(M) &
(f_enter(M)) * (f_enter(M)) = f_enter(M) &
(f_enter(M)) * (f_exit(M)) = f_enter(M)
proof
A1:(f_exit(M)) * (f_exit(M)) = f_exit(M)
proof
set R = ((the Flow of M)|(the Transitions of M));
set S = id(the Places of M);
A2: S * R = {} by Th17;
A3: R * S = R by Th17;
A4: S * S = S by SYSREL:29;
(f_exit(M)) * (f_exit(M)) = (R \/ S) * (f_exit(M)) by Def11
.= (R \/ S) * (R \/ S) by Def11
.= (R * (R \/ S)) \/ (S * (R \/ S)) by SYSREL:20
.= ((R * R) \/ (R * S)) \/ (S * (R \/ S)) by RELAT_1:51
.= ((R * R) \/ (R * S)) \/ ((S * R) \/ (S * S)) by RELAT_1:51
.= ({} \/ R) \/ ({} \/ S) by A2,A3,A4,Th16 .= f_exit(M) by Def11;
hence thesis;
end;
A5:(f_exit(M)) * (f_enter(M)) = f_exit(M)
proof
set R = ((the Flow of M)|(the Transitions of M));
set S = id(the Places of M);
set T = ((the Flow of M)~|(the Transitions of M));
A6: S * T = {} by Th17;
A7: R * S = R by Th17;
A8: S * S = S by SYSREL:29;
(f_exit(M)) * (f_enter(M)) = (R \/ S) * (f_enter(M)) by Def11
.= (R \/ S) * (T \/ S) by Def10
.= (R * (T \/ S)) \/ (S * (T \/ S)) by SYSREL:20
.= ((R * T) \/ (R * S)) \/ (S * (T \/ S))
by RELAT_1:51
.= ((R * T) \/ (R * S)) \/ ((S * T) \/ (S * S))
by RELAT_1:51
.= ({} \/ R) \/ ({} \/ S) by A6,A7,A8,Th16
.=f_exit(M) by Def11;
hence thesis;
end;
A9:(f_enter(M)) * (f_enter(M)) = f_enter(M)
proof
set R = ((the Flow of M)~|(the Transitions of M));
set S = id(the Places of M);
A10: S * R = {} by Th17;
A11: R * S = R by Th17;
A12: S * S = S by SYSREL:29;
(f_enter(M)) * (f_enter(M)) = (R \/ S) * (f_enter(M)) by Def10
.= (R \/ S) * (R \/ S) by Def10
.= (R * (R \/ S)) \/ (S * (R \/ S)) by SYSREL:20
.= ((R * R) \/ (R * S)) \/ (S * (R \/ S))
by RELAT_1:51
.= ((R * R) \/ (R * S)) \/ ((S * R) \/ (S * S))
by RELAT_1:51
.= ({} \/ R) \/ ({} \/ S) by A10,A11,A12,Th16
.=f_enter(M) by Def10;
hence thesis;
end;
(f_enter(M)) * (f_exit(M)) = f_enter(M)
proof
set R = ((the Flow of M)|(the Transitions of M));
set S = id(the Places of M);
set T = ((the Flow of M)~|(the Transitions of M));
A13: T * S = T by Th17;
A14: S * R = {} by Th17;
A15: S * S = S by SYSREL:29;
(f_enter(M)) * (f_exit(M)) = (T \/ S) * (f_exit(M)) by Def10
.= (T \/ S) * (R \/ S) by Def11
.= (T * (R \/ S)) \/ (S * (R \/ S)) by SYSREL:20
.= ((T * R) \/ (T * S)) \/ (S * (R \/ S))
by RELAT_1:51
.= ((T * R) \/ (T * S)) \/ ((S * R) \/ (S * S))
by RELAT_1:51
.= ({} \/ T) \/ ({} \/ S) by A13,A14,A15,Th16
.=f_enter(M) by Def10;
hence thesis;
end;
hence thesis by A1,A5,A9;
end;
theorem
(f_exit(M)) * (f_exit(M) \ id(Elements(M))) = {} &
(f_enter(M)) * (f_enter(M) \ id(Elements(M))) = {}
proof
set S = id(the Places of M);
thus (f_exit(M)) * (f_exit(M) \ id(Elements(M))) = {}
proof
set R = (the Flow of M)|(the Transitions of M);
A1: S * R = {} by Th17;
(f_exit(M)) * (f_exit(M) \ id(Elements(M))) =
(R \/ S) * (f_exit(M) \ id(Elements(M)))
by Def11
.= (R \/ S) * ((R \/ S) \ (id(Elements(M)))) by Def11
.= (R \/ S) * R by Th19
.= (R * R) \/ (S * R) by SYSREL:20
.= {} by A1,Th16;
hence thesis;
end;
set R = ((the Flow of M)~|(the Transitions of M));
A2: S * R = {} by Th17;
(f_enter(M)) * (f_enter(M) \ id(Elements(M))) =
(R \/ S) * (f_enter(M) \ id(Elements(M)))
by Def10
.= (R \/ S) * ((R \/ S) \ (id(Elements(M)))) by Def10
.= (R \/ S) * R by Th19
.= (R * R) \/ (S * R) by SYSREL:20
.= {} by A2,Th16;
hence thesis;
end;
::B [F ->R]
definition
let M;
func f_prox(M) -> Relation equals
:Def12: ((the Flow of M)|(the Places of M) \/
(the Flow of M)~|(the Places of M)) \/
id(the Places of M);
correctness;
func f_flow(M) -> Relation equals
:Def13: (the Flow of M) \/ id(Elements(M));
correctness;
end;
theorem
f_prox(M) * f_prox(M) = f_prox(M) &
(f_prox(M) \ id(Elements(M))) * f_prox(M) = {} &
(f_prox(M) \/ ((f_prox(M))~)) \/ id(Elements(M)) =
f_flow(M) \/ (f_flow(M))~
proof
set R = (the Flow of M)|(the Places of M);
set S = (the Flow of M)~|(the Places of M);
set T = id(the Places of M);
set Q = id(Elements(M));
A1:((R \/ S) \/ T) \ Q = R \/ S
proof
((R \/ S) \/ T) \ Q = ((R \/ T) \/ (S \/ T)) \ Q by XBOOLE_1:5
.= ((R \/ T) \ (id(Elements(M))) \/
((S \/ T) \ (id(Elements(M))))) by XBOOLE_1:42
.= R \/
((S \/ T) \ (id(Elements(M)))) by Th19
.= R \/ S by Th19;
hence thesis;
end;
A2:(R \/ S) * (R \/ S) = {}
proof
(R \/ S) * (R \/ S) = ((R \/ S) * R) \/ ((R \/ S) *S) by SYSREL:20
.= ((R * R) \/ (S * R)) \/ ((R \/ S) *S) by SYSREL:20
.= ((R * R) \/ (S * R)) \/ ((R * S) \/ (S *S)) by SYSREL:20
.= ({} \/ (S * R)) \/ ((R * S) \/ (S *S)) by Th16
.= ({} \/ {}) \/ ((R * S) \/ (S *S)) by Th16
.= ({} \/ {}) \/ ({} \/ (S *S)) by Th16
.= {} by Th16;
hence thesis;
end;
A3:R \/ S~ = the Flow of M & R~ \/ S = (the Flow of M)~
proof
A4:R \/ S~ = R \/ (((the Flow of M)|(the Transitions of M))~)~ by Th20
.= the Flow of M by Th21;
R~ \/ S = R~ \/ ((the Flow of M)|(the Transitions of M))~ by Th20
.= (the Flow of M)~ by Th21;
hence thesis by A4;
end;
A5:(R \/ S)~ \/ (R \/ S) = (the Flow of M) \/ (the Flow of M)~
proof
(R \/ S)~ \/ (R \/ S) = (R~ \/ S~) \/ (R \/ S) by RELAT_1:40
.= (R~ \/ (S \/ R)) \/ S~ by XBOOLE_1:4
.= ((R~ \/ S) \/ R) \/ S~ by XBOOLE_1:4
.= (the Flow of M) \/ (the Flow of M)~ by A3,XBOOLE_1:4;
hence thesis;
end;
A6:f_prox(M) \/ (f_prox(M))~ =
((the Flow of M) \/ (the Flow of M)~) \/ id(the Places of M)
proof
f_prox(M) \/ (f_prox(M))~ = ((R \/ S) \/ T) \/ (f_prox(M))~ by Def12
.= ((R \/ S) \/ T) \/ ((R \/ S) \/ T)~ by Def12
.= ((R \/ S) \/ T) \/ ((R \/ S)~ \/ T~) by RELAT_1:40
.= (((R \/ S) \/ T) \/ (R \/ S)~) \/ T~ by XBOOLE_1:4
.= (((R \/ S) \/ (R \/ S)~) \/ T) \/ T~ by XBOOLE_1:4
.= ((R \/ S) \/ (R \/ S)~) \/ (T \/ T~) by XBOOLE_1:4
.= ((R \/ S) \/ (R \/ S)~) \/ (T \/ T) by RELAT_1:72
.= ((the Flow of M) \/ (the Flow of M)~) \/
id(the Places of M) by A5;
hence thesis;
end;
A7:id(the Places of M) c= id(Elements(M))
proof
the Places of M c= Elements(M) by NET_1:4;
hence thesis by SYSREL:33;
end;
A8:f_prox(M) * f_prox(M) = f_prox(M) * ((R \/ S) \/ T) by Def12
.= (((R \/ S) \/ T) * ((R \/ S) \/ T)) by Def12
.= (((R \/ S) \/ T) * (R \/ S)) \/
(((R \/ S) \/ T) * T) by SYSREL:20
.= ((((R \/ S) \/ T) * R ) \/ (((R \/ S) \/ T) * S)) \/
(((R \/ S) \/ T) * T) by SYSREL:20
.= (((R \/ S) * R ) \/ (T * R )) \/
(((R \/ S) \/ T) * S) \/
(((R \/ S) \/ T) * T) by SYSREL:20
.= (((R * R) \/ (S * R)) \/ (T * R )) \/
(((R \/ S) \/ T) * S) \/
(((R \/ S) \/ T) * T) by SYSREL:20
.= (((R * R) \/ (S * R)) \/ (T * R )) \/
(((R \/ S) * S) \/ (T * S)) \/
(((R \/ S) \/ T) * T) by SYSREL:20
.= (((R * R) \/ (S * R)) \/ (T * R )) \/
(((R * S) \/ (S * S)) \/ (T * S)) \/
(((R \/ S) \/ T) * T) by SYSREL:20
.= (((R * R) \/ (S * R)) \/ (T * R )) \/
(((R * S) \/ (S * S)) \/ (T * S)) \/
(((R \/ S) * T) \/ (T * T)) by SYSREL:20
.= (((R * R) \/ (S * R)) \/ (T * R )) \/
(((R * S) \/ (S * S)) \/ (T * S)) \/
(((R * T) \/ (S * T)) \/ (T * T)) by SYSREL:20
.= (({} \/ (S * R)) \/ (T * R )) \/
(((R * S) \/ (S * S)) \/ (T * S)) \/
(((R * T) \/ (S * T)) \/ (T * T)) by Th16
.= (({} \/ {}) \/ (T * R )) \/
(((R * S) \/ (S * S)) \/ (T * S)) \/
(((R * T) \/ (S * T)) \/ (T * T)) by Th16
.= (({} \/ {}) \/ (T * R )) \/
(({} \/ (S * S)) \/ (T * S)) \/
(((R * T) \/ (S * T)) \/ (T * T)) by Th16
.= (T * R ) \/ ({} \/ (T * S)) \/
(((R * T) \/ (S * T)) \/ (T * T)) by Th16
.= R \/ (T * S) \/
(((R * T) \/ (S * T)) \/ (T * T)) by Th17
.= R \/ S \/ (((R * T) \/ (S * T)) \/ (T * T)) by Th17
.= R \/ S \/ (((R * T) \/ (S * T)) \/ T) by SYSREL:29
.= R \/ S \/ (({} \/ (S * T)) \/ T) by Th17
.= R \/ S \/ ({} \/ T) by Th17
.= f_prox(M) by Def12;
A9: (f_prox(M) \ id(Elements(M))) * f_prox(M) =
(f_prox(M) \ id(Elements(M))) * ((R \/ S) \/ T) by Def12
.= (R \/ S) * ((R \/ S) \/ T) by A1,Def12
.= {} \/ ((R \/ S) * T) by A2,SYSREL:20
.= (R * T) \/ (S * T) by SYSREL:20
.= {} \/ (S * T) by Th17
.= {} by Th17;
(f_prox(M) \/ (f_prox(M))~) \/ id(Elements(M)) =
(((the Flow of M) \/ (the Flow of M)~) \/ (id(the Places of M) \/
id(Elements(M)))) by A6,XBOOLE_1:4
.= (((the Flow of M) \/ (the Flow of M)~) \/ id(Elements(M)))
by A7,XBOOLE_1:12
.= ((the Flow of M) \/ id(Elements(M))) \/
((the Flow of M)~ \/ id(Elements(M))) by XBOOLE_1:5
.= ((the Flow of M) \/ id(Elements(M))) \/
((the Flow of M)~ \/ (id(Elements(M)))~) by RELAT_1:72
.= ((the Flow of M) \/ id(Elements(M))) \/
((the Flow of M) \/ id(Elements(M)))~ by RELAT_1:40
.= f_flow(M) \/
((the Flow of M) \/ id(Elements(M)))~ by Def13
.= f_flow(M) \/ (f_flow(M))~ by Def13;
hence thesis by A8,A9;
end;
::C [F ->P]
definition let M;
func f_places(M) -> set equals
:Def14: the Places of M;
correctness;
func f_transitions(M) -> set equals
:Def15: the Transitions of M;
correctness;
func f_pre(M) -> Relation equals
:Def16: (the Flow of M)|(the Transitions of M);
correctness;
func f_post(M) -> Relation equals
:Def17: (the Flow of M)~|(the Transitions of M);
correctness;
end;
theorem
f_pre(M) c= [:f_transitions(M),f_places(M):] &
f_post(M) c= [:f_transitions(M),f_places(M):]
proof
A1: for x,y holds [x,y] in f_pre(M) implies
[x,y] in [:f_transitions(M),f_places(M):]
proof
let x,y;
assume [x,y] in f_pre(M);
then [x,y] in (the Flow of M)|(the Transitions of M) by Def16;
then x in (the Transitions of M) & [x,y] in (the Flow of M) by RELAT_1:def 11
;
then x in f_transitions(M) & y in (the Places of M) by Def15,Th11;
then x in f_transitions(M) & y in f_places(M) by Def14;
hence thesis by ZFMISC_1:106;
end;
for x,y holds [x,y] in f_post(M) implies
[x,y] in [:f_transitions(M),f_places(M):]
proof
let x,y;
assume [x,y] in f_post(M);
then [x,y] in (the Flow of M)~|(the Transitions of M) by Def17;
then x in (the Transitions of M) & [x,y] in (the Flow of M)~ by RELAT_1:def
11;
then x in (the Transitions of M) & [y,x] in (the Flow of M) by RELAT_1:def 7
;
then x in f_transitions(M) & y in (the Places of M) by Def15,Th11;
then x in f_transitions(M) & y in f_places(M) by Def14;
hence thesis by ZFMISC_1:106;
end;
hence thesis by A1,RELAT_1:def 3;
end;
theorem
f_places(M) misses f_transitions(M)
proof
f_places(M) = the Places of M &
f_transitions(M) = the Transitions of M by Def14,Def15;
hence thesis by NET_1:def 1;
end;
theorem
f_prox(M) c= [:Elements(M), Elements(M):] &
f_flow(M) c= [:Elements(M), Elements(M):]
proof
thus f_prox(M) c= [:Elements(M), Elements(M):]
proof
A1:(the Flow of M)|(the Places of M) c= the Flow of M by RELAT_1:88;
the Flow of M c= [:Elements(M), Elements(M):] by Th13;
then A2:(the Flow of M)|(the Places of M) c= [:Elements(M), Elements(M):]
by A1,XBOOLE_1:1;
A3:(the Flow of M)~|(the Places of M) c= (the Flow of M)~ by RELAT_1:88;
(the Flow of M)~ c= [:Elements(M), Elements(M):] by Th13;
then A4:(the Flow of M)~|(the Places of M) c= [:Elements(M), Elements(M):]
by A3,XBOOLE_1:1;
the Places of M c= Elements(M) by NET_1:4;
then A5:[:the Places of M, the Places of M:] c=
[:Elements(M), Elements(M):] by ZFMISC_1:119;
id(the Places of M) c= [:the Places of M, the Places of M:]
by RELSET_1:28;
then A6:id(the Places of M) c= [:Elements(M), Elements(M):]
by A5,XBOOLE_1:1;
(the Flow of M)|(the Places of M) \/
(the Flow of M)~|(the Places of M) c= [:Elements(M), Elements(M):]
by A2,A4,XBOOLE_1:8;
then ((the Flow of M)|(the Places of M) \/
(the Flow of M)~|(the Places of M)) \/
id(the Places of M) c= [:Elements(M), Elements(M):]
by A6,XBOOLE_1:8;
hence thesis by Def12;
end;
A7:the Flow of M c= [:Elements(M), Elements(M):] by Th13;
id(Elements(M)) c= [:Elements(M), Elements(M):] by RELSET_1:28;
then (the Flow of M) \/ id(Elements(M)) c= [:Elements(M), Elements(M)
:]
by A7,XBOOLE_1:8;
hence thesis by Def13;
end;
::A [F -> E]
definition let M;
func f_entrance(M) -> Relation equals :Def18:
((the Flow of M)~|(the Places of M)) \/ id(the Transitions of M);
correctness;
func f_escape(M) -> Relation equals :Def19:
((the Flow of M)|(the Places of M)) \/ id(the Transitions of M);
correctness;
end;
theorem
f_escape(M) c= [:Elements(M),Elements(M):] &
f_entrance(M) c= [:Elements(M),Elements(M):]
proof
thus f_escape(M) c= [:Elements(M),Elements(M):]
proof
A1:id(the Transitions of M) c= [:Elements(M),Elements(M):]
proof
(the Transitions of M) c= Elements(M) by NET_1:5;
then A2: id(the Transitions of M) c= id(Elements(M))
by SYSREL:33;
id(Elements(M)) c= [:Elements(M),Elements(M):] by RELSET_1:28;
hence thesis by A2,XBOOLE_1:1;
end;
A3:(the Flow of M)|(the Places of M) c= (the Flow of M) by RELAT_1:88;
(the Flow of M) c= [:Elements(M),Elements(M):] by Th13;
then (the Flow of M)|(the Places of M) c= [:Elements(M),Elements(M):]
by A3,XBOOLE_1:1;
then ((the Flow of M)|(the Places of M)) \/
id(the Transitions of M) c= [:Elements(M),Elements(M):]
by A1,XBOOLE_1:8;
hence thesis by Def19;
end;
A4:id(the Transitions of M) c= [:Elements(M),Elements(M):]
proof
(the Transitions of M) c= Elements(M) by NET_1:5;
then A5: id(the Transitions of M) c= id(Elements(M))
by SYSREL:33;
id(Elements(M)) c= [:Elements(M),Elements(M):] by RELSET_1:28;
hence thesis by A5,XBOOLE_1:1;
end;
A6:(the Flow of M)~|(the Places of M) c= (the Flow of M)~ by RELAT_1:88;
(the Flow of M)~ c= [:Elements(M),Elements(M):] by Th13;
then (the Flow of M)~|(the Places of M) c= [:Elements(M),Elements(M):]
by A6,XBOOLE_1:1;
then ((the Flow of M)~|(the Places of M)) \/
id(the Transitions of M) c= [:Elements(M),Elements(M):]
by A4,XBOOLE_1:8;
hence thesis by Def18;
end;
theorem
dom(f_escape(M)) c= Elements(M) & rng(f_escape(M)) c= Elements(M) &
dom(f_entrance(M)) c= Elements(M) & rng(f_entrance(M)) c= Elements(M)
proof
A1: for x holds x in dom(f_escape(M)) implies x in Elements(M)
proof
let x;
assume x in dom(f_escape(M));
then x in dom(((the Flow of M)|(the Places of M)) \/
id(the Transitions of M)) by Def19;
then x in dom((the Flow of M)|(the Places of M)) \/
dom(id(the Transitions of M)) by RELAT_1:13;
then x in dom((the Flow of M)|(the Places of M)) or
x in dom(id(the Transitions of M)) by XBOOLE_0:def 2;
then x in (the Places of M) or x in the Transitions of M by RELAT_1:71,86;
then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
hence thesis by NET_1:def 2;
end;
A2: for x holds x in rng(f_escape(M)) implies x in Elements(M)
proof
let x;
assume x in rng(f_escape(M));
then x in rng(((the Flow of M)|(the Places of M)) \/
id(the Transitions of M)) by Def19;
then A3: x in rng((the Flow of M)|(the Places of M)) \/
rng(id(the Transitions of M)) by RELAT_1:26;
A4:x in rng((the Flow of M)|(the Places of M)) implies thesis
proof
assume x in rng((the Flow of M)|(the Places of M));
then consider y such that A5:[y,x] in (the Flow of M)|(the Places of M) by
RELAT_1:def 5;
y in (the Places of M) & [y,x] in (the Flow of M) by A5,RELAT_1:def 11;
then x in (the Places of M) or x in the Transitions of M by Th11;
then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
hence thesis by NET_1:def 2;
end;
x in rng(id(the Transitions of M)) implies thesis
proof
assume x in rng(id(the Transitions of M));
then x in (the Places of M) or x in the Transitions of M by RELAT_1:71;
then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
hence thesis by NET_1:def 2;
end;
hence thesis by A3,A4,XBOOLE_0:def 2;
end;
A6: for x holds x in dom(f_entrance(M)) implies x in Elements(M)
proof
let x;
assume x in dom(f_entrance(M));
then x in dom(((the Flow of M)~|(the Places of M)) \/
id(the Transitions of M)) by Def18;
then x in dom((the Flow of M)~|(the Places of M)) \/
dom(id(the Transitions of M)) by RELAT_1:13;
then x in dom((the Flow of M)~|(the Places of M)) or
x in dom(id(the Transitions of M)) by XBOOLE_0:def 2;
then x in (the Places of M) or x in the Transitions of M by RELAT_1:71,86;
then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
hence thesis by NET_1:def 2;
end;
for x holds x in rng(f_entrance(M)) implies x in Elements(M)
proof
let x;
assume x in rng(f_entrance(M));
then x in rng(((the Flow of M)~|(the Places of M)) \/
id(the Transitions of M)) by Def18;
then A7: x in rng((the Flow of M)~|(the Places of M)) \/
rng(id(the Transitions of M)) by RELAT_1:26;
A8:x in rng((the Flow of M)~|(the Places of M)) implies thesis
proof
assume x in rng((the Flow of M)~|(the Places of M));
then consider y such that A9:
[y,x] in (the Flow of M)~|(the Places of M) by
RELAT_1:def 5;
y in (the Places of M) & [y,x] in (the Flow of M)~ by A9,RELAT_1:def 11;
then y in (the Places of M) & [x,y] in (the Flow of M) by RELAT_1:def 7;
then x in (the Places of M) or x in the Transitions of M by Th11;
then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
hence thesis by NET_1:def 2;
end;
x in rng(id(the Transitions of M)) implies thesis
proof
assume x in rng(id(the Transitions of M));
then x in (the Places of M) or x in the Transitions of M by RELAT_1:71;
then x in (the Places of M) \/ (the Transitions of M) by XBOOLE_0:def 2;
hence thesis by NET_1:def 2;
end;
hence thesis by A7,A8,XBOOLE_0:def 2;
end;
hence thesis by A1,A2,A6,TARSKI:def 3;
end;
theorem
(f_escape(M)) * (f_escape(M)) = f_escape(M) &
(f_escape(M)) * (f_entrance(M)) = f_escape(M) &
(f_entrance(M)) * (f_entrance(M)) =f_entrance(M) &
(f_entrance(M)) * (f_escape(M)) = f_entrance(M)
proof
set R = ((the Flow of M)|(the Places of M));
set S = id(the Transitions of M);
A1:(f_escape(M)) * (f_escape(M)) = f_escape(M)
proof
A2: S * R = {} by Th17;
A3: R * S = R by Th17;
A4: S * S = S by SYSREL:29;
(f_escape(M)) * (f_escape(M)) = (R \/ S) * (f_escape(M)) by Def19
.= (R \/ S) * (R \/ S) by Def19
.= (R * (R \/ S)) \/ (S * (R \/ S)) by SYSREL:20
.= ((R * R) \/ (R * S)) \/ (S * (R \/ S))
by RELAT_1:51
.= ((R * R) \/ (R * S)) \/ ((S * R) \/ (S * S))
by RELAT_1:51
.= ({} \/ R) \/ ({} \/ S) by A2,A3,A4,Th16
.=f_escape(M) by Def19;
hence thesis;
end;
A5:(f_escape(M)) * (f_entrance(M)) = f_escape(M)
proof
set T = ((the Flow of M)~|(the Places of M));
A6: S * T = {} by Th17;
A7: R * S = R by Th17;
A8: S * S = S by SYSREL:29;
(f_escape(M)) * (f_entrance(M)) = (R \/ S) * (f_entrance(M)) by Def19
.= (R \/ S) * (T \/ S) by Def18
.= (R * (T \/ S)) \/ (S * (T \/ S)) by SYSREL:20
.= ((R * T) \/ (R * S)) \/ (S * (T \/ S))
by RELAT_1:51
.= ((R * T) \/ (R * S)) \/ ((S * T) \/ (S * S))
by RELAT_1:51
.= ({} \/ R) \/ ({} \/ S) by A6,A7,A8,Th16
.=f_escape(M) by Def19;
hence thesis;
end;
A9:(f_entrance(M)) * (f_entrance(M)) = f_entrance(M)
proof
set R = ((the Flow of M)~|(the Places of M));
A10: S * R = {} by Th17;
A11: R * S = R by Th17;
A12: S * S = S by SYSREL:29;
(f_entrance(M)) * (f_entrance(M)) = (R \/ S) * (f_entrance(M)) by Def18
.= (R \/ S) * (R \/ S) by Def18
.= (R * (R \/ S)) \/ (S * (R \/ S)) by SYSREL:20
.= ((R * R) \/ (R * S)) \/ (S * (R \/ S))
by RELAT_1:51
.= ((R * R) \/ (R * S)) \/ ((S * R) \/ (S * S))
by RELAT_1:51
.= ({} \/ R) \/ ({} \/ S) by A10,A11,A12,Th16
.=f_entrance(M) by Def18;
hence thesis;
end;
(f_entrance(M)) * (f_escape(M)) = f_entrance(M)
proof
set T = ((the Flow of M)~|(the Places of M));
A13: T * S = T by Th17;
A14: S * R = {} by Th17;
A15: S * S = S by SYSREL:29;
(f_entrance(M)) * (f_escape(M)) = (T \/ S) * (f_escape(M)) by Def18
.= (T \/ S) * (R \/ S) by Def19
.= (T * (R \/ S)) \/ (S * (R \/ S)) by SYSREL:20
.= ((T * R) \/ (T * S)) \/ (S * (R \/ S))
by RELAT_1:51
.= ((T * R) \/ (T * S)) \/ ((S * R) \/ (S * S))
by RELAT_1:51
.= ({} \/ T) \/ ({} \/ S) by A13,A14,A15,Th16
.=f_entrance(M) by Def18;
hence thesis;
end;
hence thesis by A1,A5,A9;
end;
theorem
(f_escape(M)) * (f_escape(M) \ id(Elements(M))) = {} &
(f_entrance(M)) * (f_entrance(M) \ id(Elements(M))) = {}
proof
set R = (the Flow of M)|(the Places of M);
set S = id(the Transitions of M);
thus (f_escape(M)) * (f_escape(M) \ id(Elements(M))) = {}
proof
A1: S * R = {} by Th17;
(f_escape(M)) * (f_escape(M) \ id(Elements(M))) =
(R \/ S) * (f_escape(M) \ id(Elements(M)))
by Def19
.= (R \/ S) * ((R \/ S) \ (id(Elements(M)))) by Def19
.= (R \/ S) * R by Th19
.= (R * R) \/ (S * R) by SYSREL:20
.= {} by A1,Th16;
hence thesis;
end;
set R = ((the Flow of M)~|(the Places of M));
A2: S * R = {} by Th17;
(f_entrance(M)) * (f_entrance(M) \ id(Elements(M))) =
(R \/ S) * (f_entrance(M) \ id(Elements(M)))
by Def18
.= (R \/ S) * ((R \/ S) \ (id(Elements(M)))) by Def18
.= (R \/ S) * R by Th19
.= (R * R) \/ (S * R) by SYSREL:20
.= {} by A2,Th16;
hence thesis;
end;
::B [F ->R]
definition let M;
func f_adjac(M) -> Relation equals
:Def20: ((the Flow of M)|(the Transitions of M) \/
(the Flow of M)~|(the Transitions of M)) \/
id(the Transitions of M);
correctness;
redefine func f_flow(M);
synonym f_circulation(M);
end;
theorem
f_adjac(M) * f_adjac(M) = f_adjac(M) &
(f_adjac(M) \ id(Elements(M))) * f_adjac(M) = {} &
(f_adjac(M) \/ ((f_adjac(M))~)) \/ id(Elements(M)) =
f_circulation(M) \/
(f_circulation(M))~
proof
set R = (the Flow of M)|(the Transitions of M);
set S = (the Flow of M)~|(the Transitions of M);
set T = id(the Transitions of M);
set Q = id(Elements(M));
A1:((R \/ S) \/ T) \ Q = R \/ S
proof
((R \/ S) \/ T) \ Q = ((R \/ T) \/ (S \/ T)) \ Q by XBOOLE_1:5
.= ((R \/ T) \ (id(Elements(M))) \/
((S \/ T) \ (id(Elements(M))))) by XBOOLE_1:42
.= R \/
((S \/ T) \ (id(Elements(M)))) by Th19
.= R \/ S by Th19;
hence thesis;
end;
A2:(R \/ S) * (R \/ S) = {}
proof
(R \/ S) * (R \/ S) = ((R \/ S) * R) \/ ((R \/ S) *S) by SYSREL:20
.= ((R * R) \/ (S * R)) \/ ((R \/ S) *S) by SYSREL:20
.= ((R * R) \/ (S * R)) \/ ((R * S) \/ (S *S)) by SYSREL:20
.= ({} \/ (S * R)) \/ ((R * S) \/ (S *S)) by Th16
.= ({} \/ {}) \/ ((R * S) \/ (S *S)) by Th16
.= ({} \/ {}) \/ ({} \/ (S *S)) by Th16
.= {} by Th16;
hence thesis;
end;
A3:R \/ S~ = the Flow of M & R~ \/ S = (the Flow of M)~
proof
A4:R \/ S~ = R \/ (((the Flow of M)|(the Places of M))~)~ by Th20
.= the Flow of M by Th21;
R~ \/ S = R~ \/ ((the Flow of M)|(the Places of M))~ by Th20
.= (the Flow of M)~ by Th21;
hence thesis by A4;
end;
A5:(R \/ S)~ \/ (R \/ S) = (the Flow of M) \/ (the Flow of M)~
proof
(R \/ S)~ \/ (R \/ S) = (R~ \/ S~) \/ (R \/ S) by RELAT_1:40
.= (R~ \/ (S \/ R)) \/ S~ by XBOOLE_1:4
.= ((R~ \/ S) \/ R) \/ S~ by XBOOLE_1:4
.= (the Flow of M) \/ (the Flow of M)~ by A3,XBOOLE_1:4;
hence thesis;
end;
A6:f_adjac(M) \/ (f_adjac(M))~ =
((the Flow of M) \/ (the Flow of M)~) \/ id(the Transitions of M)
proof
f_adjac(M) \/ (f_adjac(M))~ = ((R \/ S) \/ T) \/ (f_adjac(M))~ by Def20
.= ((R \/ S) \/ T) \/ ((R \/ S) \/ T)~ by Def20
.= ((R \/ S) \/ T) \/ ((R \/ S)~ \/ T~) by RELAT_1:40
.= (((R \/ S) \/ T) \/ (R \/ S)~) \/ T~ by XBOOLE_1:4
.= (((R \/ S) \/ (R \/ S)~) \/ T) \/ T~ by XBOOLE_1:4
.= ((R \/ S) \/ (R \/ S)~) \/ (T \/ T~) by XBOOLE_1:4
.= ((R \/ S) \/ (R \/ S)~) \/ (T \/ T) by RELAT_1:72
.= ((the Flow of M) \/ (the Flow of M)~) \/
id(the Transitions of M) by A5;
hence thesis;
end;
A7:id(the Transitions of M) c= id(Elements(M))
proof
the Transitions of M c= Elements(M) by NET_1:5;
hence thesis by SYSREL:33;
end;
A8:f_adjac(M) * f_adjac(M) = f_adjac(M) * ((R \/ S) \/ T) by Def20
.= (((R \/ S) \/ T) * ((R \/ S) \/ T)) by Def20
.= (((R \/ S) \/ T) * (R \/ S)) \/ (((R \/ S) \/ T) * T) by SYSREL:20
.= ((((R \/ S) \/ T) * R ) \/ (((R \/ S) \/ T) * S)) \/
(((R \/ S) \/ T) * T) by SYSREL:20
.= (((R \/ S) * R ) \/ (T * R )) \/ (((R \/ S) \/ T) * S) \/
(((R \/ S) \/ T) * T) by SYSREL:20
.= (((R * R) \/ (S * R)) \/ (T * R )) \/ (((R \/ S) \/ T) * S) \/
(((R \/ S) \/ T) * T) by SYSREL:20
.= (((R * R) \/ (S * R)) \/ (T * R )) \/ (((R \/ S) * S) \/ (T * S)) \/
(((R \/ S) \/ T) * T) by SYSREL:20
.= (((R * R) \/ (S * R)) \/ (T * R )) \/ (((R * S) \/ (S * S)) \/ (T * S))
\/
(((R \/ S) \/ T) * T) by SYSREL:20
.= (((R * R) \/ (S * R)) \/ (T * R )) \/ (((R * S) \/ (S * S)) \/ (T * S))
\/
(((R \/ S) * T) \/ (T * T)) by SYSREL:20
.= (((R * R) \/ (S * R)) \/ (T * R )) \/ (((R * S) \/ (S * S)) \/ (T * S))
\/
(((R * T) \/ (S * T)) \/ (T * T)) by SYSREL:20
.= (({} \/ (S * R)) \/ (T * R )) \/ (((R * S) \/ (S * S)) \/ (T * S)) \/
(((R * T) \/ (S * T)) \/ (T * T)) by Th16
.= (({} \/ {}) \/ (T * R )) \/ (((R * S) \/ (S * S)) \/ (T * S)) \/
(((R * T) \/ (S * T)) \/ (T * T)) by Th16
.= (({} \/ {}) \/ (T * R )) \/ (({} \/ (S * S)) \/ (T * S)) \/
(((R * T) \/ (S * T)) \/ (T * T)) by Th16
.= (T * R ) \/ ({} \/ (T * S)) \/ (((R * T) \/ (S * T)) \/ (T * T)) by Th16
.= R \/ (T * S) \/ (((R * T) \/ (S * T)) \/ (T * T)) by Th17
.= R \/ S \/ (((R * T) \/ (S * T)) \/ (T * T)) by Th17
.= R \/ S \/ (((R * T) \/ (S * T)) \/ T) by SYSREL:29
.= R \/ S \/ (({} \/ (S * T)) \/ T) by Th17
.= R \/ S \/ ({} \/ T) by Th17
.= f_adjac(M) by Def20;
A9: (f_adjac(M) \ id(Elements(M))) * f_adjac(M) =
(f_adjac(M) \ id(Elements(M))) * ((R \/ S) \/ T) by Def20
.= (R \/ S) * ((R \/ S) \/ T) by A1,Def20
.= {} \/ ((R \/ S) * T) by A2,SYSREL:20
.= (R * T) \/ (S * T) by SYSREL:20
.= {} \/ (S * T) by Th17
.= {} by Th17;
(f_adjac(M) \/ (f_adjac(M))~) \/ id(Elements(M)) =
(((the Flow of M) \/ (the Flow of M)~) \/
(id(the Transitions of M) \/ id(Elements(M)))) by A6,XBOOLE_1:4
.= (((the Flow of M) \/ (the Flow of M)~) \/ id(Elements(M)))
by A7,XBOOLE_1:12
.= ((the Flow of M) \/ id(Elements(M))) \/
((the Flow of M)~ \/ id(Elements(M))) by XBOOLE_1:5
.= ((the Flow of M) \/ id(Elements(M))) \/
((the Flow of M)~ \/ (id(Elements(M)))~) by RELAT_1:72
.= ((the Flow of M) \/ id(Elements(M))) \/
((the Flow of M) \/ id(Elements(M)))~ by RELAT_1:40
.= f_circulation(M) \/
((the Flow of M) \/ id(Elements(M)))~ by Def13
.= f_circulation(M) \/ (f_circulation(M))~ by Def13;
hence thesis by A8,A9;
end;