:: Definitions of Petri Net - Part I
:: by Waldemar Korczy\'nski
::
:: Received January 31, 1992
:: Copyright (c) 1992 Association of Mizar Users
:: 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 :: FF_SIEC:1
canceled;
theorem :: FF_SIEC:2
theorem :: FF_SIEC:3
theorem :: FF_SIEC:4
theorem :: FF_SIEC:5
theorem :: FF_SIEC:6
theorem :: FF_SIEC:7
theorem :: FF_SIEC:8
canceled;
theorem :: FF_SIEC:9
canceled;
theorem :: FF_SIEC:10
canceled;
theorem Th11: :: FF_SIEC:11
theorem :: FF_SIEC:12
canceled;
theorem Th13: :: FF_SIEC:13
theorem Th14: :: FF_SIEC:14
Lm1:
for A, B, C, D being set st B misses D & A c= B & C c= D holds
A misses C
theorem Th15: :: FF_SIEC:15
theorem Th16: :: FF_SIEC:16
theorem Th17: :: FF_SIEC:17
theorem Th18: :: FF_SIEC:18
theorem Th19: :: FF_SIEC:19
theorem Th20: :: FF_SIEC:20
theorem Th21: :: FF_SIEC:21
:: deftheorem defines f_enter FF_SIEC:def 10 :
:: deftheorem defines f_exit FF_SIEC:def 11 :
theorem :: FF_SIEC:22
theorem :: FF_SIEC:23
theorem :: FF_SIEC:24
theorem :: FF_SIEC:25
:: deftheorem defines f_prox FF_SIEC:def 12 :
:: deftheorem defines f_flow FF_SIEC:def 13 :
theorem :: FF_SIEC:26
:: 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 :: FF_SIEC:27
theorem :: FF_SIEC:28
canceled;
theorem :: FF_SIEC:29
:: deftheorem defines f_entrance FF_SIEC:def 18 :
:: deftheorem defines f_escape FF_SIEC:def 19 :
theorem :: FF_SIEC:30
theorem :: FF_SIEC:31
theorem :: FF_SIEC:32
theorem :: FF_SIEC:33
:: deftheorem defines f_adjac FF_SIEC:def 20 :
theorem :: FF_SIEC:34