:: Basic Concepts for Petri Nets with Boolean Markings. :: Boolean Markings and the Firability/Firing of Transitions :: by Pauline N. Kawamoto, Yasushi Fuwa and Yatsuka Nakamura :: :: Received October 8, 1993 :: Copyright (c) 1993 Association of Mizar Users environ vocabularies FUNCT_1, FUNCT_4, FUNCOP_1, RELAT_1, BOOLE, SUBSET_1, FINSEQ_1, PETRI, FRAENKEL, NET_1, MARGREL1, FUNCT_2, ARYTM_3, ARYTM_1, BOOLMARK, FINSEQ_4, ARYTM; notations TARSKI, XBOOLE_0, SUBSET_1, NUMBERS, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, DOMAIN_1, FRAENKEL, FUNCOP_1, FINSEQ_1, FUNCT_4, MARGREL1, PETRI, XXREAL_0; constructors PARTFUN1, DOMAIN_1, FUNCT_4, XXREAL_0, XREAL_0, NAT_1, MARGREL1, FINSEQ_4, PETRI; registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, XXREAL_0, XREAL_0, FINSEQ_1, MARGREL1, ORDINAL1; requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM; definitions PETRI, XBOOLE_0, XBOOLEAN, SUBSET_1; theorems SUBSET_1, TARSKI, ZFMISC_1, PETRI, FUNCT_1, FUNCOP_1, FUNCT_2, FUNCT_4, FINSEQ_1, FINSEQ_4, NAT_1, FINSEQ_2, FINSEQ_3, RELAT_1, RELSET_1, GOBOARD2, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1, CARD_1, CARD_2; schemes FINSEQ_2, NAT_1; begin theorem Th1: for A, B being non empty set, f being Function of A,B, C being Subset of A, v being Element of B holds f +* (C-->v) is Function of A,B proof let A, B be non empty set; let f be Function of A,B; let C be Subset of A; let v be Element of B; A1: dom f = A by FUNCT_2:def 1; A2: dom(f +* (C-->v)) = (dom f) \/ dom(C-->v) by FUNCT_4:def 1 .= [#]A \/ C by A1,FUNCOP_1:19 .= A by SUBSET_1:28; A3: rng f c= B by RELSET_1:12; rng(C-->v) c= {v} by FUNCOP_1:19; then A4: rng f \/ rng(C-->v) c= B \/ {v} by A3,XBOOLE_1:13; rng(f +* (C-->v)) c= rng f \/ rng(C-->v) by FUNCT_4:18; then rng(f +* (C-->v)) c= B \/ {v} by A4,XBOOLE_1:1; then rng(f +* (C-->v)) c= B by ZFMISC_1:46; hence thesis by A2,FUNCT_2:def 1,RELSET_1:11; end; theorem Th2: for X, Y being non empty set, A, B being Subset of X, f being Function of X,Y st f.:A misses f.:B holds A misses B proof let X, Y be non empty set; let A, B be Subset of X; let f be Function of X,Y such that A1: f.:A /\ f.:B = {}; assume A /\ B <> {}; then consider x being Element of X such that A2: x in A /\ B by SUBSET_1:10; x in A & x in B by A2,XBOOLE_0:def 3; then f.x in f.:A & f.x in f.:B by FUNCT_2:43; hence contradiction by A1,XBOOLE_0:def 3; end; theorem Th3: for A, B being set, f being Function, x being set holds A misses B implies (f +* (A --> x)).:B = f.:B proof let A, B be set, f be Function, x be set; assume that A1: A /\ B = {} and A2: (f +* (A --> x)).:B <> f.:B; A3: dom(f +* (A --> x)) = dom f \/ dom(A --> x) by FUNCT_4:def 1; A4: dom(A --> x) = A by FUNCOP_1:19; A5: not (for y being set holds y in (f +* (A --> x)).:B iff y in f.:B) by A2,TARSKI:2; now per cases by A5; case ex y being set st y in (f +* (A --> x)).:B & not y in f.:B; 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 12; A11: not z in A by A1,A9,XBOOLE_0:def 3; then A12: z in dom f by A3,A4,A8,XBOOLE_0:def 2; y = f.z by A4,A10,A11,FUNCT_4:12; hence contradiction by A7,A9,A12,FUNCT_1:def 12; end; case ex y being set st not y in (f +* (A --> x)).:B & y in f.:B; then consider y being set such that A13: not y in (f +* (A --> x)).:B and A14: y in f.:B; consider z being set such that A15: z in dom f and A16: z in B and A17: y = f.z by A14,FUNCT_1:def 12; A18: not z in A by A1,A16,XBOOLE_0:def 3; A19: z in dom(f +* (A --> x)) by A3,A15,XBOOLE_0:def 2; y = (f +* (A --> x)).z by A4,A17,A18,FUNCT_4:12; hence contradiction by A13,A16,A19,FUNCT_1:def 12; end; end; hence thesis; end; :: Main definitions, theorems block begin :: Boolean Markings of Place/Transition Net definition let PTN be PT_net_Str; func Bool_marks_of PTN -> FUNCTION_DOMAIN of the Places of PTN, BOOLEAN equals Funcs(the Places of PTN, BOOLEAN); correctness; end; definition let PTN be PT_net_Str; mode Boolean_marking of PTN is Element of Bool_marks_of PTN; end; :: Firable and Firing Conditions for Transitions definition let PTN be PT_net_Str; let M0 be Boolean_marking of PTN; let t be transition of PTN; pred t is_firable_on M0 means :Def2: M0.:*'{t} c= {TRUE}; end; notation let PTN be PT_net_Str; 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 PT_net_Str; let M0 be Boolean_marking of PTN; let t be transition of PTN; func Firing(t,M0) -> Boolean_marking of PTN equals M0 +* (*'{t}-->FALSE) +* ({t}*'-->TRUE); coherence proof set M1 = M0 +* (*'{t}-->FALSE) +* ({t}*'-->TRUE); M0 +* (*'{t}-->FALSE) is Function of the Places of PTN, BOOLEAN by Th1; then M1 is Function of the Places of PTN, BOOLEAN by Th1; hence thesis by FUNCT_2:11; end; correctness; end; :: Firable and Firing Conditions for Transition Sequences definition let PTN be PT_net_Str; let M0 be Boolean_marking of PTN; let Q be FinSequence of the Transitions of PTN; pred Q is_firable_on M0 means :Def4: 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; notation let PTN be PT_net_Str; let M0 be Boolean_marking of PTN; let Q be FinSequence of the Transitions of PTN; antonym Q is_not_firable_on M0 for Q is_firable_on M0; end; definition let PTN be PT_net_Str; let M0 be Boolean_marking of PTN; let Q be FinSequence of the Transitions of PTN; func Firing(Q,M0) -> Boolean_marking of PTN means :Def5: 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 proof defpred P2[Element of NAT] means for Q being FinSequence of the Transitions 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 st 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: P2[0] by CARD_2:59; A2: now let n be Element of NAT; assume A3: P2[n]; thus P2[n+1] proof let Q be FinSequence of the Transitions of PTN such that A4: n+1=len Q; thus Q = {} implies ex M1 being Boolean_marking of PTN st M1 = M0; thus Q <> {} implies ex M2 being Boolean_marking of PTN, 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) proof assume Q <> {}; then len Q<>0 by CARD_2:59; then consider Q1 being FinSequence of the Transitions of PTN, t being transition of PTN such that A5: Q=Q1^<*t*> by FINSEQ_2:22; A6: n+1=len Q1+ 1 by A4,A5,FINSEQ_2:19; per cases; suppose A7: Q1={}; take M2 = Firing(t,M0); take M = <*M2*>; A8: len Q = len Q1 + len <*t*> by A5,FINSEQ_1:35 .= 0 + len <*t*> by A7,CARD_1:47 .= 0 + 1 by FINSEQ_1:56; hence len Q = len M by FINSEQ_1:56; hence M2 = M/.len M by A8,FINSEQ_4:25; Q = <*t*> by A5,A7,FINSEQ_1:47; then Q/.1 = t by FINSEQ_4:25; hence M/.1 = Firing(Q/.1,M0) by FINSEQ_4:25; let i be Element of NAT; assume i < len Q & i > 0; hence M/.(i+1) = Firing(Q/.(i+1),M/.i) by A8,NAT_1:13; end; suppose A9: Q1<> {}; then consider B2 being Boolean_marking of PTN, B being FinSequence of Bool_marks_of PTN such that A10: len Q1 = len B and A11: B2 = B/.len B and A12: B/.1 = Firing(Q1/.1,M0) and A13: for i being Element of NAT st i < len Q1 & i > 0 holds B/.(i+1) = Firing(Q1/.(i+1),B/.i) by A3,A6; take M2 = Firing(t,B2); take M = B^<*M2*>; A14: len M =len B + len<*M2*> by FINSEQ_1:35 .=len B + 1 by FINSEQ_1:57; A15: len Q = len Q1 + len<*t*> by A5,FINSEQ_1:35 .=len Q1 + 1 by FINSEQ_1:57; hence len Q = len M by A10,A14; thus M2 = M/.len M by A14,FINSEQ_4:82; len Q1 <> 0 by A9,CARD_2:59; then A16: len Q1 > 0 by NAT_1:3; then 0 + 1 < len B + 1 by A10,XREAL_1:8; then A17: 1<= len B by NAT_1:13; then A18: 1 in dom B by FINSEQ_3:27; 0 + 1 < len Q1 + 1 by A16,XREAL_1:8; then 1<= len Q1 by NAT_1:13; then A19: 1 in dom Q1 by FINSEQ_3:27; thus M/.1 = B/.1 by A18,FINSEQ_4:83 .= Firing(Q/.1,M0) by A5,A12,A19,FINSEQ_4:83; let i be Element of NAT such that A20: i < len Q and A21: i > 0; thus M/.(i+1) = Firing(Q/.(i+1),M/.i) proof A22: Seg (len Q1 + 1) = Seg (len Q1) \/ {len Q1 + 1} by FINSEQ_1:11; A23: 1<=i+1 by NAT_1:12; i+1<=len Q1+1 by A15,A20,NAT_1:13; then A24: i+1 in Seg (len Q1 + 1) by A23,FINSEQ_1:3; per cases by A22,A24,XBOOLE_0:def 2; suppose A25: i+1 in Seg (len Q1); then i + 1 <= len Q1 by FINSEQ_1:3; then i < len Q1 by NAT_1:13; then A26: B/.(i+1) = Firing(Q1/.(i+1),B/.i) by A13,A21; 0 + 1 < i + 1 by A21,XREAL_1:8; then A27: 1<=i by NAT_1:13; i+1 in dom B by A10,A25,FINSEQ_1:def 3; then A28: B/.(i+1)=M/.(i+1) by FINSEQ_4:83; A29: i + 1 <= len B by A10,A25,FINSEQ_1:3; i+1 in dom Q1 by A25,FINSEQ_1:def 3; then A30: Q1/.(i+1)=Q/.(i+1) by A5,FINSEQ_4:83; i + 1 <= len B + 1 by A29,NAT_1:12; then i <= len B by XREAL_1:8; then i in dom B by A27,FINSEQ_3:27; hence M/.(i+1) = Firing(Q/.(i+1),M/.i) by A26,A28,A30,FINSEQ_4:83; end; suppose i+1 in {len Q1 + 1}; then A31: i + 1 = len Q1 + 1 by TARSKI:def 1; then A32: M/.(i+1)=M2 by A10,FINSEQ_4:82; A33: Q/.(i+1)=t by A5,A31,FINSEQ_4:82; len B in dom B by A17,FINSEQ_3:27; hence M/.(i+1) = Firing(Q/.(i+1),M/.i) by A10,A11,A31,A32,A33,FINSEQ_4:83; end; end; end; end; end; end; for n being Element of NAT holds P2[n] from NAT_1:sch 1(A1,A2); hence thesis; end; uniqueness proof let B1,B2 be Boolean_marking of PTN; thus Q = {} & B1 = M0 & B2 = M0 implies B1 = B2; assume Q <> {}; given M1 being FinSequence of Bool_marks_of PTN such that A34: len Q = len M1 and A35: B1 = M1/.len M1 and A36: M1/.1 = Firing(Q/.1,M0) and A37: for i being Element of NAT st i < len Q & i > 0 holds M1/.(i+1) = Firing(Q/.(i+1),M1/.i); given M2 being FinSequence of Bool_marks_of PTN such that A38: len Q = len M2 and A39: B2 = M2/.len M2 and A40: M2/.1 = Firing(Q/.1,M0) and A41: for i being Element of NAT st i < len Q & i > 0 holds M2/.(i+1) = Firing(Q/.(i+1),M2/.i); defpred P2[Element of NAT] means $1 in Seg len Q implies M1/.$1 = M2/.$1; A42: P2[0] by FINSEQ_1:3; A43: now let j be Element of NAT; assume A44: P2[j]; now assume A45: j + 1 in Seg len Q; per cases; suppose j = 0; hence M1/.(j+1) = M2/.(j+1) by A36,A40; end; suppose A46: j <> 0; A47: j + 1 <= len Q by A45,FINSEQ_1:3; A48: j < j + 1 by XREAL_1:31; then A49: j > 0 & j < len Q by A46,A47,NAT_1:3,XXREAL_0:2; 1 <= j & j <= len Q by A46,A47,A48,NAT_1:14,XXREAL_0:2; hence M1/.(j+1) = Firing(Q/.(j+1),M2/.j) by A37,A44,A49,FINSEQ_1:3 .= M2/.(j+1) by A41,A49; end; end; hence P2[j+1]; end; A50: for j being Element of NAT holds P2[j] from NAT_1:sch 1(A42,A43); X: dom M1 = Seg len Q by FINSEQ_1:def 3,A34; now let j be Nat; assume A51: j in dom M1; then A52: j in dom M1 & j in dom M2 by A38,FINSEQ_1:def 3,X; hence M1.j = M1/.j by PARTFUN1:def 8 .= M2/.j by A50,A51,X .= M2.j by A52,PARTFUN1:def 8; end; hence B1 = B2 by A34,A35,A38,A39,FINSEQ_2:10; end; correctness; end; canceled; theorem Th5: for A being non empty set, y being set, f being Function holds (f+*(A --> y)).:A = {y} proof let A be non empty set, y be set, f be Function; now let u be set; thus u in (f+*(A --> y)).:A implies u = y proof assume u in (f+*(A --> y)).:A; then consider z being set such that A1: z in dom(f+*(A --> y)) & z in A & u = (f+*(A --> y)).z by FUNCT_1:def 12; z in dom(A --> y) by A1,FUNCOP_1:19; then u = (A --> y).z by A1,FUNCT_4:14; hence u = y by A1,FUNCOP_1:13; end; consider x being set such that A2: x in A by XBOOLE_0:def 1; x in dom(A --> y) & (A --> y).x = y by A2,FUNCOP_1:13,19; then x in dom(f+*(A --> y)) & y = (f+*(A --> y)).x by FUNCT_4:13,14; hence u = y implies u in (f+*(A --> y)).:A by A2,FUNCT_1:def 12; end; hence (f+*(A --> y)).:A = {y} by TARSKI:def 1; end; theorem Th6: for PTN being PT_net_Str, M0 being Boolean_marking of PTN, t being transition of PTN, s being place of PTN st s in {t}*' holds Firing(t,M0).s = TRUE proof let PTN be PT_net_Str, M0 be Boolean_marking of PTN, t be transition of PTN, s be place of PTN; assume A1: s in {t}*'; then A2: ((M0 +* (*'{t}-->FALSE)) +* ({t}*'-->TRUE)).:({t}*') = {TRUE} by Th5; set M = M0 +* (*'{t}-->FALSE) +* ({t}*'-->TRUE); A3: [#]the Places of PTN = the Places of PTN; A4: dom M0 = the Places of PTN & dom (*'{t}-->FALSE) = (*'{t}) & dom ({t}*'-->TRUE) = ({t}*') by FUNCT_2:def 1; then dom M = dom(M0 +* (*'{t}-->FALSE)) \/ {t}*' by FUNCT_4:def 1 .= (the Places of PTN) \/ (*'{t}) \/ ({t}*') by A4,FUNCT_4:def 1 .= (the Places of PTN) \/ ((*'{t}) \/ ({t}*')) by XBOOLE_1:4 .= the Places of PTN by A3,SUBSET_1:28; then M.s in {TRUE} by A1,A2,FUNCT_1:def 12; hence Firing(t,M0).s = TRUE by TARSKI:def 1; end; Lm1: now let PTN be PT_net_Str; let Sd be non empty Subset of the Places of PTN; assume A1: for M0 being Boolean_marking of PTN st M0.:Sd = {FALSE} for t being transition of PTN st t is_firable_on M0 holds Firing(t,M0).:Sd = {FALSE}; assume Sd is not Deadlock-like; then not *'Sd c= Sd*' by PETRI:def 5; then consider t being transition of PTN such that A2: t in *'Sd and A3: not t in Sd*' by SUBSET_1:7; set M0 = ((the Places of PTN)-->TRUE qua Function) +* (Sd-->FALSE); A4: [#]the Places of PTN = the Places of PTN; dom ((the Places of PTN)-->TRUE qua Function) = the Places of PTN & dom (Sd-->FALSE) = Sd by FUNCOP_1:19; then A5: dom M0 = (the Places of PTN) \/ Sd by FUNCT_4:def 1 .= the Places of PTN by A4,SUBSET_1:28; rng ((the Places of PTN)-->TRUE) c= {TRUE} & rng (Sd-->FALSE) c= {FALSE} by FUNCOP_1:19; then rng ((the Places of PTN)-->TRUE) c= BOOLEAN & rng (Sd-->FALSE) c= BOOLEAN by XBOOLE_1:1; then A6: rng ((the Places of PTN)-->TRUE) \/ rng (Sd-->FALSE) c= BOOLEAN by XBOOLE_1:8; rng M0 c= rng ((the Places of PTN)-->TRUE) \/ rng (Sd-->FALSE) by FUNCT_4:18; then rng M0 c= BOOLEAN by A6,XBOOLE_1:1; then reconsider M0 as Boolean_marking of PTN by A5,FUNCT_2:def 2; A7: (M0).:(Sd) = {FALSE qua set} by Th5; Sd misses *'{t} by A3,PETRI:19; then A8: ((the Places of PTN)-->TRUE qua Function).:*'{t} = M0.:*'{t} by Th3; A9: rng ((the Places of PTN)-->TRUE) c= {TRUE} by FUNCOP_1:19; ((the Places of PTN)-->TRUE).:*'{t} c= rng ((the Places of PTN)-->TRUE) by RELAT_1:144; then M0.:*'{t} c= {TRUE} by A8,A9,XBOOLE_1:1; then A10: t is_firable_on M0 by Def2; {t}*' meets Sd by A2,PETRI:20; then consider s being set such that A11: s in {t}*' /\ Sd by XBOOLE_0:4; A12: s in {t}*' & s in Sd by A11,XBOOLE_0:def 3; then Firing(t,M0).s = TRUE by Th6; then TRUE in Firing(t,M0).:Sd by A12,FUNCT_2:43; then Firing(t,M0).:Sd <> {FALSE} by TARSKI:def 1; hence contradiction by A1,A7,A10; end; theorem for PTN being PT_net_Str, 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} for t being transition of PTN st t is_firable_on M0 holds Firing(t,M0).:Sd = {FALSE} proof let PTN be PT_net_Str, Sd be non empty Subset of the Places of PTN; thus Sd is Deadlock-like implies for M0 being Boolean_marking of PTN st M0.:Sd = {FALSE} for t being transition of PTN st t is_firable_on M0 holds Firing(t,M0).:Sd = {FALSE} proof assume Sd is Deadlock-like; then A1: *'Sd is Subset of Sd*' by PETRI:def 5; let M0 be Boolean_marking of PTN such that A2: M0.:Sd = {FALSE}; let t be transition of PTN; assume t is_firable_on M0; 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; end; thus thesis by Lm1; end; theorem Th8: for D being non empty set for Q0,Q1 being FinSequence of D, i being Element of NAT st 1<=i & i<=len Q0 holds (Q0^Q1)/.i=Q0/.i proof let D be non empty set; let Q0,Q1 be FinSequence of D, i be Element of NAT; 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:3,35; then A2: i in dom Q0 implies i in dom (Q0^Q1) by FINSEQ_3:27; i in dom Q0 implies Q0.i=Q0/.i by PARTFUN1:def 8; 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 thesis by A2,A3,FINSEQ_1:3,PARTFUN1:def 8; end; canceled; theorem Th10: for PTN being PT_net_Str, M0 being Boolean_marking of PTN, Q0, Q1 being FinSequence of the Transitions of PTN holds Firing(Q0^Q1,M0) = Firing(Q1,Firing(Q0,M0)) proof let PTN be PT_net_Str; let M0 be Boolean_marking of PTN; let Q0, Q1 be FinSequence of the Transitions of PTN; now per cases; case A1: Q0 = {} & Q1 = {}; then A2: Q0^Q1 = {} by FINSEQ_1:47; 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; end; case A3: Q0 = {} & Q1 <> {}; then Firing(Q0^Q1,M0) = Firing(Q1,M0) by FINSEQ_1:47; hence Firing(Q0^Q1,M0) = Firing(Q1,Firing(Q0,M0)) by A3,Def5; end; case A4: Q0 <> {} & Q1 = {}; then Firing(Q0^Q1,M0) = Firing(Q0,M0) by FINSEQ_1:47; hence Firing(Q0^Q1,M0) = Firing(Q1,Firing(Q0,M0)) by A4,Def5; end; case A5: Q0 <> {} & Q1 <> {}; let i be Element of NAT; A6: len Q0 <> 0 by A5,CARD_2:59; A7: len Q1 <> 0 by A5,CARD_2:59; then len Q0 + len Q1 <> 0 by NAT_1:7; then len(Q0^Q1) <> 0 by FINSEQ_1:35; then Q0^Q1 <> {} by CARD_1:47; then consider M being FinSequence of Bool_marks_of PTN such that A8: len (Q0^Q1) = len M and A9: Firing(Q0^Q1,M0) = M/.len M and A10: M/.1 = Firing((Q0^Q1)/.1,M0) and A11: 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 Def5; consider M3 being FinSequence of Bool_marks_of PTN such that A12: len Q0 = len M3 and A13: Firing(Q0,M0) = M3/.len M3 and A14: M3/.1 = Firing(Q0/.1,M0) and A15: for i being Element of NAT st i < len Q0 & i > 0 holds M3/.(i+1) = Firing(Q0/.(i+1),M3/.i) by A5,Def5; consider M4 being FinSequence of Bool_marks_of PTN such that A16: len Q1 = len M4 and A17: Firing(Q1,Firing(Q0,M0)) = M4/.len M4 and A18: M4/.1 = Firing(Q1/.1,Firing(Q0,M0)) and A19: 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; A20: len Q0 > 0 by A6,NAT_1:3; A21: len Q1 > 0 by A7,NAT_1:3; defpred P2[Element of NAT] means 1+$1<=len Q0 implies M/.(1+$1)=M3/.(1+$1); A22: P2[0] by A10,A14,Th8; 0 {}; hence Q0 is_firable_on M0 by Def4; Q0^Q1 = Q1 & Firing(Q0,M0) = M0 by A2,Def5,FINSEQ_1:47; hence Q1 is_firable_on Firing(Q0,M0) by A1; end; case A3: Q0 <> {} & Q1 = {}; hence Q1 is_firable_on Firing(Q0,M0) by Def4; thus Q0 is_firable_on M0 by A1,A3,FINSEQ_1:47; end; case A4: Q0 <> {} & Q1 <> {}; let i be Element of NAT; A5: len Q0 <> 0 by A4,CARD_2:59; A6: len Q1 <> 0 by A4,CARD_2:59; then len Q0 + len Q1 <> 0 by NAT_1:7; then len(Q0^Q1) <> 0 by FINSEQ_1:35; then Q0^Q1 <> {} by CARD_1:47; then consider M being FinSequence of Bool_marks_of PTN such that len (Q0^Q1) = len M and A7: (Q0^Q1)/.1 is_firable_on M0 and A8: M/.1 = Firing((Q0^Q1)/.1,M0) and A9: 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,Def4; 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 M4 being FinSequence of Bool_marks_of PTN such that A14: len Q1 = len M4 and Firing(Q1,Firing(Q0,M0)) = M4/.len M4 and A15: M4/.1 = Firing(Q1/.1,Firing(Q0,M0)) and A16: 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; A17: len Q0 > 0 by A5,NAT_1:3; A18: len Q1 > 0 by A6,NAT_1:3; A19: 0+1<=len Q0 by A17,NAT_1:13; defpred P2[Element of NAT] means 1+$1<=len Q0 implies M/.(1+$1)=M3/.(1+$1); A20: P2[0] by A8,A12,Th8; 0 0; len (Q0^Q1) = len Q0 + len Q1 by FINSEQ_1:35; then A45: len Q0 + i < len (Q0^Q1) by A44,XREAL_1:8; i < len Q0 + i by A5,NAT_1:3,XREAL_1:31; then A46: (Q0^Q1)/.(len Q0 +i+1) is_firable_on M/.(len Q0+i) & M/.(len Q0+i+1) = Firing((Q0^Q1)/.(len Q0+i+1),M/.(len Q0+i)) by A9,A44,A45; i + 1 >= 1 & i + 1 <= len Q1 by A44,NAT_1:11,13; then A47: i + 1 in dom Q1 by FINSEQ_3:27; A48: (Q0^Q1)/.(len Q0+i+1) = (Q0^Q1)/.(len Q0+(i+1)) .= Q1/.(i+1) by A47,FINSEQ_4:84; consider j being Nat such that A49: i = j + 1 by A44,NAT_1:6; reconsider j as Element of NAT by ORDINAL1:def 13; len Q0 + 1 + j = len Q0 + (j + 1); then A50: M/.(len Q0 + i) = M4/.i by A40,A44,A49; A51: len Q0 + 1 + i = len Q0 + i + 1; i + 1 <= len Q1 by A44,NAT_1:13; hence Q1/.(i+1) is_firable_on M4/.i & M4/.(i+1) = Firing(Q1/.(i+1),M4/.i) by A40,A46,A48,A50,A51; end; hence Q1 is_firable_on Firing(Q0,M0) by A11,A14,A15,A43,Def4; A52: Q0/.1 is_firable_on M0 by A7,A19,Th8; now let i be Element of NAT; assume A53: i < len Q0 & i > 0; then i < len (Q0^Q1) by A21,XXREAL_0:2; then A54: (Q0^Q1)/.(i+1) is_firable_on M/.i & M/.(i+1) = Firing((Q0^Q1)/.(i+1),M/.i) by A9,A53; i + 1 >= 1 & i + 1 <= len Q0 by A53,NAT_1:11,13; then i + 1 in dom Q0 by FINSEQ_3:27; then A55: (Q0^Q1)/.(i+1) = Q0/.(i+1) by FINSEQ_4:83; consider j being Nat such that A56: i = j + 1 by A53,NAT_1:6; reconsider j as Element of NAT by ORDINAL1:def 13; i = j+1 by A56; then A57: M/.i = M3/.i by A29,A53; i + 1 <= len Q0 by A53,NAT_1:13; hence Q0/.(i+1) is_firable_on M3/.i & M3/.(i+1) = Firing(Q0/.(i+1),M3/.i) by A29,A54,A55,A57; end; hence Q0 is_firable_on M0 by A10,A12,A52,Def4; end; end; hence thesis; end; theorem Th12: for PTN being PT_net_Str, M0 being Boolean_marking of PTN, t being transition of PTN holds t is_firable_on M0 iff <*t*> is_firable_on M0 proof let PTN be PT_net_Str, M0 be Boolean_marking of PTN, t be transition of PTN; hereby assume A1: t is_firable_on M0; set M = <*Firing(<*t*>/.1,M0)*>; A2: len <*t*> = 1 by FINSEQ_1:56 .= len M by FINSEQ_1:56; A3: <*t*>/.1 is_firable_on M0 by A1,FINSEQ_4:25; A4: M/.1 = Firing(<*t*>/.1,M0) by FINSEQ_4:25; now let i be Element of NAT such that A5: i < len <*t*> & i > 0; len <*t*> = 0 + 1 by FINSEQ_1:56; hence <*t*>/.(i+1) is_firable_on M/.i & M/.(i+1) = Firing(<*t*>/.(i+1),M/.i) by A5,NAT_1:13; end; hence <*t*> is_firable_on M0 by A2,A3,A4,Def4; end; assume <*t*> is_firable_on M0; then consider M being FinSequence of Bool_marks_of PTN such that len <*t*> = len M and A6: <*t*>/.1 is_firable_on M0 and 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; thus t is_firable_on M0 by A6,FINSEQ_4:25; end; theorem Th13: for PTN being PT_net_Str, M0 being Boolean_marking of PTN, t being transition of PTN holds Firing(t,M0) = Firing(<*t*>,M0) proof let PTN be PT_net_Str, M0 be Boolean_marking of PTN, t be transition of PTN; A1: len <*t*> = 1 & len {} = 0 by CARD_1:47,FINSEQ_1:56; set M = <*Firing(<*t*>/.1,M0)*>; A2: len <*t*> = 1 by FINSEQ_1:56 .= len M by FINSEQ_1:56; A3: <*t*>/.1 = t by FINSEQ_4:25; A4: M/.1 = Firing(<*t*>/.1,M0) by FINSEQ_4:25; now let i be Element of NAT such that A5: i < len <*t*> & i > 0; len <*t*> = 0 + 1 by FINSEQ_1:56; hence M/.(i+1) = Firing(<*t*>/.(i+1),M/.i) by A5,NAT_1:13; end; hence Firing(t,M0) = Firing(<*t*>,M0) by A1,A2,A3,A4,Def5; end; theorem for PTN being PT_net_Str, 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} for Q being FinSequence of the Transitions of PTN st Q is_firable_on M0 holds Firing(Q,M0).:Sd = {FALSE} proof let PTN be PT_net_Str, Sd be non empty Subset of the Places of PTN; thus Sd is Deadlock-like implies for M0 being Boolean_marking of PTN st M0.:Sd = {FALSE} for Q being FinSequence of the Transitions of PTN st Q is_firable_on M0 holds Firing(Q,M0).:Sd = {FALSE} proof assume Sd is Deadlock-like; then A1: *'Sd is Subset of Sd*' by PETRI:def 5; let M0 be Boolean_marking of PTN such that A2: M0.:Sd = {FALSE}; defpred P[FinSequence of the Transitions of PTN] means $1 is_firable_on M0 implies Firing($1,M0).:Sd = {FALSE}; A3: P[<*> the Transitions of PTN] by A2,Def5; A4: now let Q be FinSequence of the Transitions of PTN; let x be transition of PTN; assume A5: P[Q]; thus P[ Q^<*x*>] proof assume A6: Q^<*x*> is_firable_on M0; then A7: <*x*> is_firable_on Firing(Q,M0) by Th11; Firing(Q^<*x*>,M0) = Firing(<*x*>,Firing(Q,M0)) by Th10; then consider M being FinSequence of Bool_marks_of PTN such that A8: len <*x*> = len M and A9: Firing(Q^<*x*>,M0) = M/.len M and A10: M/.1 = Firing(<*x*>/.1,Firing(Q,M0)) and 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 A11: Firing(Q^<*x*>, M0) = Firing(Q,M0) +* (*'{x}-->FALSE) +* ({x}*'-->TRUE) by A8,A9,A10,FINSEQ_1:56; x is_firable_on Firing(Q,M0) by A7,Th12; then Firing(Q,M0).:*'{x} c= {TRUE} by Def2; then Firing(Q,M0).:*'{x} misses {FALSE} by XBOOLE_1:63,ZFMISC_1:17; then A12: *'{x} misses Sd by A5,A6,Th2,Th11; then not x in *'Sd by A1,PETRI:19; then {x}*' misses Sd by PETRI:20; hence Firing(Q^<*x*>,M0).:Sd = (Firing(Q,M0) +* (*'{x}-->FALSE)).:Sd by A11,Th3 .= {FALSE} by A5,A6,A12,Th3,Th11; end; end; thus for Q0 being FinSequence of the Transitions of PTN holds P[Q0] from FINSEQ_2:sch 2(A3,A4); end; assume A13: for M0 being Boolean_marking of PTN st M0.:Sd = {FALSE} for Q being FinSequence of the Transitions of PTN st Q is_firable_on M0 holds Firing(Q,M0).:Sd = {FALSE}; assume *'Sd is not Subset of Sd*'; then consider t being transition of PTN such that A14: t in *'Sd and A15: not t in Sd*' by SUBSET_1:7; set M0 = ((the Places of PTN)-->TRUE qua Function) +* (Sd-->FALSE); A16: [#]the Places of PTN = the Places of PTN; dom ((the Places of PTN)-->TRUE qua Function) = the Places of PTN & dom (Sd-->FALSE) = Sd by FUNCOP_1:19; then A17: dom M0 = (the Places of PTN) \/ Sd by FUNCT_4:def 1 .= the Places of PTN by A16,SUBSET_1:28; rng ((the Places of PTN)-->TRUE) c= {TRUE} & rng (Sd-->FALSE) c= {FALSE} by FUNCOP_1:19; then rng ((the Places of PTN)-->TRUE) c= BOOLEAN & rng (Sd-->FALSE) c= BOOLEAN by XBOOLE_1:1; then A18: rng ((the Places of PTN)-->TRUE) \/ rng (Sd-->FALSE) c= BOOLEAN by XBOOLE_1:8; rng M0 c= rng ((the Places of PTN)-->TRUE) \/ rng (Sd-->FALSE) by FUNCT_4:18; then rng M0 c= BOOLEAN by A18,XBOOLE_1:1; then reconsider M0 as Boolean_marking of PTN by A17,FUNCT_2:def 2; A19: (M0).:(Sd) = {FALSE qua set} by Th5; reconsider Q = <*t*> as FinSequence of the Transitions of PTN; Sd misses *'{t} by A15,PETRI:19; then A20: ((the Places of PTN)-->TRUE qua Function).:*'{t} = M0.:*'{t} by Th3; A21: rng ((the Places of PTN)-->TRUE) c= {TRUE} by FUNCOP_1:19; ((the Places of PTN)-->TRUE).:*'{t} c= rng ((the Places of PTN)--> TRUE ) by RELAT_1:144; then M0.:*'{t} c= {TRUE} by A20,A21,XBOOLE_1:1; then t is_firable_on M0 by Def2; then A22: Q is_firable_on M0 by Th12; {t}*' meets Sd by A14,PETRI:20; then consider s being set such that A23: s in {t}*' /\ Sd by XBOOLE_0:4; A24: s in {t}*' & s in Sd by A23,XBOOLE_0:def 3; then Firing(t,M0).s = TRUE by Th6; then TRUE in Firing(t,M0).:Sd by A24,FUNCT_2:43; then Firing(t,M0).:Sd <> {FALSE} by TARSKI:def 1; then Firing(Q,M0).:Sd <> {FALSE} by Th13; hence contradiction by A13,A19,A22; end;