:: Definitions of Petri Net - Part I
:: by Waldemar Korczy\'nski
::
:: Received January 31, 1992
:: Copyright (c) 1992-2021 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 NET_1, XBOOLE_0, TARSKI, ZFMISC_1, RELAT_1, FF_SIEC, STRUCT_0,
PETRI;
notations TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, PARTIT_2, STRUCT_0, PETRI,
NET_1;
constructors NET_1, PARTIT_2;
registrations RELAT_1, NET_1, PARTIT_2;
requirements SUBSET, BOOLE;
equalities NET_1;
theorems ZFMISC_1, RELAT_1, SYSREL, TARSKI, RELSET_1, NET_1, XBOOLE_0,
XBOOLE_1, XTUPLE_0;
begin :: F - Nets
reserve x,y for object,X,Y for set;
reserve M for Pnet;
definition
let X,Y;
assume
A1: X misses Y;
func PTempty_f_net(X,Y) -> strict Pnet equals
:Def1:
PT_net_Str (# X, Y, {}(X,Y), {}(Y,X) #);
correctness
proof
set M = PT_net_Str (# X, Y, {}(X,Y), {}(Y,X) #);
Flow M c= [:the carrier of M, the carrier' of M:] \/ [:the
carrier' of M, the carrier of M:] by XBOOLE_1:13;
hence thesis by A1,NET_1:def 2;
end;
end;
definition
let X;
func Tempty_f_net(X) -> strict Pnet equals
PTempty_f_net(X,{});
correctness;
func Pempty_f_net(X) -> strict Pnet equals
PTempty_f_net({},X);
correctness;
end;
definition
let x;
func Tsingle_f_net(x) -> strict Pnet equals
PTempty_f_net({},{x});
correctness;
func Psingle_f_net(x) -> strict Pnet equals
PTempty_f_net({x},{});
correctness;
end;
definition
func empty_f_net -> strict Pnet equals
PTempty_f_net({},{});
correctness;
end;
theorem
X misses Y implies the carrier of PTempty_f_net(X,Y) = X &
the carrier' of PTempty_f_net(X,Y) = Y &
Flow PTempty_f_net(X,Y) = {}
proof
assume X misses Y;
then PTempty_f_net(X,Y) = PT_net_Str (# X, Y, {}(X,Y), {}(Y,X) #) by Def1;
hence thesis;
end;
theorem
the carrier of Tempty_f_net(X) = X &
the carrier' of Tempty_f_net(X) = {} & Flow Tempty_f_net(X) = {}
proof
Tempty_f_net(X) = PT_net_Str (# X, {}, {}(X,{}), {}({},X) #)
by Def1,XBOOLE_1:65;
hence thesis;
end;
theorem
for X holds the carrier of Pempty_f_net(X) = {} &
the carrier' of Pempty_f_net(X) = X & Flow Pempty_f_net(X) = {}
proof
let X;
{} misses X by XBOOLE_1:65;
then Pempty_f_net(X) = PT_net_Str (# {}, X, {}({},X), {}(X,{}) #) by Def1;
hence thesis;
end;
theorem
for x holds the carrier of (Tsingle_f_net(x)) = {} &
the carrier' of (Tsingle_f_net(x)) = {x} &
Flow Tsingle_f_net x = {}
proof
let x;
{} misses {x} by XBOOLE_1:65;
then Tsingle_f_net(x) = PT_net_Str (# {}, {x}, {}({},{x}), {}({x},{}) #)
by Def1;
hence thesis;
end;
theorem
for x holds the carrier of (Psingle_f_net(x)) = {x} &
the carrier' of (Psingle_f_net(x)) = {} &
Flow (Psingle_f_net(x)) = {}
proof
let x;
Psingle_f_net(x) = PT_net_Str (# {x}, {}, {}({x},{}), {}({},{x}) #)
by Def1,XBOOLE_1:65;
hence thesis;
end;
theorem
the carrier of empty_f_net = {} & the carrier' of empty_f_net = {} &
Flow empty_f_net = {}
proof
empty_f_net = PT_net_Str (# {}, {}, {}({},{}), {}({},{}) #)
by Def1,XBOOLE_1:65;
hence thesis;
end;
theorem Th7:
( [x,y] in Flow M & x in the carrier' of M implies
not x in the carrier of M & not y in the carrier' of M &
y in the carrier of M) &
( [x,y] in Flow M & y in the carrier' of M implies
not y in the carrier of M & not x in the carrier' of M &
x in the carrier of M) &
( [x,y] in Flow M & x in the carrier of M implies
not y in the carrier of M & not x in the carrier' of M &
y in the carrier' of M) &
( [x,y] in Flow M & y in the carrier of M implies
not x in the carrier of M & not y in the carrier' of M &
x in the carrier' of M)
proof
A1: (the carrier of M) misses (the carrier' of M) by NET_1:def 2;
(Flow M) c= [:the carrier of M, the carrier' of M:] \/ [:the
carrier' of M, the carrier of M:] by NET_1:def 2;
hence thesis by A1,SYSREL:7;
end;
theorem Th8:
(Flow M) c= [:Elements(M), Elements(M):] &
(Flow M)~ c= [:Elements(M), Elements(M):]
proof
A1: the carrier of M c= Elements(M) by XBOOLE_1:7;
A2: the carrier' of M c= Elements(M) by XBOOLE_1:7;
then
A3: [:the carrier of M, the carrier' of M:] c=
[:Elements(M), Elements(M):] by A1,ZFMISC_1:96;
[:the carrier' of M, the carrier of M:] c=
[:Elements(M), Elements(M):] by A1,A2,ZFMISC_1:96;
then
A4: [:the carrier of M, the carrier' of M:] \/
[:the carrier' of M, the carrier of M:] c=
[:Elements(M), Elements(M):] by A3,XBOOLE_1:8;
Flow M c= [:the carrier of M, the carrier' of M:] \/
[:the carrier' of M, the carrier of M:] by NET_1:def 2;
then (Flow M) c= [:Elements(M), Elements(M):] by A4,XBOOLE_1:1;
hence thesis by SYSREL:4;
end;
theorem Th9:
rng ((Flow M)|(the carrier' of M)) c= (the carrier of M) &
rng ((Flow M)~|(the carrier' of M)) c= (the carrier of M) &
rng ((Flow M)|(the carrier of M)) c= (the carrier' of M) &
rng ((Flow M)~|(the carrier of M)) c= (the carrier' of M) &
rng id(the carrier' of M) c= (the carrier' of M) &
dom id(the carrier' of M) c= (the carrier' of M) &
rng id(the carrier of M) c= (the carrier of M) &
dom id(the carrier of M) c= (the carrier of M)
proof
A1: for x being object holds x in rng ((Flow M)|(the carrier' of M)) implies
x in (the carrier of M)
proof
let x be object;
assume x in rng ((Flow M)|(the carrier' of M));
then consider y being object such that
A2: [y,x] in (Flow M)|(the carrier' of M) by XTUPLE_0:def 13;
A3: y in (the carrier' of M) by A2,RELAT_1:def 11;
[y,x] in (Flow M) by A2,RELAT_1:def 11;
hence thesis by A3,Th7;
end;
A4: for x being object holds x in rng ((Flow M)~|(the carrier' of M)) implies
x in (the carrier of M)
proof
let x be object;
assume x in rng ((Flow M)~|(the carrier' of M));
then consider y being object such that
A5: [y,x] in (Flow M)~|(the carrier' of M) by XTUPLE_0:def 13;
A6: [y,x] in (Flow M)~ by A5,RELAT_1:def 11;
A7: y in (the carrier' of M) by A5,RELAT_1:def 11;
[x,y] in (Flow M) by A6,RELAT_1:def 7;
hence thesis by A7,Th7;
end;
A8: for x being object holds x in rng ((Flow M)|(the carrier of M)) implies
x in (the carrier' of M)
proof
let x be object;
assume x in rng ((Flow M)|(the carrier of M));
then consider y being object such that
A9: [y,x] in (Flow M)|(the carrier of M) by XTUPLE_0:def 13;
A10: y in (the carrier of M) by A9,RELAT_1:def 11;
[y,x] in (Flow M) by A9,RELAT_1:def 11;
hence thesis by A10,Th7;
end;
for x being object holds x in rng ((Flow M)~|(the carrier of M)) implies
x in (the carrier' of M)
proof
let x be object;
assume x in rng ((Flow M)~|(the carrier of M));
then consider y being object such that
A11: [y,x] in (Flow M)~|(the carrier of M) by XTUPLE_0:def 13;
A12: [y,x] in (Flow M)~ by A11,RELAT_1:def 11;
A13: y in (the carrier of M) by A11,RELAT_1:def 11;
[x,y] in (Flow M) by A12,RELAT_1:def 7;
hence thesis by A13,Th7;
end;
hence thesis by A1,A4,A8,TARSKI:def 3;
end;
theorem Th10:
rng ((Flow M)|(the carrier' of M)) misses dom((Flow M)|(the carrier' of M)) &
rng ((Flow M)|(the carrier' of M)) misses
dom((Flow M)~|(the carrier' of M)) &
rng ((Flow M)|(the carrier' of M)) misses
dom(id(the carrier' of M)) &
rng ((Flow M)~|(the carrier' of M)) misses
dom((Flow M)|(the carrier' of M)) &
rng ((Flow M)~|(the carrier' of M)) misses
dom((Flow M)~|(the carrier' of M)) &
rng ((Flow M)~|(the carrier' of M)) misses
dom(id(the carrier' of M)) &
dom ((Flow M)|(the carrier' of M)) misses
rng((Flow M)|(the carrier' of M)) &
dom ((Flow M)|(the carrier' of M)) misses
rng((Flow M)~|(the carrier' of M)) &
dom ((Flow M)|(the carrier' of M)) misses
rng(id(the carrier of M)) &
dom ((Flow M)~|(the carrier' of M)) misses
rng((Flow M)|(the carrier' of M)) &
dom ((Flow M)~|(the carrier' of M)) misses
rng((Flow M)~|(the carrier' of M)) &
dom ((Flow M)~|(the carrier' of M)) misses
rng(id(the carrier of M)) & rng ((Flow M)|(the carrier of M)) misses
dom((Flow M)|(the carrier of M)) &
rng ((Flow M)|(the carrier of M)) misses
dom((Flow M)~|(the carrier of M)) &
rng ((Flow M)|(the carrier of M)) misses dom(id(the carrier of M)) &
rng ((Flow M)~|(the carrier of M)) misses
dom((Flow M)|(the carrier of M)) &
rng ((Flow M)~|(the carrier of M)) misses
dom((Flow M)~|(the carrier of M)) &
rng ((Flow M)~|(the carrier of M)) misses dom(id(the carrier of M)) &
dom ((Flow M)|(the carrier of M)) misses
rng((Flow M)|(the carrier of M)) &
dom ((Flow M)|(the carrier of M)) misses
rng((Flow M)~|(the carrier of M)) &
dom ((Flow M)|(the carrier of M)) misses
rng(id(the carrier' of M)) &
dom ((Flow M)~|(the carrier of M)) misses
rng((Flow M)|(the carrier of M)) &
dom ((Flow M)~|(the carrier of M)) misses
rng((Flow M)~|(the carrier of M)) &
dom ((Flow M)~|(the carrier of M)) misses
rng(id(the carrier' of M))
proof
set R = (Flow M)|(the carrier' of M);
set S = (Flow M)~|(the carrier' of M);
set T = id(the carrier' of M);
set R1 = (Flow M)|(the carrier of M);
set S1 = (Flow M)~|(the carrier of M);
set T1 = id(the carrier of M);
A1: dom R c= the carrier' of M by RELAT_1:58;
A2: rng R c= the carrier of M by Th9;
A3: dom S c= the carrier' of M by RELAT_1:58;
A4: rng S c= the carrier of M by Th9;
A5: dom R1 c= the carrier of M by RELAT_1:58;
A6: rng R1 c= the carrier' of M by Th9;
A7: dom S1 c= the carrier of M by RELAT_1:58;
A8: rng S1 c= the carrier' of M by Th9;
(the carrier of M) misses (the carrier' of M) by NET_1:def 2;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,XBOOLE_1:64;
end;
theorem Th11:
((Flow M)|(the carrier' of M)) * ((Flow M)|(the carrier' of M)) = {} &
((Flow M)~|(the carrier' of M)) *
((Flow M)~|(the carrier' of M)) = {} &
((Flow M)|(the carrier' of M)) *
((Flow M)~|(the carrier' of M)) = {} &
((Flow M)~|(the carrier' of M)) *
((Flow M)|(the carrier' of M)) = {} &
((Flow M)|(the carrier of M)) *
((Flow M)|(the carrier of M)) = {} &
((Flow M)~|(the carrier of M)) *
((Flow M)~|(the carrier of M)) = {} &
((Flow M)|(the carrier of M)) *
((Flow M)~|(the carrier of M)) = {} &
((Flow M)~|(the carrier of M)) *
((Flow M)|(the carrier of M)) = {}
proof
A1: rng ((Flow M)|(the carrier' of M)) misses
dom ((Flow M)|(the carrier' of M)) by Th10;
A2: rng ((Flow M)~|(the carrier' of M)) misses
dom ((Flow M)~|(the carrier' of M)) by Th10;
A3: rng ((Flow M)|(the carrier' of M)) misses
dom ((Flow M)~|(the carrier' of M)) by Th10;
A4: rng ((Flow M)~|(the carrier' of M)) misses
dom ((Flow M)|(the carrier' of M)) by Th10;
A5: rng ((Flow M)|(the carrier of M)) misses
dom ((Flow M)|(the carrier of M)) by Th10;
A6: rng ((Flow M)~|(the carrier of M)) misses
dom ((Flow M)~|(the carrier of M)) by Th10;
A7: rng ((Flow M)|(the carrier of M)) misses
dom ((Flow M)~|(the carrier of M)) by Th10;
rng ((Flow M)~|(the carrier of M)) misses
dom ((Flow M)|(the carrier of M)) by Th10;
hence thesis by A1,A2,A3,A4,A5,A6,A7,RELAT_1:44;
end;
theorem Th12:
((Flow M)|(the carrier' of M)) *
id(the carrier of M) = (Flow M)|(the carrier' of M) &
((Flow M)~|(the carrier' of M)) *
id(the carrier of M) = (Flow M)~|(the carrier' of M) &
(id(the carrier' of M) * ((Flow M)|(the carrier' of M))) =
(Flow M)|(the carrier' of M) & (id(the carrier' of M) *
((Flow M)~|(the carrier' of M))) =
(Flow M)~|(the carrier' of M) &
((Flow M)|(the carrier of M)) *
id(the carrier' of M) = (Flow M)|(the carrier of M) &
((Flow M)~|(the carrier of M)) *
id(the carrier' of M) = (Flow M)~|(the carrier of M) &
(id(the carrier of M)) * ((Flow M)|(the carrier of M)) =
(Flow M)|(the carrier of M) &
(id(the carrier of M)) * ((Flow M)~|(the carrier of M)) =
(Flow M)~|(the carrier of M) &
((Flow M)|(the carrier of M)) * id(the carrier' of M) =
(Flow M)|(the carrier of M) &
((Flow M)~|(the carrier of M)) * id(the carrier' of M) =
(Flow M)~|(the carrier of M) &
(id(the carrier' of M) * ((Flow M)|(the carrier of M))) = {} &
(id(the carrier' of M) * ((Flow M)~|(the carrier of M))) = {} &
((Flow M)|(the carrier of M)) * id(the carrier of M) = {} &
((Flow M)~|(the carrier of M)) * id(the carrier of M) = {} &
(id(the carrier of M)) * ((Flow M)|(the carrier' of M)) = {} &
(id(the carrier of M)) * ((Flow M)~|(the carrier' of M)) = {} &
((Flow M)|(the carrier' of M)) * (id(the carrier' of M)) = {} &
((Flow M)~|(the carrier' of M)) * (id(the carrier' of M)) = {}
proof
A1: rng ((Flow M)|(the carrier' of M)) c= the carrier of M by Th9;
A2: rng ((Flow M)~|(the carrier' of M)) c= the carrier of M by Th9;
A3: rng ((Flow M)|(the carrier of M)) c= the carrier' of M by Th9;
A4: rng ((Flow M)~|(the carrier of M)) c= the carrier' of M by Th9;
A5: dom ((Flow M)|(the carrier of M)) misses
rng (id(the carrier' of M)) by Th10;
A6: dom ((Flow M)~|(the carrier of M)) misses
rng (id(the carrier' of M)) by Th10;
A7: rng ((Flow M)|(the carrier of M)) misses
dom (id(the carrier of M)) by Th10;
A8: rng ((Flow M)~|(the carrier of M)) misses
dom (id(the carrier of M)) by Th10;
A9: rng id(the carrier of M) misses dom ((Flow M)|(the carrier' of M)) by Th10;
A10: rng id(the carrier of M) misses
dom ((Flow M)~|(the carrier' of M)) by Th10;
A11: rng ((Flow M)|(the carrier' of M)) misses
dom id(the carrier' of M) by Th10;
rng ((Flow M)~|(the carrier' of M)) misses dom id(the carrier' of M) by Th10;
hence thesis by A1,A2,A3,A4,A5,A6,A7,A8,A9,A10,A11,RELAT_1:44,51,53,58;
end;
theorem Th13:
((Flow M)~|(the carrier' of M)) misses (id(Elements(M))) &
((Flow M)|(the carrier' of M)) misses (id(Elements(M))) &
((Flow M)~|(the carrier of M)) misses (id(Elements(M))) &
((Flow M)|(the carrier of M)) misses (id(Elements(M)))
proof
set T = id(Elements(M));
thus ((Flow M)~|(the carrier' of M)) misses (id(Elements(M)))
proof
set R = (Flow M)~|(the carrier' of M);
for x,y being object holds not [x,y] in R /\ T
proof
let x,y be object;
assume
A1: [x,y] in R /\ T;
then
A2: [x,y] in R by XBOOLE_0:def 4;
A3: [x,y] in T by A1,XBOOLE_0:def 4;
A4: [x,y] in (Flow M)~ by A2,RELAT_1:def 11;
A5: x in (the carrier' of M) by A2,RELAT_1:def 11;
[y,x] in (Flow M) by A4,RELAT_1:def 7;
then x <> y by A5,Th7;
hence thesis by A3,RELAT_1:def 10;
end;
then R /\ T = {} by RELAT_1:37;
hence thesis by XBOOLE_0:def 7;
end;
thus ((Flow M)|(the carrier' of M)) misses (id(Elements(M)))
proof
set R = (Flow M)|(the carrier' of M);
for x,y being object holds not [x,y] in R /\ T
proof
let x,y be object;
assume
A6: [x,y] in R /\ T;
then
A7: [x,y] in R by XBOOLE_0:def 4;
A8: [x,y] in T by A6,XBOOLE_0:def 4;
A9: x in (the carrier' of M) by A7,RELAT_1:def 11;
[x,y] in (Flow M) by A7,RELAT_1:def 11;
then x <> y by A9,Th7;
hence thesis by A8,RELAT_1:def 10;
end;
then R /\ T = {} by RELAT_1:37;
hence thesis by XBOOLE_0:def 7;
end;
thus ((Flow M)~|(the carrier of M)) misses (id(Elements(M)))
proof
set R = (Flow M)~|(the carrier of M);
for x,y being object holds not [x,y] in R /\ T
proof
let x,y be object;
assume
A10: [x,y] in R /\ T;
then
A11: [x,y] in R by XBOOLE_0:def 4;
A12: [x,y] in T by A10,XBOOLE_0:def 4;
A13: [x,y] in (Flow M)~ by A11,RELAT_1:def 11;
A14: x in the carrier of M by A11,RELAT_1:def 11;
[y,x] in Flow M by A13,RELAT_1:def 7;
then x <> y by A14,Th7;
hence thesis by A12,RELAT_1:def 10;
end;
then R /\ T = {} by RELAT_1:37;
hence thesis by XBOOLE_0:def 7;
end;
set R = (Flow M)|(the carrier of M);
for x,y being object holds not [x,y] in R /\ T
proof
let x,y be object;
assume
A15: [x,y] in R /\ T;
then
A16: [x,y] in R by XBOOLE_0:def 4;
A17: [x,y] in T by A15,XBOOLE_0:def 4;
A18: x in the carrier of M by A16,RELAT_1:def 11;
[x,y] in Flow M by A16,RELAT_1:def 11;
then x <> y by A18,Th7;
hence thesis by A17,RELAT_1:def 10;
end;
then R /\ T = {} by RELAT_1:37;
hence thesis by XBOOLE_0:def 7;
end;
theorem Th14:
((Flow M)~|(the carrier' of M)) \/ (id(the carrier of M)) \ id(Elements(M)) =
(Flow M)~|(the carrier' of M) &
((Flow M)|(the carrier' of M)) \/
(id(the carrier of M)) \ id(Elements(M)) =
(Flow M)|(the carrier' of M) &
(((Flow M)~|(the carrier of M)) \/
(id(the carrier of M))) \ id(Elements(M)) =
(Flow M)~|(the carrier of M) &
(((Flow M)|(the carrier of M)) \/
(id(the carrier of M))) \ id(Elements(M)) =
(Flow M)|(the carrier of M) & ((Flow M)~|(the carrier of M)) \/
(id(the carrier' of M)) \ id(Elements(M)) =
(Flow M)~|(the carrier of M) & ((Flow M)|(the carrier of M)) \/
(id(the carrier' of M)) \ id(Elements(M)) =
(Flow M)|(the carrier of M) &
(((Flow M)~|(the carrier' of M)) \/
(id(the carrier' of M))) \ id(Elements(M)) =
(Flow M)~|(the carrier' of M) &
(((Flow M)|(the carrier' of M)) \/
(id(the carrier' of M))) \ id(Elements(M)) =
(Flow M)|(the carrier' of M)
proof
A1: ((Flow M)~|(the carrier' of M)) \/
(id(the carrier of M)) \ id(Elements(M)) =
(Flow M)~|(the carrier' of M)
proof
set R = (Flow M)~|(the carrier' of M);
set S = id(the carrier of M);
set T = id(Elements(M));
A2: S c= T by SYSREL:15,XBOOLE_1:7;
A3: R misses T by Th13;
(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: ((Flow M)|(the carrier' of M)) \/
(id(the carrier of M)) \ id(Elements(M)) =
(Flow M)|(the carrier' of M)
proof
set R = (Flow M)|(the carrier' of M);
set S = id(the carrier of M);
set T = id(Elements(M));
A5: S c= T by SYSREL:15,XBOOLE_1:7;
A6: R misses T by Th13;
(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: ((Flow M)~|(the carrier of M)) \/ (id(the carrier of M)) \ id(Elements(M))
= (Flow M)~|(the carrier of M)
proof
set R = (Flow M)~|(the carrier of M);
set S = id(the carrier of M);
set T = id(Elements(M));
A8: S c= T by SYSREL:15,XBOOLE_1:7;
A9: R misses T by Th13;
(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: ((Flow M)|(the carrier of M)) \/
(id(the carrier of M)) \ id(Elements(M)) = (Flow M)|(the carrier of M)
proof
set R = (Flow M)|(the carrier of M);
set S = id(the carrier of M);
set T = id(Elements(M));
A11: S c= T by SYSREL:15,XBOOLE_1:7;
A12: R misses T by Th13;
(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: ((Flow M)~|(the carrier of M)) \/
(id(the carrier' of M)) \ id(Elements(M)) =
(Flow M)~|(the carrier of M)
proof
set R = (Flow M)~|(the carrier of M);
set S = id(the carrier' of M);
set T = id(Elements(M));
A14: S c= T by SYSREL:15,XBOOLE_1:7;
A15: R misses T by Th13;
(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: ((Flow M)|(the carrier of M)) \/
(id(the carrier' of M)) \ id(Elements(M)) =
(Flow M)|(the carrier of M)
proof
set R = (Flow M)|(the carrier of M);
set S = id(the carrier' of M);
set T = id(Elements(M));
A17: S c= T by SYSREL:15,XBOOLE_1:7;
A18: R misses T by Th13;
(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: ((Flow M)~|(the carrier' of M)) \/
(id(the carrier' of M)) \ id(Elements(M)) =
(Flow M)~|(the carrier' of M)
proof
set R = (Flow M)~|(the carrier' of M);
set S = id(the carrier' of M);
set T = id(Elements(M));
A20: S c= T by SYSREL:15,XBOOLE_1:7;
A21: R misses T by Th13;
(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;
((Flow M)|(the carrier' of M)) \/ (id(the carrier' of M)) \ id(Elements(M)) =
(Flow M)|(the carrier' of M)
proof
set R = (Flow M)|(the carrier' of M);
set S = id(the carrier' of M);
set T = id(Elements(M));
A22: S c= T by SYSREL:15,XBOOLE_1:7;
A23: R misses T by Th13;
(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 Th15:
((Flow M)|(the carrier of M))~ = ((Flow M)~)|(the carrier' of M) &
((Flow M)|(the carrier' of M))~ =
((Flow M)~)|(the carrier of M)
proof
set R = Flow M;
set X = the carrier of M;
set Y = the carrier' of M;
for x,y being object holds [x,y] in (R|X)~ implies [x,y] in (R~)|Y
proof
let x,y be object;
assume [x,y] in (R|X)~;
then
A1: [y,x] in R|X by RELAT_1:def 7;
then
A2: [y,x] in R by RELAT_1:def 11;
A3: y in X by A1,RELAT_1:def 11;
A4: [x,y] in R~ by A2,RELAT_1:def 7;
x in Y by A2,A3,Th7;
hence thesis by A4,RELAT_1:def 11;
end;
then
A5: ((R|X)~) c= ((R~)|Y) by RELAT_1:def 3;
for x,y being object holds [x,y] in (R~)|Y implies [x,y] in (R|X)~
proof
let x,y be object;
assume
A6: [x,y] in (R~)|Y;
then [x,y] in R~ by RELAT_1:def 11;
then
A7: [y,x] in R by RELAT_1:def 7;
x in Y by A6,RELAT_1:def 11;
then y in X by A7,Th7;
then [y,x] in R|X by A7,RELAT_1:def 11;
hence thesis by RELAT_1:def 7;
end;
then
A8: ((R~)|Y) c= ((R|X)~) by RELAT_1:def 3;
for x,y being object holds [x,y] in (R|Y)~ implies [x,y] in (R~)|X
proof
let x,y be object;
assume [x,y] in (R|Y)~;
then
A9: [y,x] in R|Y by RELAT_1:def 7;
then
A10: [y,x] in R by RELAT_1:def 11;
A11: y in Y by A9,RELAT_1:def 11;
A12: [x,y] in R~ by A10,RELAT_1:def 7;
x in X by A10,A11,Th7;
hence thesis by A12,RELAT_1:def 11;
end;
then
A13: ((R|Y)~) c= ((R~)|X) by RELAT_1:def 3;
for x,y being object holds [x,y] in (R~)|X implies [x,y] in (R|Y)~
proof
let x,y be object;
assume
A14: [x,y] in (R~)|X;
then [x,y] in R~ by RELAT_1:def 11;
then
A15: [y,x] in R by RELAT_1:def 7;
x in X by A14,RELAT_1:def 11;
then y in Y by A15,Th7;
then [y,x] in R|Y by A15,RELAT_1:def 11;
hence thesis by RELAT_1:def 7;
end;
then ((R~)|X) c= ((R|Y)~) by RELAT_1:def 3;
hence thesis by A5,A8,A13,XBOOLE_0:def 10;
end;
theorem Th16:
((Flow M)|(the carrier of M)) \/ ((Flow M)|(the carrier' of M)) = (Flow M) &
((Flow M)|(the carrier' of M)) \/
((Flow M)|(the carrier of M)) = (Flow M) &
(((Flow M)|(the carrier of M))~) \/
(((Flow M)|(the carrier' of M))~) = (Flow M)~ &
(((Flow M)|(the carrier' of M))~) \/
(((Flow M)|(the carrier of M))~) = (Flow M)~
proof
set R = Flow M;
Flow M c= [:Elements(M),Elements(M):] by Th8;
then (R|the carrier of M) \/ (R|the carrier' of M) = R by SYSREL:9;
hence thesis by RELAT_1:23;
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
((Flow M)~|(the carrier' of M)) \/ id(the carrier of M);
correctness;
func f_exit(M) -> Relation equals
((Flow M)|(the carrier' of M)) \/ id(the carrier of M);
correctness;
end;
theorem
f_exit(M) c= [:Elements(M),Elements(M):] &
f_enter(M) c= [:Elements(M),Elements(M):]
proof
A1: id(the carrier of M) c= id(Elements(M)) by SYSREL:15,XBOOLE_1:7;
id(Elements(M)) c= [:Elements(M),Elements(M):] by RELSET_1:13;
then
A2: id(the carrier of M) c= [:Elements(M),Elements(M):] by A1,XBOOLE_1:1;
A3: (Flow M)|(the carrier' of M) c= (Flow M) by RELAT_1:59;
(Flow M) c= [:Elements(M),Elements(M):] by Th8;
then (Flow M)|(the carrier' of M) c= [:Elements(M),Elements(M):]
by A3,XBOOLE_1:1;
hence f_exit(M) c= [:Elements(M),Elements(M):] by A2,XBOOLE_1:8;
A4: id(the carrier of M) c= id(Elements(M)) by SYSREL:15,XBOOLE_1:7;
id(Elements(M)) c= [:Elements(M),Elements(M):] by RELSET_1:13;
then
A5: id(the carrier of M) c= [:Elements(M),Elements(M):] by A4,XBOOLE_1:1;
A6: ( Flow M)~|(the carrier' of M) c= (Flow M)~ by RELAT_1:59;
(Flow M)~ c= [:Elements(M),Elements(M):] by Th8;
then (Flow M)~|(the carrier' of M) c= [:Elements(M),Elements(M):]
by A6,XBOOLE_1:1;
hence thesis by A5,XBOOLE_1:8;
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 being object holds x in dom(f_exit(M)) implies x in Elements(M)
proof
let x be object;
assume x in dom(f_exit(M));
then x in dom((Flow M)|(the carrier' of M)) \/
dom(id(the carrier of M)) by XTUPLE_0:23;
then x in dom((Flow M)|(the carrier' of M)) or
x in dom(id(the carrier of M)) by XBOOLE_0:def 3;
then x in (the carrier' of M) or x in the carrier of M by RELAT_1:57;
hence thesis by XBOOLE_0:def 3;
end;
A2: for x being object holds x in rng(f_exit(M)) implies x in Elements(M)
proof
let x be object;
assume x in rng(f_exit(M));
then
A3: x in rng((Flow M)|(the carrier' of M)) \/
rng(id(the carrier of M)) by RELAT_1:12;
A4: x in rng((Flow M)|(the carrier' of M)) implies thesis
proof
assume x in rng((Flow M)|(the carrier' of M));
then consider y being object such that
A5: [y,x] in (Flow M)|(the carrier' of M) by XTUPLE_0:def 13;
A6: y in (the carrier' of M) by A5,RELAT_1:def 11;
[y,x] in (Flow M) by A5,RELAT_1:def 11;
then x in (the carrier' of M) or x in the carrier of M by A6,Th7;
hence thesis by XBOOLE_0:def 3;
end;
x in rng(id(the carrier of M)) implies thesis by XBOOLE_0:def 3;
hence thesis by A3,A4,XBOOLE_0:def 3;
end;
A7: for x being object holds x in dom(f_enter(M)) implies x in Elements(M)
proof
let x be object;
assume x in dom(f_enter(M));
then x in dom((Flow M)~|(the carrier' of M)) \/
dom(id(the carrier of M)) by XTUPLE_0:23;
then x in dom((Flow M)~|(the carrier' of M)) or
x in dom(id(the carrier of M)) by XBOOLE_0:def 3;
then x in (the carrier' of M) or x in the carrier of M by RELAT_1:57;
hence thesis by XBOOLE_0:def 3;
end;
for x being object holds x in rng(f_enter(M)) implies x in Elements(M)
proof
let x be object;
assume x in rng(f_enter(M));
then
A8: x in rng((Flow M)~|(the carrier' of M)) \/
rng(id(the carrier of M)) by RELAT_1:12;
A9: x in rng((Flow M)~|(the carrier' of M)) implies thesis
proof
assume x in rng((Flow M)~|(the carrier' of M));
then consider y being object such that
A10: [y,x] in (Flow M)~|(the carrier' of M) by XTUPLE_0:def 13;
A11: [y,x] in (Flow M)~ by A10,RELAT_1:def 11;
A12: y in (the carrier' of M) by A10,RELAT_1:def 11;
[x,y] in (Flow M) by A11,RELAT_1:def 7;
then x in (the carrier' of M) or x in the carrier of M by A12,Th7;
hence thesis by XBOOLE_0:def 3;
end;
x in rng(id(the carrier of M)) implies thesis by XBOOLE_0:def 3;
hence thesis by A8,A9,XBOOLE_0:def 3;
end;
hence thesis by A1,A2,A7,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 = ((Flow M)|(the carrier' of M));
set S = id(the carrier of M);
A2: S * R = {} by Th12;
A3: R * S = R by Th12;
A4: S * S = S by SYSREL:12;
(f_exit(M)) * (f_exit(M)) = (R * (R \/ S)) \/ (S * (R \/ S)) by SYSREL:6
.= ((R * R) \/ (R * S)) \/ (S * (R \/ S)) by RELAT_1:32
.= ((R * R) \/ (R * S)) \/ ((S * R) \/ (S * S)) by RELAT_1:32
.= ({} \/ R) \/ ({} \/ S) by A2,A3,A4,Th11
.= f_exit(M);
hence thesis;
end;
A5: (f_exit(M)) * (f_enter(M)) = f_exit(M)
proof
set R = ((Flow M)|(the carrier' of M));
set S = id(the carrier of M);
set T = ((Flow M)~|(the carrier' of M));
A6: S * T = {} by Th12;
A7: R * S = R by Th12;
A8: S * S = S by SYSREL:12;
(f_exit(M)) * (f_enter(M)) = (R * (T \/ S)) \/ (S * (T \/ S)) by SYSREL:6
.= ((R * T) \/ (R * S)) \/ (S * (T \/ S)) by RELAT_1:32
.= ((R * T) \/ (R * S)) \/ ((S * T) \/ (S * S)) by RELAT_1:32
.= ({} \/ R) \/ ({} \/ S) by A6,A7,A8,Th11
.=f_exit(M);
hence thesis;
end;
A9: (f_enter(M)) * (f_enter(M)) = f_enter(M)
proof
set R = ((Flow M)~|(the carrier' of M));
set S = id(the carrier of M);
A10: S * R = {} by Th12;
A11: R * S = R by Th12;
A12: S * S = S by SYSREL:12;
(f_enter(M)) * (f_enter(M)) = (R * (R \/ S)) \/ (S * (R \/ S)) by SYSREL:6
.= ((R * R) \/ (R * S)) \/ (S * (R \/ S)) by RELAT_1:32
.= ((R * R) \/ (R * S)) \/ ((S * R) \/ (S * S)) by RELAT_1:32
.= ({} \/ R) \/ ({} \/ S) by A10,A11,A12,Th11
.=f_enter(M);
hence thesis;
end;
(f_enter(M)) * (f_exit(M)) = f_enter(M)
proof
set R = ((Flow M)|(the carrier' of M));
set S = id(the carrier of M);
set T = ((Flow M)~|(the carrier' of M));
A13: T * S = T by Th12;
A14: S * R = {} by Th12;
A15: S * S = S by SYSREL:12;
(f_enter(M)) * (f_exit(M)) = (T * (R \/ S)) \/ (S * (R \/ S)) by SYSREL:6
.= ((T * R) \/ (T * S)) \/ (S * (R \/ S)) by RELAT_1:32
.= ((T * R) \/ (T * S)) \/ ((S * R) \/ (S * S)) by RELAT_1:32
.= ({} \/ T) \/ ({} \/ S) by A13,A14,A15,Th11
.=f_enter(M);
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 carrier of M);
thus (f_exit(M)) * (f_exit(M) \ id(Elements(M))) = {}
proof
set R = (Flow M)|(the carrier' of M);
A1: S * R = {} by Th12;
(f_exit(M)) * (f_exit(M) \ id(Elements(M))) = (R \/ S) * R by Th14
.= (R * R) \/ (S * R) by SYSREL:6
.= {} by A1,Th11;
hence thesis;
end;
set R = ((Flow M)~|(the carrier' of M));
A2: S * R = {} by Th12;
(f_enter(M)) * (f_enter(M) \ id(Elements(M))) = (R \/ S) * R by Th14
.= (R * R) \/ (S * R) by SYSREL:6
.= {} by A2,Th11;
hence thesis;
end;
::B [F ->R]
definition
let M;
func f_prox(M) -> Relation equals
((Flow M)|(the carrier of M) \/
(Flow M)~|(the carrier of M)) \/ id(the carrier of M);
correctness;
func f_flow(M) -> Relation equals
(Flow 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 = (Flow M)|(the carrier of M);
set S = (Flow M)~|(the carrier of M);
set T = id(the carrier of M);
set Q = id(Elements(M));
A1: ((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 Th14
.= R \/ S by Th14;
A2: (R \/ S) * (R \/ S) = ((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
.= ({} \/ (S * R)) \/ ((R * S) \/ (S *S)) by Th11
.= ({} \/ {}) \/ ((R * S) \/ (S *S)) by Th11
.= ({} \/ {}) \/ ({} \/ (S *S)) by Th11
.= {} by Th11;
A3: R \/ S~ = R \/ (((Flow M)|(the carrier' of M))~)~ by Th15
.= Flow M by Th16;
A4: R~ \/ S = R~ \/ ((Flow M)|(the carrier' of M))~ by Th15
.= (Flow M)~ by Th16;
A5: (R \/ S)~ \/ (R \/ S) = (R~ \/ S~) \/ (R \/ S) by RELAT_1:23
.= (R~ \/ (S \/ R)) \/ S~ by XBOOLE_1:4
.= ((R~ \/ S) \/ R) \/ S~ by XBOOLE_1:4
.= (Flow M) \/ (Flow M)~ by A3,A4,XBOOLE_1:4;
A6: f_prox(M) \/ (f_prox(M))~ =
((R \/ S) \/ T) \/ ((R \/ S)~ \/ T~) by RELAT_1:23
.= (((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)
.= ((Flow M) \/ (Flow M)~) \/ id(the carrier of M) by A5;
A7: id(the carrier of M) c= id(Elements(M)) by SYSREL:15,XBOOLE_1:7;
A8: f_prox(M) * f_prox(M) = (((R \/ S) \/ T) * (R \/ S)) \/
(((R \/ S) \/ T) * T) by RELAT_1:32
.= ((((R \/ S) \/ T) * R ) \/ (((R \/ S) \/ T) * S)) \/
(((R \/ S) \/ T) * T) by RELAT_1:32
.= (((R \/ S) * R ) \/ (T * R )) \/
(((R \/ S) \/ T) * S) \/ (((R \/ S) \/ T) * T) by SYSREL:6
.= (((R * R) \/ (S * R)) \/ (T * R )) \/ (((R \/ S) \/ T) * S) \/
(((R \/ S) \/ T) * T) by SYSREL:6
.= (((R * R) \/ (S * R)) \/ (T * R )) \/
(((R \/ S) * S) \/ (T * S)) \/ (((R \/ S) \/ T) * T) by SYSREL:6
.= (((R * R) \/ (S * R)) \/ (T * R )) \/
(((R * S) \/ (S * S)) \/ (T * S)) \/ (((R \/ S) \/ T) * T) by SYSREL:6
.= (((R * R) \/ (S * R)) \/ (T * R )) \/
(((R * S) \/ (S * S)) \/ (T * S)) \/
(((R \/ S) * T) \/ (T * T)) by SYSREL:6
.= (((R * R) \/ (S * R)) \/ (T * R )) \/
(((R * S) \/ (S * S)) \/ (T * S)) \/
(((R * T) \/ (S * T)) \/ (T * T)) by SYSREL:6
.= (({} \/ (S * R)) \/ (T * R )) \/ (((R * S) \/ (S * S)) \/ (T * S)) \/
(((R * T) \/ (S * T)) \/ (T * T)) by Th11
.= (({} \/ {}) \/ (T * R )) \/
(((R * S) \/ (S * S)) \/ (T * S)) \/
(((R * T) \/ (S * T)) \/ (T * T)) by Th11
.= (({} \/ {}) \/ (T * R )) \/
(({} \/ (S * S)) \/ (T * S)) \/ (((R * T) \/ (S * T)) \/ (T * T)) by Th11
.= (T * R ) \/ ({} \/ (T * S)) \/
(((R * T) \/ (S * T)) \/ (T * T)) by Th11
.= R \/ (T * S) \/
(((R * T) \/ (S * T)) \/ (T * T)) by Th12
.= R \/ S \/ (((R * T) \/ (S * T)) \/ (T * T)) by Th12
.= R \/ S \/ (((R * T) \/ (S * T)) \/ T) by SYSREL:12
.= R \/ S \/ (({} \/ (S * T)) \/ T) by Th12
.= R \/ S \/ ({} \/ T) by Th12
.= f_prox(M);
A9: (f_prox(M) \ id(Elements(M))) * f_prox(M) = {} \/ ((R \/ S) * T) by A1,A2,
RELAT_1:32
.= (R * T) \/ (S * T) by SYSREL:6
.= {} \/ (S * T) by Th12
.= {} by Th12;
(f_prox(M) \/ (f_prox(M))~) \/ id(Elements(M)) =
(((Flow M) \/ (Flow M)~) \/ (id(the carrier of M) \/
id(Elements(M)))) by A6,XBOOLE_1:4
.= (((Flow M) \/ (Flow M)~) \/ id(Elements(M)))
by A7,XBOOLE_1:12
.= ((Flow M) \/ id(Elements(M))) \/
((Flow M)~ \/ id(Elements(M))) by XBOOLE_1:5
.= ((Flow M) \/ id(Elements(M))) \/
((Flow M)~ \/ (id(Elements(M)))~)
.= f_flow(M) \/ (f_flow(M))~ by RELAT_1:23;
hence thesis by A8,A9;
end;
::C [F ->P]
definition
let M;
func f_places(M) -> set equals
the carrier of M;
correctness;
func f_transitions(M) -> set equals
the carrier' of M;
correctness;
func f_pre(M) -> Relation equals
(Flow M)|(the carrier' of M);
correctness;
func f_post(M) -> Relation equals
(Flow M)~|(the carrier' 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 being object holds [x,y] in f_pre(M) implies
[x,y] in [:f_transitions(M),f_places(M):]
proof
let x,y be object;
assume
A2: [x,y] in f_pre(M);
then
A3: x in (the carrier' of M) by RELAT_1:def 11;
[x,y] in (Flow M) by A2,RELAT_1:def 11;
then y in (the carrier of M) by A3,Th7;
hence thesis by A3,ZFMISC_1:87;
end;
for x,y being object holds [x,y] in f_post(M) implies
[x,y] in [:f_transitions(M),f_places(M):]
proof
let x,y be object;
assume
A4: [x,y] in f_post(M);
then
A5: [x,y] in (Flow M)~ by RELAT_1:def 11;
A6: x in (the carrier' of M) by A4,RELAT_1:def 11;
[y,x] in (Flow M) by A5,RELAT_1:def 7;
then y in (the carrier of M) by A6,Th7;
hence thesis by A6,ZFMISC_1:87;
end;
hence thesis by A1,RELAT_1:def 3;
end;
theorem
f_prox(M) c= [:Elements(M), Elements(M):] &
f_flow(M) c= [:Elements(M), Elements(M):]
proof
A1: (Flow M)|(the carrier of M) c= Flow M by RELAT_1:59;
Flow M c= [:Elements(M), Elements(M):] by Th8;
then
A2: (Flow M)|(the carrier of M) c= [:Elements(M), Elements(M):]
by A1,XBOOLE_1:1;
A3: (Flow M)~|(the carrier of M) c= (Flow M)~ by RELAT_1:59;
(Flow M)~ c= [:Elements(M), Elements(M):] by Th8;
then
A4: (Flow M)~|(the carrier of M) c= [:Elements(M), Elements(M):]
by A3,XBOOLE_1:1;
the carrier of M c= Elements(M) by XBOOLE_1:7;
then
A5: [:the carrier of M, the carrier of M:] c=
[:Elements(M), Elements(M):] by ZFMISC_1:96;
id(the carrier of M) c= [:the carrier of M, the carrier of M:]
by RELSET_1:13;
then
A6: id(the carrier of M) c= [:Elements(M), Elements(M):] by A5,XBOOLE_1:1;
(Flow M)|(the carrier of M) \/
(Flow M)~|(the carrier of M) c= [:Elements(M), Elements(M):]
by A2,A4,XBOOLE_1:8;
hence f_prox(M) c= [:Elements(M), Elements(M):] by A6,XBOOLE_1:8;
A7: Flow M c= [:Elements(M), Elements(M):] by Th8;
id(Elements(M)) c= [:Elements(M), Elements(M):] by RELSET_1:13;
hence thesis by A7,XBOOLE_1:8;
end;
::A [F -> E]
definition
let M;
func f_entrance(M) -> Relation equals
((Flow M)~|(the carrier of M)) \/ id(the carrier' of M);
correctness;
func f_escape(M) -> Relation equals
((Flow M)|(the carrier of M)) \/ id(the carrier' of M);
correctness;
end;
theorem
f_escape(M) c= [:Elements(M),Elements(M):] &
f_entrance(M) c= [:Elements(M),Elements(M):]
proof
A1: id(the carrier' of M) c= id(Elements(M)) by SYSREL:15,XBOOLE_1:7;
id(Elements(M)) c= [:Elements(M),Elements(M):] by RELSET_1:13;
then
A2: id(the carrier' of M) c= [:Elements(M),Elements(M):] by A1,XBOOLE_1:1;
A3: (Flow M)|(the carrier of M) c= (Flow M) by RELAT_1:59;
(Flow M) c= [:Elements(M),Elements(M):] by Th8;
then (Flow M)|(the carrier of M) c= [:Elements(M),Elements(M):]
by A3,XBOOLE_1:1;
hence f_escape(M) c= [:Elements(M),Elements(M):] by A2,XBOOLE_1:8;
A4: id(the carrier' of M) c= id(Elements(M)) by SYSREL:15,XBOOLE_1:7;
id(Elements(M)) c= [:Elements(M),Elements(M):] by RELSET_1:13;
then
A5: id(the carrier' of M) c= [:Elements(M),Elements(M):] by A4,XBOOLE_1:1;
A6: (Flow M)~|(the carrier of M) c= (Flow M)~ by RELAT_1:59;
(Flow M)~ c= [:Elements(M),Elements(M):] by Th8;
then (Flow M)~|(the carrier of M) c= [:Elements(M),Elements(M):]
by A6,XBOOLE_1:1;
hence thesis by A5,XBOOLE_1:8;
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 being object holds x in dom(f_escape(M)) implies x in Elements(M)
proof
let x be object;
assume x in dom(f_escape(M));
then x in dom((Flow M)|(the carrier of M)) \/
dom(id(the carrier' of M)) by XTUPLE_0:23;
then x in dom((Flow M)|(the carrier of M)) or
x in dom(id(the carrier' of M)) by XBOOLE_0:def 3;
then x in (the carrier of M) or x in the carrier' of M by RELAT_1:57;
hence thesis by XBOOLE_0:def 3;
end;
A2: for x being object holds x in rng(f_escape(M)) implies x in Elements(M)
proof
let x be object;
assume x in rng(f_escape(M));
then
A3: x in rng((Flow M)|(the carrier of M)) \/
rng(id(the carrier' of M)) by RELAT_1:12;
A4: x in rng((Flow M)|(the carrier of M)) implies thesis
proof
assume x in rng((Flow M)|(the carrier of M));
then consider y being object such that
A5: [y,x] in (Flow M)|(the carrier of M) by XTUPLE_0:def 13;
A6: y in (the carrier of M) by A5,RELAT_1:def 11;
[y,x] in (Flow M) by A5,RELAT_1:def 11;
then x in (the carrier of M) or x in the carrier' of M by A6,Th7;
hence thesis by XBOOLE_0:def 3;
end;
x in rng(id(the carrier' of M)) implies thesis by XBOOLE_0:def 3;
hence thesis by A3,A4,XBOOLE_0:def 3;
end;
A7: for x being object holds x in dom(f_entrance(M)) implies x in Elements(M)
proof
let x be object;
assume x in dom(f_entrance(M));
then x in dom((Flow M)~|(the carrier of M)) \/
dom(id(the carrier' of M)) by XTUPLE_0:23;
then x in dom((Flow M)~|(the carrier of M)) or
x in dom(id(the carrier' of M)) by XBOOLE_0:def 3;
then x in (the carrier of M) or x in the carrier' of M by RELAT_1:57;
hence thesis by XBOOLE_0:def 3;
end;
for x being object holds x in rng(f_entrance(M)) implies x in Elements(M)
proof
let x be object;
assume x in rng(f_entrance(M));
then
A8: x in rng((Flow M)~|(the carrier of M)) \/
rng(id(the carrier' of M)) by RELAT_1:12;
A9: x in rng((Flow M)~|(the carrier of M)) implies thesis
proof
assume x in rng((Flow M)~|(the carrier of M));
then consider y being object such that
A10: [y,x] in (Flow M)~|(the carrier of M) by XTUPLE_0:def 13;
A11: [y,x] in (Flow M)~ by A10,RELAT_1:def 11;
A12: y in (the carrier of M) by A10,RELAT_1:def 11;
[x,y] in (Flow M) by A11,RELAT_1:def 7;
then x in (the carrier of M) or x in the carrier' of M by A12,Th7;
hence thesis by XBOOLE_0:def 3;
end;
x in rng(id(the carrier' of M)) implies thesis by XBOOLE_0:def 3;
hence thesis by A8,A9,XBOOLE_0:def 3;
end;
hence thesis by A1,A2,A7,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 = ((Flow M)|(the carrier of M));
set S = id(the carrier' of M);
A1: S * R = {} by Th12;
A2: R * S = R by Th12;
A3: S * S = S by SYSREL:12;
A4: (f_escape(M)) * (f_escape(M)) =
(R * (R \/ S)) \/ (S * (R \/ S)) by SYSREL:6
.= ((R * R) \/ (R * S)) \/ (S * (R \/ S)) by RELAT_1:32
.= ((R * R) \/ (R * S)) \/ ((S * R) \/ (S * S)) by RELAT_1:32
.= ({} \/ R) \/ ({} \/ S) by A1,A2,A3,Th11
.=f_escape(M);
A5: (f_escape(M)) * (f_entrance(M)) = f_escape(M)
proof
set T = ((Flow M)~|(the carrier of M));
A6: S * T = {} by Th12;
A7: R * S = R by Th12;
A8: S * S = S by SYSREL:12;
(f_escape(M)) * (f_entrance(M)) =
(R * (T \/ S)) \/ (S * (T \/ S)) by SYSREL:6
.= ((R * T) \/ (R * S)) \/ (S * (T \/ S)) by RELAT_1:32
.= ((R * T) \/ (R * S)) \/ ((S * T) \/ (S * S)) by RELAT_1:32
.= ({} \/ R) \/ ({} \/ S) by A6,A7,A8,Th11
.=f_escape(M);
hence thesis;
end;
A9: (f_entrance(M)) * (f_entrance(M)) = f_entrance(M)
proof
set R = ((Flow M)~|(the carrier of M));
A10: S * R = {} by Th12;
A11: R * S = R by Th12;
A12: S * S = S by SYSREL:12;
(f_entrance(M)) * (f_entrance(M)) =
(R * (R \/ S)) \/ (S * (R \/ S)) by SYSREL:6
.= ((R * R) \/ (R * S)) \/ (S * (R \/ S)) by RELAT_1:32
.= ((R * R) \/ (R * S)) \/ ((S * R) \/ (S * S)) by RELAT_1:32
.= ({} \/ R) \/ ({} \/ S) by A10,A11,A12,Th11
.=f_entrance(M);
hence thesis;
end;
(f_entrance(M)) * (f_escape(M)) = f_entrance(M)
proof
set T = ((Flow M)~|(the carrier of M));
A13: T * S = T by Th12;
A14: S * R = {} by Th12;
A15: S * S = S by SYSREL:12;
(f_entrance(M)) * (f_escape(M)) =
(T * (R \/ S)) \/ (S * (R \/ S)) by SYSREL:6
.= ((T * R) \/ (T * S)) \/ (S * (R \/ S)) by RELAT_1:32
.= ((T * R) \/ (T * S)) \/ ((S * R) \/ (S * S)) by RELAT_1:32
.= ({} \/ T) \/ ({} \/ S) by A13,A14,A15,Th11
.=f_entrance(M);
hence thesis;
end;
hence thesis by A4,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 = (Flow M)|(the carrier of M);
set S = id(the carrier' of M);
A1: S * R = {} by Th12;
(f_escape(M)) * (f_escape(M) \ id(Elements(M))) = (R \/ S) * R by Th14
.= (R * R) \/ (S * R) by SYSREL:6
.= {} by A1,Th11;
hence (f_escape(M)) * (f_escape(M) \ id(Elements(M))) = {};
set R = ((Flow M)~|(the carrier of M));
A2: S * R = {} by Th12;
(f_entrance(M)) * (f_entrance(M) \ id(Elements(M))) = (R \/ S) * R by Th14
.= (R * R) \/ (S * R) by SYSREL:6
.= {} by A2,Th11;
hence thesis;
end;
::B [F ->R]
notation
let M;
synonym f_circulation(M) for f_flow(M);
end;
definition
let M;
func f_adjac(M) -> Relation equals
((Flow M)|(the carrier' of M) \/
(Flow M)~|(the carrier' of M)) \/ id(the carrier' of M);
correctness;
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 = (Flow M)|(the carrier' of M);
set S = (Flow M)~|(the carrier' of M);
set T = id(the carrier' of M);
set Q = id(Elements(M));
A1: ((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 Th14
.= R \/ S by Th14;
A2: (R \/ S) * (R \/ S) = ((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
.= ({} \/ (S * R)) \/ ((R * S) \/ (S *S)) by Th11
.= ({} \/ {}) \/ ((R * S) \/ (S *S)) by Th11
.= ({} \/ {}) \/ ({} \/ (S *S)) by Th11
.= {} by Th11;
A3: R \/ S~ = R \/ (((Flow M)|(the carrier of M))~)~ by Th15
.= Flow M by Th16;
A4: R~ \/ S = R~ \/ ((Flow M)|(the carrier of M))~ by Th15
.= (Flow M)~ by Th16;
A5: (R \/ S)~ \/ (R \/ S) = (R~ \/ S~) \/ (R \/ S) by RELAT_1:23
.= (R~ \/ (S \/ R)) \/ S~ by XBOOLE_1:4
.= ((R~ \/ S) \/ R) \/ S~ by XBOOLE_1:4
.= (Flow M) \/ (Flow M)~ by A3,A4,XBOOLE_1:4;
A6: f_adjac(M) \/ (f_adjac(M))~ =
((R \/ S) \/ T) \/ ((R \/ S)~ \/ T~) by RELAT_1:23
.= (((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)
.= ((Flow M) \/ (Flow M)~) \/
id(the carrier' of M) by A5;
A7: id(the carrier' of M) c= id(Elements(M)) by SYSREL:15,XBOOLE_1:7;
A8: f_adjac(M) * f_adjac(M) =
(((R \/ S) \/ T) * (R \/ S)) \/ (((R \/ S) \/ T) * T) by RELAT_1:32
.= ((((R \/ S) \/ T) * R ) \/ (((R \/ S) \/ T) * S)) \/
(((R \/ S) \/ T) * T) by RELAT_1:32
.= (((R \/ S) * R ) \/ (T * R )) \/ (((R \/ S) \/ T) * S) \/
(((R \/ S) \/ T) * T) by SYSREL:6
.= (((R * R) \/ (S * R)) \/ (T * R )) \/ (((R \/ S) \/ T) * S) \/
(((R \/ S) \/ T) * T) by SYSREL:6
.= (((R * R) \/ (S * R)) \/ (T * R )) \/ (((R \/ S) * S) \/ (T * S)) \/
(((R \/ S) \/ T) * T) by SYSREL:6
.= (((R * R) \/ (S * R)) \/ (T * R )) \/ (((R * S) \/ (S * S)) \/ (T * S))
\/ (((R \/ S) \/ T) * T) by SYSREL:6
.= (((R * R) \/ (S * R)) \/ (T * R )) \/ (((R * S) \/ (S * S)) \/ (T * S))
\/ (((R \/ S) * T) \/ (T * T)) by SYSREL:6
.= (((R * R) \/ (S * R)) \/ (T * R )) \/ (((R * S) \/ (S * S)) \/ (T * S))
\/ (((R * T) \/ (S * T)) \/ (T * T)) by SYSREL:6
.= (({} \/ (S * R)) \/ (T * R )) \/ (((R * S) \/ (S * S)) \/ (T * S)) \/
(((R * T) \/ (S * T)) \/ (T * T)) by Th11
.= (({} \/ {}) \/ (T * R )) \/ (((R * S) \/ (S * S)) \/ (T * S)) \/
(((R * T) \/ (S * T)) \/ (T * T)) by Th11
.= (({} \/ {}) \/ (T * R )) \/ (({} \/ (S * S)) \/ (T * S)) \/
(((R * T) \/ (S * T)) \/ (T * T)) by Th11
.= (T * R ) \/ ({} \/ (T * S)) \/ (((R * T) \/ (S * T)) \/ (T * T)) by Th11
.= R \/ (T * S) \/ (((R * T) \/ (S * T)) \/ (T * T)) by Th12
.= R \/ S \/ (((R * T) \/ (S * T)) \/ (T * T)) by Th12
.= R \/ S \/ (((R * T) \/ (S * T)) \/ T) by SYSREL:12
.= R \/ S \/ (({} \/ (S * T)) \/ T) by Th12
.= R \/ S \/ ({} \/ T) by Th12
.= f_adjac(M);
A9: (f_adjac(M) \ id(Elements(M))) * f_adjac(M) = {} \/ ((R \/ S) * T) by A1,A2
,RELAT_1:32
.= (R * T) \/ (S * T) by SYSREL:6
.= {} \/ (S * T) by Th12
.= {} by Th12;
(f_adjac(M) \/ (f_adjac(M))~) \/ id(Elements(M)) =
(((Flow M) \/ (Flow M)~) \/
(id(the carrier' of M) \/ id(Elements(M)))) by A6,XBOOLE_1:4
.= (((Flow M) \/ (Flow M)~) \/ id(Elements(M)))
by A7,XBOOLE_1:12
.= ((Flow M) \/ id(Elements(M))) \/
((Flow M)~ \/ id(Elements(M))) by XBOOLE_1:5
.= ((Flow M) \/ id(Elements(M))) \/
((Flow M)~ \/ (id(Elements(M)))~)
.= f_circulation(M) \/ (f_circulation(M))~ by RELAT_1:23;
hence thesis by A8,A9;
end;