:: NET_1 semantic presentation begin definition let P be PT_net_Str ; func Flow P -> set equals :: NET_1:def 1 the S-T_Arcs of P \/ the T-S_Arcs of P; coherence the S-T_Arcs of P \/ the T-S_Arcs of P is set ; end; :: deftheorem defines Flow NET_1:def_1_:_ for P being PT_net_Str holds Flow P = the S-T_Arcs of P \/ the T-S_Arcs of P; registration let P be PT_net_Str ; cluster Flow P -> Relation-like ; coherence Flow P is Relation-like ; end; definition let N be PT_net_Str ; attrN is Petri means :Def2: :: NET_1:def 2 ( the carrier of N misses the carrier' of N & Flow N c= [: the carrier of N, the carrier' of N:] \/ [: the carrier' of N, the carrier of N:] ); end; :: deftheorem Def2 defines Petri NET_1:def_2_:_ for N being PT_net_Str holds ( N is Petri iff ( the carrier of N misses the carrier' of N & Flow N c= [: the carrier of N, the carrier' of N:] \/ [: the carrier' of N, the carrier of N:] ) ); definition let N be PT_net_Str ; func Elements N -> set equals :: NET_1:def 3 the carrier of N \/ the carrier' of N; correctness coherence the carrier of N \/ the carrier' of N is set ; ; end; :: deftheorem defines Elements NET_1:def_3_:_ for N being PT_net_Str holds Elements N = the carrier of N \/ the carrier' of N; theorem :: NET_1:1 for x being set for N being PT_net_Str holds ( not Elements N <> {} or not x is Element of Elements N or x is Element of the carrier of N or x is Element of the carrier' of N ) by XBOOLE_0:def_3; theorem :: NET_1:2 for x being set for N being PT_net_Str st x is Element of the carrier of N & the carrier of N <> {} holds x is Element of Elements N proof let x be set ; ::_thesis: for N being PT_net_Str st x is Element of the carrier of N & the carrier of N <> {} holds x is Element of Elements N let N be PT_net_Str ; ::_thesis: ( x is Element of the carrier of N & the carrier of N <> {} implies x is Element of Elements N ) A1: the carrier of N c= Elements N by XBOOLE_1:7; assume ( x is Element of the carrier of N & the carrier of N <> {} ) ; ::_thesis: x is Element of Elements N hence x is Element of Elements N by A1, TARSKI:def_3; ::_thesis: verum end; theorem :: NET_1:3 for x being set for N being PT_net_Str st x is Element of the carrier' of N & the carrier' of N <> {} holds x is Element of Elements N proof let x be set ; ::_thesis: for N being PT_net_Str st x is Element of the carrier' of N & the carrier' of N <> {} holds x is Element of Elements N let N be PT_net_Str ; ::_thesis: ( x is Element of the carrier' of N & the carrier' of N <> {} implies x is Element of Elements N ) A1: the carrier' of N c= Elements N by XBOOLE_1:7; assume ( x is Element of the carrier' of N & the carrier' of N <> {} ) ; ::_thesis: x is Element of Elements N hence x is Element of Elements N by A1, TARSKI:def_3; ::_thesis: verum end; Lm1: PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) is Petri proof set N = PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #); thus the carrier of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) /\ the carrier' of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) = {} ; :: according to XBOOLE_0:def_7,NET_1:def_2 ::_thesis: Flow PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) c= [: the carrier of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #), the carrier' of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #):] \/ [: the carrier' of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #), the carrier of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #):] thus Flow PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) c= [: the carrier of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #), the carrier' of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #):] \/ [: the carrier' of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #), the carrier of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #):] ; ::_thesis: verum end; registration cluster PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) -> Petri ; coherence PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) is Petri by Lm1; end; registration cluster strict Petri for PT_net_Str ; existence ex b1 being PT_net_Str st ( b1 is strict & b1 is Petri ) proof PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) is Petri ; hence ex b1 being PT_net_Str st ( b1 is strict & b1 is Petri ) ; ::_thesis: verum end; end; definition mode Pnet is Petri PT_net_Str ; end; theorem Th4: :: NET_1:4 for x being set for N being Pnet holds ( not x in the carrier of N or not x in the carrier' of N ) proof let x be set ; ::_thesis: for N being Pnet holds ( not x in the carrier of N or not x in the carrier' of N ) let N be Pnet; ::_thesis: ( not x in the carrier of N or not x in the carrier' of N ) the carrier of N misses the carrier' of N by Def2; hence ( not x in the carrier of N or not x in the carrier' of N ) by XBOOLE_0:3; ::_thesis: verum end; theorem Th5: :: NET_1:5 for x, y being set for N being Pnet st [x,y] in Flow N & x in the carrier' of N holds y in the carrier of N proof let x, y be set ; ::_thesis: for N being Pnet st [x,y] in Flow N & x in the carrier' of N holds y in the carrier of N let N be Pnet; ::_thesis: ( [x,y] in Flow N & x in the carrier' of N implies y in the carrier of N ) assume that A1: [x,y] in Flow N and A2: x in the carrier' of N ; ::_thesis: y in the carrier of N A3: not x in the carrier of N by A2, Th4; Flow N c= [: the carrier of N, the carrier' of N:] \/ [: the carrier' of N, the carrier of N:] by Def2; then ( [x,y] in [: the carrier of N, the carrier' of N:] or [x,y] in [: the carrier' of N, the carrier of N:] ) by A1, XBOOLE_0:def_3; hence y in the carrier of N by A3, ZFMISC_1:87; ::_thesis: verum end; theorem Th6: :: NET_1:6 for x, y being set for N being Pnet st [x,y] in Flow N & y in the carrier' of N holds x in the carrier of N proof let x, y be set ; ::_thesis: for N being Pnet st [x,y] in Flow N & y in the carrier' of N holds x in the carrier of N let N be Pnet; ::_thesis: ( [x,y] in Flow N & y in the carrier' of N implies x in the carrier of N ) assume that A1: [x,y] in Flow N and A2: y in the carrier' of N ; ::_thesis: x in the carrier of N A3: not y in the carrier of N by A2, Th4; Flow N c= [: the carrier of N, the carrier' of N:] \/ [: the carrier' of N, the carrier of N:] by Def2; then ( [x,y] in [: the carrier of N, the carrier' of N:] or [x,y] in [: the carrier' of N, the carrier of N:] ) by A1, XBOOLE_0:def_3; hence x in the carrier of N by A3, ZFMISC_1:87; ::_thesis: verum end; theorem :: NET_1:7 for x, y being set for N being Pnet st [x,y] in Flow N & x in the carrier of N holds y in the carrier' of N proof let x, y be set ; ::_thesis: for N being Pnet st [x,y] in Flow N & x in the carrier of N holds y in the carrier' of N let N be Pnet; ::_thesis: ( [x,y] in Flow N & x in the carrier of N implies y in the carrier' of N ) assume that A1: [x,y] in Flow N and A2: x in the carrier of N ; ::_thesis: y in the carrier' of N A3: not x in the carrier' of N by A2, Th4; Flow N c= [: the carrier of N, the carrier' of N:] \/ [: the carrier' of N, the carrier of N:] by Def2; then ( [x,y] in [: the carrier' of N, the carrier of N:] or [x,y] in [: the carrier of N, the carrier' of N:] ) by A1, XBOOLE_0:def_3; hence y in the carrier' of N by A3, ZFMISC_1:87; ::_thesis: verum end; theorem :: NET_1:8 for x, y being set for N being Pnet st [x,y] in Flow N & y in the carrier of N holds x in the carrier' of N proof let x, y be set ; ::_thesis: for N being Pnet st [x,y] in Flow N & y in the carrier of N holds x in the carrier' of N let N be Pnet; ::_thesis: ( [x,y] in Flow N & y in the carrier of N implies x in the carrier' of N ) assume that A1: [x,y] in Flow N and A2: y in the carrier of N ; ::_thesis: x in the carrier' of N A3: not y in the carrier' of N by A2, Th4; Flow N c= [: the carrier of N, the carrier' of N:] \/ [: the carrier' of N, the carrier of N:] by Def2; then ( [x,y] in [: the carrier' of N, the carrier of N:] or [x,y] in [: the carrier of N, the carrier' of N:] ) by A1, XBOOLE_0:def_3; hence x in the carrier' of N by A3, ZFMISC_1:87; ::_thesis: verum end; definition let N be Pnet; let x, y be set ; pred pre N,x,y means :Def4: :: NET_1:def 4 ( [y,x] in Flow N & x in the carrier' of N ); pred post N,x,y means :Def5: :: NET_1:def 5 ( [x,y] in Flow N & x in the carrier' of N ); end; :: deftheorem Def4 defines pre NET_1:def_4_:_ for N being Pnet for x, y being set holds ( pre N,x,y iff ( [y,x] in Flow N & x in the carrier' of N ) ); :: deftheorem Def5 defines post NET_1:def_5_:_ for N being Pnet for x, y being set holds ( post N,x,y iff ( [x,y] in Flow N & x in the carrier' of N ) ); definition let N be PT_net_Str ; let x be Element of Elements N; func Pre (N,x) -> set means :Def6: :: NET_1:def 6 for y being set holds ( y in it iff ( y in Elements N & [y,x] in Flow N ) ); existence ex b1 being set st for y being set holds ( y in b1 iff ( y in Elements N & [y,x] in Flow N ) ) proof defpred S1[ set ] means [\$1,x] in Flow N; thus ex IT being set st for y being set holds ( y in IT iff ( y in Elements N & S1[y] ) ) from XBOOLE_0:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being set st ( for y being set holds ( y in b1 iff ( y in Elements N & [y,x] in Flow N ) ) ) & ( for y being set holds ( y in b2 iff ( y in Elements N & [y,x] in Flow N ) ) ) holds b1 = b2 proof let X, Y be set ; ::_thesis: ( ( for y being set holds ( y in X iff ( y in Elements N & [y,x] in Flow N ) ) ) & ( for y being set holds ( y in Y iff ( y in Elements N & [y,x] in Flow N ) ) ) implies X = Y ) assume that A1: for y being set holds ( y in X iff ( y in Elements N & [y,x] in Flow N ) ) and A2: for y being set holds ( y in Y iff ( y in Elements N & [y,x] in Flow N ) ) ; ::_thesis: X = Y A3: for y being set st y in Y holds y in X proof let y be set ; ::_thesis: ( y in Y implies y in X ) assume y in Y ; ::_thesis: y in X then ( y in Elements N & [y,x] in Flow N ) by A2; hence y in X by A1; ::_thesis: verum end; for y being set st y in X holds y in Y proof let y be set ; ::_thesis: ( y in X implies y in Y ) assume y in X ; ::_thesis: y in Y then ( y in Elements N & [y,x] in Flow N ) by A1; hence y in Y by A2; ::_thesis: verum end; hence X = Y by A3, TARSKI:1; ::_thesis: verum end; func Post (N,x) -> set means :Def7: :: NET_1:def 7 for y being set holds ( y in it iff ( y in Elements N & [x,y] in Flow N ) ); existence ex b1 being set st for y being set holds ( y in b1 iff ( y in Elements N & [x,y] in Flow N ) ) proof defpred S1[ set ] means [x,\$1] in Flow N; thus ex IT being set st for y being set holds ( y in IT iff ( y in Elements N & S1[y] ) ) from XBOOLE_0:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being set st ( for y being set holds ( y in b1 iff ( y in Elements N & [x,y] in Flow N ) ) ) & ( for y being set holds ( y in b2 iff ( y in Elements N & [x,y] in Flow N ) ) ) holds b1 = b2 proof let X, Y be set ; ::_thesis: ( ( for y being set holds ( y in X iff ( y in Elements N & [x,y] in Flow N ) ) ) & ( for y being set holds ( y in Y iff ( y in Elements N & [x,y] in Flow N ) ) ) implies X = Y ) assume that A4: for y being set holds ( y in X iff ( y in Elements N & [x,y] in Flow N ) ) and A5: for y being set holds ( y in Y iff ( y in Elements N & [x,y] in Flow N ) ) ; ::_thesis: X = Y A6: for y being set st y in Y holds y in X proof let y be set ; ::_thesis: ( y in Y implies y in X ) assume y in Y ; ::_thesis: y in X then ( y in Elements N & [x,y] in Flow N ) by A5; hence y in X by A4; ::_thesis: verum end; for y being set st y in X holds y in Y proof let y be set ; ::_thesis: ( y in X implies y in Y ) assume y in X ; ::_thesis: y in Y then ( y in Elements N & [x,y] in Flow N ) by A4; hence y in Y by A5; ::_thesis: verum end; hence X = Y by A6, TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def6 defines Pre NET_1:def_6_:_ for N being PT_net_Str for x being Element of Elements N for b3 being set holds ( b3 = Pre (N,x) iff for y being set holds ( y in b3 iff ( y in Elements N & [y,x] in Flow N ) ) ); :: deftheorem Def7 defines Post NET_1:def_7_:_ for N being PT_net_Str for x being Element of Elements N for b3 being set holds ( b3 = Post (N,x) iff for y being set holds ( y in b3 iff ( y in Elements N & [x,y] in Flow N ) ) ); theorem Th9: :: NET_1:9 for N being Pnet for x being Element of Elements N holds Pre (N,x) c= Elements N proof let N be Pnet; ::_thesis: for x being Element of Elements N holds Pre (N,x) c= Elements N let x be Element of Elements N; ::_thesis: Pre (N,x) c= Elements N for y being set st y in Pre (N,x) holds y in Elements N by Def6; hence Pre (N,x) c= Elements N by TARSKI:def_3; ::_thesis: verum end; theorem :: NET_1:10 for N being Pnet for x being Element of Elements N holds Pre (N,x) c= Elements N by Th9; theorem Th11: :: NET_1:11 for N being Pnet for x being Element of Elements N holds Post (N,x) c= Elements N proof let N be Pnet; ::_thesis: for x being Element of Elements N holds Post (N,x) c= Elements N let x be Element of Elements N; ::_thesis: Post (N,x) c= Elements N for y being set st y in Post (N,x) holds y in Elements N by Def7; hence Post (N,x) c= Elements N by TARSKI:def_3; ::_thesis: verum end; theorem :: NET_1:12 for N being Pnet for x being Element of Elements N holds Post (N,x) c= Elements N by Th11; theorem :: NET_1:13 for x being set for N being Pnet for y being Element of Elements N st y in the carrier' of N holds ( x in Pre (N,y) iff pre N,y,x ) proof let x be set ; ::_thesis: for N being Pnet for y being Element of Elements N st y in the carrier' of N holds ( x in Pre (N,y) iff pre N,y,x ) let N be Pnet; ::_thesis: for y being Element of Elements N st y in the carrier' of N holds ( x in Pre (N,y) iff pre N,y,x ) let y be Element of Elements N; ::_thesis: ( y in the carrier' of N implies ( x in Pre (N,y) iff pre N,y,x ) ) assume A1: y in the carrier' of N ; ::_thesis: ( x in Pre (N,y) iff pre N,y,x ) A2: ( pre N,y,x implies x in Pre (N,y) ) proof assume pre N,y,x ; ::_thesis: x in Pre (N,y) then A3: [x,y] in Flow N by Def4; then x in the carrier of N by A1, Th6; then x in Elements N by XBOOLE_0:def_3; hence x in Pre (N,y) by A3, Def6; ::_thesis: verum end; ( x in Pre (N,y) implies pre N,y,x ) proof assume x in Pre (N,y) ; ::_thesis: pre N,y,x then [x,y] in Flow N by Def6; hence pre N,y,x by A1, Def4; ::_thesis: verum end; hence ( x in Pre (N,y) iff pre N,y,x ) by A2; ::_thesis: verum end; theorem :: NET_1:14 for x being set for N being Pnet for y being Element of Elements N st y in the carrier' of N holds ( x in Post (N,y) iff post N,y,x ) proof let x be set ; ::_thesis: for N being Pnet for y being Element of Elements N st y in the carrier' of N holds ( x in Post (N,y) iff post N,y,x ) let N be Pnet; ::_thesis: for y being Element of Elements N st y in the carrier' of N holds ( x in Post (N,y) iff post N,y,x ) let y be Element of Elements N; ::_thesis: ( y in the carrier' of N implies ( x in Post (N,y) iff post N,y,x ) ) assume A1: y in the carrier' of N ; ::_thesis: ( x in Post (N,y) iff post N,y,x ) A2: ( post N,y,x implies x in Post (N,y) ) proof assume post N,y,x ; ::_thesis: x in Post (N,y) then A3: [y,x] in Flow N by Def5; then x in the carrier of N by A1, Th5; then x in Elements N by XBOOLE_0:def_3; hence x in Post (N,y) by A3, Def7; ::_thesis: verum end; ( x in Post (N,y) implies post N,y,x ) proof assume x in Post (N,y) ; ::_thesis: post N,y,x then [y,x] in Flow N by Def7; hence post N,y,x by A1, Def5; ::_thesis: verum end; hence ( x in Post (N,y) iff post N,y,x ) by A2; ::_thesis: verum end; definition let N be Pnet; let x be Element of Elements N; assume A1: Elements N <> {} ; func enter (N,x) -> set means :Def8: :: NET_1:def 8 ( ( x in the carrier of N implies it = {x} ) & ( x in the carrier' of N implies it = Pre (N,x) ) ); existence ex b1 being set st ( ( x in the carrier of N implies b1 = {x} ) & ( x in the carrier' of N implies b1 = Pre (N,x) ) ) proof ( not x in the carrier of N or not x in the carrier' of N ) by Th4; hence ex b1 being set st ( ( x in the carrier of N implies b1 = {x} ) & ( x in the carrier' of N implies b1 = Pre (N,x) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being set st ( x in the carrier of N implies b1 = {x} ) & ( x in the carrier' of N implies b1 = Pre (N,x) ) & ( x in the carrier of N implies b2 = {x} ) & ( x in the carrier' of N implies b2 = Pre (N,x) ) holds b1 = b2 by A1, XBOOLE_0:def_3; end; :: deftheorem Def8 defines enter NET_1:def_8_:_ for N being Pnet for x being Element of Elements N st Elements N <> {} holds for b3 being set holds ( b3 = enter (N,x) iff ( ( x in the carrier of N implies b3 = {x} ) & ( x in the carrier' of N implies b3 = Pre (N,x) ) ) ); theorem Th15: :: NET_1:15 for N being Pnet for x being Element of Elements N holds ( not Elements N <> {} or enter (N,x) = {x} or enter (N,x) = Pre (N,x) ) proof let N be Pnet; ::_thesis: for x being Element of Elements N holds ( not Elements N <> {} or enter (N,x) = {x} or enter (N,x) = Pre (N,x) ) let x be Element of Elements N; ::_thesis: ( not Elements N <> {} or enter (N,x) = {x} or enter (N,x) = Pre (N,x) ) assume Elements N <> {} ; ::_thesis: ( enter (N,x) = {x} or enter (N,x) = Pre (N,x) ) then ( x in the carrier of N or x in the carrier' of N ) by XBOOLE_0:def_3; hence ( enter (N,x) = {x} or enter (N,x) = Pre (N,x) ) by Def8; ::_thesis: verum end; theorem Th16: :: NET_1:16 for N being Pnet for x being Element of Elements N st Elements N <> {} holds enter (N,x) c= Elements N proof let N be Pnet; ::_thesis: for x being Element of Elements N st Elements N <> {} holds enter (N,x) c= Elements N let x be Element of Elements N; ::_thesis: ( Elements N <> {} implies enter (N,x) c= Elements N ) assume A1: Elements N <> {} ; ::_thesis: enter (N,x) c= Elements N A2: ( enter (N,x) = {x} implies enter (N,x) c= Elements N ) proof x in Elements N by A1; then A3: for y being set st y in {x} holds y in Elements N by TARSKI:def_1; assume enter (N,x) = {x} ; ::_thesis: enter (N,x) c= Elements N hence enter (N,x) c= Elements N by A3, TARSKI:def_3; ::_thesis: verum end; ( enter (N,x) = {x} or enter (N,x) = Pre (N,x) ) by A1, Th15; hence enter (N,x) c= Elements N by A2, Th9; ::_thesis: verum end; theorem :: NET_1:17 for N being Pnet for x being Element of Elements N st Elements N <> {} holds enter (N,x) c= Elements N by Th16; definition let N be Pnet; let x be Element of Elements N; assume A1: Elements N <> {} ; func exit (N,x) -> set means :Def9: :: NET_1:def 9 ( ( x in the carrier of N implies it = {x} ) & ( x in the carrier' of N implies it = Post (N,x) ) ); existence ex b1 being set st ( ( x in the carrier of N implies b1 = {x} ) & ( x in the carrier' of N implies b1 = Post (N,x) ) ) proof ( not x in the carrier of N or not x in the carrier' of N ) by Th4; hence ex b1 being set st ( ( x in the carrier of N implies b1 = {x} ) & ( x in the carrier' of N implies b1 = Post (N,x) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being set st ( x in the carrier of N implies b1 = {x} ) & ( x in the carrier' of N implies b1 = Post (N,x) ) & ( x in the carrier of N implies b2 = {x} ) & ( x in the carrier' of N implies b2 = Post (N,x) ) holds b1 = b2 by A1, XBOOLE_0:def_3; end; :: deftheorem Def9 defines exit NET_1:def_9_:_ for N being Pnet for x being Element of Elements N st Elements N <> {} holds for b3 being set holds ( b3 = exit (N,x) iff ( ( x in the carrier of N implies b3 = {x} ) & ( x in the carrier' of N implies b3 = Post (N,x) ) ) ); theorem Th18: :: NET_1:18 for N being Pnet for x being Element of Elements N holds ( not Elements N <> {} or exit (N,x) = {x} or exit (N,x) = Post (N,x) ) proof let N be Pnet; ::_thesis: for x being Element of Elements N holds ( not Elements N <> {} or exit (N,x) = {x} or exit (N,x) = Post (N,x) ) let x be Element of Elements N; ::_thesis: ( not Elements N <> {} or exit (N,x) = {x} or exit (N,x) = Post (N,x) ) assume Elements N <> {} ; ::_thesis: ( exit (N,x) = {x} or exit (N,x) = Post (N,x) ) then ( x in the carrier of N or x in the carrier' of N ) by XBOOLE_0:def_3; hence ( exit (N,x) = {x} or exit (N,x) = Post (N,x) ) by Def9; ::_thesis: verum end; theorem Th19: :: NET_1:19 for N being Pnet for x being Element of Elements N st Elements N <> {} holds exit (N,x) c= Elements N proof let N be Pnet; ::_thesis: for x being Element of Elements N st Elements N <> {} holds exit (N,x) c= Elements N let x be Element of Elements N; ::_thesis: ( Elements N <> {} implies exit (N,x) c= Elements N ) assume A1: Elements N <> {} ; ::_thesis: exit (N,x) c= Elements N A2: ( exit (N,x) = {x} implies exit (N,x) c= Elements N ) proof x in Elements N by A1; then A3: for y being set st y in {x} holds y in Elements N by TARSKI:def_1; assume exit (N,x) = {x} ; ::_thesis: exit (N,x) c= Elements N hence exit (N,x) c= Elements N by A3, TARSKI:def_3; ::_thesis: verum end; ( exit (N,x) = {x} or exit (N,x) = Post (N,x) ) by A1, Th18; hence exit (N,x) c= Elements N by A2, Th11; ::_thesis: verum end; theorem :: NET_1:20 for N being Pnet for x being Element of Elements N st Elements N <> {} holds exit (N,x) c= Elements N by Th19; definition let N be Pnet; let x be Element of Elements N; func field (N,x) -> set equals :: NET_1:def 10 (enter (N,x)) \/ (exit (N,x)); correctness coherence (enter (N,x)) \/ (exit (N,x)) is set ; ; end; :: deftheorem defines field NET_1:def_10_:_ for N being Pnet for x being Element of Elements N holds field (N,x) = (enter (N,x)) \/ (exit (N,x)); definition let N be PT_net_Str ; let x be Element of the carrier' of N; func Prec (N,x) -> set means :: NET_1:def 11 for y being set holds ( y in it iff ( y in the carrier of N & [y,x] in Flow N ) ); existence ex b1 being set st for y being set holds ( y in b1 iff ( y in the carrier of N & [y,x] in Flow N ) ) proof defpred S1[ set ] means [\$1,x] in Flow N; thus ex IT being set st for y being set holds ( y in IT iff ( y in the carrier of N & S1[y] ) ) from XBOOLE_0:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being set st ( for y being set holds ( y in b1 iff ( y in the carrier of N & [y,x] in Flow N ) ) ) & ( for y being set holds ( y in b2 iff ( y in the carrier of N & [y,x] in Flow N ) ) ) holds b1 = b2 proof let X, Y be set ; ::_thesis: ( ( for y being set holds ( y in X iff ( y in the carrier of N & [y,x] in Flow N ) ) ) & ( for y being set holds ( y in Y iff ( y in the carrier of N & [y,x] in Flow N ) ) ) implies X = Y ) assume that A1: for y being set holds ( y in X iff ( y in the carrier of N & [y,x] in Flow N ) ) and A2: for y being set holds ( y in Y iff ( y in the carrier of N & [y,x] in Flow N ) ) ; ::_thesis: X = Y A3: for y being set st y in Y holds y in X proof let y be set ; ::_thesis: ( y in Y implies y in X ) assume y in Y ; ::_thesis: y in X then ( y in the carrier of N & [y,x] in Flow N ) by A2; hence y in X by A1; ::_thesis: verum end; for y being set st y in X holds y in Y proof let y be set ; ::_thesis: ( y in X implies y in Y ) assume y in X ; ::_thesis: y in Y then ( y in the carrier of N & [y,x] in Flow N ) by A1; hence y in Y by A2; ::_thesis: verum end; hence X = Y by A3, TARSKI:1; ::_thesis: verum end; func Postc (N,x) -> set means :: NET_1:def 12 for y being set holds ( y in it iff ( y in the carrier of N & [x,y] in Flow N ) ); existence ex b1 being set st for y being set holds ( y in b1 iff ( y in the carrier of N & [x,y] in Flow N ) ) proof defpred S1[ set ] means [x,\$1] in Flow N; thus ex IT being set st for y being set holds ( y in IT iff ( y in the carrier of N & S1[y] ) ) from XBOOLE_0:sch_1(); ::_thesis: verum end; uniqueness for b1, b2 being set st ( for y being set holds ( y in b1 iff ( y in the carrier of N & [x,y] in Flow N ) ) ) & ( for y being set holds ( y in b2 iff ( y in the carrier of N & [x,y] in Flow N ) ) ) holds b1 = b2 proof let X, Y be set ; ::_thesis: ( ( for y being set holds ( y in X iff ( y in the carrier of N & [x,y] in Flow N ) ) ) & ( for y being set holds ( y in Y iff ( y in the carrier of N & [x,y] in Flow N ) ) ) implies X = Y ) assume that A4: for y being set holds ( y in X iff ( y in the carrier of N & [x,y] in Flow N ) ) and A5: for y being set holds ( y in Y iff ( y in the carrier of N & [x,y] in Flow N ) ) ; ::_thesis: X = Y A6: for y being set st y in Y holds y in X proof let y be set ; ::_thesis: ( y in Y implies y in X ) assume y in Y ; ::_thesis: y in X then ( y in the carrier of N & [x,y] in Flow N ) by A5; hence y in X by A4; ::_thesis: verum end; for y being set st y in X holds y in Y proof let y be set ; ::_thesis: ( y in X implies y in Y ) assume y in X ; ::_thesis: y in Y then ( y in the carrier of N & [x,y] in Flow N ) by A4; hence y in Y by A5; ::_thesis: verum end; hence X = Y by A6, TARSKI:1; ::_thesis: verum end; end; :: deftheorem defines Prec NET_1:def_11_:_ for N being PT_net_Str for x being Element of the carrier' of N for b3 being set holds ( b3 = Prec (N,x) iff for y being set holds ( y in b3 iff ( y in the carrier of N & [y,x] in Flow N ) ) ); :: deftheorem defines Postc NET_1:def_12_:_ for N being PT_net_Str for x being Element of the carrier' of N for b3 being set holds ( b3 = Postc (N,x) iff for y being set holds ( y in b3 iff ( y in the carrier of N & [x,y] in Flow N ) ) ); definition let N be Pnet; let X be set ; func Entr (N,X) -> set means :Def13: :: NET_1:def 13 for x being set holds ( x in it iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = enter (N,y) ) ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = enter (N,y) ) ) ) proof defpred S1[ set ] means ex y being Element of Elements N st ( y in X & \$1 = enter (N,y) ); consider F being Subset-Family of (Elements N) such that A1: for x being Subset of (Elements N) holds ( x in F iff S1[x] ) from SUBSET_1:sch_3(); take F ; ::_thesis: for x being set holds ( x in F iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = enter (N,y) ) ) ) thus for x being set holds ( x in F iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = enter (N,y) ) ) ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = enter (N,y) ) ) ) ) & ( for x being set holds ( x in b2 iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = enter (N,y) ) ) ) ) holds b1 = b2 proof let W, Y be set ; ::_thesis: ( ( for x being set holds ( x in W iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = enter (N,y) ) ) ) ) & ( for x being set holds ( x in Y iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = enter (N,y) ) ) ) ) implies W = Y ) assume that A2: for x being set holds ( x in W iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = enter (N,y) ) ) ) and A3: for x being set holds ( x in Y iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = enter (N,y) ) ) ) ; ::_thesis: W = Y A4: for x being set st x in Y holds x in W proof let x be set ; ::_thesis: ( x in Y implies x in W ) assume x in Y ; ::_thesis: x in W then ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = enter (N,y) ) ) by A3; hence x in W by A2; ::_thesis: verum end; for x being set st x in W holds x in Y proof let x be set ; ::_thesis: ( x in W implies x in Y ) assume x in W ; ::_thesis: x in Y then ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = enter (N,y) ) ) by A2; hence x in Y by A3; ::_thesis: verum end; hence W = Y by A4, TARSKI:1; ::_thesis: verum end; func Ext (N,X) -> set means :Def14: :: NET_1:def 14 for x being set holds ( x in it iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = exit (N,y) ) ) ); existence ex b1 being set st for x being set holds ( x in b1 iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = exit (N,y) ) ) ) proof defpred S1[ set ] means ex y being Element of Elements N st ( y in X & \$1 = exit (N,y) ); consider F being Subset-Family of (Elements N) such that A5: for x being Subset of (Elements N) holds ( x in F iff S1[x] ) from SUBSET_1:sch_3(); take F ; ::_thesis: for x being set holds ( x in F iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = exit (N,y) ) ) ) thus for x being set holds ( x in F iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = exit (N,y) ) ) ) by A5; ::_thesis: verum end; uniqueness for b1, b2 being set st ( for x being set holds ( x in b1 iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = exit (N,y) ) ) ) ) & ( for x being set holds ( x in b2 iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = exit (N,y) ) ) ) ) holds b1 = b2 proof let W, Y be set ; ::_thesis: ( ( for x being set holds ( x in W iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = exit (N,y) ) ) ) ) & ( for x being set holds ( x in Y iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = exit (N,y) ) ) ) ) implies W = Y ) assume that A6: for x being set holds ( x in W iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = exit (N,y) ) ) ) and A7: for x being set holds ( x in Y iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = exit (N,y) ) ) ) ; ::_thesis: W = Y A8: for x being set st x in Y holds x in W proof let x be set ; ::_thesis: ( x in Y implies x in W ) assume x in Y ; ::_thesis: x in W then ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = exit (N,y) ) ) by A7; hence x in W by A6; ::_thesis: verum end; for x being set st x in W holds x in Y proof let x be set ; ::_thesis: ( x in W implies x in Y ) assume x in W ; ::_thesis: x in Y then ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = exit (N,y) ) ) by A6; hence x in Y by A7; ::_thesis: verum end; hence W = Y by A8, TARSKI:1; ::_thesis: verum end; end; :: deftheorem Def13 defines Entr NET_1:def_13_:_ for N being Pnet for X being set for b3 being set holds ( b3 = Entr (N,X) iff for x being set holds ( x in b3 iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = enter (N,y) ) ) ) ); :: deftheorem Def14 defines Ext NET_1:def_14_:_ for N being Pnet for X being set for b3 being set holds ( b3 = Ext (N,X) iff for x being set holds ( x in b3 iff ( x c= Elements N & ex y being Element of Elements N st ( y in X & x = exit (N,y) ) ) ) ); theorem Th21: :: NET_1:21 for N being Pnet for x being Element of Elements N for X being set st Elements N <> {} & x in X holds enter (N,x) in Entr (N,X) proof let N be Pnet; ::_thesis: for x being Element of Elements N for X being set st Elements N <> {} & x in X holds enter (N,x) in Entr (N,X) let x be Element of Elements N; ::_thesis: for X being set st Elements N <> {} & x in X holds enter (N,x) in Entr (N,X) let X be set ; ::_thesis: ( Elements N <> {} & x in X implies enter (N,x) in Entr (N,X) ) assume that A1: Elements N <> {} and A2: x in X ; ::_thesis: enter (N,x) in Entr (N,X) enter (N,x) c= Elements N by A1, Th16; hence enter (N,x) in Entr (N,X) by A2, Def13; ::_thesis: verum end; theorem Th22: :: NET_1:22 for N being Pnet for x being Element of Elements N for X being set st Elements N <> {} & x in X holds exit (N,x) in Ext (N,X) proof let N be Pnet; ::_thesis: for x being Element of Elements N for X being set st Elements N <> {} & x in X holds exit (N,x) in Ext (N,X) let x be Element of Elements N; ::_thesis: for X being set st Elements N <> {} & x in X holds exit (N,x) in Ext (N,X) let X be set ; ::_thesis: ( Elements N <> {} & x in X implies exit (N,x) in Ext (N,X) ) assume that A1: Elements N <> {} and A2: x in X ; ::_thesis: exit (N,x) in Ext (N,X) exit (N,x) c= Elements N by A1, Th19; hence exit (N,x) in Ext (N,X) by A2, Def14; ::_thesis: verum end; definition let N be Pnet; let X be set ; func Input (N,X) -> set equals :: NET_1:def 15 union (Entr (N,X)); correctness coherence union (Entr (N,X)) is set ; ; func Output (N,X) -> set equals :: NET_1:def 16 union (Ext (N,X)); correctness coherence union (Ext (N,X)) is set ; ; end; :: deftheorem defines Input NET_1:def_15_:_ for N being Pnet for X being set holds Input (N,X) = union (Entr (N,X)); :: deftheorem defines Output NET_1:def_16_:_ for N being Pnet for X being set holds Output (N,X) = union (Ext (N,X)); theorem :: NET_1:23 for N being Pnet for x, X being set st X c= Elements N holds ( x in Input (N,X) iff ex y being Element of Elements N st ( y in X & x in enter (N,y) ) ) proof let N be Pnet; ::_thesis: for x, X being set st X c= Elements N holds ( x in Input (N,X) iff ex y being Element of Elements N st ( y in X & x in enter (N,y) ) ) let x, X be set ; ::_thesis: ( X c= Elements N implies ( x in Input (N,X) iff ex y being Element of Elements N st ( y in X & x in enter (N,y) ) ) ) A1: ( x in Input (N,X) implies ex y being Element of Elements N st ( y in X & x in enter (N,y) ) ) proof assume x in Input (N,X) ; ::_thesis: ex y being Element of Elements N st ( y in X & x in enter (N,y) ) then consider y being set such that A2: x in y and A3: y in Entr (N,X) by TARSKI:def_4; ex z being Element of Elements N st ( z in X & y = enter (N,z) ) by A3, Def13; hence ex y being Element of Elements N st ( y in X & x in enter (N,y) ) by A2; ::_thesis: verum end; assume A4: X c= Elements N ; ::_thesis: ( x in Input (N,X) iff ex y being Element of Elements N st ( y in X & x in enter (N,y) ) ) ( ex y being Element of Elements N st ( y in X & x in enter (N,y) ) implies x in Input (N,X) ) proof given y being Element of Elements N such that A5: y in X and A6: x in enter (N,y) ; ::_thesis: x in Input (N,X) enter (N,y) in Entr (N,X) by A4, A5, Th21; hence x in Input (N,X) by A6, TARSKI:def_4; ::_thesis: verum end; hence ( x in Input (N,X) iff ex y being Element of Elements N st ( y in X & x in enter (N,y) ) ) by A1; ::_thesis: verum end; theorem :: NET_1:24 for N being Pnet for x, X being set st X c= Elements N holds ( x in Output (N,X) iff ex y being Element of Elements N st ( y in X & x in exit (N,y) ) ) proof let N be Pnet; ::_thesis: for x, X being set st X c= Elements N holds ( x in Output (N,X) iff ex y being Element of Elements N st ( y in X & x in exit (N,y) ) ) let x, X be set ; ::_thesis: ( X c= Elements N implies ( x in Output (N,X) iff ex y being Element of Elements N st ( y in X & x in exit (N,y) ) ) ) A1: ( x in Output (N,X) implies ex y being Element of Elements N st ( y in X & x in exit (N,y) ) ) proof assume x in Output (N,X) ; ::_thesis: ex y being Element of Elements N st ( y in X & x in exit (N,y) ) then consider y being set such that A2: x in y and A3: y in Ext (N,X) by TARSKI:def_4; ex z being Element of Elements N st ( z in X & y = exit (N,z) ) by A3, Def14; hence ex y being Element of Elements N st ( y in X & x in exit (N,y) ) by A2; ::_thesis: verum end; assume A4: X c= Elements N ; ::_thesis: ( x in Output (N,X) iff ex y being Element of Elements N st ( y in X & x in exit (N,y) ) ) ( ex y being Element of Elements N st ( y in X & x in exit (N,y) ) implies x in Output (N,X) ) proof given y being Element of Elements N such that A5: y in X and A6: x in exit (N,y) ; ::_thesis: x in Output (N,X) exit (N,y) in Ext (N,X) by A4, A5, Th22; hence x in Output (N,X) by A6, TARSKI:def_4; ::_thesis: verum end; hence ( x in Output (N,X) iff ex y being Element of Elements N st ( y in X & x in exit (N,y) ) ) by A1; ::_thesis: verum end; theorem :: NET_1:25 for N being Pnet for X being Subset of (Elements N) for x being Element of Elements N st Elements N <> {} holds ( x in Input (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & pre N,y,x ) ) ) proof let N be Pnet; ::_thesis: for X being Subset of (Elements N) for x being Element of Elements N st Elements N <> {} holds ( x in Input (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & pre N,y,x ) ) ) let X be Subset of (Elements N); ::_thesis: for x being Element of Elements N st Elements N <> {} holds ( x in Input (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & pre N,y,x ) ) ) let x be Element of Elements N; ::_thesis: ( Elements N <> {} implies ( x in Input (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & pre N,y,x ) ) ) ) A1: ( ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & pre N,y,x ) ) implies x in Input (N,X) ) proof A2: ( ex y being Element of Elements N st ( y in X & y in the carrier' of N & pre N,y,x ) implies x in Input (N,X) ) proof given y being Element of Elements N such that A3: y in X and A4: y in the carrier' of N and A5: pre N,y,x ; ::_thesis: x in Input (N,X) [x,y] in Flow N by A5, Def4; then x in Pre (N,y) by A4, Def6; then A6: x in enter (N,y) by A4, Def8; enter (N,y) in Entr (N,X) by A3, Th21; hence x in Input (N,X) by A6, TARSKI:def_4; ::_thesis: verum end; A7: ( x in X & x in the carrier of N implies x in Input (N,X) ) proof assume that A8: x in X and A9: x in the carrier of N ; ::_thesis: x in Input (N,X) ( enter (N,x) = {x} & {x} c= Elements N ) by A9, Def8, ZFMISC_1:31; then A10: {x} in Entr (N,X) by A8, Def13; x in {x} by TARSKI:def_1; hence x in Input (N,X) by A10, TARSKI:def_4; ::_thesis: verum end; assume ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & pre N,y,x ) ) ; ::_thesis: x in Input (N,X) hence x in Input (N,X) by A7, A2; ::_thesis: verum end; assume A11: Elements N <> {} ; ::_thesis: ( x in Input (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & pre N,y,x ) ) ) ( not x in Input (N,X) or ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & pre N,y,x ) ) proof assume x in Input (N,X) ; ::_thesis: ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & pre N,y,x ) ) then ex y being set st ( x in y & y in Entr (N,X) ) by TARSKI:def_4; then consider y being set such that A12: y in Entr (N,X) and A13: x in y ; consider z being Element of Elements N such that A14: z in X and A15: y = enter (N,z) by A12, Def13; A16: ( z in the carrier' of N implies y = Pre (N,z) ) by A15, Def8; A17: ( z in the carrier' of N implies ex y being Element of Elements N st ( y in X & y in the carrier' of N & pre N,y,x ) ) proof assume A18: z in the carrier' of N ; ::_thesis: ex y being Element of Elements N st ( y in X & y in the carrier' of N & pre N,y,x ) take z ; ::_thesis: ( z in X & z in the carrier' of N & pre N,z,x ) [x,z] in Flow N by A13, A16, A18, Def6; hence ( z in X & z in the carrier' of N & pre N,z,x ) by A14, A18, Def4; ::_thesis: verum end; A19: ( z in the carrier of N or z in the carrier' of N ) by A11, XBOOLE_0:def_3; ( z in the carrier of N implies y = {z} ) by A15, Def8; hence ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & pre N,y,x ) ) by A13, A14, A19, A17, TARSKI:def_1; ::_thesis: verum end; hence ( x in Input (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & pre N,y,x ) ) ) by A1; ::_thesis: verum end; theorem :: NET_1:26 for N being Pnet for X being Subset of (Elements N) for x being Element of Elements N st Elements N <> {} holds ( x in Output (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & post N,y,x ) ) ) proof let N be Pnet; ::_thesis: for X being Subset of (Elements N) for x being Element of Elements N st Elements N <> {} holds ( x in Output (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & post N,y,x ) ) ) let X be Subset of (Elements N); ::_thesis: for x being Element of Elements N st Elements N <> {} holds ( x in Output (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & post N,y,x ) ) ) let x be Element of Elements N; ::_thesis: ( Elements N <> {} implies ( x in Output (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & post N,y,x ) ) ) ) A1: ( ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & post N,y,x ) ) implies x in Output (N,X) ) proof A2: ( ex y being Element of Elements N st ( y in X & y in the carrier' of N & post N,y,x ) implies x in Output (N,X) ) proof given y being Element of Elements N such that A3: y in X and A4: y in the carrier' of N and A5: post N,y,x ; ::_thesis: x in Output (N,X) [y,x] in Flow N by A5, Def5; then x in Post (N,y) by A4, Def7; then A6: x in exit (N,y) by A4, Def9; exit (N,y) in Ext (N,X) by A3, Th22; hence x in Output (N,X) by A6, TARSKI:def_4; ::_thesis: verum end; A7: ( x in X & x in the carrier of N implies x in Output (N,X) ) proof assume that A8: x in X and A9: x in the carrier of N ; ::_thesis: x in Output (N,X) ( exit (N,x) = {x} & {x} c= Elements N ) by A9, Def9, ZFMISC_1:31; then A10: {x} in Ext (N,X) by A8, Def14; x in {x} by TARSKI:def_1; hence x in Output (N,X) by A10, TARSKI:def_4; ::_thesis: verum end; assume ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & post N,y,x ) ) ; ::_thesis: x in Output (N,X) hence x in Output (N,X) by A7, A2; ::_thesis: verum end; assume A11: Elements N <> {} ; ::_thesis: ( x in Output (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & post N,y,x ) ) ) ( not x in Output (N,X) or ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & post N,y,x ) ) proof assume x in Output (N,X) ; ::_thesis: ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & post N,y,x ) ) then ex y being set st ( x in y & y in Ext (N,X) ) by TARSKI:def_4; then consider y being set such that A12: y in Ext (N,X) and A13: x in y ; consider z being Element of Elements N such that A14: z in X and A15: y = exit (N,z) by A12, Def14; A16: ( z in the carrier' of N implies y = Post (N,z) ) by A15, Def9; A17: ( z in the carrier' of N implies ex y being Element of Elements N st ( y in X & y in the carrier' of N & post N,y,x ) ) proof assume A18: z in the carrier' of N ; ::_thesis: ex y being Element of Elements N st ( y in X & y in the carrier' of N & post N,y,x ) take z ; ::_thesis: ( z in X & z in the carrier' of N & post N,z,x ) [z,x] in Flow N by A13, A16, A18, Def7; hence ( z in X & z in the carrier' of N & post N,z,x ) by A14, A18, Def5; ::_thesis: verum end; A19: ( z in the carrier of N or z in the carrier' of N ) by A11, XBOOLE_0:def_3; ( z in the carrier of N implies y = {z} ) by A15, Def9; hence ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & post N,y,x ) ) by A13, A14, A19, A17, TARSKI:def_1; ::_thesis: verum end; hence ( x in Output (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st ( y in X & y in the carrier' of N & post N,y,x ) ) ) by A1; ::_thesis: verum end;