for PTN being Petri_net
for Sd being non empty Subset of the carrier of PTN holds
( Sd is Deadlock-like iff for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE} holds
for t being transition of PTN st t is_firable_on M0 holds
(Firing (t,M0)) .: Sd = {FALSE} )