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 Q being FinSequence of the carrier' of PTN st Q is_firable_on M0 holds
(Firing Q,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 Q being FinSequence of the carrier' of PTN st Q is_firable_on M0 holds
(Firing Q,M0) .: Sd = {FALSE } )
set M0 = (the carrier of PTN --> TRUE ) +* (Sd --> FALSE );
A1: [#] the carrier of PTN = the carrier of PTN ;
( dom (the carrier of PTN --> TRUE ) = the carrier of PTN & dom (Sd --> FALSE ) = Sd ) by FUNCOP_1:19;
then A2: dom ((the carrier of PTN --> TRUE ) +* (Sd --> FALSE )) = the carrier of PTN \/ Sd by FUNCT_4:def 1
.= the carrier of PTN by A1, SUBSET_1:28 ;
rng (Sd --> FALSE ) c= {FALSE } by FUNCOP_1:19;
then A3: rng (Sd --> FALSE ) c= BOOLEAN by XBOOLE_1:1;
thus ( Sd is Deadlock-like implies for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE } holds
for Q being FinSequence of the carrier' of PTN st Q is_firable_on M0 holds
(Firing Q,M0) .: Sd = {FALSE } ) :: thesis: ( ( for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE } holds
for Q being FinSequence of the carrier' of PTN st Q is_firable_on M0 holds
(Firing Q,M0) .: Sd = {FALSE } ) implies Sd is Deadlock-like )

proof

assume A4: Sd is Deadlock-like ; :: thesis: for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE } holds
for Q being FinSequence of the carrier' of PTN st Q is_firable_on M0 holds
(Firing Q,M0) .: Sd = {FALSE }
let M0 be Boolean_marking of PTN; :: thesis: ( M0 .: Sd = {FALSE } implies for Q being FinSequence of the carrier' of PTN st Q is_firable_on M0 holds
(Firing Q,M0) .: Sd = {FALSE } )
assume A5: M0 .: Sd = {FALSE } ; :: thesis: for Q being FinSequence of the carrier' of PTN st Q is_firable_on M0 holds
(Firing Q,M0) .: Sd = {FALSE }
defpred S₁[ FinSequence of the carrier' of PTN] means ( $1 is_firable_on M0 implies (Firing $1,M0) .: Sd = {FALSE } );
A6: *' Sd is Subset of (Sd *' ) by A4, PETRI:def 8;

A7: now

let Q be FinSequence of the carrier' of PTN; :: thesis: for x being transition of PTN st S₁[Q] holds
S₁[Q ^ <*x*>]
let x be transition of PTN; :: thesis: ( S₁[Q] implies S₁[Q ^ <*x*>] )
assume A8: S₁[Q] ; :: thesis: S₁[Q ^ <*x*>]
thus S₁[Q ^ <*x*>] :: thesis: verum

proof

Firing (Q ^ <*x*>),M0 = Firing <*x*>,(Firing Q,M0) by Th10;
then A9: ex M being FinSequence of Bool_marks_of PTN st
( len <*x*> = len M & Firing (Q ^ <*x*>),M0 = M /. (len M) & M /. 1 = Firing (<*x*> /. 1),(Firing Q,M0) & ( for i being Element of NAT st i < len <*x*> & i > 0 holds
M /. (i + 1) = Firing (<*x*> /. (i + 1)),(M /. i) ) ) by Def5;
<*x*> /. 1 = x by FINSEQ_4:25;
then A10: Firing (Q ^ <*x*>),M0 = ((Firing Q,M0) +* ((*' {x}) --> FALSE )) +* (({x} *' ) --> TRUE ) by A9, FINSEQ_1:56;
assume A11: Q ^ <*x*> is_firable_on M0 ; :: thesis: (Firing (Q ^ <*x*>),M0) .: Sd = {FALSE }
then <*x*> is_firable_on Firing Q,M0 by Th11;
then x is_firable_on Firing Q,M0 by Th12;
then (Firing Q,M0) .: (*' {x}) c= {TRUE } by Def2;
then A12: (Firing Q,M0) .: (*' {x}) misses {FALSE } by XBOOLE_1:63, ZFMISC_1:17;
then *' {x} misses Sd by A8, A11, Th2, Th11;
then not x in *' Sd by A6, PETRI:19;
then {x} *' misses Sd by PETRI:20;
hence (Firing (Q ^ <*x*>),M0) .: Sd = ((Firing Q,M0) +* ((*' {x}) --> FALSE )) .: Sd by A10, Th3
.= {FALSE } by A8, A11, A12, Th2, Th3, Th11 ;
:: thesis: verum

end;

end;

A13: S₁[ <*> the carrier' of PTN] by A5, Def5;
thus for Q0 being FinSequence of the carrier' of PTN holds S₁[Q0] from FINSEQ_2:sch 2(A13, A7); :: thesis: verum

end;

A14: rng ((the carrier of PTN --> TRUE ) +* (Sd --> FALSE )) c= (rng (the carrier of PTN --> TRUE )) \/ (rng (Sd --> FALSE )) by FUNCT_4:18;
rng (the carrier of PTN --> TRUE ) c= {TRUE } by FUNCOP_1:19;
then rng (the carrier of PTN --> TRUE ) c= BOOLEAN by XBOOLE_1:1;
then (rng (the carrier of PTN --> TRUE )) \/ (rng (Sd --> FALSE )) c= BOOLEAN by A3, XBOOLE_1:8;
then rng ((the carrier of PTN --> TRUE ) +* (Sd --> FALSE )) c= BOOLEAN by A14, XBOOLE_1:1;
then reconsider M0 = (the carrier of PTN --> TRUE ) +* (Sd --> FALSE ) as Boolean_marking of PTN by A2, FUNCT_2:def 2;
assume A15: for M0 being Boolean_marking of PTN st M0 .: Sd = {FALSE } holds
for Q being FinSequence of the carrier' of PTN st Q is_firable_on M0 holds
(Firing Q,M0) .: Sd = {FALSE } ; :: thesis: Sd is Deadlock-like
assume *' Sd is not Subset of (Sd *' ) ; :: according to PETRI:def 8 :: thesis: contradiction
then consider t being transition of PTN such that
A16: t in *' Sd and
A17: not t in Sd *' by SUBSET_1:7;
Sd misses *' {t} by A17, PETRI:19;
then A18: (the carrier of PTN --> TRUE ) .: (*' {t}) = M0 .: (*' {t}) by Th3;
reconsider Q = <*t*> as FinSequence of the carrier' of PTN ;
{t} *' meets Sd by A16, PETRI:20;
then consider s being set such that
A19: s in ({t} *' ) /\ Sd by XBOOLE_0:4;
s in {t} *' by A19, XBOOLE_0:def 4;
then A20: (Firing t,M0) . s = TRUE by Th6;
s in Sd by A19, XBOOLE_0:def 4;
then TRUE in (Firing t,M0) .: Sd by A20, FUNCT_2:43;
then (Firing t,M0) .: Sd <> {FALSE } by TARSKI:def 1;
then A21: (Firing Q,M0) .: Sd <> {FALSE } by Th13;
( rng (the carrier of PTN --> TRUE ) c= {TRUE } & (the carrier of PTN --> TRUE ) .: (*' {t}) c= rng (the carrier of PTN --> TRUE ) ) by FUNCOP_1:19, RELAT_1:144;
then M0 .: (*' {t}) c= {TRUE } by A18, XBOOLE_1:1;
then t is_firable_on M0 by Def2;
then A22: Q is_firable_on M0 by Th12;
M0 .: Sd = {FALSE } by Th5;
hence contradiction by A15, A22, A21; :: thesis: verum