:: by Waldemar Korczy\'nski

::

:: Received January 31, 1992

:: Copyright (c) 1992-2017 Association of Mizar Users

definition

attr c_{1} is strict ;

struct G_Net -> 1-sorted ;

aggr G_Net(# carrier, entrance, escape #) -> G_Net ;

sel entrance c_{1} -> Relation;

sel escape c_{1} -> Relation;

end;
struct G_Net -> 1-sorted ;

aggr G_Net(# carrier, entrance, escape #) -> G_Net ;

sel entrance c

sel escape c

definition

let IT be G_Net ;

end;
attr IT is GG means :Def1: :: E_SIEC:def 1

( 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 );

( 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 );

:: deftheorem Def1 defines GG E_SIEC:def 1 :

for IT being G_Net holds

( IT is GG iff ( 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 ) );

for IT being G_Net holds

( IT is GG iff ( 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 ) );

:: deftheorem Def2 defines EE E_SIEC:def 2 :

for IT being G_Net holds

( IT is EE iff ( 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)) = {} ) );

for IT being G_Net holds

( IT is EE iff ( 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)) = {} ) );

registration
end;

theorem :: E_SIEC:1

definition

let X be set ;

coherence

G_Net(# X,(id X),(id X) #) is strict e_net by Th3;

coherence

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

end;
coherence

G_Net(# X,(id X),(id X) #) is strict e_net by Th3;

coherence

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

:: deftheorem defines Tempty_e_net E_SIEC:def 4 :

for X being set holds Tempty_e_net X = G_Net(# X,(id X),(id X) #);

for X being set holds Tempty_e_net X = G_Net(# X,(id X),(id X) #);

:: deftheorem defines Pempty_e_net E_SIEC:def 5 :

for X being set holds Pempty_e_net X = G_Net(# X,{},{} #);

for X being set holds Pempty_e_net X = G_Net(# X,{},{} #);

theorem :: E_SIEC:6

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 ) ;

( 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:7

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) = {} ) ;

( 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 object ;

coherence

G_Net(# {x},(id {x}),(id {x}) #) is strict e_net by Th3;

coherence

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

end;
coherence

G_Net(# {x},(id {x}),(id {x}) #) is strict e_net by Th3;

coherence

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

:: deftheorem defines Psingle_e_net E_SIEC:def 6 :

for x being object holds Psingle_e_net x = G_Net(# {x},(id {x}),(id {x}) #);

for x being object holds Psingle_e_net x = G_Net(# {x},(id {x}),(id {x}) #);

:: deftheorem defines Tsingle_e_net E_SIEC:def 7 :

for x being object holds Tsingle_e_net x = G_Net(# {x},{},{} #);

for x being object holds Tsingle_e_net x = G_Net(# {x},{},{} #);

theorem :: E_SIEC:8

theorem :: E_SIEC:9

for x being object holds

( the carrier of (Tsingle_e_net x) = {x} & the entrance of (Tsingle_e_net x) = {} & the escape of (Tsingle_e_net x) = {} ) ;

( the carrier of (Tsingle_e_net x) = {x} & the entrance of (Tsingle_e_net x) = {} & the escape of (Tsingle_e_net x) = {} ) ;

definition
end;

:: deftheorem defines PTempty_e_net E_SIEC:def 8 :

for X, Y being set holds PTempty_e_net (X,Y) = G_Net(# (X \/ Y),(id X),(id X) #);

for X, Y being set holds PTempty_e_net (X,Y) = G_Net(# (X \/ Y),(id X),(id X) #);

theorem Th11: :: E_SIEC:11

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) )

( 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 Th13: :: E_SIEC:13

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 )

( 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 Th14: :: E_SIEC:14

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 )

( 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 Th15: :: E_SIEC:15

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)) = {} )

( 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:16

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)) = {} )

( ( 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;

:: deftheorem defines e_Places E_SIEC:def 9 :

for N being e_net holds e_Places N = rng the entrance of N;

for N being e_net holds e_Places N = rng the entrance of N;

:: deftheorem defines e_Transitions E_SIEC:def 10 :

for N being e_net holds e_Transitions N = the carrier of N \ (e_Places N);

for N being e_net holds e_Transitions N = the carrier of N \ (e_Places N);

theorem Th17: :: E_SIEC:17

for x, y being object

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 )

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 Th18: :: E_SIEC:18

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):] )

( 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;

coherence

(( the entrance of N ~) \/ the escape of N) \ (id N) is Relation;

;

end;
func e_Flow N -> Relation equals :: E_SIEC:def 11

(( the entrance of N ~) \/ the escape of N) \ (id N);

correctness (( the entrance of N ~) \/ the escape of N) \ (id N);

coherence

(( the entrance of N ~) \/ the escape of N) \ (id N) is Relation;

;

:: deftheorem defines e_Flow E_SIEC:def 11 :

for N being e_net holds e_Flow N = (( the entrance of N ~) \/ the escape of N) \ (id N);

for N being e_net holds e_Flow N = (( the entrance of N ~) \/ the escape of N) \ (id N);

theorem :: E_SIEC:19

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

proof end;

definition

let N be e_net;

correctness

coherence

the entrance of N \ (id the carrier of N) is Relation;

;

correctness

coherence

the escape of N \ (id the carrier of N) is Relation;

;

end;
correctness

coherence

the entrance of N \ (id the carrier of N) is Relation;

;

correctness

coherence

the escape of N \ (id the carrier of N) is Relation;

;

:: deftheorem defines e_pre E_SIEC:def 12 :

for N being e_net holds e_pre N = the entrance of N \ (id the carrier of N);

for N being e_net holds e_pre N = the entrance of N \ (id the carrier of N);

:: deftheorem defines e_post E_SIEC:def 13 :

for N being e_net holds e_post N = the escape of N \ (id the carrier of N);

for N being e_net holds e_post N = the escape of N \ (id the carrier of N);

theorem :: E_SIEC:20

definition

let N be e_net;

correctness

coherence

the carrier of N is set ;

;

correctness

coherence

( the entrance of N \/ the escape of N) ~ is Relation;

;

coherence

(( the entrance of N ~) \/ the escape of N) \/ (id the carrier of N) is Relation;

;

end;
correctness

coherence

the carrier of N is set ;

;

correctness

coherence

( the entrance of N \/ the escape of N) ~ is Relation;

;

func e_flow N -> Relation equals :: E_SIEC:def 16

(( the entrance of N ~) \/ the escape of N) \/ (id the carrier of N);

correctness (( the entrance of N ~) \/ the escape of N) \/ (id the carrier of N);

coherence

(( the entrance of N ~) \/ the escape of N) \/ (id the carrier of N) is Relation;

;

:: deftheorem defines e_prox E_SIEC:def 15 :

for N being e_net holds e_prox N = ( the entrance of N \/ the escape of N) ~ ;

for N being e_net holds e_prox N = ( the entrance of N \/ the escape of N) ~ ;

:: deftheorem defines e_flow E_SIEC:def 16 :

for N being e_net holds e_flow N = (( the entrance of N ~) \/ the escape of N) \/ (id the carrier of N);

for N being e_net holds e_flow N = (( the entrance of N ~) \/ the escape of N) \/ (id the carrier of N);

theorem :: E_SIEC:21

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):] )

( 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:22

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) ~) )

( (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 Th23: :: E_SIEC:23

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) )

( (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 Th24: :: E_SIEC:24

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)) = {} )

( ( 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 Th25: :: E_SIEC:25

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 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:26

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)) ~ )

( (( 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 Th27: :: E_SIEC:27

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))) = {} )

( ( 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 Th28: :: E_SIEC:28

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)) ~) = {} )

( (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;

definition

let N be e_net;

coherence

(( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N))) is Relation;

;

coherence

(( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))) is Relation;

;

end;
func e_entrance N -> Relation equals :: E_SIEC:def 17

(( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N)));

correctness (( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N)));

coherence

(( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N))) is Relation;

;

func e_escape N -> Relation equals :: E_SIEC:def 18

(( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N)));

correctness (( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N)));

coherence

(( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N))) is Relation;

;

:: deftheorem defines e_entrance E_SIEC:def 17 :

for N being e_net holds e_entrance N = (( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N)));

for N being e_net holds e_entrance N = (( the escape of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the escape of N)));

:: deftheorem defines e_escape E_SIEC:def 18 :

for N being e_net holds e_escape N = (( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N)));

for N being e_net holds e_escape N = (( the entrance of N \ (id the carrier of N)) ~) \/ (id ( the carrier of N \ (rng the entrance of N)));

theorem :: E_SIEC:29

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 )

( (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:30

for N being e_net holds

( (e_entrance N) * ((e_entrance N) \ (id (e_shore N))) = {} & (e_escape N) * ((e_escape N) \ (id (e_shore N))) = {} )

( (e_entrance N) * ((e_entrance N) \ (id (e_shore N))) = {} & (e_escape N) * ((e_escape N) \ (id (e_shore N))) = {} )

proof end;

definition

let N be e_net;

coherence

(( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N))) is Relation;

;

end;
func e_adjac N -> Relation equals :: E_SIEC:def 19

(( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)));

correctness (( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)));

coherence

(( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N))) is Relation;

;

:: deftheorem defines e_adjac E_SIEC:def 19 :

for N being e_net holds e_adjac N = (( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)));

for N being e_net holds e_adjac N = (( the entrance of N \/ the escape of N) \ (id the carrier of N)) \/ (id ( the carrier of N \ (rng the entrance of N)));

theorem :: E_SIEC:31

for N being e_net holds

( e_adjac N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] )

( e_adjac N c= [:(e_shore N),(e_shore N):] & e_flow N c= [:(e_shore N),(e_shore N):] )

proof end;

theorem :: E_SIEC:32

for N being e_net holds

( (e_adjac N) * (e_adjac N) = e_adjac N & ((e_adjac N) \ (id (e_shore N))) * (e_adjac N) = {} & ((e_adjac N) \/ ((e_adjac N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) )

( (e_adjac N) * (e_adjac N) = e_adjac N & ((e_adjac N) \ (id (e_shore N))) * (e_adjac N) = {} & ((e_adjac N) \/ ((e_adjac N) ~)) \/ (id (e_shore N)) = (e_flow N) \/ ((e_flow N) ~) )

proof end;

theorem Th33: :: E_SIEC:33

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):] )

( ( 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 ;

coherence

( the escape of N \ (id the carrier of N)) ~ is Relation ;

coherence

( the entrance of N \ (id the carrier of N)) ~ is Relation ;

end;
coherence

( the escape of N \ (id the carrier of N)) ~ is Relation ;

coherence

( the entrance of N \ (id the carrier of N)) ~ is Relation ;

:: deftheorem defines s_pre E_SIEC:def 20 :

for N being G_Net holds s_pre N = ( the escape of N \ (id the carrier of N)) ~ ;

for N being G_Net holds s_pre N = ( the escape of N \ (id the carrier of N)) ~ ;

:: deftheorem defines s_post E_SIEC:def 21 :

for N being G_Net holds s_post N = ( the entrance of N \ (id the carrier of N)) ~ ;

for N being G_Net holds s_post N = ( the entrance of N \ (id the carrier of N)) ~ ;

theorem :: E_SIEC:34