begin
definition
let X,
Y be
set ;
assume A1:
X misses Y
;
canceled;canceled;canceled;func PTempty_f_net X,
Y -> strict Pnet equals :
Def4:
PT_net_Str(#
X,
Y,
({} X,Y),
({} Y,X) #);
correctness
coherence
PT_net_Str(# X,Y,({} X,Y),({} Y,X) #) is strict Pnet;
end;
:: deftheorem FF_SIEC:def 1 :
canceled;
:: deftheorem FF_SIEC:def 2 :
canceled;
:: deftheorem FF_SIEC:def 3 :
canceled;
:: deftheorem Def4 defines PTempty_f_net FF_SIEC:def 4 :
for X, Y being set st X misses Y holds
PTempty_f_net X,Y = PT_net_Str(# X,Y,({} X,Y),({} Y,X) #);
:: deftheorem defines Tempty_f_net FF_SIEC:def 5 :
for X being set holds Tempty_f_net X = PTempty_f_net X,{} ;
:: deftheorem defines Pempty_f_net FF_SIEC:def 6 :
for X being set holds Pempty_f_net X = PTempty_f_net {} ,X;
:: deftheorem defines Tsingle_f_net FF_SIEC:def 7 :
for x being set holds Tsingle_f_net x = PTempty_f_net {} ,{x};
:: deftheorem defines Psingle_f_net FF_SIEC:def 8 :
for x being set holds Psingle_f_net x = PTempty_f_net {x},{} ;
:: deftheorem defines empty_f_net FF_SIEC:def 9 :
empty_f_net = PTempty_f_net {} ,{} ;
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th11:
theorem
canceled;
theorem Th13:
theorem Th14:
Lm1:
for A, B, C, D being set st B misses D & A c= B & C c= D holds
A misses C
theorem Th15:
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
:: deftheorem defines f_enter FF_SIEC:def 10 :
for M being Pnet holds f_enter M = (((Flow M) ~ ) | the carrier' of M) \/ (id the carrier of M);
:: deftheorem defines f_exit FF_SIEC:def 11 :
for M being Pnet holds f_exit M = ((Flow M) | the carrier' of M) \/ (id the carrier of M);
theorem
theorem
theorem
theorem
:: deftheorem defines f_prox FF_SIEC:def 12 :
for M being Pnet holds f_prox M = (((Flow M) | the carrier of M) \/ (((Flow M) ~ ) | the carrier of M)) \/ (id the carrier of M);
:: deftheorem defines f_flow FF_SIEC:def 13 :
for M being Pnet holds f_flow M = (Flow M) \/ (id (Elements M));
theorem
:: deftheorem defines f_places FF_SIEC:def 14 :
for M being Pnet holds f_places M = the carrier of M;
:: deftheorem defines f_transitions FF_SIEC:def 15 :
for M being Pnet holds f_transitions M = the carrier' of M;
:: deftheorem defines f_pre FF_SIEC:def 16 :
for M being Pnet holds f_pre M = (Flow M) | the carrier' of M;
:: deftheorem defines f_post FF_SIEC:def 17 :
for M being Pnet holds f_post M = ((Flow M) ~ ) | the carrier' of M;
theorem
theorem
canceled;
theorem
:: deftheorem defines f_entrance FF_SIEC:def 18 :
for M being Pnet holds f_entrance M = (((Flow M) ~ ) | the carrier of M) \/ (id the carrier' of M);
:: deftheorem defines f_escape FF_SIEC:def 19 :
for M being Pnet holds f_escape M = ((Flow M) | the carrier of M) \/ (id the carrier' of M);
theorem
theorem
theorem
theorem
:: deftheorem defines f_adjac FF_SIEC:def 20 :
for M being Pnet holds f_adjac M = (((Flow M) | the carrier' of M) \/ (((Flow M) ~ ) | the carrier' of M)) \/ (id the carrier' of M);
theorem