:: FF_SIEC semantic presentation

definition

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

end;

:: deftheorem Def1 FF_SIEC:def 1 :

:: deftheorem Def2 defines chaos FF_SIEC:def 2 :

definition

let c₁, c₂ be set ;
assume E1: c₁ misses c₂ ;
canceled;
func PTempty_f_net c₁,c₂ -> strict Pnet equals :Def4: :: FF_SIEC:def 4
Net(# a₁,a₂,{} #);
correctness

proof end;

end;

:: deftheorem Def3 FF_SIEC:def 3 :

:: deftheorem Def4 defines PTempty_f_net FF_SIEC:def 4 :

definition

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

end;

:: deftheorem Def5 defines Tempty_f_net FF_SIEC:def 5 :

:: deftheorem Def6 defines Pempty_f_net FF_SIEC:def 6 :

definition

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

end;

:: deftheorem Def7 defines Tsingle_f_net FF_SIEC:def 7 :

:: deftheorem Def8 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 Def9 defines empty_f_net FF_SIEC:def 9 :

theorem Th1: :: FF_SIEC:1

canceled;

theorem Th2: :: FF_SIEC:2

for b₁, b₂ being set st b₁ misses b₂ holds
( the Places of (PTempty_f_net b₁,b₂) = b₁ & the Transitions of (PTempty_f_net b₁,b₂) = b₂ & the Flow of (PTempty_f_net b₁,b₂) = {} )

proof end;

theorem Th3: :: FF_SIEC:3

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

proof end;

theorem Th4: :: FF_SIEC:4

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

proof end;

theorem Th5: :: FF_SIEC:5

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

proof end;

theorem Th6: :: FF_SIEC:6

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

proof end;

theorem Th7: :: FF_SIEC:7

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

proof end;

theorem Th8: :: FF_SIEC:8

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

theorem Th9: :: FF_SIEC:9

canceled;

theorem Th10: :: FF_SIEC:10

canceled;

theorem Th11: :: FF_SIEC:11

for b₁, b₂ being set
for b₃ being Pnet holds
( ( [b₁,b₂] in the Flow of b₃ & b₁ in the Transitions of b₃ implies ( not b₁ in the Places of b₃ & not b₂ in the Transitions of b₃ & b₂ in the Places of b₃ ) ) & ( [b₁,b₂] in the Flow of b₃ & b₂ in the Transitions of b₃ implies ( not b₂ in the Places of b₃ & not b₁ in the Transitions of b₃ & b₁ in the Places of b₃ ) ) & ( [b₁,b₂] in the Flow of b₃ & b₁ in the Places of b₃ implies ( not b₂ in the Places of b₃ & not b₁ in the Transitions of b₃ & b₂ in the Transitions of b₃ ) ) & ( [b₁,b₂] in the Flow of b₃ & b₂ in the Places of b₃ implies ( not b₁ in the Places of b₃ & not b₂ in the Transitions of b₃ & b₁ in the Transitions of b₃ ) ) )

proof end;

theorem Th12: :: FF_SIEC:12

for b₁ being Pnet holds chaos b₁ <> {}

proof end;

theorem Th13: :: FF_SIEC:13

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

proof end;

theorem Th14: :: FF_SIEC:14

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

proof end;

Lemma5: for b₁, b₂, b₃, b₄ being set st b₂ misses b₄ & b₁ c= b₂ & b₃ c= b₄ holds
b₁ misses b₃

proof end;

theorem Th15: :: FF_SIEC:15

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

proof end;

theorem Th16: :: FF_SIEC:16

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

proof end;

theorem Th17: :: FF_SIEC:17

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

proof end;

theorem Th18: :: FF_SIEC:18

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

proof end;

theorem Th19: :: FF_SIEC:19

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

proof end;

theorem Th20: :: FF_SIEC:20

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

proof end;

theorem Th21: :: FF_SIEC:21

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

proof end;

definition

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

end;

:: deftheorem Def10 defines f_enter FF_SIEC:def 10 :

:: deftheorem Def11 defines f_exit FF_SIEC:def 11 :

theorem Th22: :: FF_SIEC:22

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

proof end;

theorem Th23: :: FF_SIEC:23

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

proof end;

theorem Th24: :: FF_SIEC:24

for b₁ being Pnet holds
( (f_exit b₁) * (f_exit b₁) = f_exit b₁ & (f_exit b₁) * (f_enter b₁) = f_exit b₁ & (f_enter b₁) * (f_enter b₁) = f_enter b₁ & (f_enter b₁) * (f_exit b₁) = f_enter b₁ )

proof end;

theorem Th25: :: FF_SIEC:25

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

proof end;

definition

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

end;

:: deftheorem Def12 defines f_prox FF_SIEC:def 12 :

:: deftheorem Def13 defines f_flow FF_SIEC:def 13 :

theorem Th26: :: FF_SIEC:26

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

proof end;

definition

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

end;

:: deftheorem Def14 defines f_places FF_SIEC:def 14 :

:: deftheorem Def15 defines f_transitions FF_SIEC:def 15 :

:: deftheorem Def16 defines f_pre FF_SIEC:def 16 :

:: deftheorem Def17 defines f_post FF_SIEC:def 17 :

theorem Th27: :: FF_SIEC:27

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

proof end;

theorem Th28: :: FF_SIEC:28

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

theorem Th29: :: FF_SIEC:29

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

proof end;

definition

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

end;

:: deftheorem Def18 defines f_entrance FF_SIEC:def 18 :

:: deftheorem Def19 defines f_escape FF_SIEC:def 19 :

theorem Th30: :: FF_SIEC:30

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

proof end;

theorem Th31: :: FF_SIEC:31

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

proof end;

theorem Th32: :: FF_SIEC:32

for b₁ being Pnet holds
( (f_escape b₁) * (f_escape b₁) = f_escape b₁ & (f_escape b₁) * (f_entrance b₁) = f_escape b₁ & (f_entrance b₁) * (f_entrance b₁) = f_entrance b₁ & (f_entrance b₁) * (f_escape b₁) = f_entrance b₁ )

proof end;

theorem Th33: :: FF_SIEC:33

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

proof end;

notation

let c₁ be Pnet;
synonym f_circulation c₁ for f_flow c₁;

end;

definition

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

end;

:: deftheorem Def20 defines f_adjac FF_SIEC:def 20 :

theorem Th34: :: FF_SIEC:34

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

proof end;