:: BOOLMARK semantic presentation begin theorem Th1: :: BOOLMARK:1 for A, B being non empty set for f being Function of A,B for C being Subset of A for v being Element of B holds f +* (C --> v) is Function of A,B proof let A, B be non empty set ; ::_thesis: for f being Function of A,B for C being Subset of A for v being Element of B holds f +* (C --> v) is Function of A,B let f be Function of A,B; ::_thesis: for C being Subset of A for v being Element of B holds f +* (C --> v) is Function of A,B let C be Subset of A; ::_thesis: for v being Element of B holds f +* (C --> v) is Function of A,B let v be Element of B; ::_thesis: f +* (C --> v) is Function of A,B A1: dom f = A by FUNCT_2:def_1; ( rng f c= B & rng (C --> v) c= {v} ) by FUNCOP_1:13, RELAT_1:def_19; then A2: (rng f) \/ (rng (C --> v)) c= B \/ {v} by XBOOLE_1:13; rng (f +* (C --> v)) c= (rng f) \/ (rng (C --> v)) by FUNCT_4:17; then rng (f +* (C --> v)) c= B \/ {v} by A2, XBOOLE_1:1; then A3: rng (f +* (C --> v)) c= B by ZFMISC_1:40; dom (f +* (C --> v)) = (dom f) \/ (dom (C --> v)) by FUNCT_4:def_1 .= ([#] A) \/ C by A1, FUNCOP_1:13 .= A by SUBSET_1:11 ; hence f +* (C --> v) is Function of A,B by A3, FUNCT_2:def_1, RELSET_1:4; ::_thesis: verum end; theorem Th2: :: BOOLMARK:2 for X, Y being non empty set for A, B being Subset of X for f being Function of X,Y st f .: A misses f .: B holds A misses B proof let X, Y be non empty set ; ::_thesis: for A, B being Subset of X for f being Function of X,Y st f .: A misses f .: B holds A misses B let A, B be Subset of X; ::_thesis: for f being Function of X,Y st f .: A misses f .: B holds A misses B let f be Function of X,Y; ::_thesis: ( f .: A misses f .: B implies A misses B ) assume A1: (f .: A) /\ (f .: B) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: A misses B assume A /\ B <> {} ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction then consider x being Element of X such that A2: x in A /\ B by SUBSET_1:4; x in B by A2, XBOOLE_0:def_4; then A3: f . x in f .: B by FUNCT_2:35; x in A by A2, XBOOLE_0:def_4; then f . x in f .: A by FUNCT_2:35; hence contradiction by A1, A3, XBOOLE_0:def_4; ::_thesis: verum end; theorem Th3: :: BOOLMARK:3 for A, B being set for f being Function for x being set st A misses B holds (f +* (A --> x)) .: B = f .: B proof let A, B be set ; ::_thesis: for f being Function for x being set st A misses B holds (f +* (A --> x)) .: B = f .: B let f be Function; ::_thesis: for x being set st A misses B holds (f +* (A --> x)) .: B = f .: B let x be set ; ::_thesis: ( A misses B implies (f +* (A --> x)) .: B = f .: B ) assume that A1: A /\ B = {} and A2: (f +* (A --> x)) .: B <> f .: B ; :: according to XBOOLE_0:def_7 ::_thesis: contradiction A3: dom (f +* (A --> x)) = (dom f) \/ (dom (A --> x)) by FUNCT_4:def_1; A4: dom (A --> x) = A by FUNCOP_1:13; A5: not for y being set holds ( y in (f +* (A --> x)) .: B iff y in f .: B ) by A2, TARSKI:1; now__::_thesis:_(_(_ex_y_being_set_st_ (_y_in_(f_+*_(A_-->_x))_.:_B_&_not_y_in_f_.:_B_)_&_contradiction_)_or_(_ex_y_being_set_st_ (_not_y_in_(f_+*_(A_-->_x))_.:_B_&_y_in_f_.:_B_)_&_contradiction_)_) percases ( ex y being set st ( y in (f +* (A --> x)) .: B & not y in f .: B ) or ex y being set st ( not y in (f +* (A --> x)) .: B & y in f .: B ) ) by A5; case ex y being set st ( y in (f +* (A --> x)) .: B & not y in f .: B ) ; ::_thesis: contradiction then consider y being set such that A6: y in (f +* (A --> x)) .: B and A7: not y in f .: B ; consider z being set such that A8: z in dom (f +* (A --> x)) and A9: z in B and A10: y = (f +* (A --> x)) . z by A6, FUNCT_1:def_6; not z in A by A1, A9, XBOOLE_0:def_4; then ( z in dom f & y = f . z ) by A3, A4, A8, A10, FUNCT_4:11, XBOOLE_0:def_3; hence contradiction by A7, A9, FUNCT_1:def_6; ::_thesis: verum end; case ex y being set st ( not y in (f +* (A --> x)) .: B & y in f .: B ) ; ::_thesis: contradiction then consider y being set such that A11: not y in (f +* (A --> x)) .: B and A12: y in f .: B ; consider z being set such that A13: z in dom f and A14: z in B and A15: y = f . z by A12, FUNCT_1:def_6; not z in A by A1, A14, XBOOLE_0:def_4; then A16: y = (f +* (A --> x)) . z by A4, A15, FUNCT_4:11; z in dom (f +* (A --> x)) by A3, A13, XBOOLE_0:def_3; hence contradiction by A11, A14, A16, FUNCT_1:def_6; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; begin definition let PTN be PT_net_Str ; func Bool_marks_of PTN -> FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN equals :: BOOLMARK:def 1 Funcs ( the carrier of PTN,BOOLEAN); correctness coherence Funcs ( the carrier of PTN,BOOLEAN) is FUNCTION_DOMAIN of the carrier of PTN, BOOLEAN ; ; end; :: deftheorem defines Bool_marks_of BOOLMARK:def_1_:_ for PTN being PT_net_Str holds Bool_marks_of PTN = Funcs ( the carrier of PTN,BOOLEAN); definition let PTN be PT_net_Str ; mode Boolean_marking of PTN is Element of Bool_marks_of PTN; end; definition let PTN be Petri_net; let M0 be Boolean_marking of PTN; let t be transition of PTN; predt is_firable_on M0 means :Def2: :: BOOLMARK:def 2 M0 .: (*' {t}) c= {TRUE}; end; :: deftheorem Def2 defines is_firable_on BOOLMARK:def_2_:_ for PTN being Petri_net for M0 being Boolean_marking of PTN for t being transition of PTN holds ( t is_firable_on M0 iff M0 .: (*' {t}) c= {TRUE} ); notation let PTN be Petri_net; let M0 be Boolean_marking of PTN; let t be transition of PTN; antonym t is_not_firable_on M0 for t is_firable_on M0; end; definition let PTN be Petri_net; let M0 be Boolean_marking of PTN; let t be transition of PTN; func Firing (t,M0) -> Boolean_marking of PTN equals :: BOOLMARK:def 3 (M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE); coherence (M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE) is Boolean_marking of PTN proof set M1 = (M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE); M0 +* ((*' {t}) --> FALSE) is Function of the carrier of PTN,BOOLEAN by Th1; then (M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE) is Function of the carrier of PTN,BOOLEAN by Th1; hence (M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE) is Boolean_marking of PTN by FUNCT_2:8; ::_thesis: verum end; correctness ; end; :: deftheorem defines Firing BOOLMARK:def_3_:_ for PTN being Petri_net for M0 being Boolean_marking of PTN for t being transition of PTN holds Firing (t,M0) = (M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE); definition let PTN be Petri_net; let M0 be Boolean_marking of PTN; let Q be FinSequence of the carrier' of PTN; predQ is_firable_on M0 means :Def4: :: BOOLMARK:def 4 ( Q = {} or ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & Q /. 1 is_firable_on M0 & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds ( Q /. (i + 1) is_firable_on M /. i & M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ); end; :: deftheorem Def4 defines is_firable_on BOOLMARK:def_4_:_ for PTN being Petri_net for M0 being Boolean_marking of PTN for Q being FinSequence of the carrier' of PTN holds ( Q is_firable_on M0 iff ( Q = {} or ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & Q /. 1 is_firable_on M0 & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds ( Q /. (i + 1) is_firable_on M /. i & M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ) ); notation let PTN be Petri_net; let M0 be Boolean_marking of PTN; let Q be FinSequence of the carrier' of PTN; antonym Q is_not_firable_on M0 for Q is_firable_on M0; end; definition let PTN be Petri_net; let M0 be Boolean_marking of PTN; let Q be FinSequence of the carrier' of PTN; func Firing (Q,M0) -> Boolean_marking of PTN means :Def5: :: BOOLMARK:def 5 it = M0 if Q = {} otherwise ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & it = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ); existence ( ( Q = {} implies ex b1 being Boolean_marking of PTN st b1 = M0 ) & ( not Q = {} implies ex b1 being Boolean_marking of PTN ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & b1 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ) proof defpred S1[ Element of NAT ] means for Q being FinSequence of the carrier' of PTN st $1 = len Q holds ( ( Q = {} implies ex M1 being Boolean_marking of PTN st M1 = M0 ) & ( Q <> {} implies ex M2 being Boolean_marking of PTN ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ); A1: now__::_thesis:_for_n_being_Element_of_NAT_st_S1[n]_holds_ S1[n_+_1] let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: S1[n] ; ::_thesis: S1[n + 1] thus S1[n + 1] ::_thesis: verum proof let Q be FinSequence of the carrier' of PTN; ::_thesis: ( n + 1 = len Q implies ( ( Q = {} implies ex M1 being Boolean_marking of PTN st M1 = M0 ) & ( Q <> {} implies ex M2 being Boolean_marking of PTN ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ) ) assume A3: n + 1 = len Q ; ::_thesis: ( ( Q = {} implies ex M1 being Boolean_marking of PTN st M1 = M0 ) & ( Q <> {} implies ex M2 being Boolean_marking of PTN ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ) thus ( Q = {} implies ex M1 being Boolean_marking of PTN st M1 = M0 ) ; ::_thesis: ( Q <> {} implies ex M2 being Boolean_marking of PTN ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) thus ( Q <> {} implies ex M2 being Boolean_marking of PTN ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ::_thesis: verum proof assume Q <> {} ; ::_thesis: ex M2 being Boolean_marking of PTN ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) then len Q <> 0 ; then consider Q1 being FinSequence of the carrier' of PTN, t being transition of PTN such that A4: Q = Q1 ^ <*t*> by FINSEQ_2:19; A5: n + 1 = (len Q1) + 1 by A3, A4, FINSEQ_2:16; percases ( Q1 = {} or Q1 <> {} ) ; supposeA6: Q1 = {} ; ::_thesis: ex M2 being Boolean_marking of PTN ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) take M2 = Firing (t,M0); ::_thesis: ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) take M = <*M2*>; ::_thesis: ( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) A7: len Q = (len Q1) + (len <*t*>) by A4, FINSEQ_1:22 .= 0 + (len <*t*>) by A6 .= 0 + 1 by FINSEQ_1:39 ; hence len Q = len M by FINSEQ_1:39; ::_thesis: ( M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) hence M2 = M /. (len M) by A7, FINSEQ_4:16; ::_thesis: ( M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) Q = <*t*> by A4, A6, FINSEQ_1:34; then Q /. 1 = t by FINSEQ_4:16; hence M /. 1 = Firing ((Q /. 1),M0) by FINSEQ_4:16; ::_thesis: for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) let i be Element of NAT ; ::_thesis: ( i < len Q & i > 0 implies M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) assume ( i < len Q & i > 0 ) ; ::_thesis: M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) hence M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) by A7, NAT_1:13; ::_thesis: verum end; supposeA8: Q1 <> {} ; ::_thesis: ex M2 being Boolean_marking of PTN ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) then A9: len Q1 > 0 by NAT_1:3; then 0 + 1 < (len Q1) + 1 by XREAL_1:6; then 1 <= len Q1 by NAT_1:13; then A10: 1 in dom Q1 by FINSEQ_3:25; A11: len Q = (len Q1) + (len <*t*>) by A4, FINSEQ_1:22 .= (len Q1) + 1 by FINSEQ_1:40 ; consider B2 being Boolean_marking of PTN, B being FinSequence of Bool_marks_of PTN such that A12: len Q1 = len B and A13: B2 = B /. (len B) and A14: B /. 1 = Firing ((Q1 /. 1),M0) and A15: for i being Element of NAT st i < len Q1 & i > 0 holds B /. (i + 1) = Firing ((Q1 /. (i + 1)),(B /. i)) by A2, A5, A8; take M2 = Firing (t,B2); ::_thesis: ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) take M = B ^ <*M2*>; ::_thesis: ( len Q = len M & M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) A16: len M = (len B) + (len <*M2*>) by FINSEQ_1:22 .= (len B) + 1 by FINSEQ_1:40 ; hence len Q = len M by A12, A11; ::_thesis: ( M2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) thus M2 = M /. (len M) by A16, FINSEQ_4:67; ::_thesis: ( M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) 0 + 1 < (len B) + 1 by A12, A9, XREAL_1:6; then A17: 1 <= len B by NAT_1:13; then 1 in dom B by FINSEQ_3:25; hence M /. 1 = B /. 1 by FINSEQ_4:68 .= Firing ((Q /. 1),M0) by A4, A14, A10, FINSEQ_4:68 ; ::_thesis: for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) let i be Element of NAT ; ::_thesis: ( i < len Q & i > 0 implies M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) assume that A18: i < len Q and A19: i > 0 ; ::_thesis: M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) thus M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ::_thesis: verum proof ( 1 <= i + 1 & i + 1 <= (len Q1) + 1 ) by A11, A18, NAT_1:12, NAT_1:13; then A20: ( Seg ((len Q1) + 1) = (Seg (len Q1)) \/ {((len Q1) + 1)} & i + 1 in Seg ((len Q1) + 1) ) by FINSEQ_1:1, FINSEQ_1:9; percases ( i + 1 in Seg (len Q1) or i + 1 in {((len Q1) + 1)} ) by A20, XBOOLE_0:def_3; supposeA21: i + 1 in Seg (len Q1) ; ::_thesis: M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) then i + 1 <= len B by A12, FINSEQ_1:1; then i + 1 <= (len B) + 1 by NAT_1:12; then A22: i <= len B by XREAL_1:6; 0 + 1 < i + 1 by A19, XREAL_1:6; then 1 <= i by NAT_1:13; then A23: i in dom B by A22, FINSEQ_3:25; i + 1 <= len Q1 by A21, FINSEQ_1:1; then i < len Q1 by NAT_1:13; then A24: B /. (i + 1) = Firing ((Q1 /. (i + 1)),(B /. i)) by A15, A19; i + 1 in dom Q1 by A21, FINSEQ_1:def_3; then A25: Q1 /. (i + 1) = Q /. (i + 1) by A4, FINSEQ_4:68; i + 1 in dom B by A12, A21, FINSEQ_1:def_3; then B /. (i + 1) = M /. (i + 1) by FINSEQ_4:68; hence M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) by A24, A25, A23, FINSEQ_4:68; ::_thesis: verum end; supposeA26: i + 1 in {((len Q1) + 1)} ; ::_thesis: M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) A27: len B in dom B by A17, FINSEQ_3:25; A28: i + 1 = (len Q1) + 1 by A26, TARSKI:def_1; then ( M /. (i + 1) = M2 & Q /. (i + 1) = t ) by A4, A12, FINSEQ_4:67; hence M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) by A12, A13, A28, A27, FINSEQ_4:68; ::_thesis: verum end; end; end; end; end; end; end; end; A29: S1[ 0 ] ; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A29, A1); hence ( ( Q = {} implies ex b1 being Boolean_marking of PTN st b1 = M0 ) & ( not Q = {} implies ex b1 being Boolean_marking of PTN ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & b1 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being Boolean_marking of PTN holds ( ( Q = {} & b1 = M0 & b2 = M0 implies b1 = b2 ) & ( not Q = {} & ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & b1 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) & ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & b2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) implies b1 = b2 ) ) proof let B1, B2 be Boolean_marking of PTN; ::_thesis: ( ( Q = {} & B1 = M0 & B2 = M0 implies B1 = B2 ) & ( not Q = {} & ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & B1 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) & ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & B2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) implies B1 = B2 ) ) thus ( Q = {} & B1 = M0 & B2 = M0 implies B1 = B2 ) ; ::_thesis: ( not Q = {} & ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & B1 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) & ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & B2 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) implies B1 = B2 ) assume Q <> {} ; ::_thesis: ( for M being FinSequence of Bool_marks_of PTN holds ( not len Q = len M or not B1 = M /. (len M) or not M /. 1 = Firing ((Q /. 1),M0) or ex i being Element of NAT st ( i < len Q & i > 0 & not M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) or for M being FinSequence of Bool_marks_of PTN holds ( not len Q = len M or not B2 = M /. (len M) or not M /. 1 = Firing ((Q /. 1),M0) or ex i being Element of NAT st ( i < len Q & i > 0 & not M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) or B1 = B2 ) given M1 being FinSequence of Bool_marks_of PTN such that A30: len Q = len M1 and A31: B1 = M1 /. (len M1) and A32: M1 /. 1 = Firing ((Q /. 1),M0) and A33: for i being Element of NAT st i < len Q & i > 0 holds M1 /. (i + 1) = Firing ((Q /. (i + 1)),(M1 /. i)) ; ::_thesis: ( for M being FinSequence of Bool_marks_of PTN holds ( not len Q = len M or not B2 = M /. (len M) or not M /. 1 = Firing ((Q /. 1),M0) or ex i being Element of NAT st ( i < len Q & i > 0 & not M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) or B1 = B2 ) A34: dom M1 = Seg (len Q) by A30, FINSEQ_1:def_3; given M2 being FinSequence of Bool_marks_of PTN such that A35: len Q = len M2 and A36: B2 = M2 /. (len M2) and A37: M2 /. 1 = Firing ((Q /. 1),M0) and A38: for i being Element of NAT st i < len Q & i > 0 holds M2 /. (i + 1) = Firing ((Q /. (i + 1)),(M2 /. i)) ; ::_thesis: B1 = B2 defpred S1[ Element of NAT ] means ( $1 in Seg (len Q) implies M1 /. $1 = M2 /. $1 ); A39: now__::_thesis:_for_j_being_Element_of_NAT_st_S1[j]_holds_ S1[j_+_1] let j be Element of NAT ; ::_thesis: ( S1[j] implies S1[j + 1] ) assume A40: S1[j] ; ::_thesis: S1[j + 1] now__::_thesis:_(_j_+_1_in_Seg_(len_Q)_implies_M1_/._(j_+_1)_=_M2_/._(j_+_1)_) assume A41: j + 1 in Seg (len Q) ; ::_thesis: M1 /. (j + 1) = M2 /. (j + 1) percases ( j = 0 or j <> 0 ) ; suppose j = 0 ; ::_thesis: M1 /. (j + 1) = M2 /. (j + 1) hence M1 /. (j + 1) = M2 /. (j + 1) by A32, A37; ::_thesis: verum end; supposeA42: j <> 0 ; ::_thesis: M1 /. (j + 1) = M2 /. (j + 1) then A43: j > 0 by NAT_1:3; ( j + 1 <= len Q & j < j + 1 ) by A41, FINSEQ_1:1, XREAL_1:29; then A44: j < len Q by XXREAL_0:2; 1 <= j by A42, NAT_1:14; hence M1 /. (j + 1) = Firing ((Q /. (j + 1)),(M2 /. j)) by A33, A40, A44, FINSEQ_1:1 .= M2 /. (j + 1) by A38, A43, A44 ; ::_thesis: verum end; end; end; hence S1[j + 1] ; ::_thesis: verum end; A45: S1[ 0 ] by FINSEQ_1:1; A46: for j being Element of NAT holds S1[j] from NAT_1:sch_1(A45, A39); now__::_thesis:_for_j_being_Nat_st_j_in_dom_M1_holds_ M1_._j_=_M2_._j let j be Nat; ::_thesis: ( j in dom M1 implies M1 . j = M2 . j ) assume A47: j in dom M1 ; ::_thesis: M1 . j = M2 . j then A48: j in dom M2 by A35, A34, FINSEQ_1:def_3; thus M1 . j = M1 /. j by A47, PARTFUN1:def_6 .= M2 /. j by A46, A34, A47 .= M2 . j by A48, PARTFUN1:def_6 ; ::_thesis: verum end; hence B1 = B2 by A30, A31, A35, A36, FINSEQ_2:9; ::_thesis: verum end; correctness consistency for b1 being Boolean_marking of PTN holds verum; ; end; :: deftheorem Def5 defines Firing BOOLMARK:def_5_:_ for PTN being Petri_net for M0 being Boolean_marking of PTN for Q being FinSequence of the carrier' of PTN for b4 being Boolean_marking of PTN holds ( ( Q = {} implies ( b4 = Firing (Q,M0) iff b4 = M0 ) ) & ( not Q = {} implies ( b4 = Firing (Q,M0) iff ex M being FinSequence of Bool_marks_of PTN st ( len Q = len M & b4 = M /. (len M) & M /. 1 = Firing ((Q /. 1),M0) & ( for i being Element of NAT st i < len Q & i > 0 holds M /. (i + 1) = Firing ((Q /. (i + 1)),(M /. i)) ) ) ) ) ); theorem Th4: :: BOOLMARK:4 for A being non empty set for y being set for f being Function holds (f +* (A --> y)) .: A = {y} proof let A be non empty set ; ::_thesis: for y being set for f being Function holds (f +* (A --> y)) .: A = {y} let y be set ; ::_thesis: for f being Function holds (f +* (A --> y)) .: A = {y} let f be Function; ::_thesis: (f +* (A --> y)) .: A = {y} now__::_thesis:_for_u_being_set_holds_ (_(_u_in_(f_+*_(A_-->_y))_.:_A_implies_u_=_y_)_&_(_u_=_y_implies_u_in_(f_+*_(A_-->_y))_.:_A_)_) let u be set ; ::_thesis: ( ( u in (f +* (A --> y)) .: A implies u = y ) & ( u = y implies u in (f +* (A --> y)) .: A ) ) thus ( u in (f +* (A --> y)) .: A implies u = y ) ::_thesis: ( u = y implies u in (f +* (A --> y)) .: A ) proof assume u in (f +* (A --> y)) .: A ; ::_thesis: u = y then consider z being set such that z in dom (f +* (A --> y)) and A1: z in A and A2: u = (f +* (A --> y)) . z by FUNCT_1:def_6; z in dom (A --> y) by A1, FUNCOP_1:13; then u = (A --> y) . z by A2, FUNCT_4:13; hence u = y by A1, FUNCOP_1:7; ::_thesis: verum end; consider x being set such that A3: x in A by XBOOLE_0:def_1; A4: x in dom (A --> y) by A3, FUNCOP_1:13; then A5: x in dom (f +* (A --> y)) by FUNCT_4:12; (A --> y) . x = y by A3, FUNCOP_1:7; then y = (f +* (A --> y)) . x by A4, FUNCT_4:13; hence ( u = y implies u in (f +* (A --> y)) .: A ) by A3, A5, FUNCT_1:def_6; ::_thesis: verum end; hence (f +* (A --> y)) .: A = {y} by TARSKI:def_1; ::_thesis: verum end; theorem Th5: :: BOOLMARK:5 for PTN being Petri_net for M0 being Boolean_marking of PTN for t being transition of PTN for s being place of PTN st s in {t} *' holds (Firing (t,M0)) . s = TRUE proof let PTN be Petri_net; ::_thesis: for M0 being Boolean_marking of PTN for t being transition of PTN for s being place of PTN st s in {t} *' holds (Firing (t,M0)) . s = TRUE let M0 be Boolean_marking of PTN; ::_thesis: for t being transition of PTN for s being place of PTN st s in {t} *' holds (Firing (t,M0)) . s = TRUE let t be transition of PTN; ::_thesis: for s being place of PTN st s in {t} *' holds (Firing (t,M0)) . s = TRUE let s be place of PTN; ::_thesis: ( s in {t} *' implies (Firing (t,M0)) . s = TRUE ) set M = (M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE); A1: [#] the carrier of PTN = the carrier of PTN ; A2: ( dom M0 = the carrier of PTN & dom ((*' {t}) --> FALSE) = *' {t} ) by FUNCT_2:def_1; dom (({t} *') --> TRUE) = {t} *' by FUNCT_2:def_1; then A3: dom ((M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE)) = (dom (M0 +* ((*' {t}) --> FALSE))) \/ ({t} *') by FUNCT_4:def_1 .= ( the carrier of PTN \/ (*' {t})) \/ ({t} *') by A2, FUNCT_4:def_1 .= the carrier of PTN \/ ((*' {t}) \/ ({t} *')) by XBOOLE_1:4 .= the carrier of PTN by A1, SUBSET_1:11 ; assume A4: s in {t} *' ; ::_thesis: (Firing (t,M0)) . s = TRUE then ((M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE)) .: ({t} *') = {TRUE} by Th4; then ((M0 +* ((*' {t}) --> FALSE)) +* (({t} *') --> TRUE)) . s in {TRUE} by A4, A3, FUNCT_1:def_6; hence (Firing (t,M0)) . s = TRUE by TARSKI:def_1; ::_thesis: verum end; Lm1: now__::_thesis:_for_PTN_being_Petri_net for_Sd_being_non_empty_Subset_of_the_carrier_of_PTN_st_(_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}_)_holds_ Sd_is_Deadlock-like let PTN be Petri_net; ::_thesis: for Sd being non empty Subset of the carrier of PTN st ( 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} ) holds Sd is Deadlock-like let Sd be non empty Subset of the carrier of PTN; ::_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 ) 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 ; A3: rng (( the carrier of PTN --> TRUE) +* (Sd --> FALSE)) c= (rng ( the carrier of PTN --> TRUE)) \/ (rng (Sd --> FALSE)) by FUNCT_4:17; rng (Sd --> FALSE) c= {FALSE} by FUNCOP_1:13; then A4: rng (Sd --> FALSE) c= BOOLEAN by XBOOLE_1:1; 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 A4, XBOOLE_1:8; then rng (( the carrier of PTN --> TRUE) +* (Sd --> FALSE)) c= BOOLEAN by A3, 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 A5: 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: Sd is Deadlock-like assume not Sd is Deadlock-like ; ::_thesis: contradiction then not *' Sd c= Sd *' by PETRI:def_8; then consider t being transition of PTN such that A6: t in *' Sd and A7: not t in Sd *' by SUBSET_1:2; {t} *' meets Sd by A6, PETRI:20; then consider s being set such that A8: s in ({t} *') /\ Sd by XBOOLE_0:4; s in {t} *' by A8, XBOOLE_0:def_4; then A9: (Firing (t,M0)) . s = TRUE by Th5; s in Sd by A8, XBOOLE_0:def_4; then TRUE in (Firing (t,M0)) .: Sd by A9, FUNCT_2:35; then A10: (Firing (t,M0)) .: Sd <> {FALSE} by TARSKI:def_1; Sd misses *' {t} by A7, PETRI:19; then A11: ( the carrier of PTN --> TRUE) .: (*' {t}) = M0 .: (*' {t}) by Th3; ( 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 A11, XBOOLE_1:1; then A12: t is_firable_on M0 by Def2; M0 .: Sd = {FALSE} by Th4; hence contradiction by A5, A12, A10; ::_thesis: verum end; theorem :: BOOLMARK:6 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} ) proof 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 *') by PETRI:def_8; 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: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 end; theorem Th7: :: BOOLMARK:7 for D being non empty set for Q0, Q1 being FinSequence of D for i being Element of NAT st 1 <= i & i <= len Q0 holds (Q0 ^ Q1) /. i = Q0 /. i proof let D be non empty set ; ::_thesis: for Q0, Q1 being FinSequence of D for i being Element of NAT st 1 <= i & i <= len Q0 holds (Q0 ^ Q1) /. i = Q0 /. i let Q0, Q1 be FinSequence of D; ::_thesis: for i being Element of NAT st 1 <= i & i <= len Q0 holds (Q0 ^ Q1) /. i = Q0 /. i let i be Element of NAT ; ::_thesis: ( 1 <= i & i <= len Q0 implies (Q0 ^ Q1) /. i = Q0 /. i ) len Q0 <= (len Q0) + (len Q1) by NAT_1:11; then A1: ( i <= len Q0 implies i <= (len Q0) + (len Q1) ) by XXREAL_0:2; ( i in dom Q0 implies i in Seg (len Q0) ) by FINSEQ_1:def_3; then ( i in dom Q0 implies ( 1 <= i & i <= len (Q0 ^ Q1) ) ) by A1, FINSEQ_1:1, FINSEQ_1:22; then A2: ( i in dom Q0 implies i in dom (Q0 ^ Q1) ) by FINSEQ_3:25; ( i in dom Q0 implies Q0 . i = Q0 /. i ) by PARTFUN1:def_6; then A3: ( i in dom Q0 implies (Q0 ^ Q1) . i = Q0 /. i ) by FINSEQ_1:def_7; ( i in dom Q0 iff i in Seg (len Q0) ) by FINSEQ_1:def_3; hence ( 1 <= i & i <= len Q0 implies (Q0 ^ Q1) /. i = Q0 /. i ) by A2, A3, FINSEQ_1:1, PARTFUN1:def_6; ::_thesis: verum end; theorem Th8: :: BOOLMARK:8 for PTN being Petri_net for M0 being Boolean_marking of PTN for Q0, Q1 being FinSequence of the carrier' of PTN holds Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) proof let PTN be Petri_net; ::_thesis: for M0 being Boolean_marking of PTN for Q0, Q1 being FinSequence of the carrier' of PTN holds Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) let M0 be Boolean_marking of PTN; ::_thesis: for Q0, Q1 being FinSequence of the carrier' of PTN holds Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) let Q0, Q1 be FinSequence of the carrier' of PTN; ::_thesis: Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) now__::_thesis:_(_(_Q0_=_{}_&_Q1_=_{}_&_Firing_((Q0_^_Q1),M0)_=_Firing_(Q1,(Firing_(Q0,M0)))_)_or_(_Q0_=_{}_&_Q1_<>_{}_&_Firing_((Q0_^_Q1),M0)_=_Firing_(Q1,(Firing_(Q0,M0)))_)_or_(_Q0_<>_{}_&_Q1_=_{}_&_Firing_((Q0_^_Q1),M0)_=_Firing_(Q1,(Firing_(Q0,M0)))_)_or_(_Q0_<>_{}_&_Q1_<>_{}_&_(_for_i_being_Element_of_NAT_holds_Firing_((Q0_^_Q1),M0)_=_Firing_(Q1,(Firing_(Q0,M0)))_)_)_) percases ( ( Q0 = {} & Q1 = {} ) or ( Q0 = {} & Q1 <> {} ) or ( Q0 <> {} & Q1 = {} ) or ( Q0 <> {} & Q1 <> {} ) ) ; caseA1: ( Q0 = {} & Q1 = {} ) ; ::_thesis: Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) then A2: Q0 ^ Q1 = {} by FINSEQ_1:34; Firing (Q1,(Firing (Q0,M0))) = Firing (Q1,M0) by A1, Def5 .= M0 by A1, Def5 ; hence Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) by A2, Def5; ::_thesis: verum end; caseA3: ( Q0 = {} & Q1 <> {} ) ; ::_thesis: Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) then Firing ((Q0 ^ Q1),M0) = Firing (Q1,M0) by FINSEQ_1:34; hence Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) by A3, Def5; ::_thesis: verum end; caseA4: ( Q0 <> {} & Q1 = {} ) ; ::_thesis: Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) then Firing ((Q0 ^ Q1),M0) = Firing (Q0,M0) by FINSEQ_1:34; hence Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) by A4, Def5; ::_thesis: verum end; caseA5: ( Q0 <> {} & Q1 <> {} ) ; ::_thesis: for i being Element of NAT holds Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) then consider M3 being FinSequence of Bool_marks_of PTN such that A6: ( len Q0 = len M3 & Firing (Q0,M0) = M3 /. (len M3) ) and A7: M3 /. 1 = Firing ((Q0 /. 1),M0) and A8: for i being Element of NAT st i < len Q0 & i > 0 holds M3 /. (i + 1) = Firing ((Q0 /. (i + 1)),(M3 /. i)) by Def5; consider M being FinSequence of Bool_marks_of PTN such that A9: len (Q0 ^ Q1) = len M and A10: Firing ((Q0 ^ Q1),M0) = M /. (len M) and A11: M /. 1 = Firing (((Q0 ^ Q1) /. 1),M0) and A12: for i being Element of NAT st i < len (Q0 ^ Q1) & i > 0 holds M /. (i + 1) = Firing (((Q0 ^ Q1) /. (i + 1)),(M /. i)) by A5, Def5; defpred S1[ Element of NAT ] means ( 1 + $1 <= len Q0 implies M /. (1 + $1) = M3 /. (1 + $1) ); 0 < len Q1 by A5, NAT_1:3; then 0 + (len Q0) < (len Q0) + (len Q1) by XREAL_1:6; then A13: len Q0 < len (Q0 ^ Q1) by FINSEQ_1:22; A14: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) A15: 0 <= k by NAT_1:2; assume A16: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_(_1_+_(k_+_1)_<=_len_Q0_implies_M_/._(1_+_(k_+_1))_=_M3_/._(1_+_(k_+_1))_) assume A17: 1 + (k + 1) <= len Q0 ; ::_thesis: M /. (1 + (k + 1)) = M3 /. (1 + (k + 1)) then A18: (Q0 ^ Q1) /. (1 + (k + 1)) = Q0 /. (1 + (k + 1)) by Th7, NAT_1:11; A19: 1 + k < len Q0 by A17, NAT_1:13; then 1 + k < len (Q0 ^ Q1) by A13, XXREAL_0:2; then M /. (1 + (k + 1)) = Firing ((Q0 /. (1 + (k + 1))),(M3 /. (1 + k))) by A12, A15, A16, A17, A18, NAT_1:13; hence M /. (1 + (k + 1)) = M3 /. (1 + (k + 1)) by A8, A15, A19; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; reconsider m = (len Q0) - 1 as Element of NAT by A5, NAT_1:3, NAT_1:20; let i be Element of NAT ; ::_thesis: Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) len Q1 > 0 by A5, NAT_1:3; then A20: 0 + 1 <= len Q1 by NAT_1:13; consider M4 being FinSequence of Bool_marks_of PTN such that A21: len Q1 = len M4 and A22: Firing (Q1,(Firing (Q0,M0))) = M4 /. (len M4) and A23: M4 /. 1 = Firing ((Q1 /. 1),(Firing (Q0,M0))) and A24: for i being Element of NAT st i < len Q1 & i > 0 holds M4 /. (i + 1) = Firing ((Q1 /. (i + 1)),(M4 /. i)) by A5, Def5; consider k being Nat such that A25: len M4 = k + 1 by A5, A21, NAT_1:6; A26: S1[ 0 ] by A11, A7, Th7; A27: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A26, A14); defpred S2[ Element of NAT ] means ( 1 + $1 <= len Q1 implies M /. (((len Q0) + 1) + $1) = M4 /. (1 + $1) ); A28: now__::_thesis:_for_k_being_Element_of_NAT_st_S2[k]_holds_ S2[k_+_1] let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) assume A29: S2[k] ; ::_thesis: S2[k + 1] 0 <= k + (len Q0) by NAT_1:2; then A30: ( (((len Q0) + 1) + k) + 1 = ((len Q0) + 1) + (k + 1) & 0 < ((len Q0) + k) + 1 ) ; A31: 0 <= k by NAT_1:2; now__::_thesis:_(_1_+_(k_+_1)_<=_len_Q1_implies_M_/._(((len_Q0)_+_1)_+_(k_+_1))_=_M4_/._(1_+_(k_+_1))_) assume A32: 1 + (k + 1) <= len Q1 ; ::_thesis: M /. (((len Q0) + 1) + (k + 1)) = M4 /. (1 + (k + 1)) then A33: (Q0 ^ Q1) /. ((len Q0) + (1 + (k + 1))) = Q1 /. (1 + (k + 1)) by NAT_1:11, SEQ_4:136; A34: 1 + k < len Q1 by A32, NAT_1:13; then (len Q0) + (1 + k) < (len Q0) + (len Q1) by XREAL_1:6; then ((len Q0) + 1) + k < len (Q0 ^ Q1) by FINSEQ_1:22; then M /. (((len Q0) + 1) + (k + 1)) = Firing ((Q1 /. (1 + (k + 1))),(M4 /. (1 + k))) by A12, A30, A29, A32, A33, NAT_1:13; hence M /. (((len Q0) + 1) + (k + 1)) = M4 /. (1 + (k + 1)) by A24, A31, A34; ::_thesis: verum end; hence S2[k + 1] ; ::_thesis: verum end; len Q0 > 0 by A5, NAT_1:3; then M /. (((len Q0) + 1) + 0) = Firing (((Q0 ^ Q1) /. ((len Q0) + 1)),(M /. (1 + m))) by A12, A13 .= Firing (((Q0 ^ Q1) /. ((len Q0) + 1)),(Firing (Q0,M0))) by A6, A27 .= M4 /. (1 + 0) by A23, A20, SEQ_4:136 ; then A35: S2[ 0 ] ; A36: for k being Element of NAT holds S2[k] from NAT_1:sch_1(A35, A28); reconsider k = k as Element of NAT by ORDINAL1:def_12; M /. (len M) = M /. ((len Q0) + (1 + k)) by A9, A21, A25, FINSEQ_1:22 .= M /. (((len Q0) + 1) + k) .= M4 /. (len M4) by A21, A36, A25 ; hence Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) by A10, A22; ::_thesis: verum end; end; end; hence Firing ((Q0 ^ Q1),M0) = Firing (Q1,(Firing (Q0,M0))) ; ::_thesis: verum end; theorem Th9: :: BOOLMARK:9 for PTN being Petri_net for M0 being Boolean_marking of PTN for Q0, Q1 being FinSequence of the carrier' of PTN st Q0 ^ Q1 is_firable_on M0 holds ( Q1 is_firable_on Firing (Q0,M0) & Q0 is_firable_on M0 ) proof let PTN be Petri_net; ::_thesis: for M0 being Boolean_marking of PTN for Q0, Q1 being FinSequence of the carrier' of PTN st Q0 ^ Q1 is_firable_on M0 holds ( Q1 is_firable_on Firing (Q0,M0) & Q0 is_firable_on M0 ) let M0 be Boolean_marking of PTN; ::_thesis: for Q0, Q1 being FinSequence of the carrier' of PTN st Q0 ^ Q1 is_firable_on M0 holds ( Q1 is_firable_on Firing (Q0,M0) & Q0 is_firable_on M0 ) let Q0, Q1 be FinSequence of the carrier' of PTN; ::_thesis: ( Q0 ^ Q1 is_firable_on M0 implies ( Q1 is_firable_on Firing (Q0,M0) & Q0 is_firable_on M0 ) ) assume A1: Q0 ^ Q1 is_firable_on M0 ; ::_thesis: ( Q1 is_firable_on Firing (Q0,M0) & Q0 is_firable_on M0 ) now__::_thesis:_(_(_Q0_=_{}_&_Q1_=_{}_&_Q1_is_firable_on_Firing_(Q0,M0)_&_Q0_is_firable_on_M0_)_or_(_Q0_=_{}_&_Q1_<>_{}_&_Q0_is_firable_on_M0_&_Q1_is_firable_on_Firing_(Q0,M0)_)_or_(_Q0_<>_{}_&_Q1_=_{}_&_Q1_is_firable_on_Firing_(Q0,M0)_&_Q0_is_firable_on_M0_)_or_(_Q0_<>_{}_&_Q1_<>_{}_&_(_for_i_being_Element_of_NAT_holds_ (_Q1_is_firable_on_Firing_(Q0,M0)_&_Q0_is_firable_on_M0_)_)_)_) percases ( ( Q0 = {} & Q1 = {} ) or ( Q0 = {} & Q1 <> {} ) or ( Q0 <> {} & Q1 = {} ) or ( Q0 <> {} & Q1 <> {} ) ) ; case ( Q0 = {} & Q1 = {} ) ; ::_thesis: ( Q1 is_firable_on Firing (Q0,M0) & Q0 is_firable_on M0 ) hence ( Q1 is_firable_on Firing (Q0,M0) & Q0 is_firable_on M0 ) by Def4; ::_thesis: verum end; caseA2: ( Q0 = {} & Q1 <> {} ) ; ::_thesis: ( Q0 is_firable_on M0 & Q1 is_firable_on Firing (Q0,M0) ) hence Q0 is_firable_on M0 by Def4; ::_thesis: Q1 is_firable_on Firing (Q0,M0) Q0 ^ Q1 = Q1 by A2, FINSEQ_1:34; hence Q1 is_firable_on Firing (Q0,M0) by A1, A2, Def5; ::_thesis: verum end; caseA3: ( Q0 <> {} & Q1 = {} ) ; ::_thesis: ( Q1 is_firable_on Firing (Q0,M0) & Q0 is_firable_on M0 ) hence Q1 is_firable_on Firing (Q0,M0) by Def4; ::_thesis: Q0 is_firable_on M0 thus Q0 is_firable_on M0 by A1, A3, FINSEQ_1:34; ::_thesis: verum end; caseA4: ( Q0 <> {} & Q1 <> {} ) ; ::_thesis: for i being Element of NAT holds ( Q1 is_firable_on Firing (Q0,M0) & Q0 is_firable_on M0 ) let i be Element of NAT ; ::_thesis: ( Q1 is_firable_on Firing (Q0,M0) & Q0 is_firable_on M0 ) len Q1 > 0 by A4, NAT_1:3; then A5: 0 + 1 <= len Q1 by NAT_1:13; then A6: Q1 /. 1 = (Q0 ^ Q1) /. ((len Q0) + 1) by SEQ_4:136; reconsider m = (len Q0) - 1 as Element of NAT by A4, NAT_1:3, NAT_1:20; consider M4 being FinSequence of Bool_marks_of PTN such that A7: len Q1 = len M4 and Firing (Q1,(Firing (Q0,M0))) = M4 /. (len M4) and A8: M4 /. 1 = Firing ((Q1 /. 1),(Firing (Q0,M0))) and A9: for i being Element of NAT st i < len Q1 & i > 0 holds M4 /. (i + 1) = Firing ((Q1 /. (i + 1)),(M4 /. i)) by A4, Def5; consider M3 being FinSequence of Bool_marks_of PTN such that A10: len Q0 = len M3 and A11: Firing (Q0,M0) = M3 /. (len M3) and A12: M3 /. 1 = Firing ((Q0 /. 1),M0) and A13: for i being Element of NAT st i < len Q0 & i > 0 holds M3 /. (i + 1) = Firing ((Q0 /. (i + 1)),(M3 /. i)) by A4, Def5; consider j being Nat such that A14: len M3 = j + 1 by A4, A10, NAT_1:6; reconsider j = j as Element of NAT by ORDINAL1:def_12; consider M being FinSequence of Bool_marks_of PTN such that len (Q0 ^ Q1) = len M and A15: (Q0 ^ Q1) /. 1 is_firable_on M0 and A16: M /. 1 = Firing (((Q0 ^ Q1) /. 1),M0) and A17: for i being Element of NAT st i < len (Q0 ^ Q1) & i > 0 holds ( (Q0 ^ Q1) /. (i + 1) is_firable_on M /. i & M /. (i + 1) = Firing (((Q0 ^ Q1) /. (i + 1)),(M /. i)) ) by A1, A4, Def4; defpred S1[ Element of NAT ] means ( 1 + $1 <= len Q0 implies M /. (1 + $1) = M3 /. (1 + $1) ); 0 < len Q1 by A4, NAT_1:3; then 0 + (len Q0) < (len Q0) + (len Q1) by XREAL_1:6; then A18: len Q0 < len (Q0 ^ Q1) by FINSEQ_1:22; A19: now__::_thesis:_for_k_being_Element_of_NAT_st_S1[k]_holds_ S1[k_+_1] let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) A20: 0 <= k by NAT_1:2; assume A21: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_(_1_+_(k_+_1)_<=_len_Q0_implies_M_/._(1_+_(k_+_1))_=_M3_/._(1_+_(k_+_1))_) assume A22: 1 + (k + 1) <= len Q0 ; ::_thesis: M /. (1 + (k + 1)) = M3 /. (1 + (k + 1)) then A23: (Q0 ^ Q1) /. (1 + (k + 1)) = Q0 /. (1 + (k + 1)) by Th7, NAT_1:11; A24: 1 + k < len Q0 by A22, NAT_1:13; then 1 + k < len (Q0 ^ Q1) by A18, XXREAL_0:2; then M /. (1 + (k + 1)) = Firing ((Q0 /. (1 + (k + 1))),(M3 /. (1 + k))) by A17, A20, A21, A22, A23, NAT_1:13; hence M /. (1 + (k + 1)) = M3 /. (1 + (k + 1)) by A13, A20, A24; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; A25: S1[ 0 ] by A16, A12, Th7; A26: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A25, A19); A27: now__::_thesis:_for_i_being_Element_of_NAT_st_i_<_len_Q0_&_i_>_0_holds_ (_Q0_/._(i_+_1)_is_firable_on_M3_/._i_&_M3_/._(i_+_1)_=_Firing_((Q0_/._(i_+_1)),(M3_/._i))_) let i be Element of NAT ; ::_thesis: ( i < len Q0 & i > 0 implies ( Q0 /. (i + 1) is_firable_on M3 /. i & M3 /. (i + 1) = Firing ((Q0 /. (i + 1)),(M3 /. i)) ) ) assume that A28: i < len Q0 and A29: i > 0 ; ::_thesis: ( Q0 /. (i + 1) is_firable_on M3 /. i & M3 /. (i + 1) = Firing ((Q0 /. (i + 1)),(M3 /. i)) ) consider j being Nat such that A30: i = j + 1 by A29, NAT_1:6; ( i + 1 >= 1 & i + 1 <= len Q0 ) by A28, NAT_1:11, NAT_1:13; then i + 1 in dom Q0 by FINSEQ_3:25; then A31: (Q0 ^ Q1) /. (i + 1) = Q0 /. (i + 1) by FINSEQ_4:68; reconsider j = j as Element of NAT by ORDINAL1:def_12; i = j + 1 by A30; then A32: M /. i = M3 /. i by A26, A28; A33: i + 1 <= len Q0 by A28, NAT_1:13; A34: i < len (Q0 ^ Q1) by A18, A28, XXREAL_0:2; then M /. (i + 1) = Firing (((Q0 ^ Q1) /. (i + 1)),(M /. i)) by A17, A29; hence ( Q0 /. (i + 1) is_firable_on M3 /. i & M3 /. (i + 1) = Firing ((Q0 /. (i + 1)),(M3 /. i)) ) by A17, A26, A29, A34, A31, A32, A33; ::_thesis: verum end; defpred S2[ Element of NAT ] means ( 1 + $1 <= len Q1 implies M /. (((len Q0) + 1) + $1) = M4 /. (1 + $1) ); A35: now__::_thesis:_for_k_being_Element_of_NAT_st_S2[k]_holds_ S2[k_+_1] let k be Element of NAT ; ::_thesis: ( S2[k] implies S2[k + 1] ) assume A36: S2[k] ; ::_thesis: S2[k + 1] 0 <= k + (len Q0) by NAT_1:2; then A37: ( (((len Q0) + 1) + k) + 1 = ((len Q0) + 1) + (k + 1) & 0 < ((len Q0) + k) + 1 ) ; A38: 0 <= k by NAT_1:2; now__::_thesis:_(_1_+_(k_+_1)_<=_len_Q1_implies_M_/._(((len_Q0)_+_1)_+_(k_+_1))_=_M4_/._(1_+_(k_+_1))_) assume A39: 1 + (k + 1) <= len Q1 ; ::_thesis: M /. (((len Q0) + 1) + (k + 1)) = M4 /. (1 + (k + 1)) then A40: (Q0 ^ Q1) /. ((len Q0) + (1 + (k + 1))) = Q1 /. (1 + (k + 1)) by NAT_1:11, SEQ_4:136; A41: 1 + k < len Q1 by A39, NAT_1:13; then (len Q0) + (1 + k) < (len Q0) + (len Q1) by XREAL_1:6; then ((len Q0) + 1) + k < len (Q0 ^ Q1) by FINSEQ_1:22; then M /. (((len Q0) + 1) + (k + 1)) = Firing ((Q1 /. (1 + (k + 1))),(M4 /. (1 + k))) by A17, A37, A36, A39, A40, NAT_1:13; hence M /. (((len Q0) + 1) + (k + 1)) = M4 /. (1 + (k + 1)) by A9, A38, A41; ::_thesis: verum end; hence S2[k + 1] ; ::_thesis: verum end; A42: len Q0 > 0 by A4, NAT_1:3; then M /. (((len Q0) + 1) + 0) = Firing (((Q0 ^ Q1) /. ((len Q0) + 1)),(M /. (1 + m))) by A17, A18 .= Firing (((Q0 ^ Q1) /. ((len Q0) + 1)),(Firing (Q0,M0))) by A10, A11, A26 .= M4 /. (1 + 0) by A8, A5, SEQ_4:136 ; then A43: S2[ 0 ] ; A44: for k being Element of NAT holds S2[k] from NAT_1:sch_1(A43, A35); A45: now__::_thesis:_for_i_being_Element_of_NAT_st_i_<_len_Q1_&_i_>_0_holds_ (_Q1_/._(i_+_1)_is_firable_on_M4_/._i_&_M4_/._(i_+_1)_=_Firing_((Q1_/._(i_+_1)),(M4_/._i))_) let i be Element of NAT ; ::_thesis: ( i < len Q1 & i > 0 implies ( Q1 /. (i + 1) is_firable_on M4 /. i & M4 /. (i + 1) = Firing ((Q1 /. (i + 1)),(M4 /. i)) ) ) assume that A46: i < len Q1 and A47: i > 0 ; ::_thesis: ( Q1 /. (i + 1) is_firable_on M4 /. i & M4 /. (i + 1) = Firing ((Q1 /. (i + 1)),(M4 /. i)) ) consider j being Nat such that A48: i = j + 1 by A47, NAT_1:6; reconsider j = j as Element of NAT by ORDINAL1:def_12; ((len Q0) + 1) + j = (len Q0) + (j + 1) ; then A49: M /. ((len Q0) + i) = M4 /. i by A44, A46, A48; ( i + 1 >= 1 & i + 1 <= len Q1 ) by A46, NAT_1:11, NAT_1:13; then A50: i + 1 in dom Q1 by FINSEQ_3:25; A51: (Q0 ^ Q1) /. (((len Q0) + i) + 1) = (Q0 ^ Q1) /. ((len Q0) + (i + 1)) .= Q1 /. (i + 1) by A50, FINSEQ_4:69 ; A52: ( ((len Q0) + 1) + i = ((len Q0) + i) + 1 & i + 1 <= len Q1 ) by A46, NAT_1:13; len (Q0 ^ Q1) = (len Q0) + (len Q1) by FINSEQ_1:22; then A53: (len Q0) + i < len (Q0 ^ Q1) by A46, XREAL_1:6; A54: i < (len Q0) + i by A4, NAT_1:3, XREAL_1:29; then M /. (((len Q0) + i) + 1) = Firing (((Q0 ^ Q1) /. (((len Q0) + i) + 1)),(M /. ((len Q0) + i))) by A17, A47, A53; hence ( Q1 /. (i + 1) is_firable_on M4 /. i & M4 /. (i + 1) = Firing ((Q1 /. (i + 1)),(M4 /. i)) ) by A17, A44, A47, A53, A54, A51, A49, A52; ::_thesis: verum end; len M3 = j + 1 by A14; then M /. (len M3) = M3 /. (len M3) by A10, A26; then Q1 /. 1 is_firable_on M3 /. (len M3) by A17, A10, A42, A18, A6; hence Q1 is_firable_on Firing (Q0,M0) by A11, A7, A8, A45, Def4; ::_thesis: Q0 is_firable_on M0 0 + 1 <= len Q0 by A42, NAT_1:13; then Q0 /. 1 is_firable_on M0 by A15, Th7; hence Q0 is_firable_on M0 by A10, A12, A27, Def4; ::_thesis: verum end; end; end; hence ( Q1 is_firable_on Firing (Q0,M0) & Q0 is_firable_on M0 ) ; ::_thesis: verum end; theorem Th10: :: BOOLMARK:10 for PTN being Petri_net for M0 being Boolean_marking of PTN for t being transition of PTN holds ( t is_firable_on M0 iff <*t*> is_firable_on M0 ) proof let PTN be Petri_net; ::_thesis: for M0 being Boolean_marking of PTN for t being transition of PTN holds ( t is_firable_on M0 iff <*t*> is_firable_on M0 ) let M0 be Boolean_marking of PTN; ::_thesis: for t being transition of PTN holds ( t is_firable_on M0 iff <*t*> is_firable_on M0 ) let t be transition of PTN; ::_thesis: ( t is_firable_on M0 iff <*t*> is_firable_on M0 ) hereby ::_thesis: ( <*t*> is_firable_on M0 implies t is_firable_on M0 ) set M = <*(Firing ((<*t*> /. 1),M0))*>; A1: <*(Firing ((<*t*> /. 1),M0))*> /. 1 = Firing ((<*t*> /. 1),M0) by FINSEQ_4:16; A2: now__::_thesis:_for_i_being_Element_of_NAT_st_i_<_len_<*t*>_&_i_>_0_holds_ (_<*t*>_/._(i_+_1)_is_firable_on_<*(Firing_((<*t*>_/._1),M0))*>_/._i_&_<*(Firing_((<*t*>_/._1),M0))*>_/._(i_+_1)_=_Firing_((<*t*>_/._(i_+_1)),(<*(Firing_((<*t*>_/._1),M0))*>_/._i))_) A3: len <*t*> = 0 + 1 by FINSEQ_1:39; let i be Element of NAT ; ::_thesis: ( i < len <*t*> & i > 0 implies ( <*t*> /. (i + 1) is_firable_on <*(Firing ((<*t*> /. 1),M0))*> /. i & <*(Firing ((<*t*> /. 1),M0))*> /. (i + 1) = Firing ((<*t*> /. (i + 1)),(<*(Firing ((<*t*> /. 1),M0))*> /. i)) ) ) assume ( i < len <*t*> & i > 0 ) ; ::_thesis: ( <*t*> /. (i + 1) is_firable_on <*(Firing ((<*t*> /. 1),M0))*> /. i & <*(Firing ((<*t*> /. 1),M0))*> /. (i + 1) = Firing ((<*t*> /. (i + 1)),(<*(Firing ((<*t*> /. 1),M0))*> /. i)) ) hence ( <*t*> /. (i + 1) is_firable_on <*(Firing ((<*t*> /. 1),M0))*> /. i & <*(Firing ((<*t*> /. 1),M0))*> /. (i + 1) = Firing ((<*t*> /. (i + 1)),(<*(Firing ((<*t*> /. 1),M0))*> /. i)) ) by A3, NAT_1:13; ::_thesis: verum end; assume t is_firable_on M0 ; ::_thesis: <*t*> is_firable_on M0 then A4: <*t*> /. 1 is_firable_on M0 by FINSEQ_4:16; len <*t*> = 1 by FINSEQ_1:39 .= len <*(Firing ((<*t*> /. 1),M0))*> by FINSEQ_1:39 ; hence <*t*> is_firable_on M0 by A4, A1, A2, Def4; ::_thesis: verum end; assume <*t*> is_firable_on M0 ; ::_thesis: t is_firable_on M0 then ex M being FinSequence of Bool_marks_of PTN st ( len <*t*> = len M & <*t*> /. 1 is_firable_on M0 & M /. 1 = Firing ((<*t*> /. 1),M0) & ( for i being Element of NAT st i < len <*t*> & i > 0 holds ( <*t*> /. (i + 1) is_firable_on M /. i & M /. (i + 1) = Firing ((<*t*> /. (i + 1)),(M /. i)) ) ) ) by Def4; hence t is_firable_on M0 by FINSEQ_4:16; ::_thesis: verum end; theorem Th11: :: BOOLMARK:11 for PTN being Petri_net for M0 being Boolean_marking of PTN for t being transition of PTN holds Firing (t,M0) = Firing (<*t*>,M0) proof let PTN be Petri_net; ::_thesis: for M0 being Boolean_marking of PTN for t being transition of PTN holds Firing (t,M0) = Firing (<*t*>,M0) let M0 be Boolean_marking of PTN; ::_thesis: for t being transition of PTN holds Firing (t,M0) = Firing (<*t*>,M0) let t be transition of PTN; ::_thesis: Firing (t,M0) = Firing (<*t*>,M0) set M = <*(Firing ((<*t*> /. 1),M0))*>; A1: ( len <*t*> = 1 & <*t*> /. 1 = t ) by FINSEQ_1:39, FINSEQ_4:16; A2: <*(Firing ((<*t*> /. 1),M0))*> /. 1 = Firing ((<*t*> /. 1),M0) by FINSEQ_4:16; A3: now__::_thesis:_for_i_being_Element_of_NAT_st_i_<_len_<*t*>_&_i_>_0_holds_ <*(Firing_((<*t*>_/._1),M0))*>_/._(i_+_1)_=_Firing_((<*t*>_/._(i_+_1)),(<*(Firing_((<*t*>_/._1),M0))*>_/._i)) A4: len <*t*> = 0 + 1 by FINSEQ_1:39; let i be Element of NAT ; ::_thesis: ( i < len <*t*> & i > 0 implies <*(Firing ((<*t*> /. 1),M0))*> /. (i + 1) = Firing ((<*t*> /. (i + 1)),(<*(Firing ((<*t*> /. 1),M0))*> /. i)) ) assume ( i < len <*t*> & i > 0 ) ; ::_thesis: <*(Firing ((<*t*> /. 1),M0))*> /. (i + 1) = Firing ((<*t*> /. (i + 1)),(<*(Firing ((<*t*> /. 1),M0))*> /. i)) hence <*(Firing ((<*t*> /. 1),M0))*> /. (i + 1) = Firing ((<*t*> /. (i + 1)),(<*(Firing ((<*t*> /. 1),M0))*> /. i)) by A4, NAT_1:13; ::_thesis: verum end; len <*t*> = 1 by FINSEQ_1:39 .= len <*(Firing ((<*t*> /. 1),M0))*> by FINSEQ_1:39 ; hence Firing (t,M0) = Firing (<*t*>,M0) by A1, A2, A3, Def5; ::_thesis: verum end; theorem :: BOOLMARK:12 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 Q being FinSequence of the carrier' of PTN st Q is_firable_on M0 holds (Firing (Q,M0)) .: Sd = {FALSE} ) proof 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, PETRI:def_8; 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 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: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} by Def2; 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 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 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 by Def2; then A22: Q is_firable_on M0 by Th10; M0 .: Sd = {FALSE} by Th4; hence contradiction by A15, A22, A21; ::_thesis: verum end;