:: E_SIEC semantic presentation

definition
attr a1 is strict;
struct G_Net -> 1-sorted ;
aggr G_Net(# carrier, entrance, escape #) -> G_Net ;
sel entrance c1 -> Relation;
sel escape c1 -> Relation;
end;

definition
let c1 be 1-sorted ;
func echaos c1 -> set equals :: E_SIEC:def 1
the carrier of a1 \/ {the carrier of a1};
correctness
coherence
the carrier of c1 \/ {the carrier of c1} is set ;
;
end;

:: deftheorem Def1 defines echaos E_SIEC:def 1 :
for b1 being 1-sorted holds echaos b1 = the carrier of b1 \/ {the carrier of b1};

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

:: deftheorem Def2 defines GG E_SIEC:def 2 :
for b1 being G_Net holds
( b1 is GG iff ( the entrance of b1 c= [:the carrier of b1,the carrier of b1:] & the escape of b1 c= [:the carrier of b1,the carrier of b1:] & the entrance of b1 * the entrance of b1 = the entrance of b1 & the entrance of b1 * the escape of b1 = the entrance of b1 & the escape of b1 * the escape of b1 = the escape of b1 & the escape of b1 * the entrance of b1 = the escape of b1 ) );

registration
cluster GG G_Net ;
existence
ex b1 being G_Net st b1 is GG
proof end;
end;

definition
mode gg_net is GG G_Net ;
end;

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

:: deftheorem Def3 defines EE E_SIEC:def 3 :
for b1 being G_Net holds
( b1 is EE iff ( the entrance of b1 * (the entrance of b1 \ (id the carrier of b1)) = {} & the escape of b1 * (the escape of b1 \ (id the carrier of b1)) = {} ) );

registration
cluster EE G_Net ;
existence
ex b1 being G_Net st b1 is EE
proof end;
end;

registration
cluster strict GG EE G_Net ;
existence
ex b1 being G_Net st
( b1 is strict & b1 is GG & b1 is EE )
proof end;
end;

definition
mode e_net is GG EE G_Net ;
end;

theorem Th1: :: E_SIEC:1
for b1 being set
for b2, b3 being Relation holds
( G_Net(# b1,b2,b3 #) is e_net iff ( b2 c= [:b1,b1:] & b3 c= [:b1,b1:] & b2 * b2 = b2 & b2 * b3 = b2 & b3 * b3 = b3 & b3 * b2 = b3 & b2 * (b2 \ (id b1)) = {} & b3 * (b3 \ (id b1)) = {} ) ) by Def2, Def3;

theorem Th2: :: E_SIEC:2
for b1 being set holds G_Net(# b1,{} ,{} #) is e_net
proof end;

theorem Th3: :: E_SIEC:3
for b1 being set holds G_Net(# b1,(id b1),(id b1) #) is e_net
proof end;

theorem Th4: :: E_SIEC:4
G_Net(# {} ,{} ,{} #) is e_net by Th2;

theorem Th5: :: E_SIEC:5
canceled;

theorem Th6: :: E_SIEC:6
canceled;

theorem Th7: :: E_SIEC:7
canceled;

theorem Th8: :: E_SIEC:8
for b1, b2 being set holds G_Net(# b1,(id (b1 \ b2)),(id (b1 \ b2)) #) is e_net
proof end;

theorem Th9: :: E_SIEC:9
for b1 being e_net holds echaos b1 <> {}
proof end;

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

:: deftheorem Def4 defines empty_e_net E_SIEC:def 4 :
empty_e_net = G_Net(# {} ,{} ,{} #);

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

:: deftheorem Def5 defines Tempty_e_net E_SIEC:def 5 :
for b1 being set holds Tempty_e_net b1 = G_Net(# b1,(id b1),(id b1) #);

:: deftheorem Def6 defines Pempty_e_net E_SIEC:def 6 :
for b1 being set holds Pempty_e_net b1 = G_Net(# b1,{} ,{} #);

theorem Th10: :: E_SIEC:10
canceled;

theorem Th11: :: E_SIEC:11
for b1 being set holds
( the carrier of (Tempty_e_net b1) = b1 & the entrance of (Tempty_e_net b1) = id b1 & the escape of (Tempty_e_net b1) = id b1 ) ;

theorem Th12: :: E_SIEC:12
for b1 being set holds
( the carrier of (Pempty_e_net b1) = b1 & the entrance of (Pempty_e_net b1) = {} & the escape of (Pempty_e_net b1) = {} ) ;

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

:: deftheorem Def7 defines Psingle_e_net E_SIEC:def 7 :
for b1 being set holds Psingle_e_net b1 = G_Net(# {b1},(id {b1}),(id {b1}) #);

:: deftheorem Def8 defines Tsingle_e_net E_SIEC:def 8 :
for b1 being set holds Tsingle_e_net b1 = G_Net(# {b1},{} ,{} #);

theorem Th13: :: E_SIEC:13
for b1 being set holds
( the carrier of (Psingle_e_net b1) = {b1} & the entrance of (Psingle_e_net b1) = id {b1} & the escape of (Psingle_e_net b1) = id {b1} ) ;

theorem Th14: :: E_SIEC:14
for b1 being set holds
( the carrier of (Tsingle_e_net b1) = {b1} & the entrance of (Tsingle_e_net b1) = {} & the escape of (Tsingle_e_net b1) = {} ) ;

theorem Th15: :: E_SIEC:15
for b1, b2 being set holds G_Net(# (b1 \/ b2),(id b1),(id b1) #) is e_net
proof end;

definition
let c1, c2 be set ;
func PTempty_e_net c1,c2 -> strict e_net equals :: E_SIEC:def 9
 G_Net(# (a1 \/ a2),(id a1),(id a1) #);
coherence
G_Net(# (c1 \/ c2),(id c1),(id c1) #) is strict e_net by Th15;
end;

:: deftheorem Def9 defines PTempty_e_net E_SIEC:def 9 :
for b1, b2 being set holds PTempty_e_net b1,b2 = G_Net(# (b1 \/ b2),(id b1),(id b1) #);

theorem Th16: :: E_SIEC:16
for b1 being e_net holds
( the entrance of b1 \ (id (dom the entrance of b1)) = the entrance of b1 \ (id the carrier of b1) & the escape of b1 \ (id (dom the escape of b1)) = the escape of b1 \ (id the carrier of b1) & the entrance of b1 \ (id (rng the entrance of b1)) = the entrance of b1 \ (id the carrier of b1) & the escape of b1 \ (id (rng the escape of b1)) = the escape of b1 \ (id the carrier of b1) )
proof end;

theorem Th17: :: E_SIEC:17
for b1 being e_net holds CL the entrance of b1 = CL the escape of b1
proof end;

theorem Th18: :: E_SIEC:18
for b1 being e_net holds
( rng the entrance of b1 = rng (CL the entrance of b1) & rng the entrance of b1 = dom (CL the entrance of b1) & rng the escape of b1 = rng (CL the escape of b1) & rng the escape of b1 = dom (CL the escape of b1) & rng the entrance of b1 = rng the escape of b1 )
proof end;

theorem Th19: :: E_SIEC:19
for b1 being e_net holds
( dom the entrance of b1 c= the carrier of b1 & rng the entrance of b1 c= the carrier of b1 & dom the escape of b1 c= the carrier of b1 & rng the escape of b1 c= the carrier of b1 )
proof end;

theorem Th20: :: E_SIEC:20
for b1 being e_net holds
( the entrance of b1 * (the escape of b1 \ (id the carrier of b1)) = {} & the escape of b1 * (the entrance of b1 \ (id the carrier of b1)) = {} )
proof end;

theorem Th21: :: E_SIEC:21
for b1 being e_net holds
( (the entrance of b1 \ (id the carrier of b1)) * (the entrance of b1 \ (id the carrier of b1)) = {} & (the escape of b1 \ (id the carrier of b1)) * (the escape of b1 \ (id the carrier of b1)) = {} & (the entrance of b1 \ (id the carrier of b1)) * (the escape of b1 \ (id the carrier of b1)) = {} & (the escape of b1 \ (id the carrier of b1)) * (the entrance of b1 \ (id the carrier of b1)) = {} )
proof end;

definition
let c1 be e_net;
func e_Places c1 -> set equals :: E_SIEC:def 10
 rng the entrance of a1;
correctness
coherence
rng the entrance of c1 is set ;
;
end;

:: deftheorem Def10 defines e_Places E_SIEC:def 10 :
for b1 being e_net holds e_Places b1 = rng the entrance of b1;

definition
let c1 be e_net;
func e_Transitions c1 -> set equals :: E_SIEC:def 11
the carrier of a1 \ (e_Places a1);
correctness
coherence
the carrier of c1 \ (e_Places c1) is set ;
;
end;

:: deftheorem Def11 defines e_Transitions E_SIEC:def 11 :
for b1 being e_net holds e_Transitions b1 = the carrier of b1 \ (e_Places b1);

theorem Th22: :: E_SIEC:22
for b1 being e_net holds e_Places b1 misses e_Transitions b1 by XBOOLE_1:79;

theorem Th23: :: E_SIEC:23
for b1, b2 being set
for b3 being e_net st ( [b1,b2] in the entrance of b3 or [b1,b2] in the escape of b3 ) & b1 <> b2 holds
( b1 in e_Transitions b3 & b2 in e_Places b3 )
proof end;

theorem Th24: :: E_SIEC:24
for b1 being e_net holds
( the entrance of b1 \ (id the carrier of b1) c= [:(e_Transitions b1),(e_Places b1):] & the escape of b1 \ (id the carrier of b1) c= [:(e_Transitions b1),(e_Places b1):] )
proof end;

definition
let c1 be e_net;
func e_Flow c1 -> Relation equals :: E_SIEC:def 12
((the entrance of a1 ~ ) \/ the escape of a1) \ (id the carrier of a1);
correctness
coherence
((the entrance of c1 ~ ) \/ the escape of c1) \ (id the carrier of c1) is Relation;
;
end;

:: deftheorem Def12 defines e_Flow E_SIEC:def 12 :
for b1 being e_net holds e_Flow b1 = ((the entrance of b1 ~ ) \/ the escape of b1) \ (id the carrier of b1);

theorem Th25: :: E_SIEC:25
for b1 being e_net holds e_Flow b1 c= [:(e_Places b1),(e_Transitions b1):] \/ [:(e_Transitions b1),(e_Places b1):]
proof end;

notation
let c1 be e_net;
synonym e_places c1 for e_Places c1;
synonym e_transitions c1 for e_Transitions c1;
end;

definition
let c1 be e_net;
canceled;
canceled;
func e_pre c1 -> Relation equals :: E_SIEC:def 15
the entrance of a1 \ (id the carrier of a1);
correctness
coherence
the entrance of c1 \ (id the carrier of c1) is Relation;
;
func e_post c1 -> Relation equals :: E_SIEC:def 16
the escape of a1 \ (id the carrier of a1);
correctness
coherence
the escape of c1 \ (id the carrier of c1) is Relation;
;
end;

:: deftheorem Def13 E_SIEC:def 13 :
canceled;

:: deftheorem Def14 E_SIEC:def 14 :
canceled;

:: deftheorem Def15 defines e_pre E_SIEC:def 15 :
for b1 being e_net holds e_pre b1 = the entrance of b1 \ (id the carrier of b1);

:: deftheorem Def16 defines e_post E_SIEC:def 16 :
for b1 being e_net holds e_post b1 = the escape of b1 \ (id the carrier of b1);

theorem Th26: :: E_SIEC:26
canceled;

theorem Th27: :: E_SIEC:27
canceled;

theorem Th28: :: E_SIEC:28
for b1 being e_net holds
( e_pre b1 c= [:(e_transitions b1),(e_places b1):] & e_post b1 c= [:(e_transitions b1),(e_places b1):] ) by Th24;

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

:: deftheorem Def17 defines e_shore E_SIEC:def 17 :
for b1 being e_net holds e_shore b1 = the carrier of b1;

:: deftheorem Def18 defines e_prox E_SIEC:def 18 :
for b1 being e_net holds e_prox b1 = (the entrance of b1 \/ the escape of b1) ~ ;

:: deftheorem Def19 defines e_flow E_SIEC:def 19 :
for b1 being e_net holds e_flow b1 = ((the entrance of b1 ~ ) \/ the escape of b1) \/ (id the carrier of b1);

theorem Th29: :: E_SIEC:29
for b1 being e_net holds
( e_prox b1 c= [:(e_shore b1),(e_shore b1):] & e_flow b1 c= [:(e_shore b1),(e_shore b1):] )
proof end;

theorem Th30: :: E_SIEC:30
for b1 being e_net holds
( (e_prox b1) * (e_prox b1) = e_prox b1 & ((e_prox b1) \ (id (e_shore b1))) * (e_prox b1) = {} & ((e_prox b1) \/ ((e_prox b1) ~ )) \/ (id (e_shore b1)) = (e_flow b1) \/ ((e_flow b1) ~ ) )
proof end;

theorem Th31: :: E_SIEC:31
for b1 being e_net holds
( (id (the carrier of b1 \ (rng the escape of b1))) * (the escape of b1 \ (id the carrier of b1)) = the escape of b1 \ (id the carrier of b1) & (id (the carrier of b1 \ (rng the entrance of b1))) * (the entrance of b1 \ (id the carrier of b1)) = the entrance of b1 \ (id the carrier of b1) )
proof end;

theorem Th32: :: E_SIEC:32
for b1 being e_net holds
( (the escape of b1 \ (id the carrier of b1)) * (the escape of b1 \ (id the carrier of b1)) = {} & (the entrance of b1 \ (id the carrier of b1)) * (the entrance of b1 \ (id the carrier of b1)) = {} & (the escape of b1 \ (id the carrier of b1)) * (the entrance of b1 \ (id the carrier of b1)) = {} & (the entrance of b1 \ (id the carrier of b1)) * (the escape of b1 \ (id the carrier of b1)) = {} )
proof end;

theorem Th33: :: E_SIEC:33
for b1 being e_net holds
( ((the escape of b1 \ (id the carrier of b1)) ~ ) * ((the escape of b1 \ (id the carrier of b1)) ~ ) = {} & ((the entrance of b1 \ (id the carrier of b1)) ~ ) * ((the entrance of b1 \ (id the carrier of b1)) ~ ) = {} )
proof end;

theorem Th34: :: E_SIEC:34
for b1 being e_net holds
( ((the escape of b1 \ (id the carrier of b1)) ~ ) * ((id (the carrier of b1 \ (rng the escape of b1))) ~ ) = (the escape of b1 \ (id the carrier of b1)) ~ & ((the entrance of b1 \ (id the carrier of b1)) ~ ) * ((id (the carrier of b1 \ (rng the entrance of b1))) ~ ) = (the entrance of b1 \ (id the carrier of b1)) ~ )
proof end;

theorem Th35: :: E_SIEC:35
for b1 being e_net holds
( (the escape of b1 \ (id the carrier of b1)) * (id (the carrier of b1 \ (rng the escape of b1))) = {} & (the entrance of b1 \ (id the carrier of b1)) * (id (the carrier of b1 \ (rng the entrance of b1))) = {} )
proof end;

theorem Th36: :: E_SIEC:36
for b1 being e_net holds
( (id (the carrier of b1 \ (rng the escape of b1))) * ((the escape of b1 \ (id the carrier of b1)) ~ ) = {} & (id (the carrier of b1 \ (rng the entrance of b1))) * ((the entrance of b1 \ (id the carrier of b1)) ~ ) = {} )
proof end;

notation
let c1 be e_net;
synonym e_support c1 for e_shore c1;
end;

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

:: deftheorem Def20 E_SIEC:def 20 :
canceled;

:: deftheorem Def21 defines e_entrance E_SIEC:def 21 :
for b1 being e_net holds e_entrance b1 = ((the escape of b1 \ (id the carrier of b1)) ~ ) \/ (id (the carrier of b1 \ (rng the escape of b1)));

:: deftheorem Def22 defines e_escape E_SIEC:def 22 :
for b1 being e_net holds e_escape b1 = ((the entrance of b1 \ (id the carrier of b1)) ~ ) \/ (id (the carrier of b1 \ (rng the entrance of b1)));

theorem Th37: :: E_SIEC:37
for b1 being e_net holds
( (e_entrance b1) * (e_entrance b1) = e_entrance b1 & (e_entrance b1) * (e_escape b1) = e_entrance b1 & (e_escape b1) * (e_entrance b1) = e_escape b1 & (e_escape b1) * (e_escape b1) = e_escape b1 )
proof end;

theorem Th38: :: E_SIEC:38
for b1 being e_net holds
( (e_entrance b1) * ((e_entrance b1) \ (id (e_support b1))) = {} & (e_escape b1) * ((e_escape b1) \ (id (e_support b1))) = {} )
proof end;

notation
let c1 be e_net;
synonym e_stanchion c1 for e_shore c1;
end;

notation
let c1 be e_net;
synonym e_circulation c1 for e_flow c1;
end;

definition
let c1 be e_net;
canceled;
func e_adjac c1 -> Relation equals :: E_SIEC:def 24
((the entrance of a1 \/ the escape of a1) \ (id the carrier of a1)) \/ (id (the carrier of a1 \ (rng the entrance of a1)));
correctness
coherence
((the entrance of c1 \/ the escape of c1) \ (id the carrier of c1)) \/ (id (the carrier of c1 \ (rng the entrance of c1))) is Relation;
;
end;

:: deftheorem Def23 E_SIEC:def 23 :
canceled;

:: deftheorem Def24 defines e_adjac E_SIEC:def 24 :
for b1 being e_net holds e_adjac b1 = ((the entrance of b1 \/ the escape of b1) \ (id the carrier of b1)) \/ (id (the carrier of b1 \ (rng the entrance of b1)));

theorem Th39: :: E_SIEC:39
for b1 being e_net holds
( e_adjac b1 c= [:(e_stanchion b1),(e_stanchion b1):] & e_circulation b1 c= [:(e_stanchion b1),(e_stanchion b1):] )
proof end;

theorem Th40: :: E_SIEC:40
for b1 being e_net holds
( (e_adjac b1) * (e_adjac b1) = e_adjac b1 & ((e_adjac b1) \ (id (e_stanchion b1))) * (e_adjac b1) = {} & ((e_adjac b1) \/ ((e_adjac b1) ~ )) \/ (id (e_stanchion b1)) = (e_circulation b1) \/ ((e_circulation b1) ~ ) )
proof end;

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

theorem Th41: :: E_SIEC:41
for b1 being e_net holds
( (the entrance of b1 \ (id the carrier of b1)) ~ c= [:(e_Places b1),(e_Transitions b1):] & (the escape of b1 \ (id the carrier of b1)) ~ c= [:(e_Places b1),(e_Transitions b1):] )
proof end;

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

:: deftheorem Def25 defines s_pre E_SIEC:def 25 :
for b1 being G_Net holds s_pre b1 = (the escape of b1 \ (id the carrier of b1)) ~ ;

:: deftheorem Def26 defines s_post E_SIEC:def 26 :
for b1 being G_Net holds s_post b1 = (the entrance of b1 \ (id the carrier of b1)) ~ ;

theorem Th42: :: E_SIEC:42
for b1 being e_net holds
( s_post b1 c= [:(s_transitions b1),(s_places b1):] & s_pre b1 c= [:(s_transitions b1),(s_places b1):] ) by Th41;