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 Def2 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 Def6 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 Def7 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 :
Def8:
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 :
Def9:
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 Def8 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 Def9 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 Def10 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 Def11 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 :
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 = 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 :
Def16:
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 Def15 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 Def16 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