begin
:: deftheorem defines Flow NET_1:def 1 :
for P being PT_net_Str holds Flow P = the S-T_Arcs of P \/ the T-S_Arcs of P;
:: deftheorem Def1 defines Petri NET_1:def 2 :
for N being PT_net_Str holds
( N is Petri iff ( the carrier of N misses the carrier' of N & Flow N c= [:the carrier of N,the carrier' of N:] \/ [:the carrier' of N,the carrier of N:] ) );
:: deftheorem defines Elements NET_1:def 3 :
for N being PT_net_Str holds Elements N = the carrier of N \/ the carrier' of N;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
Lm1:
PT_net_Str(# {} ,{} ,({} {} ,{} ),({} {} ,{} ) #) is Petri
registration
cluster PT_net_Str(#
{} ,
{} ,
({} {} ,{} ),
({} {} ,{} ) #)
-> Petri ;
coherence
PT_net_Str(# {} ,{} ,({} {} ,{} ),({} {} ,{} ) #) is Petri
by Lm1;
end;
theorem
canceled;
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem
:: deftheorem NET_1:def 4 :
canceled;
:: deftheorem NET_1:def 5 :
canceled;
:: deftheorem Def5 defines pre NET_1:def 6 :
for N being Pnet
for x, y being set holds
( pre N,x,y iff ( [y,x] in Flow N & x in the carrier' of N ) );
:: deftheorem Def6 defines post NET_1:def 7 :
for N being Pnet
for x, y being set holds
( post N,x,y iff ( [x,y] in Flow N & x in the carrier' of N ) );
definition
let N be
PT_net_Str ;
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 Flow N ) );
existence
ex b1 being set st
for y being set holds
( y in b1 iff ( y in Elements N & [y,x] in Flow N ) )
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in Elements N & [y,x] in Flow N ) ) ) & ( for y being set holds
( y in b2 iff ( y in Elements N & [y,x] in Flow 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 Flow N ) );
existence
ex b1 being set st
for y being set holds
( y in b1 iff ( y in Elements N & [x,y] in Flow N ) )
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in Elements N & [x,y] in Flow N ) ) ) & ( for y being set holds
( y in b2 iff ( y in Elements N & [x,y] in Flow N ) ) ) holds
b1 = b2
end;
:: deftheorem Def7 defines Pre NET_1:def 8 :
for N being PT_net_Str
for x being Element of Elements N
for b3 being set holds
( b3 = Pre N,x iff for y being set holds
( y in b3 iff ( y in Elements N & [y,x] in Flow N ) ) );
:: deftheorem Def8 defines Post NET_1:def 9 :
for N being PT_net_Str
for x being Element of Elements N
for b3 being set holds
( b3 = Post N,x iff for y being set holds
( y in b3 iff ( y in Elements N & [x,y] in Flow N ) ) );
theorem Th16:
theorem
theorem Th18:
theorem
theorem
theorem
:: deftheorem Def9 defines enter NET_1:def 10 :
for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
for b3 being set holds
( b3 = enter N,x iff ( ( x in the carrier of N implies b3 = {x} ) & ( x in the carrier' of N implies b3 = Pre N,x ) ) );
theorem Th22:
theorem Th23:
theorem
:: deftheorem Def10 defines exit NET_1:def 11 :
for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
for b3 being set holds
( b3 = exit N,x iff ( ( x in the carrier of N implies b3 = {x} ) & ( x in the carrier' of N implies b3 = Post N,x ) ) );
theorem Th25:
theorem Th26:
theorem
:: deftheorem defines field NET_1:def 12 :
for N being Pnet
for x being Element of Elements N holds field N,x = (enter N,x) \/ (exit N,x);
definition
let N be
PT_net_Str ;
let x be
Element of the
carrier' of
N;
func Prec N,
x -> set means
for
y being
set holds
(
y in it iff (
y in the
carrier of
N &
[y,x] in Flow N ) );
existence
ex b1 being set st
for y being set holds
( y in b1 iff ( y in the carrier of N & [y,x] in Flow N ) )
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in the carrier of N & [y,x] in Flow N ) ) ) & ( for y being set holds
( y in b2 iff ( y in the carrier of N & [y,x] in Flow N ) ) ) holds
b1 = b2
func Postc N,
x -> set means
for
y being
set holds
(
y in it iff (
y in the
carrier of
N &
[x,y] in Flow N ) );
existence
ex b1 being set st
for y being set holds
( y in b1 iff ( y in the carrier of N & [x,y] in Flow N ) )
uniqueness
for b1, b2 being set st ( for y being set holds
( y in b1 iff ( y in the carrier of N & [x,y] in Flow N ) ) ) & ( for y being set holds
( y in b2 iff ( y in the carrier of N & [x,y] in Flow N ) ) ) holds
b1 = b2
end;
:: deftheorem defines Prec NET_1:def 13 :
for N being PT_net_Str
for x being Element of the carrier' of N
for b3 being set holds
( b3 = Prec N,x iff for y being set holds
( y in b3 iff ( y in the carrier of N & [y,x] in Flow N ) ) );
:: deftheorem defines Postc NET_1:def 14 :
for N being PT_net_Str
for x being Element of the carrier' of N
for b3 being set holds
( b3 = Postc N,x iff for y being set holds
( y in b3 iff ( y in the carrier of N & [x,y] in Flow N ) ) );
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 15 :
for N being Pnet
for X being set
for b3 being set holds
( b3 = Entr N,X iff for x being set holds
( x in b3 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = enter N,y ) ) ) );
:: deftheorem Def15 defines Ext NET_1:def 16 :
for N being Pnet
for X being set
for b3 being set holds
( b3 = Ext N,X iff for x being set holds
( x in b3 iff ( x c= Elements N & ex y being Element of Elements N st
( y in X & x = exit N,y ) ) ) );
theorem Th28:
theorem Th29:
:: deftheorem defines Input NET_1:def 17 :
for N being Pnet
for X being set holds Input N,X = union (Entr N,X);
:: deftheorem defines Output NET_1:def 18 :
for N being Pnet
for X being set holds Output N,X = union (Ext N,X);
theorem
theorem
theorem
theorem