:: Basic Petri Net Concepts.
:: Place/Transition Net Structure, Deadlocks, Traps, Dual Nets
::  by Pauline N. Kawamoto, Yasushi Fuwa and Yatsuka Nakamura
::
:: Received November 27, 1992
:: Copyright (c) 1992-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, RELAT_1, SUBSET_1, ZFMISC_1, MCART_1, ARYTM_3, TARSKI,
      PETRI, STRUCT_0, PNPROC_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1,
      XTUPLE_0, SUBSET_1, RELAT_1, RELSET_1, MCART_1,
      DOMAIN_1, PARTIT_2, STRUCT_0;
 constructors RELSET_1, DOMAIN_1, STRUCT_0, PARTIT_2, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELSET_1, STRUCT_0, PARTIT_2, RELAT_1,
      XTUPLE_0;
 requirements SUBSET, BOOLE;
 definitions TARSKI, XBOOLE_0, STRUCT_0, PARTIT_2, XTUPLE_0;
 theorems 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 thesis;
  end;
end;

:: Place/Transition Net Structure

definition
  struct(2-sorted) PT_net_Str (# carrier, carrier' -> set,
       S-T_Arcs -> Relation of the carrier, the carrier',
       T-S_Arcs -> Relation of the carrier', the carrier #);
end;

definition let N be PT_net_Str;
 attr N is with_S-T_arc means
:Def1: the S-T_Arcs of N is non empty;
 attr N is with_T-S_arc means
:Def2: the T-S_Arcs of N is non empty;
end;

definition
 func TrivialPetriNet -> PT_net_Str equals
  PT_net_Str (# {{}}, {{}}, [#]({{}},{{}}), [#]({{}},{{}}) #);
 coherence;
end;

registration
 cluster TrivialPetriNet ->
  with_S-T_arc with_T-S_arc strict non empty non void;
 coherence
  proof set N = TrivialPetriNet;
   thus the S-T_Arcs of N is non empty;
   thus the T-S_Arcs of N is non empty;
   thus thesis;
  end;
end;

registration
 cluster non empty non void with_S-T_arc with_T-S_arc strict for PT_net_Str;
 existence
  proof
   take TrivialPetriNet;
   thus thesis;
  end;
end;

registration let N be with_S-T_arc PT_net_Str;
 cluster the S-T_Arcs of N -> non empty;
 coherence by Def1;
end;

registration let N be with_T-S_arc PT_net_Str;
 cluster the T-S_Arcs of N -> non empty;
 coherence by Def2;
end;

definition
 mode Petri_net
  is non empty non void with_S-T_arc with_T-S_arc PT_net_Str;
end;

reserve PTN for Petri_net;

:: Place, Transition, and Arc (s->t, t->s) Elements

definition
  let PTN;
  mode place of PTN is Element of the carrier of PTN;
  mode places of PTN is Element of the carrier of PTN;
  mode transition of PTN is Element of the carrier' of PTN;
  mode transitions of PTN is Element of the carrier' 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;
  redefine 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;
  redefine 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 carrier of PTN;

definition
  let PTN, S0;
  func *'S0 -> Subset of the carrier' of PTN equals
  { 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 carrier'
    of PTN from DOMAIN_1:sch 7;
    hence thesis;
  end;
  correctness;
  func S0*' -> Subset of the carrier' of PTN equals
  { 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 carrier'
    of PTN from DOMAIN_1:sch 7;
    hence thesis;
  end;
  correctness;
end;

theorem
  *'S0 = {f`1 where f is T-S_arc of PTN : f`2 in S0}
proof
  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
A1: x = t and
A2: ex f being T-S_arc of PTN, s being place of PTN st s in S0 & f = [ t,s];
    consider f being T-S_arc of PTN, s being place of PTN such that
A3: s in S0 and
A4: f = [t,s] by A2;
    f`1 = t & f`2 = s by A4,MCART_1:7;
    hence thesis by A1,A3;
  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
A5: x = f`1 & f`2 in S0;
  f = [f`1,f`2] by MCART_1:21;
  hence thesis by A5;
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;
  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
A1: x = t and
A2: ex f being T-S_arc of PTN, s being place of PTN st s in S0 & f = [ t,s];
    consider f being T-S_arc of PTN, s being place of PTN such that
A3: s in S0 & f = [t,s] by A2;
    take f, s;
    thus thesis by A1,A3;
  end;
  given f being T-S_arc of PTN, s being place of PTN such that
A4: s in S0 and
A5: f = [x,s];
  x = f`1 by A5,MCART_1:7;
  hence thesis by A4,A5;
end;

theorem
  S0*' = {f`2 where f is S-T_arc of PTN : f`1 in S0}
proof
  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
A1: x = t and
A2: ex f being S-T_arc of PTN, s being place of PTN st s in S0 & f = [ s,t];
    consider f being S-T_arc of PTN, s being place of PTN such that
A3: s in S0 and
A4: f = [s,t] by A2;
    f`1 = s & f`2 = t by A4,MCART_1:7;
    hence thesis by A1,A3;
  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
A5: x = f`2 & f`1 in S0;
  f = [f`1,f`2] by MCART_1:21;
  hence thesis by A5;
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;
  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
A1: x = t and
A2: ex f being S-T_arc of PTN, s being place of PTN st s in S0 & f = [ s,t];
    consider f being S-T_arc of PTN, s being place of PTN such that
A3: s in S0 & f = [s,t] by A2;
    take f, s;
    thus thesis by A1,A3;
  end;
  given f being S-T_arc of PTN, s being place of PTN such that
A4: s in S0 and
A5: f = [s,x];
  x = f`2 by A5,MCART_1:7;
  hence thesis by A4,A5;
end;

:: *T, T* Definitions and Theorems

reserve T0 for Subset of the carrier' of PTN;

definition
  let PTN, T0;
  func *'T0 -> Subset of the carrier of PTN equals
  { 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 carrier of PTN
    from DOMAIN_1:sch 7;
    hence thesis;
  end;
  correctness;
  func T0*' -> Subset of the carrier of PTN equals
  { 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 carrier of PTN
    from DOMAIN_1:sch 7;
    hence thesis;
  end;
  correctness;
end;

theorem
  *'T0 = {f`1 where f is S-T_arc of PTN : f`2 in T0}
proof
  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
A1: x = s and
A2: ex f being S-T_arc of PTN, t being transition of PTN st t in T0 &
    f = [s,t];
    consider f being S-T_arc of PTN, t being transition of PTN such that
A3: t in T0 and
A4: f = [s,t] by A2;
    f`1 = s & f`2 = t by A4,MCART_1:7;
    hence thesis by A1,A3;
  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
A5: x = f`1 & f`2 in T0;
  f = [f`1,f`2] by MCART_1:21;
  hence thesis by A5;
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;
  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
A1: x = s and
A2: ex f being S-T_arc of PTN, t being transition of PTN st t in T0 &
    f = [s,t];
    consider f being S-T_arc of PTN, t being transition of PTN such that
A3: t in T0 & f = [s,t] by A2;
    take f, t;
    thus thesis by A1,A3;
  end;
  given f being S-T_arc of PTN, t being transition of PTN such that
A4: t in T0 and
A5: f = [x,t];
  x = f`1 by A5,MCART_1:7;
  hence thesis by A4,A5;
end;

theorem
  T0*' = {f`2 where f is T-S_arc of PTN : f`1 in T0}
proof
  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
A1: x = s and
A2: ex f being T-S_arc of PTN, t being transition of PTN st t in T0 &
    f = [t,s];
    consider f being T-S_arc of PTN, t being transition of PTN such that
A3: t in T0 and
A4: f = [t,s] by A2;
    f`1 = t & f`2 = s by A4,MCART_1:7;
    hence thesis by A1,A3;
  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
A5: x = f`2 & f`1 in T0;
  f = [f`1,f`2] by MCART_1:21;
  hence thesis by A5;
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;
  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
A1: x = s and
A2: ex f being T-S_arc of PTN, t being transition of PTN st t in T0 &
    f = [t,s];
    consider f being T-S_arc of PTN, t being transition of PTN such that
A3: t in T0 & f = [t,s] by A2;
    take f, t;
    thus thesis by A1,A3;
  end;
  given f being T-S_arc of PTN, t being transition of PTN such that
A4: t in T0 and
A5: f = [t,x];
  x = f`2 by A5,MCART_1:7;
  hence thesis by A4,A5;
end;

theorem
  *'{}the carrier of PTN = {}
proof
  set x = the Element of *'{}the carrier of PTN;
  assume not thesis;
  then x in *'{}the carrier of PTN;
  then ex t being transition of PTN st x = t & ex f being T-S_arc of PTN, s
  being place of PTN st s in {}the carrier of PTN & f = [t,s];
  hence contradiction;
end;

theorem
  ({}the carrier of PTN)*' = {}
proof
  set x = the Element of ({}the carrier of PTN)*';
  assume not thesis;
  then x in ({}the carrier of PTN)*';
  then ex t being transition of PTN st x = t & ex f being S-T_arc of PTN, s
  being place of PTN st s in {}the carrier of PTN & f = [s,t];
  hence contradiction;
end;

theorem
  *'{}the carrier' of PTN = {}
proof
  set x = the Element of *'{}the carrier' of PTN;
  assume not thesis;
  then x in *'{}the carrier' of PTN;
  then ex s being place of PTN st x = s & ex f being S-T_arc of PTN, t being
  transition of PTN st t in {}the carrier' of PTN & f = [s,t];
  hence contradiction;
end;

theorem
  ({}the carrier' of PTN)*' = {}
proof
  set x = the Element of ({}the carrier' of PTN)*';
  assume not thesis;
  then x in ({}the carrier' of PTN)*';
  then ex s being place of PTN st x = s & ex f being T-S_arc of PTN, t being
  transition of PTN st t in {}the carrier' of PTN & f = [t,s];
  hence contradiction;
end;

begin

:: Deadlock-like Attribute for Place Sets

definition
  let PTN;
  let IT be Subset of the carrier 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 Petri_net;
  attr IT is With_Deadlocks means
  ex S being Subset of the carrier of IT st S is Deadlock-like;
end;

registration
  cluster With_Deadlocks for Petri_net;
  existence
  proof
    take PTN1 = TrivialPetriNet;
    reconsider s = {} as place of PTN1 by TARSKI:def 1;
    reconsider t = {} as transition of PTN1 by TARSKI:def 1;
A1:  [#]({{}},{{}}) = {[{},{}]} by ZFMISC_1:29;
    then reconsider stf = [{},{}] as S-T_arc of PTN1 by TARSKI:def 1;
    reconsider tsf = [{},{}] as T-S_arc of PTN1 by A1,TARSKI:def 1;
    {{}} c= the carrier of PTN1;
    then reconsider S = {{}} as Subset of the carrier of PTN1;
    take S;
    tsf = [t,s];
    then t in *'S;
    then {t} c= *'S by ZFMISC_1:31;
    then
A2: {t} = *'S by XBOOLE_0:def 10;
    stf = [s,t];
    then t in S*';
    hence *'S is Subset of S*' by A2,ZFMISC_1:31;
  end;
end;

begin

:: Trap-like Attribute for Place Sets

definition
  let PTN;
  let IT be Subset of the carrier 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 Petri_net;
  attr IT is With_Traps means
  ex S being Subset of the carrier of IT st S is Trap-like;
end;

registration
  cluster With_Traps for Petri_net;
  existence
  proof
    take PTN1 = TrivialPetriNet;
    reconsider s = {} as place of PTN1 by TARSKI:def 1;
    reconsider t = {} as transition of PTN1 by TARSKI:def 1;
A1:  [#]({{}},{{}}) = {[{},{}]} by ZFMISC_1:29;
    then reconsider stf = [{},{}] as S-T_arc of PTN1 by TARSKI:def 1;
    reconsider tsf = [{},{}] as T-S_arc of PTN1 by A1,TARSKI:def 1;
    {{}} c= the carrier of PTN1;
    then reconsider S = {{}} as Subset of the carrier of PTN1;
    take S;
    stf = [s,t];
    then t in S*';
    then {t} c= S*' by ZFMISC_1:31;
    then
A2: {t} = S*' by XBOOLE_0:def 10;
    tsf = [t,s];
    then t in *'S;
    hence S*' is Subset of *'S by A2,ZFMISC_1:31;
  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
    set x = the 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 be PT_net_Str;
  func PTN.: -> strict PT_net_Str equals
  PT_net_Str(# the carrier of PTN, the
    carrier' of PTN, (the T-S_Arcs of PTN)~, (the S-T_Arcs of PTN)~ #);
  correctness;
end;

registration let PTN be Petri_net;
 cluster PTN.: -> with_S-T_arc with_T-S_arc non empty non void;
 coherence
  proof
    (the T-S_Arcs of PTN)~ is non empty;
   hence the S-T_Arcs of PTN.: is non empty;
    (the S-T_Arcs of PTN)~ is non empty;
   hence the T-S_Arcs of PTN.: is non empty;
   thus thesis;
  end;
end;

theorem
  PTN.:.: = the PT_net_Str of PTN;

theorem
  the carrier of PTN = the carrier of PTN.: & the carrier' of PTN = the
  carrier' 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.:;

definition
  let PTN;
  let S0 be Subset of the carrier of PTN;
  func S0.: -> Subset of the carrier of PTN.: equals
  S0;
  coherence;
end;

definition
  let PTN;
  let s be place of PTN;
  func s.: -> place of PTN.: equals
  s;
  coherence;
end;

definition
  let PTN;
  let S0 be Subset of the carrier of PTN.:;
  func .:S0 -> Subset of the carrier of PTN equals
  S0;
  coherence;
end;

definition
  let PTN;
  let s be place of PTN.:;
  func .:s -> place of PTN equals
  s;
  coherence;
end;

definition
  let PTN;
  let T0 be Subset of the carrier' of PTN;
  func T0.: -> Subset of the carrier' of PTN.: equals
  T0;
  coherence;
end;

definition
  let PTN;
  let t be transition of PTN;
  func t.: -> transition of PTN.: equals
  t;
  coherence;
end;

definition
  let PTN;
  let T0 be Subset of the carrier' of PTN.:;
  func .:T0 -> Subset of the carrier' of PTN equals
  T0;
  coherence;
end;

definition
  let PTN;
  let t be transition of PTN.:;
  func .:t -> transition of PTN equals
  t;
  coherence;
end;

reserve S for Subset of the carrier of PTN;

theorem Th15:
  S.:*' = *'S
proof
  thus S.:*' c= *'S
  proof
    let x be set;
    assume x in S.:*';
    then consider f being S-T_arc of PTN.:, s being place of PTN.: such that
A1: s in S.: and
A2: f = [s,x] by Th4;
    [x,.:s] is T-S_arc of PTN by A2,RELAT_1:def 7;
    hence thesis by A1,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
A3: s in S and
A4: f = [x,s] by Th2;
  [s.:,x] is S-T_arc of PTN.: by A4,RELAT_1:def 7;
  hence thesis by A3,Th4;
end;

theorem Th16:
  *'(S.:) = S*'
proof
  thus *'(S.:) c= S*'
  proof
    let x be set;
    assume x in *'(S.:);
    then consider f being T-S_arc of PTN.:, s being place of PTN.: such that
A1: s in S.: and
A2: f = [x,s] by Th2;
    [.:s,x] is S-T_arc of PTN by A2,RELAT_1:def 7;
    hence thesis by A1,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
A3: s in S and
A4: f = [s,x] by Th4;
  [x,s.:] is T-S_arc of PTN.: by A4,RELAT_1:def 7;
  hence thesis by A3,Th2;
end;

theorem
  S is Deadlock-like iff S.: is Trap-like
proof
A1: S.:*' = *'S by Th15;
  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,Th16;
  end;
  assume S.:*' is Subset of *'(S.:);
  hence *'S is Subset of S*' by A1,Th16;
end;

theorem
  S is Trap-like iff S.: is Deadlock-like
proof
A1: S.:*' = *'S by Th15;
  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,Th16;
  end;
  assume *'(S.:) is Subset of S.:*';
  hence S*' is Subset of *'S by A1,Th16;
end;

theorem
  for PTN being Petri_net, t being transition of PTN, S0 being Subset
  of the carrier of PTN holds t in S0*' iff *'{t} meets S0
proof
  let PTN be Petri_net;
  let t be transition of PTN;
  let S0 be Subset of the carrier 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 and
A2: f = [s,t] by Th4;
    t in {t} by TARSKI:def 1;
    then s in *'{t} by A2;
    hence *'{t} /\ S0 <> {} by A1,XBOOLE_0:def 4;
  end;
  assume *'{t} /\ S0 <> {};
  then consider s being place of PTN such that
A3: s in *'{t} /\ S0 by SUBSET_1:4;
A4: s in S0 by A3,XBOOLE_0:def 4;
  s in *'{t} by A3,XBOOLE_0:def 4;
  then consider f being S-T_arc of PTN, t0 being transition of PTN such that
A5: t0 in {t} and
A6: f = [s,t0] by Th6;
  t0 = t by A5,TARSKI:def 1;
  hence thesis by A4,A6;
end;

theorem
  for PTN being Petri_net, t being transition of PTN, S0 being Subset
  of the carrier of PTN holds t in *'S0 iff {t}*' meets S0
proof
  let PTN be Petri_net;
  let t be transition of PTN;
  let S0 be Subset of the carrier 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 and
A2: f = [t,s] by Th2;
    t in {t} by TARSKI:def 1;
    then s in {t}*' by A2;
    hence {t}*' /\ S0 <> {} by A1,XBOOLE_0:def 4;
  end;
  assume {t}*' /\ S0 <> {};
  then consider s being place of PTN such that
A3: s in {t}*' /\ S0 by SUBSET_1:4;
A4: s in S0 by A3,XBOOLE_0:def 4;
  s in {t}*' by A3,XBOOLE_0:def 4;
  then consider f being T-S_arc of PTN, t0 being transition of PTN such that
A5: t0 in {t} and
A6: f = [t0,s] by Th8;
  t0 = t by A5,TARSKI:def 1;
  hence thesis by A4,A6;
end;