:: PNPROC_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: PNPROC_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for x being set st i > 0 holds
{[i,x]} is FinSubsequence
proof end;

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

theorem Th2: :: PNPROC_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q being FinSubsequence holds
( q = {} iff Seq q = {} )
proof end;

theorem Th3: :: PNPROC_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for x being set
for q being FinSubsequence st q = {[i,x]} holds
Seq q = <*x*>
proof end;

registration
cluster -> finite set ;
coherence
for b1 being FinSubsequence holds b1 is finite
proof end;
end;

theorem Th4: :: PNPROC_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being set
for q being FinSubsequence st Seq q = <*x*> holds
ex i being Nat st q = {[i,x]}
proof end;

theorem Th5: :: PNPROC_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 ) )
proof end;

theorem Th6: :: PNPROC_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2 being set holds <*x1,x2*> = {[1,x1],[2,x2]}
proof end;

Lm2: for j, k, l being Nat st ( ( 1 <= j & j <= l ) or ( l + 1 <= j & j <= l + k ) ) holds
( 1 <= j & j <= l + k )
proof end;

theorem Th7: :: PNPROC_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p being FinSubsequence holds Card p = len (Seq p)
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;

theorem Th8: :: PNPROC_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P, R being Relation st dom P misses dom R holds
P misses R
proof end;

theorem Th9: :: PNPROC_1:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X, Y being set
for P, R being Relation st X misses Y holds
P | X misses R | Y
proof end;

Lm4: for q being FinSubsequence holds dom (Seq q) = dom (Sgm (dom q))
proof end;

Lm5: for q being FinSubsequence holds rng q = rng (Seq q)
proof end;

theorem Th10: :: PNPROC_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for f, g, h being Function st f c= h & g c= h & f misses g holds
dom f misses dom g
proof end;

theorem :: PNPROC_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for R being Relation holds Y | R c= R | (R " Y)
proof end;

theorem Th12: :: PNPROC_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for Y being set
for f being Function holds Y | f = f | (f " Y)
proof end;

definition
let P be set ;
mode marking of P -> Function means :Def1: :: PNPROC_1:def 1
( dom it = P & rng it c= NAT );
existence
ex b1 being Function st
( dom b1 = P & rng b1 c= NAT )
proof end;
end;

:: deftheorem Def1 defines marking PNPROC_1:def 1 :
for P being set
for b2 being Function holds
( b2 is marking of P iff ( dom b2 = P & rng b2 c= NAT ) );

notation
let P be set ;
let m be marking of P;
let p be set ;
synonym m multitude_of p for P . m;
end;

definition
let P be set ;
let m be marking of P;
let p be set ;
:: original: multitude_of
redefine func m multitude_of p -> Nat;
coherence
p multitude_of is Nat
proof end;
:: original: multitude_of
redefine func m . p -> Nat;
coherence
p multitude_of is Nat
proof end;
end;

scheme :: PNPROC_1:sch 1
MarkingLambda{ F1() -> set , F2( set ) -> Nat } :
ex m being marking of F1() st
for p being set st p in F1() holds
m multitude_of p = F2(p)
proof end;

definition
let P be set ;
let m1, m2 be marking of P;
:: original: =
redefine pred m1 = m2 means :: PNPROC_1:def 2
for p being set st p in P holds
m1 multitude_of p = m2 multitude_of p;
compatibility
( m1 = m2 iff for p being set st p in P holds
m1 multitude_of p = m2 multitude_of p )
proof end;
end;

:: deftheorem defines = PNPROC_1:def 2 :
for P being set
for m1, m2 being marking of P holds
( m1 = m2 iff for p being set st p in P holds
m1 multitude_of p = m2 multitude_of p );

definition
let P be set ;
func {$} P -> marking of P equals :: PNPROC_1:def 3
P --> 0;
coherence
P --> 0 is marking of P
proof end;
end;

:: deftheorem defines {$} PNPROC_1:def 3 :
for P being set holds {$} P = P --> 0;

definition
let P be set ;
let m1, m2 be marking of P;
pred m1 c= m2 means :Def4: :: PNPROC_1:def 4
for p being set st p in P holds
m1 multitude_of p <= m2 multitude_of p;
reflexivity
for m1 being marking of P
for p being set st p in P holds
m1 multitude_of p <= m1 multitude_of p
;
end;

:: deftheorem Def4 defines c= PNPROC_1:def 4 :
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
m1 multitude_of p <= m2 multitude_of p );

Lm6: for p, P being set st p in P holds
({$} P) multitude_of p = 0
proof end;

theorem Th13: :: PNPROC_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for m being marking of P holds {$} P c= m
proof end;

theorem Th14: :: PNPROC_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for m1, m2, m3 being marking of P st m1 c= m2 & m2 c= m3 holds
m1 c= m3
proof end;

definition
let P be set ;
let m1, m2 be marking of P;
func m1 + m2 -> marking of P means :Def5: :: PNPROC_1:def 5
for p being set st p in P holds
it multitude_of p = (m1 multitude_of p) + (m2 multitude_of p);
existence
ex b1 being marking of P st
for p being set st p in P holds
b1 multitude_of p = (m1 multitude_of p) + (m2 multitude_of p)
proof end;
uniqueness
for b1, b2 being marking of P st ( for p being set st p in P holds
b1 multitude_of p = (m1 multitude_of p) + (m2 multitude_of p) ) & ( for p being set st p in P holds
b2 multitude_of p = (m1 multitude_of p) + (m2 multitude_of p) ) holds
b1 = b2
proof end;
commutativity
for b1, m1, m2 being marking of P st ( for p being set st p in P holds
b1 multitude_of p = (m1 multitude_of p) + (m2 multitude_of p) ) holds
for p being set st p in P holds
b1 multitude_of p = (m2 multitude_of p) + (m1 multitude_of p)
;
end;

:: deftheorem Def5 defines + PNPROC_1:def 5 :
for P being set
for m1, m2, b4 being marking of P holds
( b4 = m1 + m2 iff for p being set st p in P holds
b4 multitude_of p = (m1 multitude_of p) + (m2 multitude_of p) );

theorem :: PNPROC_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for m being marking of P holds m + ({$} P) = m
proof end;

definition
let P be set ;
let m1, m2 be marking of P;
assume A1: m2 c= m1 ;
func m1 - m2 -> marking of P means :Def6: :: PNPROC_1:def 6
for p being set st p in P holds
it multitude_of p = (m1 multitude_of p) - (m2 multitude_of p);
existence
ex b1 being marking of P st
for p being set st p in P holds
b1 multitude_of p = (m1 multitude_of p) - (m2 multitude_of p)
proof end;
uniqueness
for b1, b2 being marking of P st ( for p being set st p in P holds
b1 multitude_of p = (m1 multitude_of p) - (m2 multitude_of p) ) & ( for p being set st p in P holds
b2 multitude_of p = (m1 multitude_of p) - (m2 multitude_of p) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def6 defines - PNPROC_1:def 6 :
for P being set
for m1, m2 being marking of P st m2 c= m1 holds
for b4 being marking of P holds
( b4 = m1 - m2 iff for p being set st p in P holds
b4 multitude_of p = (m1 multitude_of p) - (m2 multitude_of p) );

theorem Th16: :: PNPROC_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for m1, m2 being marking of P holds m1 c= m1 + m2
proof end;

theorem :: PNPROC_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for m being marking of P holds m - ({$} P) = m
proof end;

theorem :: PNPROC_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for m1, m2, m3 being marking of P st m1 c= m2 & m2 c= m3 holds
m3 - m2 c= m3 - m1
proof end;

theorem Th19: :: PNPROC_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for m1, m2 being marking of P holds (m1 + m2) - m2 = m1
proof end;

theorem Th20: :: PNPROC_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for m, m1, m2 being marking of P st m c= m1 & m1 c= m2 holds
m1 - m c= m2 - m
proof end;

theorem Th21: :: PNPROC_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for m1, m2, m3 being marking of P st m1 c= m2 holds
(m2 + m3) - m1 = (m2 - m1) + m3
proof end;

theorem :: PNPROC_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for m1, m2 being marking of P st m1 c= m2 & m2 c= m1 holds
m1 = m2
proof end;

theorem Th23: :: PNPROC_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for m1, m2, m3 being marking of P holds (m1 + m2) + m3 = m1 + (m2 + m3)
proof end;

theorem :: PNPROC_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: PNPROC_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for m1, m2 being marking of P st m1 c= m2 holds
m2 - m1 c= m2
proof end;

theorem Th26: :: PNPROC_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th27: :: PNPROC_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for m1, m2 being marking of P st m1 c= m2 holds
m2 = (m2 - m1) + m1
proof end;

theorem Th28: :: PNPROC_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for m1, m2 being marking of P holds (m1 + m2) - m1 = m2
proof end;

theorem Th29: :: PNPROC_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
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:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem Th31: :: PNPROC_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for m being marking of P holds m in Funcs P,NAT
proof end;

theorem Th32: :: PNPROC_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, P being set st x in Funcs P,NAT holds
x is marking of P
proof end;

definition
let P be set ;
mode transition of P -> set means :Def7: :: PNPROC_1:def 7
ex m1, m2 being marking of P st it = [m1,m2];
existence
ex b1 being set ex m1, m2 being marking of P st b1 = [m1,m2]
proof end;
end;

:: deftheorem Def7 defines transition PNPROC_1:def 7 :
for P being set
for b2 being set holds
( b2 is transition of P iff ex m1, m2 being marking of P st b2 = [m1,m2] );

notation
let P be set ;
let t be transition of P;
synonym Pre t for P `1 ;
synonym Post t for P `2 ;
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
proof end;
:: original: Post
redefine func Post t -> marking of P;
coherence
Post is marking of P
proof end;
end;

definition
let P be set ;
let m be marking of P;
let t be transition of P;
func fire t,m -> marking of P equals :Def8: :: PNPROC_1:def 8
(m - (Pre t)) + (Post t) if Pre t c= m
otherwise m;
coherence
( ( 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 b1 being marking of P holds verum
;
end;

:: deftheorem Def8 defines fire PNPROC_1:def 8 :
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:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

definition
let P be set ;
let t be transition of P;
func fire t -> Function means :Def9: :: PNPROC_1:def 9
( dom it = Funcs P,NAT & ( for m being marking of P holds it . m = fire t,m ) );
existence
ex b1 being Function st
( dom b1 = Funcs P,NAT & ( for m being marking of P holds b1 . m = fire t,m ) )
proof end;
uniqueness
for b1, b2 being Function st dom b1 = Funcs P,NAT & ( for m being marking of P holds b1 . m = fire t,m ) & dom b2 = Funcs P,NAT & ( for m being marking of P holds b2 . m = fire t,m ) holds
b1 = b2
proof end;
end;

:: deftheorem Def9 defines fire PNPROC_1:def 9 :
for P being set
for t being transition of P
for b3 being Function holds
( b3 = fire t iff ( dom b3 = Funcs P,NAT & ( for m being marking of P holds b3 . m = fire t,m ) ) );

theorem Th34: :: PNPROC_1:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for t being transition of P holds rng (fire t) c= Funcs P,NAT
proof end;

theorem :: PNPROC_1:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

definition
let P be set ;
mode Petri_net of P -> non empty set means :Def10: :: PNPROC_1:def 10
for x being set st x in it holds
x is transition of P;
existence
ex b1 being non empty set st
for x being set st x in b1 holds
x is transition of P
proof end;
end;

:: deftheorem Def10 defines Petri_net PNPROC_1:def 10 :
for P being set
for b2 being non empty set holds
( b2 is Petri_net of P iff for x being set st x in b2 holds
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 b1 being Element of N holds b1 is transition of P
by Def10;
end;

definition
let P be set ;
let N be Petri_net of P;
mode firing-sequence of N is Element of N * ;
end;

definition
let P be set ;
let N be Petri_net of P;
let C be firing-sequence of N;
func fire C -> Function means :Def11: :: PNPROC_1:def 11
ex F being Function-yielding FinSequence st
( it = compose F,(Funcs P,NAT ) & len F = len C & ( for i being Nat st i in dom C holds
F . i = fire (C /. i) ) );
existence
ex b1 being Function ex F being Function-yielding FinSequence st
( b1 = compose F,(Funcs P,NAT ) & len F = len C & ( for i being Nat st i in dom C holds
F . i = fire (C /. i) ) )
proof end;
uniqueness
for b1, b2 being Function st ex F being Function-yielding FinSequence st
( b1 = compose F,(Funcs P,NAT ) & len F = len C & ( for i being Nat st i in dom C holds
F . i = fire (C /. i) ) ) & ex F being Function-yielding FinSequence st
( b2 = compose F,(Funcs P,NAT ) & len F = len C & ( for i being Nat st i in dom C holds
F . i = fire (C /. i) ) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 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 b4 being Function holds
( b4 = fire C iff ex F being Function-yielding FinSequence st
( b4 = compose F,(Funcs P,NAT ) & len F = len C & ( for i being Nat st i in dom C holds
F . i = fire (C /. i) ) ) );

theorem :: PNPROC_1:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for N being Petri_net of P holds fire (<*> N) = id (Funcs P,NAT )
proof end;

theorem Th37: :: PNPROC_1:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for N being Petri_net of P
for e being Element of N holds fire <*e*> = fire e
proof end;

theorem Th38: :: PNPROC_1:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: PNPROC_1:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th40: :: PNPROC_1:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem Th41: :: PNPROC_1:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: PNPROC_1:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
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;
func fire C,m -> marking of P equals :: PNPROC_1:def 12
(fire C) . m;
coherence
(fire C) . m is marking of P
proof end;
end;

:: deftheorem defines fire PNPROC_1:def 12 :
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;
mode process of N is Subset of (N * );
end;

registration
cluster FinSequence-like -> finite FinSubsequence-like set ;
coherence
for b1 being Function st b1 is FinSequence-like holds
b1 is FinSubsequence-like
by FINSEQ_1:68;
end;

definition
let P be set ;
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 13
{ (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 ) } is process of N
proof end;
end;

:: deftheorem defines before PNPROC_1:def 13 :
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;
cluster R1 before R2 -> non empty ;
coherence
not R1 before R2 is empty
proof end;
end;

theorem Th43: :: PNPROC_1:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th44: :: PNPROC_1:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th45: :: PNPROC_1:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)}
proof end;

theorem :: PNPROC_1:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)}
proof end;

theorem :: PNPROC_1:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)}
proof end;

definition
let P be set ;
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 14
{ 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 )
}
is process of N
proof end;
commutativity
for b1, R1, R2 being process of N st b1 = { 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
b1 = { 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 )
}
proof end;
end;

:: deftheorem defines concur PNPROC_1:def 14 :
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 Th48: :: PNPROC_1:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem Th49: :: PNPROC_1:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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*>}
proof end;

theorem :: PNPROC_1:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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*>}
proof end;

theorem :: PNPROC_1:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

definition
let p be FinSubsequence;
let i be Nat;
set X = { (i + k) where k is Nat : k in dom p } ;
func i Shift p -> FinSubsequence means :Def15: :: PNPROC_1:def 15
( dom it = { (i + k) where k is Nat : k in dom p } & ( for j being Nat st j in dom p holds
it . (i + j) = p . j ) );
existence
ex b1 being FinSubsequence st
( dom b1 = { (i + k) where k is Nat : k in dom p } & ( for j being Nat st j in dom p holds
b1 . (i + j) = p . j ) )
proof end;
uniqueness
for b1, b2 being FinSubsequence st dom b1 = { (i + k) where k is Nat : k in dom p } & ( for j being Nat st j in dom p holds
b1 . (i + j) = p . j ) & dom b2 = { (i + k) where k is Nat : k in dom p } & ( for j being Nat st j in dom p holds
b2 . (i + j) = p . j ) holds
b1 = b2
proof end;
end;

:: deftheorem Def15 defines Shift PNPROC_1:def 15 :
for p being FinSubsequence
for i being Nat
for b3 being FinSubsequence holds
( b3 = i Shift p iff ( dom b3 = { (i + k) where k is Nat : k in dom p } & ( for j being Nat st j in dom p holds
b3 . (i + j) = p . j ) ) );

theorem Th52: :: PNPROC_1:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for q being FinSubsequence holds 0 Shift q = q
proof end;

theorem :: PNPROC_1:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i, j being Nat
for q being FinSubsequence holds (i + j) Shift q = i Shift (j Shift q)
proof end;

theorem Th54: :: PNPROC_1:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for p being FinSequence st p <> {} holds
dom (i Shift p) = { j1 where j1 is Nat : ( i + 1 <= j1 & j1 <= i + (len p) ) }
proof end;

theorem Th55: :: PNPROC_1:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for q being FinSubsequence holds
( q = {} iff i Shift q = {} )
proof end;

theorem Th56: :: PNPROC_1:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for q being FinSubsequence ex ss being FinSubsequence st
( dom ss = dom q & rng ss = dom (i Shift q) & ( for k being Nat st k in dom q holds
ss . k = i + k ) & ss is one-to-one )
proof end;

Lm7: for i being Nat
for p being FinSequence ex fs being FinSequence st
( dom fs = dom p & rng fs = dom (i Shift p) & ( for k being Nat st k in dom p holds
fs . k = i + k ) & fs is one-to-one )
proof end;

theorem Th57: :: PNPROC_1:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for q being FinSubsequence holds Card q = Card (i Shift q)
proof end;

theorem Th58: :: PNPROC_1:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for p being FinSequence holds dom p = dom (Seq (i Shift p))
proof end;

theorem Th59: :: PNPROC_1:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, i being Nat
for p being FinSequence st k in dom p holds
(Sgm (dom (i Shift p))) . k = i + k
proof end;

theorem Th60: :: PNPROC_1:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, i being Nat
for p being FinSequence st k in dom p holds
(Seq (i Shift p)) . k = p . k
proof end;

theorem Th61: :: PNPROC_1:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for p being FinSequence holds Seq (i Shift p) = p
proof end;

theorem Th62: :: PNPROC_1:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being FinSequence holds dom (p1 \/ ((len p1) Shift p2)) = Seg ((len p1) + (len p2))
proof end;

theorem Th63: :: PNPROC_1:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for p1 being FinSequence
for p2 being FinSubsequence st len p1 <= i holds
dom p1 misses dom (i Shift p2)
proof end;

theorem Th64: :: PNPROC_1:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being FinSequence holds p1 ^ p2 = p1 \/ ((len p1) Shift p2)
proof end;

theorem Th65: :: PNPROC_1:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for p1 being FinSequence
for p2 being FinSubsequence st i >= len p1 holds
p1 misses i Shift p2
proof end;

theorem :: PNPROC_1:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

theorem :: PNPROC_1:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: PNPROC_1:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

theorem :: PNPROC_1:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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
proof end;

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

Lm9: for p1 being FinSequence
for q1, q2 being FinSubsequence st q1 c= p1 holds
q1 misses (len p1) Shift q2
proof end;

Lm10: for i being Nat
for p, q being FinSubsequence st q c= p holds
dom (i Shift q) c= dom (i Shift p)
proof end;

theorem Th70: :: PNPROC_1:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for p, q being FinSubsequence st q c= p holds
i Shift q c= i Shift p
proof end;

theorem Th71: :: PNPROC_1:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for p1, p2 being FinSequence holds (len p1) Shift p2 c= p1 ^ p2
proof end;

theorem Th72: :: PNPROC_1:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for q1, q2 being FinSubsequence st dom q1 misses dom q2 holds
dom (i Shift q1) misses dom (i Shift q2)
proof end;

theorem Th73: :: PNPROC_1:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
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 Th74: :: PNPROC_1:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for q being FinSubsequence holds dom (Seq q) = dom (Seq (i Shift q))
proof end;

theorem Th75: :: PNPROC_1:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, i being Nat
for q being FinSubsequence st k in dom (Seq q) holds
ex j being Nat st
( j = (Sgm (dom q)) . k & (Sgm (dom (i Shift q))) . k = i + j )
proof end;

theorem Th76: :: PNPROC_1:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, i being Nat
for q being FinSubsequence st k in dom (Seq q) holds
(Seq (i Shift q)) . k = (Seq q) . k
proof end;

theorem Th77: :: PNPROC_1:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for i being Nat
for q being FinSubsequence holds Seq q = Seq (i Shift q)
proof end;

theorem Th78: :: PNPROC_1:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for k, i being Nat
for q being FinSubsequence st dom q c= Seg k holds
dom (i Shift q) c= Seg (i + k)
proof end;

theorem Th79: :: PNPROC_1:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

Lm11: for p1, p2 being FinSequence
for q1, q2 being FinSubsequence st q2 <> {} & 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 Th80: :: PNPROC_1:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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))) )
proof end;

theorem Th81: :: PNPROC_1:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)) )
proof end;

theorem Th82: :: PNPROC_1:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 )
proof end;

theorem :: PNPROC_1:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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)
proof end;

registration
let P be set ;
let N be Petri_net of P;
let R1, R2 be non empty process of N;
cluster R1 concur R2 -> non empty ;
coherence
not R1 concur R2 is empty
proof end;
end;

definition
let P be set ;
let N be Petri_net of P;
func NeutralProcess N -> non empty process of N equals :: PNPROC_1:def 16
{(<*> N)};
coherence
{(<*> N)} is non empty process of N
;
end;

:: deftheorem defines NeutralProcess PNPROC_1:def 16 :
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;
func ElementaryProcess t -> non empty process of N equals :: PNPROC_1:def 17
{<*t*>};
coherence
{<*t*>} is non empty process of N
;
end;

:: deftheorem defines ElementaryProcess PNPROC_1:def 17 :
for P being set
for N being Petri_net of P
for t being Element of N holds ElementaryProcess t = {<*t*>};

theorem :: PNPROC_1:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for N being Petri_net of P
for R being process of N holds (NeutralProcess N) before R = R
proof end;

theorem :: PNPROC_1:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for N being Petri_net of P
for R being process of N holds R before (NeutralProcess N) = R
proof end;

theorem :: PNPROC_1:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for P being set
for N being Petri_net of P
for R being process of N holds (NeutralProcess N) concur R = R
proof end;