:: 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;