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:13;
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:11 ;
rng (Sd --> FALSE) c= {FALSE} by FUNCOP_1:13;
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 S1[ 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;
A7: now :: thesis: for Q being FinSequence of the carrier' of PTN
for x being transition of PTN st S1[Q] holds
S1[Q ^ <*x*>]
let Q be FinSequence of the carrier' of PTN; :: thesis: for x being transition of PTN st S1[Q] holds
S1[Q ^ <*x*>]
let x be transition of PTN; :: thesis: ( S1[Q] implies S1[Q ^ <*x*>] )
assume A8: S1[Q] ; :: thesis: S1[Q ^ <*x*>]
thus S1[Q ^ <*x*>] :: thesis: verum
proof
Firing ((Q ^ <*x*>),M0) = Firing (<*x*>,(Firing (Q,M0))) by Th8;
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 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:16;
then A10: Firing ((Q ^ <*x*>),M0) = ((Firing (Q,M0)) +* ((*' {x}) --> FALSE)) +* (({x} *') --> TRUE) by A9, FINSEQ_1:39;
assume A11: Q ^ <*x*> is_firable_on M0 ; :: thesis: (Firing ((Q ^ <*x*>),M0)) .: Sd = {FALSE}
then <*x*> is_firable_on Firing (Q,M0) by Th9;
then x is_firable_on Firing (Q,M0) by Th10;
then (Firing (Q,M0)) .: (*' {x}) c= {TRUE} ;
then A12: (Firing (Q,M0)) .: (*' {x}) misses {FALSE} by XBOOLE_1:63, ZFMISC_1:11;
then *' {x} misses Sd by A8, A11, Th2, Th9;
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, Th9 ;
:: thesis: verum
end;
end;
A13: S1[ <*> the carrier' of PTN] by A5, Def5;
thus for Q0 being FinSequence of the carrier' of PTN holds S1[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:17;
rng ( the carrier of PTN --> TRUE) c= {TRUE} by FUNCOP_1:13;
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:2;
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 object 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 Th5;
s in Sd by A19, XBOOLE_0:def 4;
then TRUE in (Firing (t,M0)) .: Sd by A20, FUNCT_2:35;
then (Firing (t,M0)) .: Sd <> {FALSE} by TARSKI:def 1;
then A21: (Firing (Q,M0)) .: Sd <> {FALSE} by Th11;
( rng ( the carrier of PTN --> TRUE) c= {TRUE} & ( the carrier of PTN --> TRUE) .: (*' {t}) c= rng ( the carrier of PTN --> TRUE) ) by FUNCOP_1:13, RELAT_1:111;
then M0 .: (*' {t}) c= {TRUE} by A18, XBOOLE_1:1;
then t is_firable_on M0 ;
then A22: Q is_firable_on M0 by Th10;
M0 .: Sd = {FALSE} by Th4;
hence contradiction by A15, A22, A21; :: thesis: verum