begin
:: deftheorem Def1 defines with_S-T_arc PETRI:def 1 :
for N being PT_net_Str holds
( N is with_S-T_arc iff not the S-T_Arcs of N is empty );
:: deftheorem Def2 defines with_T-S_arc PETRI:def 2 :
for N being PT_net_Str holds
( N is with_T-S_arc iff not the T-S_Arcs of N is empty );
definition
func TrivialPetriNet -> PT_net_Str equals
PT_net_Str(#
{{}},
{{}},
([#] ({{}},{{}})),
([#] ({{}},{{}})) #);
coherence
PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})) #) is PT_net_Str
;
end;
:: deftheorem defines TrivialPetriNet PETRI:def 3 :
TrivialPetriNet = PT_net_Str(# {{}},{{}},([#] ({{}},{{}})),([#] ({{}},{{}})) #);
:: deftheorem defines *' PETRI:def 4 :
for PTN being Petri_net
for S0 being Subset of the carrier of PTN holds *' S0 = { t where t is transition of PTN : ex f being T-S_arc of PTN ex s being place of PTN st
( s in S0 & f = [t,s] ) } ;
:: deftheorem defines *' PETRI:def 5 :
for PTN being Petri_net
for S0 being Subset of the carrier of PTN holds S0 *' = { t where t is transition of PTN : ex f being S-T_arc of PTN ex s being place of PTN st
( s in S0 & f = [s,t] ) } ;
theorem
theorem Th2:
theorem
theorem Th4:
:: deftheorem defines *' PETRI:def 6 :
for PTN being Petri_net
for T0 being Subset of the carrier' of PTN holds *' T0 = { s where s is place of PTN : ex f being S-T_arc of PTN ex t being transition of PTN st
( t in T0 & f = [s,t] ) } ;
:: deftheorem defines *' PETRI:def 7 :
for PTN being Petri_net
for T0 being Subset of the carrier' of PTN holds T0 *' = { s where s is place of PTN : ex f being T-S_arc of PTN ex t being transition of PTN st
( t in T0 & f = [t,s] ) } ;
theorem
theorem Th6:
theorem
theorem Th8:
theorem
theorem
theorem
theorem
begin
:: deftheorem defines Deadlock-like PETRI:def 8 :
for PTN being Petri_net
for IT being Subset of the carrier of PTN holds
( IT is Deadlock-like iff *' IT is Subset of (IT *') );
:: deftheorem defines With_Deadlocks PETRI:def 9 :
for IT being Petri_net holds
( IT is With_Deadlocks iff ex S being Subset of the carrier of IT st S is Deadlock-like );
begin
:: deftheorem defines Trap-like PETRI:def 10 :
for PTN being Petri_net
for IT being Subset of the carrier of PTN holds
( IT is Trap-like iff IT *' is Subset of (*' IT) );
:: deftheorem defines With_Traps PETRI:def 11 :
for IT being Petri_net holds
( IT is With_Traps iff ex S being Subset of the carrier of IT st S is Trap-like );
begin
:: deftheorem defines .: PETRI:def 12 :
for PTN being PT_net_Str holds PTN .: = PT_net_Str(# the carrier of PTN, the carrier' of PTN,( the T-S_Arcs of PTN ~),( the S-T_Arcs of PTN ~) #);
theorem
theorem
:: deftheorem defines .: PETRI:def 13 :
for PTN being Petri_net
for S0 being Subset of the carrier of PTN holds S0 .: = S0;
:: deftheorem defines .: PETRI:def 14 :
for PTN being Petri_net
for s being place of PTN holds s .: = s;
:: deftheorem defines .: PETRI:def 15 :
for PTN being Petri_net
for S0 being Subset of the carrier of (PTN .:) holds .: S0 = S0;
:: deftheorem defines .: PETRI:def 16 :
for PTN being Petri_net
for s being place of (PTN .:) holds .: s = s;
:: deftheorem defines .: PETRI:def 17 :
for PTN being Petri_net
for T0 being Subset of the carrier' of PTN holds T0 .: = T0;
:: deftheorem defines .: PETRI:def 18 :
for PTN being Petri_net
for t being transition of PTN holds t .: = t;
:: deftheorem defines .: PETRI:def 19 :
for PTN being Petri_net
for T0 being Subset of the carrier' of (PTN .:) holds .: T0 = T0;
:: deftheorem defines .: PETRI:def 20 :
for PTN being Petri_net
for t being transition of (PTN .:) holds .: t = t;
theorem Th15:
theorem Th16:
theorem
theorem
theorem
theorem