:: Definitions of Petri Net - Part II
:: by Waldemar Korczy\'nski
::
:: Received January 31, 1992
:: Copyright (c) 1992 Association of Mizar Users
:: deftheorem E_SIEC:def 1 :
canceled;
:: deftheorem Def2 defines GG E_SIEC:def 2 :
:: deftheorem Def3 defines EE E_SIEC:def 3 :
theorem :: E_SIEC:1
theorem Th2: :: E_SIEC:2
theorem Th3: :: E_SIEC:3
theorem :: E_SIEC:4
theorem :: E_SIEC:5
canceled;
theorem :: E_SIEC:6
canceled;
theorem :: E_SIEC:7
canceled;
theorem :: E_SIEC:8
:: 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 :: E_SIEC:9
canceled;
theorem :: E_SIEC:10
canceled;
theorem :: E_SIEC:11
theorem :: E_SIEC:12
:: deftheorem defines Psingle_e_net E_SIEC:def 7 :
:: deftheorem defines Tsingle_e_net E_SIEC:def 8 :
theorem :: E_SIEC:13
theorem :: E_SIEC:14
theorem Th15: :: E_SIEC:15
:: deftheorem defines PTempty_e_net E_SIEC:def 9 :
theorem Th16: :: E_SIEC:16
theorem Th17: :: E_SIEC:17
theorem Th18: :: E_SIEC:18
theorem Th19: :: E_SIEC:19
theorem Th20: :: E_SIEC:20
theorem :: E_SIEC:21
:: deftheorem defines e_Places E_SIEC:def 10 :
:: deftheorem defines e_Transitions E_SIEC:def 11 :
theorem :: E_SIEC:22
canceled;
theorem Th23: :: E_SIEC:23
theorem Th24: :: E_SIEC:24
:: deftheorem defines e_Flow E_SIEC:def 12 :
theorem :: E_SIEC:25
:: 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 :: E_SIEC:26
canceled;
theorem :: E_SIEC:27
canceled;
theorem :: E_SIEC:28
:: 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 :: E_SIEC:29
theorem :: E_SIEC:30
theorem Th31: :: E_SIEC:31
theorem Th32: :: E_SIEC:32
theorem Th33: :: E_SIEC:33
theorem :: E_SIEC:34
theorem Th35: :: E_SIEC:35
theorem Th36: :: E_SIEC:36
:: deftheorem E_SIEC:def 20 :
canceled;
:: deftheorem defines e_entrance E_SIEC:def 21 :
:: deftheorem defines e_escape E_SIEC:def 22 :
theorem :: E_SIEC:37
theorem :: E_SIEC:38
:: deftheorem E_SIEC:def 23 :
canceled;
:: deftheorem defines e_adjac E_SIEC:def 24 :
theorem :: E_SIEC:39
theorem :: E_SIEC:40
theorem Th41: :: E_SIEC:41
:: deftheorem defines s_pre E_SIEC:def 25 :
:: deftheorem defines s_post E_SIEC:def 26 :
theorem :: E_SIEC:42