let PTN be PT_net_Str ; :: thesis: for Sd being non empty Subset of the Places 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 } )
let Sd be non empty Subset of the Places of PTN; :: thesis: ( 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 } )
thus ( Sd is Deadlock-like implies 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 } ) :: thesis: ( ( 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 } ) implies Sd is Deadlock-like )

proof

assume Sd is Deadlock-like ; :: thesis: 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 }
then A1: *' Sd is Subset of (Sd *' ) by PETRI:def 5;
let M0 be Boolean_marking of PTN; :: thesis: ( M0 .: Sd = {FALSE } implies for t being transition of PTN st t is_firable_on M0 holds
(Firing t,M0) .: Sd = {FALSE } )
assume A2: M0 .: Sd = {FALSE } ; :: thesis: for t being transition of PTN st t is_firable_on M0 holds
(Firing t,M0) .: Sd = {FALSE }
let t be transition of PTN; :: thesis: ( t is_firable_on M0 implies (Firing t,M0) .: Sd = {FALSE } )
assume t is_firable_on M0 ; :: thesis: (Firing t,M0) .: Sd = {FALSE }
then M0 .: (*' {t}) c= {TRUE } by Def2;
then A3: M0 .: (*' {t}) misses {FALSE } by XBOOLE_1:63, ZFMISC_1:17;
then *' {t} misses Sd by A2, Th2;
then not t in *' Sd by A1, PETRI:19;
then {t} *' misses Sd by PETRI:20;
hence (Firing t,M0) .: Sd = (M0 +* ((*' {t}) --> FALSE )) .: Sd by Th3
.= {FALSE } by A2, A3, Th2, Th3 ;
:: thesis: verum

end;

thus ( ( 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 } ) implies Sd is Deadlock-like ) by Lm1; :: thesis: verum