begin
:: deftheorem E_SIEC:def 1 :
canceled;
:: deftheorem Def2 defines GG E_SIEC:def 2 :
:: deftheorem Def3 defines EE E_SIEC:def 3 :
theorem
theorem Th2:
theorem Th3:
theorem
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem defines empty_e_net E_SIEC:def 4 :
:: deftheorem defines Tempty_e_net E_SIEC:def 5 :
:: deftheorem defines Pempty_e_net E_SIEC:def 6 :
theorem
canceled;
theorem
canceled;
theorem
theorem
:: deftheorem defines Psingle_e_net E_SIEC:def 7 :
:: deftheorem defines Tsingle_e_net E_SIEC:def 8 :
theorem
theorem
theorem Th15:
:: deftheorem defines PTempty_e_net E_SIEC:def 9 :
theorem Th16:
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem
:: deftheorem defines e_Places E_SIEC:def 10 :
:: deftheorem defines e_Transitions E_SIEC:def 11 :
theorem
canceled;
theorem Th23:
theorem Th24:
:: deftheorem defines e_Flow E_SIEC:def 12 :
theorem
:: deftheorem E_SIEC:def 13 :
canceled;
:: deftheorem E_SIEC:def 14 :
canceled;
:: deftheorem defines e_pre E_SIEC:def 15 :
:: deftheorem defines e_post E_SIEC:def 16 :
theorem
canceled;
theorem
canceled;
theorem
:: deftheorem defines e_shore E_SIEC:def 17 :
:: deftheorem defines e_prox E_SIEC:def 18 :
:: deftheorem defines e_flow E_SIEC:def 19 :
theorem
theorem
theorem Th31:
theorem Th32:
theorem Th33:
theorem
theorem Th35:
theorem Th36:
:: deftheorem E_SIEC:def 20 :
canceled;
:: deftheorem defines e_entrance E_SIEC:def 21 :
:: deftheorem defines e_escape E_SIEC:def 22 :
theorem
theorem
:: deftheorem E_SIEC:def 23 :
canceled;
:: deftheorem defines e_adjac E_SIEC:def 24 :
theorem
theorem
theorem Th41:
:: deftheorem defines s_pre E_SIEC:def 25 :
:: deftheorem defines s_post E_SIEC:def 26 :
theorem