:: Basic Petri Net Concepts.Place/Transition Net Structure, Deadlocks, Traps, Dual Nets
:: by Pauline N. Kawamoto, Yasushi Fuwa and Yatsuka Nakamura
::
:: Received November 27, 1992
:: Copyright (c) 1992 Association of Mizar Users
:: deftheorem defines *' PETRI:def 1 :
:: deftheorem defines *' PETRI:def 2 :
theorem :: PETRI:1
theorem Th2: :: PETRI:2
theorem :: PETRI:3
theorem Th4: :: PETRI:4
:: deftheorem defines *' PETRI:def 3 :
:: deftheorem defines *' PETRI:def 4 :
theorem :: PETRI:5
theorem Th6: :: PETRI:6
theorem :: PETRI:7
theorem Th8: :: PETRI:8
theorem :: PETRI:9
theorem :: PETRI:10
theorem :: PETRI:11
theorem :: PETRI:12
:: deftheorem defines Deadlock-like PETRI:def 5 :
:: deftheorem defines With_Deadlocks PETRI:def 6 :
:: deftheorem defines Trap-like PETRI:def 7 :
:: deftheorem defines With_Traps PETRI:def 8 :
:: deftheorem defines .: PETRI:def 9 :
theorem :: PETRI:13
theorem :: PETRI:14
:: 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: :: PETRI:15
theorem Th16: :: PETRI:16
theorem :: PETRI:17
theorem :: PETRI:18
theorem :: PETRI:19
theorem :: PETRI:20