:: E_SIEC semantic presentation begin definition attrc1 is strict ; struct G_Net -> 1-sorted ; aggrG_Net(# carrier, entrance, escape #) -> G_Net ; sel entrance c1 -> Relation; sel escape c1 -> Relation; end; definition let IT be G_Net ; attrIT is GG means :Def1: :: E_SIEC:def 1 ( the entrance of IT c= [: the carrier of IT, the carrier of IT:] & the escape of IT c= [: the carrier of IT, the carrier of IT:] & the entrance of IT * the entrance of IT = the entrance of IT & the entrance of IT * the escape of IT = the entrance of IT & the escape of IT * the escape of IT = the escape of IT & the escape of IT * the entrance of IT = the escape of IT ); end; :: deftheorem Def1 defines GG E_SIEC:def_1_:_ for IT being G_Net holds ( IT is GG iff ( the entrance of IT c= [: the carrier of IT, the carrier of IT:] & the escape of IT c= [: the carrier of IT, the carrier of IT:] & the entrance of IT * the entrance of IT = the entrance of IT & the entrance of IT * the escape of IT = the entrance of IT & the escape of IT * the escape of IT = the escape of IT & the escape of IT * the entrance of IT = the escape of IT ) ); registration cluster GG for G_Net ; existence ex b1 being G_Net st b1 is GG proof take N = G_Net(# {},{},{} #); ::_thesis: N is GG ( the escape of N c= [: the carrier of N, the carrier of N:] & the entrance of N * the entrance of N = {} ) by XBOOLE_1:2; hence N is GG by Def1; ::_thesis: verum end; end; definition mode gg_net is GG G_Net ; end; definition let IT be G_Net ; attrIT is EE means :Def2: :: E_SIEC:def 2 ( the entrance of IT * ( the entrance of IT \ (id the carrier of IT)) = {} & the escape of IT * ( the escape of IT \ (id the carrier of IT)) = {} ); end; :: deftheorem Def2 defines EE E_SIEC:def_2_:_ for IT being G_Net holds ( IT is EE iff ( the entrance of IT * ( the entrance of IT \ (id the carrier of IT)) = {} & the escape of IT * ( the escape of IT \ (id the carrier of IT)) = {} ) ); registration cluster EE for G_Net ; existence ex b1 being G_Net st b1 is EE proof take N = G_Net(# {},{},{} #); ::_thesis: N is EE the entrance of N * ( the entrance of N \ (id N)) = {} ; hence N is EE by Def2; ::_thesis: verum end; end; registration cluster strict GG EE for G_Net ; existence ex b1 being G_Net st ( b1 is strict & b1 is GG & b1 is EE ) proof take N = G_Net(# {},{},{} #); ::_thesis: ( N is strict & N is GG & N is EE ) ( the entrance of N c= [: the carrier of N, the carrier of N:] & the escape of N * ( the escape of N \ (id N)) = {} ) by XBOOLE_1:2; hence ( N is strict & N is GG & N is EE ) by Def1, Def2; ::_thesis: verum end; end; definition mode e_net is GG EE G_Net ; end; theorem :: E_SIEC:1 for X being set for R, S being Relation holds ( G_Net(# X,R,S #) is e_net iff ( R c= [:X,X:] & S c= [:X,X:] & R * R = R & R * S = R & S * S = S & S * R = S & R * (R \ (id X)) = {} & S * (S \ (id X)) = {} ) ) by Def1, Def2; theorem Th2: :: E_SIEC:2 for X being set holds G_Net(# X,{},{} #) is e_net proof let X be set ; ::_thesis: G_Net(# X,{},{} #) is e_net ( {} c= [:X,X:] & {} * ({} \ (id X)) = {} ) by XBOOLE_1:2; hence G_Net(# X,{},{} #) is e_net by Def1, Def2; ::_thesis: verum end; theorem Th3: :: E_SIEC:3 for X being set holds G_Net(# X,(id X),(id X) #) is e_net proof let X be set ; ::_thesis: G_Net(# X,(id X),(id X) #) is e_net A1: (id X) * ((id X) \ (id X)) = (id X) * {} by XBOOLE_1:37 .= {} ; ( id X c= [:X,X:] & (id X) * (id X) = id X ) by RELSET_1:13, SYSREL:12; hence G_Net(# X,(id X),(id X) #) is e_net by A1, Def1, Def2; ::_thesis: verum end; theorem :: E_SIEC:4 G_Net(# {},{},{} #) is e_net by Th2; theorem :: E_SIEC:5 for X, Y being set holds G_Net(# X,(id (X \ Y)),(id (X \ Y)) #) is e_net proof let X, Y be set ; ::_thesis: G_Net(# X,(id (X \ Y)),(id (X \ Y)) #) is e_net A1: (id (X \ Y)) * ((id (X \ Y)) \ (id X)) = (id (X \ Y)) * {} by SYSREL:16 .= {} ; X \ Y c= X by XBOOLE_1:36; then A2: [:(X \ Y),(X \ Y):] c= [:X,X:] by ZFMISC_1:96; id (X \ Y) c= [:(X \ Y),(X \ Y):] by RELSET_1:13; then A3: id (X \ Y) c= [:X,X:] by A2, XBOOLE_1:1; (id (X \ Y)) * (id (X \ Y)) = id (X \ Y) by SYSREL:12; hence G_Net(# X,(id (X \ Y)),(id (X \ Y)) #) is e_net by A3, A1, Def1, Def2; ::_thesis: verum end; definition func empty_e_net -> strict e_net equals :: E_SIEC:def 3 G_Net(# {},{},{} #); correctness coherence G_Net(# {},{},{} #) is strict e_net; by Th2; end; :: deftheorem defines empty_e_net E_SIEC:def_3_:_ empty_e_net = G_Net(# {},{},{} #); definition let X be set ; func Tempty_e_net X -> strict e_net equals :: E_SIEC:def 4 G_Net(# X,(id X),(id X) #); coherence G_Net(# X,(id X),(id X) #) is strict e_net by Th3; func Pempty_e_net X -> strict e_net equals :: E_SIEC:def 5 G_Net(# X,{},{} #); coherence G_Net(# X,{},{} #) is strict e_net by Th2; end; :: deftheorem defines Tempty_e_net E_SIEC:def_4_:_ for X being set holds Tempty_e_net X = G_Net(# X,(id X),(id X) #); :: deftheorem defines Pempty_e_net E_SIEC:def_5_:_ for X being set holds Pempty_e_net X = G_Net(# X,{},{} #); theorem :: E_SIEC:6 for X being set holds ( the carrier of (Tempty_e_net X) = X & the entrance of (Tempty_e_net X) = id X & the escape of (Tempty_e_net X) = id X ) ; theorem :: E_SIEC:7 for X being set holds ( the carrier of (Pempty_e_net X) = X & the entrance of (Pempty_e_net X) = {} & the escape of (Pempty_e_net X) = {} ) ; definition let x be set ; func Psingle_e_net x -> strict e_net equals :: E_SIEC:def 6 G_Net(# {x},(id {x}),(id {x}) #); coherence G_Net(# {x},(id {x}),(id {x}) #) is strict e_net by Th3; func Tsingle_e_net x -> strict e_net equals :: E_SIEC:def 7 G_Net(# {x},{},{} #); coherence G_Net(# {x},{},{} #) is strict e_net by Th2; end; :: deftheorem defines Psingle_e_net E_SIEC:def_6_:_ for x being set holds Psingle_e_net x = G_Net(# {x},(id {x}),(id {x}) #); :: deftheorem defines Tsingle_e_net E_SIEC:def_7_:_ for x being set holds Tsingle_e_net x = G_Net(# {x},{},{} #); theorem :: E_SIEC:8 for x being set holds ( the carrier of (Psingle_e_net x) = {x} & the entrance of (Psingle_e_net x) = id {x} & the escape of (Psingle_e_net x) = id {x} ) ; theorem :: E_SIEC:9 for x being set holds ( the carrier of (Tsingle_e_net x) = {x} & the entrance of (Tsingle_e_net x) = {} & the escape of (Tsingle_e_net x) = {} ) ; theorem Th10: :: E_SIEC:10 for X, Y being set holds G_Net(# (X \/ Y),(id X),(id X) #) is e_net proof let X, Y be set ; ::_thesis: G_Net(# (X \/ Y),(id X),(id X) #) is e_net X c= X \/ Y by XBOOLE_1:7; then ( id X c= [:X,X:] & [:X,X:] c= [:(X \/ Y),(X \/ Y):] ) by RELSET_1:13, ZFMISC_1:96; then A1: id X c= [:(X \/ Y),(X \/ Y):] by XBOOLE_1:1; id X c= (id X) \/ (id Y) by XBOOLE_1:7; then id X c= id (X \/ Y) by SYSREL:14; then A2: (id X) * ((id X) \ (id (X \/ Y))) = (id X) * {} by XBOOLE_1:37 .= {} ; (id X) * (id X) = id X by SYSREL:12; hence G_Net(# (X \/ Y),(id X),(id X) #) is e_net by A1, A2, Def1, Def2; ::_thesis: verum end; definition let X, Y be set ; func PTempty_e_net (X,Y) -> strict e_net equals :: E_SIEC:def 8 G_Net(# (X \/ Y),(id X),(id X) #); coherence G_Net(# (X \/ Y),(id X),(id X) #) is strict e_net by Th10; end; :: deftheorem defines PTempty_e_net E_SIEC:def_8_:_ for X, Y being set holds PTempty_e_net (X,Y) = G_Net(# (X \/ Y),(id X),(id X) #); theorem Th11: :: E_SIEC:11 for N being e_net holds ( the entrance of N \ (id (dom the entrance of N)) = the entrance of N \ (id the carrier of N) & the escape of N \ (id (dom the escape of N)) = the escape of N \ (id the carrier of N) & the entrance of N \ (id (rng the entrance of N)) = the entrance of N \ (id the carrier of N) & the escape of N \ (id (rng the escape of N)) = the escape of N \ (id the carrier of N) ) proof let N be e_net; ::_thesis: ( the entrance of N \ (id (dom the entrance of N)) = the entrance of N \ (id the carrier of N) & the escape of N \ (id (dom the escape of N)) = the escape of N \ (id the carrier of N) & the entrance of N \ (id (rng the entrance of N)) = the entrance of N \ (id the carrier of N) & the escape of N \ (id (rng the escape of N)) = the escape of N \ (id the carrier of N) ) ( the entrance of N c= [: the carrier of N, the carrier of N:] & the escape of N c= [: the carrier of N, the carrier of N:] ) by Def1; hence ( the entrance of N \ (id (dom the entrance of N)) = the entrance of N \ (id the carrier of N) & the escape of N \ (id (dom the escape of N)) = the escape of N \ (id the carrier of N) & the entrance of N \ (id (rng the entrance of N)) = the entrance of N \ (id the carrier of N) & the escape of N \ (id (rng the escape of N)) = the escape of N \ (id the carrier of N) ) by SYSREL:20; ::_thesis: verum end; theorem Th12: :: E_SIEC:12 for N being e_net holds CL the entrance of N = CL the escape of N proof let N be e_net; ::_thesis: CL the entrance of N = CL the escape of N the escape of N * ( the escape of N \ (id N)) = {} by Def2; then A1: the escape of N * ( the escape of N \ (id (dom the escape of N))) = {} by Th11; the entrance of N * ( the entrance of N \ (id N)) = {} by Def2; then A2: the entrance of N * ( the entrance of N \ (id (dom the entrance of N))) = {} by Th11; ( the entrance of N * the escape of N = the entrance of N & the escape of N * the entrance of N = the escape of N ) by Def1; hence CL the entrance of N = CL the escape of N by A1, A2, SYSREL:40; ::_thesis: verum end; theorem Th13: :: E_SIEC:13 for N being e_net holds ( rng the entrance of N = rng (CL the entrance of N) & rng the entrance of N = dom (CL the entrance of N) & rng the escape of N = rng (CL the escape of N) & rng the escape of N = dom (CL the escape of N) & rng the entrance of N = rng the escape of N ) proof let N be e_net; ::_thesis: ( rng the entrance of N = rng (CL the entrance of N) & rng the entrance of N = dom (CL the entrance of N) & rng the escape of N = rng (CL the escape of N) & rng the escape of N = dom (CL the escape of N) & rng the entrance of N = rng the escape of N ) the entrance of N * ( the entrance of N \ (id the carrier of N)) = {} by Def2; then A1: the entrance of N * ( the entrance of N \ (id (dom the entrance of N))) = {} by Th11; the escape of N * ( the escape of N \ (id the carrier of N)) = {} by Def2; then A2: the escape of N * ( the escape of N \ (id (dom the escape of N))) = {} by Th11; A3: the escape of N * the escape of N = the escape of N by Def1; then A4: rng the escape of N = rng (CL the escape of N) by A2, SYSREL:31; A5: the entrance of N * the entrance of N = the entrance of N by Def1; then rng the entrance of N = rng (CL the entrance of N) by A1, SYSREL:31; hence ( rng the entrance of N = rng (CL the entrance of N) & rng the entrance of N = dom (CL the entrance of N) & rng the escape of N = rng (CL the escape of N) & rng the escape of N = dom (CL the escape of N) & rng the entrance of N = rng the escape of N ) by A5, A1, A3, A2, A4, Th12, SYSREL:31; ::_thesis: verum end; theorem Th14: :: E_SIEC:14 for N being e_net holds ( dom the entrance of N c= the carrier of N & rng the entrance of N c= the carrier of N & dom the escape of N c= the carrier of N & rng the escape of N c= the carrier of N ) proof let N be e_net; ::_thesis: ( dom the entrance of N c= the carrier of N & rng the entrance of N c= the carrier of N & dom the escape of N c= the carrier of N & rng the escape of N c= the carrier of N ) ( the entrance of N c= [: the carrier of N, the carrier of N:] & the escape of N c= [: the carrier of N, the carrier of N:] ) by Def1; hence ( dom the entrance of N c= the carrier of N & rng the entrance of N c= the carrier of N & dom the escape of N c= the carrier of N & rng the escape of N c= the carrier of N ) by SYSREL:3; ::_thesis: verum end; theorem Th15: :: E_SIEC:15 for N being e_net holds ( the entrance of N * ( the escape of N \ (id the carrier of N)) = {} & the escape of N * ( the entrance of N \ (id the carrier of N)) = {} ) proof let N be e_net; ::_thesis: ( the entrance of N * ( the escape of N \ (id the carrier of N)) = {} & the escape of N * ( the entrance of N \ (id the carrier of N)) = {} ) set R = the entrance of N; set S = the escape of N; set T = id the carrier of N; A1: the escape of N * ( the entrance of N \ (id the carrier of N)) = the escape of N * ( the entrance of N \ (id (dom the entrance of N))) by Th11 .= ( the escape of N * the entrance of N) * ( the entrance of N \ (id (dom the entrance of N))) by Def1 .= the escape of N * ( the entrance of N * ( the entrance of N \ (id (dom the entrance of N)))) by RELAT_1:36 .= the escape of N * ( the entrance of N * ( the entrance of N \ (id the carrier of N))) by Th11 .= the escape of N * {} by Def2 .= {} ; the entrance of N * ( the escape of N \ (id the carrier of N)) = the entrance of N * ( the escape of N \ (id (dom the escape of N))) by Th11 .= ( the entrance of N * the escape of N) * ( the escape of N \ (id (dom the escape of N))) by Def1 .= the entrance of N * ( the escape of N * ( the escape of N \ (id (dom the escape of N)))) by RELAT_1:36 .= the entrance of N * ( the escape of N * ( the escape of N \ (id the carrier of N))) by Th11 .= the entrance of N * {} by Def2 .= {} ; hence ( the entrance of N * ( the escape of N \ (id the carrier of N)) = {} & the escape of N * ( the entrance of N \ (id the carrier of N)) = {} ) by A1; ::_thesis: verum end; theorem :: E_SIEC:16 for N being e_net holds ( ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} & ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} ) proof let N be e_net; ::_thesis: ( ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} & ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} ) set R = the entrance of N; set S = the escape of N; set T = id the carrier of N; ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= the entrance of N * ( the escape of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36; then A1: ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Th15; ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= the escape of N * ( the escape of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36; then A2: ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Def2; ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= the escape of N * ( the entrance of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36; then A3: ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= {} by Th15; ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= the entrance of N * ( the entrance of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36; then ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= {} by Def2; hence ( ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} & ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} ) by A1, A2, A3, XBOOLE_1:3; ::_thesis: verum end; definition let N be e_net; func e_Places N -> set equals :: E_SIEC:def 9 rng the entrance of N; correctness coherence rng the entrance of N is set ; ; end; :: deftheorem defines e_Places E_SIEC:def_9_:_ for N being e_net holds e_Places N = rng the entrance of N; definition let N be e_net; func e_Transitions N -> set equals :: E_SIEC:def 10 the carrier of N \ (e_Places N); correctness coherence the carrier of N \ (e_Places N) is set ; ; end; :: deftheorem defines e_Transitions E_SIEC:def_10_:_ for N being e_net holds e_Transitions N = the carrier of N \ (e_Places N); theorem Th17: :: E_SIEC:17 for x, y being set for N being e_net st ( [x,y] in the entrance of N or [x,y] in the escape of N ) & x <> y holds ( x in e_Transitions N & y in e_Places N ) proof let x, y be set ; ::_thesis: for N being e_net st ( [x,y] in the entrance of N or [x,y] in the escape of N ) & x <> y holds ( x in e_Transitions N & y in e_Places N ) let N be e_net; ::_thesis: ( ( [x,y] in the entrance of N or [x,y] in the escape of N ) & x <> y implies ( x in e_Transitions N & y in e_Places N ) ) A1: ( [x,y] in the escape of N & x <> y implies ( x in e_Transitions N & y in e_Places N ) ) proof the escape of N * ( the escape of N \ (id the carrier of N)) = {} by Def2; then A2: the escape of N * ( the escape of N \ (id (dom the escape of N))) = {} by Th11; dom the escape of N c= the carrier of N by Th14; then A3: (dom the escape of N) \ (dom (CL the escape of N)) c= the carrier of N \ (dom (CL the escape of N)) by XBOOLE_1:33; assume A4: ( [x,y] in the escape of N & x <> y ) ; ::_thesis: ( x in e_Transitions N & y in e_Places N ) A5: the escape of N * the escape of N = the escape of N by Def1; then x in (dom the escape of N) \ (dom (CL the escape of N)) by A4, A2, SYSREL:30; then x in the carrier of N \ (dom (CL the escape of N)) by A3; then A6: x in the carrier of N \ (rng the escape of N) by Th13; y in dom (CL the escape of N) by A4, A5, A2, SYSREL:30; then y in rng the escape of N by Th13; hence ( x in e_Transitions N & y in e_Places N ) by A6, Th13; ::_thesis: verum end; ( [x,y] in the entrance of N & x <> y implies ( x in e_Transitions N & y in e_Places N ) ) proof the entrance of N * ( the entrance of N \ (id the carrier of N)) = {} by Def2; then A7: the entrance of N * ( the entrance of N \ (id (dom the entrance of N))) = {} by Th11; dom the entrance of N c= the carrier of N by Th14; then A8: (dom the entrance of N) \ (dom (CL the entrance of N)) c= the carrier of N \ (dom (CL the entrance of N)) by XBOOLE_1:33; assume A9: ( [x,y] in the entrance of N & x <> y ) ; ::_thesis: ( x in e_Transitions N & y in e_Places N ) A10: the entrance of N * the entrance of N = the entrance of N by Def1; then x in (dom the entrance of N) \ (dom (CL the entrance of N)) by A9, A7, SYSREL:30; then A11: x in the carrier of N \ (dom (CL the entrance of N)) by A8; y in dom (CL the entrance of N) by A9, A10, A7, SYSREL:30; hence ( x in e_Transitions N & y in e_Places N ) by A11, Th13; ::_thesis: verum end; hence ( ( [x,y] in the entrance of N or [x,y] in the escape of N ) & x <> y implies ( x in e_Transitions N & y in e_Places N ) ) by A1; ::_thesis: verum end; theorem Th18: :: E_SIEC:18 for N being e_net holds ( the entrance of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] & the escape of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] ) proof let N be e_net; ::_thesis: ( the entrance of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] & the escape of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] ) A1: for x, y being set st [x,y] in the entrance of N \ (id the carrier of N) holds [x,y] in [:(e_Transitions N),(e_Places N):] proof let x, y be set ; ::_thesis: ( [x,y] in the entrance of N \ (id the carrier of N) implies [x,y] in [:(e_Transitions N),(e_Places N):] ) assume A2: [x,y] in the entrance of N \ (id the carrier of N) ; ::_thesis: [x,y] in [:(e_Transitions N),(e_Places N):] then [x,y] in the entrance of N by XBOOLE_0:def_5; then A3: x in dom the entrance of N by XTUPLE_0:def_12; not [x,y] in id the carrier of N by A2, XBOOLE_0:def_5; then A4: ( not x in the carrier of N or x <> y ) by RELAT_1:def_10; A5: [x,y] in the entrance of N by A2, XBOOLE_0:def_5; then A6: y in e_Places N by XTUPLE_0:def_13; dom the entrance of N c= the carrier of N by Th14; then x in e_Transitions N by A5, A4, A3, Th17; hence [x,y] in [:(e_Transitions N),(e_Places N):] by A6, ZFMISC_1:87; ::_thesis: verum end; for x, y being set st [x,y] in the escape of N \ (id the carrier of N) holds [x,y] in [:(e_Transitions N),(e_Places N):] proof let x, y be set ; ::_thesis: ( [x,y] in the escape of N \ (id the carrier of N) implies [x,y] in [:(e_Transitions N),(e_Places N):] ) A7: dom the escape of N c= the carrier of N by Th14; assume A8: [x,y] in the escape of N \ (id the carrier of N) ; ::_thesis: [x,y] in [:(e_Transitions N),(e_Places N):] then [x,y] in the escape of N by XBOOLE_0:def_5; then A9: x in dom the escape of N by XTUPLE_0:def_12; not [x,y] in id the carrier of N by A8, XBOOLE_0:def_5; then A10: ( not x in the carrier of N or x <> y ) by RELAT_1:def_10; [x,y] in the escape of N by A8, XBOOLE_0:def_5; then ( x in e_Transitions N & y in e_Places N ) by A10, A9, A7, Th17; hence [x,y] in [:(e_Transitions N),(e_Places N):] by ZFMISC_1:87; ::_thesis: verum end; hence ( the entrance of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] & the escape of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] ) by A1, RELAT_1:def_3; ::_thesis: verum end; definition let N be e_net; func e_Flow N -> Relation equals :: E_SIEC:def 11 (( the entrance of N ~) \/ the escape of N) \ (id N); correctness coherence (( the entrance of N ~) \/ the escape of N) \ (id N) is Relation; ; end; :: deftheorem defines e_Flow E_SIEC:def_11_:_ for N being e_net holds e_Flow N = (( the entrance of N ~) \/ the escape of N) \ (id N); theorem :: E_SIEC:19 for N being e_net holds e_Flow N c= [:(e_Places N),(e_Transitions N):] \/ [:(e_Transitions N),(e_Places N):] proof let N be e_net; ::_thesis: e_Flow N c= [:(e_Places N),(e_Transitions N):] \/ [:(e_Transitions N),(e_Places N):] A1: ( the entrance of N ~) \ (id N) = ( the entrance of N ~) \ ((id the carrier of N) ~) by RELAT_1:46 .= ( the entrance of N \ (id the carrier of N)) ~ by RELAT_1:24 ; A2: ( e_Flow N = (( the entrance of N ~) \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)) & the escape of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] ) by Th18, XBOOLE_1:42; the entrance of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] by Th18; then ( the entrance of N ~) \ (id the carrier of N) c= [:(e_Places N),(e_Transitions N):] by A1, SYSREL:4; hence e_Flow N c= [:(e_Places N),(e_Transitions N):] \/ [:(e_Transitions N),(e_Places N):] by A2, XBOOLE_1:13; ::_thesis: verum end; definition let N be e_net; func e_pre N -> Relation equals :: E_SIEC:def 12 the entrance of N \ (id the carrier of N); correctness coherence the entrance of N \ (id the carrier of N) is Relation; ; func e_post N -> Relation equals :: E_SIEC:def 13 the escape of N \ (id the carrier of N); correctness coherence the escape of N \ (id the carrier of N) is Relation; ; end; :: deftheorem defines e_pre E_SIEC:def_12_:_ for N being e_net holds e_pre N = the entrance of N \ (id the carrier of N); :: deftheorem defines e_post E_SIEC:def_13_:_ for N being e_net holds e_post N = the escape of N \ (id the carrier of N); theorem :: E_SIEC:20 for N being e_net holds ( e_pre N c= [:(e_Transitions N),(e_Places N):] & e_post N c= [:(e_Transitions N),(e_Places N):] ) by Th18; definition let N be e_net; func e_shore N -> set equals :: E_SIEC:def 14 the carrier of N; correctness coherence the carrier of N is set ; ; func e_prox N -> Relation equals :: E_SIEC:def 15 ( the entrance of N \/ the escape of N) ~ ; correctness coherence ( the entrance of N \/ the escape of N) ~ is Relation; ; func e_flow N -> Relation equals :: E_SIEC:def 16 (( the entrance of N ~) \/ the escape of N) \/ (id the carrier of N); correctness coherence (( the entrance of N ~) \/ the escape of N) \/ (id the carrier of N) is Relation; ; end; :: deftheorem defines e_shore E_SIEC:def_14_:_ for N being e_net holds e_shore N = the carrier of N; :: deftheorem defines e_prox E_SIEC:def_15_:_ for N being e_net holds e_prox N = ( the entrance of N \/ the escape of N) ~ ; :: deftheorem defines e_flow E_SIEC:def_16_:_ for N being e_net holds e_flow N = (( the entrance of N ~) \/ the escape of N) \/ (id the carrier of N); theorem :: E_SIEC:21 for N being e_net holds ( e_prox N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] ) proof let N be e_net; ::_thesis: ( e_prox N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] ) A1: id the carrier of N c= [: the carrier of N, the carrier of N:] by RELSET_1:13; A2: the escape of N c= [: the carrier of N, the carrier of N:] by Def1; A3: the entrance of N c= [: the carrier of N, the carrier of N:] by Def1; then the entrance of N ~ c= [: the carrier of N, the carrier of N:] by SYSREL:4; then A4: ( the entrance of N ~) \/ the escape of N c= [: the carrier of N, the carrier of N:] by A2, XBOOLE_1:8; the entrance of N \/ the escape of N c= [: the carrier of N, the carrier of N:] by A3, A2, XBOOLE_1:8; hence ( e_prox N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] ) by A4, A1, SYSREL:4, XBOOLE_1:8; ::_thesis: verum end; theorem :: E_SIEC:22 for N being e_net holds ( (e_prox N) * (e_prox N) = e_prox N & ((e_prox N) \ (id (e_shore N))) * (e_prox N) = {} & ((e_prox N) \/ ((e_prox N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) ) proof let N be e_net; ::_thesis: ( (e_prox N) * (e_prox N) = e_prox N & ((e_prox N) \ (id (e_shore N))) * (e_prox N) = {} & ((e_prox N) \/ ((e_prox N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) ) set R = the entrance of N; set S = the escape of N; set T = id the carrier of N; A1: ((e_prox N) \/ ((e_prox N) ~)) \/ (id (e_shore N)) = ((( the entrance of N ~) \/ ( the escape of N ~)) \/ ( the escape of N \/ the entrance of N)) \/ (id the carrier of N) by RELAT_1:23 .= (((( the entrance of N ~) \/ ( the escape of N ~)) \/ the escape of N) \/ the entrance of N) \/ (id the carrier of N) by XBOOLE_1:4 .= ((( the entrance of N ~) \/ (( the escape of N ~) \/ the escape of N)) \/ the entrance of N) \/ (id the carrier of N) by XBOOLE_1:4 .= (( the entrance of N ~) \/ (( the escape of N \/ ( the escape of N ~)) \/ the entrance of N)) \/ (id the carrier of N) by XBOOLE_1:4 .= (( the entrance of N ~) \/ ( the escape of N \/ (( the escape of N ~) \/ the entrance of N))) \/ (id the carrier of N) by XBOOLE_1:4 .= ((( the entrance of N ~) \/ the escape of N) \/ (( the escape of N ~) \/ the entrance of N)) \/ (id the carrier of N) by XBOOLE_1:4 .= (e_flow N) \/ ((( the escape of N ~) \/ (( the entrance of N ~) ~)) \/ (id the carrier of N)) by XBOOLE_1:5 .= (e_flow N) \/ (((( the entrance of N ~) \/ the escape of N) ~) \/ (id the carrier of N)) by RELAT_1:23 .= (e_flow N) \/ (((( the entrance of N ~) \/ the escape of N) ~) \/ ((id the carrier of N) ~)) .= (e_flow N) \/ ((e_flow N) ~) by RELAT_1:23 ; A2: ((e_prox N) \ (id the carrier of N)) * (e_prox N) = ((( the entrance of N ~) \/ ( the escape of N ~)) \ (id the carrier of N)) * (( the entrance of N \/ the escape of N) ~) by RELAT_1:23 .= ((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * (( the entrance of N \/ the escape of N) ~) by XBOOLE_1:42 .= ((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * (( the entrance of N ~) \/ ( the escape of N ~)) by RELAT_1:23 .= (((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * ( the entrance of N ~)) \/ (((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * ( the escape of N ~)) by RELAT_1:32 .= (((( the entrance of N ~) \ (id the carrier of N)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ (id the carrier of N)) \/ (( the escape of N ~) \ (id the carrier of N))) * ( the escape of N ~)) by SYSREL:6 .= (((( the entrance of N ~) \ (id the carrier of N)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ (id the carrier of N)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~))) by SYSREL:6 .= (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ (id the carrier of N)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~))) .= (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ (id the carrier of N)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~))) .= (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ (id the carrier of N)) * ( the escape of N ~))) .= (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~))) .= (((( the entrance of N \ (id the carrier of N)) ~) * ( the entrance of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~))) by RELAT_1:24 .= (((( the entrance of N \ (id the carrier of N)) ~) * ( the entrance of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the entrance of N ~))) \/ (((( the entrance of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~))) by RELAT_1:24 .= (((( the entrance of N \ (id the carrier of N)) ~) * ( the entrance of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the entrance of N ~))) \/ (((( the entrance of N \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N ~) \ ((id the carrier of N) ~)) * ( the escape of N ~))) by RELAT_1:24 .= (((( the entrance of N \ (id the carrier of N)) ~) * ( the entrance of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the entrance of N ~))) \/ (((( the entrance of N \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~))) by RELAT_1:24 .= ((( the entrance of N * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the entrance of N ~))) \/ (((( the entrance of N \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~))) by RELAT_1:35 .= ((( the entrance of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ (((( the entrance of N \ (id the carrier of N)) ~) * ( the escape of N ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~))) by RELAT_1:35 .= ((( the entrance of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ( the escape of N ~))) by RELAT_1:35 .= ((( the entrance of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the escape of N * ( the escape of N \ (id the carrier of N))) ~)) by RELAT_1:35 .= (({} ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ (( the escape of N * ( the escape of N \ (id the carrier of N))) ~)) by Def2 .= (({} ~) \/ (( the entrance of N * ( the escape of N \ (id the carrier of N))) ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ ({} ~)) by Def2 .= (({} ~) \/ ({} ~)) \/ ((( the escape of N * ( the entrance of N \ (id the carrier of N))) ~) \/ ({} ~)) by Th15 .= {} by Th15 ; (e_prox N) * (e_prox N) = (( the entrance of N \/ the escape of N) * ( the entrance of N \/ the escape of N)) ~ by RELAT_1:35 .= ((( the entrance of N \/ the escape of N) * the entrance of N) \/ (( the entrance of N \/ the escape of N) * the escape of N)) ~ by RELAT_1:32 .= ((( the entrance of N * the entrance of N) \/ ( the escape of N * the entrance of N)) \/ (( the entrance of N \/ the escape of N) * the escape of N)) ~ by SYSREL:6 .= ((( the entrance of N * the entrance of N) \/ ( the escape of N * the entrance of N)) \/ (( the entrance of N * the escape of N) \/ ( the escape of N * the escape of N))) ~ by SYSREL:6 .= (( the entrance of N \/ ( the escape of N * the entrance of N)) \/ (( the entrance of N * the escape of N) \/ ( the escape of N * the escape of N))) ~ by Def1 .= (( the entrance of N \/ the escape of N) \/ (( the entrance of N * the escape of N) \/ ( the escape of N * the escape of N))) ~ by Def1 .= (( the entrance of N \/ the escape of N) \/ ( the entrance of N \/ ( the escape of N * the escape of N))) ~ by Def1 .= (( the entrance of N \/ the escape of N) \/ ( the entrance of N \/ the escape of N)) ~ by Def1 .= e_prox N ; hence ( (e_prox N) * (e_prox N) = e_prox N & ((e_prox N) \ (id (e_shore N))) * (e_prox N) = {} & ((e_prox N) \/ ((e_prox N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) ) by A2, A1; ::_thesis: verum end; theorem Th23: :: E_SIEC:23 for N being e_net holds ( (id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N)) = the escape of N \ (id the carrier of N) & (id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N)) = the entrance of N \ (id the carrier of N) ) proof let N be e_net; ::_thesis: ( (id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N)) = the escape of N \ (id the carrier of N) & (id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N)) = the entrance of N \ (id the carrier of N) ) set T = the entrance of N; set C = the carrier of N; set E = the escape of N; set I = id the carrier of N; for x, y being set st [x,y] in the escape of N \ (id the carrier of N) holds [x,y] in (id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N)) proof let x, y be set ; ::_thesis: ( [x,y] in the escape of N \ (id the carrier of N) implies [x,y] in (id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N)) ) assume A1: [x,y] in the escape of N \ (id the carrier of N) ; ::_thesis: [x,y] in (id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N)) then [x,y] in the escape of N by XBOOLE_0:def_5; then A2: x in dom the escape of N by XTUPLE_0:def_12; A3: not x in rng the escape of N proof assume x in rng the escape of N ; ::_thesis: contradiction then ex z being set st [z,x] in the escape of N by XTUPLE_0:def_13; then the escape of N * ( the escape of N \ (id the carrier of N)) <> {} by A1, RELAT_1:def_8; hence contradiction by Def2; ::_thesis: verum end; dom the escape of N c= the carrier of N by Th14; then x in the carrier of N \ (rng the escape of N) by A2, A3, XBOOLE_0:def_5; then [x,x] in id ( the carrier of N \ (rng the escape of N)) by RELAT_1:def_10; hence [x,y] in (id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N)) by A1, RELAT_1:def_8; ::_thesis: verum end; then A4: the escape of N \ (id the carrier of N) c= (id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N)) by RELAT_1:def_3; for x, y being set st [x,y] in the entrance of N \ (id the carrier of N) holds [x,y] in (id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N)) proof let x, y be set ; ::_thesis: ( [x,y] in the entrance of N \ (id the carrier of N) implies [x,y] in (id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N)) ) assume A5: [x,y] in the entrance of N \ (id the carrier of N) ; ::_thesis: [x,y] in (id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N)) then [x,y] in the entrance of N by XBOOLE_0:def_5; then A6: x in dom the entrance of N by XTUPLE_0:def_12; A7: not x in rng the entrance of N proof assume x in rng the entrance of N ; ::_thesis: contradiction then ex z being set st [z,x] in the entrance of N by XTUPLE_0:def_13; then the entrance of N * ( the entrance of N \ (id the carrier of N)) <> {} by A5, RELAT_1:def_8; hence contradiction by Def2; ::_thesis: verum end; dom the entrance of N c= the carrier of N by Th14; then x in the carrier of N \ (rng the entrance of N) by A6, A7, XBOOLE_0:def_5; then [x,x] in id ( the carrier of N \ (rng the entrance of N)) by RELAT_1:def_10; hence [x,y] in (id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N)) by A5, RELAT_1:def_8; ::_thesis: verum end; then A8: the entrance of N \ (id the carrier of N) c= (id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N)) by RELAT_1:def_3; ( (id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N)) c= the escape of N \ (id the carrier of N) & (id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N)) c= the entrance of N \ (id the carrier of N) ) by RELAT_1:50; hence ( (id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N)) = the escape of N \ (id the carrier of N) & (id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N)) = the entrance of N \ (id the carrier of N) ) by A4, A8, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th24: :: E_SIEC:24 for N being e_net holds ( ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} ) proof let N be e_net; ::_thesis: ( ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} ) set T = the entrance of N; set C = the carrier of N; set E = the escape of N; set I = id the carrier of N; ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= the entrance of N * ( the entrance of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36; then A1: ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= {} by Def2; ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= the escape of N * ( the entrance of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36; then A2: ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= {} by Th15; ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= the entrance of N * ( the escape of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36; then A3: ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Th15; ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= the escape of N * ( the escape of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36; then ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Def2; hence ( ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} ) by A1, A2, A3, XBOOLE_1:3; ::_thesis: verum end; theorem Th25: :: E_SIEC:25 for N being e_net holds ( (( the escape of N \ (id the carrier of N)) ~) * (( the escape of N \ (id the carrier of N)) ~) = {} & (( the entrance of N \ (id the carrier of N)) ~) * (( the entrance of N \ (id the carrier of N)) ~) = {} ) proof let N be e_net; ::_thesis: ( (( the escape of N \ (id the carrier of N)) ~) * (( the escape of N \ (id the carrier of N)) ~) = {} & (( the entrance of N \ (id the carrier of N)) ~) * (( the entrance of N \ (id the carrier of N)) ~) = {} ) A1: (( the entrance of N \ (id the carrier of N)) ~) * (( the entrance of N \ (id the carrier of N)) ~) = (( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~ by RELAT_1:35 .= {} by Th24, RELAT_1:43 ; (( the escape of N \ (id the carrier of N)) ~) * (( the escape of N \ (id the carrier of N)) ~) = (( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~ by RELAT_1:35 .= {} by Th24, RELAT_1:43 ; hence ( (( the escape of N \ (id the carrier of N)) ~) * (( the escape of N \ (id the carrier of N)) ~) = {} & (( the entrance of N \ (id the carrier of N)) ~) * (( the entrance of N \ (id the carrier of N)) ~) = {} ) by A1; ::_thesis: verum end; theorem :: E_SIEC:26 for N being e_net holds ( (( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~) = ( the escape of N \ (id the carrier of N)) ~ & (( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~) = ( the entrance of N \ (id the carrier of N)) ~ ) proof let N be e_net; ::_thesis: ( (( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~) = ( the escape of N \ (id the carrier of N)) ~ & (( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~) = ( the entrance of N \ (id the carrier of N)) ~ ) A1: (( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~) = ((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) ~ by RELAT_1:35 .= ( the entrance of N \ (id the carrier of N)) ~ by Th23 ; (( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~) = ((id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N))) ~ by RELAT_1:35 .= ( the escape of N \ (id the carrier of N)) ~ by Th23 ; hence ( (( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~) = ( the escape of N \ (id the carrier of N)) ~ & (( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~) = ( the entrance of N \ (id the carrier of N)) ~ ) by A1; ::_thesis: verum end; theorem Th27: :: E_SIEC:27 for N being e_net holds ( ( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N))) = {} & ( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))) = {} ) proof let N be e_net; ::_thesis: ( ( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N))) = {} & ( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))) = {} ) A1: for x, y being set holds not [x,y] in ( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))) proof let x, y be set ; ::_thesis: not [x,y] in ( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))) assume [x,y] in ( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))) ; ::_thesis: contradiction then consider z being set such that A2: [x,z] in the entrance of N \ (id the carrier of N) and A3: [z,y] in id ( the carrier of N \ (rng the entrance of N)) by RELAT_1:def_8; z in the carrier of N \ (rng the entrance of N) by A3, RELAT_1:def_10; then A4: not z in rng the entrance of N by XBOOLE_0:def_5; [x,z] in the entrance of N by A2, XBOOLE_0:def_5; hence contradiction by A4, XTUPLE_0:def_13; ::_thesis: verum end; for x, y being set holds not [x,y] in ( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N))) proof let x, y be set ; ::_thesis: not [x,y] in ( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N))) assume [x,y] in ( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N))) ; ::_thesis: contradiction then consider z being set such that A5: [x,z] in the escape of N \ (id the carrier of N) and A6: [z,y] in id ( the carrier of N \ (rng the escape of N)) by RELAT_1:def_8; z in the carrier of N \ (rng the escape of N) by A6, RELAT_1:def_10; then A7: not z in rng the escape of N by XBOOLE_0:def_5; [x,z] in the escape of N by A5, XBOOLE_0:def_5; hence contradiction by A7, XTUPLE_0:def_13; ::_thesis: verum end; hence ( ( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N))) = {} & ( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))) = {} ) by A1, RELAT_1:37; ::_thesis: verum end; theorem Th28: :: E_SIEC:28 for N being e_net holds ( (id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~) = {} & (id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~) = {} ) proof let N be e_net; ::_thesis: ( (id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~) = {} & (id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~) = {} ) A1: (id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~) = ((id ( the carrier of N \ (rng the entrance of N))) ~) * (( the entrance of N \ (id the carrier of N)) ~) .= (( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) ~ by RELAT_1:35 .= {} by Th27, RELAT_1:43 ; (id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~) = ((id ( the carrier of N \ (rng the escape of N))) ~) * (( the escape of N \ (id the carrier of N)) ~) .= (( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) ~ by RELAT_1:35 .= {} by Th27, RELAT_1:43 ; hence ( (id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~) = {} & (id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~) = {} ) by A1; ::_thesis: verum end; definition let N be e_net; func e_entrance N -> Relation equals :: E_SIEC:def 17 (( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N))); correctness coherence (( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N))) is Relation; ; func e_escape N -> Relation equals :: E_SIEC:def 18 (( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))); correctness coherence (( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))) is Relation; ; end; :: deftheorem defines e_entrance E_SIEC:def_17_:_ for N being e_net holds e_entrance N = (( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N))); :: deftheorem defines e_escape E_SIEC:def_18_:_ for N being e_net holds e_escape N = (( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))); theorem :: E_SIEC:29 for N being e_net holds ( (e_entrance N) * (e_entrance N) = e_entrance N & (e_entrance N) * (e_escape N) = e_entrance N & (e_escape N) * (e_entrance N) = e_escape N & (e_escape N) * (e_escape N) = e_escape N ) proof let N be e_net; ::_thesis: ( (e_entrance N) * (e_entrance N) = e_entrance N & (e_entrance N) * (e_escape N) = e_entrance N & (e_escape N) * (e_entrance N) = e_escape N & (e_escape N) * (e_escape N) = e_escape N ) set P = the escape of N \ (id the carrier of N); set Q = the entrance of N \ (id the carrier of N); set S = id ( the carrier of N \ (rng the entrance of N)); set T = id ( the carrier of N \ (rng the escape of N)); A1: (e_entrance N) * (e_entrance N) = ((( the escape of N \ (id the carrier of N)) ~) * ((( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N))))) \/ ((id ( the carrier of N \ (rng the escape of N))) * ((( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N))))) by SYSREL:6 .= (((( the escape of N \ (id the carrier of N)) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the escape of N))))) \/ ((id ( the carrier of N \ (rng the escape of N))) * ((( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N))))) by RELAT_1:32 .= (((( the escape of N \ (id the carrier of N)) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the escape of N))))) \/ (((id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the escape of N))) * (id ( the carrier of N \ (rng the escape of N))))) by RELAT_1:32 .= (((( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the escape of N))))) \/ (((id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the escape of N))) * (id ( the carrier of N \ (rng the escape of N))))) by RELAT_1:35 .= (((( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~))) \/ (((id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the escape of N))) * (id ( the carrier of N \ (rng the escape of N))))) .= (((( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~))) \/ ((((id ( the carrier of N \ (rng the escape of N))) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the escape of N))) * (id ( the carrier of N \ (rng the escape of N))))) .= (((( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~))) \/ ((((id ( the carrier of N \ (rng the escape of N))) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ (id ( the carrier of N \ (rng the escape of N)))) by SYSREL:12 .= (((( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N))) ~)) \/ ((((id ( the carrier of N \ (rng the escape of N))) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ (id ( the carrier of N \ (rng the escape of N)))) by RELAT_1:35 .= (((( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N))) ~)) \/ (((( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) by RELAT_1:35 .= (({} ~) \/ (((id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N))) ~)) \/ (((( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) by Th24 .= (({} ~) \/ (( the escape of N \ (id the carrier of N)) ~)) \/ (((( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) by Th23 .= ({} \/ (( the escape of N \ (id the carrier of N)) ~)) \/ ({} \/ (id ( the carrier of N \ (rng the escape of N)))) by Th27 .= e_entrance N ; A2: (e_escape N) * (e_escape N) = ((( the entrance of N \ (id the carrier of N)) ~) * ((( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ((( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))))) by SYSREL:6 .= (((( the entrance of N \ (id the carrier of N)) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((( the entrance of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the entrance of N))))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ((( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))))) by RELAT_1:32 .= (((( the entrance of N \ (id the carrier of N)) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((( the entrance of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by RELAT_1:32 .= (((( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the entrance of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by RELAT_1:35 .= (((( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) .= (((( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~))) \/ ((((id ( the carrier of N \ (rng the entrance of N))) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) .= (((( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~))) \/ ((((id ( the carrier of N \ (rng the entrance of N))) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ (id ( the carrier of N \ (rng the entrance of N)))) by SYSREL:12 .= (((( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) ~)) \/ ((((id ( the carrier of N \ (rng the entrance of N))) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ (id ( the carrier of N \ (rng the entrance of N)))) by RELAT_1:35 .= (((( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) ~)) \/ (((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) by RELAT_1:35 .= (({} ~) \/ (((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) ~)) \/ (((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th24 .= (({} ~) \/ (( the entrance of N \ (id the carrier of N)) ~)) \/ (((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th23 .= ({} \/ (( the entrance of N \ (id the carrier of N)) ~)) \/ ({} \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th27 .= e_escape N ; A3: (e_escape N) * (e_entrance N) = ((( the entrance of N \ (id the carrier of N)) ~) * ((( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N))))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ((( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N))))) by SYSREL:6 .= (((( the entrance of N \ (id the carrier of N)) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((( the entrance of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the escape of N))))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ((( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N))))) by RELAT_1:32 .= (((( the entrance of N \ (id the carrier of N)) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((( the entrance of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the escape of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the escape of N))))) by RELAT_1:32 .= (((( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the entrance of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the escape of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the escape of N))))) by RELAT_1:35 .= (((( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the escape of N))))) .= (((( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~))) \/ ((((id ( the carrier of N \ (rng the entrance of N))) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the escape of N))))) .= (((( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~))) \/ ((((id ( the carrier of N \ (rng the entrance of N))) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by Th13 .= (((( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ ((( the entrance of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the escape of N))) ~))) \/ ((((id ( the carrier of N \ (rng the entrance of N))) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ (id ( the carrier of N \ (rng the entrance of N)))) by SYSREL:12 .= (((( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the escape of N))) * ( the entrance of N \ (id the carrier of N))) ~)) \/ ((((id ( the carrier of N \ (rng the entrance of N))) ~) * (( the escape of N \ (id the carrier of N)) ~)) \/ (id ( the carrier of N \ (rng the entrance of N)))) by RELAT_1:35 .= (((( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the escape of N))) * ( the entrance of N \ (id the carrier of N))) ~)) \/ (((( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) by RELAT_1:35 .= (((( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) ~)) \/ (((( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th13 .= (((( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) ~)) \/ (((( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th13 .= (({} ~) \/ (((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) ~)) \/ (((( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th24 .= (({} ~) \/ (( the entrance of N \ (id the carrier of N)) ~)) \/ (((( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th23 .= ({} \/ (( the entrance of N \ (id the carrier of N)) ~)) \/ ({} \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th27 .= e_escape N ; (e_entrance N) * (e_escape N) = ((( the escape of N \ (id the carrier of N)) ~) * ((( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))))) \/ ((id ( the carrier of N \ (rng the escape of N))) * ((( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))))) by SYSREL:6 .= (((( the escape of N \ (id the carrier of N)) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the entrance of N))))) \/ ((id ( the carrier of N \ (rng the escape of N))) * ((( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))))) by RELAT_1:32 .= (((( the escape of N \ (id the carrier of N)) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((( the escape of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the escape of N))) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the escape of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by RELAT_1:32 .= (((( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the escape of N))) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the escape of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by RELAT_1:35 .= (((( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~))) \/ (((id ( the carrier of N \ (rng the escape of N))) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the escape of N))) * (id ( the carrier of N \ (rng the entrance of N))))) .= (((( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~))) \/ ((((id ( the carrier of N \ (rng the escape of N))) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the escape of N))) * (id ( the carrier of N \ (rng the entrance of N))))) .= (((( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~))) \/ ((((id ( the carrier of N \ (rng the escape of N))) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ ((id ( the carrier of N \ (rng the escape of N))) * (id ( the carrier of N \ (rng the escape of N))))) by Th13 .= (((( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ ((( the escape of N \ (id the carrier of N)) ~) * ((id ( the carrier of N \ (rng the entrance of N))) ~))) \/ ((((id ( the carrier of N \ (rng the escape of N))) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ (id ( the carrier of N \ (rng the escape of N)))) by SYSREL:12 .= (((( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the entrance of N))) * ( the escape of N \ (id the carrier of N))) ~)) \/ ((((id ( the carrier of N \ (rng the escape of N))) ~) * (( the entrance of N \ (id the carrier of N)) ~)) \/ (id ( the carrier of N \ (rng the escape of N)))) by RELAT_1:35 .= (((( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the entrance of N))) * ( the escape of N \ (id the carrier of N))) ~)) \/ (((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) by RELAT_1:35 .= (((( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N))) ~)) \/ (((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) by Th13 .= (((( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))) ~) \/ (((id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N))) ~)) \/ (((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) by Th13 .= (({} ~) \/ (((id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N))) ~)) \/ (((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) by Th24 .= (({} ~) \/ (( the escape of N \ (id the carrier of N)) ~)) \/ (((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) by Th23 .= ({} \/ (( the escape of N \ (id the carrier of N)) ~)) \/ ({} \/ (id ( the carrier of N \ (rng the escape of N)))) by Th27 .= e_entrance N ; hence ( (e_entrance N) * (e_entrance N) = e_entrance N & (e_entrance N) * (e_escape N) = e_entrance N & (e_escape N) * (e_entrance N) = e_escape N & (e_escape N) * (e_escape N) = e_escape N ) by A1, A3, A2; ::_thesis: verum end; theorem :: E_SIEC:30 for N being e_net holds ( (e_entrance N) * ((e_entrance N) \ (id (e_shore N))) = {} & (e_escape N) * ((e_escape N) \ (id (e_shore N))) = {} ) proof let N be e_net; ::_thesis: ( (e_entrance N) * ((e_entrance N) \ (id (e_shore N))) = {} & (e_escape N) * ((e_escape N) \ (id (e_shore N))) = {} ) set P = the escape of N \ (id N); set Q = the entrance of N \ (id the carrier of N); set S = id ( the carrier of N \ (rng the entrance of N)); set T = id ( the carrier of N \ (rng the escape of N)); set R = id the carrier of N; A1: id ( the carrier of N \ (rng the entrance of N)) c= id the carrier of N by SYSREL:15, XBOOLE_1:36; (( the entrance of N \ (id the carrier of N)) ~) * ((( the entrance of N \ (id the carrier of N)) ~) \ (id the carrier of N)) c= (( the entrance of N \ (id the carrier of N)) ~) * (( the entrance of N \ (id the carrier of N)) ~) by RELAT_1:29, XBOOLE_1:36; then (( the entrance of N \ (id the carrier of N)) ~) * ((( the entrance of N \ (id the carrier of N)) ~) \ (id the carrier of N)) c= {} by Th25; then A2: (( the entrance of N \ (id the carrier of N)) ~) * ((( the entrance of N \ (id the carrier of N)) ~) \ (id the carrier of N)) = {} by XBOOLE_1:3; (id ( the carrier of N \ (rng the entrance of N))) * ((( the entrance of N \ (id the carrier of N)) ~) \ (id the carrier of N)) c= (id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) ~) by RELAT_1:29, XBOOLE_1:36; then (id ( the carrier of N \ (rng the entrance of N))) * ((( the entrance of N \ (id the carrier of N)) ~) \ (id the carrier of N)) c= {} by Th28; then A3: (id ( the carrier of N \ (rng the entrance of N))) * ((( the entrance of N \ (id the carrier of N)) ~) \ (id the carrier of N)) = {} by XBOOLE_1:3; A4: (e_escape N) * ((e_escape N) \ (id (e_shore N))) = ((( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) * (((( the entrance of N \ (id the carrier of N)) ~) \ (id the carrier of N)) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) by XBOOLE_1:42 .= ((( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) * (((( the entrance of N \ (id the carrier of N)) ~) \ (id the carrier of N)) \/ {}) by A1, XBOOLE_1:37 .= {} \/ {} by A2, A3, SYSREL:6 .= {} ; A5: id ( the carrier of N \ (rng the escape of N)) c= id the carrier of N by SYSREL:15, XBOOLE_1:36; (id ( the carrier of N \ (rng the escape of N))) * ((( the escape of N \ (id N)) ~) \ (id the carrier of N)) c= (id ( the carrier of N \ (rng the escape of N))) * (( the escape of N \ (id N)) ~) by RELAT_1:29, XBOOLE_1:36; then (id ( the carrier of N \ (rng the escape of N))) * ((( the escape of N \ (id N)) ~) \ (id the carrier of N)) c= {} by Th28; then A6: (id ( the carrier of N \ (rng the escape of N))) * ((( the escape of N \ (id N)) ~) \ (id the carrier of N)) = {} by XBOOLE_1:3; (( the escape of N \ (id N)) ~) * ((( the escape of N \ (id N)) ~) \ (id the carrier of N)) c= (( the escape of N \ (id N)) ~) * (( the escape of N \ (id N)) ~) by RELAT_1:29, XBOOLE_1:36; then (( the escape of N \ (id N)) ~) * ((( the escape of N \ (id N)) ~) \ (id the carrier of N)) c= {} by Th25; then A7: (( the escape of N \ (id N)) ~) * ((( the escape of N \ (id N)) ~) \ (id the carrier of N)) = {} by XBOOLE_1:3; (e_entrance N) * ((e_entrance N) \ (id (e_shore N))) = ((( the escape of N \ (id N)) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) * (((( the escape of N \ (id N)) ~) \ (id the carrier of N)) \/ ((id ( the carrier of N \ (rng the escape of N))) \ (id the carrier of N))) by XBOOLE_1:42 .= ((( the escape of N \ (id N)) ~) \/ (id ( the carrier of N \ (rng the escape of N)))) * (((( the escape of N \ (id N)) ~) \ (id the carrier of N)) \/ {}) by A5, XBOOLE_1:37 .= {} \/ {} by A7, A6, SYSREL:6 .= {} ; hence ( (e_entrance N) * ((e_entrance N) \ (id (e_shore N))) = {} & (e_escape N) * ((e_escape N) \ (id (e_shore N))) = {} ) by A4; ::_thesis: verum end; definition let N be e_net; func e_adjac N -> Relation equals :: E_SIEC:def 19 (( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N))); correctness coherence (( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N))) is Relation; ; end; :: deftheorem defines e_adjac E_SIEC:def_19_:_ for N being e_net holds e_adjac N = (( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N))); theorem :: E_SIEC:31 for N being e_net holds ( e_adjac N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] ) proof let N be e_net; ::_thesis: ( e_adjac N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] ) A1: ( the entrance of N \/ the escape of N) \ (id the carrier of N) c= the entrance of N \/ the escape of N by XBOOLE_1:36; A2: the escape of N c= [: the carrier of N, the carrier of N:] by Def1; A3: the entrance of N c= [: the carrier of N, the carrier of N:] by Def1; then the entrance of N ~ c= [: the carrier of N, the carrier of N:] by SYSREL:4; then A4: ( id the carrier of N c= [: the carrier of N, the carrier of N:] & ( the entrance of N ~) \/ the escape of N c= [: the carrier of N, the carrier of N:] ) by A2, RELSET_1:13, XBOOLE_1:8; ( id ( the carrier of N \ (rng the entrance of N)) c= id the carrier of N & id the carrier of N c= [: the carrier of N, the carrier of N:] ) by RELSET_1:13, SYSREL:15, XBOOLE_1:36; then A5: id ( the carrier of N \ (rng the entrance of N)) c= [: the carrier of N, the carrier of N:] by XBOOLE_1:1; the entrance of N \/ the escape of N c= [: the carrier of N, the carrier of N:] by A3, A2, XBOOLE_1:8; then ( the entrance of N \/ the escape of N) \ (id the carrier of N) c= [: the carrier of N, the carrier of N:] by A1, XBOOLE_1:1; hence ( e_adjac N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] ) by A5, A4, XBOOLE_1:8; ::_thesis: verum end; theorem :: E_SIEC:32 for N being e_net holds ( (e_adjac N) * (e_adjac N) = e_adjac N & ((e_adjac N) \ (id (e_shore N))) * (e_adjac N) = {} & ((e_adjac N) \/ ((e_adjac N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) ) proof let N be e_net; ::_thesis: ( (e_adjac N) * (e_adjac N) = e_adjac N & ((e_adjac N) \ (id (e_shore N))) * (e_adjac N) = {} & ((e_adjac N) \/ ((e_adjac N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) ) set P = the entrance of N; set Q = the escape of N; set R = id the carrier of N; set S = id ( the carrier of N \ (rng the entrance of N)); set T = id ( the carrier of N \ (rng the escape of N)); A1: id ( the carrier of N \ (rng the entrance of N)) c= id the carrier of N by SYSREL:15, XBOOLE_1:36; (e_adjac N) \/ ((e_adjac N) ~) = ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \/ (((( the entrance of N \/ the escape of N) \ (id the carrier of N)) ~) \/ ((id ( the carrier of N \ (rng the entrance of N))) ~)) by RELAT_1:23 .= ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \/ (((( the entrance of N \/ the escape of N) \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N)))) .= ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) ~)) \/ (id ( the carrier of N \ (rng the entrance of N))) by XBOOLE_1:5 .= ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ ((( the entrance of N \/ the escape of N) ~) \ ((id the carrier of N) ~))) \/ (id ( the carrier of N \ (rng the entrance of N))) by RELAT_1:24 .= ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ ((( the entrance of N \/ the escape of N) ~) \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N))) .= ((( the entrance of N \/ the escape of N) \/ (( the entrance of N \/ the escape of N) ~)) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N))) by XBOOLE_1:42 ; then A2: ((e_adjac N) \/ ((e_adjac N) ~)) \/ (id (e_shore N)) = ((( the entrance of N \/ the escape of N) \/ (( the entrance of N \/ the escape of N) ~)) \ (id the carrier of N)) \/ ((id ( the carrier of N \ (rng the entrance of N))) \/ (id the carrier of N)) by XBOOLE_1:4 .= ((( the entrance of N \/ the escape of N) \/ (( the entrance of N \/ the escape of N) ~)) \ (id the carrier of N)) \/ (id the carrier of N) by A1, XBOOLE_1:12 .= (((( the entrance of N ~) \/ ( the escape of N ~)) \/ ( the entrance of N \/ the escape of N)) \ (id the carrier of N)) \/ (id the carrier of N) by RELAT_1:23 .= ((( the entrance of N ~) \/ (( the escape of N \/ the entrance of N) \/ ( the escape of N ~))) \ (id the carrier of N)) \/ (id the carrier of N) by XBOOLE_1:4 .= ((( the entrance of N ~) \/ ( the escape of N \/ ( the entrance of N \/ ( the escape of N ~)))) \ (id the carrier of N)) \/ (id the carrier of N) by XBOOLE_1:4 .= (((( the entrance of N ~) \/ the escape of N) \/ ( the entrance of N \/ ( the escape of N ~))) \ (id the carrier of N)) \/ (id the carrier of N) by XBOOLE_1:4 .= ((( the entrance of N ~) \/ the escape of N) \/ ( the entrance of N \/ ( the escape of N ~))) \/ (id the carrier of N) by XBOOLE_1:39 .= (e_flow N) \/ (((( the entrance of N \/ ( the escape of N ~)) ~) ~) \/ (id the carrier of N)) by XBOOLE_1:5 .= (e_flow N) \/ (((( the entrance of N ~) \/ (( the escape of N ~) ~)) ~) \/ (id the carrier of N)) by RELAT_1:23 .= (e_flow N) \/ (((( the entrance of N ~) \/ the escape of N) ~) \/ ((id the carrier of N) ~)) .= (e_flow N) \/ ((e_flow N) ~) by RELAT_1:23 ; id ( the carrier of N \ (rng the entrance of N)) c= id the carrier of N by SYSREL:15, XBOOLE_1:36; then A3: (id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N) = {} by XBOOLE_1:37; ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= the entrance of N * ( the escape of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36; then ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Th15; then A4: ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} by XBOOLE_1:3; ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= the entrance of N * ( the entrance of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36; then ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= {} by Def2; then A5: ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} by XBOOLE_1:3; ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= the escape of N * ( the entrance of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36; then ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) c= {} by Th15; then A6: ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} by XBOOLE_1:3; ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= the escape of N * ( the escape of N \ (id the carrier of N)) by RELAT_1:30, XBOOLE_1:36; then ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) c= {} by Def2; then A7: ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} by XBOOLE_1:3; A8: ((e_adjac N) \ (id the carrier of N)) * (e_adjac N) = ((((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by RELAT_1:32 .= ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:42 .= ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \ (id the carrier of N)) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:42 .= ((((( the entrance of N \ (id the carrier of N)) \ (id the carrier of N)) \/ (( the escape of N \ (id the carrier of N)) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:42 .= (((( the entrance of N \ ((id the carrier of N) \/ (id the carrier of N))) \/ (( the escape of N \ (id the carrier of N)) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:41 .= (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ ((id the carrier of N) \/ (id the carrier of N)))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:41 .= (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:42 .= (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by XBOOLE_1:42 .= ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * ( the entrance of N \ (id the carrier of N))) \/ (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * ( the escape of N \ (id the carrier of N)))) \/ ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by RELAT_1:32 .= ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * ( the entrance of N \ (id the carrier of N))) \/ (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * ( the escape of N \ (id the carrier of N))) \/ (((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))))) \/ ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by SYSREL:6 .= ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * ( the entrance of N \ (id the carrier of N))) \/ (((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)))) \/ (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * ( the escape of N \ (id the carrier of N))) \/ (((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))))) \/ ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by SYSREL:6 .= ((({} \/ {}) \/ (((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)))) \/ (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * ( the escape of N \ (id the carrier of N))) \/ (((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N))))) \/ ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by A5, A6, SYSREL:6 .= (({} * ( the entrance of N \ (id the carrier of N))) \/ ({} * ( the escape of N \ (id the carrier of N)))) \/ ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N)))) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by A3, A4, A7, SYSREL:6 .= (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \ (id the carrier of N)) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))) by XBOOLE_1:42 .= (((( the entrance of N \ (id the carrier of N)) \ (id the carrier of N)) \/ (( the escape of N \ (id the carrier of N)) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))) by XBOOLE_1:42 .= ((( the entrance of N \ ((id the carrier of N) \/ (id the carrier of N))) \/ (( the escape of N \ (id the carrier of N)) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))) by XBOOLE_1:41 .= ((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ ((id the carrier of N) \/ (id the carrier of N)))) \/ ((id ( the carrier of N \ (rng the entrance of N))) \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))) by XBOOLE_1:41 .= (( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) \/ (( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by A3, SYSREL:6 .= {} \/ (( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) by Th27 .= {} \/ (( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) by Th13 .= {} by Th27 ; (e_adjac N) * (e_adjac N) = ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) * ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N))))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N))))) by SYSREL:6 .= (((( the entrance of N \/ the escape of N) \ (id the carrier of N)) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N))))) by RELAT_1:32 .= (((( the entrance of N \/ the escape of N) \ (id the carrier of N)) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by RELAT_1:32 .= (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by XBOOLE_1:42 .= (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((( the entrance of N \/ the escape of N) \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by XBOOLE_1:42 .= (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \/ the escape of N) \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by XBOOLE_1:42 .= (((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by XBOOLE_1:42 .= ((((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * ( the entrance of N \ (id the carrier of N))) \/ ((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * ( the escape of N \ (id the carrier of N)))) \/ ((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by RELAT_1:32 .= ((({} \/ {}) \/ ((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * ( the escape of N \ (id the carrier of N)))) \/ ((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by A5, A6, SYSREL:6 .= ({} \/ ((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * (id ( the carrier of N \ (rng the entrance of N))))) by A4, A7, SYSREL:6 .= ((( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) * (id ( the carrier of N \ (rng the entrance of N)))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ (id ( the carrier of N \ (rng the entrance of N)))) by SYSREL:12 .= ((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) \/ (( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))))) \/ (((id ( the carrier of N \ (rng the entrance of N))) * (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N)))) \/ (id ( the carrier of N \ (rng the entrance of N)))) by SYSREL:6 .= ((( the entrance of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N)))) \/ (( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))))) \/ ((((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ( the escape of N \ (id the carrier of N)))) \/ (id ( the carrier of N \ (rng the entrance of N)))) by RELAT_1:32 .= ({} \/ (( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the entrance of N))))) \/ ((((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ( the escape of N \ (id the carrier of N)))) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th27 .= (( the escape of N \ (id the carrier of N)) * (id ( the carrier of N \ (rng the escape of N)))) \/ ((((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ( the escape of N \ (id the carrier of N)))) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th13 .= {} \/ ((((id ( the carrier of N \ (rng the entrance of N))) * ( the entrance of N \ (id the carrier of N))) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ( the escape of N \ (id the carrier of N)))) \/ (id ( the carrier of N \ (rng the entrance of N)))) by Th27 .= (( the entrance of N \ (id the carrier of N)) \/ ((id ( the carrier of N \ (rng the entrance of N))) * ( the escape of N \ (id the carrier of N)))) \/ (id ( the carrier of N \ (rng the entrance of N))) by Th23 .= (( the entrance of N \ (id the carrier of N)) \/ ((id ( the carrier of N \ (rng the escape of N))) * ( the escape of N \ (id the carrier of N)))) \/ (id ( the carrier of N \ (rng the entrance of N))) by Th13 .= (( the entrance of N \ (id the carrier of N)) \/ ( the escape of N \ (id the carrier of N))) \/ (id ( the carrier of N \ (rng the entrance of N))) by Th23 .= e_adjac N by XBOOLE_1:42 ; hence ( (e_adjac N) * (e_adjac N) = e_adjac N & ((e_adjac N) \ (id (e_shore N))) * (e_adjac N) = {} & ((e_adjac N) \/ ((e_adjac N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) ) by A8, A2; ::_thesis: verum end; theorem Th33: :: E_SIEC:33 for N being e_net holds ( ( the entrance of N \ (id the carrier of N)) ~ c= [:(e_Places N),(e_Transitions N):] & ( the escape of N \ (id the carrier of N)) ~ c= [:(e_Places N),(e_Transitions N):] ) proof let N be e_net; ::_thesis: ( ( the entrance of N \ (id the carrier of N)) ~ c= [:(e_Places N),(e_Transitions N):] & ( the escape of N \ (id the carrier of N)) ~ c= [:(e_Places N),(e_Transitions N):] ) ( the entrance of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] & the escape of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] ) by Th18; hence ( ( the entrance of N \ (id the carrier of N)) ~ c= [:(e_Places N),(e_Transitions N):] & ( the escape of N \ (id the carrier of N)) ~ c= [:(e_Places N),(e_Transitions N):] ) by SYSREL:4; ::_thesis: verum end; definition let N be G_Net ; func s_pre N -> Relation equals :: E_SIEC:def 20 ( the escape of N \ (id the carrier of N)) ~ ; coherence ( the escape of N \ (id the carrier of N)) ~ is Relation ; func s_post N -> Relation equals :: E_SIEC:def 21 ( the entrance of N \ (id the carrier of N)) ~ ; coherence ( the entrance of N \ (id the carrier of N)) ~ is Relation ; end; :: deftheorem defines s_pre E_SIEC:def_20_:_ for N being G_Net holds s_pre N = ( the escape of N \ (id the carrier of N)) ~ ; :: deftheorem defines s_post E_SIEC:def_21_:_ for N being G_Net holds s_post N = ( the entrance of N \ (id the carrier of N)) ~ ; theorem :: E_SIEC:34 for N being e_net holds ( s_post N c= [:(e_Places N),(e_Transitions N):] & s_pre N c= [:(e_Places N),(e_Transitions N):] ) by Th33;