begin
:: 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 :
:: deftheorem defines Tempty_f_net FF_SIEC:def 5 :
:: deftheorem defines Pempty_f_net FF_SIEC:def 6 :
:: deftheorem defines Tsingle_f_net FF_SIEC:def 7 :
:: deftheorem defines Psingle_f_net FF_SIEC:def 8 :
:: deftheorem defines empty_f_net FF_SIEC:def 9 :
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 :
:: deftheorem defines f_exit FF_SIEC:def 11 :
theorem
theorem
theorem
theorem
:: deftheorem defines f_prox FF_SIEC:def 12 :
:: deftheorem defines f_flow FF_SIEC:def 13 :
theorem
:: 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
theorem
canceled;
theorem
:: deftheorem defines f_entrance FF_SIEC:def 18 :
:: deftheorem defines f_escape FF_SIEC:def 19 :
theorem
theorem
theorem
theorem
:: deftheorem defines f_adjac FF_SIEC:def 20 :
theorem