let PTN be Petri_net; :: thesis: 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} )
let Sd be non empty Subset of the carrier 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 *') ;
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} ;
then A3: M0 .: (*' {t}) misses {FALSE} by XBOOLE_1:63, ZFMISC_1:11;
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