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

definition
attr c1 is strict;
struct Net -> ;
aggr Net(# Places, Transitions, Flow #) -> Net ;
sel Places c1 -> set ;
sel Transitions c1 -> set ;
sel Flow c1 -> Relation;
end;

definition
let N be Net ;
attr N is Petri means :Def1: :: NET_1:def 1
( the Places of N misses the Transitions of N & the Flow of N c= [:the Places of N,the Transitions of N:] \/ [:the Transitions of N,the Places of N:] );
end;

:: deftheorem Def1 defines Petri NET_1:def 1 :
for N being Net holds
( N is Petri iff ( the Places of N misses the Transitions of N & the Flow of N c= [:the Places of N,the Transitions of N:] \/ [:the Transitions of N,the Places of N:] ) );

notation
let N be Net ;
synonym N is_Petri_net for Petri N;
end;

definition
let N be Net ;
func Elements N -> set equals :: NET_1:def 2
the Places of N \/ the Transitions of N;
correctness
coherence
the Places of N \/ the Transitions of N is set ;
;
end;

:: deftheorem defines Elements NET_1:def 2 :
for N being Net holds Elements N = the Places of N \/ the Transitions of N;

theorem :: NET_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: NET_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem :: NET_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th4: :: NET_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Net holds the Places of N c= Elements N by XBOOLE_1:7;

theorem Th5: :: NET_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Net holds the Transitions of N c= Elements N by XBOOLE_1:7;

theorem Th6: :: NET_1:6  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 N being Net holds
( x in Elements N iff ( x in the Places of N or x in the Transitions of N ) ) by XBOOLE_0:def 2;

theorem :: NET_1:7  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 N being Net holds
( not Elements N <> {} or not x is Element of Elements N or x is Element of the Places of N or x is Element of the Transitions of N ) by Th6;

theorem :: NET_1:8  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 N being Net st x is Element of the Places of N & the Places of N <> {} holds
x is Element of Elements N
proof end;

theorem :: NET_1:9  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 N being Net st x is Element of the Transitions of N & the Transitions of N <> {} holds
x is Element of Elements N
proof end;

Lm1: Net(# {} ,{} ,{} #) is_Petri_net
proof end;

registration
cluster Net(# {} ,{} ,{} #) -> Petri ;
coherence
Net(# {} ,{} ,{} #) is Petri by Lm1;
end;

registration
cluster strict Petri Net ;
existence
ex b1 being Net st
( b1 is strict & b1 is Petri )
proof end;
end;

definition
mode Pnet is Petri Net ;
end;

theorem :: NET_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th11: :: NET_1:11  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 N being Pnet holds
( not x in the Places of N or not x in the Transitions of N )
proof end;

theorem Th12: :: NET_1:12  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 N being Pnet st [x,y] in the Flow of N & x in the Transitions of N holds
y in the Places of N
proof end;

theorem Th13: :: NET_1:13  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 N being Pnet st [x,y] in the Flow of N & y in the Transitions of N holds
x in the Places of N
proof end;

theorem :: NET_1:14  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 N being Pnet st [x,y] in the Flow of N & x in the Places of N holds
y in the Transitions of N
proof end;

theorem :: NET_1:15  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 N being Pnet st [x,y] in the Flow of N & y in the Places of N holds
x in the Transitions of N
proof end;

definition
let N be Pnet;
let x, y be set ;
canceled;
canceled;
pred pre N,x,y means :Def5: :: NET_1:def 5
( [y,x] in the Flow of N & x in the Transitions of N );
pred post N,x,y means :Def6: :: NET_1:def 6
( [x,y] in the Flow of N & x in the Transitions of N );
end;

:: deftheorem NET_1:def 3 :
canceled;

:: deftheorem NET_1:def 4 :
canceled;

:: deftheorem Def5 defines pre NET_1:def 5 :
for N being Pnet
for x, y being set holds
( pre N,x,y iff ( [y,x] in the Flow of N & x in the Transitions of N ) );

:: deftheorem Def6 defines post NET_1:def 6 :
for N being Pnet
for x, y being set holds
( post N,x,y iff ( [x,y] in the Flow of N & x in the Transitions of N ) );

definition
let N be Net ;
let x be Element of Elements N;
func Pre N,x -> set means :Def7: :: NET_1:def 7
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 ) )
proof end;
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
proof end;
func Post N,x -> set means :Def8: :: NET_1:def 8
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 ) )
proof end;
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
proof end;
end;

:: deftheorem Def7 defines Pre NET_1:def 7 :
for N being Net
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 the Flow of N ) ) );

:: deftheorem Def8 defines Post NET_1:def 8 :
for N being Net
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 the Flow of N ) ) );

theorem Th16: :: NET_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Pnet
for x being Element of Elements N holds Pre N,x c= Elements N
proof end;

theorem :: NET_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Pnet
for x being Element of Elements N holds Pre N,x c= Elements N by Th16;

theorem Th18: :: NET_1:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Pnet
for x being Element of Elements N holds Post N,x c= Elements N
proof end;

theorem :: NET_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Pnet
for x being Element of Elements N holds Post N,x c= Elements N by Th18;

theorem :: NET_1:20  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 N being Pnet
for y being Element of Elements N st y in the Transitions of N holds
( x in Pre N,y iff pre N,y,x )
proof end;

theorem :: NET_1:21  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 N being Pnet
for y being Element of Elements N st y in the Transitions of N holds
( x in Post N,y iff post N,y,x )
proof end;

definition
let N be Pnet;
let x be Element of Elements N;
assume A1: Elements N <> {} ;
func enter N,x -> set means :Def9: :: NET_1:def 9
( ( x in the Places of N implies it = {x} ) & ( x in the Transitions of N implies it = Pre N,x ) );
existence
ex b1 being set st
( ( x in the Places of N implies b1 = {x} ) & ( x in the Transitions of N implies b1 = Pre N,x ) )
proof end;
uniqueness
for b1, b2 being set st ( x in the Places of N implies b1 = {x} ) & ( x in the Transitions of N implies b1 = Pre N,x ) & ( x in the Places of N implies b2 = {x} ) & ( x in the Transitions of N implies b2 = Pre N,x ) holds
b1 = b2 by A1, Th6;
end;

:: deftheorem Def9 defines enter NET_1:def 9 :
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 Places of N implies b3 = {x} ) & ( x in the Transitions of N implies b3 = Pre N,x ) ) );

theorem Th22: :: NET_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Pnet
for x being Element of Elements N holds
( not Elements N <> {} or enter N,x = {x} or enter N,x = Pre N,x )
proof end;

theorem Th23: :: NET_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
enter N,x c= Elements N
proof end;

theorem :: NET_1:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
enter N,x c= Elements N by Th23;

definition
let N be Pnet;
let x be Element of Elements N;
assume A1: Elements N <> {} ;
func exit N,x -> set means :Def10: :: NET_1:def 10
( ( x in the Places of N implies it = {x} ) & ( x in the Transitions of N implies it = Post N,x ) );
existence
ex b1 being set st
( ( x in the Places of N implies b1 = {x} ) & ( x in the Transitions of N implies b1 = Post N,x ) )
proof end;
uniqueness
for b1, b2 being set st ( x in the Places of N implies b1 = {x} ) & ( x in the Transitions of N implies b1 = Post N,x ) & ( x in the Places of N implies b2 = {x} ) & ( x in the Transitions of N implies b2 = Post N,x ) holds
b1 = b2 by A1, Th6;
end;

:: deftheorem Def10 defines exit 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 = exit N,x iff ( ( x in the Places of N implies b3 = {x} ) & ( x in the Transitions of N implies b3 = Post N,x ) ) );

theorem Th25: :: NET_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Pnet
for x being Element of Elements N holds
( not Elements N <> {} or exit N,x = {x} or exit N,x = Post N,x )
proof end;

theorem Th26: :: NET_1:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
exit N,x c= Elements N
proof end;

theorem :: NET_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
exit N,x c= Elements N by Th26;

definition
let N be Pnet;
let x be Element of Elements N;
func field N,x -> set equals :: NET_1:def 11
(enter N,x) \/ (exit N,x);
correctness
coherence
(enter N,x) \/ (exit N,x) is set ;
;
end;

:: deftheorem defines field NET_1:def 11 :
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 Net ;
let x be Element of the Transitions of N;
func Prec N,x -> set means :: NET_1:def 12
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 ) )
proof end;
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
proof end;
func Postc N,x -> set means :: NET_1:def 13
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 ) )
proof end;
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
proof end;
end;

:: deftheorem defines Prec NET_1:def 12 :
for N being Net
for x being Element of the Transitions of N
for b3 being set holds
( b3 = Prec N,x iff for y being set holds
( y in b3 iff ( y in the Places of N & [y,x] in the Flow of N ) ) );

:: deftheorem defines Postc NET_1:def 13 :
for N being Net
for x being Element of the Transitions of N
for b3 being set holds
( b3 = Postc N,x iff for y being set holds
( y in b3 iff ( y in the Places of N & [x,y] in the Flow of N ) ) );

definition
let N be Pnet;
let X be set ;
func Entr N,X -> set means :Def14: :: NET_1:def 14
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 ) ) )
proof end;
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
proof end;
func Ext N,X -> set means :Def15: :: NET_1:def 15
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 ) ) )
proof end;
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
proof end;
end;

:: deftheorem Def14 defines Entr NET_1:def 14 :
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 15 :
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: :: NET_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Pnet
for x being Element of Elements N
for X being set st Elements N <> {} & X c= Elements N & x in X holds
enter N,x in Entr N,X
proof end;

theorem Th29: :: NET_1:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Pnet
for x being Element of Elements N
for X being set st Elements N <> {} & X c= Elements N & x in X holds
exit N,x in Ext N,X
proof end;

definition
let N be Pnet;
let X be set ;
func Input N,X -> set equals :: NET_1:def 16
 union (Entr N,X);
correctness
coherence
union (Entr N,X) is set ;
;
func Output N,X -> set equals :: NET_1:def 17
 union (Ext N,X);
correctness
coherence
union (Ext N,X) is set ;
;
end;

:: deftheorem defines Input NET_1:def 16 :
for N being Pnet
for X being set holds Input N,X = union (Entr N,X);

:: deftheorem defines Output NET_1:def 17 :
for N being Pnet
for X being set holds Output N,X = union (Ext N,X);

theorem :: NET_1:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Pnet
for x, X being set st Elements N <> {} & X c= Elements N holds
( x in Input N,X iff ex y being Element of Elements N st
( y in X & x in enter N,y ) )
proof end;

theorem :: NET_1:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Pnet
for x, X being set st Elements N <> {} & X c= Elements N holds
( x in Output N,X iff ex y being Element of Elements N st
( y in X & x in exit N,y ) )
proof end;

theorem :: NET_1:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Pnet
for X being Subset of (Elements N)
for x being Element of Elements N st Elements N <> {} holds
( x in Input N,X iff ( ( x in X & x in the Places of N ) or ex y being Element of Elements N st
( y in X & y in the Transitions of N & pre N,y,x ) ) )
proof end;

theorem :: NET_1:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for N being Pnet
for X being Subset of (Elements N)
for x being Element of Elements N st Elements N <> {} holds
( x in Output N,X iff ( ( x in X & x in the Places of N ) or ex y being Element of Elements N st
( y in X & y in the Transitions of N & post N,y,x ) ) )
proof end;