:: FF_SIEC semantic presentation

definition

let N be Net ;
canceled;
func chaos N -> set equals :: FF_SIEC:def 2
(Elements N) \/ {(Elements N)};
correctness ;

end;

:: deftheorem FF_SIEC:def 1 :

:: deftheorem defines chaos FF_SIEC:def 2 :

definition

let X, Y be set ;
assume A1: X misses Y ;
canceled;
func PTempty_f_net X,Y -> strict Pnet equals :Def4: :: FF_SIEC:def 4
Net(# X,Y,{} #);
correctness

proof end;

end;

:: deftheorem FF_SIEC:def 3 :

:: deftheorem Def4 defines PTempty_f_net FF_SIEC:def 4 :

definition

let X be set ;
func Tempty_f_net X -> strict Pnet equals :: FF_SIEC:def 5
PTempty_f_net X,{} ;
correctness ;
func Pempty_f_net X -> strict Pnet equals :: FF_SIEC:def 6
PTempty_f_net {} ,X;
correctness ;

end;

:: deftheorem defines Tempty_f_net FF_SIEC:def 5 :

:: deftheorem defines Pempty_f_net FF_SIEC:def 6 :

definition

let x be set ;
func Tsingle_f_net x -> strict Pnet equals :: FF_SIEC:def 7
PTempty_f_net {} ,{x};
correctness ;
func Psingle_f_net x -> strict Pnet equals :: FF_SIEC:def 8
PTempty_f_net {x},{} ;
correctness ;

end;

:: deftheorem defines Tsingle_f_net FF_SIEC:def 7 :

:: deftheorem defines Psingle_f_net FF_SIEC:def 8 :

definition

func empty_f_net -> strict Pnet equals :: FF_SIEC:def 9
PTempty_f_net {} ,{} ;
correctness ;

end;

:: deftheorem defines empty_f_net FF_SIEC:def 9 :

theorem :: FF_SIEC:1

canceled;

theorem :: FF_SIEC:2

for X, Y being set st X misses Y holds
( the Places of (PTempty_f_net X,Y) = X & the Transitions of (PTempty_f_net X,Y) = Y & the Flow of (PTempty_f_net X,Y) = {} )

proof end;

theorem :: FF_SIEC:3

for X being set holds
( the Places of (Tempty_f_net X) = X & the Transitions of (Tempty_f_net X) = {} & the Flow of (Tempty_f_net X) = {} )

proof end;

theorem :: FF_SIEC:4

for X being set holds
( the Places of (Pempty_f_net X) = {} & the Transitions of (Pempty_f_net X) = X & the Flow of (Pempty_f_net X) = {} )

proof end;

theorem :: FF_SIEC:5

for x being set holds
( the Places of (Tsingle_f_net x) = {} & the Transitions of (Tsingle_f_net x) = {x} & the Flow of (Tsingle_f_net x) = {} )

proof end;

theorem :: FF_SIEC:6

for x being set holds
( the Places of (Psingle_f_net x) = {x} & the Transitions of (Psingle_f_net x) = {} & the Flow of (Psingle_f_net x) = {} )

proof end;

theorem :: FF_SIEC:7

( the Places of empty_f_net = {} & the Transitions of empty_f_net = {} & the Flow of empty_f_net = {} )

proof end;

theorem :: FF_SIEC:8

for M being Pnet holds
( the Places of M c= Elements M & the Transitions of M c= Elements M ) by NET_1:4, NET_1:5;

theorem :: FF_SIEC:9

canceled;

theorem :: FF_SIEC:10

canceled;

theorem Th11: :: FF_SIEC:11

for x, y being set
for M being Pnet holds
( ( [x,y] in the Flow of M & x in the Transitions of M implies ( not x in the Places of M & not y in the Transitions of M & y in the Places of M ) ) & ( [x,y] in the Flow of M & y in the Transitions of M implies ( not y in the Places of M & not x in the Transitions of M & x in the Places of M ) ) & ( [x,y] in the Flow of M & x in the Places of M implies ( not y in the Places of M & not x in the Transitions of M & y in the Transitions of M ) ) & ( [x,y] in the Flow of M & y in the Places of M implies ( not x in the Places of M & not y in the Transitions of M & x in the Transitions of M ) ) )

proof end;

theorem :: FF_SIEC:12

for M being Pnet holds chaos M <> {}

proof end;

theorem Th13: :: FF_SIEC:13

for M being Pnet holds
( the Flow of M c= [:(Elements M),(Elements M):] & the Flow of M ~ c= [:(Elements M),(Elements M):] )

proof end;

theorem Th14: :: FF_SIEC:14

for M being Pnet holds
( rng (the Flow of M | the Transitions of M) c= the Places of M & rng ((the Flow of M ~ ) | the Transitions of M) c= the Places of M & dom (the Flow of M | the Transitions of M) c= the Transitions of M & dom ((the Flow of M ~ ) | the Transitions of M) c= the Transitions of M & rng (the Flow of M | the Places of M) c= the Transitions of M & rng ((the Flow of M ~ ) | the Places of M) c= the Transitions of M & dom (the Flow of M | the Places of M) c= the Places of M & dom ((the Flow of M ~ ) | the Places of M) c= the Places of M & rng (id the Transitions of M) c= the Transitions of M & dom (id the Transitions of M) c= the Transitions of M & rng (id the Places of M) c= the Places of M & dom (id the Places of M) c= the Places of M )

proof end;

Lm1: for A, B, C, D being set st B misses D & A c= B & C c= D holds
A misses C

proof end;

theorem Th15: :: FF_SIEC:15

for M being Pnet holds
( rng (the Flow of M | the Transitions of M) misses dom (the Flow of M | the Transitions of M) & rng (the Flow of M | the Transitions of M) misses dom ((the Flow of M ~ ) | the Transitions of M) & rng (the Flow of M | the Transitions of M) misses dom (id the Transitions of M) & rng ((the Flow of M ~ ) | the Transitions of M) misses dom (the Flow of M | the Transitions of M) & rng ((the Flow of M ~ ) | the Transitions of M) misses dom ((the Flow of M ~ ) | the Transitions of M) & rng ((the Flow of M ~ ) | the Transitions of M) misses dom (id the Transitions of M) & dom (the Flow of M | the Transitions of M) misses rng (the Flow of M | the Transitions of M) & dom (the Flow of M | the Transitions of M) misses rng ((the Flow of M ~ ) | the Transitions of M) & dom (the Flow of M | the Transitions of M) misses rng (id the Places of M) & dom ((the Flow of M ~ ) | the Transitions of M) misses rng (the Flow of M | the Transitions of M) & dom ((the Flow of M ~ ) | the Transitions of M) misses rng ((the Flow of M ~ ) | the Transitions of M) & dom ((the Flow of M ~ ) | the Transitions of M) misses rng (id the Places of M) & rng (the Flow of M | the Places of M) misses dom (the Flow of M | the Places of M) & rng (the Flow of M | the Places of M) misses dom ((the Flow of M ~ ) | the Places of M) & rng (the Flow of M | the Places of M) misses dom (id the Places of M) & rng ((the Flow of M ~ ) | the Places of M) misses dom (the Flow of M | the Places of M) & rng ((the Flow of M ~ ) | the Places of M) misses dom ((the Flow of M ~ ) | the Places of M) & rng ((the Flow of M ~ ) | the Places of M) misses dom (id the Places of M) & dom (the Flow of M | the Places of M) misses rng (the Flow of M | the Places of M) & dom (the Flow of M | the Places of M) misses rng ((the Flow of M ~ ) | the Places of M) & dom (the Flow of M | the Places of M) misses rng (id the Transitions of M) & dom ((the Flow of M ~ ) | the Places of M) misses rng (the Flow of M | the Places of M) & dom ((the Flow of M ~ ) | the Places of M) misses rng ((the Flow of M ~ ) | the Places of M) & dom ((the Flow of M ~ ) | the Places of M) misses rng (id the Transitions of M) )

proof end;

theorem Th16: :: FF_SIEC:16

for M being Pnet holds
( (the Flow of M | the Transitions of M) * (the Flow of M | the Transitions of M) = {} & ((the Flow of M ~ ) | the Transitions of M) * ((the Flow of M ~ ) | the Transitions of M) = {} & (the Flow of M | the Transitions of M) * ((the Flow of M ~ ) | the Transitions of M) = {} & ((the Flow of M ~ ) | the Transitions of M) * (the Flow of M | the Transitions of M) = {} & (the Flow of M | the Places of M) * (the Flow of M | the Places of M) = {} & ((the Flow of M ~ ) | the Places of M) * ((the Flow of M ~ ) | the Places of M) = {} & (the Flow of M | the Places of M) * ((the Flow of M ~ ) | the Places of M) = {} & ((the Flow of M ~ ) | the Places of M) * (the Flow of M | the Places of M) = {} )

proof end;

theorem Th17: :: FF_SIEC:17

for M being Pnet holds
( (the Flow of M | the Transitions of M) * (id the Places of M) = the Flow of M | the Transitions of M & ((the Flow of M ~ ) | the Transitions of M) * (id the Places of M) = (the Flow of M ~ ) | the Transitions of M & (id the Transitions of M) * (the Flow of M | the Transitions of M) = the Flow of M | the Transitions of M & (id the Transitions of M) * ((the Flow of M ~ ) | the Transitions of M) = (the Flow of M ~ ) | the Transitions of M & (the Flow of M | the Places of M) * (id the Transitions of M) = the Flow of M | the Places of M & ((the Flow of M ~ ) | the Places of M) * (id the Transitions of M) = (the Flow of M ~ ) | the Places of M & (id the Places of M) * (the Flow of M | the Places of M) = the Flow of M | the Places of M & (id the Places of M) * ((the Flow of M ~ ) | the Places of M) = (the Flow of M ~ ) | the Places of M & (the Flow of M | the Places of M) * (id the Transitions of M) = the Flow of M | the Places of M & ((the Flow of M ~ ) | the Places of M) * (id the Transitions of M) = (the Flow of M ~ ) | the Places of M & (id the Transitions of M) * (the Flow of M | the Places of M) = {} & (id the Transitions of M) * ((the Flow of M ~ ) | the Places of M) = {} & (the Flow of M | the Places of M) * (id the Places of M) = {} & ((the Flow of M ~ ) | the Places of M) * (id the Places of M) = {} & (id the Places of M) * (the Flow of M | the Transitions of M) = {} & (id the Places of M) * ((the Flow of M ~ ) | the Transitions of M) = {} & (the Flow of M | the Transitions of M) * (id the Transitions of M) = {} & ((the Flow of M ~ ) | the Transitions of M) * (id the Transitions of M) = {} )

proof end;

theorem Th18: :: FF_SIEC:18

for M being Pnet holds
( (the Flow of M ~ ) | the Transitions of M misses id (Elements M) & the Flow of M | the Transitions of M misses id (Elements M) & (the Flow of M ~ ) | the Places of M misses id (Elements M) & the Flow of M | the Places of M misses id (Elements M) )

proof end;

theorem Th19: :: FF_SIEC:19

for M being Pnet holds
( (((the Flow of M ~ ) | the Transitions of M) \/ (id the Places of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Transitions of M & ((the Flow of M | the Transitions of M) \/ (id the Places of M)) \ (id (Elements M)) = the Flow of M | the Transitions of M & (((the Flow of M ~ ) | the Places of M) \/ (id the Places of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Places of M & ((the Flow of M | the Places of M) \/ (id the Places of M)) \ (id (Elements M)) = the Flow of M | the Places of M & (((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Places of M & ((the Flow of M | the Places of M) \/ (id the Transitions of M)) \ (id (Elements M)) = the Flow of M | the Places of M & (((the Flow of M ~ ) | the Transitions of M) \/ (id the Transitions of M)) \ (id (Elements M)) = (the Flow of M ~ ) | the Transitions of M & ((the Flow of M | the Transitions of M) \/ (id the Transitions of M)) \ (id (Elements M)) = the Flow of M | the Transitions of M )

proof end;

theorem Th20: :: FF_SIEC:20

for M being Pnet holds
( (the Flow of M | the Places of M) ~ = (the Flow of M ~ ) | the Transitions of M & (the Flow of M | the Transitions of M) ~ = (the Flow of M ~ ) | the Places of M )

proof end;

theorem Th21: :: FF_SIEC:21

for M being Pnet holds
( (the Flow of M | the Places of M) \/ (the Flow of M | the Transitions of M) = the Flow of M & (the Flow of M | the Transitions of M) \/ (the Flow of M | the Places of M) = the Flow of M & ((the Flow of M | the Places of M) ~ ) \/ ((the Flow of M | the Transitions of M) ~ ) = the Flow of M ~ & ((the Flow of M | the Transitions of M) ~ ) \/ ((the Flow of M | the Places of M) ~ ) = the Flow of M ~ )

proof end;

definition

let M be Pnet;
func f_enter M -> Relation equals :: FF_SIEC:def 10
((the Flow of M ~ ) | the Transitions of M) \/ (id the Places of M);
correctness ;
func f_exit M -> Relation equals :: FF_SIEC:def 11
(the Flow of M | the Transitions of M) \/ (id the Places of M);
correctness ;

end;

:: deftheorem defines f_enter FF_SIEC:def 10 :

:: deftheorem defines f_exit FF_SIEC:def 11 :

theorem :: FF_SIEC:22

for M being Pnet holds
( f_exit M c= [:(Elements M),(Elements M):] & f_enter M c= [:(Elements M),(Elements M):] )

proof end;

theorem :: FF_SIEC:23

for M being Pnet holds
( dom (f_exit M) c= Elements M & rng (f_exit M) c= Elements M & dom (f_enter M) c= Elements M & rng (f_enter M) c= Elements M )

proof end;

theorem :: FF_SIEC:24

for M being Pnet holds
( (f_exit M) * (f_exit M) = f_exit M & (f_exit M) * (f_enter M) = f_exit M & (f_enter M) * (f_enter M) = f_enter M & (f_enter M) * (f_exit M) = f_enter M )

proof end;

theorem :: FF_SIEC:25

for M being Pnet holds
( (f_exit M) * ((f_exit M) \ (id (Elements M))) = {} & (f_enter M) * ((f_enter M) \ (id (Elements M))) = {} )

proof end;

definition

let M be Pnet;
func f_prox M -> Relation equals :: FF_SIEC:def 12
((the Flow of M | the Places of M) \/ ((the Flow of M ~ ) | the Places of M)) \/ (id the Places of M);
correctness ;
func f_flow M -> Relation equals :: FF_SIEC:def 13
the Flow of M \/ (id (Elements M));
correctness ;

end;

:: deftheorem defines f_prox FF_SIEC:def 12 :

:: deftheorem defines f_flow FF_SIEC:def 13 :

theorem :: FF_SIEC:26

for M being Pnet holds
( (f_prox M) * (f_prox M) = f_prox M & ((f_prox M) \ (id (Elements M))) * (f_prox M) = {} & ((f_prox M) \/ ((f_prox M) ~ )) \/ (id (Elements M)) = (f_flow M) \/ ((f_flow M) ~ ) )

proof end;

definition

let M be Pnet;
func f_places M -> set equals :: FF_SIEC:def 14
the Places of M;
correctness ;
func f_transitions M -> set equals :: FF_SIEC:def 15
the Transitions of M;
correctness ;
func f_pre M -> Relation equals :: FF_SIEC:def 16
the Flow of M | the Transitions of M;
correctness ;
func f_post M -> Relation equals :: FF_SIEC:def 17
(the Flow of M ~ ) | the Transitions of M;
correctness ;

end;

:: deftheorem defines f_places FF_SIEC:def 14 :

:: deftheorem defines f_transitions FF_SIEC:def 15 :

:: deftheorem defines f_pre FF_SIEC:def 16 :

:: deftheorem defines f_post FF_SIEC:def 17 :

theorem :: FF_SIEC:27

for M being Pnet holds
( f_pre M c= [:(f_transitions M),(f_places M):] & f_post M c= [:(f_transitions M),(f_places M):] )

proof end;

theorem :: FF_SIEC:28

for M being Pnet holds f_places M misses f_transitions M by NET_1:def 1;

theorem :: FF_SIEC:29

for M being Pnet holds
( f_prox M c= [:(Elements M),(Elements M):] & f_flow M c= [:(Elements M),(Elements M):] )

proof end;

definition

let M be Pnet;
func f_entrance M -> Relation equals :: FF_SIEC:def 18
((the Flow of M ~ ) | the Places of M) \/ (id the Transitions of M);
correctness ;
func f_escape M -> Relation equals :: FF_SIEC:def 19
(the Flow of M | the Places of M) \/ (id the Transitions of M);
correctness ;

end;

:: deftheorem defines f_entrance FF_SIEC:def 18 :

:: deftheorem defines f_escape FF_SIEC:def 19 :

theorem :: FF_SIEC:30

for M being Pnet holds
( f_escape M c= [:(Elements M),(Elements M):] & f_entrance M c= [:(Elements M),(Elements M):] )

proof end;

theorem :: FF_SIEC:31

for M being Pnet holds
( dom (f_escape M) c= Elements M & rng (f_escape M) c= Elements M & dom (f_entrance M) c= Elements M & rng (f_entrance M) c= Elements M )

proof end;

theorem :: FF_SIEC:32

for M being Pnet holds
( (f_escape M) * (f_escape M) = f_escape M & (f_escape M) * (f_entrance M) = f_escape M & (f_entrance M) * (f_entrance M) = f_entrance M & (f_entrance M) * (f_escape M) = f_entrance M )

proof end;

theorem :: FF_SIEC:33

for M being Pnet holds
( (f_escape M) * ((f_escape M) \ (id (Elements M))) = {} & (f_entrance M) * ((f_entrance M) \ (id (Elements M))) = {} )

proof end;

notation

let M be Pnet;
synonym f_circulation M for f_flow M;

end;

definition

let M be Pnet;
func f_adjac M -> Relation equals :: FF_SIEC:def 20
((the Flow of M | the Transitions of M) \/ ((the Flow of M ~ ) | the Transitions of M)) \/ (id the Transitions of M);
correctness ;

end;

:: deftheorem defines f_adjac FF_SIEC:def 20 :

theorem :: FF_SIEC:34

for M being Pnet holds
( (f_adjac M) * (f_adjac M) = f_adjac M & ((f_adjac M) \ (id (Elements M))) * (f_adjac M) = {} & ((f_adjac M) \/ ((f_adjac M) ~ )) \/ (id (Elements M)) = (f_circulation M) \/ ((f_circulation M) ~ ) )

proof end;