:: E_SIEC semantic presentation

definition

attr c₁ is strict;
struct G_Net -> 1-sorted ;
aggr G_Net(# carrier, entrance, escape #) -> G_Net ;
sel entrance c₁ -> Relation;
sel escape c₁ -> Relation;

end;

definition

let N be 1-sorted ;
func echaos N -> set equals :: E_SIEC:def 1
the carrier of N \/ {the carrier of N};
correctness ;

end;

:: deftheorem defines echaos E_SIEC:def 1 :

definition

let IT be G_Net ;
attr IT is GG means :Def2: :: E_SIEC:def 2
( the entrance of IT c= [:the carrier of IT,the carrier of IT:] & the escape of IT c= [:the carrier of IT,the carrier of IT:] & the entrance of IT * the entrance of IT = the entrance of IT & the entrance of IT * the escape of IT = the entrance of IT & the escape of IT * the escape of IT = the escape of IT & the escape of IT * the entrance of IT = the escape of IT );

end;

:: deftheorem Def2 defines GG E_SIEC:def 2 :

registration

cluster GG G_Net ;
existence

proof end;

end;

definition

mode gg_net is GG G_Net ;

end;

definition

let IT be G_Net ;
attr IT is EE means :Def3: :: E_SIEC:def 3
( the entrance of IT * (the entrance of IT \ (id the carrier of IT)) = {} & the escape of IT * (the escape of IT \ (id the carrier of IT)) = {} );

end;

:: deftheorem Def3 defines EE E_SIEC:def 3 :

registration

cluster EE G_Net ;
existence

proof end;

end;

registration

cluster strict GG EE G_Net ;
existence

proof end;

end;

definition

mode e_net is GG EE G_Net ;

end;

theorem :: E_SIEC:1

for X being set
for R, S being Relation holds
( G_Net(# X,R,S #) is e_net iff ( R c= [:X,X:] & S c= [:X,X:] & R * R = R & R * S = R & S * S = S & S * R = S & R * (R \ (id X)) = {} & S * (S \ (id X)) = {} ) ) by Def2, Def3;

theorem Th2: :: E_SIEC:2

for X being set holds G_Net(# X,{} ,{} #) is e_net

proof end;

theorem Th3: :: E_SIEC:3

for X being set holds G_Net(# X,(id X),(id X) #) is e_net

proof end;

theorem :: E_SIEC:4

G_Net(# {} ,{} ,{} #) is e_net by Th2;

theorem :: E_SIEC:5

canceled;

theorem :: E_SIEC:6

canceled;

theorem :: E_SIEC:7

canceled;

theorem :: E_SIEC:8

for X, Y being set holds G_Net(# X,(id (X \ Y)),(id (X \ Y)) #) is e_net

proof end;

theorem :: E_SIEC:9

for N being e_net holds echaos N <> {}

proof end;

definition

func empty_e_net -> strict e_net equals :: E_SIEC:def 4
G_Net(# {} ,{} ,{} #);
correctness by Th2;

end;

:: deftheorem defines empty_e_net E_SIEC:def 4 :

definition

let X be set ;
func Tempty_e_net X -> strict e_net equals :: E_SIEC:def 5
G_Net(# X,(id X),(id X) #);
coherence by Th3;
func Pempty_e_net X -> strict e_net equals :: E_SIEC:def 6
G_Net(# X,{} ,{} #);
coherence by Th2;

end;

:: deftheorem defines Tempty_e_net E_SIEC:def 5 :

:: deftheorem defines Pempty_e_net E_SIEC:def 6 :

theorem :: E_SIEC:10

canceled;

theorem :: E_SIEC:11

for X being set holds
( the carrier of (Tempty_e_net X) = X & the entrance of (Tempty_e_net X) = id X & the escape of (Tempty_e_net X) = id X ) ;

theorem :: E_SIEC:12

for X being set holds
( the carrier of (Pempty_e_net X) = X & the entrance of (Pempty_e_net X) = {} & the escape of (Pempty_e_net X) = {} ) ;

definition

let x be set ;
func Psingle_e_net x -> strict e_net equals :: E_SIEC:def 7
G_Net(# {x},(id {x}),(id {x}) #);
coherence by Th3;
func Tsingle_e_net x -> strict e_net equals :: E_SIEC:def 8
G_Net(# {x},{} ,{} #);
coherence by Th2;

end;

:: deftheorem defines Psingle_e_net E_SIEC:def 7 :

:: deftheorem defines Tsingle_e_net E_SIEC:def 8 :

theorem :: E_SIEC:13

for x being set holds
( the carrier of (Psingle_e_net x) = {x} & the entrance of (Psingle_e_net x) = id {x} & the escape of (Psingle_e_net x) = id {x} ) ;

theorem :: E_SIEC:14

for x being set holds
( the carrier of (Tsingle_e_net x) = {x} & the entrance of (Tsingle_e_net x) = {} & the escape of (Tsingle_e_net x) = {} ) ;

theorem Th15: :: E_SIEC:15

for X, Y being set holds G_Net(# (X \/ Y),(id X),(id X) #) is e_net

proof end;

definition

let X, Y be set ;
func PTempty_e_net X,Y -> strict e_net equals :: E_SIEC:def 9
G_Net(# (X \/ Y),(id X),(id X) #);
coherence by Th15;

end;

:: deftheorem defines PTempty_e_net E_SIEC:def 9 :

theorem Th16: :: E_SIEC:16

for N being e_net holds
( the entrance of N \ (id (dom the entrance of N)) = the entrance of N \ (id the carrier of N) & the escape of N \ (id (dom the escape of N)) = the escape of N \ (id the carrier of N) & the entrance of N \ (id (rng the entrance of N)) = the entrance of N \ (id the carrier of N) & the escape of N \ (id (rng the escape of N)) = the escape of N \ (id the carrier of N) )

proof end;

theorem Th17: :: E_SIEC:17

for N being e_net holds CL the entrance of N = CL the escape of N

proof end;

theorem Th18: :: E_SIEC:18

for N being e_net holds
( rng the entrance of N = rng (CL the entrance of N) & rng the entrance of N = dom (CL the entrance of N) & rng the escape of N = rng (CL the escape of N) & rng the escape of N = dom (CL the escape of N) & rng the entrance of N = rng the escape of N )

proof end;

theorem Th19: :: E_SIEC:19

for N being e_net holds
( dom the entrance of N c= the carrier of N & rng the entrance of N c= the carrier of N & dom the escape of N c= the carrier of N & rng the escape of N c= the carrier of N )

proof end;

theorem Th20: :: E_SIEC:20

for N being e_net holds
( the entrance of N * (the escape of N \ (id the carrier of N)) = {} & the escape of N * (the entrance of N \ (id the carrier of N)) = {} )

proof end;

theorem :: E_SIEC:21

for N being e_net holds
( (the entrance of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N)) = {} & (the escape of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N)) = {} & (the entrance of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N)) = {} & (the escape of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N)) = {} )

proof end;

definition

let N be e_net;
func e_Places N -> set equals :: E_SIEC:def 10
rng the entrance of N;
correctness ;

end;

:: deftheorem defines e_Places E_SIEC:def 10 :

definition

let N be e_net;
func e_Transitions N -> set equals :: E_SIEC:def 11
the carrier of N \ (e_Places N);
correctness ;

end;

:: deftheorem defines e_Transitions E_SIEC:def 11 :

theorem :: E_SIEC:22

for N being e_net holds e_Places N misses e_Transitions N by XBOOLE_1:79;

theorem Th23: :: E_SIEC:23

for x, y being set
for N being e_net st ( [x,y] in the entrance of N or [x,y] in the escape of N ) & x <> y holds
( x in e_Transitions N & y in e_Places N )

proof end;

theorem Th24: :: E_SIEC:24

for N being e_net holds
( the entrance of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] & the escape of N \ (id the carrier of N) c= [:(e_Transitions N),(e_Places N):] )

proof end;

definition

let N be e_net;
func e_Flow N -> Relation equals :: E_SIEC:def 12
((the entrance of N ~ ) \/ the escape of N) \ (id the carrier of N);
correctness ;

end;

:: deftheorem defines e_Flow E_SIEC:def 12 :

theorem :: E_SIEC:25

for N being e_net holds e_Flow N c= [:(e_Places N),(e_Transitions N):] \/ [:(e_Transitions N),(e_Places N):]

proof end;

notation

let N be e_net;
synonym e_places N for e_Places N;
synonym e_transitions N for e_Transitions N;

end;

definition

let N be e_net;
canceled;
canceled;
func e_pre N -> Relation equals :: E_SIEC:def 15
the entrance of N \ (id the carrier of N);
correctness ;
func e_post N -> Relation equals :: E_SIEC:def 16
the escape of N \ (id the carrier of N);
correctness ;

end;

:: deftheorem E_SIEC:def 13 :

:: deftheorem E_SIEC:def 14 :

:: deftheorem defines e_pre E_SIEC:def 15 :

:: deftheorem defines e_post E_SIEC:def 16 :

theorem :: E_SIEC:26

canceled;

theorem :: E_SIEC:27

canceled;

theorem :: E_SIEC:28

for N being e_net holds
( e_pre N c= [:(e_transitions N),(e_places N):] & e_post N c= [:(e_transitions N),(e_places N):] ) by Th24;

definition

let N be e_net;
func e_shore N -> set equals :: E_SIEC:def 17
the carrier of N;
correctness ;
func e_prox N -> Relation equals :: E_SIEC:def 18
(the entrance of N \/ the escape of N) ~ ;
correctness ;
func e_flow N -> Relation equals :: E_SIEC:def 19
((the entrance of N ~ ) \/ the escape of N) \/ (id the carrier of N);
correctness ;

end;

:: deftheorem defines e_shore E_SIEC:def 17 :

:: deftheorem defines e_prox E_SIEC:def 18 :

:: deftheorem defines e_flow E_SIEC:def 19 :

theorem :: E_SIEC:29

for N being e_net holds
( e_prox N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] )

proof end;

theorem :: E_SIEC:30

for N being e_net holds
( (e_prox N) * (e_prox N) = e_prox N & ((e_prox N) \ (id (e_shore N))) * (e_prox N) = {} & ((e_prox N) \/ ((e_prox N) ~ )) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~ ) )

proof end;

theorem Th31: :: E_SIEC:31

for N being e_net holds
( (id (the carrier of N \ (rng the escape of N))) * (the escape of N \ (id the carrier of N)) = the escape of N \ (id the carrier of N) & (id (the carrier of N \ (rng the entrance of N))) * (the entrance of N \ (id the carrier of N)) = the entrance of N \ (id the carrier of N) )

proof end;

theorem Th32: :: E_SIEC:32

for N being e_net holds
( (the escape of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N)) = {} & (the entrance of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N)) = {} & (the escape of N \ (id the carrier of N)) * (the entrance of N \ (id the carrier of N)) = {} & (the entrance of N \ (id the carrier of N)) * (the escape of N \ (id the carrier of N)) = {} )

proof end;

theorem Th33: :: E_SIEC:33

for N being e_net holds
( ((the escape of N \ (id the carrier of N)) ~ ) * ((the escape of N \ (id the carrier of N)) ~ ) = {} & ((the entrance of N \ (id the carrier of N)) ~ ) * ((the entrance of N \ (id the carrier of N)) ~ ) = {} )

proof end;

theorem :: E_SIEC:34

for N being e_net holds
( ((the escape of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the escape of N))) ~ ) = (the escape of N \ (id the carrier of N)) ~ & ((the entrance of N \ (id the carrier of N)) ~ ) * ((id (the carrier of N \ (rng the entrance of N))) ~ ) = (the entrance of N \ (id the carrier of N)) ~ )

proof end;

theorem Th35: :: E_SIEC:35

for N being e_net holds
( (the escape of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the escape of N))) = {} & (the entrance of N \ (id the carrier of N)) * (id (the carrier of N \ (rng the entrance of N))) = {} )

proof end;

theorem Th36: :: E_SIEC:36

for N being e_net holds
( (id (the carrier of N \ (rng the escape of N))) * ((the escape of N \ (id the carrier of N)) ~ ) = {} & (id (the carrier of N \ (rng the entrance of N))) * ((the entrance of N \ (id the carrier of N)) ~ ) = {} )

proof end;

notation

let N be e_net;
synonym e_support N for e_shore N;

end;

definition

let N be e_net;
canceled;
func e_entrance N -> Relation equals :: E_SIEC:def 21
((the escape of N \ (id the carrier of N)) ~ ) \/ (id (the carrier of N \ (rng the escape of N)));
correctness ;
func e_escape N -> Relation equals :: E_SIEC:def 22
((the entrance of N \ (id the carrier of N)) ~ ) \/ (id (the carrier of N \ (rng the entrance of N)));
correctness ;

end;

:: deftheorem E_SIEC:def 20 :

:: deftheorem defines e_entrance E_SIEC:def 21 :

:: deftheorem defines e_escape E_SIEC:def 22 :

theorem :: E_SIEC:37

for N being e_net holds
( (e_entrance N) * (e_entrance N) = e_entrance N & (e_entrance N) * (e_escape N) = e_entrance N & (e_escape N) * (e_entrance N) = e_escape N & (e_escape N) * (e_escape N) = e_escape N )

proof end;

theorem :: E_SIEC:38

for N being e_net holds
( (e_entrance N) * ((e_entrance N) \ (id (e_support N))) = {} & (e_escape N) * ((e_escape N) \ (id (e_support N))) = {} )

proof end;

notation

let N be e_net;
synonym e_stanchion N for e_shore N;

end;

notation

let N be e_net;
synonym e_circulation N for e_flow N;

end;

definition

let N be e_net;
canceled;
func e_adjac N -> Relation equals :: E_SIEC:def 24
((the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id (the carrier of N \ (rng the entrance of N)));
correctness ;

end;

:: deftheorem E_SIEC:def 23 :

:: deftheorem defines e_adjac E_SIEC:def 24 :

theorem :: E_SIEC:39

for N being e_net holds
( e_adjac N c= [:(e_stanchion N),(e_stanchion N):] & e_circulation N c= [:(e_stanchion N),(e_stanchion N):] )

proof end;

theorem :: E_SIEC:40

for N being e_net holds
( (e_adjac N) * (e_adjac N) = e_adjac N & ((e_adjac N) \ (id (e_stanchion N))) * (e_adjac N) = {} & ((e_adjac N) \/ ((e_adjac N) ~ )) \/ (id (e_stanchion N)) = (e_circulation N) \/ ((e_circulation N) ~ ) )

proof end;

notation

let N be e_net;
synonym s_transitions N for e_Places N;
synonym s_places N for e_Transitions N;
synonym s_carrier N for e_shore N;
synonym s_enter N for e_entrance N;
synonym s_exit N for e_escape N;
synonym s_prox N for e_adjac N;

end;

theorem Th41: :: E_SIEC:41

for N being e_net holds
( (the entrance of N \ (id the carrier of N)) ~ c= [:(e_Places N),(e_Transitions N):] & (the escape of N \ (id the carrier of N)) ~ c= [:(e_Places N),(e_Transitions N):] )

proof end;

definition

let N be G_Net ;
func s_pre N -> Relation equals :: E_SIEC:def 25
(the escape of N \ (id the carrier of N)) ~ ;
coherence ;
func s_post N -> Relation equals :: E_SIEC:def 26
(the entrance of N \ (id the carrier of N)) ~ ;
coherence ;

end;

:: deftheorem defines s_pre E_SIEC:def 25 :

:: deftheorem defines s_post E_SIEC:def 26 :

theorem :: E_SIEC:42

for N being e_net holds
( s_post N c= [:(s_transitions N),(s_places N):] & s_pre N c= [:(s_transitions N),(s_places N):] ) by Th41;