begin
:: deftheorem defines *' PETRI:def 1 :
:: deftheorem defines *' PETRI:def 2 :
theorem
theorem Th2:
theorem
theorem Th4:
:: deftheorem defines *' PETRI:def 3 :
:: deftheorem defines *' PETRI:def 4 :
theorem
theorem Th6:
theorem
theorem Th8:
theorem
theorem
theorem
theorem
begin
:: deftheorem defines Deadlock-like PETRI:def 5 :
:: deftheorem defines With_Deadlocks PETRI:def 6 :
begin
:: deftheorem defines Trap-like PETRI:def 7 :
:: deftheorem defines With_Traps PETRI:def 8 :
begin
:: deftheorem defines .: PETRI:def 9 :
theorem
theorem
:: deftheorem defines .: PETRI:def 10 :
:: deftheorem defines .: PETRI:def 11 :
:: deftheorem defines .: PETRI:def 12 :
:: deftheorem defines .: PETRI:def 13 :
:: deftheorem defines .: PETRI:def 14 :
:: deftheorem defines .: PETRI:def 15 :
:: deftheorem defines .: PETRI:def 16 :
:: deftheorem defines .: PETRI:def 17 :
theorem Th15:
theorem Th16:
theorem
theorem
theorem
theorem