:: PNPROC_1 semantic presentation

theorem Th1: :: PNPROC_1:1

for b₁ being Nat
for b₂ being set st b₁ > 0 holds
{[b₁,b₂]} is FinSubsequence

proof end;

Lemma2: for b₁ being FinSubsequence st Seq b₁ = {} holds
b₁ = {}

proof end;

theorem Th2: :: PNPROC_1:2

for b₁ being FinSubsequence holds
( b₁ = {} iff Seq b₁ = {} )

proof end;

theorem Th3: :: PNPROC_1:3

for b₁ being Nat
for b₂ being set
for b₃ being FinSubsequence st b₃ = {[b₁,b₂]} holds
Seq b₃ = <*b₂*>

proof end;

registration

cluster -> finite set ;
coherence

proof end;

end;

theorem Th4: :: PNPROC_1:4

for b₁ being set
for b₂ being FinSubsequence st Seq b₂ = <*b₁*> holds
ex b₃ being Nat st b₂ = {[b₃,b₁]}

proof end;

theorem Th5: :: PNPROC_1:5

for b₁, b₂, b₃, b₄ being set holds
( not {[b₁,b₂],[b₃,b₄]} is FinSequence or ( b₁ = 1 & b₃ = 1 & b₂ = b₄ ) or ( b₁ = 1 & b₃ = 2 ) or ( b₁ = 2 & b₃ = 1 ) )

proof end;

theorem Th6: :: PNPROC_1:6

for b₁, b₂ being set holds <*b₁,b₂*> = {[1,b₁],[2,b₂]}

proof end;

Lemma8: for b₁, b₂, b₃ being Nat st ( ( 1 <= b₁ & b₁ <= b₃ ) or ( b₃ + 1 <= b₁ & b₁ <= b₃ + b₂ ) ) holds
( 1 <= b₁ & b₁ <= b₃ + b₂ )

proof end;

theorem Th7: :: PNPROC_1:7

for b₁ being FinSubsequence holds Card b₁ = len (Seq b₁)

proof end;

Lemma10: for b₁, b₂ being set holds
( ( for b₃ being set st b₃ in b₁ holds
not b₃ in b₂ ) iff b₁ misses b₂ )

proof end;

theorem Th8: :: PNPROC_1:8

for b₁, b₂ being Relation st dom b₁ misses dom b₂ holds
b₁ misses b₂

proof end;

theorem Th9: :: PNPROC_1:9

for b₁, b₂ being set
for b₃, b₄ being Relation st b₁ misses b₂ holds
b₃ | b₁ misses b₄ | b₂

proof end;

Lemma13: for b₁ being FinSubsequence holds dom (Seq b₁) = dom (Sgm (dom b₁))

proof end;

Lemma14: for b₁ being FinSubsequence holds rng b₁ = rng (Seq b₁)

proof end;

theorem Th10: :: PNPROC_1:10

for b₁, b₂, b₃ being Function st b₁ c= b₃ & b₂ c= b₃ & b₁ misses b₂ holds
dom b₁ misses dom b₂

proof end;

theorem Th11: :: PNPROC_1:11

for b₁ being set
for b₂ being Relation holds b₁ | b₂ c= b₂ | (b₂ " b₁)

proof end;

theorem Th12: :: PNPROC_1:12

for b₁ being set
for b₂ being Function holds b₁ | b₂ = b₂ | (b₂ " b₁)

proof end;

definition

let c₁ be set ;
mode marking of c₁ -> Function means :Def1: :: PNPROC_1:def 1
( dom a₂ = a₁ & rng a₂ c= NAT );
existence

proof end;

end;

:: deftheorem Def1 defines marking PNPROC_1:def 1 :

notation

let c₁ be set ;
let c₂ be marking of c₁;
let c₃ be set ;
synonym c₂ multitude_of c₃ for c₁ . c₂;

end;

definition

let c₁ be set ;
let c₂ be marking of c₁;
let c₃ be set ;
redefine func multitude_of as c₂ multitude_of c₃ -> Nat;
coherence

proof end;

redefine func multitude_of as c₂ . c₃ -> Nat;
coherence

proof end;

end;

scheme :: PNPROC_1:sch 1
s1{ F₁() -> set , F₂( set ) -> Nat } :

ex b₁ being marking of F₁() st
for b₂ being set st b₂ in F₁() holds
b₁ multitude_of b₂ = F₂(b₂)

proof end;

definition

let c₁ be set ;
let c₂, c₃ be marking of c₁;
redefine pred = as c₂ = c₃ means :: PNPROC_1:def 2
for b₁ being set st b₁ in a₁ holds
a₂ multitude_of b₁ = a₃ multitude_of b₁;
compatibility

proof end;

end;

:: deftheorem Def2 defines = PNPROC_1:def 2 :

definition

let c₁ be set ;
func {$} c₁ -> marking of a₁ equals :: PNPROC_1:def 3
a₁ --> 0;
coherence

proof end;

end;

:: deftheorem Def3 defines {$} PNPROC_1:def 3 :

definition

let c₁ be set ;
let c₂, c₃ be marking of c₁;
pred c₂ c= c₃ means :Def4: :: PNPROC_1:def 4
for b₁ being set st b₁ in a₁ holds
a₂ multitude_of b₁ <= a₃ multitude_of b₁;
reflexivity ;

end;

:: deftheorem Def4 defines c= PNPROC_1:def 4 :

Lemma19: for b₁, b₂ being set st b₁ in b₂ holds
({$} b₂) multitude_of b₁ = 0

proof end;

theorem Th13: :: PNPROC_1:13

for b₁ being set
for b₂ being marking of b₁ holds {$} b₁ c= b₂

proof end;

theorem Th14: :: PNPROC_1:14

for b₁ being set
for b₂, b₃, b₄ being marking of b₁ st b₂ c= b₃ & b₃ c= b₄ holds
b₂ c= b₄

proof end;

definition

let c₁ be set ;
let c₂, c₃ be marking of c₁;
func c₂ + c₃ -> marking of a₁ means :Def5: :: PNPROC_1:def 5
for b₁ being set st b₁ in a₁ holds
a₄ multitude_of b₁ = (a₂ multitude_of b₁) + (a₃ multitude_of b₁);
existence

proof end;

uniqueness

proof end;

commutativity ;

end;

:: deftheorem Def5 defines + PNPROC_1:def 5 :

theorem Th15: :: PNPROC_1:15

for b₁ being set
for b₂ being marking of b₁ holds b₂ + ({$} b₁) = b₂

proof end;

definition

let c₁ be set ;
let c₂, c₃ be marking of c₁;
assume E23: c₃ c= c₂ ;
func c₂ - c₃ -> marking of a₁ means :Def6: :: PNPROC_1:def 6
for b₁ being set st b₁ in a₁ holds
a₄ multitude_of b₁ = (a₂ multitude_of b₁) - (a₃ multitude_of b₁);
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def6 defines - PNPROC_1:def 6 :

theorem Th16: :: PNPROC_1:16

for b₁ being set
for b₂, b₃ being marking of b₁ holds b₂ c= b₂ + b₃

proof end;

theorem Th17: :: PNPROC_1:17

for b₁ being set
for b₂ being marking of b₁ holds b₂ - ({$} b₁) = b₂

proof end;

theorem Th18: :: PNPROC_1:18

for b₁ being set
for b₂, b₃, b₄ being marking of b₁ st b₂ c= b₃ & b₃ c= b₄ holds
b₄ - b₃ c= b₄ - b₂

proof end;

theorem Th19: :: PNPROC_1:19

for b₁ being set
for b₂, b₃ being marking of b₁ holds (b₂ + b₃) - b₃ = b₂

proof end;

theorem Th20: :: PNPROC_1:20

for b₁ being set
for b₂, b₃, b₄ being marking of b₁ st b₂ c= b₃ & b₃ c= b₄ holds
b₃ - b₂ c= b₄ - b₂

proof end;

theorem Th21: :: PNPROC_1:21

for b₁ being set
for b₂, b₃, b₄ being marking of b₁ st b₂ c= b₃ holds
(b₃ + b₄) - b₂ = (b₃ - b₂) + b₄

proof end;

theorem Th22: :: PNPROC_1:22

for b₁ being set
for b₂, b₃ being marking of b₁ st b₂ c= b₃ & b₃ c= b₂ holds
b₂ = b₃

proof end;

theorem Th23: :: PNPROC_1:23

for b₁ being set
for b₂, b₃, b₄ being marking of b₁ holds (b₂ + b₃) + b₄ = b₂ + (b₃ + b₄)

proof end;

theorem Th24: :: PNPROC_1:24

for b₁ being set
for b₂, b₃, b₄, b₅ being marking of b₁ st b₂ c= b₃ & b₄ c= b₅ holds
b₂ + b₄ c= b₃ + b₅

proof end;

theorem Th25: :: PNPROC_1:25

for b₁ being set
for b₂, b₃ being marking of b₁ st b₂ c= b₃ holds
b₃ - b₂ c= b₃

proof end;

theorem Th26: :: PNPROC_1:26

for b₁ being set
for b₂, b₃, b₄, b₅ being marking of b₁ st b₂ c= b₃ & b₄ c= b₅ & b₅ c= b₂ holds
b₂ - b₅ c= b₃ - b₄

proof end;

theorem Th27: :: PNPROC_1:27

for b₁ being set
for b₂, b₃ being marking of b₁ st b₂ c= b₃ holds
b₃ = (b₃ - b₂) + b₂

proof end;

theorem Th28: :: PNPROC_1:28

for b₁ being set
for b₂, b₃ being marking of b₁ holds (b₂ + b₃) - b₂ = b₃

proof end;

theorem Th29: :: PNPROC_1:29

for b₁ being set
for b₂, b₃, b₄ being marking of b₁ st b₂ + b₃ c= b₄ holds
(b₄ - b₂) - b₃ = b₄ - (b₂ + b₃)

proof end;

theorem Th30: :: PNPROC_1:30

for b₁ being set
for b₂, b₃, b₄ being marking of b₁ st b₂ c= b₃ & b₃ c= b₄ holds
b₄ - (b₃ - b₂) = (b₄ - b₃) + b₂

proof end;

theorem Th31: :: PNPROC_1:31

for b₁ being set
for b₂ being marking of b₁ holds b₂ in Funcs b₁,NAT

proof end;

theorem Th32: :: PNPROC_1:32

for b₁, b₂ being set st b₁ in Funcs b₂,NAT holds
b₁ is marking of b₂

proof end;

definition

let c₁ be set ;
mode transition of c₁ -> set means :Def7: :: PNPROC_1:def 7
ex b₁, b₂ being marking of a₁ st a₂ = [b₁,b₂];
existence

proof end;

end;

:: deftheorem Def7 defines transition PNPROC_1:def 7 :

notation

let c₁ be set ;
let c₂ be transition of c₁;
synonym Pre c₂ for c₁ `1 ;
synonym Post c₂ for c₁ `2 ;

end;

definition

let c₁ be set ;
let c₂ be transition of c₁;
redefine func Pre as Pre c₂ -> marking of a₁;
coherence

proof end;

redefine func Post as Post c₂ -> marking of a₁;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be marking of c₁;
let c₃ be transition of c₁;
func fire c₃,c₂ -> marking of a₁ equals :Def8: :: PNPROC_1:def 8
(a₂ - (Pre a₃)) + (Post a₃) if Pre a₃ c= a₂
otherwise a₂;
coherence ;
consistency ;

end;

:: deftheorem Def8 defines fire PNPROC_1:def 8 :

theorem Th33: :: PNPROC_1:33

for b₁ being set
for b₂ being marking of b₁
for b₃, b₄ being transition of b₁ st (Pre b₃) + (Pre b₄) c= b₂ holds
fire b₄,(fire b₃,b₂) = (((b₂ - (Pre b₃)) - (Pre b₄)) + (Post b₃)) + (Post b₄)

proof end;

definition

let c₁ be set ;
let c₂ be transition of c₁;
func fire c₂ -> Function means :Def9: :: PNPROC_1:def 9
( dom a₃ = Funcs a₁,NAT & ( for b₁ being marking of a₁ holds a₃ . b₁ = fire a₂,b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def9 defines fire PNPROC_1:def 9 :

theorem Th34: :: PNPROC_1:34

for b₁ being set
for b₂ being transition of b₁ holds rng (fire b₂) c= Funcs b₁,NAT

proof end;

theorem Th35: :: PNPROC_1:35

for b₁ being set
for b₂ being marking of b₁
for b₃, b₄ being transition of b₁ holds fire b₃,(fire b₄,b₂) = ((fire b₃) * (fire b₄)) . b₂

proof end;

definition

let c₁ be set ;
mode Petri_net of c₁ -> non empty set means :Def10: :: PNPROC_1:def 10
for b₁ being set st b₁ in a₂ holds
b₁ is transition of a₁;
existence

proof end;

end;

:: deftheorem Def10 defines Petri_net PNPROC_1:def 10 :

definition

let c₁ be set ;
let c₂ be Petri_net of c₁;
redefine mode Element as Element of c₂ -> transition of a₁;
coherence by Def10;

end;

definition

let c₁ be set ;
let c₂ be Petri_net of c₁;
mode firing-sequence of a₂ is Element of a₂ * ;

end;

definition

let c₁ be set ;
let c₂ be Petri_net of c₁;
let c₃ be firing-sequence of c₂;
func fire c₃ -> Function means :Def11: :: PNPROC_1:def 11
ex b₁ being Function-yielding FinSequence st
( a₄ = compose b₁,(Funcs a₁,NAT ) & len b₁ = len a₃ & ( for b₂ being Nat st b₂ in dom a₃ holds
b₁ . b₂ = fire (a₃ /. b₂) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines fire PNPROC_1:def 11 :

theorem Th36: :: PNPROC_1:36

for b₁ being set
for b₂ being Petri_net of b₁ holds fire (<*> b₂) = id (Funcs b₁,NAT )

proof end;

theorem Th37: :: PNPROC_1:37

for b₁ being set
for b₂ being Petri_net of b₁
for b₃ being Element of b₂ holds fire <*b₃*> = fire b₃

proof end;

theorem Th38: :: PNPROC_1:38

for b₁ being set
for b₂ being Petri_net of b₁
for b₃ being Element of b₂ holds (fire b₃) * (id (Funcs b₁,NAT )) = fire b₃

proof end;

theorem Th39: :: PNPROC_1:39

for b₁ being set
for b₂ being Petri_net of b₁
for b₃, b₄ being Element of b₂ holds fire <*b₃,b₄*> = (fire b₄) * (fire b₃)

proof end;

theorem Th40: :: PNPROC_1:40

for b₁ being set
for b₂ being Petri_net of b₁
for b₃ being firing-sequence of b₂ holds
( dom (fire b₃) = Funcs b₁,NAT & rng (fire b₃) c= Funcs b₁,NAT )

proof end;

theorem Th41: :: PNPROC_1:41

for b₁ being set
for b₂ being Petri_net of b₁
for b₃, b₄ being firing-sequence of b₂ holds fire (b₃ ^ b₄) = (fire b₄) * (fire b₃)

proof end;

theorem Th42: :: PNPROC_1:42

for b₁ being set
for b₂ being Petri_net of b₁
for b₃ being Element of b₂
for b₄ being firing-sequence of b₂ holds fire (b₄ ^ <*b₃*>) = (fire b₃) * (fire b₄)

proof end;

definition

let c₁ be set ;
let c₂ be Petri_net of c₁;
let c₃ be firing-sequence of c₂;
let c₄ be marking of c₁;
func fire c₃,c₄ -> marking of a₁ equals :: PNPROC_1:def 12
(fire a₃) . a₄;
coherence

proof end;

end;

:: deftheorem Def12 defines fire PNPROC_1:def 12 :

definition

let c₁ be set ;
let c₂ be Petri_net of c₁;
mode process of a₂ is Subset of (a₂ * );

end;

registration

cluster FinSequence-like -> finite FinSubsequence-like set ;
coherence by FINSEQ_1:68;

end;

definition

let c₁ be set ;
let c₂ be Petri_net of c₁;
let c₃, c₄ be process of c₂;
func c₃ before c₄ -> process of a₂ equals :: PNPROC_1:def 13
{ (b₁ ^ b₂) where B is firing-sequence of a₂, B is firing-sequence of a₂ : ( b₁ in a₃ & b₂ in a₄ ) } ;
coherence

proof end;

end;

:: deftheorem Def13 defines before PNPROC_1:def 13 :

registration

let c₁ be set ;
let c₂ be Petri_net of c₁;
let c₃, c₄ be non empty process of c₂;
cluster a₃ before a₄ -> non empty ;
coherence

proof end;

end;

theorem Th43: :: PNPROC_1:43

for b₁ being set
for b₂ being Petri_net of b₁
for b₃, b₄, b₅ being process of b₂ holds (b₃ \/ b₄) before b₅ = (b₃ before b₅) \/ (b₄ before b₅)

proof end;

theorem Th44: :: PNPROC_1:44

for b₁ being set
for b₂ being Petri_net of b₁
for b₃, b₄, b₅ being process of b₂ holds b₃ before (b₄ \/ b₅) = (b₃ before b₄) \/ (b₃ before b₅)

proof end;

theorem Th45: :: PNPROC_1:45

for b₁ being set
for b₂ being Petri_net of b₁
for b₃, b₄ being firing-sequence of b₂ holds {b₃} before {b₄} = {(b₃ ^ b₄)}

proof end;

theorem Th46: :: PNPROC_1:46

for b₁ being set
for b₂ being Petri_net of b₁
for b₃, b₄, b₅ being firing-sequence of b₂ holds {b₃,b₄} before {b₅} = {(b₃ ^ b₅),(b₄ ^ b₅)}

proof end;

theorem Th47: :: PNPROC_1:47

for b₁ being set
for b₂ being Petri_net of b₁
for b₃, b₄, b₅ being firing-sequence of b₂ holds {b₃} before {b₄,b₅} = {(b₃ ^ b₄),(b₃ ^ b₅)}

proof end;

definition

let c₁ be set ;
let c₂ be Petri_net of c₁;
let c₃, c₄ be process of c₂;
func c₃ concur c₄ -> process of a₂ equals :: PNPROC_1:def 14
{ b₁ where B is firing-sequence of a₂ : ex b₁, b₂ being FinSubsequence st
( b₁ = b₂ \/ b₃ & b₂ misses b₃ & Seq b₂ in a₃ & Seq b₃ in a₄ ) } ;
coherence

proof end;

commutativity

proof end;

end;

:: deftheorem Def14 defines concur PNPROC_1:def 14 :

theorem Th48: :: PNPROC_1:48

for b₁ being set
for b₂ being Petri_net of b₁
for b₃, b₄, b₅ being process of b₂ holds (b₃ \/ b₄) concur b₅ = (b₃ concur b₅) \/ (b₄ concur b₅)

proof end;

theorem Th49: :: PNPROC_1:49

for b₁ being set
for b₂ being Petri_net of b₁
for b₃, b₄ being Element of b₂ holds {<*b₃*>} concur {<*b₄*>} = {<*b₃,b₄*>,<*b₄,b₃*>}

proof end;

theorem Th50: :: PNPROC_1:50

for b₁ being set
for b₂ being Petri_net of b₁
for b₃, b₄, b₅ being Element of b₂ holds {<*b₃*>,<*b₄*>} concur {<*b₅*>} = {<*b₃,b₅*>,<*b₄,b₅*>,<*b₅,b₃*>,<*b₅,b₄*>}

proof end;

theorem Th51: :: PNPROC_1:51

for b₁ being set
for b₂ being Petri_net of b₁
for b₃, b₄, b₅ being process of b₂ holds (b₃ before b₄) before b₅ = b₃ before (b₄ before b₅)

proof end;

definition

let c₁ be FinSubsequence;
let c₂ be Nat;
set c₃ = { (c₂ + b₁) where B is Nat : b₁ in dom c₁ } ;
func c₂ Shift c₁ -> FinSubsequence means :Def15: :: PNPROC_1:def 15
( dom a₃ = { (a₂ + b₁) where B is Nat : b₁ in dom a₁ } & ( for b₁ being Nat st b₁ in dom a₁ holds
a₃ . (a₂ + b₁) = a₁ . b₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def15 defines Shift PNPROC_1:def 15 :

theorem Th52: :: PNPROC_1:52

for b₁ being FinSubsequence holds 0 Shift b₁ = b₁

proof end;

theorem Th53: :: PNPROC_1:53

for b₁, b₂ being Nat
for b₃ being FinSubsequence holds (b₁ + b₂) Shift b₃ = b₁ Shift (b₂ Shift b₃)

proof end;

theorem Th54: :: PNPROC_1:54

for b₁ being Nat
for b₂ being FinSequence st b₂ <> {} holds
dom (b₁ Shift b₂) = { b₃ where B is Nat : ( b₁ + 1 <= b₃ & b₃ <= b₁ + (len b₂) ) }

proof end;

theorem Th55: :: PNPROC_1:55

for b₁ being Nat
for b₂ being FinSubsequence holds
( b₂ = {} iff b₁ Shift b₂ = {} )

proof end;

theorem Th56: :: PNPROC_1:56

for b₁ being Nat
for b₂ being FinSubsequence ex b₃ being FinSubsequence st
( dom b₃ = dom b₂ & rng b₃ = dom (b₁ Shift b₂) & ( for b₄ being Nat st b₄ in dom b₂ holds
b₃ . b₄ = b₁ + b₄ ) & b₃ is one-to-one )

proof end;

Lemma55: for b₁ being Nat
for b₂ being FinSequence ex b₃ being FinSequence st
( dom b₃ = dom b₂ & rng b₃ = dom (b₁ Shift b₂) & ( for b₄ being Nat st b₄ in dom b₂ holds
b₃ . b₄ = b₁ + b₄ ) & b₃ is one-to-one )

proof end;

theorem Th57: :: PNPROC_1:57

for b₁ being Nat
for b₂ being FinSubsequence holds Card b₂ = Card (b₁ Shift b₂)

proof end;

theorem Th58: :: PNPROC_1:58

for b₁ being Nat
for b₂ being FinSequence holds dom b₂ = dom (Seq (b₁ Shift b₂))

proof end;

theorem Th59: :: PNPROC_1:59

for b₁, b₂ being Nat
for b₃ being FinSequence st b₁ in dom b₃ holds
(Sgm (dom (b₂ Shift b₃))) . b₁ = b₂ + b₁

proof end;

theorem Th60: :: PNPROC_1:60

for b₁, b₂ being Nat
for b₃ being FinSequence st b₁ in dom b₃ holds
(Seq (b₂ Shift b₃)) . b₁ = b₃ . b₁

proof end;

theorem Th61: :: PNPROC_1:61

for b₁ being Nat
for b₂ being FinSequence holds Seq (b₁ Shift b₂) = b₂

proof end;

theorem Th62: :: PNPROC_1:62

for b₁, b₂ being FinSequence holds dom (b₁ \/ ((len b₁) Shift b₂)) = Seg ((len b₁) + (len b₂))

proof end;

theorem Th63: :: PNPROC_1:63

for b₁ being Nat
for b₂ being FinSequence
for b₃ being FinSubsequence st len b₂ <= b₁ holds
dom b₂ misses dom (b₁ Shift b₃)

proof end;

theorem Th64: :: PNPROC_1:64

for b₁, b₂ being FinSequence holds b₁ ^ b₂ = b₁ \/ ((len b₁) Shift b₂)

proof end;

theorem Th65: :: PNPROC_1:65

for b₁ being Nat
for b₂ being FinSequence
for b₃ being FinSubsequence st b₁ >= len b₂ holds
b₂ misses b₁ Shift b₃

proof end;

theorem Th66: :: PNPROC_1:66

for b₁ being set
for b₂ being Petri_net of b₁
for b₃, b₄, b₅ being process of b₂ holds (b₃ concur b₄) concur b₅ = b₃ concur (b₄ concur b₅)

proof end;

theorem Th67: :: PNPROC_1:67

for b₁ being set
for b₂ being Petri_net of b₁
for b₃, b₄ being process of b₂ holds b₃ before b₄ c= b₃ concur b₄

proof end;

theorem Th68: :: PNPROC_1:68

for b₁ being set
for b₂ being Petri_net of b₁
for b₃, b₄, b₅, b₆ being process of b₂ st b₃ c= b₄ & b₅ c= b₆ holds
b₃ before b₅ c= b₄ before b₆

proof end;

theorem Th69: :: PNPROC_1:69

for b₁ being set
for b₂ being Petri_net of b₁
for b₃, b₄, b₅, b₆ being process of b₂ st b₃ c= b₄ & b₅ c= b₆ holds
b₃ concur b₅ c= b₄ concur b₆

proof end;

Lemma65: for b₁, b₂ being FinSequence
for b₃, b₄ being FinSubsequence st b₃ c= b₁ & b₄ c= b₂ holds
dom (b₃ \/ ((len b₁) Shift b₄)) c= dom (b₁ ^ b₂)

proof end;

Lemma66: for b₁ being FinSequence
for b₂, b₃ being FinSubsequence st b₂ c= b₁ holds
b₂ misses (len b₁) Shift b₃

proof end;

Lemma67: for b₁ being Nat
for b₂, b₃ being FinSubsequence st b₃ c= b₂ holds
dom (b₁ Shift b₃) c= dom (b₁ Shift b₂)

proof end;

theorem Th70: :: PNPROC_1:70

for b₁ being Nat
for b₂, b₃ being FinSubsequence st b₃ c= b₂ holds
b₁ Shift b₃ c= b₁ Shift b₂

proof end;

theorem Th71: :: PNPROC_1:71

for b₁, b₂ being FinSequence holds (len b₁) Shift b₂ c= b₁ ^ b₂

proof end;

theorem Th72: :: PNPROC_1:72

for b₁ being Nat
for b₂, b₃ being FinSubsequence st dom b₂ misses dom b₃ holds
dom (b₁ Shift b₂) misses dom (b₁ Shift b₃)

proof end;

theorem Th73: :: PNPROC_1:73

for b₁ being Nat
for b₂, b₃, b₄ being FinSubsequence st b₂ = b₃ \/ b₄ & b₃ misses b₄ holds
(b₁ Shift b₃) \/ (b₁ Shift b₄) = b₁ Shift b₂

proof end;

theorem Th74: :: PNPROC_1:74

for b₁ being Nat
for b₂ being FinSubsequence holds dom (Seq b₂) = dom (Seq (b₁ Shift b₂))

proof end;

theorem Th75: :: PNPROC_1:75

for b₁, b₂ being Nat
for b₃ being FinSubsequence st b₁ in dom (Seq b₃) holds
ex b₄ being Nat st
( b₄ = (Sgm (dom b₃)) . b₁ & (Sgm (dom (b₂ Shift b₃))) . b₁ = b₂ + b₄ )

proof end;

theorem Th76: :: PNPROC_1:76

for b₁, b₂ being Nat
for b₃ being FinSubsequence st b₁ in dom (Seq b₃) holds
(Seq (b₂ Shift b₃)) . b₁ = (Seq b₃) . b₁

proof end;

theorem Th77: :: PNPROC_1:77

for b₁ being Nat
for b₂ being FinSubsequence holds Seq b₂ = Seq (b₁ Shift b₂)

proof end;

theorem Th78: :: PNPROC_1:78

for b₁, b₂ being Nat
for b₃ being FinSubsequence st dom b₃ c= Seg b₁ holds
dom (b₂ Shift b₃) c= Seg (b₂ + b₁)

proof end;

theorem Th79: :: PNPROC_1:79

for b₁ being FinSequence
for b₂, b₃ being FinSubsequence st b₂ c= b₁ holds
ex b₄ being FinSubsequence st b₄ = b₂ \/ ((len b₁) Shift b₃)

proof end;

Lemma78: for b₁, b₂ being FinSequence
for b₃, b₄ being FinSubsequence st b₄ <> {} & b₃ c= b₁ & b₄ c= b₂ holds
Sgm ((dom b₃) \/ (dom ((len b₁) Shift b₄))) = (Sgm (dom b₃)) ^ (Sgm (dom ((len b₁) Shift b₄)))

proof end;

theorem Th80: :: PNPROC_1:80

for b₁, b₂ being FinSequence
for b₃, b₄ being FinSubsequence st b₃ c= b₁ & b₄ c= b₂ holds
ex b₅ being FinSubsequence st
( b₅ = b₃ \/ ((len b₁) Shift b₄) & dom (Seq b₅) = Seg ((len (Seq b₃)) + (len (Seq b₄))) )

proof end;

theorem Th81: :: PNPROC_1:81

proof end;

theorem Th82: :: PNPROC_1:82

for b₁, b₂ being FinSequence
for b₃, b₄ being FinSubsequence st b₃ c= b₁ & b₄ c= b₂ holds
ex b₅ being FinSubsequence st
( b₅ = b₃ \/ ((len b₁) Shift b₄) & (Seq b₃) ^ (Seq b₄) = Seq b₅ )

proof end;

theorem Th83: :: PNPROC_1:83

for b₁ being set
for b₂ being Petri_net of b₁
for b₃, b₄, b₅, b₆ being process of b₂ holds (b₃ concur b₄) before (b₅ concur b₆) c= (b₃ before b₅) concur (b₄ before b₆)

proof end;

registration

let c₁ be set ;
let c₂ be Petri_net of c₁;
let c₃, c₄ be non empty process of c₂;
cluster a₃ concur a₄ -> non empty ;
coherence

proof end;

end;

definition

let c₁ be set ;
let c₂ be Petri_net of c₁;
func NeutralProcess c₂ -> non empty process of a₂ equals :: PNPROC_1:def 16
{(<*> a₂)};
coherence ;

end;

:: deftheorem Def16 defines NeutralProcess PNPROC_1:def 16 :

definition

let c₁ be set ;
let c₂ be Petri_net of c₁;
let c₃ be Element of c₂;
func ElementaryProcess c₃ -> non empty process of a₂ equals :: PNPROC_1:def 17
{<*a₃*>};
coherence ;

end;

:: deftheorem Def17 defines ElementaryProcess PNPROC_1:def 17 :

theorem Th84: :: PNPROC_1:84

for b₁ being set
for b₂ being Petri_net of b₁
for b₃ being process of b₂ holds (NeutralProcess b₂) before b₃ = b₃

proof end;

theorem Th85: :: PNPROC_1:85

for b₁ being set
for b₂ being Petri_net of b₁
for b₃ being process of b₂ holds b₃ before (NeutralProcess b₂) = b₃

proof end;

theorem Th86: :: PNPROC_1:86

for b₁ being set
for b₂ being Petri_net of b₁
for b₃ being process of b₂ holds (NeutralProcess b₂) concur b₃ = b₃

proof end;