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

::

:: Received December 20, 2002

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

begin

Lm1: for p being FinSubsequence st Seq p = {} holds

p = {}

proof end;

theorem Th3: :: PNPROC_1:3

for i being Element of NAT

for x being set

for q being FinSubsequence st q = {[i,x]} holds

Seq q = <*x*>

for x being set

for q being FinSubsequence st q = {[i,x]} holds

Seq q = <*x*>

proof end;

theorem Th4: :: PNPROC_1:4

for x being set

for q being FinSubsequence st Seq q = <*x*> holds

ex i being Element of NAT st q = {[i,x]}

for q being FinSubsequence st Seq q = <*x*> holds

ex i being Element of NAT st q = {[i,x]}

proof end;

theorem Th5: :: PNPROC_1:5

for x1, y1, x2, y2 being set holds

( not {[x1,y1],[x2,y2]} is FinSequence or ( x1 = 1 & x2 = 1 & y1 = y2 ) or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) )

( not {[x1,y1],[x2,y2]} is FinSequence or ( x1 = 1 & x2 = 1 & y1 = y2 ) or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) )

proof end;

Lm2: for j, k, l being Element of NAT st ( ( 1 <= j & j <= l ) or ( l + 1 <= j & j <= l + k ) ) holds

( 1 <= j & j <= l + k )

proof end;

Lm3: for X, Y being set holds

( ( for x being set st x in X holds

not x in Y ) iff X misses Y )

proof end;

Lm4: for P, R being Relation st dom P misses dom R holds

P misses R

by RELAT_1:179;

Lm5: for q being FinSubsequence holds dom (Seq q) = dom (Sgm (dom q))

proof end;

Lm6: for q being FinSubsequence holds rng q = rng (Seq q)

proof end;

begin

definition

let P be set ;

let m1, m2 be marking of P;

( m1 = m2 iff for p being set 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 set st p in P holds

p multitude_of = p multitude_of ;

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

for p being set st p in P holds

p multitude_of = p multitude_of ;

( m1 = m2 iff for p being set 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 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 = m2 iff for p being set 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 :Def3: :: 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 Def3 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 );

Lm7: 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 B1: 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 B1: 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:23

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 Th25: :: PNPROC_1:25

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 Th28: :: PNPROC_1:28

for P being set

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

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

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

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

proof end;

theorem :: PNPROC_1:29

for P being set

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

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

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

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

proof end;

begin

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 being set

for 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 being set

for 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:30

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:32

for P being set

for m being marking of P

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

for m being marking of P

for t2, t1 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

begin

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 Th35: :: PNPROC_1:35

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:36

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 Th37: :: PNPROC_1:37

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 Th38: :: PNPROC_1:38

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:39

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;

begin

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 Th40: :: PNPROC_1:40

for P being set

for N being Petri_net of P

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

for N being Petri_net of P

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

proof end;

theorem Th41: :: PNPROC_1:41

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 Th42: :: PNPROC_1:42

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:43

for P being set

for N being Petri_net of P

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

for N being Petri_net of P

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

proof end;

theorem :: PNPROC_1:44

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;

begin

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 Th45: :: PNPROC_1:45

for P being set

for N being Petri_net of P

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

for N being Petri_net of P

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

proof end;

theorem Th46: :: PNPROC_1:46

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:47

for P being set

for N being Petri_net of P

for e1, e2, e 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 e1, e2, e being Element of N holds {<*e1*>,<*e2*>} concur {<*e*>} = {<*e1,e*>,<*e2,e*>,<*e,e1*>,<*e,e2*>}

proof end;

theorem :: PNPROC_1:48

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;

definition

let p be FinSubsequence;

let i be Element of NAT ;

set X = { (i + k) where k is Element of NAT : k in dom p } ;

ex b_{1} being FinSubsequence st

( dom b_{1} = { (i + k) where k is Element of NAT : k in dom p } & ( for j being Nat st j in dom p holds

b_{1} . (i + j) = p . j ) )

for b_{1}, b_{2} being FinSubsequence st dom b_{1} = { (i + k) where k is Element of NAT : k in dom p } & ( for j being Nat st j in dom p holds

b_{1} . (i + j) = p . j ) & dom b_{2} = { (i + k) where k is Element of NAT : k in dom p } & ( for j being Nat st j in dom p holds

b_{2} . (i + j) = p . j ) holds

b_{1} = b_{2}

end;
let i be Element of NAT ;

set X = { (i + k) where k is Element of NAT : k in dom p } ;

func i Shift p -> FinSubsequence means :Def14: :: PNPROC_1:def 14

( dom it = { (i + k) where k is Element of NAT : k in dom p } & ( for j being Nat st j in dom p holds

it . (i + j) = p . j ) );

existence ( dom it = { (i + k) where k is Element of NAT : k in dom p } & ( for j being Nat st j in dom p holds

it . (i + j) = p . j ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def14 defines Shift PNPROC_1:def 14 :

for p being FinSubsequence

for i being Element of NAT

for b_{3} being FinSubsequence holds

( b_{3} = i Shift p iff ( dom b_{3} = { (i + k) where k is Element of NAT : k in dom p } & ( for j being Nat st j in dom p holds

b_{3} . (i + j) = p . j ) ) );

for p being FinSubsequence

for i being Element of NAT

for b

( b

b

theorem :: PNPROC_1:50

for i, j being Element of NAT

for q being FinSubsequence holds (i + j) Shift q = i Shift (j Shift q)

for q being FinSubsequence holds (i + j) Shift q = i Shift (j Shift q)

proof end;

theorem Th51: :: PNPROC_1:51

for i being Element of NAT

for p being FinSequence holds dom (i Shift p) = { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) }

for p being FinSequence holds dom (i Shift p) = { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) }

proof end;

theorem Th53: :: PNPROC_1:53

for i being Element of NAT

for q being FinSubsequence ex ss being FinSubsequence st

( dom ss = dom q & rng ss = dom (i Shift q) & ( for k being Element of NAT st k in dom q holds

ss . k = i + k ) & ss is one-to-one )

for q being FinSubsequence ex ss being FinSubsequence st

( dom ss = dom q & rng ss = dom (i Shift q) & ( for k being Element of NAT st k in dom q holds

ss . k = i + k ) & ss is one-to-one )

proof end;

Lm8: for i being Element of NAT

for p being FinSequence ex fs being FinSequence st

( dom fs = dom p & rng fs = dom (i Shift p) & ( for k being Element of NAT st k in dom p holds

fs . k = i + k ) & fs is one-to-one )

proof end;

theorem Th56: :: PNPROC_1:56

for k, i being Element of NAT

for p being FinSequence st k in dom p holds

(Sgm (dom (i Shift p))) . k = i + k

for p being FinSequence st k in dom p holds

(Sgm (dom (i Shift p))) . k = i + k

proof end;

theorem Th57: :: PNPROC_1:57

for k, i being Element of NAT

for p being FinSequence st k in dom p holds

(Seq (i Shift p)) . k = p . k

for p being FinSequence st k in dom p holds

(Seq (i Shift p)) . k = p . k

proof end;

theorem Th60: :: PNPROC_1:60

for i being Element of NAT

for p1 being FinSequence

for p2 being FinSubsequence st len p1 <= i holds

dom p1 misses dom (i Shift p2)

for p1 being FinSequence

for p2 being FinSubsequence st len p1 <= i holds

dom p1 misses dom (i Shift p2)

proof end;

theorem Th62: :: PNPROC_1:62

for i being Element of NAT

for p1 being FinSequence

for p2 being FinSubsequence st i >= len p1 holds

p1 misses i Shift p2

for p1 being FinSequence

for p2 being FinSubsequence st i >= len p1 holds

p1 misses i Shift p2

proof end;

theorem :: PNPROC_1:63

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:64

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:65

for P being set

for N being Petri_net of P

for R1, P1, R2, 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, P1, R2, 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:66

for P being set

for N being Petri_net of P

for R1, P1, R2, 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, P1, R2, P2 being process of N st R1 c= P1 & R2 c= P2 holds

R1 concur R2 c= P1 concur P2

proof end;

Lm9: 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;

Lm10: for p1 being FinSequence

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

q1 misses (len p1) Shift q2

by Th62, XBOOLE_1:63;

Lm11: for i being Element of NAT

for p, q being FinSubsequence st q c= p holds

dom (i Shift q) c= dom (i Shift p)

proof end;

theorem Th69: :: PNPROC_1:69

for i being Element of NAT

for q1, q2 being FinSubsequence st dom q1 misses dom q2 holds

dom (i Shift q1) misses dom (i Shift q2)

for q1, q2 being FinSubsequence st dom q1 misses dom q2 holds

dom (i Shift q1) misses dom (i Shift q2)

proof end;

theorem Th70: :: PNPROC_1:70

for i being Element of NAT

for q, q1, q2 being FinSubsequence st q = q1 \/ q2 & q1 misses q2 holds

(i Shift q1) \/ (i Shift q2) = i Shift q

for q, q1, q2 being FinSubsequence st q = q1 \/ q2 & q1 misses q2 holds

(i Shift q1) \/ (i Shift q2) = i Shift q

proof end;

theorem Th72: :: PNPROC_1:72

for k, i being Element of NAT

for q being FinSubsequence st k in dom (Seq q) holds

ex j being Element of NAT st

( j = (Sgm (dom q)) . k & (Sgm (dom (i Shift q))) . k = i + j )

for q being FinSubsequence st k in dom (Seq q) holds

ex j being Element of NAT st

( j = (Sgm (dom q)) . k & (Sgm (dom (i Shift q))) . k = i + j )

proof end;

theorem Th73: :: PNPROC_1:73

for k, i being Element of NAT

for q being FinSubsequence st k in dom (Seq q) holds

(Seq (i Shift q)) . k = (Seq q) . k

for q being FinSubsequence st k in dom (Seq q) holds

(Seq (i Shift q)) . k = (Seq q) . k

proof end;

theorem Th75: :: PNPROC_1:75

for k, i being Element of NAT

for q being FinSubsequence st dom q c= Seg k holds

dom (i Shift q) c= Seg (i + k)

for q being FinSubsequence st dom q c= Seg k holds

dom (i Shift q) c= Seg (i + k)

proof end;

theorem Th76: :: PNPROC_1:76

for p being FinSequence

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

ex ss being FinSubsequence st ss = q1 \/ ((len p) Shift q2)

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

ex ss being FinSubsequence st ss = q1 \/ ((len p) Shift q2)

proof end;

Lm12: for p1, p2 being FinSequence

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

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

proof end;

theorem Th77: :: PNPROC_1:77

for p1, p2 being FinSequence

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

ex ss being FinSubsequence st

( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) )

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

ex ss being FinSubsequence st

( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) )

proof end;

theorem Th78: :: PNPROC_1:78

for p1, p2 being FinSequence

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

ex ss being FinSubsequence st

( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) & Seq ss = (Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) )

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

ex ss being FinSubsequence st

( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) & Seq ss = (Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) )

proof end;

theorem Th79: :: PNPROC_1:79

for p1, p2 being FinSequence

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

ex ss being FinSubsequence st

( ss = q1 \/ ((len p1) Shift q2) & (Seq q1) ^ (Seq q2) = Seq ss )

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

ex ss being FinSubsequence st

( ss = q1 \/ ((len p1) Shift q2) & (Seq q1) ^ (Seq q2) = Seq ss )

proof end;

theorem :: PNPROC_1:80

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;

begin

definition
end;

:: deftheorem defines NeutralProcess PNPROC_1:def 15 :

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 16 :

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:81

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:82

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:83

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;