E_SIEC

:: E_SIEC semantic presentation

begin

definition

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

end;

definition

let IT be ( ( ) ( ) G_Net ) ;

attr IT is GG means :: E_SIEC:def 1
( the entrance of IT : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) c= [: the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) & the escape of IT : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) c= [: the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) & the entrance of IT : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) * the entrance of IT : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = the entrance of IT : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) & the entrance of IT : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) * the escape of IT : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = the entrance of IT : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) & the escape of IT : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) * the escape of IT : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = the escape of IT : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) & the escape of IT : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) * the entrance of IT : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = the escape of IT : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) );

end;

registration

cluster GG for ( ( ) ( ) G_Net ) ;

end;

definition

mode gg_net is ( ( GG ) ( GG ) G_Net ) ;

end;

definition

let IT be ( ( ) ( ) G_Net ) ;

attr IT is EE means :: E_SIEC:def 2
( the entrance of IT : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) * ( the entrance of IT : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -defined the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) & the escape of IT : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) * ( the escape of IT : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -defined the carrier of IT : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) );

end;

registration

cluster EE for ( ( ) ( ) G_Net ) ;

end;

registration

cluster strict GG EE for ( ( ) ( ) G_Net ) ;

end;

definition

mode e_net is ( ( GG EE ) ( GG EE ) G_Net ) ;

end;

theorem :: E_SIEC:1

for X being ( ( ) ( ) set )
for R, S being ( ( Relation-like ) ( Relation-like ) Relation) holds
( G_Net(# X : ( ( ) ( ) set ) ,R : ( ( Relation-like ) ( Relation-like ) Relation) ,S : ( ( Relation-like ) ( Relation-like ) Relation) #) : ( ( strict ) ( strict ) G_Net ) is ( ( GG EE ) ( GG EE ) e_net) iff ( R : ( ( Relation-like ) ( Relation-like ) Relation) c= [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) & S : ( ( Relation-like ) ( Relation-like ) Relation) c= [:X : ( ( ) ( ) set ) ,X : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) & R : ( ( Relation-like ) ( Relation-like ) Relation) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = R : ( ( Relation-like ) ( Relation-like ) Relation) & R : ( ( Relation-like ) ( Relation-like ) Relation) * S : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = R : ( ( Relation-like ) ( Relation-like ) Relation) & S : ( ( Relation-like ) ( Relation-like ) Relation) * S : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = S : ( ( Relation-like ) ( Relation-like ) Relation) & S : ( ( Relation-like ) ( Relation-like ) Relation) * R : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = S : ( ( Relation-like ) ( Relation-like ) Relation) & R : ( ( Relation-like ) ( Relation-like ) Relation) * (R : ( ( Relation-like ) ( Relation-like ) Relation) \ (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) & S : ( ( Relation-like ) ( Relation-like ) Relation) * (S : ( ( Relation-like ) ( Relation-like ) Relation) \ (id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) ) ) ;

theorem :: E_SIEC:2

for X being ( ( ) ( ) set ) holds G_Net(# X : ( ( ) ( ) set ) ,{} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) ,{} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) #) : ( ( strict ) ( strict ) G_Net ) is ( ( GG EE ) ( GG EE ) e_net) ;

theorem :: E_SIEC:3

for X being ( ( ) ( ) set ) holds G_Net(# X : ( ( ) ( ) set ) ,(id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) set ) ,(id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) set ) #) : ( ( strict ) ( strict ) G_Net ) is ( ( GG EE ) ( GG EE ) e_net) ;

theorem :: E_SIEC:4

G_Net(# {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) ,{} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) ,{} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) #) : ( ( strict ) ( strict ) G_Net ) is ( ( GG EE ) ( GG EE ) e_net) ;

theorem :: E_SIEC:5

for X, Y being ( ( ) ( ) set ) holds G_Net(# X : ( ( ) ( ) set ) ,(id (X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b₁ : ( ( ) ( ) set ) \ b₂ : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) \ b₂ : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) set ) ,(id (X : ( ( ) ( ) set ) \ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b₁ : ( ( ) ( ) set ) \ b₂ : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) \ b₂ : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) set ) #) : ( ( strict ) ( strict ) G_Net ) is ( ( GG EE ) ( GG EE ) e_net) ;

definition

func empty_e_net -> ( ( strict GG EE ) ( strict GG EE ) e_net) equals :: E_SIEC:def 3
G_Net(# {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) ,{} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) ,{} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) #) : ( ( strict ) ( strict ) G_Net ) ;

end;

definition

let X be ( ( ) ( ) set ) ;

func Tempty_e_net X -> ( ( strict GG EE ) ( strict GG EE ) e_net) equals :: E_SIEC:def 4
G_Net(# X : ( ( ) ( ) 2-sorted ) ,(id X : ( ( ) ( ) 2-sorted ) ) : ( ( Relation-like ) ( Relation-like X : ( ( ) ( ) 2-sorted ) -defined X : ( ( ) ( ) 2-sorted ) -valued ) set ) ,(id X : ( ( ) ( ) 2-sorted ) ) : ( ( Relation-like ) ( Relation-like X : ( ( ) ( ) 2-sorted ) -defined X : ( ( ) ( ) 2-sorted ) -valued ) set ) #) : ( ( strict ) ( strict ) G_Net ) ;

func Pempty_e_net X -> ( ( strict GG EE ) ( strict GG EE ) e_net) equals :: E_SIEC:def 5
G_Net(# X : ( ( ) ( ) 2-sorted ) ,{} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) ,{} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) #) : ( ( strict ) ( strict ) G_Net ) ;

end;

theorem :: E_SIEC:6

for X being ( ( ) ( ) set ) holds
( the carrier of (Tempty_e_net X : ( ( ) ( ) set ) ) : ( ( strict GG EE ) ( strict GG EE ) e_net) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) & the entrance of (Tempty_e_net X : ( ( ) ( ) set ) ) : ( ( strict GG EE ) ( strict GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) = id X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) set ) & the escape of (Tempty_e_net X : ( ( ) ( ) set ) ) : ( ( strict GG EE ) ( strict GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) = id X : ( ( ) ( ) set ) : ( ( Relation-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) set ) ) ;

theorem :: E_SIEC:7

for X being ( ( ) ( ) set ) holds
( the carrier of (Pempty_e_net X : ( ( ) ( ) set ) ) : ( ( strict GG EE ) ( strict GG EE ) e_net) : ( ( ) ( ) set ) = X : ( ( ) ( ) set ) & the entrance of (Pempty_e_net X : ( ( ) ( ) set ) ) : ( ( strict GG EE ) ( strict GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) & the escape of (Pempty_e_net X : ( ( ) ( ) set ) ) : ( ( strict GG EE ) ( strict GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) ) ;

definition

let x be ( ( ) ( ) set ) ;

func Psingle_e_net x -> ( ( strict GG EE ) ( strict GG EE ) e_net) equals :: E_SIEC:def 6
G_Net(# {x : ( ( ) ( ) 2-sorted ) } : ( ( ) ( non empty ) set ) ,(id {x : ( ( ) ( ) 2-sorted ) } : ( ( ) ( non empty ) set ) ) : ( ( Relation-like ) ( Relation-like {x : ( ( ) ( ) 2-sorted ) } : ( ( ) ( non empty ) set ) -defined {x : ( ( ) ( ) 2-sorted ) } : ( ( ) ( non empty ) set ) -valued ) set ) ,(id {x : ( ( ) ( ) 2-sorted ) } : ( ( ) ( non empty ) set ) ) : ( ( Relation-like ) ( Relation-like {x : ( ( ) ( ) 2-sorted ) } : ( ( ) ( non empty ) set ) -defined {x : ( ( ) ( ) 2-sorted ) } : ( ( ) ( non empty ) set ) -valued ) set ) #) : ( ( strict ) ( strict ) G_Net ) ;

func Tsingle_e_net x -> ( ( strict GG EE ) ( strict GG EE ) e_net) equals :: E_SIEC:def 7
G_Net(# {x : ( ( ) ( ) 2-sorted ) } : ( ( ) ( non empty ) set ) ,{} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) ,{} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) #) : ( ( strict ) ( strict ) G_Net ) ;

end;

theorem :: E_SIEC:8

for x being ( ( ) ( ) set ) holds
( the carrier of (Psingle_e_net x : ( ( ) ( ) set ) ) : ( ( strict GG EE ) ( strict GG EE ) e_net) : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) & the entrance of (Psingle_e_net x : ( ( ) ( ) set ) ) : ( ( strict GG EE ) ( strict GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) = id {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) : ( ( Relation-like ) ( Relation-like {b₁ : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -defined {b₁ : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -valued ) set ) & the escape of (Psingle_e_net x : ( ( ) ( ) set ) ) : ( ( strict GG EE ) ( strict GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) = id {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) : ( ( Relation-like ) ( Relation-like {b₁ : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -defined {b₁ : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) -valued ) set ) ) ;

theorem :: E_SIEC:9

for x being ( ( ) ( ) set ) holds
( the carrier of (Tsingle_e_net x : ( ( ) ( ) set ) ) : ( ( strict GG EE ) ( strict GG EE ) e_net) : ( ( ) ( ) set ) = {x : ( ( ) ( ) set ) } : ( ( ) ( non empty ) set ) & the entrance of (Tsingle_e_net x : ( ( ) ( ) set ) ) : ( ( strict GG EE ) ( strict GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) & the escape of (Tsingle_e_net x : ( ( ) ( ) set ) ) : ( ( strict GG EE ) ( strict GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) ) ;

theorem :: E_SIEC:10

for X, Y being ( ( ) ( ) set ) holds G_Net(# (X : ( ( ) ( ) set ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) set ) ,(id X : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like b₁ : ( ( ) ( ) set ) -defined b₁ : ( ( ) ( ) set ) -valued ) set ) #) : ( ( strict ) ( strict ) G_Net ) is ( ( GG EE ) ( GG EE ) e_net) ;

definition

let X, Y be ( ( ) ( ) set ) ;

func PTempty_e_net (X,Y) -> ( ( strict GG EE ) ( strict GG EE ) e_net) equals :: E_SIEC:def 8
G_Net(# (X : ( ( ) ( ) 2-sorted ) \/ Y : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ,(id X : ( ( ) ( ) 2-sorted ) ) : ( ( Relation-like ) ( Relation-like X : ( ( ) ( ) 2-sorted ) -defined X : ( ( ) ( ) 2-sorted ) -valued ) set ) ,(id X : ( ( ) ( ) 2-sorted ) ) : ( ( Relation-like ) ( Relation-like X : ( ( ) ( ) 2-sorted ) -defined X : ( ( ) ( ) 2-sorted ) -valued ) set ) #) : ( ( strict ) ( strict ) G_Net ) ;

end;

theorem :: E_SIEC:11

for N being ( ( GG EE ) ( GG EE ) e_net) holds
( the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom the entrance of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom the entrance of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) = the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) & the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (dom the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like dom the escape of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined dom the escape of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) = the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) & the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (rng the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like rng the entrance of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined rng the entrance of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) = the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) & the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (rng the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like rng the escape of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -defined rng the escape of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) = the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) ) ;

theorem :: E_SIEC:12

for N being ( ( GG EE ) ( GG EE ) e_net) holds CL the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = CL the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) ;

theorem :: E_SIEC:13

for N being ( ( GG EE ) ( GG EE ) e_net) holds
( rng the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) = rng (CL the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( ) set ) & rng the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) = dom (CL the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( ) set ) & rng the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) = rng (CL the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( ) set ) & rng the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) = dom (CL the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( ) set ) & rng the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) = rng the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) ) ;

theorem :: E_SIEC:14

for N being ( ( GG EE ) ( GG EE ) e_net) holds
( dom the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) c= the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) & rng the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) c= the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) & dom the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) c= the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) & rng the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) c= the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) ;

theorem :: E_SIEC:15

for N being ( ( GG EE ) ( GG EE ) e_net) holds
( the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) * ( the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) & the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) * ( the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) ) ;

theorem :: E_SIEC:16

for N being ( ( GG EE ) ( GG EE ) e_net) holds
( ( the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) * ( the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) & ( the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) * ( the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) & ( the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) * ( the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) & ( the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) * ( the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) ) ;

definition

let N be ( ( GG EE ) ( GG EE ) e_net) ;

func e_Places N -> ( ( ) ( ) set ) equals :: E_SIEC:def 9
rng the entrance of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( ) ( ) set ) ;

end;

definition

let N be ( ( GG EE ) ( GG EE ) e_net) ;

func e_Transitions N -> ( ( ) ( ) set ) equals :: E_SIEC:def 10
the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) \ (e_Places N : ( ( ) ( ) 2-sorted ) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) ;

end;

theorem :: E_SIEC:17

for x, y being ( ( ) ( ) set )
for N being ( ( GG EE ) ( GG EE ) e_net) st ( [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) or [x : ( ( ) ( ) set ) ,y : ( ( ) ( ) set ) ] : ( ( ) ( ) set ) in the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) & x : ( ( ) ( ) set ) <> y : ( ( ) ( ) set ) holds
( x : ( ( ) ( ) set ) in e_Transitions N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) & y : ( ( ) ( ) set ) in e_Places N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) ;

theorem :: E_SIEC:18

for N being ( ( GG EE ) ( GG EE ) e_net) holds
( the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) c= [:(e_Transitions N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) ,(e_Places N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) & the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) c= [:(e_Transitions N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) ,(e_Places N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ) ;

definition

let N be ( ( GG EE ) ( GG EE ) e_net) ;

func e_Flow N -> ( ( Relation-like ) ( Relation-like ) Relation) equals :: E_SIEC:def 11
(( the entrance of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) ~) : ( ( Relation-like ) ( Relation-like ) set ) \/ the escape of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( Relation-like ) set ) \ (id N : ( ( ) ( ) 2-sorted ) ) : ( ( V6() V18( the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) ) ( Relation-like V6() V18( the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) ) M2( bool [: the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) , the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( ) set ) )) : ( ( ) ( Relation-like ) set ) ;

end;

theorem :: E_SIEC:19

for N being ( ( GG EE ) ( GG EE ) e_net) holds e_Flow N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) c= [:(e_Places N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) ,(e_Transitions N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) \/ [:(e_Transitions N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) ,(e_Places N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) : ( ( ) ( Relation-like ) set ) ;

definition

let N be ( ( GG EE ) ( GG EE ) e_net) ;

func e_pre N -> ( ( Relation-like ) ( Relation-like ) Relation) equals :: E_SIEC:def 12
the entrance of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -defined the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) ;

func e_post N -> ( ( Relation-like ) ( Relation-like ) Relation) equals :: E_SIEC:def 13
the escape of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -defined the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) ;

end;

theorem :: E_SIEC:20

for N being ( ( GG EE ) ( GG EE ) e_net) holds
( e_pre N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) c= [:(e_Transitions N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) ,(e_Places N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) & e_post N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) c= [:(e_Transitions N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) ,(e_Places N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ) ;

definition

let N be ( ( GG EE ) ( GG EE ) e_net) ;

func e_shore N -> ( ( ) ( ) set ) equals :: E_SIEC:def 14
the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ;

func e_prox N -> ( ( Relation-like ) ( Relation-like ) Relation) equals :: E_SIEC:def 15
( the entrance of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) \/ the escape of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( Relation-like ) set ) ~ : ( ( Relation-like ) ( Relation-like ) set ) ;

func e_flow N -> ( ( Relation-like ) ( Relation-like ) Relation) equals :: E_SIEC:def 16
(( the entrance of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) ~) : ( ( Relation-like ) ( Relation-like ) set ) \/ the escape of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( Relation-like ) set ) \/ (id the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -defined the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) ;

end;

theorem :: E_SIEC:21

for N being ( ( GG EE ) ( GG EE ) e_net) holds
( e_prox N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) c= [:(e_shore N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) ,(e_shore N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) & e_flow N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) c= [:(e_shore N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) ,(e_shore N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ) ;

theorem :: E_SIEC:22

for N being ( ( GG EE ) ( GG EE ) e_net) holds
( (e_prox N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) * (e_prox N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = e_prox N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) & ((e_prox N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (e_shore N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like e_shore b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined e_shore b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) * (e_prox N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) & ((e_prox N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) \/ ((e_prox N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) ~) : ( ( Relation-like ) ( Relation-like ) set ) ) : ( ( ) ( Relation-like ) set ) \/ (id (e_shore N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like e_shore b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined e_shore b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) = (e_flow N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) \/ ((e_flow N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) ~) : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( Relation-like ) set ) ) ;

theorem :: E_SIEC:23

for N being ( ( GG EE ) ( GG EE ) e_net) holds
( (id ( the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the escape of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the escape of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) set ) * ( the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the escape of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined ) set ) = the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) & (id ( the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the entrance of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the entrance of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) set ) * ( the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the entrance of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined ) set ) = the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) ) ;

theorem :: E_SIEC:24

for N being ( ( GG EE ) ( GG EE ) e_net) holds
( ( the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) * ( the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) & ( the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) * ( the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) & ( the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) * ( the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) & ( the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) * ( the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) ) ;

theorem :: E_SIEC:25

theorem :: E_SIEC:26

for N being ( ( GG EE ) ( GG EE ) e_net) holds
( (( the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) ~) : ( ( Relation-like ) ( Relation-like ) set ) * ((id ( the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the escape of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the escape of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) set ) ~) : ( ( Relation-like ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = ( the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) ~ : ( ( Relation-like ) ( Relation-like ) set ) & (( the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) ~) : ( ( Relation-like ) ( Relation-like ) set ) * ((id ( the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the entrance of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the entrance of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) set ) ~) : ( ( Relation-like ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = ( the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) ~ : ( ( Relation-like ) ( Relation-like ) set ) ) ;

theorem :: E_SIEC:27

for N being ( ( GG EE ) ( GG EE ) e_net) holds
( ( the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) * (id ( the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the escape of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the escape of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) set ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the escape of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) & ( the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) * (id ( the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the entrance of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the entrance of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) set ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the entrance of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) ) ;

theorem :: E_SIEC:28

for N being ( ( GG EE ) ( GG EE ) e_net) holds
( (id ( the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the escape of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the escape of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) set ) * (( the escape of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) ~) : ( ( Relation-like ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the escape of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) & (id ( the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the entrance of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the entrance of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) set ) * (( the entrance of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) ~) : ( ( Relation-like ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like the carrier of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) \ (rng the entrance of b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) ) ;

definition

let N be ( ( GG EE ) ( GG EE ) e_net) ;

func e_entrance N -> ( ( Relation-like ) ( Relation-like ) Relation) equals :: E_SIEC:def 17
(( the escape of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -defined the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) ~) : ( ( Relation-like ) ( Relation-like ) set ) \/ (id ( the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) \ (rng the escape of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) \ (rng the escape of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) \ (rng the escape of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) ;

func e_escape N -> ( ( Relation-like ) ( Relation-like ) Relation) equals :: E_SIEC:def 18
(( the entrance of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -defined the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) ~) : ( ( Relation-like ) ( Relation-like ) set ) \/ (id ( the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) \ (rng the entrance of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) \ (rng the entrance of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) \ (rng the entrance of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) ;

end;

theorem :: E_SIEC:29

for N being ( ( GG EE ) ( GG EE ) e_net) holds
( (e_entrance N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) * (e_entrance N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = e_entrance N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) & (e_entrance N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) * (e_escape N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = e_entrance N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) & (e_escape N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) * (e_entrance N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = e_escape N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) & (e_escape N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) * (e_escape N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = e_escape N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) ) ;

theorem :: E_SIEC:30

for N being ( ( GG EE ) ( GG EE ) e_net) holds
( (e_entrance N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) * ((e_entrance N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (e_shore N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like e_shore b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined e_shore b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) & (e_escape N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) * ((e_escape N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (e_shore N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like e_shore b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined e_shore b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) ) ;

definition

let N be ( ( GG EE ) ( GG EE ) e_net) ;

func e_adjac N -> ( ( Relation-like ) ( Relation-like ) Relation) equals :: E_SIEC:def 19
(( the entrance of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) \/ the escape of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( Relation-like ) set ) \ (id the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -defined the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) \/ (id ( the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) \ (rng the entrance of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) \ (rng the entrance of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -defined the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) \ (rng the entrance of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) ) : ( ( ) ( ) set ) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) ;

end;

theorem :: E_SIEC:31

for N being ( ( GG EE ) ( GG EE ) e_net) holds
( e_adjac N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) c= [:(e_shore N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) ,(e_shore N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) & e_flow N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) c= [:(e_shore N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) ,(e_shore N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ) ;

theorem :: E_SIEC:32

for N being ( ( GG EE ) ( GG EE ) e_net) holds
( (e_adjac N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) * (e_adjac N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = e_adjac N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) & ((e_adjac N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id (e_shore N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like e_shore b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined e_shore b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) * (e_adjac N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) : ( ( Relation-like ) ( Relation-like ) set ) = {} : ( ( ) ( Relation-like non-empty empty-yielding empty ) set ) & ((e_adjac N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) \/ ((e_adjac N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) ~) : ( ( Relation-like ) ( Relation-like ) set ) ) : ( ( ) ( Relation-like ) set ) \/ (id (e_shore N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like e_shore b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -defined e_shore b₁ : ( ( GG EE ) ( GG EE ) e_net) : ( ( ) ( ) set ) -valued ) set ) : ( ( ) ( Relation-like ) set ) = (e_flow N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) \/ ((e_flow N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( Relation-like ) ( Relation-like ) Relation) ~) : ( ( Relation-like ) ( Relation-like ) set ) : ( ( ) ( Relation-like ) set ) ) ;

theorem :: E_SIEC:33

definition

let N be ( ( ) ( ) G_Net ) ;

func s_pre N -> ( ( Relation-like ) ( Relation-like ) Relation) equals :: E_SIEC:def 20
( the escape of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -defined the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) ~ : ( ( Relation-like ) ( Relation-like ) set ) ;

func s_post N -> ( ( Relation-like ) ( Relation-like ) Relation) equals :: E_SIEC:def 21
( the entrance of N : ( ( ) ( ) 2-sorted ) : ( ( Relation-like ) ( Relation-like ) Relation) \ (id the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) ) : ( ( Relation-like ) ( Relation-like the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -defined the carrier of N : ( ( ) ( ) 2-sorted ) : ( ( ) ( ) set ) -valued ) set ) ) : ( ( ) ( Relation-like ) set ) ~ : ( ( Relation-like ) ( Relation-like ) set ) ;

end;

theorem :: E_SIEC:34

for N being ( ( GG EE ) ( GG EE ) e_net) holds
( s_post N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) c= [:(e_Places N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) ,(e_Transitions N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) & s_pre N : ( ( GG EE ) ( GG EE ) e_net) : ( ( Relation-like ) ( Relation-like ) Relation) c= [:(e_Places N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) ,(e_Transitions N : ( ( GG EE ) ( GG EE ) e_net) ) : ( ( ) ( ) set ) :] : ( ( ) ( Relation-like ) set ) ) ;