begin
:: deftheorem Def1 defines Petri NET_1:def 1 :
:: deftheorem defines Elements NET_1:def 2 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
Lm1:
Net(# {} ,{} ,{} #) is Petri
theorem
canceled;
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem
:: deftheorem NET_1:def 3 :
canceled;
:: deftheorem NET_1:def 4 :
canceled;
:: deftheorem Def5 defines pre NET_1:def 5 :
:: deftheorem Def6 defines post NET_1:def 6 :
definition
let N be
Net ;
let x be
Element of
Elements N;
func Pre N,
x -> set means :
Def7:
for
y being
set holds
(
y in it iff (
y in Elements N &
[y,x] in the
Flow of
N ) );
existence
ex b1 being set st
for y being set holds
( y in b1 iff ( y in Elements N & [y,x] in the Flow of N ) )
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in Elements N & [y,x] in the Flow of N ) ) ) & ( for y being set holds
( y in b2 iff ( y in Elements N & [y,x] in the Flow of N ) ) ) holds
b1 = b2
func Post N,
x -> set means :
Def8:
for
y being
set holds
(
y in it iff (
y in Elements N &
[x,y] in the
Flow of
N ) );
existence
ex b1 being set st
for y being set holds
( y in b1 iff ( y in Elements N & [x,y] in the Flow of N ) )
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in Elements N & [x,y] in the Flow of N ) ) ) & ( for y being set holds
( y in b2 iff ( y in Elements N & [x,y] in the Flow of N ) ) ) holds
b1 = b2
end;
:: deftheorem Def7 defines Pre NET_1:def 7 :
:: deftheorem Def8 defines Post NET_1:def 8 :
theorem Th16:
theorem
theorem Th18:
theorem
theorem
theorem
:: deftheorem Def9 defines enter NET_1:def 9 :
theorem Th22:
theorem Th23:
theorem
:: deftheorem Def10 defines exit NET_1:def 10 :
theorem Th25:
theorem Th26:
theorem
:: deftheorem defines field NET_1:def 11 :
definition
let N be
Net ;
let x be
Element of the
Transitions of
N;
func Prec N,
x -> set means
for
y being
set holds
(
y in it iff (
y in the
Places of
N &
[y,x] in the
Flow of
N ) );
existence
ex b1 being set st
for y being set holds
( y in b1 iff ( y in the Places of N & [y,x] in the Flow of N ) )
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in the Places of N & [y,x] in the Flow of N ) ) ) & ( for y being set holds
( y in b2 iff ( y in the Places of N & [y,x] in the Flow of N ) ) ) holds
b1 = b2
func Postc N,
x -> set means
for
y being
set holds
(
y in it iff (
y in the
Places of
N &
[x,y] in the
Flow of
N ) );
existence
ex b1 being set st
for y being set holds
( y in b1 iff ( y in the Places of N & [x,y] in the Flow of N ) )
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in the Places of N & [x,y] in the Flow of N ) ) ) & ( for y being set holds
( y in b2 iff ( y in the Places of N & [x,y] in the Flow of N ) ) ) holds
b1 = b2
end;
:: deftheorem defines Prec NET_1:def 12 :
:: deftheorem defines Postc NET_1:def 13 :
definition
let N be
Pnet;
let X be
set ;
func Entr N,
X -> set means :
Def14:
for
x being
set holds
(
x in it iff (
x c= Elements N & ex
y being
Element of
Elements N st
(
y in X &
x = enter N,
y ) ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter N,y ) ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter N,y ) ) ) ) & ( for x being set holds
( x in b2 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter N,y ) ) ) ) holds
b1 = b2
func Ext N,
X -> set means :
Def15:
for
x being
set holds
(
x in it iff (
x c= Elements N & ex
y being
Element of
Elements N st
(
y in X &
x = exit N,
y ) ) );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit N,y ) ) )
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit N,y ) ) ) ) & ( for x being set holds
( x in b2 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit N,y ) ) ) ) holds
b1 = b2
end;
:: deftheorem Def14 defines Entr NET_1:def 14 :
:: deftheorem Def15 defines Ext NET_1:def 15 :
theorem Th28:
theorem Th29:
:: deftheorem defines Input NET_1:def 16 :
:: deftheorem defines Output NET_1:def 17 :
theorem
theorem
theorem
theorem