Journal of Formalized Mathematics
Volume 4, 1992
University of Bialystok
Copyright (c) 1992
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Waldemar Korczynski
- Received January 31, 1992
- MML identifier: FF_SIEC
- [
Mizar article,
MML identifier index
]
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;
begin :: F - Nets
reserve x,y,X,Y for set;
definition
let N be Net;
canceled;
func chaos(N) -> set equals
:: FF_SIEC:def 2
Elements(N) \/ {Elements(N)};
end;
reserve M for Pnet;
definition let X,Y;
assume X misses Y;
canceled;
func PTempty_f_net(X,Y) -> strict Pnet equals
:: FF_SIEC:def 4
Net (# X, Y, {} #);
end;
definition let X;
func Tempty_f_net(X) -> strict Pnet equals
:: FF_SIEC:def 5
PTempty_f_net(X,{});
func Pempty_f_net(X) -> strict Pnet equals
:: FF_SIEC:def 6
PTempty_f_net({},X);
end;
definition let x;
func Tsingle_f_net(x) -> strict Pnet equals
:: FF_SIEC:def 7
PTempty_f_net({},{x});
func Psingle_f_net(x) -> strict Pnet equals
:: FF_SIEC:def 8
PTempty_f_net({x},{});
end;
definition
func empty_f_net -> strict Pnet equals
:: FF_SIEC:def 9
PTempty_f_net({},{});
end;
canceled;
theorem :: FF_SIEC:2
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) = {};
theorem :: FF_SIEC:3
the Places of Tempty_f_net(X) = X &
the Transitions of Tempty_f_net(X) = {} &
the Flow of Tempty_f_net(X) = {};
theorem :: FF_SIEC:4
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) = {};
theorem :: FF_SIEC:5
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)) = {};
theorem :: FF_SIEC:6
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)) = {};
theorem :: FF_SIEC:7
the Places of empty_f_net = {} &
the Transitions of empty_f_net = {} &
the Flow of empty_f_net = {};
theorem :: FF_SIEC:8
the Places of M c= Elements M & the Transitions of M c= Elements M;
canceled 2;
theorem :: FF_SIEC:11
(([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);
theorem :: FF_SIEC:12
chaos(M) <> {};
theorem :: FF_SIEC:13
(the Flow of M) c= [:Elements(M), Elements(M):] &
(the Flow of M)~ c= [:Elements(M), Elements(M):];
theorem :: FF_SIEC:14
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);
theorem :: FF_SIEC:15
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));
theorem :: FF_SIEC:16
(((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)) = {});
theorem :: FF_SIEC:17
(((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)) = {};
theorem :: FF_SIEC:18
(((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))));
theorem :: FF_SIEC:19
((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);
theorem :: FF_SIEC:20
((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);
theorem :: FF_SIEC:21
((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)~;
:: 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
:: FF_SIEC:def 10
((the Flow of M)~|(the Transitions of M)) \/ id(the Places of M);
func f_exit(M) -> Relation equals
:: FF_SIEC:def 11
((the Flow of M)|(the Transitions of M)) \/ id(the Places of M);
end;
theorem :: FF_SIEC:22
f_exit(M) c= [:Elements(M),Elements(M):] &
f_enter(M) c= [:Elements(M),Elements(M):];
theorem :: FF_SIEC:23
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);
theorem :: FF_SIEC:24
(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);
theorem :: FF_SIEC:25
(f_exit(M)) * (f_exit(M) \ id(Elements(M))) = {} &
(f_enter(M)) * (f_enter(M) \ id(Elements(M))) = {};
::B [F ->R]
definition
let M;
func f_prox(M) -> Relation equals
:: FF_SIEC:def 12
((the Flow of M)|(the Places of M) \/
(the Flow of M)~|(the Places of M)) \/
id(the Places of M);
func f_flow(M) -> Relation equals
:: FF_SIEC:def 13
(the Flow of M) \/ id(Elements(M));
end;
theorem :: FF_SIEC:26
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))~;
::C [F ->P]
definition let M;
func f_places(M) -> set equals
:: FF_SIEC:def 14
the Places of M;
func f_transitions(M) -> set equals
:: FF_SIEC:def 15
the Transitions of M;
func f_pre(M) -> Relation equals
:: FF_SIEC:def 16
(the Flow of M)|(the Transitions of M);
func f_post(M) -> Relation equals
:: FF_SIEC:def 17
(the Flow of M)~|(the Transitions of M);
end;
theorem :: FF_SIEC:27
f_pre(M) c= [:f_transitions(M),f_places(M):] &
f_post(M) c= [:f_transitions(M),f_places(M):];
theorem :: FF_SIEC:28
f_places(M) misses f_transitions(M);
theorem :: FF_SIEC:29
f_prox(M) c= [:Elements(M), Elements(M):] &
f_flow(M) c= [:Elements(M), Elements(M):];
::A [F -> E]
definition let M;
func f_entrance(M) -> Relation equals
:: FF_SIEC:def 18
((the Flow of M)~|(the Places of M)) \/ id(the Transitions of M);
func f_escape(M) -> Relation equals
:: FF_SIEC:def 19
((the Flow of M)|(the Places of M)) \/ id(the Transitions of M);
end;
theorem :: FF_SIEC:30
f_escape(M) c= [:Elements(M),Elements(M):] &
f_entrance(M) c= [:Elements(M),Elements(M):];
theorem :: FF_SIEC:31
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);
theorem :: FF_SIEC:32
(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);
theorem :: FF_SIEC:33
(f_escape(M)) * (f_escape(M) \ id(Elements(M))) = {} &
(f_entrance(M)) * (f_entrance(M) \ id(Elements(M))) = {};
::B [F ->R]
definition let M;
func f_adjac(M) -> Relation equals
:: FF_SIEC:def 20
((the Flow of M)|(the Transitions of M) \/
(the Flow of M)~|(the Transitions of M)) \/
id(the Transitions of M);
redefine func f_flow(M);
synonym f_circulation(M);
end;
theorem :: FF_SIEC:34
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))~;
Back to top