:: by Grzegorz Bancerek , Mitsuru Aoki , Akio Matsumoto and Yasunari Shidama

::

:: Received December 20, 2002

:: Copyright (c) 2002-2021 Association of Mizar Users

notation
end;

definition

let P be set ;

let m1, m2 be marking of P;

( m1 = m2 iff for p being object st p in P holds

p multitude_of = p multitude_of )

end;
let m1, m2 be marking of P;

:: original: =

redefine pred m1 = m2 means :: PNPROC_1:def 1

for p being object st p in P holds

p multitude_of = p multitude_of ;

compatibility redefine pred m1 = m2 means :: PNPROC_1:def 1

for p being object st p in P holds

p multitude_of = p multitude_of ;

( m1 = m2 iff for p being object st p in P holds

p multitude_of = p multitude_of )

proof end;

:: deftheorem defines = PNPROC_1:def 1 :

for P being set

for m1, m2 being marking of P holds

( m1 = m2 iff for p being object st p in P holds

p multitude_of = p multitude_of );

for P being set

for m1, m2 being marking of P holds

( m1 = m2 iff for p being object st p in P holds

p multitude_of = p multitude_of );

definition

let P be set ;

let m1, m2 be marking of P;

for m1 being marking of P

for p being set st p in P holds

p multitude_of <= p multitude_of ;

end;
let m1, m2 be marking of P;

pred m1 c= m2 means :: PNPROC_1:def 3

for p being set st p in P holds

p multitude_of <= p multitude_of ;

reflexivity for p being set st p in P holds

p multitude_of <= p multitude_of ;

for m1 being marking of P

for p being set st p in P holds

p multitude_of <= p multitude_of ;

:: deftheorem defines c= PNPROC_1:def 3 :

for P being set

for m1, m2 being marking of P holds

( m1 c= m2 iff for p being set st p in P holds

p multitude_of <= p multitude_of );

for P being set

for m1, m2 being marking of P holds

( m1 c= m2 iff for p being set st p in P holds

p multitude_of <= p multitude_of );

Lm1: for P, p being set st p in P holds

({$} P) . p = 0

by FUNCOP_1:7;

definition

let P be set ;

let m1, m2 be marking of P;

m1 + m2 is marking of P

for b_{1} being marking of P holds

( b_{1} = m1 + m2 iff for p being set st p in P holds

p multitude_of = (p multitude_of ) + (p multitude_of ) )

end;
let m1, m2 be marking of P;

:: original: +

redefine func m1 + m2 -> marking of P means :Def4: :: PNPROC_1:def 4

for p being set st p in P holds

p multitude_of = (p multitude_of ) + (p multitude_of );

coherence redefine func m1 + m2 -> marking of P means :Def4: :: PNPROC_1:def 4

for p being set st p in P holds

p multitude_of = (p multitude_of ) + (p multitude_of );

m1 + m2 is marking of P

proof end;

compatibility for b

( b

p multitude_of = (p multitude_of ) + (p multitude_of ) )

proof end;

:: deftheorem Def4 defines + PNPROC_1:def 4 :

for P being set

for m1, m2, b_{4} being marking of P holds

( b_{4} = m1 + m2 iff for p being set st p in P holds

p multitude_of = (p multitude_of ) + (p multitude_of ) );

for P being set

for m1, m2, b

( b

p multitude_of = (p multitude_of ) + (p multitude_of ) );

definition

let P be set ;

let m1, m2 be marking of P;

assume A1: m2 c= m1 ;

ex b_{1} being marking of P st

for p being set st p in P holds

p multitude_of = (p multitude_of ) - (p multitude_of )

for b_{1}, b_{2} being marking of P st ( for p being set st p in P holds

p multitude_of = (p multitude_of ) - (p multitude_of ) ) & ( for p being set st p in P holds

p multitude_of = (p multitude_of ) - (p multitude_of ) ) holds

b_{1} = b_{2}

end;
let m1, m2 be marking of P;

assume A1: m2 c= m1 ;

func m1 - m2 -> marking of P means :Def5: :: PNPROC_1:def 5

for p being set st p in P holds

p multitude_of = (p multitude_of ) - (p multitude_of );

existence for p being set st p in P holds

p multitude_of = (p multitude_of ) - (p multitude_of );

ex b

for p being set st p in P holds

p multitude_of = (p multitude_of ) - (p multitude_of )

proof end;

uniqueness for b

p multitude_of = (p multitude_of ) - (p multitude_of ) ) & ( for p being set st p in P holds

p multitude_of = (p multitude_of ) - (p multitude_of ) ) holds

b

proof end;

:: deftheorem Def5 defines - PNPROC_1:def 5 :

for P being set

for m1, m2 being marking of P st m2 c= m1 holds

for b_{4} being marking of P holds

( b_{4} = m1 - m2 iff for p being set st p in P holds

p multitude_of = (p multitude_of ) - (p multitude_of ) );

for P being set

for m1, m2 being marking of P st m2 c= m1 holds

for b

( b

p multitude_of = (p multitude_of ) - (p multitude_of ) );

theorem :: PNPROC_1:12

for P being set

for m1, m2, m3, m4 being marking of P st m1 c= m2 & m3 c= m4 holds

m1 + m3 c= m2 + m4

for m1, m2, m3, m4 being marking of P st m1 c= m2 & m3 c= m4 holds

m1 + m3 c= m2 + m4

proof end;

theorem Th14: :: PNPROC_1:14

for P being set

for m1, m2, m3, m4 being marking of P st m1 c= m2 & m3 c= m4 & m4 c= m1 holds

m1 - m4 c= m2 - m3

for m1, m2, m3, m4 being marking of P st m1 c= m2 & m3 c= m4 & m4 c= m1 holds

m1 - m4 c= m2 - m3

proof end;

theorem Th17: :: PNPROC_1:17

for P being set

for m1, m2, m3 being marking of P st m2 + m3 c= m1 holds

(m1 - m2) - m3 = m1 - (m2 + m3)

for m1, m2, m3 being marking of P st m2 + m3 c= m1 holds

(m1 - m2) - m3 = m1 - (m2 + m3)

proof end;

theorem :: PNPROC_1:18

for P being set

for m1, m2, m3 being marking of P st m3 c= m2 & m2 c= m1 holds

m1 - (m2 - m3) = (m1 - m2) + m3

for m1, m2, m3 being marking of P st m3 c= m2 & m2 c= m1 holds

m1 - (m2 - m3) = (m1 - m2) + m3

proof end;

definition

let P be set ;

ex b_{1} being set ex m1, m2 being marking of P st b_{1} = [m1,m2]

end;
mode transition of P -> set means :Def6: :: PNPROC_1:def 6

ex m1, m2 being marking of P st it = [m1,m2];

existence ex m1, m2 being marking of P st it = [m1,m2];

ex b

proof end;

:: deftheorem Def6 defines transition PNPROC_1:def 6 :

for P, b_{2} being set holds

( b_{2} is transition of P iff ex m1, m2 being marking of P st b_{2} = [m1,m2] );

for P, b

( b

notation
end;

definition

let P be set ;

let t be transition of P;

:: original: Pre

redefine func Pre t -> marking of P;

coherence

Pre is marking of P

redefine func Post t -> marking of P;

coherence

Post is marking of P

end;
let t be transition of P;

:: original: Pre

redefine func Pre t -> marking of P;

coherence

Pre is marking of P

proof end;

:: original: Postredefine func Post t -> marking of P;

coherence

Post is marking of P

proof end;

definition

let P be set ;

let m be marking of P;

let t be transition of P;

( ( Pre t c= m implies (m - (Pre t)) + (Post t) is marking of P ) & ( not Pre t c= m implies m is marking of P ) ) ;

consistency

for b_{1} being marking of P holds verum
;

end;
let m be marking of P;

let t be transition of P;

func fire (t,m) -> marking of P equals :Def7: :: PNPROC_1:def 7

(m - (Pre t)) + (Post t) if Pre t c= m

otherwise m;

coherence (m - (Pre t)) + (Post t) if Pre t c= m

otherwise m;

( ( Pre t c= m implies (m - (Pre t)) + (Post t) is marking of P ) & ( not Pre t c= m implies m is marking of P ) ) ;

consistency

for b

:: deftheorem Def7 defines fire PNPROC_1:def 7 :

for P being set

for m being marking of P

for t being transition of P holds

( ( Pre t c= m implies fire (t,m) = (m - (Pre t)) + (Post t) ) & ( not Pre t c= m implies fire (t,m) = m ) );

for P being set

for m being marking of P

for t being transition of P holds

( ( Pre t c= m implies fire (t,m) = (m - (Pre t)) + (Post t) ) & ( not Pre t c= m implies fire (t,m) = m ) );

theorem :: PNPROC_1:19

for P being set

for m being marking of P

for t1, t2 being transition of P st (Pre t1) + (Pre t2) c= m holds

fire (t2,(fire (t1,m))) = (((m - (Pre t1)) - (Pre t2)) + (Post t1)) + (Post t2)

for m being marking of P

for t1, t2 being transition of P st (Pre t1) + (Pre t2) c= m holds

fire (t2,(fire (t1,m))) = (((m - (Pre t1)) - (Pre t2)) + (Post t1)) + (Post t2)

proof end;

definition

let P be set ;

let t be transition of P;

ex b_{1} being Function st

( dom b_{1} = Funcs (P,NAT) & ( for m being marking of P holds b_{1} . m = fire (t,m) ) )

for b_{1}, b_{2} being Function st dom b_{1} = Funcs (P,NAT) & ( for m being marking of P holds b_{1} . m = fire (t,m) ) & dom b_{2} = Funcs (P,NAT) & ( for m being marking of P holds b_{2} . m = fire (t,m) ) holds

b_{1} = b_{2}

end;
let t be transition of P;

func fire t -> Function means :Def8: :: PNPROC_1:def 8

( dom it = Funcs (P,NAT) & ( for m being marking of P holds it . m = fire (t,m) ) );

existence ( dom it = Funcs (P,NAT) & ( for m being marking of P holds it . m = fire (t,m) ) );

ex b

( dom b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def8 defines fire PNPROC_1:def 8 :

for P being set

for t being transition of P

for b_{3} being Function holds

( b_{3} = fire t iff ( dom b_{3} = Funcs (P,NAT) & ( for m being marking of P holds b_{3} . m = fire (t,m) ) ) );

for P being set

for t being transition of P

for b

( b

theorem :: PNPROC_1:21

for P being set

for m being marking of P

for t1, t2 being transition of P holds fire (t2,(fire (t1,m))) = ((fire t2) * (fire t1)) . m

for m being marking of P

for t1, t2 being transition of P holds fire (t2,(fire (t1,m))) = ((fire t2) * (fire t1)) . m

proof end;

definition

let P be set ;

ex b_{1} being non empty set st

for x being set st x in b_{1} holds

x is transition of P

end;
mode Petri_net of P -> non empty set means :Def9: :: PNPROC_1:def 9

for x being set st x in it holds

x is transition of P;

existence for x being set st x in it holds

x is transition of P;

ex b

for x being set st x in b

x is transition of P

proof end;

:: deftheorem Def9 defines Petri_net PNPROC_1:def 9 :

for P being set

for b_{2} being non empty set holds

( b_{2} is Petri_net of P iff for x being set st x in b_{2} holds

x is transition of P );

for P being set

for b

( b

x is transition of P );

definition

let P be set ;

let N be Petri_net of P;

:: original: Element

redefine mode Element of N -> transition of P;

coherence

for b_{1} being Element of N holds b_{1} is transition of P
by Def9;

end;
let N be Petri_net of P;

:: original: Element

redefine mode Element of N -> transition of P;

coherence

for b

definition

let P be set ;

let N be Petri_net of P;

let C be firing-sequence of N;

ex b_{1} being Function ex F being Function-yielding FinSequence st

( b_{1} = compose (F,(Funcs (P,NAT))) & len F = len C & ( for i being Element of NAT st i in dom C holds

F . i = fire (C /. i) ) )

for b_{1}, b_{2} being Function st ex F being Function-yielding FinSequence st

( b_{1} = compose (F,(Funcs (P,NAT))) & len F = len C & ( for i being Element of NAT st i in dom C holds

F . i = fire (C /. i) ) ) & ex F being Function-yielding FinSequence st

( b_{2} = compose (F,(Funcs (P,NAT))) & len F = len C & ( for i being Element of NAT st i in dom C holds

F . i = fire (C /. i) ) ) holds

b_{1} = b_{2}

end;
let N be Petri_net of P;

let C be firing-sequence of N;

func fire C -> Function means :Def10: :: PNPROC_1:def 10

ex F being Function-yielding FinSequence st

( it = compose (F,(Funcs (P,NAT))) & len F = len C & ( for i being Element of NAT st i in dom C holds

F . i = fire (C /. i) ) );

existence ex F being Function-yielding FinSequence st

( it = compose (F,(Funcs (P,NAT))) & len F = len C & ( for i being Element of NAT st i in dom C holds

F . i = fire (C /. i) ) );

ex b

( b

F . i = fire (C /. i) ) )

proof end;

uniqueness for b

( b

F . i = fire (C /. i) ) ) & ex F being Function-yielding FinSequence st

( b

F . i = fire (C /. i) ) ) holds

b

proof end;

:: deftheorem Def10 defines fire PNPROC_1:def 10 :

for P being set

for N being Petri_net of P

for C being firing-sequence of N

for b_{4} being Function holds

( b_{4} = fire C iff ex F being Function-yielding FinSequence st

( b_{4} = compose (F,(Funcs (P,NAT))) & len F = len C & ( for i being Element of NAT st i in dom C holds

F . i = fire (C /. i) ) ) );

for P being set

for N being Petri_net of P

for C being firing-sequence of N

for b

( b

( b

F . i = fire (C /. i) ) ) );

:: Firing of empty firing-sequence <*>N

:: Firing of firing-sequence with one translation <*e*>

theorem Th24: :: PNPROC_1:24

for P being set

for N being Petri_net of P

for e being Element of N holds (fire e) * (id (Funcs (P,NAT))) = fire e

for N being Petri_net of P

for e being Element of N holds (fire e) * (id (Funcs (P,NAT))) = fire e

proof end;

:: Firing of firing-sequence with two translations <*e1,e2*>

theorem :: PNPROC_1:25

for P being set

for N being Petri_net of P

for e1, e2 being Element of N holds fire <*e1,e2*> = (fire e2) * (fire e1)

for N being Petri_net of P

for e1, e2 being Element of N holds fire <*e1,e2*> = (fire e2) * (fire e1)

proof end;

theorem Th26: :: PNPROC_1:26

for P being set

for N being Petri_net of P

for C being firing-sequence of N holds

( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )

for N being Petri_net of P

for C being firing-sequence of N holds

( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )

proof end;

:: Firing of compound firing-sequence

theorem Th27: :: PNPROC_1:27

for P being set

for N being Petri_net of P

for C1, C2 being firing-sequence of N holds fire (C1 ^ C2) = (fire C2) * (fire C1)

for N being Petri_net of P

for C1, C2 being firing-sequence of N holds fire (C1 ^ C2) = (fire C2) * (fire C1)

proof end;

theorem :: PNPROC_1:28

for P being set

for N being Petri_net of P

for e being Element of N

for C being firing-sequence of N holds fire (C ^ <*e*>) = (fire e) * (fire C)

for N being Petri_net of P

for e being Element of N

for C being firing-sequence of N holds fire (C ^ <*e*>) = (fire e) * (fire C)

proof end;

definition

let P be set ;

let N be Petri_net of P;

let C be firing-sequence of N;

let m be marking of P;

coherence

(fire C) . m is marking of P

end;
let N be Petri_net of P;

let C be firing-sequence of N;

let m be marking of P;

coherence

(fire C) . m is marking of P

proof end;

:: deftheorem defines fire PNPROC_1:def 11 :

for P being set

for N being Petri_net of P

for C being firing-sequence of N

for m being marking of P holds fire (C,m) = (fire C) . m;

for P being set

for N being Petri_net of P

for C being firing-sequence of N

for m being marking of P holds fire (C,m) = (fire C) . m;

definition

let P be set ;

let N be Petri_net of P;

let R1, R2 be process of N;

{ (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } is process of N

end;
let N be Petri_net of P;

let R1, R2 be process of N;

func R1 before R2 -> process of N equals :: PNPROC_1:def 12

{ (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } ;

coherence { (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } ;

{ (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } is process of N

proof end;

:: deftheorem defines before PNPROC_1:def 12 :

for P being set

for N being Petri_net of P

for R1, R2 being process of N holds R1 before R2 = { (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } ;

for P being set

for N being Petri_net of P

for R1, R2 being process of N holds R1 before R2 = { (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } ;

registration

let P be set ;

let N be Petri_net of P;

let R1, R2 be non empty process of N;

coherence

not R1 before R2 is empty

end;
let N be Petri_net of P;

let R1, R2 be non empty process of N;

coherence

not R1 before R2 is empty

proof end;

theorem Th29: :: PNPROC_1:29

for P being set

for N being Petri_net of P

for R, R1, R2 being process of N holds (R1 \/ R2) before R = (R1 before R) \/ (R2 before R)

for N being Petri_net of P

for R, R1, R2 being process of N holds (R1 \/ R2) before R = (R1 before R) \/ (R2 before R)

proof end;

theorem Th30: :: PNPROC_1:30

for P being set

for N being Petri_net of P

for R, R1, R2 being process of N holds R before (R1 \/ R2) = (R before R1) \/ (R before R2)

for N being Petri_net of P

for R, R1, R2 being process of N holds R before (R1 \/ R2) = (R before R1) \/ (R before R2)

proof end;

theorem Th31: :: PNPROC_1:31

for P being set

for N being Petri_net of P

for C1, C2 being firing-sequence of N holds {C1} before {C2} = {(C1 ^ C2)}

for N being Petri_net of P

for C1, C2 being firing-sequence of N holds {C1} before {C2} = {(C1 ^ C2)}

proof end;

theorem :: PNPROC_1:32

for P being set

for N being Petri_net of P

for C, C1, C2 being firing-sequence of N holds {C1,C2} before {C} = {(C1 ^ C),(C2 ^ C)}

for N being Petri_net of P

for C, C1, C2 being firing-sequence of N holds {C1,C2} before {C} = {(C1 ^ C),(C2 ^ C)}

proof end;

theorem :: PNPROC_1:33

for P being set

for N being Petri_net of P

for C, C1, C2 being firing-sequence of N holds {C} before {C1,C2} = {(C ^ C1),(C ^ C2)}

for N being Petri_net of P

for C, C1, C2 being firing-sequence of N holds {C} before {C1,C2} = {(C ^ C1),(C ^ C2)}

proof end;

definition

let P be set ;

let N be Petri_net of P;

let R1, R2 be process of N;

{ C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } is process of N

for b_{1}, R1, R2 being process of N st b_{1} = { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } holds

b_{1} = { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) }

end;
let N be Petri_net of P;

let R1, R2 be process of N;

func R1 concur R2 -> process of N equals :: PNPROC_1:def 13

{ C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } ;

coherence { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } ;

{ C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } is process of N

proof end;

commutativity for b

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } holds

b

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) }

proof end;

:: deftheorem defines concur PNPROC_1:def 13 :

for P being set

for N being Petri_net of P

for R1, R2 being process of N holds R1 concur R2 = { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } ;

for P being set

for N being Petri_net of P

for R1, R2 being process of N holds R1 concur R2 = { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st

( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } ;

theorem Th34: :: PNPROC_1:34

for P being set

for N being Petri_net of P

for R, R1, R2 being process of N holds (R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R)

for N being Petri_net of P

for R, R1, R2 being process of N holds (R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R)

proof end;

theorem Th35: :: PNPROC_1:35

for P being set

for N being Petri_net of P

for e1, e2 being Element of N holds {<*e1*>} concur {<*e2*>} = {<*e1,e2*>,<*e2,e1*>}

for N being Petri_net of P

for e1, e2 being Element of N holds {<*e1*>} concur {<*e2*>} = {<*e1,e2*>,<*e2,e1*>}

proof end;

theorem :: PNPROC_1:36

for P being set

for N being Petri_net of P

for e, e1, e2 being Element of N holds {<*e1*>,<*e2*>} concur {<*e*>} = {<*e1,e*>,<*e2,e*>,<*e,e1*>,<*e,e2*>}

for N being Petri_net of P

for e, e1, e2 being Element of N holds {<*e1*>,<*e2*>} concur {<*e*>} = {<*e1,e*>,<*e2,e*>,<*e,e1*>,<*e,e2*>}

proof end;

theorem :: PNPROC_1:37

for P being set

for N being Petri_net of P

for R1, R2, R3 being process of N holds (R1 before R2) before R3 = R1 before (R2 before R3)

for N being Petri_net of P

for R1, R2, R3 being process of N holds (R1 before R2) before R3 = R1 before (R2 before R3)

proof end;

theorem :: PNPROC_1:38

for P being set

for N being Petri_net of P

for R1, R2, R3 being process of N holds (R1 concur R2) concur R3 = R1 concur (R2 concur R3)

for N being Petri_net of P

for R1, R2, R3 being process of N holds (R1 concur R2) concur R3 = R1 concur (R2 concur R3)

proof end;

theorem :: PNPROC_1:39

for P being set

for N being Petri_net of P

for R1, R2 being process of N holds R1 before R2 c= R1 concur R2

for N being Petri_net of P

for R1, R2 being process of N holds R1 before R2 c= R1 concur R2

proof end;

theorem :: PNPROC_1:40

for P being set

for N being Petri_net of P

for R1, R2, P1, P2 being process of N st R1 c= P1 & R2 c= P2 holds

R1 before R2 c= P1 before P2

for N being Petri_net of P

for R1, R2, P1, P2 being process of N st R1 c= P1 & R2 c= P2 holds

R1 before R2 c= P1 before P2

proof end;

theorem :: PNPROC_1:41

for P being set

for N being Petri_net of P

for R1, R2, P1, P2 being process of N st R1 c= P1 & R2 c= P2 holds

R1 concur R2 c= P1 concur P2

for N being Petri_net of P

for R1, R2, P1, P2 being process of N st R1 c= P1 & R2 c= P2 holds

R1 concur R2 c= P1 concur P2

proof end;

Lm2: for p1, p2 being FinSequence

for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds

dom (q1 \/ ((len p1) Shift q2)) c= dom (p1 ^ p2)

proof end;

Lm3: for p1 being FinSequence

for q1, q2 being FinSubsequence st q1 c= p1 holds

q1 misses (len p1) Shift q2

by VALUED_1:50, XBOOLE_1:63;

theorem :: PNPROC_1:42

for P being set

for N being Petri_net of P

for R1, R2, P1, P2 being process of N holds (R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2)

for N being Petri_net of P

for R1, R2, P1, P2 being process of N holds (R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2)

proof end;

registration

let P be set ;

let N be Petri_net of P;

let R1, R2 be non empty process of N;

coherence

not R1 concur R2 is empty

end;
let N be Petri_net of P;

let R1, R2 be non empty process of N;

coherence

not R1 concur R2 is empty

proof end;

definition
end;

:: deftheorem defines NeutralProcess PNPROC_1:def 14 :

for P being set

for N being Petri_net of P holds NeutralProcess N = {(<*> N)};

for P being set

for N being Petri_net of P holds NeutralProcess N = {(<*> N)};

definition

let P be set ;

let N be Petri_net of P;

let t be Element of N;

coherence

{<*t*>} is non empty process of N ;

end;
let N be Petri_net of P;

let t be Element of N;

coherence

{<*t*>} is non empty process of N ;

:: deftheorem defines ElementaryProcess PNPROC_1:def 15 :

for P being set

for N being Petri_net of P

for t being Element of N holds ElementaryProcess t = {<*t*>};

for P being set

for N being Petri_net of P

for t being Element of N holds ElementaryProcess t = {<*t*>};

theorem :: PNPROC_1:43

for P being set

for N being Petri_net of P

for R being process of N holds (NeutralProcess N) before R = R

for N being Petri_net of P

for R being process of N holds (NeutralProcess N) before R = R

proof end;

theorem :: PNPROC_1:44

for P being set

for N being Petri_net of P

for R being process of N holds R before (NeutralProcess N) = R

for N being Petri_net of P

for R being process of N holds R before (NeutralProcess N) = R

proof end;

theorem :: PNPROC_1:45

for P being set

for N being Petri_net of P

for R being process of N holds (NeutralProcess N) concur R = R

for N being Petri_net of P

for R being process of N holds (NeutralProcess N) concur R = R

proof end;