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