:: Definitions of Petri Net - Part I :: by Waldemar Korczy\'nski :: :: Received January 31, 1992 :: Copyright (c) 1992-2018 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;