The Mizar article:

Basic Petri Net Concepts

by
Pauline N. Kawamoto,
Yasushi Fuwa, and
Yatsuka Nakamura

Received November 27, 1992

Copyright (c) 1992 Association of Mizar Users

MML identifier: PETRI
[ MML identifier index ]


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;

Back to top