:: Definitions of Petri Net - Part II
:: by Waldemar Korczy\'nski
::
:: Received January 31, 1992
:: Copyright (c) 1992-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies STRUCT_0, RELAT_1, TARSKI, ZFMISC_1, XBOOLE_0, SYSREL, E_SIEC;
notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, SYSREL, STRUCT_0;
constructors SYSREL, STRUCT_0, XTUPLE_0;
registrations XBOOLE_0, RELAT_1;
requirements SUBSET, BOOLE;
equalities STRUCT_0;
theorems ZFMISC_1, RELAT_1, SYSREL, RELSET_1, XBOOLE_0, XBOOLE_1, XTUPLE_0;
begin
reserve x,y,z for object,X,Y for set;
definition
struct (1-sorted) G_Net (# carrier -> set, entrance, escape -> Relation #);
end;
definition
let IT be G_Net;
attr IT is GG means :Def1:
the entrance of IT c= [:the carrier of IT,the carrier of IT:] &
the escape of IT c= [:the carrier of IT,the carrier of IT:] &
(the entrance of IT) * (the entrance of IT) = the entrance of IT &
(the entrance of IT) * (the escape of IT) = the entrance of IT &
(the escape of IT) * (the escape of IT) = the escape of IT &
(the escape of IT) * (the entrance of IT) = the escape of IT;
end;
registration
cluster GG for G_Net;
existence
proof
take N = G_Net (# {}, {}, {} #);
the escape of N c= [:the carrier of N,the carrier of N:] & (the
entrance of N) * (the entrance of N) = {} by XBOOLE_1:2;
hence thesis;
end;
end;
definition
mode gg_net is GG G_Net;
end;
definition
let IT be G_Net;
attr IT is EE means
:Def2:
(the entrance of IT) * ((the entrance of IT) \ id the carrier of IT) = {} &
(the escape of IT) * ((the escape of IT) \ id the carrier of IT) = {};
end;
registration
cluster EE for G_Net;
existence
proof
take N = G_Net (# {}, {}, {} #);
thus thesis;
end;
end;
registration
cluster strict GG EE for G_Net;
existence
proof
take N = G_Net (# {} , {} , {} #);
the entrance of N c= [:the carrier of N,the carrier of N:] &
(the escape of N) * ((the escape of N) \ id N) = {}
by XBOOLE_1:2;
hence thesis;
end;
end;
definition
mode e_net is EE GG G_Net;
end;
reserve N for e_net;
theorem
for R, S being Relation holds G_Net (# X, R, S #) is e_net iff
R c= [:X,X:] & S c= [:X,X:] & R * R = R & R * S = R &
S * S = S & S * R = S & R * (R \ id X) = {} & S * (S \ id X) = {}
by Def1,Def2;
theorem Th2:
G_Net (# X, {}, {} #) is e_net
proof
{} c= [:X, X:] & {} * ({} \ id(X)) = {} by XBOOLE_1:2;
hence thesis by Def1,Def2;
end;
theorem Th3:
G_Net (# X, id X, id X #) is e_net
proof
A1: id(X) * (id(X) \ id(X)) = id(X) * {} by XBOOLE_1:37
.= {};
id(X) c= [:X, X:] & id(X) * id(X) = id(X) by RELSET_1:13,SYSREL:12;
hence thesis by A1,Def1,Def2;
end;
theorem
G_Net (# {}, {}, {} #) is e_net by Th2;
theorem
G_Net (# X, id(X \ Y), id(X \ Y) #) is e_net
proof
A1: id(X \ Y) * (id(X \ Y) \ id X) = id(X \ Y) * {} by SYSREL:16
.= {};
X \ Y c= X by XBOOLE_1:36; then
A2: [:X \ Y, X \ Y:] c= [:X, X:] by ZFMISC_1:96;
id(X \ Y) c= [:X \ Y, X \ Y:] by RELSET_1:13; then
A3: id(X \ Y) c= [:X, X:] by A2,XBOOLE_1:1;
id(X \ Y) * id(X \ Y) = id(X \ Y) by SYSREL:12;
hence thesis by A3,A1,Def1,Def2;
end;
definition
func empty_e_net -> strict e_net equals
G_Net (# {}, {}, {} #);
correctness by Th2;
end;
definition
let X;
func Tempty_e_net X -> strict e_net equals
G_Net (# X, id X, id X #);
coherence by Th3;
func Pempty_e_net(X) -> strict e_net equals
G_Net (# X, {}, {} #);
coherence by Th2;
end;
theorem
the carrier of Tempty_e_net(X) = X & the entrance of Tempty_e_net(X) = id X &
the escape of Tempty_e_net(X) = id X;
theorem
the carrier of Pempty_e_net(X) = X & the entrance of Pempty_e_net(X) = {} &
the escape of Pempty_e_net(X) = {};
definition
let x;
func Psingle_e_net(x) -> strict e_net equals
G_Net (#{x}, id{x}, id{x}#);
coherence by Th3;
func Tsingle_e_net(x) -> strict e_net equals
G_Net (# {x}, {}, {} #);
coherence by Th2;
end;
theorem
the carrier of Psingle_e_net(x) = {x} &
the entrance of Psingle_e_net(x) = id{x} &
the escape of Psingle_e_net(x) = id{x};
theorem
the carrier of Tsingle_e_net(x) = {x} &
the entrance of Tsingle_e_net(x) = {} &
the escape of Tsingle_e_net(x) = {};
theorem Th10:
G_Net (# X \/ Y, id X, id X #) is e_net
proof
X c= X \/ Y by XBOOLE_1:7;
then id(X) c= [:X, X:] & [:X, X:] c= [:X \/ Y, X \/ Y:] by RELSET_1:13
,ZFMISC_1:96; then
A1: id(X) c= [:X \/ Y, X \/ Y:] by XBOOLE_1:1;
id(X) c= id(X) \/ id(Y) by XBOOLE_1:7;
then id(X) c= id(X \/ Y) by SYSREL:14; then
A2: id(X) * (id(X) \ id(X \/ Y)) = id(X) * {} by XBOOLE_1:37
.= {};
id(X) * id(X) = id(X) by SYSREL:12;
hence thesis by A1,A2,Def1,Def2;
end;
definition
let X,Y;
func PTempty_e_net(X,Y) -> strict e_net equals
G_Net (#X \/ Y, id(X), id(X)#);
coherence by Th10;
end;
theorem Th11:
(the entrance of N) \ id(dom(the entrance of N)) =
(the entrance of N) \ id the carrier of N &
(the escape of N) \ id(dom(the escape of N)) =
(the escape of N) \ id the carrier of N &
(the entrance of N) \ id(rng(the entrance of N)) =
(the entrance of N) \ id the carrier of N &
(the escape of N) \ id(rng(the escape of N)) =
(the escape of N) \ id the carrier of N
proof
the entrance of N c= [:the carrier of N,the carrier of N:] & the escape
of N c= [:the carrier of N,the carrier of N:] by Def1;
hence thesis by SYSREL:20;
end;
theorem Th12:
CL the entrance of N = CL the escape of N
proof
(the escape of N) * ((the escape of N) \ id N) = {} by Def2; then
A1: (the escape of N) * ((the escape of N) \ id dom the escape of N) = {}
by Th11;
(the entrance of N) * ((the entrance of N) \ id N) = {} by Def2; then
A2: (the entrance of N) * ((the entrance of N) \ id dom the entrance of N
) = {} by Th11;
(the entrance of N) * (the escape of N) = the entrance of N &
(the escape of N) * (the entrance of N) = the escape of N by Def1;
hence thesis by A1,A2,SYSREL:40;
end;
theorem Th13:
rng (the entrance of N) = rng (CL(the entrance of N)) &
rng (the entrance of N) = dom (CL(the entrance of N)) &
rng (the escape of N) = rng (CL(the escape of N)) &
rng (the escape of N) = dom (CL(the escape of N)) &
rng the entrance of N = rng the escape of N
proof
(the entrance of N) * ((the entrance of N) \ id(the carrier of N)) = {}
by Def2; then
A1: (the entrance of N) * ((the entrance of N) \ id(dom (the entrance of N))
) = {} by Th11;
(the escape of N) * ((the escape of N) \ id(the carrier of N)) = {} by Def2;
then
A2: (the escape of N) * ((the escape of N) \ id(dom(the escape of N))) = {}
by Th11;
A3: (the escape of N) * (the escape of N) = the escape of N by Def1; then
A4: rng (the escape of N) = rng (CL(the escape of N)) by A2,SYSREL:31;
A5: (the entrance of N) * (the entrance of N) = the entrance of N by Def1;
then rng (the entrance of N) = rng (CL(the entrance of N)) by A1,SYSREL:31;
hence thesis by A5,A1,A3,A2,A4,Th12,SYSREL:31;
end;
theorem Th14:
dom (the entrance of N) c= the carrier of N & rng (the entrance
of N) c= the carrier of N & dom (the escape of N) c= the carrier of N & rng (
the escape of N) c= the carrier of N
proof
the entrance of N c= [:the carrier of N,the carrier of N:] & the escape
of N c= [:the carrier of N,the carrier of N:] by Def1;
hence thesis by SYSREL:3;
end;
theorem Th15:
(the entrance of N) * ((the escape of N) \ id the carrier of N) = {} &
(the escape of N) * ((the entrance of N) \ id the carrier of N) = {}
proof
set R = the entrance of N;
set S = the escape of N;
set T = id the carrier of N;
A1: S * (R \ T) = S * (R \ id dom R) by Th11
.= (S * R) * (R \ id dom R) by Def1
.= S * (R * (R \ id dom R)) by RELAT_1:36
.= S * (R * (R \ T)) by Th11
.= S * {} by Def2
.= {};
R * (S \ T) = R * (S \ id dom S) by Th11
.= (R * S) * (S \ id dom S) by Def1
.= R * (S * (S \ id dom S)) by RELAT_1:36
.= R * (S * (S \ T)) by Th11
.= R * {} by Def2
.= {};
hence thesis by A1;
end;
theorem
((the entrance of N) \ id(the carrier of N)) *
((the entrance of N) \ id(the carrier of N)) = {} &
((the escape of N) \ id(the carrier of N)) *
((the escape of N) \ id(the carrier of N)) = {} &
((the entrance of N) \ id(the carrier of N)) *
((the escape of N) \ id(the carrier of N)) = {} &
((the escape of N) \ id(the carrier of N)) *
((the entrance of N) \ id(the carrier of N)) = {}
proof
set R = the entrance of N;
set S = the escape of N;
set T = id(the carrier of N);
(R \ T) * (S \ T) c= R * (S \ T) by RELAT_1:30,XBOOLE_1:36; then
A1: (R \ T) * (S \ T) c= {} by Th15;
(S \ T) * (S \ T) c= S * (S \ T) by RELAT_1:30,XBOOLE_1:36; then
A2: (S \ T) * (S \ T) c= {} by Def2;
(S \ T) * (R \ T) c= S * (R \ T) by RELAT_1:30,XBOOLE_1:36; then
A3: (S \ T) * (R \ T) c= {} by Th15;
(R \ T) * (R \ T) c= R * (R \ T) by RELAT_1:30,XBOOLE_1:36;
then ((R \ T) * (R \ T)) c= {} by Def2;
hence thesis by A1,A2,A3,XBOOLE_1:3;
end;
definition
let N;
func e_Places(N) -> set equals
rng (the entrance of N);
correctness;
end;
definition
let N;
func e_Transitions(N) -> set equals
(the carrier of N) \ e_Places(N);
correctness;
end;
theorem Th17:
([x,y] in the entrance of N or [x,y] in the escape of N) &
x <> y implies x in e_Transitions(N) & y in e_Places(N)
proof
A1: [x,y] in the escape of N & x <> y implies x in e_Transitions(N) & y in
e_Places(N)
proof
(the escape of N) * ((the escape of N) \ id(the carrier of N)) = {}
by Def2; then
A2: (the escape of N) * ((the escape of N) \ id(dom (the escape of N))) =
{} by Th11;
dom (the escape of N) c= the carrier of N by Th14; then
A3: dom (the escape of N) \ dom (CL(the escape of N)) c= (the carrier of
N) \ dom (CL(the escape of N)) by XBOOLE_1:33;
assume
A4: [x,y] in the escape of N & x <> y;
A5: (the escape of N) * (the escape of N) = (the escape of N) by Def1;
then x in dom (the escape of N) \ dom (CL(the escape of N)) by A4,A2,
SYSREL:30;
then x in (the carrier of N) \ dom (CL(the escape of N)) by A3;
then
A6: x in ((the carrier of N) \ rng (the escape of N)) by Th13;
y in dom(CL(the escape of N)) by A4,A5,A2,SYSREL:30;
then y in rng (the escape of N) by Th13;
hence thesis by A6,Th13;
end;
[x,y] in the entrance of N & x <> y implies x in e_Transitions(N) & y in
e_Places(N)
proof
(the entrance of N) * ((the entrance of N) \ id(the carrier of N)) =
{} by Def2;
then
A7: (the entrance of N) * ((the entrance of N) \ id(dom (the entrance of N
)) ) = {} by Th11;
dom (the entrance of N) c= the carrier of N by Th14;
then
A8: dom (the entrance of N) \ dom (CL(the entrance of N)) c= (the carrier
of N) \ dom (CL(the entrance of N)) by XBOOLE_1:33;
assume
A9: [x,y] in the entrance of N & x <> y;
A10: (the entrance of N) * (the entrance of N) = (the entrance of N) by Def1;
then x in dom (the entrance of N) \ dom (CL(the entrance of N)) by A9,A7,
SYSREL:30; then
A11: x in (the carrier of N) \ dom (CL(the entrance of N)) by A8;
y in dom(CL(the entrance of N)) by A9,A10,A7,SYSREL:30;
hence thesis by A11,Th13;
end;
hence thesis by A1;
end;
theorem Th18:
(the entrance of N) \ id(the carrier of N) c=
[:e_Transitions(N),e_Places(N):] &
(the escape of N) \ id(the carrier of N) c=
[:e_Transitions(N),e_Places(N):]
proof
A1: for x,y being object
holds [x,y] in (the entrance of N) \ id(the carrier of N)
implies [x,y] in [:e_Transitions(N),e_Places(N):]
proof
let x,y be object;
assume
A2: [x,y] in (the entrance of N) \ id(the carrier of N);
then [x,y] in (the entrance of N) by XBOOLE_0:def 5;
then
A3: x in dom (the entrance of N) by XTUPLE_0:def 12;
not [x,y] in id(the carrier of N) by A2,XBOOLE_0:def 5;
then
A4: not x in (the carrier of N) or x <> y by RELAT_1:def 10;
A5: [x,y] in (the entrance of N) by A2,XBOOLE_0:def 5;
then
A6: y in e_Places(N) by XTUPLE_0:def 13;
dom (the entrance of N) c= the carrier of N by Th14;
then x in e_Transitions(N) by A5,A4,A3,Th17;
hence thesis by A6,ZFMISC_1:87;
end;
for x,y being object
holds [x,y] in (the escape of N) \ id(the carrier of N) implies
[x,y] in [:e_Transitions(N),e_Places(N):]
proof
let x,y be object;
A7: dom (the escape of N) c= the carrier of N by Th14;
assume
A8: [x,y] in (the escape of N) \ id(the carrier of N);
then [x,y] in (the escape of N) by XBOOLE_0:def 5;
then
A9: x in dom (the escape of N) by XTUPLE_0:def 12;
not [x,y] in id(the carrier of N) by A8,XBOOLE_0:def 5;
then
A10: not x in (the carrier of N) or x <> y by RELAT_1:def 10;
[x,y] in (the escape of N) by A8,XBOOLE_0:def 5;
then x in e_Transitions(N) & y in e_Places(N) by A10,A9,A7,Th17;
hence thesis by ZFMISC_1:87;
end;
hence thesis by A1,RELAT_1:def 3;
end;
definition
let N;
func e_Flow N -> Relation equals
((the entrance of N)~ \/ (the escape of N)) \ id N;
correctness;
end;
theorem
e_Flow N c= [:e_Places(N), e_Transitions(N):] \/
[:e_Transitions(N), e_Places(N):]
proof
A1: (the entrance of N)~ \ id N = (the entrance of N)~ \ (id
(the carrier of N))~
.= ((the entrance of N) \ id(the carrier of N))~ by RELAT_1:24;
A2: e_Flow(N) = ((the entrance of N)~ \ id(the carrier of N)) \/ ((the
escape of N) \ id(the carrier of N)) & (the escape of N) \ id(the carrier of N)
c= [: e_Transitions(N) , e_Places(N):] by Th18,XBOOLE_1:42;
(the entrance of N) \ id(the carrier of N) c= [:e_Transitions(N) ,
e_Places(N):] by Th18;
then (the entrance of N)~ \ id(the carrier of N) c= [:e_Places(N) ,
e_Transitions(N):] by A1,SYSREL:4;
hence thesis by A2,XBOOLE_1:13;
end;
definition
let N;
func e_pre(N) -> Relation equals
(the entrance of N) \ id(the carrier of N);
correctness;
func e_post(N) -> Relation equals
(the escape of N) \ id(the carrier of N);
correctness;
end;
theorem
e_pre(N) c= [:e_Transitions(N),e_Places(N):] &
e_post(N) c= [:e_Transitions(N),e_Places(N):] by Th18;
definition
let N;
func e_shore(N) -> set equals
the carrier of N;
correctness;
func e_prox(N) -> Relation equals
((the entrance of N) \/ (the escape of N))~;
correctness;
func e_flow(N) -> Relation equals
((the entrance of N)~ \/ (the escape of N)) \/ id(the carrier of N);
correctness;
end;
theorem
e_prox(N) c= [:e_shore(N),e_shore(N):] &
e_flow(N) c= [:e_shore(N),e_shore(N):]
proof
A1: id(the carrier of N) c= [:the carrier of N,the carrier of N:] by
RELSET_1:13;
A2: the escape of N c= [:the carrier of N,the carrier of N:] by Def1;
A3: the entrance of N c= [:the carrier of N,the carrier of N:] by Def1;
then (the entrance of N)~ c= [:the carrier of N,the carrier of N:] by
SYSREL:4; then
A4: (the entrance of N)~ \/ (the escape of N) c= [:the carrier of N,the
carrier of N:] by A2,XBOOLE_1:8;
(the entrance of N) \/ (the escape of N) c= [:the carrier of N,the
carrier of N:] by A3,A2,XBOOLE_1:8;
hence thesis by A4,A1,SYSREL:4,XBOOLE_1:8;
end;
theorem
(e_prox(N)) * (e_prox(N)) = e_prox(N) &
(e_prox(N) \ id(e_shore(N))) * e_prox(N) = {} &
(e_prox(N) \/ (e_prox(N))~) \/ id(e_shore(N)) = e_flow(N) \/ (e_flow(N))~
proof
set R = the entrance of N;
set S = the escape of N;
set T = id(the carrier of N);
A1: (e_prox(N) \/ (e_prox(N))~) \/ id(e_shore(N)) = ((R~ \/ S~) \/ (S \/ R))
\/ T by RELAT_1:23
.= (((R~ \/ S~) \/ S) \/ R) \/ T by XBOOLE_1:4
.= ((R~ \/ (S~ \/ S)) \/ R) \/ T by XBOOLE_1:4
.= (R~ \/ ((S \/ S~) \/ R)) \/ T by XBOOLE_1:4
.= (R~ \/ (S \/ (S~ \/ R))) \/ T by XBOOLE_1:4
.= ((R~ \/ S) \/ (S~ \/ R)) \/ T by XBOOLE_1:4
.= e_flow(N) \/ ((S~ \/ (R~)~) \/ T) by XBOOLE_1:5
.= e_flow(N) \/ ((R~ \/ S)~ \/ T) by RELAT_1:23
.= e_flow(N) \/ ((R~ \/ S)~ \/ T~)
.= e_flow(N) \/ (e_flow(N))~ by RELAT_1:23;
A2: (e_prox(N) \ T) * e_prox(N) = ((R~ \/ S~) \ T) * ((R \/ S)~) by RELAT_1:23
.= ((R~ \ T) \/ (S~ \ T)) * ((R \/ S)~) by XBOOLE_1:42
.= ((R~ \ T) \/ (S~ \ T)) * (R~ \/ S~) by RELAT_1:23
.= (((R~ \ T) \/ (S~ \ T)) * R~) \/ (((R~ \ T) \/ (S~ \ T)) * S~) by
RELAT_1:32
.= (((R~ \ T) * R~) \/ ((S~ \ T) * R~)) \/ (((R~ \ T) \/ (S~ \ T)) * S~)
by SYSREL:6
.= (((R~ \ T) * R~) \/ ((S~ \ T) * R~)) \/ (((R~ \ T) * S~) \/ ((S~ \ T)
* S~)) by SYSREL:6
.= (((R~ \ T~) * R~) \/ ((S~ \ T) * R~)) \/ (((R~ \ T) * S~) \/ ((S~ \ T
) * S~))
.= (((R~ \ T~) * R~) \/ ((S~ \ T~) * R~)) \/ (((R~ \ T) * S~) \/ ((S~ \
T) * S~))
.= (((R~ \ T~) * R~) \/ ((S~ \ T~) * R~)) \/ (((R~ \ T~) * S~) \/ ((S~ \
T) * S~))
.= (((R~ \ T~) * R~) \/ ((S~ \ T~) * R~)) \/ (((R~ \ T~) * S~) \/ ((S~ \
T~) * S~))
.= (((R \ T)~ * R~) \/ ((S~ \ T~) * R~)) \/ (((R~ \ T~) * S~) \/ ((S~ \
T~) * S~)) by RELAT_1:24
.= (((R \ T)~ * R~) \/ ((S \ T)~ * R~)) \/ (((R~ \ T~) * S~) \/ ((S~ \ T
~) * S~)) by RELAT_1:24
.= (((R \ T)~ * R~) \/ ((S \ T)~ * R~)) \/ (((R \ T)~ * S~) \/ ((S~ \ T~
) * S~)) by RELAT_1:24
.= (((R \ T)~ * R~) \/ ((S \ T)~ * R~)) \/ (((R \ T)~ * S~) \/ ((S \ T)~
* S~)) by RELAT_1:24
.= ((R * (R \ T))~ \/ ((S \ T)~ * R~)) \/ (((R \ T)~ * S~) \/ ((S \ T)~
* S~)) by RELAT_1:35
.= ((R * (R \ T))~ \/ (R * (S \ T))~) \/ (((R \ T)~ * S~) \/ ((S \ T)~ *
S~)) by RELAT_1:35
.= ((R * (R \ T))~ \/ (R * (S \ T))~) \/ ((S *(R \ T))~ \/ ((S \ T)~ * S
~)) by RELAT_1:35
.= ((R * (R \ T))~ \/ (R * (S \ T))~) \/ ((S * (R \ T))~ \/ (S * (S \ T)
)~) by RELAT_1:35
.= (({}~) \/ (R * (S \ T))~) \/ ((S * (R \ T))~ \/ (S * (S \ T))~) by Def2
.= (({}~) \/ (R * (S \ T))~) \/ ((S * (R \ T))~ \/ ({})~) by Def2
.= ({}~ \/ {}~) \/ ((S * (R \ T))~ \/ {}~) by Th15
.= {} by Th15;
(e_prox(N)) * (e_prox(N)) = ((R \/ S) * (R \/ S))~ by RELAT_1:35
.= (((R \/ S) * R) \/ ((R \/ S) * S))~ by RELAT_1:32
.= (((R * R) \/ (S * R)) \/ ((R \/ S) * S))~ by SYSREL:6
.= (((R * R) \/ (S * R)) \/ ((R * S) \/ (S * S)))~ by SYSREL:6
.= ((R \/ (S * R)) \/ ((R * S) \/ (S * S) ) )~ by Def1
.= ((R \/ S) \/ ((R * S) \/ (S * S)))~ by Def1
.= ((R \/ S) \/ (R \/ (S * S)))~ by Def1
.= ((R \/ S) \/ (R \/ S))~ by Def1
.= e_prox(N);
hence thesis by A2,A1;
end;
theorem Th23:
id((the carrier of N) \ rng(the escape of N)) *
((the escape of N) \ id(the carrier of N)) =
((the escape of N) \ id(the carrier of N)) &
id((the carrier of N) \ rng(the entrance of N)) *
((the entrance of N) \ id(the carrier of N)) =
((the entrance of N) \ id(the carrier of N))
proof
set T = the entrance of N, C = the carrier of N;
set E = the escape of N, I = id C;
for x,y being object
holds [x,y] in (E \ I) implies [x,y] in (id(C \ rng E) * (E \ I))
proof
let x,y be object;
assume
A1: [x,y] in (E \ I);
then [x,y] in E by XBOOLE_0:def 5; then
A2: x in dom(E) by XTUPLE_0:def 12;
A3: not x in rng E
proof
assume x in rng E;
then ex z being object st [z,x] in E by XTUPLE_0:def 13; then
E * (E \ I) <> {} by A1,RELAT_1:def 8;
hence thesis by Def2;
end;
dom E c= C by Th14;
then x in (C \ rng E) by A2,A3,XBOOLE_0:def 5;
then [x,x] in id(C \ rng E) by RELAT_1:def 10;
hence thesis by A1,RELAT_1:def 8;
end; then
A4: E \ I c= id(C \ rng E) * (E \ I) by RELAT_1:def 3;
for x,y being object
holds [x,y] in (T \ I) implies [x,y] in (id(C \ rng T) * (T \ I))
proof
let x,y be object;
assume
A5: [x,y] in (T \ I);
then [x,y] in T by XBOOLE_0:def 5; then
A6: x in dom(T) by XTUPLE_0:def 12;
A7: not x in rng T
proof
assume x in rng T;
then ex z being object st [z,x] in T by XTUPLE_0:def 13;
then T * (T \ I) <> {} by A5,RELAT_1:def 8;
hence thesis by Def2;
end;
dom T c= C by Th14;
then x in (C \ rng T) by A6,A7,XBOOLE_0:def 5;
then [x,x] in id(C \ rng T) by RELAT_1:def 10;
hence thesis by A5,RELAT_1:def 8;
end; then
A8: (T \ I) c= id(C \ rng T) * (T \ I) by RELAT_1:def 3;
id(C \ rng E) * (E \ I) c= (E \ I) &
id(C \ rng T) * (T \ I) c= (T \ I) by RELAT_1:50;
hence thesis by A4,A8,XBOOLE_0:def 10;
end;
theorem Th24:
((the escape of N) \ id the carrier of N) *
((the escape of N) \ id the carrier of N) = {} &
((the entrance of N) \ id the carrier of N) *
((the entrance of N) \ id the carrier of N) = {} &
((the escape of N) \ id(the carrier of N)) *
((the entrance of N) \ id the carrier of N) = {} &
((the entrance of N) \ id the carrier of N) *
((the escape of N) \ id the carrier of N) = {}
proof
set T = the entrance of N, C = the carrier of N;
set E = the escape of N, I = id C;
(T \ I) * (T \ I) c= T * (T \ I) by RELAT_1:30,XBOOLE_1:36; then
A1: (T \ I) * (T \ I) c= {} by Def2;
(E \ I) * (T \ I) c= E * (T \ I) by RELAT_1:30,XBOOLE_1:36;
then
A2: (E \ I) * (T \ I) c= {} by Th15;
(T \ I) * (E \ I) c= T * (E \ I) by RELAT_1:30,XBOOLE_1:36; then
A3: (T \ I) * (E \ I) c= {} by Th15;
(E \ I) * (E \ I) c= E * (E \ I) by RELAT_1:30,XBOOLE_1:36; then
(E \ I) * (E \ I) c= {} by Def2;
hence thesis by A1,A2,A3,XBOOLE_1:3;
end;
theorem Th25:
((the escape of N) \ id(the carrier of N))~ *
((the escape of N) \ id(the carrier of N))~ = {} &
((the entrance of N) \ id(the carrier of N))~ *
((the entrance of N) \ id(the carrier of N))~ = {}
proof
A1: ((the entrance of N) \ id(the carrier of N))~ * ((the entrance of N) \
id(the carrier of N))~ = (((the entrance of N) \ id(the carrier of N)) * ((the
entrance of N) \ id(the carrier of N)))~ by RELAT_1:35
.= {} by Th24,RELAT_1:43;
((the escape of N) \ id(the carrier of N))~ * ((the escape of N) \ id(
the carrier of N))~ = (((the escape of N) \ id(the carrier of N)) * ((the
escape of N) \ id(the carrier of N)))~ by RELAT_1:35
.= {} by Th24,RELAT_1:43;
hence thesis by A1;
end;
theorem
((the escape of N) \ id(the carrier of N))~ * id((the carrier of N) \
rng(the escape of N))~ = ((the escape of N) \ id(the carrier of N))~ &
((the entrance of N) \ id(the carrier of N))~ *
id((the carrier of N) \ rng(the entrance of N))~ =
((the entrance of N) \ id(the carrier of N))~
proof
A1: ((the entrance of N) \ id(the carrier of N))~ * id((the carrier of N) \
rng(the entrance of N))~ = ((id((the carrier of N) \ rng(the entrance of N))) *
((the entrance of N) \ id(the carrier of N)))~ by RELAT_1:35
.= ((the entrance of N) \ id(the carrier of N))~ by Th23;
((the escape of N) \ id(the carrier of N))~ * id((the carrier of N) \
rng(the escape of N))~ = ((id((the carrier of N) \ rng(the escape of N))) * ((
the escape of N) \ id(the carrier of N)))~ by RELAT_1:35
.= ((the escape of N) \ id(the carrier of N))~ by Th23;
hence thesis by A1;
end;
theorem Th27:
((the escape of N) \ id(the carrier of N)) *
(id((the carrier of N) \ rng(the escape of N))) = {} &
((the entrance of N) \ id(the carrier of N)) *
(id((the carrier of N) \ rng(the entrance of N))) = {}
proof
A1: for x,y being object
holds not [x,y] in ((the entrance of N) \ id(the carrier of N))
* (id((the carrier of N) \ rng(the entrance of N)))
proof
let x,y be object;
assume [x,y] in ((the entrance of N) \ id(the carrier of N)) * (id((the
carrier of N) \ rng(the entrance of N)));
then consider z being object such that
A2: [x,z] in ((the entrance of N) \ id(the carrier of N)) and
A3: [z,y] in (id((the carrier of N) \ rng(the entrance of N))) by RELAT_1:def 8
;
z in (the carrier of N) \ rng(the entrance of N) by A3,RELAT_1:def 10;
then
A4: not z in rng(the entrance of N) by XBOOLE_0:def 5;
[x,z] in the entrance of N by A2,XBOOLE_0:def 5;
hence thesis by A4,XTUPLE_0:def 13;
end;
for x,y being object
holds not [x,y] in ((the escape of N) \ id the carrier of N) *
(id((the carrier of N) \ rng the escape of N))
proof
let x,y be object;
assume [x,y] in ((the escape of N) \ id(the carrier of N)) * (id((the
carrier of N) \ rng(the escape of N)));
then consider z being object such that
A5: [x,z] in ((the escape of N) \ id(the carrier of N)) and
A6: [z,y] in (id((the carrier of N) \ rng(the escape of N))) by RELAT_1:def 8;
z in (the carrier of N) \ rng(the escape of N ) by A6,RELAT_1:def 10;
then
A7: not z in rng(the escape of N) by XBOOLE_0:def 5;
[x,z] in the escape of N by A5,XBOOLE_0:def 5;
hence thesis by A7,XTUPLE_0:def 13;
end;
hence thesis by A1,RELAT_1:37;
end;
theorem Th28:
id((the carrier of N) \ rng(the escape of N)) *
((the escape of N) \ id(the carrier of N))~ = {} &
id((the carrier of N) \ rng(the entrance of N)) *
((the entrance of N) \ id(the carrier of N))~ = {}
proof
A1: id((the carrier of N) \ rng(the entrance of N)) * ((the entrance of N) \
id(the carrier of N))~ = (id((the carrier of N) \ rng(the entrance of N)))~ * (
(the entrance of N) \ id(the carrier of N))~
.= (((the entrance of N) \ id(the carrier of N)) * (id((the carrier of N
) \ rng(the entrance of N))))~ by RELAT_1:35
.= {} by Th27,RELAT_1:43;
id((the carrier of N) \ rng(the escape of N)) * ((the escape of N) \ id(
the carrier of N))~ = (id((the carrier of N) \ rng(the escape of N)))~ * ((the
escape of N) \ id(the carrier of N))~
.= (((the escape of N) \ id(the carrier of N)) * (id((the carrier of N)
\ rng(the escape of N))))~ by RELAT_1:35
.= {} by Th27,RELAT_1:43;
hence thesis by A1;
end;
definition
let N;
func e_entrance(N) -> Relation equals
(((the escape of N) \ id(the carrier of N))~) \/
id((the carrier of N) \ rng(the escape of N));
correctness;
func e_escape(N) -> Relation equals
(((the entrance of N) \ id(the carrier of N))~) \/
id((the carrier of N) \ rng(the entrance of N));
correctness;
end;
theorem
e_entrance(N) * e_entrance(N) = e_entrance(N) &
e_entrance(N) * e_escape(N) = e_entrance(N) &
e_escape(N) * e_entrance(N) = e_escape(N) &
e_escape(N) * e_escape(N) = e_escape(N)
proof
set P = ((the escape of N) \ id the carrier of N);
set Q = ((the entrance of N) \ id the carrier of N);
set S = id((the carrier of N) \ rng the entrance of N);
set T = id((the carrier of N) \ rng the escape of N);
A1: e_entrance(N) * e_entrance(N) = ((P~) * ((P~) \/ T)) \/ (T * ((P~) \/ T)
) by SYSREL:6
.= (((P~) * (P~)) \/ ((P~) * T)) \/ (T * ((P~) \/ T)) by RELAT_1:32
.= (((P~) * (P~)) \/ ((P~) * T)) \/ ((T * (P~)) \/ (T * T)) by RELAT_1:32
.= (((P * P)~) \/ ((P~) * T)) \/ ((T * (P~)) \/ (T * T)) by RELAT_1:35
.= (((P * P)~) \/ ((P~) * (T~))) \/ ((T * (P~)) \/ (T * T))
.= (((P * P)~) \/ ((P~) * (T~))) \/ (((T~) * (P~)) \/ (T * T))
.= (((P * P)~) \/ ((P~) * (T~))) \/ (((T~) * (P~)) \/ T) by SYSREL:12
.= (((P * P)~) \/ ((T * P)~)) \/ (((T~) * (P~)) \/ T) by RELAT_1:35
.= (((P * P)~) \/ ((T * P)~)) \/ (((P * T)~) \/ T) by RELAT_1:35
.= (({}~) \/ ((T * P)~)) \/ (((P * T)~) \/ T) by Th24
.= (({}~) \/ (P~)) \/ (((P * T)~) \/ T) by Th23
.= ({} \/ (P~)) \/ ({} \/ T) by Th27
.= e_entrance(N);
A2: e_escape(N) * e_escape(N) = ((Q~) * ((Q~) \/ S)) \/ (S * ((Q~) \/ S)) by
SYSREL:6
.= (((Q~) * (Q~)) \/ ((Q~) * S)) \/ (S * ((Q~) \/ S)) by RELAT_1:32
.= (((Q~) * (Q~)) \/ ((Q~) * S)) \/ ((S * (Q~)) \/ (S * S)) by RELAT_1:32
.= (((Q * Q)~) \/ ((Q~) * S)) \/ ((S * (Q~)) \/ (S * S)) by RELAT_1:35
.= (((Q * Q)~) \/ ((Q~) * (S~))) \/ ((S * (Q~)) \/ (S * S))
.= (((Q * Q)~) \/ ((Q~) * (S~))) \/ (((S~) * (Q~)) \/ (S * S))
.= (((Q * Q)~) \/ ((Q~) * (S~))) \/ (((S~) * (Q~)) \/ S) by SYSREL:12
.= (((Q * Q)~) \/ ((S * Q)~)) \/ (((S~) * (Q~)) \/ S) by RELAT_1:35
.= (((Q * Q)~) \/ ((S * Q)~)) \/ (((Q * S)~) \/ S) by RELAT_1:35
.= (({}~) \/ ((S * Q)~)) \/ (((Q * S)~) \/ S) by Th24
.= (({}~) \/ (Q~)) \/ (((Q * S)~) \/ S) by Th23
.= ({} \/ (Q~)) \/ ({} \/ S) by Th27
.= e_escape(N);
A3: e_escape(N) * e_entrance(N) = ((Q~) * ((P~) \/ T)) \/ (S * ((P~) \/ T))
by SYSREL:6
.= (((Q~) * (P~)) \/ ((Q~) * T)) \/ (S * ((P~) \/ T)) by RELAT_1:32
.= (((Q~) * (P~)) \/ ((Q~) * T)) \/ ((S * (P~)) \/ (S * T)) by RELAT_1:32
.= (((P * Q)~) \/ ((Q~) * T)) \/ ((S * (P~)) \/ (S * T)) by RELAT_1:35
.= (((P * Q)~) \/ ((Q~) * (T~))) \/ ((S * (P~)) \/ (S * T))
.= (((P * Q)~) \/ ((Q~) * (T~))) \/ (((S~) * (P~)) \/ (S * T))
.= (((P * Q)~) \/ ((Q~) * (T~))) \/ (((S~) * (P~)) \/ (S * S)) by Th13
.= (((P * Q)~) \/ ((Q~) * (T~))) \/ (((S~) * (P~)) \/ S) by SYSREL:12
.= (((P * Q)~) \/ ((T * Q)~)) \/ (((S~) * (P~)) \/ S) by RELAT_1:35
.= (((P * Q)~) \/ ((T * Q)~)) \/ (((P * S)~) \/ S) by RELAT_1:35
.= (((P * Q)~) \/ ((S * Q)~)) \/ (((P * S)~) \/ S) by Th13
.= (((P * Q)~) \/ ((S * Q)~)) \/ (((P * T)~) \/ S) by Th13
.= (({}~) \/ ((S * Q)~)) \/ (((P * T)~) \/ S) by Th24
.= (({}~) \/ (Q~)) \/ (((P * T)~) \/ S) by Th23
.= ({} \/ (Q~)) \/ ({} \/ S) by Th27
.= e_escape(N);
e_entrance(N) * e_escape(N) = ((P~) * ((Q~) \/ S)) \/ (T * ((Q~) \/ S))
by SYSREL:6
.= (((P~) * (Q~)) \/ ((P~) * S)) \/ (T * ((Q~) \/ S)) by RELAT_1:32
.= (((P~) * (Q~)) \/ ((P~) * S)) \/ ((T * (Q~)) \/ (T * S)) by RELAT_1:32
.= (((Q * P)~) \/ ((P~) * S)) \/ ((T * (Q~)) \/ (T * S)) by RELAT_1:35
.= (((Q * P)~) \/ ((P~) * (S~))) \/ ((T * (Q~)) \/ (T * S))
.= (((Q * P)~) \/ ((P~) * (S~))) \/ (((T~) * (Q~)) \/ (T * S))
.= (((Q * P)~) \/ ((P~) * (S~))) \/ (((T~) * (Q~)) \/ (T * T)) by Th13
.= (((Q * P)~) \/ ((P~) * (S~))) \/ (((T~) * (Q~)) \/ T) by SYSREL:12
.= (((Q * P)~) \/ ((S * P)~)) \/ (((T~) * (Q~)) \/ T) by RELAT_1:35
.= (((Q * P)~) \/ ((S * P)~)) \/ (((Q * T)~) \/ T) by RELAT_1:35
.= (((Q * P)~) \/ ((T * P)~)) \/ (((Q * T)~) \/ T) by Th13
.= (((Q * P)~) \/ ((T * P)~)) \/ (((Q * S)~) \/ T) by Th13
.= (({}~) \/ ((T * P)~)) \/ (((Q * S)~) \/ T) by Th24
.= (({}~) \/ (P~)) \/ (((Q * S)~) \/ T) by Th23
.= ({} \/ (P~)) \/ ({} \/ T) by Th27
.= e_entrance(N);
hence thesis by A1,A3,A2;
end;
theorem
e_entrance(N) * (e_entrance(N) \ id(e_shore N)) = {} &
e_escape(N) * (e_escape(N) \ id(e_shore N)) = {}
proof
set P = ((the escape of N) \ id N);
set Q = ((the entrance of N) \ id(the carrier of N));
set S = id((the carrier of N) \ rng the entrance of N);
set T = id((the carrier of N) \ rng the escape of N);
set R = id the carrier of N;
A1: S c= R by SYSREL:15,XBOOLE_1:36;
(Q~) * ((Q~) \ R) c= (Q~) * (Q~) by RELAT_1:29,XBOOLE_1:36;
then (Q~) * ((Q~) \ R) c= {} by Th25;
then
A2: (Q~) * ((Q~) \ R) = {} by XBOOLE_1:3;
S * ((Q~) \ R) c= S * (Q~) by RELAT_1:29,XBOOLE_1:36;
then S * ((Q~) \ R) c= {} by Th28;
then
A3: S * ((Q~) \ R) = {} by XBOOLE_1:3;
A4: e_escape(N) * (e_escape(N) \ id(e_shore(N))) = ((Q~) \/ S) * (((Q~) \
R) \/ (S \ R)) by XBOOLE_1:42
.= ((Q~) \/ S) * (((Q~) \ R) \/ {}) by A1,XBOOLE_1:37
.= {} \/ {} by A2,A3,SYSREL:6
.= {};
A5: T c= R by SYSREL:15,XBOOLE_1:36;
T * ((P~) \ R) c= T * (P~) by RELAT_1:29,XBOOLE_1:36;
then T * ((P~) \ R) c= {} by Th28;
then
A6: T * ((P~) \ R) = {} by XBOOLE_1:3;
(P~) * ((P~) \ R) c= (P~) * (P~) by RELAT_1:29,XBOOLE_1:36;
then (P~) * ((P~) \ R) c= {} by Th25;
then
A7: (P~) * ((P~) \ R) = {} by XBOOLE_1:3;
e_entrance(N) * (e_entrance(N) \ id(e_shore N)) = ((P~) \/ T) * (((P
~) \ R) \/ (T \ R)) by XBOOLE_1:42
.= ((P~) \/ T) * (((P~) \ R) \/ {}) by A5,XBOOLE_1:37
.= {} \/ {} by A7,A6,SYSREL:6
.= {};
hence thesis by A4;
end;
definition
let N;
func e_adjac(N) -> Relation equals
(((the entrance of N) \/ (the escape of N)) \ id(the carrier of N))
\/ id((the carrier of N) \ rng(the entrance of N));
correctness;
end;
theorem
e_adjac(N) c= [:e_shore(N),e_shore(N):] &
e_flow(N) c= [:e_shore(N),e_shore(N):]
proof
A1: ((the entrance of N) \/ (the escape of N)) \ id(the carrier of N) c= ((
the entrance of N) \/ (the escape of N)) by XBOOLE_1:36;
A2: the escape of N c= [:the carrier of N,the carrier of N:] by Def1;
A3: the entrance of N c= [:the carrier of N,the carrier of N:] by Def1;
then (the entrance of N)~ c= [:the carrier of N,the carrier of N:] by
SYSREL:4;
then
A4: id(the carrier of N) c= [:the carrier of N,the carrier of N:] & (the
entrance of N)~ \/ (the escape of N) c= [:the carrier of N,the carrier of N:]
by A2,RELSET_1:13,XBOOLE_1:8;
id((the carrier of N) \ rng(the entrance of N)) c= id(the carrier of N)
& id (the carrier of N) c= [:the carrier of N,the carrier of N:] by RELSET_1:13
,SYSREL:15,XBOOLE_1:36; then
A5: id((the carrier of N) \ rng(the entrance of N)) c= [:the carrier of N,
the carrier of N:] by XBOOLE_1:1;
(the entrance of N) \/ (the escape of N) c= [:the carrier of N,the
carrier of N:] by A3,A2,XBOOLE_1:8; then
((the entrance of N) \/ (the escape of N)) \ id(the carrier of N) c= [:
the carrier of N,the carrier of N:] by A1,XBOOLE_1:1;
hence thesis by A5,A4,XBOOLE_1:8;
end;
theorem
(e_adjac(N)) * (e_adjac(N)) = e_adjac(N) &
(e_adjac(N) \ id(e_shore(N))) * e_adjac(N) = {} &
(e_adjac(N) \/ (e_adjac(N))~) \/ id(e_shore(N)) = e_flow(N) \/ (e_flow(N))~
proof
set P = the entrance of N;
set Q = the escape of N;
set R = id(the carrier of N);
set S = id((the carrier of N) \ rng(the entrance of N));
set T = id((the carrier of N) \ rng(the escape of N));
A1: S c= R by SYSREL:15,XBOOLE_1:36;
(e_adjac N \/ (e_adjac N)~) = (((P \/ Q) \ R) \/ S) \/ ( (((P \/ Q) \ R
)~) \/ (S~)) by RELAT_1:23
.= (((P \/ Q) \ R) \/ S) \/ ( ( ((P \/ Q) \ R)~) \/ S)
.= (((P \/ Q) \ R) \/ ( ((P \/ Q) \ R)~ ) ) \/ S by XBOOLE_1:5
.= (((P \/ Q) \ R) \/ ( ((P \/ Q)~) \ (R~) )) \/ S by RELAT_1:24
.= (((P \/ Q) \ R) \/ (((P \/ Q)~) \ R)) \/ S
.= (((P \/ Q) \/ ((P \/ Q)~)) \ R) \/ S by XBOOLE_1:42;
then
A2: (e_adjac(N) \/ (e_adjac(N))~) \/ id(e_shore(N)) = (((P \/ Q) \/ ((P
\/ Q)~)) \ R) \/ (S \/ R) by XBOOLE_1:4
.= (((P \/ Q) \/ ((P \/ Q)~)) \ R) \/ R by A1,XBOOLE_1:12
.= (((P~ \/ (Q~)) \/ (P \/ Q)) \ R) \/ R by RELAT_1:23
.= (P~ \/ ((Q \/ P) \/ (Q~)) \ R) \/ R by XBOOLE_1:4
.= (P~ \/ (Q \/ (P \/ (Q~))) \ R) \/ R by XBOOLE_1:4
.= ( ( (P~ \/ Q) \/ (P \/ (Q~)) ) \ R) \/ R by XBOOLE_1:4
.= ( (P~ \/ Q) \/ (P \/ (Q~)) ) \/ R by XBOOLE_1:39
.= e_flow N \/ ((((P \/ (Q~))~)~) \/ R) by XBOOLE_1:5
.= e_flow N \/ (((P~ \/ ((Q~)~))~) \/ R) by RELAT_1:23
.= e_flow N \/ (((P~ \/ Q)~) \/ (R~))
.= e_flow N \/ (e_flow N)~ by RELAT_1:23;
S c= R by SYSREL:15,XBOOLE_1:36;
then
A3: S \ R = {} by XBOOLE_1:37;
(P \ R) * (Q \ R) c= P * (Q \ R) by RELAT_1:30,XBOOLE_1:36;
then (P \ R) * (Q \ R) c= {} by Th15;
then
A4: (P \ R) * (Q \ R) = {} by XBOOLE_1:3;
(P \ R) * (P \ R) c= P * (P \ R) by RELAT_1:30,XBOOLE_1:36;
then (P \ R) * (P \ R) c= {} by Def2;
then
A5: (P \ R) * (P \ R) = {} by XBOOLE_1:3;
(Q \ R) * (P \ R) c= Q * (P \ R) by RELAT_1:30,XBOOLE_1:36;
then (Q \ R) * (P \ R) c= {} by Th15;
then
A6: (Q \ R) * (P \ R) = {} by XBOOLE_1:3;
(Q \ R) * (Q \ R) c= Q * (Q \ R) by RELAT_1:30,XBOOLE_1:36;
then (Q \ R) * (Q \ R) c= {} by Def2;
then
A7: (Q \ R) * (Q \ R) = {} by XBOOLE_1:3;
A8: (e_adjac(N) \ R) * e_adjac(N) = (((((P \/ Q) \ R) \/ S
) \ R) * ((P \/ Q) \ R)) \/ (((((P \/ Q) \ R) \/ S) \ R) * S) by RELAT_1:32
.= (((((P \ R) \/ (Q \ R)) \/ S) \ R) * ((P \/ Q) \ R)) \/ (((((P \/ Q)
\ R) \/ S) \ R) * S) by XBOOLE_1:42
.= ((( (((P \ R) \/ (Q \ R)) \ R) \/ (S \ R)) * ((P \/ Q) \ R)) \/ ((((P
\/ Q) \ R) \/ S) \ R) * S) by XBOOLE_1:42
.= (((( ( ((P \ R) \ R) \/ ((Q \ R) \ R)) ) \/ (S \ R)) * ((P \/ Q) \ R)
) \/ ((((P \/ Q) \ R) \/ S) \ R) * S) by XBOOLE_1:42
.= (((((((P \ (R \/ R)) \/ ((Q \ R) \ R))) \/ (S \ R)) * ((P \/ Q) \ R))
\/ ((((P \/ Q) \ R) \/ S) \ R) * S)) by XBOOLE_1:41
.= ((((((P \ R) \/ ((Q \ (R \/ R))) \/ (S \ R)) * ((P \/ Q) \ R)) \/ (((
(P \/ Q) \ R) \/ S) \ R) * S))) by XBOOLE_1:41
.= (((((P \ R) \/ (Q \ R)) \/ (S \ R)) * ((P \ R) \/ (Q \ R)) \/ ((((P
\/ Q) \ R) \/ S) \ R) * S)) by XBOOLE_1:42
.= (((((P \ R) \/ (Q \ R) \/ (S \ R)) * ((P \ R) \/ (Q \ R))) \/ ((((P \
R) \/ (Q \ R)) \/ S) \ R) * S)) by XBOOLE_1:42
.= ((( ( ( ((P \ R) \/ (Q \ R)) \/ (S \ R) ) * (P \ R) ) \/ ( ( ((P \ R)
\/ (Q \ R)) \/ (S \ R) ) * (Q \ R))) \/ ((((P \ R) \/ (Q \ R)) \/ S) \ R) * S))
by RELAT_1:32
.= ((( ( ( ((P \ R) \/ (Q \ R)) \/ (S \ R) ) * (P \ R) ) \/ ( ( ((P \ R)
\/ (Q \ R)) * (Q \ R) ) \/ ((S \ R) * (Q \ R)) ) ) \/ ((((P \ R) \/ (Q \ R)) \/
S) \ R) * S)) by SYSREL:6
.= ((( ( ( ((P \ R) \/ (Q \ R)) * (P \ R)) \/ ((S \ R) ) * (P \ R)) ) \/
( ( ((P \ R) \/ (Q \ R)) * (Q \ R)) \/ ((S \ R) * (Q \ R)) ) ) \/ ((((P \ R) \/
(Q \ R)) \/ S) \ R) * S) by SYSREL:6
.= ((( ( ({} \/ {}) \/ ((S \ R) ) * (P \ R)) ) \/ ( ( ((P \ R) \/ (Q \ R
)) * (Q \ R)) \/ ((S \ R) * (Q \ R)) ) ) \/ ((((P \ R) \/ (Q \ R)) \/ S) \ R) *
S) by A5,A6,SYSREL:6
.= ((( {} * (P \ R)) \/ ({} * (Q \ R))) \/ ((((P \ R) \/ (Q \ R)) \/ S)
\ R) * S) by A3,A4,A7,SYSREL:6
.= ( ( ((P \ R) \/ (Q \ R)) \ R) \/ (S \ R) ) * S by XBOOLE_1:42
.= ( ( ((P \ R) \ R) \/ ((Q \ R) \ R)) \/ (S \ R) ) * S by XBOOLE_1:42
.= ( ((P \ (R \/ R)) \/ ((Q \ R) \ R)) \/ (S \ R) ) * S by XBOOLE_1:41
.= ( ((P \ R) \/ (Q \ (R \/ R)) ) \/ (S \ R) ) * S by XBOOLE_1:41
.= ((P \ R) * S) \/ ((Q \ R) * S) by A3,SYSREL:6
.= {} \/ ((Q \ R) * S) by Th27
.= {} \/ ((Q \ R) * T) by Th13
.= {} by Th27;
e_adjac(N) * e_adjac(N) = ((((P \/ Q) \ R) * (((P \/ Q) \ R) \/ S)) \/
(S * (((P \/ Q) \ R) \/ S))) by SYSREL:6
.= ((((P \/ Q) \ R) * ((P \/ Q) \ R)) \/ (((P \/ Q) \ R) * S)) \/ (S * (
((P \/ Q) \ R) \/ S)) by RELAT_1:32
.= ((((P \/ Q) \ R) * ((P \/ Q) \ R)) \/ (((P \/ Q) \ R) * S)) \/ ((S *
((P \/ Q) \ R)) \/ (S * S)) by RELAT_1:32
.= ((((P \ R) \/ (Q \ R)) * ((P \/ Q) \ R)) \/ (((P \/ Q) \ R) * S)) \/
((S * ((P \/ Q) \ R)) \/ (S * S)) by XBOOLE_1:42
.= ((((P \ R) \/ (Q \ R)) * ((P \ R) \/ (Q \ R))) \/ (((P \/ Q) \ R) * S
)) \/ ((S * ((P \/ Q) \ R)) \/ (S * S)) by XBOOLE_1:42
.= ((((P \ R) \/ (Q \ R)) * ((P \ R) \/ (Q \ R))) \/ (((P \ R) \/ (Q \ R
)) * S)) \/ ((S * ((P \/ Q) \ R)) \/ (S * S)) by XBOOLE_1:42
.= ((((P \ R) \/ (Q \ R)) * ((P \ R) \/ (Q \ R))) \/ (((P \ R) \/ (Q \ R
)) * S)) \/ ((S * ((P \ R) \/ (Q \ R))) \/ (S * S)) by XBOOLE_1:42
.= ((((P \ R) \/ (Q \ R)) * ((P \ R)) \/ (((P \ R) \/ (Q \ R)) * (Q \ R)
)) \/ (((P \ R) \/ (Q \ R)) * S)) \/ ((S * ((P \ R) \/ (Q \ R))) \/ (S * S))
by RELAT_1:32
.= ((({} \/ {}) \/ (((P \ R) \/ (Q \ R)) * (Q \ R))) \/ (((P \ R) \/ (Q
\ R)) * S)) \/ ((S * ((P \ R) \/ (Q \ R))) \/ (S * S)) by A5,A6,SYSREL:6
.= {} \/ (((P \ R) \/ (Q \ R)) * S) \/ ((S * ((P \ R) \/ (Q \ R))) \/ (S
* S)) by A4,A7,SYSREL:6
.= (((P \ R) \/ (Q \ R)) * S) \/ ((S * ((P \ R) \/ (Q \ R))) \/ S) by
SYSREL:12
.= (((P \ R) * S) \/ ((Q \ R) * S)) \/ ((S * ((P \ R) \/ (Q \ R))) \/ S)
by SYSREL:6
.= (((P \ R) * S) \/ ((Q \ R) * S)) \/ ((S * (P \ R)) \/ (S * (Q \ R))
\/ S) by RELAT_1:32
.= ({} \/ ((Q \ R) * S)) \/ ((S * (P \ R)) \/ (S * (Q \ R)) \/ S) by Th27
.= ((Q \ R) * T) \/ ((S * (P \ R)) \/ (S * (Q \ R)) \/ S) by Th13
.= {} \/ ((S * (P \ R)) \/ (S * (Q \ R)) \/ S) by Th27
.= ((P \ R) \/ (S * (Q \ R)) \/ S) by Th23
.= ((P \ R) \/ (T * (Q \ R)) \/ S) by Th13
.= ((P \ R) \/ (Q \ R)) \/ S by Th23
.= e_adjac N by XBOOLE_1:42;
hence thesis by A8,A2;
end;
reserve N for e_net;
theorem Th33:
((the entrance of N) \ id(the carrier of N))~ c=
[:e_Places(N), e_Transitions(N):] &
((the escape of N) \ id(the carrier of N))~ c=
[:e_Places(N),e_Transitions(N):]
proof
(the entrance of N) \ id(the carrier of N) c=
[:e_Transitions(N),e_Places N :] &
(the escape of N) \ id(the carrier of N) c=
[:e_Transitions(N),e_Places N:] by Th18;
hence thesis by SYSREL:4;
end;
definition
let N be G_Net;
func s_pre(N) -> Relation equals
((the escape of N) \ id(the carrier of N))~;
coherence;
func s_post(N) -> Relation equals
((the entrance of N) \ id(the carrier of N))~;
coherence;
end;
theorem
s_post(N) c= [:e_Places(N),e_Transitions(N):] &
s_pre(N) c= [:e_Places(N),e_Transitions(N):] by Th33;