Copyright (c) 1992 Association of Mizar Users
environ vocabulary RELAT_1, NET_1, MCART_1, ARYTM_3, BOOLE, PETRI; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, RELSET_1, MCART_1, DOMAIN_1; constructors RELSET_1, DOMAIN_1, MEMBERED, XBOOLE_0; clusters RELSET_1, PRELAMB, SUBSET_1, MEMBERED, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; definitions TARSKI, XBOOLE_0; theorems RELSET_1, SUBSET_1, MCART_1, TARSKI, ZFMISC_1, RELAT_1, XBOOLE_0; schemes DOMAIN_1; begin :: Redefinition of Element for Non-empty Relation definition let A, B be non empty set; let r be non empty Relation of A, B; redefine mode Element of r -> Element of [:A,B:]; coherence proof let a be Element of r; thus a is Element of [:A,B:]; end; end; :: Place/Transition Net Structure definition struct PT_net_Str (# Places, Transitions -> non empty set, S-T_Arcs -> non empty Relation of the Places, the Transitions, T-S_Arcs -> non empty Relation of the Transitions, the Places #); end; reserve PTN for PT_net_Str; :: Place, Transition, and Arc (s->t, t->s) Elements definition let PTN; mode place of PTN is Element of the Places of PTN; mode places of PTN is Element of the Places of PTN; mode transition of PTN is Element of the Transitions of PTN; mode transitions of PTN is Element of the Transitions of PTN; mode S-T_arc of PTN is Element of the S-T_Arcs of PTN; mode T-S_arc of PTN is Element of the T-S_Arcs of PTN; end; :: Redefinition of Relation for s->t Arcs definition let PTN; let x be S-T_arc of PTN; redefine func x`1 -> place of PTN; coherence proof thus x`1 is place of PTN; end; func x`2 -> transition of PTN; coherence proof thus x`2 is transition of PTN; end; end; :: Redefinition of Relation for t->s Arcs definition let PTN; let x be T-S_arc of PTN; redefine func x`1 -> transition of PTN; coherence proof thus x`1 is transition of PTN; end; func x`2 -> place of PTN; coherence proof thus x`2 is place of PTN; end; end; :: *S, S* Definitions and Theorems reserve S0 for Subset of the Places of PTN; definition let PTN, S0; func *'S0 -> Subset of the Transitions of PTN equals :Def1: { t where t is transition of PTN : ex f being T-S_arc of PTN, s being place of PTN st s in S0 & f = [t,s] }; coherence proof defpred P[set] means ex f being T-S_arc of PTN, s being place of PTN st s in S0 & f = [$1,s]; { t where t is transition of PTN : P[t] } is Subset of the Transitions of PTN from SubsetD; hence thesis; end; correctness; func S0*' -> Subset of the Transitions of PTN equals :Def2: { t where t is transition of PTN : ex f being S-T_arc of PTN, s being place of PTN st s in S0 & f = [s,t] }; coherence proof defpred P[set] means ex f being S-T_arc of PTN, s being place of PTN st s in S0 & f = [s,$1]; { t where t is transition of PTN : P[t] } is Subset of the Transitions of PTN from SubsetD; hence thesis; end; correctness; end; theorem *'S0 = {f`1 where f is T-S_arc of PTN : f`2 in S0} proof A1: *'S0 = { t where t is transition of PTN : ex f being T-S_arc of PTN, s being place of PTN st s in S0 & f = [t,s] } by Def1; thus *'S0 c= {f`1 where f is T-S_arc of PTN : f`2 in S0} proof let x be set; assume x in *'S0; then consider t being transition of PTN such that A2: x = t and A3: ex f being T-S_arc of PTN, s being place of PTN st s in S0 & f = [t,s] by A1; consider f being T-S_arc of PTN, s being place of PTN such that A4: s in S0 and A5: f = [t,s] by A3; f`1 = t & f`2 = s by A5,MCART_1:7; hence x in {f0`1 where f0 is T-S_arc of PTN : f0`2 in S0} by A2,A4; end; let x be set; assume x in {f`1 where f is T-S_arc of PTN : f`2 in S0}; then consider f being T-S_arc of PTN such that A6: x = f`1 and A7: f`2 in S0; f = [f`1,f`2] by MCART_1:23; hence x in *'S0 by A1,A6,A7; end; theorem Th2: for x being set holds x in *'S0 iff ex f being T-S_arc of PTN, s being place of PTN st s in S0 & f = [x,s] proof let x be set; A1: *'S0 = { t where t is transition of PTN : ex f being T-S_arc of PTN, s being place of PTN st s in S0 & f = [t,s] } by Def1; thus x in *'S0 implies ex f being T-S_arc of PTN, s being place of PTN st s in S0 & f = [x,s] proof assume x in *'S0; then consider t being transition of PTN such that A2: x = t and A3: ex f being T-S_arc of PTN, s being place of PTN st s in S0 & f = [t,s] by A1; consider f being T-S_arc of PTN, s being place of PTN such that A4: s in S0 and A5: f = [t,s] by A3; take f, s; thus thesis by A2,A4,A5; end; given f being T-S_arc of PTN, s being place of PTN such that A6: s in S0 & f = [x,s]; x = f`1 by A6,MCART_1:7; hence thesis by A1,A6; end; theorem S0*' = {f`2 where f is S-T_arc of PTN : f`1 in S0} proof A1: S0*' = { t where t is transition of PTN : ex f being S-T_arc of PTN, s being place of PTN st s in S0 & f = [s,t] } by Def2; thus S0*' c= {f`2 where f is S-T_arc of PTN : f`1 in S0} proof let x be set; assume x in S0*'; then consider t being transition of PTN such that A2: x = t and A3: ex f being S-T_arc of PTN, s being place of PTN st s in S0 & f = [s,t] by A1; consider f being S-T_arc of PTN, s being place of PTN such that A4: s in S0 and A5: f = [s,t] by A3; f`1 = s & f`2 = t by A5,MCART_1:7; hence x in {f0`2 where f0 is S-T_arc of PTN : f0`1 in S0} by A2,A4; end; let x be set; assume x in {f`2 where f is S-T_arc of PTN : f`1 in S0}; then consider f being S-T_arc of PTN such that A6: x = f`2 and A7: f`1 in S0; f = [f`1,f`2] by MCART_1:23; hence x in S0*' by A1,A6,A7; end; theorem Th4: for x being set holds x in S0*' iff ex f being S-T_arc of PTN, s being place of PTN st s in S0 & f = [s,x] proof let x be set; A1: S0*' = { t where t is transition of PTN : ex f being S-T_arc of PTN, s being place of PTN st s in S0 & f = [s,t] } by Def2; thus x in S0*' implies ex f being S-T_arc of PTN, s being place of PTN st s in S0 & f = [s,x] proof assume x in S0*'; then consider t being transition of PTN such that A2: x = t and A3: ex f being S-T_arc of PTN, s being place of PTN st s in S0 & f = [s,t] by A1; consider f being S-T_arc of PTN, s being place of PTN such that A4: s in S0 and A5: f = [s,t] by A3; take f, s; thus thesis by A2,A4,A5; end; given f being S-T_arc of PTN, s being place of PTN such that A6: s in S0 & f = [s,x]; x = f`2 by A6,MCART_1:7; hence thesis by A1,A6; end; :: *T, T* Definitions and Theorems reserve T0 for Subset of the Transitions of PTN; definition let PTN, T0; func *'T0 -> Subset of the Places of PTN equals :Def3: { s where s is place of PTN : ex f being S-T_arc of PTN, t being transition of PTN st t in T0 & f = [s,t] }; coherence proof defpred P[set] means ex f being S-T_arc of PTN, t being transition of PTN st t in T0 & f = [$1,t]; { s where s is place of PTN : P[s] } is Subset of the Places of PTN from SubsetD; hence thesis; end; correctness; func T0*' -> Subset of the Places of PTN equals :Def4: { s where s is place of PTN : ex f being T-S_arc of PTN, t being transition of PTN st t in T0 & f = [t,s] }; coherence proof defpred P[set] means ex f being T-S_arc of PTN, t being transition of PTN st t in T0 & f = [t,$1]; { s where s is place of PTN : P[s] } is Subset of the Places of PTN from SubsetD; hence thesis; end; correctness; end; theorem *'T0 = {f`1 where f is S-T_arc of PTN : f`2 in T0} proof A1: *'T0 = { s where s is place of PTN : ex f being S-T_arc of PTN, t being transition of PTN st t in T0 & f = [s,t] } by Def3; thus *'T0 c= {f`1 where f is S-T_arc of PTN : f`2 in T0} proof let x be set; assume x in *'T0; then consider s being place of PTN such that A2: x = s and A3: ex f being S-T_arc of PTN, t being transition of PTN st t in T0 & f = [s,t] by A1; consider f being S-T_arc of PTN, t being transition of PTN such that A4: t in T0 and A5: f = [s,t] by A3; f`1 = s & f`2 = t by A5,MCART_1:7; hence x in {f0`1 where f0 is S-T_arc of PTN : f0`2 in T0} by A2,A4; end; let x be set; assume x in {f`1 where f is S-T_arc of PTN : f`2 in T0}; then consider f being S-T_arc of PTN such that A6: x = f`1 and A7: f`2 in T0; f = [f`1,f`2] by MCART_1:23; hence x in *'T0 by A1,A6,A7; end; theorem Th6: for x being set holds x in *'T0 iff ex f being S-T_arc of PTN, t being transition of PTN st t in T0 & f = [x,t] proof let x be set; A1: *'T0 = { s where s is place of PTN : ex f being S-T_arc of PTN, t being transition of PTN st t in T0 & f = [s,t] } by Def3; thus x in *'T0 implies ex f being S-T_arc of PTN, t being transition of PTN st t in T0 & f = [x,t] proof assume x in *'T0; then consider s being place of PTN such that A2: x = s and A3: ex f being S-T_arc of PTN, t being transition of PTN st t in T0 & f = [s,t] by A1; consider f being S-T_arc of PTN, t being transition of PTN such that A4: t in T0 and A5: f = [s,t] by A3; take f, t; thus thesis by A2,A4,A5; end; given f being S-T_arc of PTN, t being transition of PTN such that A6: t in T0 & f = [x,t]; x = f`1 by A6,MCART_1:7; hence thesis by A1,A6; end; theorem T0*' = {f`2 where f is T-S_arc of PTN : f`1 in T0} proof A1: T0*' = { s where s is place of PTN : ex f being T-S_arc of PTN, t being transition of PTN st t in T0 & f = [t,s] } by Def4; thus T0*' c= {f`2 where f is T-S_arc of PTN : f`1 in T0} proof let x be set; assume x in T0*'; then consider s being place of PTN such that A2: x = s and A3: ex f being T-S_arc of PTN, t being transition of PTN st t in T0 & f = [t,s] by A1; consider f being T-S_arc of PTN, t being transition of PTN such that A4: t in T0 and A5: f = [t,s] by A3; f`1 = t & f`2 = s by A5,MCART_1:7; hence x in {f0`2 where f0 is T-S_arc of PTN : f0`1 in T0} by A2,A4; end; let x be set; assume x in {f`2 where f is T-S_arc of PTN : f`1 in T0}; then consider f being T-S_arc of PTN such that A6: x = f`2 and A7: f`1 in T0; f = [f`1,f`2] by MCART_1:23; hence x in T0*' by A1,A6,A7; end; theorem Th8: for x being set holds x in T0*' iff ex f being T-S_arc of PTN, t being transition of PTN st t in T0 & f = [t,x] proof let x be set; A1: T0*' = { s where s is place of PTN : ex f being T-S_arc of PTN, t being transition of PTN st t in T0 & f = [t,s] } by Def4; thus x in T0*' implies ex f being T-S_arc of PTN, t being transition of PTN st t in T0 & f = [t,x] proof assume x in T0*'; then consider s being place of PTN such that A2: x = s and A3: ex f being T-S_arc of PTN, t being transition of PTN st t in T0 & f = [t,s] by A1; consider f being T-S_arc of PTN, t being transition of PTN such that A4: t in T0 and A5: f = [t,s] by A3; take f, t; thus thesis by A2,A4,A5; end; given f being T-S_arc of PTN, t being transition of PTN such that A6: t in T0 & f = [t,x]; x = f`2 by A6,MCART_1:7; hence thesis by A1,A6; end; theorem *'{}the Places of PTN = {} proof consider x being Element of *'{}the Places of PTN; assume not thesis; then x in *'{}the Places of PTN; then x in { t where t is transition of PTN : ex f being T-S_arc of PTN , s being place of PTN st s in {}the Places of PTN & f = [t,s] } by Def1; then consider t being transition of PTN such that x = t and A1: ex f being T-S_arc of PTN, s being place of PTN st s in {}the Places of PTN & f = [t,s]; consider f being T-S_arc of PTN, s being place of PTN such that A2: s in {}the Places of PTN & f = [t,s] by A1; thus contradiction by A2; end; theorem ({}the Places of PTN)*' = {} proof consider x being Element of ({}the Places of PTN)*'; assume not thesis; then x in ({}the Places of PTN)*'; then x in { t where t is transition of PTN : ex f being S-T_arc of PTN , s being place of PTN st s in {}the Places of PTN & f = [s,t] } by Def2; then consider t being transition of PTN such that x = t and A1: ex f being S-T_arc of PTN, s being place of PTN st s in {}the Places of PTN & f = [s,t]; consider f being S-T_arc of PTN, s being place of PTN such that A2: s in {}the Places of PTN & f = [s,t] by A1; thus contradiction by A2; end; theorem *'{}the Transitions of PTN = {} proof consider x being Element of *'{}the Transitions of PTN; assume not thesis; then x in *'{}the Transitions of PTN; then x in { s where s is place of PTN : ex f being S-T_arc of PTN, t being transition of PTN st t in {}the Transitions of PTN & f = [s,t] } by Def3; then consider s being place of PTN such that x = s and A1: ex f being S-T_arc of PTN, t being transition of PTN st t in {}the Transitions of PTN & f = [s,t]; consider f being S-T_arc of PTN, t being transition of PTN such that A2: t in {}the Transitions of PTN & f = [s,t] by A1; thus contradiction by A2; end; theorem ({}the Transitions of PTN)*' = {} proof consider x being Element of ({}the Transitions of PTN)*'; assume not thesis; then x in ({}the Transitions of PTN)*'; then x in { s where s is place of PTN : ex f being T-S_arc of PTN, t being transition of PTN st t in {}the Transitions of PTN & f = [t,s] } by Def4; then consider s being place of PTN such that x = s and A1: ex f being T-S_arc of PTN, t being transition of PTN st t in {}the Transitions of PTN & f = [t,s]; consider f being T-S_arc of PTN, t being transition of PTN such that A2: t in {}the Transitions of PTN & f = [t,s] by A1; thus contradiction by A2; end; begin :: Deadlock-like Attribute for Place Sets definition let PTN; let IT be Subset of the Places of PTN; attr IT is Deadlock-like means *'IT is Subset of IT*'; end; :: With_Deadlocks Mode for Place\Transition Nets definition let IT be PT_net_Str; attr IT is With_Deadlocks means ex S being Subset of the Places of IT st S is Deadlock-like; end; definition cluster With_Deadlocks PT_net_Str; existence proof 0 in {0} by TARSKI:def 1; then reconsider f = {[0,0]} as non empty Relation of {0}, {0} by RELSET_1:8; take PTN1 = PT_net_Str (# {0}, {0}, f, f #); {0} c= the Places of PTN1; then reconsider S = {0} as Subset of the Places of PTN1; take S; A1: *'S = { t where t is transition of PTN1 : ex f being T-S_arc of PTN1, s being place of PTN1 st s in S & f = [t,s] } by Def1; A2: S*' = { t where t is transition of PTN1 : ex f being S-T_arc of PTN1, s being place of PTN1 st s in S & f = [s,t] } by Def2; reconsider s = 0 as place of PTN1 by TARSKI:def 1; reconsider t = 0 as transition of PTN1 by TARSKI:def 1; reconsider st_f = [0,0] as S-T_arc of PTN1 by TARSKI:def 1; reconsider ts_f = [0,0] as T-S_arc of PTN1 by TARSKI:def 1; ts_f = [t,s] & s in S; then t in *'S by A1; then {t} c= *'S by ZFMISC_1:37; then A3: {t} = *'S by XBOOLE_0:def 10; st_f = [s,t] & s in S; then t in S*' by A2; hence *'S is Subset of S*' by A3,ZFMISC_1:37; end; end; begin :: Trap-like Attribute for Place Sets definition let PTN; let IT be Subset of the Places of PTN; attr IT is Trap-like means IT*' is Subset of *'IT; end; :: With_Traps Mode for Place\Transition Nets definition let IT be PT_net_Str; attr IT is With_Traps means ex S being Subset of the Places of IT st S is Trap-like; end; definition cluster With_Traps PT_net_Str; existence proof 0 in {0} by TARSKI:def 1; then reconsider f = {[0,0]} as non empty Relation of {0}, {0} by RELSET_1:8; take PTN1 = PT_net_Str (# {0}, {0}, f, f #); {0} c= the Places of PTN1; then reconsider S = {0} as Subset of the Places of PTN1; take S; A1: *'S = { t where t is transition of PTN1 : ex f being T-S_arc of PTN1, s being place of PTN1 st s in S & f = [t,s] } by Def1; A2: S*' = { t where t is transition of PTN1 : ex f being S-T_arc of PTN1, s being place of PTN1 st s in S & f = [s,t] } by Def2; reconsider s = 0 as place of PTN1 by TARSKI:def 1; reconsider t = 0 as transition of PTN1 by TARSKI:def 1; reconsider st_f = [0,0] as S-T_arc of PTN1 by TARSKI:def 1; reconsider ts_f = [0,0] as T-S_arc of PTN1 by TARSKI:def 1; st_f = [s,t] & s in S; then t in S*' by A2; then {t} c= S*' by ZFMISC_1:37; then A3: {t} = S*' by XBOOLE_0:def 10; ts_f = [t,s] & s in S; then t in *'S by A1; hence S*' is Subset of *'S by A3,ZFMISC_1:37; end; end; definition let A, B be non empty set; let r be non empty Relation of A, B; redefine func r~ -> non empty Relation of B, A; coherence proof consider x being Element of r; consider y, z being set such that A1: x = [y,z] by RELAT_1:def 1; [z,y] in r~ by A1,RELAT_1:def 7; hence thesis; end; end; begin :: Duality Definitions and Theorems for Place/Transition Nets definition let PTN; func PTN.: -> strict PT_net_Str equals :Def9: PT_net_Str (# the Places of PTN, the Transitions of PTN, (the T-S_Arcs of PTN)~, (the S-T_Arcs of PTN)~ #); correctness; end; theorem Th13: PTN.:.: = the PT_net_Str of PTN proof A1: (the S-T_Arcs of PTN)~~ = the S-T_Arcs of PTN & (the T-S_Arcs of PTN)~~ = the T-S_Arcs of PTN; thus PTN.:.: = PT_net_Str (# the Places of PTN, the Transitions of PTN, (the T-S_Arcs of PTN)~, (the S-T_Arcs of PTN)~ #).: by Def9 .= the PT_net_Str of PTN by A1,Def9; end; theorem Th14: the Places of PTN = the Places of PTN.: & the Transitions of PTN = the Transitions of PTN.: & (the S-T_Arcs of PTN)~ = the T-S_Arcs of PTN.: & (the T-S_Arcs of PTN)~ = the S-T_Arcs of PTN.: proof PTN.: = PT_net_Str (# the Places of PTN, the Transitions of PTN, (the T-S_Arcs of PTN)~, (the S-T_Arcs of PTN)~ #) by Def9; hence thesis; end; definition let PTN; let S0 be Subset of the Places of PTN; func S0.: -> Subset of the Places of PTN.: equals :Def10: S0; coherence by Th14; end; definition let PTN; let s be place of PTN; func s.: -> place of PTN.: equals :Def11: s; coherence by Th14; end; definition let PTN; let S0 be Subset of the Places of PTN.:; func .:S0 -> Subset of the Places of PTN equals S0; coherence by Th14; end; definition let PTN; let s be place of PTN.:; func .:s -> place of PTN equals :Def13: s; coherence by Th14; end; definition let PTN; let T0 be Subset of the Transitions of PTN; func T0.: -> Subset of the Transitions of PTN.: equals T0; coherence by Th14; end; definition let PTN; let t be transition of PTN; func t.: -> transition of PTN.: equals t; coherence by Th14; end; definition let PTN; let T0 be Subset of the Transitions of PTN.:; func .:T0 -> Subset of the Transitions of PTN equals T0; coherence by Th14; end; definition let PTN; let t be transition of PTN.:; func .:t -> transition of PTN equals t; coherence by Th14; end; reserve S for Subset of the Places of PTN; theorem Th15: S.:*' = *'S proof thus S.:*' c= *'S proof let x be set; A1: the T-S_Arcs of the PT_net_Str of PTN = the T-S_Arcs of PTN; assume x in S.:*'; then consider f being S-T_arc of PTN.:, s being place of PTN.: such that A2: s in S.: & f = [s,x] by Th4; A3: .:s = s & S.: = S by Def10,Def13; (the S-T_Arcs of PTN.:)~ = the T-S_Arcs of PTN.:.: by Th14; then (the S-T_Arcs of PTN.:)~ = the T-S_Arcs of PTN by A1,Th13; then [x,.:s] is T-S_arc of PTN by A2,A3,RELAT_1:def 7; hence x in *'S by A2,A3,Th2; end; let x be set; assume x in *'S; then consider f being T-S_arc of PTN, s being place of PTN such that A4: s in S & f = [x,s] by Th2; A5: s.: = s & S.: = S by Def10,Def11; (the T-S_Arcs of PTN)~ = the S-T_Arcs of PTN.: by Th14; then [s.:,x] is S-T_arc of PTN.: by A4,A5,RELAT_1:def 7; hence x in S.:*' by A4,A5,Th4; end; theorem Th16: *'(S.:) = S*' proof thus *'(S.:) c= S*' proof let x be set; A1: the T-S_Arcs of the PT_net_Str of PTN = the T-S_Arcs of PTN; assume x in *'(S.:); then consider f being T-S_arc of PTN.:, s being place of PTN.: such that A2: s in S.: & f = [x,s] by Th2; A3: .:s = s & S.: = S by Def10,Def13; (the T-S_Arcs of PTN.:)~ = the S-T_Arcs of PTN.:.: by Th14; then (the T-S_Arcs of PTN.:)~ = the S-T_Arcs of PTN by A1,Th13; then [.:s,x] is S-T_arc of PTN by A2,A3,RELAT_1:def 7; hence x in S*' by A2,A3,Th4; end; let x be set; assume x in S*'; then consider f being S-T_arc of PTN, s being place of PTN such that A4: s in S & f = [s,x] by Th4; A5: s.: = s & S.: = S by Def10,Def11; (the S-T_Arcs of PTN)~ = the T-S_Arcs of PTN.: by Th14; then [x,s.:] is T-S_arc of PTN.: by A4,A5,RELAT_1:def 7; hence x in *'(S.:) by A4,A5,Th2; end; theorem S is Deadlock-like iff S.: is Trap-like proof A1: S.:*' = *'S & *'(S.:) = S*' by Th15,Th16; thus S is Deadlock-like implies S.: is Trap-like proof assume *'S is Subset of S*'; hence S.:*' is Subset of *'(S.:) by A1; end; assume S.:*' is Subset of *'(S.:); hence *'S is Subset of S*' by A1; end; theorem S is Trap-like iff S.: is Deadlock-like proof A1: S.:*' = *'S & *'(S.:) = S*' by Th15,Th16; thus S is Trap-like implies S.: is Deadlock-like proof assume S*' is Subset of *'S; hence *'(S.:) is Subset of S.:*' by A1; end; assume *'(S.:) is Subset of S.:*'; hence S*' is Subset of *'S by A1; end; theorem for PTN being PT_net_Str, t being transition of PTN, S0 being Subset of the Places of PTN holds t in S0*' iff *'{t} meets S0 proof let PTN be PT_net_Str; let t be transition of PTN; let S0 be Subset of the Places of PTN; thus t in S0*' implies *'{t} meets S0 proof assume t in S0*'; then consider f being S-T_arc of PTN, s being place of PTN such that A1: s in S0 & f = [s,t] by Th4; t in {t} by TARSKI:def 1; then s in *'{t} by A1,Th6; hence *'{t} /\ S0 <> {} by A1,XBOOLE_0:def 3; end; assume *'{t} /\ S0 <> {}; then consider s being place of PTN such that A2: s in *'{t} /\ S0 by SUBSET_1:10; A3: s in *'{t} & s in S0 by A2,XBOOLE_0:def 3; then consider f being S-T_arc of PTN, t0 being transition of PTN such that A4: t0 in {t} and A5: f = [s,t0] by Th6; t0 = t by A4,TARSKI:def 1; hence t in S0*' by A3,A5,Th4; end; theorem for PTN being PT_net_Str, t being transition of PTN, S0 being Subset of the Places of PTN holds t in *'S0 iff {t}*' meets S0 proof let PTN be PT_net_Str; let t be transition of PTN; let S0 be Subset of the Places of PTN; thus t in *'S0 implies {t}*' meets S0 proof assume t in *'S0; then consider f being T-S_arc of PTN, s being place of PTN such that A1: s in S0 & f = [t,s] by Th2; t in {t} by TARSKI:def 1; then s in {t}*' by A1,Th8; hence {t}*' /\ S0 <> {} by A1,XBOOLE_0:def 3; end; assume {t}*' /\ S0 <> {}; then consider s being place of PTN such that A2: s in {t}*' /\ S0 by SUBSET_1:10; A3: s in {t}*' & s in S0 by A2,XBOOLE_0:def 3; then consider f being T-S_arc of PTN, t0 being transition of PTN such that A4: t0 in {t} and A5: f = [t0,s] by Th8; t0 = t by A4,TARSKI:def 1; hence t in *'S0 by A3,A5,Th2; end;