:: PNPROC_1 semantic presentation
begin
theorem Th1: :: PNPROC_1:1
for i being Element of NAT
for x being set st i > 0 holds
{[i,x]} is FinSubsequence
proof
let i be Element of NAT ; ::_thesis: for x being set st i > 0 holds
{[i,x]} is FinSubsequence
let x be set ; ::_thesis: ( i > 0 implies {[i,x]} is FinSubsequence )
assume A1: i > 0 ; ::_thesis: {[i,x]} is FinSubsequence
A2: dom {[i,x]} = {i} by RELAT_1:9;
{i} c= Seg i
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {i} or x in Seg i )
assume x in {i} ; ::_thesis: x in Seg i
then x = i by TARSKI:def_1;
hence x in Seg i by A1, FINSEQ_1:3; ::_thesis: verum
end;
hence {[i,x]} is FinSubsequence by A2, FINSEQ_1:def_12; ::_thesis: verum
end;
Lm1: for p being FinSubsequence st Seq p = {} holds
p = {}
proof
let p be FinSubsequence; ::_thesis: ( Seq p = {} implies p = {} )
assume A1: Seq p = {} ; ::_thesis: p = {}
A2: Seq p = p * (Sgm (dom p)) by FINSEQ_1:def_14;
rng (Sgm (dom p)) = dom p by FINSEQ_1:50;
then dom {} = dom (Sgm (dom p)) by A1, A2, RELAT_1:27;
then Sgm (dom p) = {} ;
then dom p = rng {} by FINSEQ_1:50;
hence p = {} ; ::_thesis: verum
end;
theorem :: PNPROC_1:2
for q being FinSubsequence holds
( q = {} iff Seq q = {} )
proof
let q be FinSubsequence; ::_thesis: ( q = {} iff Seq q = {} )
thus ( q = {} implies Seq q = {} ) ::_thesis: ( Seq q = {} implies q = {} )
proof
assume A1: q = {} ; ::_thesis: Seq q = {}
Seq q = q * (Sgm (dom q)) by FINSEQ_1:def_14;
hence Seq q = q * {} by A1
.= {} ;
::_thesis: verum
end;
thus ( Seq q = {} implies q = {} ) by Lm1; ::_thesis: verum
end;
theorem Th3: :: PNPROC_1:3
for i being Element of NAT
for x being set
for q being FinSubsequence st q = {[i,x]} holds
Seq q = <*x*>
proof
let i be Element of NAT ; ::_thesis: for x being set
for q being FinSubsequence st q = {[i,x]} holds
Seq q = <*x*>
let x be set ; ::_thesis: for q being FinSubsequence st q = {[i,x]} holds
Seq q = <*x*>
let q be FinSubsequence; ::_thesis: ( q = {[i,x]} implies Seq q = <*x*> )
assume A1: q = {[i,x]} ; ::_thesis: Seq q = <*x*>
then [i,x] in q by TARSKI:def_1;
then A2: i in dom q by XTUPLE_0:def_12;
ex k being Nat st dom q c= Seg k by FINSEQ_1:def_12;
then i >= 0 + 1 by A2, FINSEQ_1:1;
then A3: i > 0 by NAT_1:13;
then reconsider p = {[i,x]} as FinSubsequence by Th1;
A4: Seq q = q * (Sgm (dom q)) by FINSEQ_1:def_14;
dom p = {i} by RELAT_1:9;
then Seq p = {[i,x]} * <*i*> by A1, A3, A4, FINSEQ_3:44
.= <*({[i,x]} . i)*> by A1, A2, FINSEQ_2:34
.= <*x*> by GRFUNC_1:6 ;
hence Seq q = <*x*> by A1; ::_thesis: verum
end;
registration
cluster Relation-like Function-like FinSubsequence-like -> finite for set ;
coherence
for b1 being FinSubsequence holds b1 is finite
proof
let q be FinSubsequence; ::_thesis: q is finite
ex n being Nat st dom q c= Seg n by FINSEQ_1:def_12;
hence q is finite by FINSET_1:10; ::_thesis: verum
end;
end;
theorem Th4: :: PNPROC_1:4
for x being set
for q being FinSubsequence st Seq q = <*x*> holds
ex i being Element of NAT st q = {[i,x]}
proof
let x be set ; ::_thesis: for q being FinSubsequence st Seq q = <*x*> holds
ex i being Element of NAT st q = {[i,x]}
let q be FinSubsequence; ::_thesis: ( Seq q = <*x*> implies ex i being Element of NAT st q = {[i,x]} )
assume Seq q = <*x*> ; ::_thesis: ex i being Element of NAT st q = {[i,x]}
then A1: Seq q = {[1,x]} by FINSEQ_1:def_5;
then A2: dom (Seq q) = {1} by RELAT_1:9;
A3: rng (Seq q) = {x} by A1, RELAT_1:9;
A4: Seq q = q * (Sgm (dom q)) by FINSEQ_1:def_14;
A5: rng (Sgm (dom q)) = dom q by FINSEQ_1:50;
then A6: {1} = dom (Sgm (dom q)) by A2, A4, RELAT_1:27;
A7: rng (Seq q) = rng q by A4, A5, RELAT_1:28;
consider n being Nat such that
A8: dom q c= Seg n by FINSEQ_1:def_12;
Seg (card (dom q)) = {1} by A6, A8, FINSEQ_3:40;
then card (dom q) = card {1} by FINSEQ_1:57;
then consider y being set such that
A9: dom q = {y} by CARD_1:29;
y in dom q by A9, TARSKI:def_1;
then y in Seg n by A8;
then reconsider y = y as Element of NAT ;
q = {[y,x]} by A3, A7, A9, PRE_CIRC:1;
hence ex i being Element of NAT st q = {[i,x]} ; ::_thesis: verum
end;
theorem Th5: :: PNPROC_1:5
for x1, y1, x2, y2 being set holds
( not {[x1,y1],[x2,y2]} is FinSequence or ( x1 = 1 & x2 = 1 & y1 = y2 ) or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) )
proof
let x1, y1, x2, y2 be set ; ::_thesis: ( not {[x1,y1],[x2,y2]} is FinSequence or ( x1 = 1 & x2 = 1 & y1 = y2 ) or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) )
assume {[x1,y1],[x2,y2]} is FinSequence ; ::_thesis: ( ( x1 = 1 & x2 = 1 & y1 = y2 ) or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) )
then reconsider p = {[x1,y1],[x2,y2]} as FinSequence ;
A1: dom p = {x1,x2} by RELAT_1:10;
then A2: x1 in dom p by TARSKI:def_2;
A3: x2 in dom p by A1, TARSKI:def_2;
A4: [x1,y1] in p by TARSKI:def_2;
A5: [x2,y2] in p by TARSKI:def_2;
A6: p . x1 = y1 by A4, FUNCT_1:1;
A7: p . x2 = y2 by A5, FUNCT_1:1;
A8: dom p = Seg (len p) by FINSEQ_1:def_3;
A9: len p <= 1 + 1 by CARD_2:50;
len p > 0 by NAT_1:3;
then A10: len p >= 0 + 1 by NAT_1:13;
A11: now__::_thesis:_(_len_p_=_1_implies_(_x1_=_1_&_x2_=_1_&_y1_=_y2_)_)
assume len p = 1 ; ::_thesis: ( x1 = 1 & x2 = 1 & y1 = y2 )
hence ( x1 = 1 & x2 = 1 ) by A2, A3, A8, FINSEQ_1:2, TARSKI:def_1; ::_thesis: y1 = y2
hence y1 = y2 by A5, A6, FUNCT_1:1; ::_thesis: verum
end;
now__::_thesis:_(_not_len_p_=_2_or_(_x1_=_1_&_x2_=_2_)_or_(_x1_=_2_&_x2_=_1_)_)
assume A12: len p = 2 ; ::_thesis: ( ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) )
A13: ( x1 = x2 implies p = {[x1,y1]} ) by A6, A7, ENUMSET1:29;
( ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) or ( x1 = 1 & x2 = 1 ) or ( x1 = 2 & x2 = 2 ) ) by A2, A3, A8, A12, FINSEQ_1:2, TARSKI:def_2;
hence ( ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) ) by A12, A13, CARD_1:30; ::_thesis: verum
end;
hence ( ( x1 = 1 & x2 = 1 & y1 = y2 ) or ( x1 = 1 & x2 = 2 ) or ( x1 = 2 & x2 = 1 ) ) by A9, A10, A11, NAT_1:9; ::_thesis: verum
end;
theorem Th6: :: PNPROC_1:6
for x1, x2 being set holds <*x1,x2*> = {[1,x1],[2,x2]}
proof
let x1, x2 be set ; ::_thesis: <*x1,x2*> = {[1,x1],[2,x2]}
reconsider f = {[1,x1],[2,x2]} as Function by GRFUNC_1:8;
A1: dom f = {1,2} by RELAT_1:10;
then A2: dom <*x1,x2*> = dom f by FINSEQ_1:2, FINSEQ_1:89;
now__::_thesis:_for_x_being_set_st_x_in_{1,2}_holds_
f_._x_=_<*x1,x2*>_._x
let x be set ; ::_thesis: ( x in {1,2} implies f . b1 = <*x1,x2*> . b1 )
assume A3: x in {1,2} ; ::_thesis: f . b1 = <*x1,x2*> . b1
percases ( x = 1 or x = 2 ) by A3, TARSKI:def_2;
supposeA4: x = 1 ; ::_thesis: f . b1 = <*x1,x2*> . b1
then A5: <*x1,x2*> . x = x1 by FINSEQ_1:44;
[x,x1] in f by A4, TARSKI:def_2;
hence f . x = <*x1,x2*> . x by A5, FUNCT_1:1; ::_thesis: verum
end;
supposeA6: x = 2 ; ::_thesis: f . b1 = <*x1,x2*> . b1
then A7: <*x1,x2*> . x = x2 by FINSEQ_1:44;
[x,x2] in f by A6, TARSKI:def_2;
hence f . x = <*x1,x2*> . x by A7, FUNCT_1:1; ::_thesis: verum
end;
end;
end;
hence <*x1,x2*> = {[1,x1],[2,x2]} by A1, A2, FUNCT_1:2; ::_thesis: verum
end;
Lm2: for j, k, l being Element of NAT st ( ( 1 <= j & j <= l ) or ( l + 1 <= j & j <= l + k ) ) holds
( 1 <= j & j <= l + k )
proof
let j, k, l be Element of NAT ; ::_thesis: ( ( ( 1 <= j & j <= l ) or ( l + 1 <= j & j <= l + k ) ) implies ( 1 <= j & j <= l + k ) )
assume A1: ( ( 1 <= j & j <= l ) or ( l + 1 <= j & j <= l + k ) ) ; ::_thesis: ( 1 <= j & j <= l + k )
percases ( ( 1 <= j & j <= l ) or ( l + 1 <= j & j <= l + k ) ) by A1;
supposeA2: ( 1 <= j & j <= l ) ; ::_thesis: ( 1 <= j & j <= l + k )
0 <= k by NAT_1:2;
then l + 0 <= l + k by XREAL_1:7;
hence ( 1 <= j & j <= l + k ) by A2, XXREAL_0:2; ::_thesis: verum
end;
supposeA3: ( l + 1 <= j & j <= l + k ) ; ::_thesis: ( 1 <= j & j <= l + k )
0 <= l by NAT_1:2;
then 0 + 1 <= l + 1 by XREAL_1:7;
hence ( 1 <= j & j <= l + k ) by A3, XXREAL_0:2; ::_thesis: verum
end;
end;
end;
theorem Th7: :: PNPROC_1:7
for p being FinSubsequence holds card p = len (Seq p)
proof
let p be FinSubsequence; ::_thesis: card p = len (Seq p)
A1: ex k being Nat st dom p c= Seg k by FINSEQ_1:def_12;
A2: Seq p = p * (Sgm (dom p)) by FINSEQ_1:def_14;
A3: rng (Sgm (dom p)) = dom p by FINSEQ_1:50;
then A4: dom (Seq p) = dom (Sgm (dom p)) by A2, RELAT_1:27;
Sgm (dom p) is one-to-one by A1, FINSEQ_3:92;
then rng (Sgm (dom p)), dom (Sgm (dom p)) are_equipotent by WELLORD2:def_4;
then A5: card (dom p) = card (dom (Sgm (dom p))) by A3, CARD_1:5;
card (dom p) = card p by CARD_1:62;
hence card p = len (Seq p) by A4, A5, CARD_1:62; ::_thesis: verum
end;
Lm3: for X, Y being set holds
( ( for x being set st x in X holds
not x in Y ) iff X misses Y )
proof
let X, Y be set ; ::_thesis: ( ( for x being set st x in X holds
not x in Y ) iff X misses Y )
thus ( ( for x being set st x in X holds
not x in Y ) implies X misses Y ) ::_thesis: ( X misses Y implies for x being set st x in X holds
not x in Y )
proof
assume A1: for x being set st x in X holds
not x in Y ; ::_thesis: X misses Y
now__::_thesis:_for_x1_being_set_holds_not_x1_in_X_/\_Y
given x1 being set such that A2: x1 in X /\ Y ; ::_thesis: contradiction
A3: x1 in X by A2, XBOOLE_0:def_4;
x1 in Y by A2, XBOOLE_0:def_4;
hence contradiction by A1, A3; ::_thesis: verum
end;
then X /\ Y = {} by XBOOLE_0:def_1;
hence X misses Y by XBOOLE_0:def_7; ::_thesis: verum
end;
assume A4: X misses Y ; ::_thesis: for x being set st x in X holds
not x in Y
now__::_thesis:_for_x_being_set_st_x_in_X_holds_
not_x_in_Y
let x be set ; ::_thesis: ( x in X implies not x in Y )
assume A5: x in X ; ::_thesis: not x in Y
now__::_thesis:_not_x_in_Y
assume x in Y ; ::_thesis: contradiction
then x in X /\ Y by A5, XBOOLE_0:def_4;
hence contradiction by A4, XBOOLE_0:def_7; ::_thesis: verum
end;
hence not x in Y ; ::_thesis: verum
end;
hence for x being set st x in X holds
not x in Y ; ::_thesis: verum
end;
Lm4: for P, R being Relation st dom P misses dom R holds
P misses R
by RELAT_1:179;
theorem Th8: :: PNPROC_1:8
for X, Y being set
for P, R being Relation st X misses Y holds
P | X misses R | Y
proof
let X, Y be set ; ::_thesis: for P, R being Relation st X misses Y holds
P | X misses R | Y
let P, R be Relation; ::_thesis: ( X misses Y implies P | X misses R | Y )
assume X misses Y ; ::_thesis: P | X misses R | Y
then A1: X /\ Y = {} by XBOOLE_0:def_7;
A2: dom (P | X) = (dom P) /\ X by RELAT_1:61;
dom (R | Y) = (dom R) /\ Y by RELAT_1:61;
then (dom (P | X)) /\ (dom (R | Y)) = (dom P) /\ (X /\ ((dom R) /\ Y)) by A2, XBOOLE_1:16
.= (dom P) /\ ((X /\ Y) /\ (dom R)) by XBOOLE_1:16
.= {} by A1 ;
then dom (P | X) misses dom (R | Y) by XBOOLE_0:def_7;
hence P | X misses R | Y by Lm4; ::_thesis: verum
end;
Lm5: for q being FinSubsequence holds dom (Seq q) = dom (Sgm (dom q))
proof
let q be FinSubsequence; ::_thesis: dom (Seq q) = dom (Sgm (dom q))
A1: Seq q = q * (Sgm (dom q)) by FINSEQ_1:def_14;
rng (Sgm (dom q)) = dom q by FINSEQ_1:50;
hence dom (Seq q) = dom (Sgm (dom q)) by A1, RELAT_1:27; ::_thesis: verum
end;
Lm6: for q being FinSubsequence holds rng q = rng (Seq q)
proof
let q be FinSubsequence; ::_thesis: rng q = rng (Seq q)
A1: rng (Seq q) = rng (q * (Sgm (dom q))) by FINSEQ_1:def_14;
dom q = rng (Sgm (dom q)) by FINSEQ_1:50;
hence rng q = rng (Seq q) by A1, RELAT_1:28; ::_thesis: verum
end;
theorem Th9: :: PNPROC_1:9
for f, g, h being Function st f c= h & g c= h & f misses g holds
dom f misses dom g
proof
let f, g, h be Function; ::_thesis: ( f c= h & g c= h & f misses g implies dom f misses dom g )
assume that
A1: f c= h and
A2: g c= h and
A3: f misses g ; ::_thesis: dom f misses dom g
for x being set st x in dom f holds
not x in dom g
proof
let x be set ; ::_thesis: ( x in dom f implies not x in dom g )
assume x in dom f ; ::_thesis: not x in dom g
then A4: [x,(f . x)] in f by FUNCT_1:def_2;
now__::_thesis:_not_x_in_dom_g
assume x in dom g ; ::_thesis: contradiction
then A5: [x,(g . x)] in g by FUNCT_1:def_2;
then f . x = g . x by A1, A2, A4, FUNCT_1:def_1;
hence contradiction by A3, A4, A5, Lm3; ::_thesis: verum
end;
hence not x in dom g ; ::_thesis: verum
end;
hence dom f misses dom g by Lm3; ::_thesis: verum
end;
theorem :: PNPROC_1:10
for Y being set
for R being Relation holds Y |` R c= R | (R " Y)
proof
let Y be set ; ::_thesis: for R being Relation holds Y |` R c= R | (R " Y)
let R be Relation; ::_thesis: Y |` R c= R | (R " Y)
let a, b be set ; :: according to RELAT_1:def_3 ::_thesis: ( not [a,b] in Y |` R or [a,b] in R | (R " Y) )
assume A1: [a,b] in Y |` R ; ::_thesis: [a,b] in R | (R " Y)
then A2: b in Y by RELAT_1:def_12;
A3: [a,b] in R by A1, RELAT_1:def_12;
then a in R " Y by A2, RELAT_1:def_14;
hence [a,b] in R | (R " Y) by A3, RELAT_1:def_11; ::_thesis: verum
end;
theorem Th11: :: PNPROC_1:11
for Y being set
for f being Function holds Y |` f = f | (f " Y)
proof
let Y be set ; ::_thesis: for f being Function holds Y |` f = f | (f " Y)
let f be Function; ::_thesis: Y |` f = f | (f " Y)
let x, y be set ; :: according to RELAT_1:def_2 ::_thesis: ( ( not [x,y] in Y |` f or [x,y] in f | (f " Y) ) & ( not [x,y] in f | (f " Y) or [x,y] in Y |` f ) )
thus ( [x,y] in Y |` f implies [x,y] in f | (f " Y) ) ::_thesis: ( not [x,y] in f | (f " Y) or [x,y] in Y |` f )
proof
assume A1: [x,y] in Y |` f ; ::_thesis: [x,y] in f | (f " Y)
then A2: y in Y by RELAT_1:def_12;
A3: [x,y] in f by A1, RELAT_1:def_12;
then A4: x in dom f by FUNCT_1:1;
f . x in Y by A2, A3, FUNCT_1:1;
then x in f " Y by A4, FUNCT_1:def_7;
hence [x,y] in f | (f " Y) by A3, RELAT_1:def_11; ::_thesis: verum
end;
assume A5: [x,y] in f | (f " Y) ; ::_thesis: [x,y] in Y |` f
then A6: x in f " Y by RELAT_1:def_11;
A7: [x,y] in f by A5, RELAT_1:def_11;
f . x in Y by A6, FUNCT_1:def_7;
then y in Y by A7, FUNCT_1:1;
hence [x,y] in Y |` f by A7, RELAT_1:def_12; ::_thesis: verum
end;
begin
definition
let P be set ;
mode marking of P is Function of P,NAT;
end;
notation
let P be set ;
let m be marking of P;
let p be set ;
synonym m multitude_of p for P . m;
end;
scheme :: PNPROC_1:sch 1
MarkingLambda{ F1() -> set , F2( set ) -> Element of NAT } :
ex m being Function of F1(),NAT st
for p being set st p in F1() holds
m . p = F2(p)
proof
consider m being Function such that
A1: dom m = F1() and
A2: for p being set st p in F1() holds
m . p = F2(p) from FUNCT_1:sch_3();
rng m c= NAT
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng m or y in NAT )
assume y in rng m ; ::_thesis: y in NAT
then consider x being set such that
A3: x in dom m and
A4: y = m . x by FUNCT_1:def_3;
y = F2(x) by A1, A2, A3, A4;
hence y in NAT ; ::_thesis: verum
end;
then reconsider m = m as marking of F1() by A1, FUNCT_2:67, RELSET_1:4;
take m ; ::_thesis: for p being set st p in F1() holds
m . p = F2(p)
thus for p being set st p in F1() holds
m . p = F2(p) by A2; ::_thesis: verum
end;
definition
let P be set ;
let m1, m2 be marking of P;
:: original: =
redefine predm1 = m2 means :: PNPROC_1:def 1
for p being set st p in P holds
p multitude_of = p multitude_of ;
compatibility
( m1 = m2 iff for p being set st p in P holds
p multitude_of = p multitude_of )
proof
thus ( m1 = m2 implies for p being set st p in P holds
p multitude_of = p multitude_of ) ; ::_thesis: ( ( for p being set st p in P holds
p multitude_of = p multitude_of ) implies m1 = m2 )
A1: dom m1 = P by FUNCT_2:def_1;
dom m2 = P by FUNCT_2:def_1;
hence ( ( for p being set st p in P holds
p multitude_of = p multitude_of ) implies m1 = m2 ) by A1, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem defines = PNPROC_1:def_1_:_
for P being set
for m1, m2 being marking of P holds
( m1 = m2 iff for p being set st p in P holds
p multitude_of = p multitude_of );
definition
let P be set ;
func {$} P -> marking of P equals :: PNPROC_1:def 2
P --> 0;
coherence
P --> 0 is marking of P ;
end;
:: deftheorem defines {$} PNPROC_1:def_2_:_
for P being set holds {$} P = P --> 0;
definition
let P be set ;
let m1, m2 be marking of P;
predm1 c= m2 means :Def3: :: PNPROC_1:def 3
for p being set st p in P holds
p multitude_of <= p multitude_of ;
reflexivity
for m1 being marking of P
for p being set st p in P holds
p multitude_of <= p multitude_of ;
end;
:: deftheorem Def3 defines c= PNPROC_1:def_3_:_
for P being set
for m1, m2 being marking of P holds
( m1 c= m2 iff for p being set st p in P holds
p multitude_of <= p multitude_of );
Lm7: for p, P being set st p in P holds
({$} P) . p = 0
by FUNCOP_1:7;
theorem Th12: :: PNPROC_1:12
for P being set
for m being marking of P holds {$} P c= m
proof
let P be set ; ::_thesis: for m being marking of P holds {$} P c= m
let m be marking of P; ::_thesis: {$} P c= m
let p be set ; :: according to PNPROC_1:def_3 ::_thesis: ( p in P implies p multitude_of <= p multitude_of )
assume p in P ; ::_thesis: p multitude_of <= p multitude_of
then ({$} P) . p = 0 by Lm7;
hence p multitude_of <= p multitude_of by NAT_1:2; ::_thesis: verum
end;
theorem Th13: :: PNPROC_1:13
for P being set
for m1, m2, m3 being marking of P st m1 c= m2 & m2 c= m3 holds
m1 c= m3
proof
let P be set ; ::_thesis: for m1, m2, m3 being marking of P st m1 c= m2 & m2 c= m3 holds
m1 c= m3
let m1, m2, m3 be marking of P; ::_thesis: ( m1 c= m2 & m2 c= m3 implies m1 c= m3 )
assume that
A1: m1 c= m2 and
A2: m2 c= m3 ; ::_thesis: m1 c= m3
let p be set ; :: according to PNPROC_1:def_3 ::_thesis: ( p in P implies p multitude_of <= p multitude_of )
assume A3: p in P ; ::_thesis: p multitude_of <= p multitude_of
then A4: m1 . p <= m2 . p by A1, Def3;
m2 . p <= m3 . p by A2, A3, Def3;
hence p multitude_of <= p multitude_of by A4, XXREAL_0:2; ::_thesis: verum
end;
definition
let P be set ;
let m1, m2 be marking of P;
:: original: +
redefine funcm1 + m2 -> marking of P means :Def4: :: PNPROC_1:def 4
for p being set st p in P holds
p multitude_of = (p multitude_of ) + (p multitude_of );
coherence
m1 + m2 is marking of P
proof
dom (m1 + m2) = P by FUNCT_2:def_1;
hence m1 + m2 is marking of P ; ::_thesis: verum
end;
compatibility
for b1 being marking of P holds
( b1 = m1 + m2 iff for p being set st p in P holds
p multitude_of = (p multitude_of ) + (p multitude_of ) )
proof
let m be marking of P; ::_thesis: ( m = m1 + m2 iff for p being set st p in P holds
p multitude_of = (p multitude_of ) + (p multitude_of ) )
thus ( m = m1 + m2 implies for p being set st p in P holds
p multitude_of = (p multitude_of ) + (p multitude_of ) ) by VALUED_1:1; ::_thesis: ( ( for p being set st p in P holds
p multitude_of = (p multitude_of ) + (p multitude_of ) ) implies m = m1 + m2 )
assume A1: for p being set st p in P holds
p multitude_of = (p multitude_of ) + (p multitude_of ) ; ::_thesis: m = m1 + m2
A2: dom m = P by FUNCT_2:def_1;
A3: dom (m1 + m2) = (dom m1) /\ (dom m2) by VALUED_1:def_1
.= P /\ (dom m2) by FUNCT_2:def_1
.= P /\ P by FUNCT_2:def_1 ;
now__::_thesis:_for_x_being_set_st_x_in_dom_m_holds_
m_._x_=_(m1_+_m2)_._x
let x be set ; ::_thesis: ( x in dom m implies m . x = (m1 + m2) . x )
assume A4: x in dom m ; ::_thesis: m . x = (m1 + m2) . x
hence m . x = (m1 . x) + (m2 . x) by A1, A2
.= (m1 + m2) . x by A2, A3, A4, VALUED_1:def_1 ;
::_thesis: verum
end;
hence m = m1 + m2 by A2, A3, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines + PNPROC_1:def_4_:_
for P being set
for m1, m2, b4 being marking of P holds
( b4 = m1 + m2 iff for p being set st p in P holds
p multitude_of = (p multitude_of ) + (p multitude_of ) );
theorem :: PNPROC_1:14
for P being set
for m being marking of P holds m + ({$} P) = m
proof
let P be set ; ::_thesis: for m being marking of P holds m + ({$} P) = m
let m be marking of P; ::_thesis: m + ({$} P) = m
now__::_thesis:_for_p_being_set_st_p_in_P_holds_
m_._p_=_(m_._p)_+_(({$}_P)_._p)
let p be set ; ::_thesis: ( p in P implies m . p = (m . p) + (({$} P) . p) )
assume p in P ; ::_thesis: m . p = (m . p) + (({$} P) . p)
then ({$} P) . p = 0 by Lm7;
hence m . p = (m . p) + (({$} P) . p) ; ::_thesis: verum
end;
hence m + ({$} P) = m by Def4; ::_thesis: verum
end;
definition
let P be set ;
let m1, m2 be marking of P;
assume B1: m2 c= m1 ;
funcm1 - m2 -> marking of P means :Def5: :: PNPROC_1:def 5
for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of );
existence
ex b1 being marking of P st
for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of )
proof
deffunc H1( set ) -> Element of NAT = ($1 multitude_of ) -' ($1 multitude_of );
consider m being marking of P such that
A1: for p being set st p in P holds
p multitude_of = H1(p) from PNPROC_1:sch_1();
take m ; ::_thesis: for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of )
let p be set ; ::_thesis: ( p in P implies p multitude_of = (p multitude_of ) - (p multitude_of ) )
assume A2: p in P ; ::_thesis: p multitude_of = (p multitude_of ) - (p multitude_of )
then A3: p multitude_of >= p multitude_of by B1, Def3;
thus p multitude_of = (p multitude_of ) -' (p multitude_of ) by A1, A2
.= (p multitude_of ) - (p multitude_of ) by A3, XREAL_1:233 ; ::_thesis: verum
end;
uniqueness
for b1, b2 being marking of P st ( for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of ) ) & ( for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of ) ) holds
b1 = b2
proof
let M1, M2 be marking of P; ::_thesis: ( ( for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of ) ) & ( for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of ) ) implies M1 = M2 )
assume that
A4: for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of ) and
A5: for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of ) ; ::_thesis: M1 = M2
let p be set ; :: according to PNPROC_1:def_1 ::_thesis: ( p in P implies p multitude_of = p multitude_of )
assume A6: p in P ; ::_thesis: p multitude_of = p multitude_of
hence p multitude_of = (p multitude_of ) - (p multitude_of ) by A4
.= p multitude_of by A5, A6 ;
::_thesis: verum
end;
end;
:: deftheorem Def5 defines - PNPROC_1:def_5_:_
for P being set
for m1, m2 being marking of P st m2 c= m1 holds
for b4 being marking of P holds
( b4 = m1 - m2 iff for p being set st p in P holds
p multitude_of = (p multitude_of ) - (p multitude_of ) );
theorem Th15: :: PNPROC_1:15
for P being set
for m1, m2 being marking of P holds m1 c= m1 + m2
proof
let P be set ; ::_thesis: for m1, m2 being marking of P holds m1 c= m1 + m2
let m1, m2 be marking of P; ::_thesis: m1 c= m1 + m2
let p be set ; :: according to PNPROC_1:def_3 ::_thesis: ( p in P implies p multitude_of <= p multitude_of )
assume p in P ; ::_thesis: p multitude_of <= p multitude_of
then p multitude_of = (p multitude_of ) + (p multitude_of ) by Def4;
hence p multitude_of <= p multitude_of by NAT_1:11; ::_thesis: verum
end;
theorem :: PNPROC_1:16
for P being set
for m being marking of P holds m - ({$} P) = m
proof
let P be set ; ::_thesis: for m being marking of P holds m - ({$} P) = m
let m be marking of P; ::_thesis: m - ({$} P) = m
A1: now__::_thesis:_for_p_being_set_st_p_in_P_holds_
m_._p_=_(m_._p)_-_(({$}_P)_._p)
let p be set ; ::_thesis: ( p in P implies m . p = (m . p) - (({$} P) . p) )
assume p in P ; ::_thesis: m . p = (m . p) - (({$} P) . p)
then ({$} P) . p = 0 by Lm7;
hence m . p = (m . p) - (({$} P) . p) ; ::_thesis: verum
end;
{$} P c= m by Th12;
hence m - ({$} P) = m by A1, Def5; ::_thesis: verum
end;
theorem :: PNPROC_1:17
for P being set
for m1, m2, m3 being marking of P st m1 c= m2 & m2 c= m3 holds
m3 - m2 c= m3 - m1
proof
let P be set ; ::_thesis: for m1, m2, m3 being marking of P st m1 c= m2 & m2 c= m3 holds
m3 - m2 c= m3 - m1
let m1, m2, m3 be marking of P; ::_thesis: ( m1 c= m2 & m2 c= m3 implies m3 - m2 c= m3 - m1 )
assume that
A1: m1 c= m2 and
A2: m2 c= m3 ; ::_thesis: m3 - m2 c= m3 - m1
A3: m1 c= m3 by A1, A2, Th13;
let p be set ; :: according to PNPROC_1:def_3 ::_thesis: ( p in P implies p multitude_of <= p multitude_of )
assume A4: p in P ; ::_thesis: p multitude_of <= p multitude_of
then A5: m1 . p <= m2 . p by A1, Def3;
A6: (m3 - m1) . p = (m3 . p) - (m1 . p) by A3, A4, Def5;
(m3 - m2) . p = (m3 . p) - (m2 . p) by A2, A4, Def5;
hence p multitude_of <= p multitude_of by A5, A6, XREAL_1:10; ::_thesis: verum
end;
theorem Th18: :: PNPROC_1:18
for P being set
for m1, m2 being marking of P holds (m1 + m2) - m2 = m1
proof
let P be set ; ::_thesis: for m1, m2 being marking of P holds (m1 + m2) - m2 = m1
let m1, m2 be marking of P; ::_thesis: (m1 + m2) - m2 = m1
let p be set ; :: according to PNPROC_1:def_1 ::_thesis: ( p in P implies p multitude_of = p multitude_of )
assume A1: p in P ; ::_thesis: p multitude_of = p multitude_of
m2 c= m1 + m2 by Th15;
hence ((m1 + m2) - m2) . p = ((m1 + m2) . p) - (m2 . p) by A1, Def5
.= ((m1 . p) + (m2 . p)) - (m2 . p) by A1, Def4
.= m1 . p ;
::_thesis: verum
end;
theorem Th19: :: PNPROC_1:19
for P being set
for m, m1, m2 being marking of P st m c= m1 & m1 c= m2 holds
m1 - m c= m2 - m
proof
let P be set ; ::_thesis: for m, m1, m2 being marking of P st m c= m1 & m1 c= m2 holds
m1 - m c= m2 - m
let m, m1, m2 be marking of P; ::_thesis: ( m c= m1 & m1 c= m2 implies m1 - m c= m2 - m )
assume A1: m c= m1 ; ::_thesis: ( not m1 c= m2 or m1 - m c= m2 - m )
assume A2: m1 c= m2 ; ::_thesis: m1 - m c= m2 - m
let p be set ; :: according to PNPROC_1:def_3 ::_thesis: ( p in P implies p multitude_of <= p multitude_of )
assume A3: p in P ; ::_thesis: p multitude_of <= p multitude_of
A4: m c= m2 by A1, A2, Th13;
m1 . p <= m2 . p by A2, A3, Def3;
then (m1 . p) - (m . p) <= (m2 . p) - (m . p) by XREAL_1:9;
then (m1 - m) . p <= (m2 . p) - (m . p) by A1, A3, Def5;
hence p multitude_of <= p multitude_of by A3, A4, Def5; ::_thesis: verum
end;
theorem Th20: :: PNPROC_1:20
for P being set
for m1, m2, m3 being marking of P st m1 c= m2 holds
(m2 + m3) - m1 = (m2 - m1) + m3
proof
let P be set ; ::_thesis: for m1, m2, m3 being marking of P st m1 c= m2 holds
(m2 + m3) - m1 = (m2 - m1) + m3
let m1, m2, m3 be marking of P; ::_thesis: ( m1 c= m2 implies (m2 + m3) - m1 = (m2 - m1) + m3 )
assume A1: m1 c= m2 ; ::_thesis: (m2 + m3) - m1 = (m2 - m1) + m3
let p be set ; :: according to PNPROC_1:def_1 ::_thesis: ( p in P implies p multitude_of = p multitude_of )
assume A2: p in P ; ::_thesis: p multitude_of = p multitude_of
m2 c= m2 + m3 by Th15;
then A3: m1 c= m2 + m3 by A1, Th13;
((m2 - m1) + m3) . p = ((m2 - m1) . p) + (m3 . p) by A2, Def4
.= (m3 . p) + ((m2 . p) - (m1 . p)) by A1, A2, Def5
.= ((m3 . p) + (m2 . p)) - (m1 . p)
.= ((m3 + m2) . p) - (m1 . p) by A2, Def4
.= ((m2 + m3) - m1) . p by A2, A3, Def5 ;
hence p multitude_of = p multitude_of ; ::_thesis: verum
end;
theorem :: PNPROC_1:21
for P being set
for m1, m2 being marking of P st m1 c= m2 & m2 c= m1 holds
m1 = m2
proof
let P be set ; ::_thesis: for m1, m2 being marking of P st m1 c= m2 & m2 c= m1 holds
m1 = m2
let m1, m2 be marking of P; ::_thesis: ( m1 c= m2 & m2 c= m1 implies m1 = m2 )
assume A1: m1 c= m2 ; ::_thesis: ( not m2 c= m1 or m1 = m2 )
assume A2: m2 c= m1 ; ::_thesis: m1 = m2
let p be set ; :: according to PNPROC_1:def_1 ::_thesis: ( p in P implies p multitude_of = p multitude_of )
assume A3: p in P ; ::_thesis: p multitude_of = p multitude_of
then A4: m1 . p <= m2 . p by A1, Def3;
m2 . p <= m1 . p by A2, A3, Def3;
hence p multitude_of = p multitude_of by A4, XXREAL_0:1; ::_thesis: verum
end;
theorem Th22: :: PNPROC_1:22
for P being set
for m1, m2, m3 being marking of P holds (m1 + m2) + m3 = m1 + (m2 + m3)
proof
let P be set ; ::_thesis: for m1, m2, m3 being marking of P holds (m1 + m2) + m3 = m1 + (m2 + m3)
let m1, m2, m3 be marking of P; ::_thesis: (m1 + m2) + m3 = m1 + (m2 + m3)
let p be set ; :: according to PNPROC_1:def_1 ::_thesis: ( p in P implies p multitude_of = p multitude_of )
assume A1: p in P ; ::_thesis: p multitude_of = p multitude_of
then A2: ((m1 + m2) + m3) . p = ((m1 + m2) . p) + (m3 . p) by Def4
.= ((m1 . p) + (m2 . p)) + (m3 . p) by A1, Def4 ;
(m1 + (m2 + m3)) . p = (m1 . p) + ((m2 + m3) . p) by A1, Def4
.= (m1 . p) + ((m2 . p) + (m3 . p)) by A1, Def4
.= ((m1 . p) + (m2 . p)) + (m3 . p) ;
hence p multitude_of = p multitude_of by A2; ::_thesis: verum
end;
theorem :: PNPROC_1:23
for P being set
for m1, m2, m3, m4 being marking of P st m1 c= m2 & m3 c= m4 holds
m1 + m3 c= m2 + m4
proof
let P be set ; ::_thesis: for m1, m2, m3, m4 being marking of P st m1 c= m2 & m3 c= m4 holds
m1 + m3 c= m2 + m4
let m1, m2, m3, m4 be marking of P; ::_thesis: ( m1 c= m2 & m3 c= m4 implies m1 + m3 c= m2 + m4 )
assume A1: m1 c= m2 ; ::_thesis: ( not m3 c= m4 or m1 + m3 c= m2 + m4 )
assume A2: m3 c= m4 ; ::_thesis: m1 + m3 c= m2 + m4
let p be set ; :: according to PNPROC_1:def_3 ::_thesis: ( p in P implies p multitude_of <= p multitude_of )
assume A3: p in P ; ::_thesis: p multitude_of <= p multitude_of
then A4: m1 . p <= m2 . p by A1, Def3;
m3 . p <= m4 . p by A2, A3, Def3;
then A5: (m1 . p) + (m3 . p) <= (m2 . p) + (m4 . p) by A4, XREAL_1:7;
(m1 + m3) . p = (m1 . p) + (m3 . p) by A3, Def4;
hence p multitude_of <= p multitude_of by A3, A5, Def4; ::_thesis: verum
end;
theorem :: PNPROC_1:24
for P being set
for m1, m2 being marking of P st m1 c= m2 holds
m2 - m1 c= m2
proof
let P be set ; ::_thesis: for m1, m2 being marking of P st m1 c= m2 holds
m2 - m1 c= m2
let m1, m2 be marking of P; ::_thesis: ( m1 c= m2 implies m2 - m1 c= m2 )
assume A1: m1 c= m2 ; ::_thesis: m2 - m1 c= m2
let p be set ; :: according to PNPROC_1:def_3 ::_thesis: ( p in P implies p multitude_of <= p multitude_of )
assume p in P ; ::_thesis: p multitude_of <= p multitude_of
then A2: (m2 - m1) . p = (m2 . p) - (m1 . p) by A1, Def5;
A3: p multitude_of >= 0 by NAT_1:2;
(m2 . p) - 0 = m2 . p ;
hence p multitude_of <= p multitude_of by A2, A3, XREAL_1:13; ::_thesis: verum
end;
theorem Th25: :: PNPROC_1:25
for P being set
for m1, m2, m3, m4 being marking of P st m1 c= m2 & m3 c= m4 & m4 c= m1 holds
m1 - m4 c= m2 - m3
proof
let P be set ; ::_thesis: for m1, m2, m3, m4 being marking of P st m1 c= m2 & m3 c= m4 & m4 c= m1 holds
m1 - m4 c= m2 - m3
let m1, m2, m3, m4 be marking of P; ::_thesis: ( m1 c= m2 & m3 c= m4 & m4 c= m1 implies m1 - m4 c= m2 - m3 )
assume A1: m1 c= m2 ; ::_thesis: ( not m3 c= m4 or not m4 c= m1 or m1 - m4 c= m2 - m3 )
assume A2: m3 c= m4 ; ::_thesis: ( not m4 c= m1 or m1 - m4 c= m2 - m3 )
assume A3: m4 c= m1 ; ::_thesis: m1 - m4 c= m2 - m3
then m4 c= m2 by A1, Th13;
then A4: m3 c= m2 by A2, Th13;
let p be set ; :: according to PNPROC_1:def_3 ::_thesis: ( p in P implies p multitude_of <= p multitude_of )
assume A5: p in P ; ::_thesis: p multitude_of <= p multitude_of
then A6: m1 . p <= m2 . p by A1, Def3;
A7: m3 . p <= m4 . p by A2, A5, Def3;
A8: (m2 - m3) . p = (m2 . p) - (m3 . p) by A4, A5, Def5;
(m1 - m4) . p = (m1 . p) - (m4 . p) by A3, A5, Def5;
hence p multitude_of <= p multitude_of by A6, A7, A8, XREAL_1:13; ::_thesis: verum
end;
theorem Th26: :: PNPROC_1:26
for P being set
for m1, m2 being marking of P st m1 c= m2 holds
m2 = (m2 - m1) + m1
proof
let P be set ; ::_thesis: for m1, m2 being marking of P st m1 c= m2 holds
m2 = (m2 - m1) + m1
let m1, m2 be marking of P; ::_thesis: ( m1 c= m2 implies m2 = (m2 - m1) + m1 )
assume A1: m1 c= m2 ; ::_thesis: m2 = (m2 - m1) + m1
let p be set ; :: according to PNPROC_1:def_1 ::_thesis: ( p in P implies p multitude_of = p multitude_of )
assume A2: p in P ; ::_thesis: p multitude_of = p multitude_of
then ((m2 - m1) + m1) . p = ((m2 - m1) . p) + (m1 . p) by Def4
.= ((m2 . p) - (m1 . p)) + (m1 . p) by A1, A2, Def5
.= m2 . p ;
hence p multitude_of = p multitude_of ; ::_thesis: verum
end;
theorem Th27: :: PNPROC_1:27
for P being set
for m1, m2 being marking of P holds (m1 + m2) - m1 = m2
proof
let P be set ; ::_thesis: for m1, m2 being marking of P holds (m1 + m2) - m1 = m2
let m1, m2 be marking of P; ::_thesis: (m1 + m2) - m1 = m2
A1: m1 c= m1 + m2 by Th15;
let p be set ; :: according to PNPROC_1:def_1 ::_thesis: ( p in P implies p multitude_of = p multitude_of )
assume A2: p in P ; ::_thesis: p multitude_of = p multitude_of
then ((m1 + m2) - m1) . p = ((m1 + m2) . p) - (m1 . p) by A1, Def5
.= ((m1 . p) + (m2 . p)) - (m1 . p) by A2, Def4
.= m2 . p ;
hence p multitude_of = p multitude_of ; ::_thesis: verum
end;
theorem Th28: :: PNPROC_1:28
for P being set
for m2, m3, m1 being marking of P st m2 + m3 c= m1 holds
(m1 - m2) - m3 = m1 - (m2 + m3)
proof
let P be set ; ::_thesis: for m2, m3, m1 being marking of P st m2 + m3 c= m1 holds
(m1 - m2) - m3 = m1 - (m2 + m3)
let m2, m3, m1 be marking of P; ::_thesis: ( m2 + m3 c= m1 implies (m1 - m2) - m3 = m1 - (m2 + m3) )
assume m2 + m3 c= m1 ; ::_thesis: (m1 - m2) - m3 = m1 - (m2 + m3)
then (m1 - m2) - m3 = (((m1 - (m2 + m3)) + (m2 + m3)) - m2) - m3 by Th26
.= ((((m1 - (m2 + m3)) + m3) + m2) - m2) - m3 by Th22
.= ((m1 - (m2 + m3)) + m3) - m3 by Th27
.= m1 - (m2 + m3) by Th27 ;
hence (m1 - m2) - m3 = m1 - (m2 + m3) ; ::_thesis: verum
end;
theorem :: PNPROC_1:29
for P being set
for m3, m2, m1 being marking of P st m3 c= m2 & m2 c= m1 holds
m1 - (m2 - m3) = (m1 - m2) + m3
proof
let P be set ; ::_thesis: for m3, m2, m1 being marking of P st m3 c= m2 & m2 c= m1 holds
m1 - (m2 - m3) = (m1 - m2) + m3
let m3, m2, m1 be marking of P; ::_thesis: ( m3 c= m2 & m2 c= m1 implies m1 - (m2 - m3) = (m1 - m2) + m3 )
assume A1: m3 c= m2 ; ::_thesis: ( not m2 c= m1 or m1 - (m2 - m3) = (m1 - m2) + m3 )
assume A2: m2 c= m1 ; ::_thesis: m1 - (m2 - m3) = (m1 - m2) + m3
A3: m2 - m3 c= m3 + (m2 - m3) by Th15;
A4: m2 = m3 + (m2 - m3) by A1, Th26;
then (m3 + (m2 - m3)) - (m2 - m3) c= m1 - (m2 - m3) by A2, A3, Th25;
then A5: m3 c= m1 - (m2 - m3) by Th27;
thus (m1 - m2) + m3 = ((m1 - (m2 - m3)) - m3) + m3 by A2, A4, Th28
.= m1 - (m2 - m3) by A5, Th26 ; ::_thesis: verum
end;
begin
definition
let P be set ;
mode transition of P -> set means :Def6: :: PNPROC_1:def 6
ex m1, m2 being marking of P st it = [m1,m2];
existence
ex b1 being set ex m1, m2 being marking of P st b1 = [m1,m2]
proof
set m1 = the marking of P;
take [ the marking of P, the marking of P] ; ::_thesis: ex m1, m2 being marking of P st [ the marking of P, the marking of P] = [m1,m2]
thus ex m1, m2 being marking of P st [ the marking of P, the marking of P] = [m1,m2] ; ::_thesis: verum
end;
end;
:: deftheorem Def6 defines transition PNPROC_1:def_6_:_
for P being set
for b2 being set holds
( b2 is transition of P iff ex m1, m2 being marking of P st b2 = [m1,m2] );
notation
let P be set ;
let t be transition of P;
synonym Pre t for P `1 ;
synonym Post t for P `2 ;
end;
definition
let P be set ;
let t be transition of P;
:: original: Pre
redefine func Pre t -> marking of P;
coherence
Pre is marking of P
proof
ex m1, m2 being marking of P st t = [m1,m2] by Def6;
hence Pre is marking of P by MCART_1:7; ::_thesis: verum
end;
:: original: Post
redefine func Post t -> marking of P;
coherence
Post is marking of P
proof
ex m1, m2 being marking of P st t = [m1,m2] by Def6;
hence Post is marking of P by MCART_1:7; ::_thesis: verum
end;
end;
definition
let P be set ;
let m be marking of P;
let t be transition of P;
func fire (t,m) -> marking of P equals :Def7: :: PNPROC_1:def 7
(m - (Pre t)) + (Post t) if Pre t c= m
otherwise m;
coherence
( ( Pre t c= m implies (m - (Pre t)) + (Post t) is marking of P ) & ( not Pre t c= m implies m is marking of P ) ) ;
consistency
for b1 being marking of P holds verum ;
end;
:: deftheorem Def7 defines fire PNPROC_1:def_7_:_
for P being set
for m being marking of P
for t being transition of P holds
( ( Pre t c= m implies fire (t,m) = (m - (Pre t)) + (Post t) ) & ( not Pre t c= m implies fire (t,m) = m ) );
theorem :: PNPROC_1:30
for P being set
for m being marking of P
for t1, t2 being transition of P st (Pre t1) + (Pre t2) c= m holds
fire (t2,(fire (t1,m))) = (((m - (Pre t1)) - (Pre t2)) + (Post t1)) + (Post t2)
proof
let P be set ; ::_thesis: for m being marking of P
for t1, t2 being transition of P st (Pre t1) + (Pre t2) c= m holds
fire (t2,(fire (t1,m))) = (((m - (Pre t1)) - (Pre t2)) + (Post t1)) + (Post t2)
let m be marking of P; ::_thesis: for t1, t2 being transition of P st (Pre t1) + (Pre t2) c= m holds
fire (t2,(fire (t1,m))) = (((m - (Pre t1)) - (Pre t2)) + (Post t1)) + (Post t2)
let t1, t2 be transition of P; ::_thesis: ( (Pre t1) + (Pre t2) c= m implies fire (t2,(fire (t1,m))) = (((m - (Pre t1)) - (Pre t2)) + (Post t1)) + (Post t2) )
assume A1: (Pre t1) + (Pre t2) c= m ; ::_thesis: fire (t2,(fire (t1,m))) = (((m - (Pre t1)) - (Pre t2)) + (Post t1)) + (Post t2)
A2: Pre t1 c= (Pre t1) + (Pre t2) by Th15;
then A3: Pre t1 c= m by A1, Th13;
then A4: fire (t1,m) = (m - (Pre t1)) + (Post t1) by Def7;
A5: Pre t2 = ((Pre t2) + (Pre t1)) - (Pre t1) by Th18;
A6: ((Pre t1) + (Pre t2)) - (Pre t1) c= m - (Pre t1) by A1, A2, Th19;
m - (Pre t1) c= (m - (Pre t1)) + (Post t1) by Th15;
then Pre t2 c= fire (t1,m) by A4, A5, A6, Th13;
hence fire (t2,(fire (t1,m))) = ((fire (t1,m)) - (Pre t2)) + (Post t2) by Def7
.= (((m - (Pre t1)) + (Post t1)) - (Pre t2)) + (Post t2) by A3, Def7
.= (((m - (Pre t1)) - (Pre t2)) + (Post t1)) + (Post t2) by A1, A2, A5, Th19, Th20 ;
::_thesis: verum
end;
definition
let P be set ;
let t be transition of P;
func fire t -> Function means :Def8: :: PNPROC_1:def 8
( dom it = Funcs (P,NAT) & ( for m being marking of P holds it . m = fire (t,m) ) );
existence
ex b1 being Function st
( dom b1 = Funcs (P,NAT) & ( for m being marking of P holds b1 . m = fire (t,m) ) )
proof
defpred S1[ set , set ] means ex m being marking of P st
( m = $1 & $2 = fire (t,m) );
A1: for x being set st x in Funcs (P,NAT) holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in Funcs (P,NAT) implies ex y being set st S1[x,y] )
assume x in Funcs (P,NAT) ; ::_thesis: ex y being set st S1[x,y]
then reconsider m = x as marking of P by FUNCT_2:66;
take fire (t,m) ; ::_thesis: S1[x, fire (t,m)]
thus S1[x, fire (t,m)] ; ::_thesis: verum
end;
consider f being Function such that
A2: dom f = Funcs (P,NAT) and
A3: for x being set st x in Funcs (P,NAT) holds
S1[x,f . x] from CLASSES1:sch_1(A1);
take f ; ::_thesis: ( dom f = Funcs (P,NAT) & ( for m being marking of P holds f . m = fire (t,m) ) )
thus dom f = Funcs (P,NAT) by A2; ::_thesis: for m being marking of P holds f . m = fire (t,m)
let m be marking of P; ::_thesis: f . m = fire (t,m)
m in Funcs (P,NAT) by FUNCT_2:8;
then S1[m,f . m] by A3;
hence f . m = fire (t,m) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function st dom b1 = Funcs (P,NAT) & ( for m being marking of P holds b1 . m = fire (t,m) ) & dom b2 = Funcs (P,NAT) & ( for m being marking of P holds b2 . m = fire (t,m) ) holds
b1 = b2
proof
let f1, f2 be Function; ::_thesis: ( dom f1 = Funcs (P,NAT) & ( for m being marking of P holds f1 . m = fire (t,m) ) & dom f2 = Funcs (P,NAT) & ( for m being marking of P holds f2 . m = fire (t,m) ) implies f1 = f2 )
assume that
A4: dom f1 = Funcs (P,NAT) and
A5: for m being marking of P holds f1 . m = fire (t,m) and
A6: dom f2 = Funcs (P,NAT) and
A7: for m being marking of P holds f2 . m = fire (t,m) ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in_dom_f1_holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in dom f1 implies f1 . x = f2 . x )
assume x in dom f1 ; ::_thesis: f1 . x = f2 . x
then reconsider m = x as marking of P by A4, FUNCT_2:66;
thus f1 . x = fire (t,m) by A5
.= f2 . x by A7 ; ::_thesis: verum
end;
hence f1 = f2 by A4, A6, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def8 defines fire PNPROC_1:def_8_:_
for P being set
for t being transition of P
for b3 being Function holds
( b3 = fire t iff ( dom b3 = Funcs (P,NAT) & ( for m being marking of P holds b3 . m = fire (t,m) ) ) );
theorem Th31: :: PNPROC_1:31
for P being set
for t being transition of P holds rng (fire t) c= Funcs (P,NAT)
proof
let P be set ; ::_thesis: for t being transition of P holds rng (fire t) c= Funcs (P,NAT)
let t be transition of P; ::_thesis: rng (fire t) c= Funcs (P,NAT)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (fire t) or y in Funcs (P,NAT) )
assume y in rng (fire t) ; ::_thesis: y in Funcs (P,NAT)
then consider x being set such that
A1: x in dom (fire t) and
A2: y = (fire t) . x by FUNCT_1:def_3;
dom (fire t) = Funcs (P,NAT) by Def8;
then reconsider m = x as marking of P by A1, FUNCT_2:66;
y = fire (t,m) by A2, Def8;
hence y in Funcs (P,NAT) by FUNCT_2:8; ::_thesis: verum
end;
theorem :: PNPROC_1:32
for P being set
for m being marking of P
for t2, t1 being transition of P holds fire (t2,(fire (t1,m))) = ((fire t2) * (fire t1)) . m
proof
let P be set ; ::_thesis: for m being marking of P
for t2, t1 being transition of P holds fire (t2,(fire (t1,m))) = ((fire t2) * (fire t1)) . m
let m be marking of P; ::_thesis: for t2, t1 being transition of P holds fire (t2,(fire (t1,m))) = ((fire t2) * (fire t1)) . m
let t2, t1 be transition of P; ::_thesis: fire (t2,(fire (t1,m))) = ((fire t2) * (fire t1)) . m
dom (fire t1) = Funcs (P,NAT) by Def8;
then A1: m in dom (fire t1) by FUNCT_2:8;
thus fire (t2,(fire (t1,m))) = (fire t2) . (fire (t1,m)) by Def8
.= (fire t2) . ((fire t1) . m) by Def8
.= ((fire t2) * (fire t1)) . m by A1, FUNCT_1:13 ; ::_thesis: verum
end;
definition
let P be set ;
mode Petri_net of P -> non empty set means :Def9: :: PNPROC_1:def 9
for x being set st x in it holds
x is transition of P;
existence
ex b1 being non empty set st
for x being set st x in b1 holds
x is transition of P
proof
set t = the transition of P;
take { the transition of P} ; ::_thesis: for x being set st x in { the transition of P} holds
x is transition of P
thus for x being set st x in { the transition of P} holds
x is transition of P by TARSKI:def_1; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines Petri_net PNPROC_1:def_9_:_
for P being set
for b2 being non empty set holds
( b2 is Petri_net of P iff for x being set st x in b2 holds
x is transition of P );
definition
let P be set ;
let N be Petri_net of P;
:: original: Element
redefine mode Element of N -> transition of P;
coherence
for b1 being Element of N holds b1 is transition of P by Def9;
end;
begin
definition
let P be set ;
let N be Petri_net of P;
mode firing-sequence of N is Element of N * ;
end;
definition
let P be set ;
let N be Petri_net of P;
let C be firing-sequence of N;
func fire C -> Function means :Def10: :: PNPROC_1:def 10
ex F being Function-yielding FinSequence st
( it = compose (F,(Funcs (P,NAT))) & len F = len C & ( for i being Element of NAT st i in dom C holds
F . i = fire (C /. i) ) );
existence
ex b1 being Function ex F being Function-yielding FinSequence st
( b1 = compose (F,(Funcs (P,NAT))) & len F = len C & ( for i being Element of NAT st i in dom C holds
F . i = fire (C /. i) ) )
proof
deffunc H1( set ) -> Function = fire (C /. $1);
consider F being FinSequence such that
A1: len F = len C and
A2: for k being Nat st k in dom F holds
F . k = H1(k) from FINSEQ_1:sch_2();
A3: dom F = Seg (len F) by FINSEQ_1:def_3;
A4: dom C = Seg (len C) by FINSEQ_1:def_3;
F is Function-yielding
proof
let x be set ; :: according to FUNCOP_1:def_6 ::_thesis: ( not x in proj1 F or x multitude_of is set )
assume A5: x in dom F ; ::_thesis: x multitude_of is set
then reconsider i = x as Element of NAT ;
F . x = fire (C /. i) by A2, A5;
hence x multitude_of is set ; ::_thesis: verum
end;
then reconsider F = F as Function-yielding FinSequence ;
take f = compose (F,(Funcs (P,NAT))); ::_thesis: ex F being Function-yielding FinSequence st
( f = compose (F,(Funcs (P,NAT))) & len F = len C & ( for i being Element of NAT st i in dom C holds
F . i = fire (C /. i) ) )
take F ; ::_thesis: ( f = compose (F,(Funcs (P,NAT))) & len F = len C & ( for i being Element of NAT st i in dom C holds
F . i = fire (C /. i) ) )
thus f = compose (F,(Funcs (P,NAT))) ; ::_thesis: ( len F = len C & ( for i being Element of NAT st i in dom C holds
F . i = fire (C /. i) ) )
thus ( len F = len C & ( for i being Element of NAT st i in dom C holds
F . i = fire (C /. i) ) ) by A1, A2, A3, A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being Function st ex F being Function-yielding FinSequence st
( b1 = compose (F,(Funcs (P,NAT))) & len F = len C & ( for i being Element of NAT st i in dom C holds
F . i = fire (C /. i) ) ) & ex F being Function-yielding FinSequence st
( b2 = compose (F,(Funcs (P,NAT))) & len F = len C & ( for i being Element of NAT st i in dom C holds
F . i = fire (C /. i) ) ) holds
b1 = b2
proof
let f1, f2 be Function; ::_thesis: ( ex F being Function-yielding FinSequence st
( f1 = compose (F,(Funcs (P,NAT))) & len F = len C & ( for i being Element of NAT st i in dom C holds
F . i = fire (C /. i) ) ) & ex F being Function-yielding FinSequence st
( f2 = compose (F,(Funcs (P,NAT))) & len F = len C & ( for i being Element of NAT st i in dom C holds
F . i = fire (C /. i) ) ) implies f1 = f2 )
given F1 being Function-yielding FinSequence such that A6: f1 = compose (F1,(Funcs (P,NAT))) and
A7: len F1 = len C and
A8: for i being Element of NAT st i in dom C holds
F1 . i = fire (C /. i) ; ::_thesis: ( for F being Function-yielding FinSequence holds
( not f2 = compose (F,(Funcs (P,NAT))) or not len F = len C or ex i being Element of NAT st
( i in dom C & not F . i = fire (C /. i) ) ) or f1 = f2 )
given F2 being Function-yielding FinSequence such that A9: f2 = compose (F2,(Funcs (P,NAT))) and
A10: len F2 = len C and
A11: for i being Element of NAT st i in dom C holds
F2 . i = fire (C /. i) ; ::_thesis: f1 = f2
A12: dom F1 = Seg (len F1) by FINSEQ_1:def_3;
A13: dom F2 = Seg (len F2) by FINSEQ_1:def_3;
A14: dom C = Seg (len C) by FINSEQ_1:def_3;
now__::_thesis:_for_i_being_Nat_st_i_in_dom_C_holds_
F1_._i_=_F2_._i
let i be Nat; ::_thesis: ( i in dom C implies F1 . i = F2 . i )
assume A15: i in dom C ; ::_thesis: F1 . i = F2 . i
then F1 . i = fire (C /. i) by A8;
hence F1 . i = F2 . i by A11, A15; ::_thesis: verum
end;
hence f1 = f2 by A6, A7, A9, A10, A12, A13, A14, FINSEQ_1:13; ::_thesis: verum
end;
end;
:: deftheorem Def10 defines fire PNPROC_1:def_10_:_
for P being set
for N being Petri_net of P
for C being firing-sequence of N
for b4 being Function holds
( b4 = fire C iff ex F being Function-yielding FinSequence st
( b4 = compose (F,(Funcs (P,NAT))) & len F = len C & ( for i being Element of NAT st i in dom C holds
F . i = fire (C /. i) ) ) );
theorem :: PNPROC_1:33
for P being set
for N being Petri_net of P holds fire (<*> N) = id (Funcs (P,NAT))
proof
let P be set ; ::_thesis: for N being Petri_net of P holds fire (<*> N) = id (Funcs (P,NAT))
let N be Petri_net of P; ::_thesis: fire (<*> N) = id (Funcs (P,NAT))
consider F being Function-yielding FinSequence such that
A1: fire (<*> N) = compose (F,(Funcs (P,NAT))) and
A2: len F = len (<*> N) and
for i being Element of NAT st i in dom (<*> N) holds
F . i = fire ((<*> N) /. i) by Def10;
F = {} by A2;
hence fire (<*> N) = id (Funcs (P,NAT)) by A1, FUNCT_7:39; ::_thesis: verum
end;
theorem Th34: :: PNPROC_1:34
for P being set
for N being Petri_net of P
for e being Element of N holds fire <*e*> = fire e
proof
let P be set ; ::_thesis: for N being Petri_net of P
for e being Element of N holds fire <*e*> = fire e
let N be Petri_net of P; ::_thesis: for e being Element of N holds fire <*e*> = fire e
let e be Element of N; ::_thesis: fire <*e*> = fire e
consider F being Function-yielding FinSequence such that
A1: fire <*e*> = compose (F,(Funcs (P,NAT))) and
A2: len F = len <*e*> and
A3: for i being Element of NAT st i in dom <*e*> holds
F . i = fire (<*e*> /. i) by Def10;
A4: len <*e*> = 1 by FINSEQ_1:40;
A5: <*e*> . 1 = e by FINSEQ_1:40;
dom <*e*> = {1} by FINSEQ_1:2, FINSEQ_1:def_8;
then A6: 1 in dom <*e*> by TARSKI:def_1;
then A7: <*e*> /. 1 = <*e*> . 1 by PARTFUN1:def_6;
F . 1 = fire (<*e*> /. 1) by A3, A6;
then A8: F = <*(fire e)*> by A2, A4, A5, A7, FINSEQ_1:40;
dom (fire e) c= Funcs (P,NAT) by Def8;
hence fire <*e*> = fire e by A1, A8, FUNCT_7:46; ::_thesis: verum
end;
theorem Th35: :: PNPROC_1:35
for P being set
for N being Petri_net of P
for e being Element of N holds (fire e) * (id (Funcs (P,NAT))) = fire e
proof
let P be set ; ::_thesis: for N being Petri_net of P
for e being Element of N holds (fire e) * (id (Funcs (P,NAT))) = fire e
let N be Petri_net of P; ::_thesis: for e being Element of N holds (fire e) * (id (Funcs (P,NAT))) = fire e
let e be Element of N; ::_thesis: (fire e) * (id (Funcs (P,NAT))) = fire e
A1: compose (<*(fire e)*>,(Funcs (P,NAT))) = (fire e) * (id (Funcs (P,NAT))) by FUNCT_7:45;
dom (fire e) c= Funcs (P,NAT) by Def8;
hence (fire e) * (id (Funcs (P,NAT))) = fire e by A1, FUNCT_7:46; ::_thesis: verum
end;
theorem :: PNPROC_1:36
for P being set
for N being Petri_net of P
for e1, e2 being Element of N holds fire <*e1,e2*> = (fire e2) * (fire e1)
proof
let P be set ; ::_thesis: for N being Petri_net of P
for e1, e2 being Element of N holds fire <*e1,e2*> = (fire e2) * (fire e1)
let N be Petri_net of P; ::_thesis: for e1, e2 being Element of N holds fire <*e1,e2*> = (fire e2) * (fire e1)
let e1, e2 be Element of N; ::_thesis: fire <*e1,e2*> = (fire e2) * (fire e1)
consider F being Function-yielding FinSequence such that
A1: fire <*e1,e2*> = compose (F,(Funcs (P,NAT))) and
A2: len F = len <*e1,e2*> and
A3: for i being Element of NAT st i in dom <*e1,e2*> holds
F . i = fire (<*e1,e2*> /. i) by Def10;
A4: len <*e1,e2*> = 2 by FINSEQ_1:44;
A5: <*e1,e2*> . 1 = e1 by FINSEQ_1:44;
A6: <*e1,e2*> . 2 = e2 by FINSEQ_1:44;
A7: dom <*e1,e2*> = {1,2} by A4, FINSEQ_1:2, FINSEQ_1:def_3;
A8: 1 in {1,2} by TARSKI:def_2;
A9: 2 in {1,2} by TARSKI:def_2;
A10: <*e1,e2*> /. 1 = <*e1,e2*> . 1 by A7, A8, PARTFUN1:def_6;
A11: <*e1,e2*> /. 2 = <*e1,e2*> . 2 by A7, A9, PARTFUN1:def_6;
A12: F . 1 = fire e1 by A3, A5, A7, A8, A10;
F . 2 = fire e2 by A3, A6, A7, A9, A11;
then A13: F = <*(fire e1),(fire e2)*> by A2, A4, A12, FINSEQ_1:44;
(fire e1) * (id (Funcs (P,NAT))) = fire e1 by Th35;
then ((fire e2) * (fire e1)) * (id (Funcs (P,NAT))) = (fire e2) * (fire e1) by RELAT_1:36;
hence fire <*e1,e2*> = (fire e2) * (fire e1) by A1, A13, FUNCT_7:51; ::_thesis: verum
end;
theorem Th37: :: PNPROC_1:37
for P being set
for N being Petri_net of P
for C being firing-sequence of N holds
( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )
proof
let P be set ; ::_thesis: for N being Petri_net of P
for C being firing-sequence of N holds
( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )
let N be Petri_net of P; ::_thesis: for C being firing-sequence of N holds
( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )
let C be firing-sequence of N; ::_thesis: ( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) )
defpred S1[ Element of NAT ] means for F being Function-yielding FinSequence st len F = $1 & ( for i being Element of NAT st i in dom F holds
ex t being transition of P st F . i = fire t ) holds
( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) );
A1: S1[ 0 ]
proof
let F be Function-yielding FinSequence; ::_thesis: ( len F = 0 & ( for i being Element of NAT st i in dom F holds
ex t being transition of P st F . i = fire t ) implies ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) )
assume len F = 0 ; ::_thesis: ( ex i being Element of NAT st
( i in dom F & ( for t being transition of P holds not F . i = fire t ) ) or ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) )
then F = {} ;
then compose (F,(Funcs (P,NAT))) = id (Funcs (P,NAT)) by FUNCT_7:39;
hence ( ex i being Element of NAT st
( i in dom F & ( for t being transition of P holds not F . i = fire t ) ) or ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) ) by RELAT_1:45; ::_thesis: verum
end;
A2: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: for G being Function-yielding FinSequence st len G = k & ( for i being Element of NAT st i in dom G holds
ex t being transition of P st G . i = fire t ) holds
( dom (compose (G,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (G,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) ; ::_thesis: S1[k + 1]
let F be Function-yielding FinSequence; ::_thesis: ( len F = k + 1 & ( for i being Element of NAT st i in dom F holds
ex t being transition of P st F . i = fire t ) implies ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) )
assume that
A4: len F = k + 1 and
A5: for i being Element of NAT st i in dom F holds
ex t being transition of P st F . i = fire t ; ::_thesis: ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) )
consider G being FinSequence, x being set such that
A6: F = G ^ <*x*> and
A7: len G = k by A4, TREES_2:3;
reconsider G = G as Function-yielding FinSequence by A6, FUNCT_7:23;
0 <= k by NAT_1:2;
then 0 + 1 <= k + 1 by XREAL_1:7;
then k + 1 in dom F by A4, FINSEQ_3:25;
then consider t being transition of P such that
A8: F . (k + 1) = fire t by A5;
x = F . (k + 1) by A6, A7, FINSEQ_1:42;
then A9: compose (F,(Funcs (P,NAT))) = (fire t) * (compose (G,(Funcs (P,NAT)))) by A6, A8, FUNCT_7:41;
A10: dom (fire t) = Funcs (P,NAT) by Def8;
A11: rng (fire t) c= Funcs (P,NAT) by Th31;
A12: for i being Element of NAT st i in dom G holds
ex t being transition of P st G . i = fire t
proof
let i be Element of NAT ; ::_thesis: ( i in dom G implies ex t being transition of P st G . i = fire t )
A13: dom G c= dom F by A6, FINSEQ_1:26;
assume A14: i in dom G ; ::_thesis: ex t being transition of P st G . i = fire t
then G . i = F . i by A6, FINSEQ_1:def_7;
hence ex t being transition of P st G . i = fire t by A5, A13, A14; ::_thesis: verum
end;
then A15: dom (compose (G,(Funcs (P,NAT)))) = Funcs (P,NAT) by A3, A7;
A16: rng (compose (G,(Funcs (P,NAT)))) c= Funcs (P,NAT) by A3, A7, A12;
rng (compose (F,(Funcs (P,NAT)))) c= rng (fire t) by A9, RELAT_1:26;
hence ( dom (compose (F,(Funcs (P,NAT)))) = Funcs (P,NAT) & rng (compose (F,(Funcs (P,NAT)))) c= Funcs (P,NAT) ) by A9, A10, A11, A15, A16, RELAT_1:27, XBOOLE_1:1; ::_thesis: verum
end;
A17: for k being Element of NAT holds S1[k] from NAT_1:sch_1(A1, A2);
consider F being Function-yielding FinSequence such that
A18: fire C = compose (F,(Funcs (P,NAT))) and
A19: len F = len C and
A20: for i being Element of NAT st i in dom C holds
F . i = fire (C /. i) by Def10;
for i being Element of NAT st i in dom F holds
ex t being transition of P st F . i = fire t
proof
let i be Element of NAT ; ::_thesis: ( i in dom F implies ex t being transition of P st F . i = fire t )
assume A21: i in dom F ; ::_thesis: ex t being transition of P st F . i = fire t
A22: dom F = Seg (len F) by FINSEQ_1:def_3;
A23: dom C = Seg (len C) by FINSEQ_1:def_3;
reconsider t = C /. i as Element of N ;
take t ; ::_thesis: F . i = fire t
thus F . i = fire t by A19, A20, A21, A22, A23; ::_thesis: verum
end;
hence ( dom (fire C) = Funcs (P,NAT) & rng (fire C) c= Funcs (P,NAT) ) by A17, A18, A19; ::_thesis: verum
end;
theorem Th38: :: PNPROC_1:38
for P being set
for N being Petri_net of P
for C1, C2 being firing-sequence of N holds fire (C1 ^ C2) = (fire C2) * (fire C1)
proof
let P be set ; ::_thesis: for N being Petri_net of P
for C1, C2 being firing-sequence of N holds fire (C1 ^ C2) = (fire C2) * (fire C1)
let N be Petri_net of P; ::_thesis: for C1, C2 being firing-sequence of N holds fire (C1 ^ C2) = (fire C2) * (fire C1)
let C1, C2 be firing-sequence of N; ::_thesis: fire (C1 ^ C2) = (fire C2) * (fire C1)
consider F being Function-yielding FinSequence such that
A1: fire (C1 ^ C2) = compose (F,(Funcs (P,NAT))) and
A2: len F = len (C1 ^ C2) and
A3: for i being Element of NAT st i in dom (C1 ^ C2) holds
F . i = fire ((C1 ^ C2) /. i) by Def10;
consider F1 being Function-yielding FinSequence such that
A4: fire C1 = compose (F1,(Funcs (P,NAT))) and
A5: len F1 = len C1 and
A6: for i being Element of NAT st i in dom C1 holds
F1 . i = fire (C1 /. i) by Def10;
consider F2 being Function-yielding FinSequence such that
A7: fire C2 = compose (F2,(Funcs (P,NAT))) and
A8: len F2 = len C2 and
A9: for i being Element of NAT st i in dom C2 holds
F2 . i = fire (C2 /. i) by Def10;
A10: rng (fire C1) c= Funcs (P,NAT) by Th37;
len F = (len C1) + (len C2) by A2, FINSEQ_1:22;
then A11: dom F = Seg ((len F1) + (len F2)) by A5, A8, FINSEQ_1:def_3;
A12: for k being Nat st k in dom F1 holds
F . k = F1 . k
proof
let k be Nat; ::_thesis: ( k in dom F1 implies F . k = F1 . k )
assume A13: k in dom F1 ; ::_thesis: F . k = F1 . k
A14: dom F1 = Seg (len F1) by FINSEQ_1:def_3;
A15: dom F1 = Seg (len C1) by A5, FINSEQ_1:def_3;
A16: dom F1 = dom C1 by A5, A14, FINSEQ_1:def_3;
A17: k in dom C1 by A13, A15, FINSEQ_1:def_3;
A18: dom C1 c= dom (C1 ^ C2) by FINSEQ_1:26;
then A19: F . k = fire ((C1 ^ C2) /. k) by A3, A17;
A20: (C1 ^ C2) /. k = (C1 ^ C2) . k by A17, A18, PARTFUN1:def_6;
A21: (C1 ^ C2) . k = C1 . k by A13, A16, FINSEQ_1:def_7;
C1 . k = C1 /. k by A13, A16, PARTFUN1:def_6;
hence F . k = F1 . k by A6, A13, A16, A19, A20, A21; ::_thesis: verum
end;
for k being Nat st k in dom F2 holds
F . ((len F1) + k) = F2 . k
proof
let k be Nat; ::_thesis: ( k in dom F2 implies F . ((len F1) + k) = F2 . k )
assume A22: k in dom F2 ; ::_thesis: F . ((len F1) + k) = F2 . k
dom F2 = Seg (len F2) by FINSEQ_1:def_3;
then A23: dom F2 = dom C2 by A8, FINSEQ_1:def_3;
then A24: (len F1) + k in dom (C1 ^ C2) by A5, A22, FINSEQ_1:28;
A25: F . ((len F1) + k) = fire ((C1 ^ C2) /. ((len F1) + k)) by A3, A5, A22, A23, FINSEQ_1:28;
A26: (C1 ^ C2) /. ((len F1) + k) = (C1 ^ C2) . ((len F1) + k) by A24, PARTFUN1:def_6;
A27: (C1 ^ C2) . ((len F1) + k) = C2 . k by A5, A22, A23, FINSEQ_1:def_7;
C2 . k = C2 /. k by A22, A23, PARTFUN1:def_6;
hence F . ((len F1) + k) = F2 . k by A9, A22, A23, A25, A26, A27; ::_thesis: verum
end;
then F = F1 ^ F2 by A11, A12, FINSEQ_1:def_7;
hence fire (C1 ^ C2) = (fire C2) * (fire C1) by A1, A4, A7, A10, FUNCT_7:48; ::_thesis: verum
end;
theorem :: PNPROC_1:39
for P being set
for N being Petri_net of P
for e being Element of N
for C being firing-sequence of N holds fire (C ^ <*e*>) = (fire e) * (fire C)
proof
let P be set ; ::_thesis: for N being Petri_net of P
for e being Element of N
for C being firing-sequence of N holds fire (C ^ <*e*>) = (fire e) * (fire C)
let N be Petri_net of P; ::_thesis: for e being Element of N
for C being firing-sequence of N holds fire (C ^ <*e*>) = (fire e) * (fire C)
let e be Element of N; ::_thesis: for C being firing-sequence of N holds fire (C ^ <*e*>) = (fire e) * (fire C)
let C be firing-sequence of N; ::_thesis: fire (C ^ <*e*>) = (fire e) * (fire C)
fire (C ^ <*e*>) = (fire <*e*>) * (fire C) by Th38;
hence fire (C ^ <*e*>) = (fire e) * (fire C) by Th34; ::_thesis: verum
end;
definition
let P be set ;
let N be Petri_net of P;
let C be firing-sequence of N;
let m be marking of P;
func fire (C,m) -> marking of P equals :: PNPROC_1:def 11
(fire C) . m;
coherence
(fire C) . m is marking of P
proof
A1: dom (fire C) = Funcs (P,NAT) by Th37;
A2: rng (fire C) c= Funcs (P,NAT) by Th37;
m in dom (fire C) by A1, FUNCT_2:8;
then [m,((fire C) . m)] in fire C by FUNCT_1:def_2;
then (fire C) . m in rng (fire C) by XTUPLE_0:def_13;
hence (fire C) . m is marking of P by A2, FUNCT_2:66; ::_thesis: verum
end;
end;
:: deftheorem defines fire PNPROC_1:def_11_:_
for P being set
for N being Petri_net of P
for C being firing-sequence of N
for m being marking of P holds fire (C,m) = (fire C) . m;
begin
definition
let P be set ;
let N be Petri_net of P;
mode process of N is Subset of (N *);
end;
definition
let P be set ;
let N be Petri_net of P;
let R1, R2 be process of N;
funcR1 before R2 -> process of N equals :: PNPROC_1:def 12
{ (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } ;
coherence
{ (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } is process of N
proof
set X = { (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } ;
{ (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } c= N *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } or x in N * )
assume x in { (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } ; ::_thesis: x in N *
then ex C1, C2 being firing-sequence of N st
( x = C1 ^ C2 & C1 in R1 & C2 in R2 ) ;
hence x in N * ; ::_thesis: verum
end;
hence { (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } is process of N ; ::_thesis: verum
end;
end;
:: deftheorem defines before PNPROC_1:def_12_:_
for P being set
for N being Petri_net of P
for R1, R2 being process of N holds R1 before R2 = { (C1 ^ C2) where C1, C2 is firing-sequence of N : ( C1 in R1 & C2 in R2 ) } ;
registration
let P be set ;
let N be Petri_net of P;
let R1, R2 be non empty process of N;
clusterR1 before R2 -> non empty ;
coherence
not R1 before R2 is empty
proof
consider fs1 being set such that
A1: fs1 in R1 by XBOOLE_0:def_1;
consider fs2 being set such that
A2: fs2 in R2 by XBOOLE_0:def_1;
reconsider fs1 = fs1, fs2 = fs2 as firing-sequence of N by A1, A2;
fs1 ^ fs2 in R1 before R2 by A1, A2;
hence not R1 before R2 is empty ; ::_thesis: verum
end;
end;
theorem Th40: :: PNPROC_1:40
for P being set
for N being Petri_net of P
for R1, R2, R being process of N holds (R1 \/ R2) before R = (R1 before R) \/ (R2 before R)
proof
let P be set ; ::_thesis: for N being Petri_net of P
for R1, R2, R being process of N holds (R1 \/ R2) before R = (R1 before R) \/ (R2 before R)
let N be Petri_net of P; ::_thesis: for R1, R2, R being process of N holds (R1 \/ R2) before R = (R1 before R) \/ (R2 before R)
let R1, R2, R be process of N; ::_thesis: (R1 \/ R2) before R = (R1 before R) \/ (R2 before R)
thus (R1 \/ R2) before R c= (R1 before R) \/ (R2 before R) :: according to XBOOLE_0:def_10 ::_thesis: (R1 before R) \/ (R2 before R) c= (R1 \/ R2) before R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (R1 \/ R2) before R or x in (R1 before R) \/ (R2 before R) )
assume x in (R1 \/ R2) before R ; ::_thesis: x in (R1 before R) \/ (R2 before R)
then consider fs1, fs being firing-sequence of N such that
A1: x = fs1 ^ fs and
A2: fs1 in R1 \/ R2 and
A3: fs in R ;
( fs1 in R1 or fs1 in R2 ) by A2, XBOOLE_0:def_3;
then ( x in { (a1 ^ a) where a1, a is firing-sequence of N : ( a1 in R1 & a in R ) } or x in { (b2 ^ b) where b2, b is firing-sequence of N : ( b2 in R2 & b in R ) } ) by A1, A3;
hence x in (R1 before R) \/ (R2 before R) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (R1 before R) \/ (R2 before R) or x in (R1 \/ R2) before R )
assume A4: x in (R1 before R) \/ (R2 before R) ; ::_thesis: x in (R1 \/ R2) before R
percases ( x in R1 before R or x in R2 before R ) by A4, XBOOLE_0:def_3;
suppose x in R1 before R ; ::_thesis: x in (R1 \/ R2) before R
then consider fs1, fs being firing-sequence of N such that
A5: x = fs1 ^ fs and
A6: fs1 in R1 and
A7: fs in R ;
fs1 in R1 \/ R2 by A6, XBOOLE_0:def_3;
hence x in (R1 \/ R2) before R by A5, A7; ::_thesis: verum
end;
suppose x in R2 before R ; ::_thesis: x in (R1 \/ R2) before R
then consider fs2, fs being firing-sequence of N such that
A8: x = fs2 ^ fs and
A9: fs2 in R2 and
A10: fs in R ;
fs2 in R1 \/ R2 by A9, XBOOLE_0:def_3;
hence x in (R1 \/ R2) before R by A8, A10; ::_thesis: verum
end;
end;
end;
theorem Th41: :: PNPROC_1:41
for P being set
for N being Petri_net of P
for R, R1, R2 being process of N holds R before (R1 \/ R2) = (R before R1) \/ (R before R2)
proof
let P be set ; ::_thesis: for N being Petri_net of P
for R, R1, R2 being process of N holds R before (R1 \/ R2) = (R before R1) \/ (R before R2)
let N be Petri_net of P; ::_thesis: for R, R1, R2 being process of N holds R before (R1 \/ R2) = (R before R1) \/ (R before R2)
let R, R1, R2 be process of N; ::_thesis: R before (R1 \/ R2) = (R before R1) \/ (R before R2)
thus R before (R1 \/ R2) c= (R before R1) \/ (R before R2) :: according to XBOOLE_0:def_10 ::_thesis: (R before R1) \/ (R before R2) c= R before (R1 \/ R2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R before (R1 \/ R2) or x in (R before R1) \/ (R before R2) )
assume x in R before (R1 \/ R2) ; ::_thesis: x in (R before R1) \/ (R before R2)
then consider fs, fs1 being firing-sequence of N such that
A1: x = fs ^ fs1 and
A2: fs in R and
A3: fs1 in R1 \/ R2 ;
( fs1 in R1 or fs1 in R2 ) by A3, XBOOLE_0:def_3;
then ( x in { (a ^ a1) where a, a1 is firing-sequence of N : ( a in R & a1 in R1 ) } or x in { (b ^ b2) where b, b2 is firing-sequence of N : ( b in R & b2 in R2 ) } ) by A1, A2;
hence x in (R before R1) \/ (R before R2) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (R before R1) \/ (R before R2) or x in R before (R1 \/ R2) )
assume A4: x in (R before R1) \/ (R before R2) ; ::_thesis: x in R before (R1 \/ R2)
percases ( x in R before R1 or x in R before R2 ) by A4, XBOOLE_0:def_3;
suppose x in R before R1 ; ::_thesis: x in R before (R1 \/ R2)
then consider fs, fs1 being firing-sequence of N such that
A5: x = fs ^ fs1 and
A6: fs in R and
A7: fs1 in R1 ;
fs1 in R1 \/ R2 by A7, XBOOLE_0:def_3;
hence x in R before (R1 \/ R2) by A5, A6; ::_thesis: verum
end;
suppose x in R before R2 ; ::_thesis: x in R before (R1 \/ R2)
then consider fs, fs2 being firing-sequence of N such that
A8: x = fs ^ fs2 and
A9: fs in R and
A10: fs2 in R2 ;
fs2 in R1 \/ R2 by A10, XBOOLE_0:def_3;
hence x in R before (R1 \/ R2) by A8, A9; ::_thesis: verum
end;
end;
end;
theorem Th42: :: PNPROC_1:42
for P being set
for N being Petri_net of P
for C1, C2 being firing-sequence of N holds {C1} before {C2} = {(C1 ^ C2)}
proof
let P be set ; ::_thesis: for N being Petri_net of P
for C1, C2 being firing-sequence of N holds {C1} before {C2} = {(C1 ^ C2)}
let N be Petri_net of P; ::_thesis: for C1, C2 being firing-sequence of N holds {C1} before {C2} = {(C1 ^ C2)}
let C1, C2 be firing-sequence of N; ::_thesis: {C1} before {C2} = {(C1 ^ C2)}
thus {C1} before {C2} c= {(C1 ^ C2)} :: according to XBOOLE_0:def_10 ::_thesis: {(C1 ^ C2)} c= {C1} before {C2}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {C1} before {C2} or x in {(C1 ^ C2)} )
assume x in {C1} before {C2} ; ::_thesis: x in {(C1 ^ C2)}
then consider fs1, fs2 being firing-sequence of N such that
A1: x = fs1 ^ fs2 and
A2: fs1 in {C1} and
A3: fs2 in {C2} ;
A4: fs1 = C1 by A2, TARSKI:def_1;
fs2 = C2 by A3, TARSKI:def_1;
hence x in {(C1 ^ C2)} by A1, A4, TARSKI:def_1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {(C1 ^ C2)} or x in {C1} before {C2} )
assume x in {(C1 ^ C2)} ; ::_thesis: x in {C1} before {C2}
then A5: x = C1 ^ C2 by TARSKI:def_1;
A6: C1 in {C1} by TARSKI:def_1;
C2 in {C2} by TARSKI:def_1;
hence x in {C1} before {C2} by A5, A6; ::_thesis: verum
end;
theorem :: PNPROC_1:43
for P being set
for N being Petri_net of P
for C1, C2, C being firing-sequence of N holds {C1,C2} before {C} = {(C1 ^ C),(C2 ^ C)}
proof
let P be set ; ::_thesis: for N being Petri_net of P
for C1, C2, C being firing-sequence of N holds {C1,C2} before {C} = {(C1 ^ C),(C2 ^ C)}
let N be Petri_net of P; ::_thesis: for C1, C2, C being firing-sequence of N holds {C1,C2} before {C} = {(C1 ^ C),(C2 ^ C)}
let C1, C2, C be firing-sequence of N; ::_thesis: {C1,C2} before {C} = {(C1 ^ C),(C2 ^ C)}
thus {C1,C2} before {C} = ({C1} \/ {C2}) before {C} by ENUMSET1:1
.= ({C1} before {C}) \/ ({C2} before {C}) by Th40
.= {(C1 ^ C)} \/ ({C2} before {C}) by Th42
.= {(C1 ^ C)} \/ {(C2 ^ C)} by Th42
.= {(C1 ^ C),(C2 ^ C)} by ENUMSET1:1 ; ::_thesis: verum
end;
theorem :: PNPROC_1:44
for P being set
for N being Petri_net of P
for C, C1, C2 being firing-sequence of N holds {C} before {C1,C2} = {(C ^ C1),(C ^ C2)}
proof
let P be set ; ::_thesis: for N being Petri_net of P
for C, C1, C2 being firing-sequence of N holds {C} before {C1,C2} = {(C ^ C1),(C ^ C2)}
let N be Petri_net of P; ::_thesis: for C, C1, C2 being firing-sequence of N holds {C} before {C1,C2} = {(C ^ C1),(C ^ C2)}
let C, C1, C2 be firing-sequence of N; ::_thesis: {C} before {C1,C2} = {(C ^ C1),(C ^ C2)}
thus {C} before {C1,C2} = {C} before ({C1} \/ {C2}) by ENUMSET1:1
.= ({C} before {C1}) \/ ({C} before {C2}) by Th41
.= {(C ^ C1)} \/ ({C} before {C2}) by Th42
.= {(C ^ C1)} \/ {(C ^ C2)} by Th42
.= {(C ^ C1),(C ^ C2)} by ENUMSET1:1 ; ::_thesis: verum
end;
begin
definition
let P be set ;
let N be Petri_net of P;
let R1, R2 be process of N;
funcR1 concur R2 -> process of N equals :: PNPROC_1:def 13
{ C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } ;
coherence
{ C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } is process of N
proof
set X = { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } ;
{ C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } c= N *
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } or x in N * )
assume x in { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } ; ::_thesis: x in N *
then ex C being firing-sequence of N st
( x = C & ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) ) ;
hence x in N * ; ::_thesis: verum
end;
hence { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } is process of N ; ::_thesis: verum
end;
commutativity
for b1, R1, R2 being process of N st b1 = { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } holds
b1 = { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) }
proof
let R, R1, R2 be process of N; ::_thesis: ( R = { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } implies R = { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) } )
assume A1: R = { C1 where C1 is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C1 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } ; ::_thesis: R = { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) }
thus R c= { C2 where C2 is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C2 = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) } :: according to XBOOLE_0:def_10 ::_thesis: { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) } c= R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R or x in { C2 where C2 is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C2 = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) } )
assume x in R ; ::_thesis: x in { C2 where C2 is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C2 = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) }
then A2: ex C1 being firing-sequence of N st
( x = C1 & ex q1, q2 being FinSubsequence st
( C1 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) ) by A1;
thus x in { C2 where C2 is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C2 = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) } by A2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) } or x in R )
assume x in { C2 where C2 is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C2 = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) } ; ::_thesis: x in R
then ex C2 being firing-sequence of N st
( x = C2 & ex q1, q2 being FinSubsequence st
( C2 = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R1 ) ) ;
hence x in R by A1; ::_thesis: verum
end;
end;
:: deftheorem defines concur PNPROC_1:def_13_:_
for P being set
for N being Petri_net of P
for R1, R2 being process of N holds R1 concur R2 = { C where C is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) } ;
theorem Th45: :: PNPROC_1:45
for P being set
for N being Petri_net of P
for R1, R2, R being process of N holds (R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R)
proof
let P be set ; ::_thesis: for N being Petri_net of P
for R1, R2, R being process of N holds (R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R)
let N be Petri_net of P; ::_thesis: for R1, R2, R being process of N holds (R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R)
let R1, R2, R be process of N; ::_thesis: (R1 \/ R2) concur R = (R1 concur R) \/ (R2 concur R)
thus (R1 \/ R2) concur R c= (R1 concur R) \/ (R2 concur R) :: according to XBOOLE_0:def_10 ::_thesis: (R1 concur R) \/ (R2 concur R) c= (R1 \/ R2) concur R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (R1 \/ R2) concur R or x in (R1 concur R) \/ (R2 concur R) )
assume x in (R1 \/ R2) concur R ; ::_thesis: x in (R1 concur R) \/ (R2 concur R)
then consider C being firing-sequence of N such that
A1: x = C and
A2: ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 \/ R2 & Seq q2 in R ) ;
consider q1, q2 being FinSubsequence such that
A3: C = q1 \/ q2 and
A4: q1 misses q2 and
A5: Seq q1 in R1 \/ R2 and
A6: Seq q2 in R by A2;
( Seq q1 in R1 or Seq q1 in R2 ) by A5, XBOOLE_0:def_3;
then ( x in { C1 where C1 is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C1 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R ) } or x in { C2 where C2 is firing-sequence of N : ex q1, q2 being FinSubsequence st
( C2 = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R ) } ) by A1, A3, A4, A6;
hence x in (R1 concur R) \/ (R2 concur R) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (R1 concur R) \/ (R2 concur R) or x in (R1 \/ R2) concur R )
assume A7: x in (R1 concur R) \/ (R2 concur R) ; ::_thesis: x in (R1 \/ R2) concur R
percases ( x in R1 concur R or x in R2 concur R ) by A7, XBOOLE_0:def_3;
suppose x in R1 concur R ; ::_thesis: x in (R1 \/ R2) concur R
then consider C being firing-sequence of N such that
A8: x = C and
A9: ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R ) ;
consider q1, q2 being FinSubsequence such that
A10: C = q1 \/ q2 and
A11: q1 misses q2 and
A12: Seq q1 in R1 and
A13: Seq q2 in R by A9;
Seq q1 in R1 \/ R2 by A12, XBOOLE_0:def_3;
hence x in (R1 \/ R2) concur R by A8, A10, A11, A13; ::_thesis: verum
end;
suppose x in R2 concur R ; ::_thesis: x in (R1 \/ R2) concur R
then consider C being firing-sequence of N such that
A14: x = C and
A15: ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R2 & Seq q2 in R ) ;
consider q1, q2 being FinSubsequence such that
A16: C = q1 \/ q2 and
A17: q1 misses q2 and
A18: Seq q1 in R2 and
A19: Seq q2 in R by A15;
Seq q1 in R1 \/ R2 by A18, XBOOLE_0:def_3;
hence x in (R1 \/ R2) concur R by A14, A16, A17, A19; ::_thesis: verum
end;
end;
end;
theorem Th46: :: PNPROC_1:46
for P being set
for N being Petri_net of P
for e1, e2 being Element of N holds {<*e1*>} concur {<*e2*>} = {<*e1,e2*>,<*e2,e1*>}
proof
let P be set ; ::_thesis: for N being Petri_net of P
for e1, e2 being Element of N holds {<*e1*>} concur {<*e2*>} = {<*e1,e2*>,<*e2,e1*>}
let N be Petri_net of P; ::_thesis: for e1, e2 being Element of N holds {<*e1*>} concur {<*e2*>} = {<*e1,e2*>,<*e2,e1*>}
let e1, e2 be Element of N; ::_thesis: {<*e1*>} concur {<*e2*>} = {<*e1,e2*>,<*e2,e1*>}
set C1 = <*e1*>;
set C2 = <*e2*>;
set R1 = {<*e1*>};
set R2 = {<*e2*>};
thus {<*e1*>} concur {<*e2*>} c= {<*e1,e2*>,<*e2,e1*>} :: according to XBOOLE_0:def_10 ::_thesis: {<*e1,e2*>,<*e2,e1*>} c= {<*e1*>} concur {<*e2*>}
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {<*e1*>} concur {<*e2*>} or x in {<*e1,e2*>,<*e2,e1*>} )
assume x in {<*e1*>} concur {<*e2*>} ; ::_thesis: x in {<*e1,e2*>,<*e2,e1*>}
then consider C being firing-sequence of N such that
A1: x = C and
A2: ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in {<*e1*>} & Seq q2 in {<*e2*>} ) ;
consider q1, q2 being FinSubsequence such that
A3: C = q1 \/ q2 and
A4: q1 misses q2 and
A5: Seq q1 in {<*e1*>} and
A6: Seq q2 in {<*e2*>} by A2;
A7: Seq q1 = <*e1*> by A5, TARSKI:def_1;
A8: Seq q2 = <*e2*> by A6, TARSKI:def_1;
consider i being Element of NAT such that
A9: q1 = {[i,e1]} by A7, Th4;
consider j being Element of NAT such that
A10: q2 = {[j,e2]} by A8, Th4;
A11: [i,e1] in q1 by A9, TARSKI:def_1;
A12: [j,e2] in q2 by A10, TARSKI:def_1;
A13: C = {[i,e1],[j,e2]} by A3, A9, A10, ENUMSET1:1;
then ( ( i = 1 & j = 1 & e1 = e2 ) or ( i = 1 & j = 2 ) or ( i = 2 & j = 1 ) ) by Th5;
then ( C = <*e1,e2*> or C = <*e2,e1*> ) by A4, A11, A12, A13, Th6, XBOOLE_0:3;
hence x in {<*e1,e2*>,<*e2,e1*>} by A1, TARSKI:def_2; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {<*e1,e2*>,<*e2,e1*>} or x in {<*e1*>} concur {<*e2*>} )
assume A14: x in {<*e1,e2*>,<*e2,e1*>} ; ::_thesis: x in {<*e1*>} concur {<*e2*>}
percases ( x = <*e1,e2*> or x = <*e2,e1*> ) by A14, TARSKI:def_2;
supposeA15: x = <*e1,e2*> ; ::_thesis: x in {<*e1*>} concur {<*e2*>}
then A16: x = {[1,e1],[2,e2]} by Th6
.= {[1,e1]} \/ {[2,e2]} by ENUMSET1:1 ;
reconsider q1 = {[1,e1]}, q2 = {[2,e2]} as FinSubsequence by Th1;
[1,e1] <> [2,e2] by XTUPLE_0:1;
then not [1,e1] in q2 by TARSKI:def_1;
then A17: q1 misses q2 by ZFMISC_1:50;
A18: Seq q1 = <*e1*> by Th3;
A19: Seq q2 = <*e2*> by Th3;
A20: <*e1*> in {<*e1*>} by TARSKI:def_1;
<*e2*> in {<*e2*>} by TARSKI:def_1;
hence x in {<*e1*>} concur {<*e2*>} by A15, A16, A17, A18, A19, A20; ::_thesis: verum
end;
supposeA21: x = <*e2,e1*> ; ::_thesis: x in {<*e1*>} concur {<*e2*>}
then A22: x = {[1,e2],[2,e1]} by Th6
.= {[1,e2]} \/ {[2,e1]} by ENUMSET1:1 ;
reconsider q1 = {[2,e1]}, q2 = {[1,e2]} as FinSubsequence by Th1;
[1,e2] <> [2,e1] by XTUPLE_0:1;
then not [2,e1] in q2 by TARSKI:def_1;
then A23: q1 misses q2 by ZFMISC_1:50;
A24: Seq q1 = <*e1*> by Th3;
A25: Seq q2 = <*e2*> by Th3;
A26: <*e1*> in {<*e1*>} by TARSKI:def_1;
<*e2*> in {<*e2*>} by TARSKI:def_1;
hence x in {<*e1*>} concur {<*e2*>} by A21, A22, A23, A24, A25, A26; ::_thesis: verum
end;
end;
end;
theorem :: PNPROC_1:47
for P being set
for N being Petri_net of P
for e1, e2, e being Element of N holds {<*e1*>,<*e2*>} concur {<*e*>} = {<*e1,e*>,<*e2,e*>,<*e,e1*>,<*e,e2*>}
proof
let P be set ; ::_thesis: for N being Petri_net of P
for e1, e2, e being Element of N holds {<*e1*>,<*e2*>} concur {<*e*>} = {<*e1,e*>,<*e2,e*>,<*e,e1*>,<*e,e2*>}
let N be Petri_net of P; ::_thesis: for e1, e2, e being Element of N holds {<*e1*>,<*e2*>} concur {<*e*>} = {<*e1,e*>,<*e2,e*>,<*e,e1*>,<*e,e2*>}
let e1, e2, e be Element of N; ::_thesis: {<*e1*>,<*e2*>} concur {<*e*>} = {<*e1,e*>,<*e2,e*>,<*e,e1*>,<*e,e2*>}
{<*e1*>,<*e2*>} = {<*e1*>} \/ {<*e2*>} by ENUMSET1:1;
then A1: {<*e1*>,<*e2*>} concur {<*e*>} = ({<*e1*>} concur {<*e*>}) \/ ({<*e2*>} concur {<*e*>}) by Th45;
A2: {<*e1*>} concur {<*e*>} = {<*e1,e*>,<*e,e1*>} by Th46;
{<*e2*>} concur {<*e*>} = {<*e2,e*>,<*e,e2*>} by Th46;
hence {<*e1*>,<*e2*>} concur {<*e*>} = {<*e1,e*>,<*e,e1*>,<*e2,e*>,<*e,e2*>} by A1, A2, ENUMSET1:5
.= {<*e1,e*>,<*e2,e*>,<*e,e1*>,<*e,e2*>} by ENUMSET1:62 ;
::_thesis: verum
end;
theorem :: PNPROC_1:48
for P being set
for N being Petri_net of P
for R1, R2, R3 being process of N holds (R1 before R2) before R3 = R1 before (R2 before R3)
proof
let P be set ; ::_thesis: for N being Petri_net of P
for R1, R2, R3 being process of N holds (R1 before R2) before R3 = R1 before (R2 before R3)
let N be Petri_net of P; ::_thesis: for R1, R2, R3 being process of N holds (R1 before R2) before R3 = R1 before (R2 before R3)
let R1, R2, R3 be process of N; ::_thesis: (R1 before R2) before R3 = R1 before (R2 before R3)
thus (R1 before R2) before R3 c= R1 before (R2 before R3) :: according to XBOOLE_0:def_10 ::_thesis: R1 before (R2 before R3) c= (R1 before R2) before R3
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (R1 before R2) before R3 or x in R1 before (R2 before R3) )
assume x in (R1 before R2) before R3 ; ::_thesis: x in R1 before (R2 before R3)
then consider C1, C2 being firing-sequence of N such that
A1: x = C1 ^ C2 and
A2: C1 in R1 before R2 and
A3: C2 in R3 ;
consider fs1, fs2 being firing-sequence of N such that
A4: C1 = fs1 ^ fs2 and
A5: fs1 in R1 and
A6: fs2 in R2 by A2;
A7: x = fs1 ^ (fs2 ^ C2) by A1, A4, FINSEQ_1:32;
consider C3 being firing-sequence of N such that
A8: C3 = fs2 ^ C2 and
A9: fs2 in R2 and
A10: C2 in R3 by A3, A6;
C3 in R2 before R3 by A8, A9, A10;
hence x in R1 before (R2 before R3) by A5, A7, A8; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R1 before (R2 before R3) or x in (R1 before R2) before R3 )
assume x in R1 before (R2 before R3) ; ::_thesis: x in (R1 before R2) before R3
then consider C1, C2 being firing-sequence of N such that
A11: x = C1 ^ C2 and
A12: C1 in R1 and
A13: C2 in R2 before R3 ;
consider fs1, fs2 being firing-sequence of N such that
A14: C2 = fs1 ^ fs2 and
A15: fs1 in R2 and
A16: fs2 in R3 by A13;
A17: x = (C1 ^ fs1) ^ fs2 by A11, A14, FINSEQ_1:32;
consider C being firing-sequence of N such that
A18: C = C1 ^ fs1 and
A19: C1 in R1 and
A20: fs1 in R2 by A12, A15;
C in R1 before R2 by A18, A19, A20;
hence x in (R1 before R2) before R3 by A16, A17, A18; ::_thesis: verum
end;
definition
let p be FinSubsequence;
let i be Element of NAT ;
set X = { (i + k) where k is Element of NAT : k in dom p } ;
funci Shift p -> FinSubsequence means :Def14: :: PNPROC_1:def 14
( dom it = { (i + k) where k is Element of NAT : k in dom p } & ( for j being Nat st j in dom p holds
it . (i + j) = p . j ) );
existence
ex b1 being FinSubsequence st
( dom b1 = { (i + k) where k is Element of NAT : k in dom p } & ( for j being Nat st j in dom p holds
b1 . (i + j) = p . j ) )
proof
consider K being Nat such that
A1: dom p c= Seg K by FINSEQ_1:def_12;
defpred S1[ set , set ] means ex k being Element of NAT st
( $1 = i + k & $2 = p . k );
A2: for x being set st x in { (i + k) where k is Element of NAT : k in dom p } holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in { (i + k) where k is Element of NAT : k in dom p } implies ex y being set st S1[x,y] )
assume x in { (i + k) where k is Element of NAT : k in dom p } ; ::_thesis: ex y being set st S1[x,y]
then consider k being Element of NAT such that
A3: x = i + k and
A4: k in dom p ;
[k,(p . k)] in p by A4, FUNCT_1:def_2;
hence ex y being set st S1[x,y] by A3; ::_thesis: verum
end;
consider f being Function such that
A5: dom f = { (i + k) where k is Element of NAT : k in dom p } and
A6: for x being set st x in { (i + k) where k is Element of NAT : k in dom p } holds
S1[x,f . x] from CLASSES1:sch_1(A2);
{ (i + k) where k is Element of NAT : k in dom p } c= Seg (i + K)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (i + k) where k is Element of NAT : k in dom p } or x in Seg (i + K) )
assume x in { (i + k) where k is Element of NAT : k in dom p } ; ::_thesis: x in Seg (i + K)
then consider k being Element of NAT such that
A7: x = i + k and
A8: k in dom p ;
A9: i + k >= k by NAT_1:11;
A10: k >= 1 by A1, A8, FINSEQ_1:1;
A11: k <= K by A1, A8, FINSEQ_1:1;
A12: i + k >= 1 by A9, A10, XXREAL_0:2;
i + k <= i + K by A11, XREAL_1:6;
hence x in Seg (i + K) by A7, A12, FINSEQ_1:1; ::_thesis: verum
end;
then reconsider f = f as FinSubsequence by A5, FINSEQ_1:def_12;
take f ; ::_thesis: ( dom f = { (i + k) where k is Element of NAT : k in dom p } & ( for j being Nat st j in dom p holds
f . (i + j) = p . j ) )
thus dom f = { (i + k) where k is Element of NAT : k in dom p } by A5; ::_thesis: for j being Nat st j in dom p holds
f . (i + j) = p . j
let j be Nat; ::_thesis: ( j in dom p implies f . (i + j) = p . j )
A13: j in NAT by ORDINAL1:def_12;
assume j in dom p ; ::_thesis: f . (i + j) = p . j
then i + j in { (i + k) where k is Element of NAT : k in dom p } by A13;
then ex k being Element of NAT st
( i + j = i + k & f . (i + j) = p . k ) by A6;
hence f . (i + j) = p . j ; ::_thesis: verum
end;
uniqueness
for b1, b2 being FinSubsequence st dom b1 = { (i + k) where k is Element of NAT : k in dom p } & ( for j being Nat st j in dom p holds
b1 . (i + j) = p . j ) & dom b2 = { (i + k) where k is Element of NAT : k in dom p } & ( for j being Nat st j in dom p holds
b2 . (i + j) = p . j ) holds
b1 = b2
proof
let f1, f2 be FinSubsequence; ::_thesis: ( dom f1 = { (i + k) where k is Element of NAT : k in dom p } & ( for j being Nat st j in dom p holds
f1 . (i + j) = p . j ) & dom f2 = { (i + k) where k is Element of NAT : k in dom p } & ( for j being Nat st j in dom p holds
f2 . (i + j) = p . j ) implies f1 = f2 )
assume that
A14: dom f1 = { (i + k) where k is Element of NAT : k in dom p } and
A15: for j being Nat st j in dom p holds
f1 . (i + j) = p . j and
A16: dom f2 = { (i + k) where k is Element of NAT : k in dom p } and
A17: for j being Nat st j in dom p holds
f2 . (i + j) = p . j ; ::_thesis: f1 = f2
now__::_thesis:_for_x_being_set_st_x_in__{__(i_+_k)_where_k_is_Element_of_NAT_:_k_in_dom_p__}__holds_
f1_._x_=_f2_._x
let x be set ; ::_thesis: ( x in { (i + k) where k is Element of NAT : k in dom p } implies f1 . x = f2 . x )
assume x in { (i + k) where k is Element of NAT : k in dom p } ; ::_thesis: f1 . x = f2 . x
then consider k being Element of NAT such that
A18: x = i + k and
A19: k in dom p ;
thus f1 . x = p . k by A15, A18, A19
.= f2 . x by A17, A18, A19 ; ::_thesis: verum
end;
hence f1 = f2 by A14, A16, FUNCT_1:2; ::_thesis: verum
end;
end;
:: deftheorem Def14 defines Shift PNPROC_1:def_14_:_
for p being FinSubsequence
for i being Element of NAT
for b3 being FinSubsequence holds
( b3 = i Shift p iff ( dom b3 = { (i + k) where k is Element of NAT : k in dom p } & ( for j being Nat st j in dom p holds
b3 . (i + j) = p . j ) ) );
theorem :: PNPROC_1:49
for q being FinSubsequence holds 0 Shift q = q
proof
let q be FinSubsequence; ::_thesis: 0 Shift q = q
set X = { (0 + k) where k is Element of NAT : k in dom q } ;
A1: dom (0 Shift q) = { (0 + k) where k is Element of NAT : k in dom q } by Def14;
A2: { (0 + k) where k is Element of NAT : k in dom q } = dom q
proof
thus { (0 + k) where k is Element of NAT : k in dom q } c= dom q :: according to XBOOLE_0:def_10 ::_thesis: dom q c= { (0 + k) where k is Element of NAT : k in dom q }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (0 + k) where k is Element of NAT : k in dom q } or x in dom q )
assume x in { (0 + k) where k is Element of NAT : k in dom q } ; ::_thesis: x in dom q
then ex k being Element of NAT st
( x = 0 + k & k in dom q ) ;
hence x in dom q ; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom q or x in { (0 + k) where k is Element of NAT : k in dom q } )
assume A3: x in dom q ; ::_thesis: x in { (0 + k) where k is Element of NAT : k in dom q }
consider l being Nat such that
A4: dom q c= Seg l by FINSEQ_1:def_12;
x in Seg l by A3, A4;
then reconsider k = x as Element of NAT ;
x = 0 + k ;
hence x in { (0 + k) where k is Element of NAT : k in dom q } by A3; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in__{__(0_+_k)_where_k_is_Element_of_NAT_:_k_in_dom_q__}__holds_
(0_Shift_q)_._x_=_q_._x
let x be set ; ::_thesis: ( x in { (0 + k) where k is Element of NAT : k in dom q } implies (0 Shift q) . x = q . x )
assume x in { (0 + k) where k is Element of NAT : k in dom q } ; ::_thesis: (0 Shift q) . x = q . x
then ex k being Element of NAT st
( x = 0 + k & k in dom q ) ;
hence (0 Shift q) . x = q . x by Def14; ::_thesis: verum
end;
hence 0 Shift q = q by A1, A2, FUNCT_1:2; ::_thesis: verum
end;
theorem :: PNPROC_1:50
for i, j being Element of NAT
for q being FinSubsequence holds (i + j) Shift q = i Shift (j Shift q)
proof
let i, j be Element of NAT ; ::_thesis: for q being FinSubsequence holds (i + j) Shift q = i Shift (j Shift q)
let q be FinSubsequence; ::_thesis: (i + j) Shift q = i Shift (j Shift q)
set Sj = j Shift q;
set Sij = (i + j) Shift q;
set Si = i Shift (j Shift q);
set Xj = { (j + k) where k is Element of NAT : k in dom q } ;
set Xi = { (i + k) where k is Element of NAT : k in dom (j Shift q) } ;
set Xij = { ((i + j) + k) where k is Element of NAT : k in dom q } ;
A1: dom (j Shift q) = { (j + k) where k is Element of NAT : k in dom q } by Def14;
A2: dom (i Shift (j Shift q)) = { (i + k) where k is Element of NAT : k in dom (j Shift q) } by Def14;
A3: dom ((i + j) Shift q) = { ((i + j) + k) where k is Element of NAT : k in dom q } by Def14;
A4: { (i + k) where k is Element of NAT : k in dom (j Shift q) } = { ((i + j) + k) where k is Element of NAT : k in dom q }
proof
thus { (i + k) where k is Element of NAT : k in dom (j Shift q) } c= { ((i + j) + k) where k is Element of NAT : k in dom q } :: according to XBOOLE_0:def_10 ::_thesis: { ((i + j) + k) where k is Element of NAT : k in dom q } c= { (i + k) where k is Element of NAT : k in dom (j Shift q) }
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { (i + k) where k is Element of NAT : k in dom (j Shift q) } or x in { ((i + j) + k) where k is Element of NAT : k in dom q } )
assume x in { (i + k) where k is Element of NAT : k in dom (j Shift q) } ; ::_thesis: x in { ((i + j) + k) where k is Element of NAT : k in dom q }
then consider k being Element of NAT such that
A5: x = i + k and
A6: k in dom (j Shift q) ;
dom (j Shift q) = { (j + K) where K is Element of NAT : K in dom q } by Def14;
then consider K being Element of NAT such that
A7: k = j + K and
A8: K in dom q by A6;
x = (i + j) + K by A5, A7;
hence x in { ((i + j) + k) where k is Element of NAT : k in dom q } by A8; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { ((i + j) + k) where k is Element of NAT : k in dom q } or x in { (i + k) where k is Element of NAT : k in dom (j Shift q) } )
assume x in { ((i + j) + k) where k is Element of NAT : k in dom q } ; ::_thesis: x in { (i + k) where k is Element of NAT : k in dom (j Shift q) }
then consider k being Element of NAT such that
A9: x = (i + j) + k and
A10: k in dom q ;
reconsider K = j + k as Element of NAT ;
A11: dom (j Shift q) = { (j + l) where l is Element of NAT : l in dom q } by Def14;
A12: x = i + K by A9;
K in dom (j Shift q) by A10, A11;
hence x in { (i + k) where k is Element of NAT : k in dom (j Shift q) } by A12; ::_thesis: verum
end;
now__::_thesis:_for_x_being_set_st_x_in__{__((i_+_j)_+_k)_where_k_is_Element_of_NAT_:_k_in_dom_q__}__holds_
((i_+_j)_Shift_q)_._x_=_(i_Shift_(j_Shift_q))_._x
let x be set ; ::_thesis: ( x in { ((i + j) + k) where k is Element of NAT : k in dom q } implies ((i + j) Shift q) . x = (i Shift (j Shift q)) . x )
assume x in { ((i + j) + k) where k is Element of NAT : k in dom q } ; ::_thesis: ((i + j) Shift q) . x = (i Shift (j Shift q)) . x
then consider k being Element of NAT such that
A13: x = (i + j) + k and
A14: k in dom q ;
A15: x = i + (j + k) by A13;
A16: j + k in dom (j Shift q) by A1, A14;
thus ((i + j) Shift q) . x = q . k by A13, A14, Def14
.= (j Shift q) . (j + k) by A14, Def14
.= (i Shift (j Shift q)) . x by A15, A16, Def14 ; ::_thesis: verum
end;
hence (i + j) Shift q = i Shift (j Shift q) by A2, A3, A4, FUNCT_1:2; ::_thesis: verum
end;
theorem Th51: :: PNPROC_1:51
for i being Element of NAT
for p being FinSequence holds dom (i Shift p) = { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) }
proof
let i be Element of NAT ; ::_thesis: for p being FinSequence holds dom (i Shift p) = { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) }
let p be FinSequence; ::_thesis: dom (i Shift p) = { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) }
A1: dom p = Seg (len p) by FINSEQ_1:def_3
.= { k where k is Element of NAT : ( 1 <= k & k <= len p ) } by FINSEQ_1:def_1 ;
set X = { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) } ;
A2: dom (i Shift p) = { (i + k1) where k1 is Element of NAT : k1 in dom p } by Def14;
thus dom (i Shift p) c= { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) } :: according to XBOOLE_0:def_10 ::_thesis: { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) } c= dom (i Shift p)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (i Shift p) or x in { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) } )
assume x in dom (i Shift p) ; ::_thesis: x in { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) }
then consider k1 being Element of NAT such that
A3: x = i + k1 and
A4: k1 in dom p by A2;
consider k being Element of NAT such that
A5: k1 = k and
A6: 1 <= k and
A7: k <= len p by A1, A4;
A8: i + 1 <= i + k by A6, XREAL_1:7;
i + k <= i + (len p) by A7, XREAL_1:7;
hence x in { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) } by A3, A5, A8; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) } or x in dom (i Shift p) )
assume x in { j1 where j1 is Element of NAT : ( i + 1 <= j1 & j1 <= i + (len p) ) } ; ::_thesis: x in dom (i Shift p)
then consider j1 being Element of NAT such that
A9: x = j1 and
A10: i + 1 <= j1 and
A11: j1 <= i + (len p) ;
i + 0 <= i + 1 by XREAL_1:7;
then consider k2 being Nat such that
A12: j1 = i + k2 by A10, NAT_1:10, XXREAL_0:2;
A13: k2 in NAT by ORDINAL1:def_12;
A14: 1 <= k2 by A10, A12, XREAL_1:6;
k2 <= len p by A11, A12, XREAL_1:6;
then k2 in dom p by A1, A13, A14;
hence x in dom (i Shift p) by A2, A9, A12; ::_thesis: verum
end;
theorem :: PNPROC_1:52
for i being Element of NAT
for q being FinSubsequence holds
( q = {} iff i Shift q = {} )
proof
let i be Element of NAT ; ::_thesis: for q being FinSubsequence holds
( q = {} iff i Shift q = {} )
let q be FinSubsequence; ::_thesis: ( q = {} iff i Shift q = {} )
A1: dom (i Shift q) = { (i + k) where k is Element of NAT : k in dom q } by Def14;
thus ( q = {} implies i Shift q = {} ) ::_thesis: ( i Shift q = {} implies q = {} )
proof
assume A2: q = {} ; ::_thesis: i Shift q = {}
now__::_thesis:_for_x,_y_being_set_holds_not_[x,y]_in_i_Shift_q
let x, y be set ; ::_thesis: not [x,y] in i Shift q
now__::_thesis:_not_x_in_dom_(i_Shift_q)
assume x in dom (i Shift q) ; ::_thesis: contradiction
then ex k being Element of NAT st
( x = i + k & k in dom q ) by A1;
hence contradiction by A2; ::_thesis: verum
end;
hence not [x,y] in i Shift q by FUNCT_1:1; ::_thesis: verum
end;
hence i Shift q = {} by RELAT_1:37; ::_thesis: verum
end;
assume A3: i Shift q = {} ; ::_thesis: q = {}
now__::_thesis:_not_q_<>_{}
assume q <> {} ; ::_thesis: contradiction
then consider x being set such that
A4: x in dom q by XBOOLE_0:def_1;
A5: x in rng (Sgm (dom q)) by A4, FINSEQ_1:50;
rng (Sgm (dom q)) c= NAT by FINSEQ_1:def_4;
then reconsider x = x as Element of NAT by A5;
consider k being Element of NAT such that
A6: k = i + x and
A7: x in dom q by A4;
k in dom (i Shift q) by A1, A6, A7;
hence contradiction by A3; ::_thesis: verum
end;
hence q = {} ; ::_thesis: verum
end;
theorem Th53: :: PNPROC_1:53
for i being Element of NAT
for q being FinSubsequence ex ss being FinSubsequence st
( dom ss = dom q & rng ss = dom (i Shift q) & ( for k being Element of NAT st k in dom q holds
ss . k = i + k ) & ss is one-to-one )
proof
let i be Element of NAT ; ::_thesis: for q being FinSubsequence ex ss being FinSubsequence st
( dom ss = dom q & rng ss = dom (i Shift q) & ( for k being Element of NAT st k in dom q holds
ss . k = i + k ) & ss is one-to-one )
let q be FinSubsequence; ::_thesis: ex ss being FinSubsequence st
( dom ss = dom q & rng ss = dom (i Shift q) & ( for k being Element of NAT st k in dom q holds
ss . k = i + k ) & ss is one-to-one )
consider n being Nat such that
A1: dom q c= Seg n by FINSEQ_1:def_12;
defpred S1[ set , set ] means ex k being Element of NAT st
( k = $1 & $2 = i + k );
A2: for x being set st x in dom q holds
ex y being set st S1[x,y]
proof
let x be set ; ::_thesis: ( x in dom q implies ex y being set st S1[x,y] )
assume x in dom q ; ::_thesis: ex y being set st S1[x,y]
then x in Seg n by A1;
then reconsider x = x as Element of NAT ;
take i + x ; ::_thesis: S1[x,i + x]
thus S1[x,i + x] ; ::_thesis: verum
end;
consider f being Function such that
A3: dom f = dom q and
A4: for x being set st x in dom q holds
S1[x,f . x] from CLASSES1:sch_1(A2);
reconsider ss = f as FinSubsequence by A1, A3, FINSEQ_1:def_12;
A5: dom (i Shift q) = { (i + k) where k is Element of NAT : k in dom q } by Def14;
A6: rng ss = dom (i Shift q)
proof
thus rng ss c= dom (i Shift q) :: according to XBOOLE_0:def_10 ::_thesis: dom (i Shift q) c= rng ss
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ss or y in dom (i Shift q) )
assume y in rng ss ; ::_thesis: y in dom (i Shift q)
then consider x being set such that
A7: x in dom ss and
A8: y = ss . x by FUNCT_1:def_3;
ex k1 being Element of NAT st
( k1 = x & ss . x = i + k1 ) by A3, A4, A7;
hence y in dom (i Shift q) by A3, A5, A7, A8; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in dom (i Shift q) or y in rng ss )
assume y in dom (i Shift q) ; ::_thesis: y in rng ss
then consider k2 being Element of NAT such that
A9: y = i + k2 and
A10: k2 in dom q by A5;
ex k3 being Element of NAT st
( k3 = k2 & ss . k2 = i + k3 ) by A4, A10;
hence y in rng ss by A3, A9, A10, FUNCT_1:def_3; ::_thesis: verum
end;
A11: for k being Element of NAT st k in dom q holds
ss . k = i + k
proof
let k be Element of NAT ; ::_thesis: ( k in dom q implies ss . k = i + k )
assume k in dom q ; ::_thesis: ss . k = i + k
then ex k1 being Element of NAT st
( k1 = k & ss . k = i + k1 ) by A4;
hence ss . k = i + k ; ::_thesis: verum
end;
for x1, x2 being set st x1 in dom ss & x2 in dom ss & ss . x1 = ss . x2 holds
x1 = x2
proof
let x1, x2 be set ; ::_thesis: ( x1 in dom ss & x2 in dom ss & ss . x1 = ss . x2 implies x1 = x2 )
assume that
A12: x1 in dom ss and
A13: x2 in dom ss and
A14: ss . x1 = ss . x2 ; ::_thesis: x1 = x2
A15: ex k1 being Element of NAT st
( k1 = x1 & ss . x1 = i + k1 ) by A3, A4, A12;
ex k2 being Element of NAT st
( k2 = x2 & ss . x2 = i + k2 ) by A3, A4, A13;
hence x1 = x2 by A14, A15; ::_thesis: verum
end;
then ss is one-to-one by FUNCT_1:def_4;
hence ex ss being FinSubsequence st
( dom ss = dom q & rng ss = dom (i Shift q) & ( for k being Element of NAT st k in dom q holds
ss . k = i + k ) & ss is one-to-one ) by A3, A6, A11; ::_thesis: verum
end;
Lm8: for i being Element of NAT
for p being FinSequence ex fs being FinSequence st
( dom fs = dom p & rng fs = dom (i Shift p) & ( for k being Element of NAT st k in dom p holds
fs . k = i + k ) & fs is one-to-one )
proof
let i be Element of NAT ; ::_thesis: for p being FinSequence ex fs being FinSequence st
( dom fs = dom p & rng fs = dom (i Shift p) & ( for k being Element of NAT st k in dom p holds
fs . k = i + k ) & fs is one-to-one )
let p be FinSequence; ::_thesis: ex fs being FinSequence st
( dom fs = dom p & rng fs = dom (i Shift p) & ( for k being Element of NAT st k in dom p holds
fs . k = i + k ) & fs is one-to-one )
consider ss being FinSubsequence such that
A1: dom ss = dom p and
A2: rng ss = dom (i Shift p) and
A3: for k being Element of NAT st k in dom p holds
ss . k = i + k and
A4: ss is one-to-one by Th53;
dom ss = Seg (len p) by A1, FINSEQ_1:def_3;
then reconsider fs = ss as FinSequence by FINSEQ_1:def_2;
dom fs = dom p by A1;
hence ex fs being FinSequence st
( dom fs = dom p & rng fs = dom (i Shift p) & ( for k being Element of NAT st k in dom p holds
fs . k = i + k ) & fs is one-to-one ) by A2, A3, A4; ::_thesis: verum
end;
theorem Th54: :: PNPROC_1:54
for i being Element of NAT
for q being FinSubsequence holds card q = card (i Shift q)
proof
let i be Element of NAT ; ::_thesis: for q being FinSubsequence holds card q = card (i Shift q)
let q be FinSubsequence; ::_thesis: card q = card (i Shift q)
ex ss being FinSubsequence st
( dom ss = dom q & rng ss = dom (i Shift q) & ( for k being Element of NAT st k in dom q holds
ss . k = i + k ) & ss is one-to-one ) by Th53;
then A1: dom q, dom (i Shift q) are_equipotent by WELLORD2:def_4;
A2: card (dom q) = card q by CARD_1:62;
card (dom (i Shift q)) = card (i Shift q) by CARD_1:62;
hence card q = card (i Shift q) by A1, A2, CARD_1:5; ::_thesis: verum
end;
theorem Th55: :: PNPROC_1:55
for i being Element of NAT
for p being FinSequence holds dom p = dom (Seq (i Shift p))
proof
let i be Element of NAT ; ::_thesis: for p being FinSequence holds dom p = dom (Seq (i Shift p))
let p be FinSequence; ::_thesis: dom p = dom (Seq (i Shift p))
A1: rng (Sgm (dom (i Shift p))) = dom (i Shift p) by FINSEQ_1:50;
A2: Seq (i Shift p) = (i Shift p) * (Sgm (dom (i Shift p))) by FINSEQ_1:def_14;
A3: dom p = Seg (len p) by FINSEQ_1:def_3;
A4: dom (Sgm (dom (i Shift p))) = Seg (len (Sgm (dom (i Shift p)))) by FINSEQ_1:def_3;
ex k being Nat st dom (i Shift p) c= Seg k by FINSEQ_1:def_12;
then A5: len (Sgm (dom (i Shift p))) = card (dom (i Shift p)) by FINSEQ_3:39;
card (dom (i Shift p)) = card (i Shift p) by CARD_1:62;
then card (dom (i Shift p)) = len p by Th54;
hence dom p = dom (Seq (i Shift p)) by A1, A2, A3, A4, A5, RELAT_1:27; ::_thesis: verum
end;
theorem Th56: :: PNPROC_1:56
for k, i being Element of NAT
for p being FinSequence st k in dom p holds
(Sgm (dom (i Shift p))) . k = i + k
proof
let k, i be Element of NAT ; ::_thesis: for p being FinSequence st k in dom p holds
(Sgm (dom (i Shift p))) . k = i + k
let p be FinSequence; ::_thesis: ( k in dom p implies (Sgm (dom (i Shift p))) . k = i + k )
assume A1: k in dom p ; ::_thesis: (Sgm (dom (i Shift p))) . k = i + k
consider fs being FinSequence such that
A2: dom fs = dom p and
A3: rng fs = dom (i Shift p) and
A4: for j being Element of NAT st j in dom p holds
fs . j = i + j and
fs is one-to-one by Lm8;
A5: ex l being Nat st dom (i Shift p) c= Seg l by FINSEQ_1:def_12;
rng fs = rng (Sgm (dom (i Shift p))) by A3, FINSEQ_1:50;
then reconsider fs = fs as FinSequence of NAT by FINSEQ_1:def_4;
for n, m, k1, k2 being Nat st 1 <= n & n < m & m <= len fs & k1 = fs . n & k2 = fs . m holds
k1 < k2
proof
let n, m, k1, k2 be Nat; ::_thesis: ( 1 <= n & n < m & m <= len fs & k1 = fs . n & k2 = fs . m implies k1 < k2 )
assume that
A6: 1 <= n and
A7: n < m and
A8: m <= len fs and
A9: k1 = fs . n and
A10: k2 = fs . m ; ::_thesis: k1 < k2
reconsider n = n, m = m as Element of NAT by ORDINAL1:def_12;
A11: dom fs = Seg (len fs) by FINSEQ_1:def_3
.= { n1 where n1 is Element of NAT : ( 1 <= n1 & n1 <= len fs ) } by FINSEQ_1:def_1 ;
n + 1 <= m by A7, INT_1:7;
then n + 1 <= len fs by A8, XXREAL_0:2;
then A12: n <= (len fs) - 1 by XREAL_1:19;
(len fs) + 0 <= (len fs) + 1 by XREAL_1:7;
then (len fs) - 1 <= len fs by XREAL_1:20;
then n <= len fs by A12, XXREAL_0:2;
then A13: n in dom p by A2, A6, A11;
1 <= m by A6, A7, XXREAL_0:2;
then A14: m in dom p by A2, A8, A11;
A15: k1 = i + n by A4, A9, A13;
k2 = i + m by A4, A10, A14;
hence k1 < k2 by A7, A15, XREAL_1:8; ::_thesis: verum
end;
then fs = Sgm (dom (i Shift p)) by A3, A5, FINSEQ_1:def_13;
hence (Sgm (dom (i Shift p))) . k = i + k by A1, A4; ::_thesis: verum
end;
theorem Th57: :: PNPROC_1:57
for k, i being Element of NAT
for p being FinSequence st k in dom p holds
(Seq (i Shift p)) . k = p . k
proof
let k, i be Element of NAT ; ::_thesis: for p being FinSequence st k in dom p holds
(Seq (i Shift p)) . k = p . k
let p be FinSequence; ::_thesis: ( k in dom p implies (Seq (i Shift p)) . k = p . k )
assume A1: k in dom p ; ::_thesis: (Seq (i Shift p)) . k = p . k
then A2: k in dom (Seq (i Shift p)) by Th55;
A3: Seq (i Shift p) = (i Shift p) * (Sgm (dom (i Shift p))) by FINSEQ_1:def_14;
A4: (Seq (i Shift p)) . k = ((i Shift p) * (Sgm (dom (i Shift p)))) . k by FINSEQ_1:def_14;
((i Shift p) * (Sgm (dom (i Shift p)))) . k = (i Shift p) . ((Sgm (dom (i Shift p))) . k) by A2, A3, FUNCT_1:12
.= (i Shift p) . (i + k) by A1, Th56 ;
hence (Seq (i Shift p)) . k = p . k by A1, A4, Def14; ::_thesis: verum
end;
theorem Th58: :: PNPROC_1:58
for i being Element of NAT
for p being FinSequence holds Seq (i Shift p) = p
proof
let i be Element of NAT ; ::_thesis: for p being FinSequence holds Seq (i Shift p) = p
let p be FinSequence; ::_thesis: Seq (i Shift p) = p
A1: dom (Seq (i Shift p)) = dom p by Th55;
for x being set st x in dom p holds
(Seq (i Shift p)) . x = p . x by Th57;
hence Seq (i Shift p) = p by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th59: :: PNPROC_1:59
for p1, p2 being FinSequence holds dom (p1 \/ ((len p1) Shift p2)) = Seg ((len p1) + (len p2))
proof
let p1, p2 be FinSequence; ::_thesis: dom (p1 \/ ((len p1) Shift p2)) = Seg ((len p1) + (len p2))
A1: Seg ((len p1) + (len p2)) = { j where j is Element of NAT : ( 1 <= j & j <= (len p1) + (len p2) ) } by FINSEQ_1:def_1;
A2: dom (p1 \/ ((len p1) Shift p2)) = (dom p1) \/ (dom ((len p1) Shift p2)) by RELAT_1:1;
A3: dom p1 = Seg (len p1) by FINSEQ_1:def_3
.= { k where k is Element of NAT : ( 1 <= k & k <= len p1 ) } by FINSEQ_1:def_1 ;
A4: dom ((len p1) Shift p2) = { k1 where k1 is Element of NAT : ( (len p1) + 1 <= k1 & k1 <= (len p1) + (len p2) ) } by Th51;
thus dom (p1 \/ ((len p1) Shift p2)) c= Seg ((len p1) + (len p2)) :: according to XBOOLE_0:def_10 ::_thesis: Seg ((len p1) + (len p2)) c= dom (p1 \/ ((len p1) Shift p2))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (p1 \/ ((len p1) Shift p2)) or x in Seg ((len p1) + (len p2)) )
assume x in dom (p1 \/ ((len p1) Shift p2)) ; ::_thesis: x in Seg ((len p1) + (len p2))
then ( x in dom p1 or x in dom ((len p1) Shift p2) ) by A2, XBOOLE_0:def_3;
then A5: ex k3 being Element of NAT st
( ( x = k3 & 1 <= k3 & k3 <= len p1 ) or ( x = k3 & (len p1) + 1 <= k3 & k3 <= (len p1) + (len p2) ) ) by A3, A4;
then reconsider x = x as Element of NAT ;
A6: 1 <= x by A5, Lm2;
x <= (len p1) + (len p2) by A5, Lm2;
hence x in Seg ((len p1) + (len p2)) by A1, A6; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Seg ((len p1) + (len p2)) or x in dom (p1 \/ ((len p1) Shift p2)) )
assume x in Seg ((len p1) + (len p2)) ; ::_thesis: x in dom (p1 \/ ((len p1) Shift p2))
then consider j being Element of NAT such that
A7: x = j and
A8: 1 <= j and
A9: j <= (len p1) + (len p2) by A1;
reconsider i0 = len p1 as Integer ;
( ( 1 <= j & j <= i0 ) or ( i0 + 1 <= j & j <= i0 + (len p2) ) ) by A8, A9, INT_1:7;
then ( x in dom p1 or x in dom ((len p1) Shift p2) ) by A3, A4, A7;
hence x in dom (p1 \/ ((len p1) Shift p2)) by A2, XBOOLE_0:def_3; ::_thesis: verum
end;
theorem Th60: :: PNPROC_1:60
for i being Element of NAT
for p1 being FinSequence
for p2 being FinSubsequence st len p1 <= i holds
dom p1 misses dom (i Shift p2)
proof
let i be Element of NAT ; ::_thesis: for p1 being FinSequence
for p2 being FinSubsequence st len p1 <= i holds
dom p1 misses dom (i Shift p2)
let p1 be FinSequence; ::_thesis: for p2 being FinSubsequence st len p1 <= i holds
dom p1 misses dom (i Shift p2)
let p2 be FinSubsequence; ::_thesis: ( len p1 <= i implies dom p1 misses dom (i Shift p2) )
assume A1: len p1 <= i ; ::_thesis: dom p1 misses dom (i Shift p2)
A2: dom p1 = Seg (len p1) by FINSEQ_1:def_3
.= { k where k is Element of NAT : ( 1 <= k & k <= len p1 ) } by FINSEQ_1:def_1 ;
A3: dom (i Shift p2) = { (i + k) where k is Element of NAT : k in dom p2 } by Def14;
for x being set holds not x in (dom p1) /\ (dom (i Shift p2))
proof
given x being set such that A4: x in (dom p1) /\ (dom (i Shift p2)) ; ::_thesis: contradiction
A5: x in dom p1 by A4, XBOOLE_0:def_4;
A6: x in dom (i Shift p2) by A4, XBOOLE_0:def_4;
A7: ex k1 being Element of NAT st
( x = k1 & 1 <= k1 & k1 <= len p1 ) by A2, A5;
consider k2 being Element of NAT such that
A8: x = i + k2 and
A9: k2 in dom p2 by A3, A6;
consider n being Nat such that
A10: dom p2 c= Seg n by FINSEQ_1:def_12;
A11: k2 in Seg n by A9, A10;
Seg n = { m where m is Element of NAT : ( 1 <= m & m <= n ) } by FINSEQ_1:def_1;
then ex m being Element of NAT st
( k2 = m & 1 <= m & m <= n ) by A11;
then A12: 1 - 1 < k2 - 0 by XREAL_1:15;
reconsider x = x as Element of NAT by A4;
(len p1) + k2 <= i + k2 by A1, XREAL_1:7;
then ((len p1) + k2) - k2 < x - 0 by A8, A12, XREAL_1:15;
hence contradiction by A7; ::_thesis: verum
end;
hence (dom p1) /\ (dom (i Shift p2)) = {} by XBOOLE_0:def_1; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
theorem Th61: :: PNPROC_1:61
for p1, p2 being FinSequence holds p1 ^ p2 = p1 \/ ((len p1) Shift p2)
proof
let p1, p2 be FinSequence; ::_thesis: p1 ^ p2 = p1 \/ ((len p1) Shift p2)
A1: dom (p1 \/ ((len p1) Shift p2)) = Seg ((len p1) + (len p2)) by Th59;
dom p1 misses dom ((len p1) Shift p2) by Th60;
then reconsider p = p1 \/ ((len p1) Shift p2) as FinSequence by A1, FINSEQ_1:def_2, GRFUNC_1:13;
A2: dom p = Seg ((len p1) + (len p2)) by Th59;
A3: for k being Nat st k in dom p1 holds
p . k = p1 . k
proof
let k be Nat; ::_thesis: ( k in dom p1 implies p . k = p1 . k )
assume k in dom p1 ; ::_thesis: p . k = p1 . k
then [k,(p1 . k)] in p1 by FUNCT_1:def_2;
then [k,(p1 . k)] in p by XBOOLE_0:def_3;
hence p . k = p1 . k by FUNCT_1:1; ::_thesis: verum
end;
for k being Nat st k in dom p2 holds
p . ((len p1) + k) = p2 . k
proof
let k be Nat; ::_thesis: ( k in dom p2 implies p . ((len p1) + k) = p2 . k )
assume A4: k in dom p2 ; ::_thesis: p . ((len p1) + k) = p2 . k
dom ((len p1) Shift p2) = { ((len p1) + j) where j is Element of NAT : j in dom p2 } by Def14;
then (len p1) + k in dom ((len p1) Shift p2) by A4;
then [((len p1) + k),(((len p1) Shift p2) . ((len p1) + k))] in (len p1) Shift p2 by FUNCT_1:def_2;
then [((len p1) + k),(((len p1) Shift p2) . ((len p1) + k))] in p by XBOOLE_0:def_3;
then p . ((len p1) + k) = ((len p1) Shift p2) . ((len p1) + k) by FUNCT_1:1;
hence p . ((len p1) + k) = p2 . k by A4, Def14; ::_thesis: verum
end;
hence p1 ^ p2 = p1 \/ ((len p1) Shift p2) by A2, A3, FINSEQ_1:def_7; ::_thesis: verum
end;
theorem Th62: :: PNPROC_1:62
for i being Element of NAT
for p1 being FinSequence
for p2 being FinSubsequence st i >= len p1 holds
p1 misses i Shift p2
proof
let i be Element of NAT ; ::_thesis: for p1 being FinSequence
for p2 being FinSubsequence st i >= len p1 holds
p1 misses i Shift p2
let p1 be FinSequence; ::_thesis: for p2 being FinSubsequence st i >= len p1 holds
p1 misses i Shift p2
let p2 be FinSubsequence; ::_thesis: ( i >= len p1 implies p1 misses i Shift p2 )
assume i >= len p1 ; ::_thesis: p1 misses i Shift p2
then dom p1 misses dom (i Shift p2) by Th60;
hence p1 misses i Shift p2 by Lm4; ::_thesis: verum
end;
theorem :: PNPROC_1:63
for P being set
for N being Petri_net of P
for R1, R2, R3 being process of N holds (R1 concur R2) concur R3 = R1 concur (R2 concur R3)
proof
let P be set ; ::_thesis: for N being Petri_net of P
for R1, R2, R3 being process of N holds (R1 concur R2) concur R3 = R1 concur (R2 concur R3)
let N be Petri_net of P; ::_thesis: for R1, R2, R3 being process of N holds (R1 concur R2) concur R3 = R1 concur (R2 concur R3)
let R1, R2, R3 be process of N; ::_thesis: (R1 concur R2) concur R3 = R1 concur (R2 concur R3)
thus (R1 concur R2) concur R3 c= R1 concur (R2 concur R3) :: according to XBOOLE_0:def_10 ::_thesis: R1 concur (R2 concur R3) c= (R1 concur R2) concur R3
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (R1 concur R2) concur R3 or x in R1 concur (R2 concur R3) )
assume x in (R1 concur R2) concur R3 ; ::_thesis: x in R1 concur (R2 concur R3)
then consider C1 being firing-sequence of N such that
A1: x = C1 and
A2: ex q1, q2 being FinSubsequence st
( C1 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 concur R2 & Seq q2 in R3 ) ;
consider q1, q2 being FinSubsequence such that
A3: C1 = q1 \/ q2 and
A4: q1 misses q2 and
A5: Seq q1 in R1 concur R2 and
A6: Seq q2 in R3 by A2;
consider C2 being firing-sequence of N such that
A7: Seq q1 = C2 and
A8: ex q3, q4 being FinSubsequence st
( C2 = q3 \/ q4 & q3 misses q4 & Seq q3 in R1 & Seq q4 in R2 ) by A5;
consider q3, q4 being FinSubsequence such that
A9: C2 = q3 \/ q4 and
A10: q3 misses q4 and
A11: Seq q3 in R1 and
A12: Seq q4 in R2 by A8;
consider n1 being Nat such that
A13: dom q1 c= Seg n1 by FINSEQ_1:def_12;
A14: q3 c= Seq q1 by A7, A9, XBOOLE_1:7;
A15: q4 c= Seq q1 by A7, A9, XBOOLE_1:7;
Sgm (dom q1) is one-to-one by A13, FINSEQ_3:92;
then A16: (Sgm (dom q1)) .: (dom q3) misses (Sgm (dom q1)) .: (dom q4) by A10, A14, A15, Th9, FUNCT_1:66;
A17: rng ((Sgm (dom q1)) | (dom q3)) = (Sgm (dom q1)) .: (dom q3) by RELAT_1:115;
A18: rng ((Sgm (dom q1)) | (dom q4)) = (Sgm (dom q1)) .: (dom q4) by RELAT_1:115;
then A19: q1 | (rng ((Sgm (dom q1)) | (dom q3))) misses q1 | (rng ((Sgm (dom q1)) | (dom q4))) by A16, A17, Th8;
A20: dom (Sgm (dom q1)) = dom (q3 \/ q4) by A7, A9, Lm5
.= (dom q3) \/ (dom q4) by RELAT_1:1 ;
A21: (q1 | (rng ((Sgm (dom q1)) | (dom q3)))) \/ (q1 | (rng ((Sgm (dom q1)) | (dom q4)))) = q1 | ((rng ((Sgm (dom q1)) | (dom q3))) \/ (rng ((Sgm (dom q1)) | (dom q4)))) by RELAT_1:78
.= q1 | ((Sgm (dom q1)) .: ((dom q3) \/ (dom q4))) by A17, A18, RELAT_1:120
.= q1 | (rng ((Sgm (dom q1)) | (dom (Sgm (dom q1))))) by A20, RELAT_1:115
.= q1 | (rng (Sgm (dom q1)))
.= q1 | (dom q1) by FINSEQ_1:50
.= q1 ;
A22: q1 c= C1 by A3, XBOOLE_1:7;
A23: q1 | (rng ((Sgm (dom q1)) | (dom q3))) c= q1 by A21, XBOOLE_1:7;
A24: q1 | (rng ((Sgm (dom q1)) | (dom q4))) c= q1 by A21, XBOOLE_1:7;
rng C1 = (rng q1) \/ (rng q2) by A3, RELAT_1:12;
then A25: rng q1 c= rng C1 by XBOOLE_1:7;
A26: rng q1 = rng (Seq q1) by Lm6;
A27: rng (Seq q1) c= rng C1 by A25, Lm6;
A28: rng (Seq q1) = (rng q3) \/ (rng q4) by A7, A9, RELAT_1:12;
then A29: rng q3 c= rng (Seq q1) by XBOOLE_1:7;
rng q3 = rng (Seq q3) by Lm6;
then A30: rng (Seq q3) c= rng C1 by A27, A29, XBOOLE_1:1;
A31: rng q4 c= rng (Seq q1) by A28, XBOOLE_1:7;
rng q4 = rng (Seq q4) by Lm6;
then A32: rng (Seq q4) c= rng C1 by A27, A31, XBOOLE_1:1;
reconsider q5 = q1 | (rng ((Sgm (dom q1)) | (dom q3))), q6 = q1 | (rng ((Sgm (dom q1)) | (dom q4))) as FinSubsequence ;
reconsider fs = C1 as FinSequence of rng C1 by FINSEQ_1:def_4;
reconsider fs1 = Seq q1 as FinSequence of rng C1 by A25, A26, FINSEQ_1:def_4;
reconsider fs2 = Seq q3 as FinSequence of rng C1 by A30, FINSEQ_1:def_4;
reconsider fs3 = Seq q4 as FinSequence of rng C1 by A32, FINSEQ_1:def_4;
reconsider fss = q1, fss1 = q5, fss2 = q6 as Subset of fs by A22, A23, A24, XBOOLE_1:1;
reconsider fss3 = q3, fss4 = q4 as Subset of fs1 by A7, A9, XBOOLE_1:7;
A33: Seq fss3 = fs2 ;
fss1 = fss | (rng ((Sgm (dom fss)) | (dom fss3))) ;
then A34: Seq q3 = Seq q5 by A33, GRAPH_2:28;
A35: Seq fss4 = fs3 ;
A36: fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss4))) ;
q1 /\ q2 = {} by A4, XBOOLE_0:def_7;
then A37: (q5 /\ q2) \/ (q6 /\ q2) = {} by A21, XBOOLE_1:23;
then A38: q5 /\ q2 = {} ;
q6 /\ q2 = {} by A37;
then A39: q6 misses q2 by XBOOLE_0:def_7;
A40: q1 c= C1 by A3, XBOOLE_1:7;
A41: q2 c= C1 by A3, XBOOLE_1:7;
q6 c= q1 by A21, XBOOLE_1:7;
then q6 c= C1 by A40, XBOOLE_1:1;
then A42: dom q6 misses dom q2 by A39, A41, Th9;
then reconsider q7 = q6 \/ q2 as Function by GRFUNC_1:13;
A43: dom C1 = (dom q1) \/ (dom q2) by A3, RELAT_1:1
.= ((dom q5) \/ (dom q6)) \/ (dom q2) by A21, RELAT_1:1
.= (dom q5) \/ ((dom q6) \/ (dom q2)) by XBOOLE_1:4
.= (dom q5) \/ (dom q7) by RELAT_1:1 ;
then A44: dom q7 c= dom C1 by XBOOLE_1:7;
A45: dom C1 = Seg (len C1) by FINSEQ_1:def_3;
then reconsider q7 = q7 as FinSubsequence by A44, FINSEQ_1:def_12;
A46: C1 = q5 \/ q7 by A3, A21, XBOOLE_1:4;
A47: q5 /\ q7 = (q5 /\ q6) \/ (q5 /\ q2) by XBOOLE_1:23;
q5 /\ q6 = {} by A19, XBOOLE_0:def_7;
then A48: q5 misses q7 by A38, A47, XBOOLE_0:def_7;
A49: rng (Seq q7) = rng q7 by Lm6;
rng C1 = (rng q7) \/ (rng q5) by A46, RELAT_1:12;
then A50: rng (Seq q7) c= rng C1 by A49, XBOOLE_1:7;
rng C1 c= N by FINSEQ_1:def_4;
then rng (Seq q7) c= N by A50, XBOOLE_1:1;
then Seq q7 is FinSequence of N by FINSEQ_1:def_4;
then reconsider C3 = Seq q7 as firing-sequence of N by FINSEQ_1:def_11;
A51: dom (Seq q7) = Seg (len (Seq q7)) by FINSEQ_1:def_3;
A52: dom (q6 * (Sgm (dom q7))) c= dom (Sgm (dom q7)) by RELAT_1:25;
A53: dom (q2 * (Sgm (dom q7))) c= dom (Sgm (dom q7)) by RELAT_1:25;
A54: dom (q6 * (Sgm (dom q7))) c= dom (Seq q7) by A52, Lm5;
dom (q2 * (Sgm (dom q7))) c= dom (Seq q7) by A53, Lm5;
then reconsider q8 = q6 * (Sgm (dom q7)), q9 = q2 * (Sgm (dom q7)) as FinSubsequence by A51, A54, FINSEQ_1:def_12;
A55: C3 = q7 * (Sgm (dom q7)) by FINSEQ_1:def_14
.= q8 \/ q9 by RELAT_1:32 ;
A56: dom q8 = (Sgm (dom q7)) " (dom q6) by RELAT_1:147;
A57: dom q9 = (Sgm (dom q7)) " (dom q2) by RELAT_1:147;
(dom q2) /\ (dom q6) = {} by A42, XBOOLE_0:def_7;
then (Sgm (dom q7)) " ((dom q6) /\ (dom q2)) = {} ;
then ((Sgm (dom q7)) " (dom q6)) /\ ((Sgm (dom q7)) " (dom q2)) = {} by FUNCT_1:68;
then A58: (Sgm (dom q7)) " (dom q6) misses (Sgm (dom q7)) " (dom q2) by XBOOLE_0:def_7;
A59: dom q6 c= (dom q6) \/ (dom q2) by XBOOLE_1:7;
A60: dom q2 c= (dom q6) \/ (dom q2) by XBOOLE_1:7;
A61: dom q6 c= dom q7 by A59, RELAT_1:1;
A62: dom q2 c= dom q7 by A60, RELAT_1:1;
A63: dom q6 c= rng (Sgm (dom q7)) by A61, FINSEQ_1:50;
A64: dom q2 c= rng (Sgm (dom q7)) by A62, FINSEQ_1:50;
A65: dom q8 = (Sgm (dom q7)) " (dom q6) by RELAT_1:147;
A66: dom q9 = (Sgm (dom q7)) " (dom q2) by RELAT_1:147;
A67: rng ((Sgm (dom q7)) | (dom q8)) = rng ((dom q6) |` (Sgm (dom q7))) by A65, Th11
.= dom q6 by A63, RELAT_1:89 ;
A68: dom q8 c= dom (Sgm (dom q7)) by RELAT_1:25;
A69: dom q9 c= dom (Sgm (dom q7)) by RELAT_1:25;
A70: (Sgm (dom q7)) * (Sgm (dom q8)) = Sgm (rng ((Sgm (dom q7)) | (dom q8))) by A43, A45, A68, GRAPH_2:3, XBOOLE_1:7;
A71: Seq q8 = (q6 * (Sgm (dom q7))) * (Sgm (dom q8)) by FINSEQ_1:def_14
.= q6 * ((Sgm (dom q7)) * (Sgm (dom q8))) by RELAT_1:36
.= Seq q6 by A67, A70, FINSEQ_1:def_14 ;
A72: rng ((Sgm (dom q7)) | (dom q9)) = rng ((dom q2) |` (Sgm (dom q7))) by A66, Th11
.= dom q2 by A64, RELAT_1:89 ;
A73: (Sgm (dom q7)) * (Sgm (dom q9)) = Sgm (rng ((Sgm (dom q7)) | (dom q9))) by A43, A45, A69, GRAPH_2:3, XBOOLE_1:7;
A74: Seq q9 = (q2 * (Sgm (dom q7))) * (Sgm (dom q9)) by FINSEQ_1:def_14
.= q2 * ((Sgm (dom q7)) * (Sgm (dom q9))) by RELAT_1:36
.= Seq q2 by A72, A73, FINSEQ_1:def_14 ;
Seq q8 in R2 by A12, A35, A36, A71, GRAPH_2:28;
then ex ss1, ss2 being FinSubsequence st
( C3 = ss1 \/ ss2 & ss1 misses ss2 & Seq ss1 in R2 & Seq ss2 in R3 ) by A6, A55, A56, A57, A58, A74, Lm4;
then Seq q7 in R2 concur R3 ;
hence x in R1 concur (R2 concur R3) by A1, A11, A34, A46, A48; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R1 concur (R2 concur R3) or x in (R1 concur R2) concur R3 )
assume x in R1 concur (R2 concur R3) ; ::_thesis: x in (R1 concur R2) concur R3
then consider C1 being firing-sequence of N such that
A75: x = C1 and
A76: ex q1, q2 being FinSubsequence st
( C1 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 concur R3 ) ;
consider q1, q2 being FinSubsequence such that
A77: C1 = q1 \/ q2 and
A78: q1 misses q2 and
A79: Seq q1 in R1 and
A80: Seq q2 in R2 concur R3 by A76;
consider C2 being firing-sequence of N such that
A81: Seq q2 = C2 and
A82: ex q3, q4 being FinSubsequence st
( C2 = q3 \/ q4 & q3 misses q4 & Seq q3 in R2 & Seq q4 in R3 ) by A80;
consider q3, q4 being FinSubsequence such that
A83: C2 = q3 \/ q4 and
A84: q3 misses q4 and
A85: Seq q3 in R2 and
A86: Seq q4 in R3 by A82;
consider n1 being Nat such that
A87: dom q2 c= Seg n1 by FINSEQ_1:def_12;
A88: q3 c= Seq q2 by A81, A83, XBOOLE_1:7;
A89: q4 c= Seq q2 by A81, A83, XBOOLE_1:7;
Sgm (dom q2) is one-to-one by A87, FINSEQ_3:92;
then A90: (Sgm (dom q2)) .: (dom q3) misses (Sgm (dom q2)) .: (dom q4) by A84, A88, A89, Th9, FUNCT_1:66;
A91: rng ((Sgm (dom q2)) | (dom q3)) = (Sgm (dom q2)) .: (dom q3) by RELAT_1:115;
A92: rng ((Sgm (dom q2)) | (dom q4)) = (Sgm (dom q2)) .: (dom q4) by RELAT_1:115;
then A93: q2 | (rng ((Sgm (dom q2)) | (dom q3))) misses q2 | (rng ((Sgm (dom q2)) | (dom q4))) by A90, A91, Th8;
A94: dom (Sgm (dom q2)) = dom (Seq q2) by Lm5
.= (dom q3) \/ (dom q4) by A81, A83, RELAT_1:1 ;
A95: (q2 | (rng ((Sgm (dom q2)) | (dom q3)))) \/ (q2 | (rng ((Sgm (dom q2)) | (dom q4)))) = q2 | ((rng ((Sgm (dom q2)) | (dom q3))) \/ (rng ((Sgm (dom q2)) | (dom q4)))) by RELAT_1:78
.= q2 | ((Sgm (dom q2)) .: ((dom q3) \/ (dom q4))) by A91, A92, RELAT_1:120
.= q2 | (rng ((Sgm (dom q2)) | (dom (Sgm (dom q2))))) by A94, RELAT_1:115
.= q2 | (rng (Sgm (dom q2)))
.= q2 | (dom q2) by FINSEQ_1:50
.= q2 ;
A96: q2 c= C1 by A77, XBOOLE_1:7;
A97: q2 | (rng ((Sgm (dom q2)) | (dom q3))) c= q2 by A95, XBOOLE_1:7;
A98: q2 | (rng ((Sgm (dom q2)) | (dom q4))) c= q2 by A95, XBOOLE_1:7;
rng C1 = (rng q1) \/ (rng q2) by A77, RELAT_1:12;
then A99: rng q2 c= rng C1 by XBOOLE_1:7;
A100: rng q2 = rng (Seq q2) by Lm6;
A101: rng (Seq q2) c= rng C1 by A99, Lm6;
A102: rng (Seq q2) = (rng q3) \/ (rng q4) by A81, A83, RELAT_1:12;
then A103: rng q3 c= rng (Seq q2) by XBOOLE_1:7;
rng q3 = rng (Seq q3) by Lm6;
then A104: rng (Seq q3) c= rng C1 by A101, A103, XBOOLE_1:1;
A105: rng q4 c= rng (Seq q2) by A102, XBOOLE_1:7;
rng q4 = rng (Seq q4) by Lm6;
then A106: rng (Seq q4) c= rng C1 by A101, A105, XBOOLE_1:1;
reconsider q5 = q2 | (rng ((Sgm (dom q2)) | (dom q3))), q6 = q2 | (rng ((Sgm (dom q2)) | (dom q4))) as FinSubsequence ;
reconsider fs = C1 as FinSequence of rng C1 by FINSEQ_1:def_4;
reconsider fs1 = Seq q2 as FinSequence of rng C1 by A99, A100, FINSEQ_1:def_4;
reconsider fs2 = Seq q3 as FinSequence of rng C1 by A104, FINSEQ_1:def_4;
reconsider fs3 = Seq q4 as FinSequence of rng C1 by A106, FINSEQ_1:def_4;
reconsider fss = q2, fss1 = q5, fss2 = q6 as Subset of fs by A96, A97, A98, XBOOLE_1:1;
reconsider fss3 = q3, fss4 = q4 as Subset of fs1 by A81, A83, XBOOLE_1:7;
A107: Seq fss3 = fs2 ;
A108: fss1 = fss | (rng ((Sgm (dom fss)) | (dom fss3))) ;
A109: Seq fss4 = fs3 ;
fss2 = fss | (rng ((Sgm (dom fss)) | (dom fss4))) ;
then A110: Seq q4 = Seq q6 by A109, GRAPH_2:28;
q1 /\ q2 = {} by A78, XBOOLE_0:def_7;
then A111: (q1 /\ q5) \/ (q1 /\ q6) = {} by A95, XBOOLE_1:23;
then A112: q1 /\ q5 = {} ;
A113: q1 /\ q6 = {} by A111;
A114: q1 misses q5 by A112, XBOOLE_0:def_7;
A115: q1 c= C1 by A77, XBOOLE_1:7;
A116: q2 c= C1 by A77, XBOOLE_1:7;
q5 c= q2 by A95, XBOOLE_1:7;
then q5 c= C1 by A116, XBOOLE_1:1;
then A117: dom q1 misses dom q5 by A114, A115, Th9;
then reconsider q7 = q1 \/ q5 as Function by GRFUNC_1:13;
A118: dom C1 = (dom q1) \/ (dom q2) by A77, RELAT_1:1
.= (dom q1) \/ ((dom q5) \/ (dom q6)) by A95, RELAT_1:1
.= ((dom q1) \/ (dom q5)) \/ (dom q6) by XBOOLE_1:4
.= (dom q7) \/ (dom q6) by RELAT_1:1 ;
then A119: dom q7 c= dom C1 by XBOOLE_1:7;
A120: dom C1 = Seg (len C1) by FINSEQ_1:def_3;
then reconsider q7 = q7 as FinSubsequence by A119, FINSEQ_1:def_12;
A121: C1 = q7 \/ q6 by A77, A95, XBOOLE_1:4;
A122: q7 /\ q6 = (q1 /\ q6) \/ (q5 /\ q6) by XBOOLE_1:23;
q5 /\ q6 = {} by A93, XBOOLE_0:def_7;
then A123: q7 misses q6 by A113, A122, XBOOLE_0:def_7;
A124: rng (Seq q7) = rng q7 by Lm6;
rng C1 = (rng q7) \/ (rng q6) by A121, RELAT_1:12;
then A125: rng (Seq q7) c= rng C1 by A124, XBOOLE_1:7;
rng C1 c= N by FINSEQ_1:def_4;
then rng (Seq q7) c= N by A125, XBOOLE_1:1;
then Seq q7 is FinSequence of N by FINSEQ_1:def_4;
then reconsider C3 = Seq q7 as firing-sequence of N by FINSEQ_1:def_11;
A126: dom (Seq q7) = Seg (len (Seq q7)) by FINSEQ_1:def_3;
A127: dom (q1 * (Sgm (dom q7))) c= dom (Sgm (dom q7)) by RELAT_1:25;
A128: dom (q5 * (Sgm (dom q7))) c= dom (Sgm (dom q7)) by RELAT_1:25;
A129: dom (q1 * (Sgm (dom q7))) c= dom (Seq q7) by A127, Lm5;
dom (q5 * (Sgm (dom q7))) c= dom (Seq q7) by A128, Lm5;
then reconsider q8 = q1 * (Sgm (dom q7)), q9 = q5 * (Sgm (dom q7)) as FinSubsequence by A126, A129, FINSEQ_1:def_12;
A130: C3 = q7 * (Sgm (dom q7)) by FINSEQ_1:def_14
.= q8 \/ q9 by RELAT_1:32 ;
A131: dom q8 = (Sgm (dom q7)) " (dom q1) by RELAT_1:147;
A132: dom q9 = (Sgm (dom q7)) " (dom q5) by RELAT_1:147;
(dom q1) /\ (dom q5) = {} by A117, XBOOLE_0:def_7;
then (Sgm (dom q7)) " ((dom q1) /\ (dom q5)) = {} ;
then ((Sgm (dom q7)) " (dom q1)) /\ ((Sgm (dom q7)) " (dom q5)) = {} by FUNCT_1:68;
then A133: (Sgm (dom q7)) " (dom q1) misses (Sgm (dom q7)) " (dom q5) by XBOOLE_0:def_7;
A134: dom q1 c= (dom q1) \/ (dom q5) by XBOOLE_1:7;
A135: dom q5 c= (dom q1) \/ (dom q5) by XBOOLE_1:7;
A136: dom q1 c= dom q7 by A134, RELAT_1:1;
A137: dom q5 c= dom q7 by A135, RELAT_1:1;
A138: dom q1 c= rng (Sgm (dom q7)) by A136, FINSEQ_1:50;
A139: dom q5 c= rng (Sgm (dom q7)) by A137, FINSEQ_1:50;
A140: dom q8 = (Sgm (dom q7)) " (dom q1) by RELAT_1:147;
A141: dom q9 = (Sgm (dom q7)) " (dom q5) by RELAT_1:147;
A142: rng ((Sgm (dom q7)) | (dom q8)) = rng ((dom q1) |` (Sgm (dom q7))) by A140, Th11
.= dom q1 by A138, RELAT_1:89 ;
A143: dom q8 c= dom (Sgm (dom q7)) by RELAT_1:25;
A144: dom q9 c= dom (Sgm (dom q7)) by RELAT_1:25;
A145: (Sgm (dom q7)) * (Sgm (dom q8)) = Sgm (rng ((Sgm (dom q7)) | (dom q8))) by A118, A120, A143, GRAPH_2:3, XBOOLE_1:7;
A146: Seq q8 = (q1 * (Sgm (dom q7))) * (Sgm (dom q8)) by FINSEQ_1:def_14
.= q1 * ((Sgm (dom q7)) * (Sgm (dom q8))) by RELAT_1:36
.= Seq q1 by A142, A145, FINSEQ_1:def_14 ;
A147: rng ((Sgm (dom q7)) | (dom q9)) = rng ((dom q5) |` (Sgm (dom q7))) by A141, Th11
.= dom q5 by A139, RELAT_1:89 ;
A148: (Sgm (dom q7)) * (Sgm (dom q9)) = Sgm (rng ((Sgm (dom q7)) | (dom q9))) by A118, A120, A144, GRAPH_2:3, XBOOLE_1:7;
Seq q9 = (q5 * (Sgm (dom q7))) * (Sgm (dom q9)) by FINSEQ_1:def_14
.= q5 * ((Sgm (dom q7)) * (Sgm (dom q9))) by RELAT_1:36
.= Seq q5 by A147, A148, FINSEQ_1:def_14 ;
then Seq q9 in R2 by A85, A107, A108, GRAPH_2:28;
then ex ss1, ss2 being FinSubsequence st
( C3 = ss1 \/ ss2 & ss1 misses ss2 & Seq ss1 in R1 & Seq ss2 in R2 ) by A79, A130, A131, A132, A133, A146, Lm4;
then Seq q7 in R1 concur R2 ;
hence x in (R1 concur R2) concur R3 by A75, A86, A110, A121, A123; ::_thesis: verum
end;
theorem :: PNPROC_1:64
for P being set
for N being Petri_net of P
for R1, R2 being process of N holds R1 before R2 c= R1 concur R2
proof
let P be set ; ::_thesis: for N being Petri_net of P
for R1, R2 being process of N holds R1 before R2 c= R1 concur R2
let N be Petri_net of P; ::_thesis: for R1, R2 being process of N holds R1 before R2 c= R1 concur R2
let R1, R2 be process of N; ::_thesis: R1 before R2 c= R1 concur R2
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R1 before R2 or x in R1 concur R2 )
assume A1: x in R1 before R2 ; ::_thesis: x in R1 concur R2
then reconsider C = x as firing-sequence of N ;
consider C1, C2 being firing-sequence of N such that
A2: x = C1 ^ C2 and
A3: C1 in R1 and
A4: C2 in R2 by A1;
set q1 = C1;
set q2 = (len C1) Shift C2;
reconsider q1 = C1 as FinSequence ;
A5: C = q1 \/ ((len C1) Shift C2) by A2, Th61;
A6: q1 misses (len C1) Shift C2 by Th62;
A7: Seq q1 in R1 by A3, FINSEQ_3:116;
Seq ((len C1) Shift C2) in R2 by A4, Th58;
hence x in R1 concur R2 by A5, A6, A7; ::_thesis: verum
end;
theorem :: PNPROC_1:65
for P being set
for N being Petri_net of P
for R1, P1, R2, P2 being process of N st R1 c= P1 & R2 c= P2 holds
R1 before R2 c= P1 before P2
proof
let P be set ; ::_thesis: for N being Petri_net of P
for R1, P1, R2, P2 being process of N st R1 c= P1 & R2 c= P2 holds
R1 before R2 c= P1 before P2
let N be Petri_net of P; ::_thesis: for R1, P1, R2, P2 being process of N st R1 c= P1 & R2 c= P2 holds
R1 before R2 c= P1 before P2
let R1, P1, R2, P2 be process of N; ::_thesis: ( R1 c= P1 & R2 c= P2 implies R1 before R2 c= P1 before P2 )
assume that
A1: R1 c= P1 and
A2: R2 c= P2 ; ::_thesis: R1 before R2 c= P1 before P2
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R1 before R2 or x in P1 before P2 )
assume x in R1 before R2 ; ::_thesis: x in P1 before P2
then ex C1, C2 being firing-sequence of N st
( x = C1 ^ C2 & C1 in R1 & C2 in R2 ) ;
hence x in P1 before P2 by A1, A2; ::_thesis: verum
end;
theorem :: PNPROC_1:66
for P being set
for N being Petri_net of P
for R1, P1, R2, P2 being process of N st R1 c= P1 & R2 c= P2 holds
R1 concur R2 c= P1 concur P2
proof
let P be set ; ::_thesis: for N being Petri_net of P
for R1, P1, R2, P2 being process of N st R1 c= P1 & R2 c= P2 holds
R1 concur R2 c= P1 concur P2
let N be Petri_net of P; ::_thesis: for R1, P1, R2, P2 being process of N st R1 c= P1 & R2 c= P2 holds
R1 concur R2 c= P1 concur P2
let R1, P1, R2, P2 be process of N; ::_thesis: ( R1 c= P1 & R2 c= P2 implies R1 concur R2 c= P1 concur P2 )
assume that
A1: R1 c= P1 and
A2: R2 c= P2 ; ::_thesis: R1 concur R2 c= P1 concur P2
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R1 concur R2 or x in P1 concur P2 )
assume x in R1 concur R2 ; ::_thesis: x in P1 concur P2
then ex C being firing-sequence of N st
( x = C & ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) ) ;
hence x in P1 concur P2 by A1, A2; ::_thesis: verum
end;
Lm9: for p1, p2 being FinSequence
for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
dom (q1 \/ ((len p1) Shift q2)) c= dom (p1 ^ p2)
proof
let p1, p2 be FinSequence; ::_thesis: for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
dom (q1 \/ ((len p1) Shift q2)) c= dom (p1 ^ p2)
let q1, q2 be FinSubsequence; ::_thesis: ( q1 c= p1 & q2 c= p2 implies dom (q1 \/ ((len p1) Shift q2)) c= dom (p1 ^ p2) )
assume that
A1: q1 c= p1 and
A2: q2 c= p2 ; ::_thesis: dom (q1 \/ ((len p1) Shift q2)) c= dom (p1 ^ p2)
A3: dom q1 c= dom p1 by A1, GRFUNC_1:2;
A4: dom q2 c= dom p2 by A2, GRFUNC_1:2;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (q1 \/ ((len p1) Shift q2)) or x in dom (p1 ^ p2) )
assume x in dom (q1 \/ ((len p1) Shift q2)) ; ::_thesis: x in dom (p1 ^ p2)
then A5: x in (dom q1) \/ (dom ((len p1) Shift q2)) by RELAT_1:1;
A6: dom (p1 ^ p2) = Seg ((len p1) + (len p2)) by FINSEQ_1:def_7;
A7: now__::_thesis:_(_x_in_dom_q1_implies_x_in_dom_(p1_^_p2)_)
assume A8: x in dom q1 ; ::_thesis: x in dom (p1 ^ p2)
A9: dom p1 = Seg (len p1) by FINSEQ_1:def_3;
len p1 <= (len p1) + (len p2) by INT_1:6;
then Seg (len p1) c= Seg ((len p1) + (len p2)) by FINSEQ_1:5;
hence x in dom (p1 ^ p2) by A3, A6, A8, A9, TARSKI:def_3; ::_thesis: verum
end;
now__::_thesis:_(_x_in_dom_((len_p1)_Shift_q2)_implies_x_in_dom_(p1_^_p2)_)
assume A10: x in dom ((len p1) Shift q2) ; ::_thesis: x in dom (p1 ^ p2)
A11: dom ((len p1) Shift q2) c= dom ((len p1) Shift p2)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom ((len p1) Shift q2) or x in dom ((len p1) Shift p2) )
assume A12: x in dom ((len p1) Shift q2) ; ::_thesis: x in dom ((len p1) Shift p2)
A13: dom ((len p1) Shift p2) = { ((len p1) + k) where k is Element of NAT : k in dom p2 } by Def14;
dom ((len p1) Shift q2) = { ((len p1) + k) where k is Element of NAT : k in dom q2 } by Def14;
then ex k being Element of NAT st
( x = (len p1) + k & k in dom q2 ) by A12;
hence x in dom ((len p1) Shift p2) by A4, A13; ::_thesis: verum
end;
dom (p1 ^ p2) = dom (p1 \/ ((len p1) Shift p2)) by Th61
.= (dom p1) \/ (dom ((len p1) Shift p2)) by RELAT_1:1 ;
then dom ((len p1) Shift p2) c= dom (p1 ^ p2) by XBOOLE_1:7;
then dom ((len p1) Shift q2) c= dom (p1 ^ p2) by A11, XBOOLE_1:1;
hence x in dom (p1 ^ p2) by A10; ::_thesis: verum
end;
hence x in dom (p1 ^ p2) by A5, A7, XBOOLE_0:def_3; ::_thesis: verum
end;
Lm10: for p1 being FinSequence
for q1, q2 being FinSubsequence st q1 c= p1 holds
q1 misses (len p1) Shift q2
by Th62, XBOOLE_1:63;
Lm11: for i being Element of NAT
for p, q being FinSubsequence st q c= p holds
dom (i Shift q) c= dom (i Shift p)
proof
let i be Element of NAT ; ::_thesis: for p, q being FinSubsequence st q c= p holds
dom (i Shift q) c= dom (i Shift p)
let p, q be FinSubsequence; ::_thesis: ( q c= p implies dom (i Shift q) c= dom (i Shift p) )
assume A1: q c= p ; ::_thesis: dom (i Shift q) c= dom (i Shift p)
A2: dom (i Shift q) = { (i + k) where k is Element of NAT : k in dom q } by Def14;
A3: dom (i Shift p) = { (i + k) where k is Element of NAT : k in dom p } by Def14;
A4: dom q c= dom p by A1, GRFUNC_1:2;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (i Shift q) or x in dom (i Shift p) )
assume x in dom (i Shift q) ; ::_thesis: x in dom (i Shift p)
then ex k1 being Element of NAT st
( x = i + k1 & k1 in dom q ) by A2;
hence x in dom (i Shift p) by A3, A4; ::_thesis: verum
end;
theorem Th67: :: PNPROC_1:67
for i being Element of NAT
for p, q being FinSubsequence st q c= p holds
i Shift q c= i Shift p
proof
let i be Element of NAT ; ::_thesis: for p, q being FinSubsequence st q c= p holds
i Shift q c= i Shift p
let p, q be FinSubsequence; ::_thesis: ( q c= p implies i Shift q c= i Shift p )
assume A1: q c= p ; ::_thesis: i Shift q c= i Shift p
A2: dom (i Shift q) = { (i + k) where k is Element of NAT : k in dom q } by Def14;
A3: dom (i Shift p) = { (i + k) where k is Element of NAT : k in dom p } by Def14;
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in i Shift q or [x,b1] in i Shift p )
let y be set ; ::_thesis: ( not [x,y] in i Shift q or [x,y] in i Shift p )
assume A4: [x,y] in i Shift q ; ::_thesis: [x,y] in i Shift p
then A5: x in dom (i Shift q) by FUNCT_1:1;
A6: y = (i Shift q) . x by A4, FUNCT_1:1;
consider k being Element of NAT such that
A7: x = i + k and
A8: k in dom q by A2, A5;
A9: dom q c= dom p by A1, GRFUNC_1:2;
then A10: x in dom (i Shift p) by A3, A7, A8;
y = q . k by A6, A7, A8, Def14
.= p . k by A1, A8, GRFUNC_1:2
.= (i Shift p) . x by A7, A8, A9, Def14 ;
hence [x,y] in i Shift p by A10, FUNCT_1:1; ::_thesis: verum
end;
theorem Th68: :: PNPROC_1:68
for p1, p2 being FinSequence holds (len p1) Shift p2 c= p1 ^ p2
proof
let p1, p2 be FinSequence; ::_thesis: (len p1) Shift p2 c= p1 ^ p2
A1: dom ((len p1) Shift p2) = { ((len p1) + k) where k is Element of NAT : k in dom p2 } by Def14;
A2: dom ((len p1) Shift p2) = { k where k is Element of NAT : ( (len p1) + 1 <= k & k <= (len p1) + (len p2) ) } by Th51;
A3: dom (p1 ^ p2) = Seg ((len p1) + (len p2)) by FINSEQ_1:def_7
.= { k where k is Element of NAT : ( 1 <= k & k <= (len p1) + (len p2) ) } by FINSEQ_1:def_1 ;
let x be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [x,b1] in (len p1) Shift p2 or [x,b1] in p1 ^ p2 )
let y be set ; ::_thesis: ( not [x,y] in (len p1) Shift p2 or [x,y] in p1 ^ p2 )
assume A4: [x,y] in (len p1) Shift p2 ; ::_thesis: [x,y] in p1 ^ p2
then A5: x in dom ((len p1) Shift p2) by FUNCT_1:1;
A6: y = ((len p1) Shift p2) . x by A4, FUNCT_1:1;
consider k being Element of NAT such that
A7: x = k and
A8: (len p1) + 1 <= k and
A9: k <= (len p1) + (len p2) by A2, A5;
1 <= (len p1) + 1 by INT_1:6;
then 1 <= k by A8, XXREAL_0:2;
then A10: x in dom (p1 ^ p2) by A3, A7, A9;
consider j being Element of NAT such that
A11: x = (len p1) + j and
A12: j in dom p2 by A1, A5;
y = p2 . j by A6, A11, A12, Def14
.= (p1 ^ p2) . x by A11, A12, FINSEQ_1:def_7 ;
hence [x,y] in p1 ^ p2 by A10, FUNCT_1:1; ::_thesis: verum
end;
theorem Th69: :: PNPROC_1:69
for i being Element of NAT
for q1, q2 being FinSubsequence st dom q1 misses dom q2 holds
dom (i Shift q1) misses dom (i Shift q2)
proof
let i be Element of NAT ; ::_thesis: for q1, q2 being FinSubsequence st dom q1 misses dom q2 holds
dom (i Shift q1) misses dom (i Shift q2)
let q1, q2 be FinSubsequence; ::_thesis: ( dom q1 misses dom q2 implies dom (i Shift q1) misses dom (i Shift q2) )
assume A1: dom q1 misses dom q2 ; ::_thesis: dom (i Shift q1) misses dom (i Shift q2)
A2: dom (i Shift q1) = { (i + k) where k is Element of NAT : k in dom q1 } by Def14;
A3: dom (i Shift q2) = { (i + k) where k is Element of NAT : k in dom q2 } by Def14;
now__::_thesis:_for_x_being_set_holds_not_x_in_(dom_(i_Shift_q1))_/\_(dom_(i_Shift_q2))
given x being set such that A4: x in (dom (i Shift q1)) /\ (dom (i Shift q2)) ; ::_thesis: contradiction
A5: x in dom (i Shift q1) by A4, XBOOLE_0:def_4;
A6: x in dom (i Shift q2) by A4, XBOOLE_0:def_4;
A7: ex k1 being Element of NAT st
( x = i + k1 & k1 in dom q1 ) by A2, A5;
consider k2 being Element of NAT such that
A8: x = i + k2 and
A9: k2 in dom q2 by A3, A6;
k2 in (dom q1) /\ (dom q2) by A7, A8, A9, XBOOLE_0:def_4;
hence contradiction by A1, XBOOLE_0:def_7; ::_thesis: verum
end;
hence (dom (i Shift q1)) /\ (dom (i Shift q2)) = {} by XBOOLE_0:def_1; :: according to XBOOLE_0:def_7 ::_thesis: verum
end;
theorem Th70: :: PNPROC_1:70
for i being Element of NAT
for q, q1, q2 being FinSubsequence st q = q1 \/ q2 & q1 misses q2 holds
(i Shift q1) \/ (i Shift q2) = i Shift q
proof
let i be Element of NAT ; ::_thesis: for q, q1, q2 being FinSubsequence st q = q1 \/ q2 & q1 misses q2 holds
(i Shift q1) \/ (i Shift q2) = i Shift q
let q, q1, q2 be FinSubsequence; ::_thesis: ( q = q1 \/ q2 & q1 misses q2 implies (i Shift q1) \/ (i Shift q2) = i Shift q )
assume that
A1: q = q1 \/ q2 and
A2: q1 misses q2 ; ::_thesis: (i Shift q1) \/ (i Shift q2) = i Shift q
A3: dom (i Shift q) = { (i + k) where k is Element of NAT : k in dom q } by Def14;
A4: dom (i Shift q1) = { (i + k) where k is Element of NAT : k in dom q1 } by Def14;
A5: dom (i Shift q2) = { (i + k) where k is Element of NAT : k in dom q2 } by Def14;
A6: q1 c= q by A1, XBOOLE_1:7;
A7: q2 c= q by A1, XBOOLE_1:7;
A8: i Shift q1 c= i Shift q by A1, Th67, XBOOLE_1:7;
A9: i Shift q2 c= i Shift q by A1, Th67, XBOOLE_1:7;
dom q1 misses dom q2 by A2, A6, A7, Th9;
then dom (i Shift q1) misses dom (i Shift q2) by Th69;
then reconsider q3 = (i Shift q1) \/ (i Shift q2) as Function by GRFUNC_1:13;
let x be set ; :: according to RELAT_1:def_2 ::_thesis: for b1 being set holds
( ( not [x,b1] in (i Shift q1) \/ (i Shift q2) or [x,b1] in i Shift q ) & ( not [x,b1] in i Shift q or [x,b1] in (i Shift q1) \/ (i Shift q2) ) )
let y be set ; ::_thesis: ( ( not [x,y] in (i Shift q1) \/ (i Shift q2) or [x,y] in i Shift q ) & ( not [x,y] in i Shift q or [x,y] in (i Shift q1) \/ (i Shift q2) ) )
thus ( [x,y] in (i Shift q1) \/ (i Shift q2) implies [x,y] in i Shift q ) ::_thesis: ( not [x,y] in i Shift q or [x,y] in (i Shift q1) \/ (i Shift q2) )
proof
assume A10: [x,y] in (i Shift q1) \/ (i Shift q2) ; ::_thesis: [x,y] in i Shift q
then x in dom q3 by FUNCT_1:1;
then A11: x in (dom (i Shift q1)) \/ (dom (i Shift q2)) by RELAT_1:1;
A12: now__::_thesis:_(_x_in_dom_(i_Shift_q1)_implies_(_x_in_dom_(i_Shift_q)_&_y_=_(i_Shift_q)_._x_)_)
assume A13: x in dom (i Shift q1) ; ::_thesis: ( x in dom (i Shift q) & y = (i Shift q) . x )
A14: dom (i Shift q1) c= dom (i Shift q) by A8, GRFUNC_1:2;
(i Shift q1) . x = (i Shift q) . x by A8, A13, GRFUNC_1:2;
then [x,((i Shift q) . x)] in i Shift q1 by A13, FUNCT_1:def_2;
then [x,((i Shift q) . x)] in q3 by XBOOLE_0:def_3;
hence ( x in dom (i Shift q) & y = (i Shift q) . x ) by A10, A13, A14, FUNCT_1:def_1; ::_thesis: verum
end;
now__::_thesis:_(_x_in_dom_(i_Shift_q2)_implies_(_x_in_dom_(i_Shift_q)_&_y_=_(i_Shift_q)_._x_)_)
assume A15: x in dom (i Shift q2) ; ::_thesis: ( x in dom (i Shift q) & y = (i Shift q) . x )
A16: dom (i Shift q2) c= dom (i Shift q) by A9, GRFUNC_1:2;
(i Shift q2) . x = (i Shift q) . x by A9, A15, GRFUNC_1:2;
then [x,((i Shift q) . x)] in i Shift q2 by A15, FUNCT_1:def_2;
then [x,((i Shift q) . x)] in q3 by XBOOLE_0:def_3;
hence ( x in dom (i Shift q) & y = (i Shift q) . x ) by A10, A15, A16, FUNCT_1:def_1; ::_thesis: verum
end;
hence [x,y] in i Shift q by A11, A12, FUNCT_1:1, XBOOLE_0:def_3; ::_thesis: verum
end;
assume A17: [x,y] in i Shift q ; ::_thesis: [x,y] in (i Shift q1) \/ (i Shift q2)
then A18: x in dom (i Shift q) by FUNCT_1:1;
A19: y = (i Shift q) . x by A17, FUNCT_1:1;
consider k being Element of NAT such that
A20: x = i + k and
A21: k in dom q by A3, A18;
dom q = (dom q1) \/ (dom q2) by A1, RELAT_1:1;
then A22: ( k in dom q1 or k in dom q2 ) by A21, XBOOLE_0:def_3;
then ( x in dom (i Shift q1) or x in dom (i Shift q2) ) by A4, A5, A20;
then x in (dom (i Shift q1)) \/ (dom (i Shift q2)) by XBOOLE_0:def_3;
then A23: x in dom q3 by RELAT_1:1;
A24: now__::_thesis:_(_x_in_dom_(i_Shift_q1)_implies_y_=_q3_._x_)
assume A25: x in dom (i Shift q1) ; ::_thesis: y = q3 . x
then A26: ex k1 being Element of NAT st
( x = i + k1 & k1 in dom q1 ) by A4;
thus y = q . k by A19, A20, A21, Def14
.= q1 . k by A1, A20, A26, GRFUNC_1:15
.= (i Shift q1) . x by A20, A26, Def14
.= q3 . x by A25, GRFUNC_1:15 ; ::_thesis: verum
end;
now__::_thesis:_(_x_in_dom_(i_Shift_q2)_implies_y_=_q3_._x_)
assume A27: x in dom (i Shift q2) ; ::_thesis: y = q3 . x
then A28: ex k2 being Element of NAT st
( x = i + k2 & k2 in dom q2 ) by A5;
thus y = q . k by A19, A20, A21, Def14
.= q2 . k by A1, A20, A28, GRFUNC_1:15
.= (i Shift q2) . x by A20, A28, Def14
.= q3 . x by A27, GRFUNC_1:15 ; ::_thesis: verum
end;
hence [x,y] in (i Shift q1) \/ (i Shift q2) by A4, A5, A20, A22, A23, A24, FUNCT_1:1; ::_thesis: verum
end;
theorem Th71: :: PNPROC_1:71
for i being Element of NAT
for q being FinSubsequence holds dom (Seq q) = dom (Seq (i Shift q))
proof
let i be Element of NAT ; ::_thesis: for q being FinSubsequence holds dom (Seq q) = dom (Seq (i Shift q))
let q be FinSubsequence; ::_thesis: dom (Seq q) = dom (Seq (i Shift q))
A1: card q = card (i Shift q) by Th54;
A2: len (Seq q) = card q by Th7;
A3: len (Seq (i Shift q)) = card (i Shift q) by Th7;
thus dom (Seq q) = Seg (len (Seq q)) by FINSEQ_1:def_3
.= dom (Seq (i Shift q)) by A1, A2, A3, FINSEQ_1:def_3 ; ::_thesis: verum
end;
theorem Th72: :: PNPROC_1:72
for k, i being Element of NAT
for q being FinSubsequence st k in dom (Seq q) holds
ex j being Element of NAT st
( j = (Sgm (dom q)) . k & (Sgm (dom (i Shift q))) . k = i + j )
proof
let k, i be Element of NAT ; ::_thesis: for q being FinSubsequence st k in dom (Seq q) holds
ex j being Element of NAT st
( j = (Sgm (dom q)) . k & (Sgm (dom (i Shift q))) . k = i + j )
let q be FinSubsequence; ::_thesis: ( k in dom (Seq q) implies ex j being Element of NAT st
( j = (Sgm (dom q)) . k & (Sgm (dom (i Shift q))) . k = i + j ) )
assume A1: k in dom (Seq q) ; ::_thesis: ex j being Element of NAT st
( j = (Sgm (dom q)) . k & (Sgm (dom (i Shift q))) . k = i + j )
consider ss being FinSubsequence such that
A2: dom ss = dom q and
A3: rng ss = dom (i Shift q) and
A4: for l being Element of NAT st l in dom q holds
ss . l = i + l and
ss is one-to-one by Th53;
A5: rng (Seq ss) = dom (i Shift q) by A3, Lm6;
A6: rng (Sgm (dom q)) = dom q by FINSEQ_1:50;
A7: dom (Seq q) = dom (q * (Sgm (dom q))) by FINSEQ_1:def_14
.= dom (Sgm (dom q)) by A6, RELAT_1:27 ;
A8: for l1 being Element of NAT st l1 in dom (Seq q) holds
ex j1 being Element of NAT st
( j1 = (Sgm (dom q)) . l1 & (Seq ss) . l1 = i + j1 )
proof
let l1 be Element of NAT ; ::_thesis: ( l1 in dom (Seq q) implies ex j1 being Element of NAT st
( j1 = (Sgm (dom q)) . l1 & (Seq ss) . l1 = i + j1 ) )
assume A9: l1 in dom (Seq q) ; ::_thesis: ex j1 being Element of NAT st
( j1 = (Sgm (dom q)) . l1 & (Seq ss) . l1 = i + j1 )
A10: (Sgm (dom q)) . l1 in rng (Sgm (dom q)) by A7, A9, FUNCT_1:def_3;
then A11: (Sgm (dom q)) . l1 in dom q by FINSEQ_1:50;
rng (Sgm (dom q)) c= NAT by FINSEQ_1:def_4;
then reconsider j1 = (Sgm (dom q)) . l1 as Element of NAT by A10;
(Seq ss) . l1 = (ss * (Sgm (dom ss))) . l1 by FINSEQ_1:def_14
.= ss . j1 by A2, A7, A9, FUNCT_1:13
.= i + j1 by A4, A11 ;
hence ex j1 being Element of NAT st
( j1 = (Sgm (dom q)) . l1 & (Seq ss) . l1 = i + j1 ) ; ::_thesis: verum
end;
A12: rng ss = rng (Sgm (dom (i Shift q))) by A3, FINSEQ_1:50;
rng (Sgm (dom (i Shift q))) c= NAT by FINSEQ_1:def_4;
then rng (Seq ss) c= NAT by A12, Lm6;
then reconsider fs = Seq ss as FinSequence of NAT by FINSEQ_1:def_4;
A13: ex l2 being Nat st dom (i Shift q) c= Seg l2 by FINSEQ_1:def_12;
A14: dom (Seq ss) = dom (ss * (Sgm (dom ss))) by FINSEQ_1:def_14
.= dom (Sgm (dom q)) by A2, A6, RELAT_1:27 ;
for n, m, k1, k2 being Nat st 1 <= n & n < m & m <= len fs & k1 = fs . n & k2 = fs . m holds
k1 < k2
proof
let n, m, k1, k2 be Nat; ::_thesis: ( 1 <= n & n < m & m <= len fs & k1 = fs . n & k2 = fs . m implies k1 < k2 )
assume that
A15: 1 <= n and
A16: n < m and
A17: m <= len fs and
A18: k1 = fs . n and
A19: k2 = fs . m ; ::_thesis: k1 < k2
reconsider n = n, m = m as Element of NAT by ORDINAL1:def_12;
A20: dom fs = Seg (len fs) by FINSEQ_1:def_3
.= { l3 where l3 is Element of NAT : ( 1 <= l3 & l3 <= len fs ) } by FINSEQ_1:def_1 ;
n + 1 <= m by A16, INT_1:7;
then n + 1 <= len fs by A17, XXREAL_0:2;
then A21: n <= (len fs) - 1 by XREAL_1:19;
(len fs) + 0 <= (len fs) + 1 by XREAL_1:7;
then (len fs) - 1 <= len fs by XREAL_1:20;
then n <= len fs by A21, XXREAL_0:2;
then A22: n in dom (Seq q) by A7, A14, A15, A20;
1 <= m by A15, A16, XXREAL_0:2;
then A23: m in dom (Seq q) by A7, A14, A17, A20;
consider j2 being Element of NAT such that
A24: j2 = (Sgm (dom q)) . n and
A25: fs . n = i + j2 by A8, A22;
consider j3 being Element of NAT such that
A26: j3 = (Sgm (dom q)) . m and
A27: fs . m = i + j3 by A8, A23;
A28: ex l3 being Nat st dom q c= Seg l3 by FINSEQ_1:def_12;
dom (Seq ss) = Seg (len fs) by FINSEQ_1:def_3;
then len fs = len (Sgm (dom q)) by A14, FINSEQ_1:def_3;
then j2 < j3 by A15, A16, A17, A24, A26, A28, FINSEQ_1:def_13;
hence k1 < k2 by A18, A19, A25, A27, XREAL_1:8; ::_thesis: verum
end;
then fs = Sgm (dom (i Shift q)) by A5, A13, FINSEQ_1:def_13;
hence ex j being Element of NAT st
( j = (Sgm (dom q)) . k & (Sgm (dom (i Shift q))) . k = i + j ) by A1, A8; ::_thesis: verum
end;
theorem Th73: :: PNPROC_1:73
for k, i being Element of NAT
for q being FinSubsequence st k in dom (Seq q) holds
(Seq (i Shift q)) . k = (Seq q) . k
proof
let k, i be Element of NAT ; ::_thesis: for q being FinSubsequence st k in dom (Seq q) holds
(Seq (i Shift q)) . k = (Seq q) . k
let q be FinSubsequence; ::_thesis: ( k in dom (Seq q) implies (Seq (i Shift q)) . k = (Seq q) . k )
assume A1: k in dom (Seq q) ; ::_thesis: (Seq (i Shift q)) . k = (Seq q) . k
then consider j being Element of NAT such that
A2: j = (Sgm (dom q)) . k and
A3: (Sgm (dom (i Shift q))) . k = i + j by Th72;
A4: rng (Sgm (dom q)) = dom q by FINSEQ_1:50;
A5: dom (Seq q) = dom (Seq (i Shift q)) by Th71
.= dom ((i Shift q) * (Sgm (dom (i Shift q)))) by FINSEQ_1:def_14 ;
A6: dom (Seq q) = dom (q * (Sgm (dom q))) by FINSEQ_1:def_14
.= dom (Sgm (dom q)) by A4, RELAT_1:27 ;
then j in rng (Sgm (dom q)) by A1, A2, FUNCT_1:def_3;
then A7: j in dom q by FINSEQ_1:50;
(Seq (i Shift q)) . k = ((i Shift q) * (Sgm (dom (i Shift q)))) . k by FINSEQ_1:def_14
.= (i Shift q) . ((Sgm (dom (i Shift q))) . k) by A1, A5, FUNCT_1:12
.= q . j by A3, A7, Def14
.= (q * (Sgm (dom q))) . k by A1, A2, A6, FUNCT_1:13
.= (Seq q) . k by FINSEQ_1:def_14 ;
hence (Seq (i Shift q)) . k = (Seq q) . k ; ::_thesis: verum
end;
theorem :: PNPROC_1:74
for i being Element of NAT
for q being FinSubsequence holds Seq q = Seq (i Shift q)
proof
let i be Element of NAT ; ::_thesis: for q being FinSubsequence holds Seq q = Seq (i Shift q)
let q be FinSubsequence; ::_thesis: Seq q = Seq (i Shift q)
A1: dom (Seq q) = dom (Seq (i Shift q)) by Th71;
for x being set st x in dom (Seq q) holds
(Seq (i Shift q)) . x = (Seq q) . x by Th73;
hence Seq q = Seq (i Shift q) by A1, FUNCT_1:2; ::_thesis: verum
end;
theorem Th75: :: PNPROC_1:75
for k, i being Element of NAT
for q being FinSubsequence st dom q c= Seg k holds
dom (i Shift q) c= Seg (i + k)
proof
let k, i be Element of NAT ; ::_thesis: for q being FinSubsequence st dom q c= Seg k holds
dom (i Shift q) c= Seg (i + k)
let q be FinSubsequence; ::_thesis: ( dom q c= Seg k implies dom (i Shift q) c= Seg (i + k) )
assume A1: dom q c= Seg k ; ::_thesis: dom (i Shift q) c= Seg (i + k)
A2: dom (i Shift q) = { (i + j) where j is Element of NAT : j in dom q } by Def14;
A3: Seg k = { j where j is Element of NAT : ( 1 <= j & j <= k ) } by FINSEQ_1:def_1;
A4: Seg (i + k) = { j where j is Element of NAT : ( 1 <= j & j <= i + k ) } by FINSEQ_1:def_1;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in dom (i Shift q) or x in Seg (i + k) )
assume x in dom (i Shift q) ; ::_thesis: x in Seg (i + k)
then consider j1 being Element of NAT such that
A5: x = i + j1 and
A6: j1 in dom q by A2;
j1 in Seg k by A1, A6;
then A7: ex j2 being Element of NAT st
( j1 = j2 & 1 <= j2 & j2 <= k ) by A3;
0 <= i by NAT_1:2;
then A8: 0 + 1 <= i + j1 by A7, XREAL_1:7;
i + j1 <= i + k by A7, XREAL_1:7;
hence x in Seg (i + k) by A4, A5, A8; ::_thesis: verum
end;
theorem Th76: :: PNPROC_1:76
for p being FinSequence
for q1, q2 being FinSubsequence st q1 c= p holds
ex ss being FinSubsequence st ss = q1 \/ ((len p) Shift q2)
proof
let p be FinSequence; ::_thesis: for q1, q2 being FinSubsequence st q1 c= p holds
ex ss being FinSubsequence st ss = q1 \/ ((len p) Shift q2)
let q1, q2 be FinSubsequence; ::_thesis: ( q1 c= p implies ex ss being FinSubsequence st ss = q1 \/ ((len p) Shift q2) )
assume q1 c= p ; ::_thesis: ex ss being FinSubsequence st ss = q1 \/ ((len p) Shift q2)
then A1: dom q1 c= dom p by GRFUNC_1:2;
dom p misses dom ((len p) Shift q2) by Th60;
then reconsider ss = q1 \/ ((len p) Shift q2) as Function by A1, GRFUNC_1:13, XBOOLE_1:63;
A2: dom p = Seg (len p) by FINSEQ_1:def_3;
consider k being Nat such that
A3: dom q2 c= Seg k by FINSEQ_1:def_12;
k in NAT by ORDINAL1:def_12;
then A4: dom ((len p) Shift q2) c= Seg ((len p) + k) by A3, Th75;
0 <= k by NAT_1:2;
then (len p) + 0 <= (len p) + k by XREAL_1:7;
then Seg (len p) c= Seg ((len p) + k) by FINSEQ_1:5;
then dom q1 c= Seg ((len p) + k) by A1, A2, XBOOLE_1:1;
then (dom q1) \/ (dom ((len p) Shift q2)) c= Seg ((len p) + k) by A4, XBOOLE_1:8;
then dom (q1 \/ ((len p) Shift q2)) c= Seg ((len p) + k) by RELAT_1:1;
then reconsider ss = ss as FinSubsequence by FINSEQ_1:def_12;
take ss ; ::_thesis: ss = q1 \/ ((len p) Shift q2)
thus ss = q1 \/ ((len p) Shift q2) ; ::_thesis: verum
end;
Lm12: for p1, p2 being FinSequence
for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
Sgm ((dom q1) \/ (dom ((len p1) Shift q2))) = (Sgm (dom q1)) ^ (Sgm (dom ((len p1) Shift q2)))
proof
let p1, p2 be FinSequence; ::_thesis: for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
Sgm ((dom q1) \/ (dom ((len p1) Shift q2))) = (Sgm (dom q1)) ^ (Sgm (dom ((len p1) Shift q2)))
let q1, q2 be FinSubsequence; ::_thesis: ( q1 c= p1 & q2 c= p2 implies Sgm ((dom q1) \/ (dom ((len p1) Shift q2))) = (Sgm (dom q1)) ^ (Sgm (dom ((len p1) Shift q2))) )
assume that
A1: q1 c= p1 and
A2: q2 c= p2 ; ::_thesis: Sgm ((dom q1) \/ (dom ((len p1) Shift q2))) = (Sgm (dom q1)) ^ (Sgm (dom ((len p1) Shift q2)))
A3: ex k1 being Nat st dom q1 c= Seg k1 by FINSEQ_1:def_12;
A4: ex k2 being Nat st dom ((len p1) Shift q2) c= Seg k2 by FINSEQ_1:def_12;
for m, n being Element of NAT st m in dom q1 & n in dom ((len p1) Shift q2) holds
m < n
proof
let m, n be Element of NAT ; ::_thesis: ( m in dom q1 & n in dom ((len p1) Shift q2) implies m < n )
assume that
A5: m in dom q1 and
A6: n in dom ((len p1) Shift q2) ; ::_thesis: m < n
A7: dom p1 = Seg (len p1) by FINSEQ_1:def_3
.= { k where k is Element of NAT : ( 1 <= k & k <= len p1 ) } by FINSEQ_1:def_1 ;
A8: dom ((len p1) Shift p2) = { k where k is Element of NAT : ( (len p1) + 1 <= k & k <= (len p1) + (len p2) ) } by Th51;
A9: dom q1 c= dom p1 by A1, GRFUNC_1:2;
A10: dom ((len p1) Shift q2) c= dom ((len p1) Shift p2) by A2, Lm11;
A11: m in dom p1 by A5, A9;
A12: n in dom ((len p1) Shift p2) by A6, A10;
consider k3 being Element of NAT such that
A13: k3 = m and
1 <= k3 and
A14: k3 <= len p1 by A7, A11;
consider k4 being Element of NAT such that
A15: k4 = n and
A16: (len p1) + 1 <= k4 and
k4 <= (len p1) + (len p2) by A8, A12;
len p1 < (len p1) + 1 by XREAL_1:29;
then k3 <= (len p1) + 1 by A14, XXREAL_0:2;
then A17: k3 <= k4 by A16, XXREAL_0:2;
dom p1 misses dom ((len p1) Shift p2) by Th60;
then k3 <> k4 by A5, A6, A9, A10, A13, A15, Lm3;
hence m < n by A13, A15, A17, XXREAL_0:1; ::_thesis: verum
end;
hence Sgm ((dom q1) \/ (dom ((len p1) Shift q2))) = (Sgm (dom q1)) ^ (Sgm (dom ((len p1) Shift q2))) by A3, A4, FINSEQ_3:42; ::_thesis: verum
end;
theorem Th77: :: PNPROC_1:77
for p1, p2 being FinSequence
for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) )
proof
let p1, p2 be FinSequence; ::_thesis: for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) )
let q1, q2 be FinSubsequence; ::_thesis: ( q1 c= p1 & q2 c= p2 implies ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) ) )
assume that
A1: q1 c= p1 and
A2: q2 c= p2 ; ::_thesis: ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) )
consider ss being FinSubsequence such that
A3: ss = q1 \/ ((len p1) Shift q2) by A1, Th76;
A4: ex k1 being Nat st dom q1 c= Seg k1 by FINSEQ_1:def_12;
A5: ex k2 being Nat st dom ((len p1) Shift q2) c= Seg k2 by FINSEQ_1:def_12;
A6: rng (Sgm (dom ss)) = dom ss by FINSEQ_1:50;
dom (Seq ss) = dom (ss * (Sgm (dom ss))) by FINSEQ_1:def_14;
then A7: dom (Seq ss) = dom (Sgm (dom ss)) by A6, RELAT_1:27
.= dom (Sgm ((dom q1) \/ (dom ((len p1) Shift q2)))) by A3, RELAT_1:1
.= dom ((Sgm (dom q1)) ^ (Sgm (dom ((len p1) Shift q2)))) by A1, A2, Lm12
.= Seg ((len (Sgm (dom q1))) + (len (Sgm (dom ((len p1) Shift q2))))) by FINSEQ_1:def_7 ;
A8: len (Sgm (dom ((len p1) Shift q2))) = card (dom ((len p1) Shift q2)) by A5, FINSEQ_3:39;
A9: len (Sgm (dom q1)) = card (dom q1) by A4, FINSEQ_3:39;
len (Sgm (dom ((len p1) Shift q2))) = card ((len p1) Shift q2) by A8, CARD_1:62;
then A10: len (Sgm (dom ((len p1) Shift q2))) = card q2 by Th54;
A11: len (Sgm (dom q1)) = card q1 by A9, CARD_1:62;
A12: len (Sgm (dom ((len p1) Shift q2))) = len (Seq q2) by A10, Th7;
len (Sgm (dom q1)) = len (Seq q1) by A11, Th7;
hence ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) ) by A3, A7, A12; ::_thesis: verum
end;
theorem Th78: :: PNPROC_1:78
for p1, p2 being FinSequence
for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) & Seq ss = (Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) )
proof
let p1, p2 be FinSequence; ::_thesis: for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) & Seq ss = (Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) )
let q1, q2 be FinSubsequence; ::_thesis: ( q1 c= p1 & q2 c= p2 implies ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) & Seq ss = (Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) ) )
assume that
A1: q1 c= p1 and
A2: q2 c= p2 ; ::_thesis: ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) & Seq ss = (Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) )
consider ss being FinSubsequence such that
A3: ss = q1 \/ ((len p1) Shift q2) and
A4: dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) by A1, A2, Th77;
A5: Seg ((len (Seq q1)) + (len (Seq q2))) = { k where k is Element of NAT : ( 1 <= k & k <= (len (Seq q1)) + (len (Seq q2)) ) } by FINSEQ_1:def_1;
A6: dom (Seq q1) = Seg (len (Seq q1)) by FINSEQ_1:def_3
.= { k where k is Element of NAT : ( 1 <= k & k <= len (Seq q1) ) } by FINSEQ_1:def_1 ;
A7: dom ((len (Seq q1)) Shift (Seq q2)) = { k where k is Element of NAT : ( (len (Seq q1)) + 1 <= k & k <= (len (Seq q1)) + (len (Seq q2)) ) } by Th51;
A8: Seg ((len (Seq q1)) + (len (Seq q2))) = (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2)))
proof
thus Seg ((len (Seq q1)) + (len (Seq q2))) c= (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2))) :: according to XBOOLE_0:def_10 ::_thesis: (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2))) c= Seg ((len (Seq q1)) + (len (Seq q2)))
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Seg ((len (Seq q1)) + (len (Seq q2))) or x in (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2))) )
assume x in Seg ((len (Seq q1)) + (len (Seq q2))) ; ::_thesis: x in (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2)))
then consider k1 being Element of NAT such that
A9: x = k1 and
A10: 1 <= k1 and
A11: k1 <= (len (Seq q1)) + (len (Seq q2)) by A5;
A12: ( 1 <= k1 & k1 <= len (Seq q1) implies k1 in dom (Seq q1) ) by A6;
( (len (Seq q1)) + 1 <= k1 & k1 <= (len (Seq q1)) + (len (Seq q2)) implies k1 in dom ((len (Seq q1)) Shift (Seq q2)) ) by A7;
hence x in (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2))) by A9, A10, A11, A12, INT_1:7, XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2))) or x in Seg ((len (Seq q1)) + (len (Seq q2))) )
assume A13: x in (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2))) ; ::_thesis: x in Seg ((len (Seq q1)) + (len (Seq q2)))
A14: 0 <= len (Seq q1) by NAT_1:2;
A15: 0 <= len (Seq q2) by NAT_1:2;
A16: now__::_thesis:_(_x_in_dom_(Seq_q1)_implies_x_in_Seg_((len_(Seq_q1))_+_(len_(Seq_q2)))_)
assume x in dom (Seq q1) ; ::_thesis: x in Seg ((len (Seq q1)) + (len (Seq q2)))
then consider k1 being Element of NAT such that
A17: x = k1 and
A18: 1 <= k1 and
A19: k1 <= len (Seq q1) by A6;
(len (Seq q1)) + 0 <= (len (Seq q1)) + (len (Seq q2)) by A15, XREAL_1:7;
then k1 <= (len (Seq q1)) + (len (Seq q2)) by A19, XXREAL_0:2;
hence x in Seg ((len (Seq q1)) + (len (Seq q2))) by A5, A17, A18; ::_thesis: verum
end;
now__::_thesis:_(_x_in_dom_((len_(Seq_q1))_Shift_(Seq_q2))_implies_x_in_Seg_((len_(Seq_q1))_+_(len_(Seq_q2)))_)
assume x in dom ((len (Seq q1)) Shift (Seq q2)) ; ::_thesis: x in Seg ((len (Seq q1)) + (len (Seq q2)))
then consider k2 being Element of NAT such that
A20: x = k2 and
A21: (len (Seq q1)) + 1 <= k2 and
A22: k2 <= (len (Seq q1)) + (len (Seq q2)) by A7;
0 + 1 <= (len (Seq q1)) + 1 by A14, XREAL_1:7;
then 1 <= k2 by A21, XXREAL_0:2;
hence x in Seg ((len (Seq q1)) + (len (Seq q2))) by A5, A20, A22; ::_thesis: verum
end;
hence x in Seg ((len (Seq q1)) + (len (Seq q2))) by A13, A16, XBOOLE_0:def_3; ::_thesis: verum
end;
A23: (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2))) = dom ((Seq q1) \/ ((len (Seq q1)) Shift (Seq q2))) by RELAT_1:1;
dom (Seq q1) misses dom ((len (Seq q1)) Shift (Seq q2)) by Th60;
then reconsider ss1 = (Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) as Function by GRFUNC_1:13;
for x being set st x in dom (Seq ss) holds
(Seq ss) . x = ss1 . x
proof
let x be set ; ::_thesis: ( x in dom (Seq ss) implies (Seq ss) . x = ss1 . x )
assume A24: x in dom (Seq ss) ; ::_thesis: (Seq ss) . x = ss1 . x
then A25: x in dom (ss * (Sgm (dom ss))) by FINSEQ_1:def_14;
A26: (Seq ss) . x = (ss * (Sgm (dom ss))) . x by FINSEQ_1:def_14
.= ss . ((Sgm (dom ss)) . x) by A25, FUNCT_1:12
.= ss . ((Sgm ((dom q1) \/ (dom ((len p1) Shift q2)))) . x) by A3, RELAT_1:1
.= ss . (((Sgm (dom q1)) ^ (Sgm (dom ((len p1) Shift q2)))) . x) by A1, A2, Lm12 ;
A27: now__::_thesis:_(_x_in_dom_(Seq_q1)_implies_(Seq_ss)_._x_=_ss1_._x_)
assume A28: x in dom (Seq q1) ; ::_thesis: (Seq ss) . x = ss1 . x
then A29: x in dom (Sgm (dom q1)) by Lm5;
then (Sgm (dom q1)) . x in rng (Sgm (dom q1)) by FUNCT_1:def_3;
then A30: (Sgm (dom q1)) . x in dom q1 by FINSEQ_1:50;
(Seq ss) . x = ss . ((Sgm (dom q1)) . x) by A26, A29, FINSEQ_1:def_7
.= q1 . ((Sgm (dom q1)) . x) by A3, A30, GRFUNC_1:15
.= (q1 * (Sgm (dom q1))) . x by A29, FUNCT_1:13
.= (Seq q1) . x by FINSEQ_1:def_14 ;
hence (Seq ss) . x = ss1 . x by A28, GRFUNC_1:15; ::_thesis: verum
end;
now__::_thesis:_(_x_in_dom_((len_(Seq_q1))_Shift_(Seq_q2))_implies_(Seq_ss)_._x_=_ss1_._x_)
assume A31: x in dom ((len (Seq q1)) Shift (Seq q2)) ; ::_thesis: (Seq ss) . x = ss1 . x
dom ((len (Seq q1)) Shift (Seq q2)) = { ((len (Seq q1)) + j) where j is Element of NAT : j in dom (Seq q2) } by Def14;
then consider j being Element of NAT such that
A32: x = (len (Seq q1)) + j and
A33: j in dom (Seq q2) by A31;
A34: ss1 . x = ((len (Seq q1)) Shift (Seq q2)) . x by A31, GRFUNC_1:15
.= (Seq q2) . j by A32, A33, Def14 ;
A35: ex l1 being Nat st dom q1 c= Seg l1 by FINSEQ_1:def_12;
A36: ex l2 being Nat st dom ((len p1) Shift q2) c= Seg l2 by FINSEQ_1:def_12;
card (dom q1) = len (Sgm (dom q1)) by A35, FINSEQ_3:39;
then A37: card q1 = len (Sgm (dom q1)) by CARD_1:62;
A38: len (Seq q1) = card q1 by Th7;
A39: dom (Seq q2) = Seg (len (Seq q2)) by FINSEQ_1:def_3;
card q2 = len (Seq q2) by Th7;
then card ((len p1) Shift q2) = len (Seq q2) by Th54;
then A40: card (dom ((len p1) Shift q2)) = len (Seq q2) by CARD_1:62;
A41: card (dom ((len p1) Shift q2)) = len (Sgm (dom ((len p1) Shift q2))) by A36, FINSEQ_3:39;
A42: len (Sgm (dom ((len p1) Shift q2))) = len (Seq q2) by A36, A40, FINSEQ_3:39;
A43: dom (Seq q2) = dom (Sgm (dom ((len p1) Shift q2))) by A39, A40, A41, FINSEQ_1:def_3;
A44: j in dom (Sgm (dom ((len p1) Shift q2))) by A33, A39, A42, FINSEQ_1:def_3;
(Sgm (dom ((len p1) Shift q2))) . j in rng (Sgm (dom ((len p1) Shift q2))) by A33, A43, FUNCT_1:def_3;
then A45: (Sgm (dom ((len p1) Shift q2))) . j in dom ((len p1) Shift q2) by FINSEQ_1:50;
(Seq ss) . x = ss . ((Sgm (dom ((len p1) Shift q2))) . j) by A26, A32, A37, A38, A44, FINSEQ_1:def_7
.= ((len p1) Shift q2) . ((Sgm (dom ((len p1) Shift q2))) . j) by A3, A45, GRFUNC_1:15
.= (((len p1) Shift q2) * (Sgm (dom ((len p1) Shift q2)))) . j by A33, A43, FUNCT_1:13
.= (Seq ((len p1) Shift q2)) . j by FINSEQ_1:def_14
.= (Seq q2) . j by A33, Th73 ;
hence (Seq ss) . x = ss1 . x by A34; ::_thesis: verum
end;
hence (Seq ss) . x = ss1 . x by A4, A8, A24, A27, XBOOLE_0:def_3; ::_thesis: verum
end;
then Seq ss = ss1 by A4, A8, A23, FUNCT_1:2;
hence ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) & Seq ss = (Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) ) by A3, A4; ::_thesis: verum
end;
theorem Th79: :: PNPROC_1:79
for p1, p2 being FinSequence
for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & (Seq q1) ^ (Seq q2) = Seq ss )
proof
let p1, p2 be FinSequence; ::_thesis: for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & (Seq q1) ^ (Seq q2) = Seq ss )
let q1, q2 be FinSubsequence; ::_thesis: ( q1 c= p1 & q2 c= p2 implies ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & (Seq q1) ^ (Seq q2) = Seq ss ) )
assume that
A1: q1 c= p1 and
A2: q2 c= p2 ; ::_thesis: ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & (Seq q1) ^ (Seq q2) = Seq ss )
consider ss being FinSubsequence such that
A3: ss = q1 \/ ((len p1) Shift q2) and
A4: dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) and
A5: Seq ss = (Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) by A1, A2, Th78;
A6: for j1 being Nat st j1 in dom (Seq q1) holds
(Seq ss) . j1 = (Seq q1) . j1 by A5, GRFUNC_1:15;
for j2 being Nat st j2 in dom (Seq q2) holds
(Seq ss) . ((len (Seq q1)) + j2) = (Seq q2) . j2
proof
let j2 be Nat; ::_thesis: ( j2 in dom (Seq q2) implies (Seq ss) . ((len (Seq q1)) + j2) = (Seq q2) . j2 )
assume A7: j2 in dom (Seq q2) ; ::_thesis: (Seq ss) . ((len (Seq q1)) + j2) = (Seq q2) . j2
dom ((len (Seq q1)) Shift (Seq q2)) = { ((len (Seq q1)) + k) where k is Element of NAT : k in dom (Seq q2) } by Def14;
then (len (Seq q1)) + j2 in dom ((len (Seq q1)) Shift (Seq q2)) by A7;
hence (Seq ss) . ((len (Seq q1)) + j2) = ((len (Seq q1)) Shift (Seq q2)) . ((len (Seq q1)) + j2) by A5, GRFUNC_1:15
.= (Seq q2) . j2 by A7, Def14 ;
::_thesis: verum
end;
then Seq ss = (Seq q1) ^ (Seq q2) by A4, A6, FINSEQ_1:def_7;
hence ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & (Seq q1) ^ (Seq q2) = Seq ss ) by A3; ::_thesis: verum
end;
theorem :: PNPROC_1:80
for P being set
for N being Petri_net of P
for R1, R2, P1, P2 being process of N holds (R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2)
proof
let P be set ; ::_thesis: for N being Petri_net of P
for R1, R2, P1, P2 being process of N holds (R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2)
let N be Petri_net of P; ::_thesis: for R1, R2, P1, P2 being process of N holds (R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2)
let R1, R2, P1, P2 be process of N; ::_thesis: (R1 concur R2) before (P1 concur P2) c= (R1 before P1) concur (R2 before P2)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (R1 concur R2) before (P1 concur P2) or x in (R1 before P1) concur (R2 before P2) )
assume x in (R1 concur R2) before (P1 concur P2) ; ::_thesis: x in (R1 before P1) concur (R2 before P2)
then consider C1, C2 being firing-sequence of N such that
A1: x = C1 ^ C2 and
A2: C1 in R1 concur R2 and
A3: C2 in P1 concur P2 ;
consider C3 being firing-sequence of N such that
A4: C1 = C3 and
A5: ex q1, q2 being FinSubsequence st
( C3 = q1 \/ q2 & q1 misses q2 & Seq q1 in R1 & Seq q2 in R2 ) by A2;
consider q1, q2 being FinSubsequence such that
A6: C3 = q1 \/ q2 and
A7: q1 misses q2 and
A8: Seq q1 in R1 and
A9: Seq q2 in R2 by A5;
consider C4 being firing-sequence of N such that
A10: C2 = C4 and
A11: ex q3, q4 being FinSubsequence st
( C4 = q3 \/ q4 & q3 misses q4 & Seq q3 in P1 & Seq q4 in P2 ) by A3;
consider q3, q4 being FinSubsequence such that
A12: C4 = q3 \/ q4 and
A13: q3 misses q4 and
A14: Seq q3 in P1 and
A15: Seq q4 in P2 by A11;
reconsider C = C1 ^ C2 as firing-sequence of N ;
reconsider q5 = (len C1) Shift q3, q6 = (len C1) Shift q4 as FinSubsequence ;
A16: q1 c= C1 by A4, A6, XBOOLE_1:7;
A17: q2 c= C1 by A4, A6, XBOOLE_1:7;
A18: q3 c= C2 by A10, A12, XBOOLE_1:7;
A19: q4 c= C2 by A10, A12, XBOOLE_1:7;
A20: C1 c= C1 ^ C2 by FINSEQ_6:10;
then A21: q1 c= C1 ^ C2 by A16, XBOOLE_1:1;
A22: q2 c= C1 ^ C2 by A17, A20, XBOOLE_1:1;
reconsider ss = C2 as FinSubsequence ;
A23: q5 c= (len C1) Shift ss by A10, A12, Th67, XBOOLE_1:7;
A24: q6 c= (len C1) Shift ss by A10, A12, Th67, XBOOLE_1:7;
A25: (len C1) Shift C2 c= C1 ^ C2 by Th68;
then A26: q5 c= C1 ^ C2 by A23, XBOOLE_1:1;
A27: q6 c= C1 ^ C2 by A24, A25, XBOOLE_1:1;
A28: dom q1 misses dom q5 by A16, A21, A26, Lm10, Th9;
dom q2 misses dom q6 by A17, A22, A27, Lm10, Th9;
then reconsider ss1 = q1 \/ q5, ss2 = q2 \/ q6 as Function by A28, GRFUNC_1:13;
A29: dom C = Seg (len C) by FINSEQ_1:def_3;
A30: dom ss1 c= dom C by A16, A18, Lm9;
dom ss2 c= dom C by A17, A19, Lm9;
then reconsider ss1 = ss1, ss2 = ss2 as FinSubsequence by A29, A30, FINSEQ_1:def_12;
A31: ss1 \/ ss2 = ((q1 \/ ((len C1) Shift q3)) \/ q2) \/ ((len C1) Shift q4) by XBOOLE_1:4
.= ((q1 \/ q2) \/ ((len C1) Shift q3)) \/ ((len C1) Shift q4) by XBOOLE_1:4
.= C1 \/ (((len C1) Shift q3) \/ ((len C1) Shift q4)) by A4, A6, XBOOLE_1:4
.= C1 \/ ((len C1) Shift C2) by A10, A12, A13, Th70
.= C by Th61 ;
A32: ss1 /\ q2 = (q1 /\ q2) \/ (((len C1) Shift q3) /\ q2) by XBOOLE_1:23;
ss1 /\ ((len C1) Shift q4) = (q1 /\ ((len C1) Shift q4)) \/ (((len C1) Shift q3) /\ ((len C1) Shift q4)) by XBOOLE_1:23;
then A33: ss1 /\ ss2 = ((q1 /\ q2) \/ (((len C1) Shift q3) /\ q2)) \/ ((q1 /\ ((len C1) Shift q4)) \/ (((len C1) Shift q3) /\ ((len C1) Shift q4))) by A32, XBOOLE_1:23;
A34: q1 /\ q2 = {} by A7, XBOOLE_0:def_7;
A35: (len C1) Shift q3 misses q2 by A4, A6, Lm10, XBOOLE_1:7;
A36: q1 misses (len C1) Shift q4 by A4, A6, Lm10, XBOOLE_1:7;
A37: ((len C1) Shift q3) /\ q2 = {} by A35, XBOOLE_0:def_7;
A38: q1 /\ ((len C1) Shift q4) = {} by A36, XBOOLE_0:def_7;
dom q3 misses dom q4 by A13, A18, A19, Th9;
then dom ((len C1) Shift q3) misses dom ((len C1) Shift q4) by Th69;
then (len C1) Shift q3 misses (len C1) Shift q4 by Lm4;
then ss1 /\ ss2 = {} by A33, A34, A37, A38, XBOOLE_0:def_7;
then A39: ss1 misses ss2 by XBOOLE_0:def_7;
A40: ex ss3 being FinSubsequence st
( ss3 = ss1 & (Seq q1) ^ (Seq q3) = Seq ss3 ) by A16, A18, Th79;
A41: ex ss4 being FinSubsequence st
( ss4 = ss2 & (Seq q2) ^ (Seq q4) = Seq ss4 ) by A17, A19, Th79;
A42: Seq ss1 in R1 before P1 by A8, A14, A40;
Seq ss2 in R2 before P2 by A9, A15, A41;
hence x in (R1 before P1) concur (R2 before P2) by A1, A31, A39, A42; ::_thesis: verum
end;
registration
let P be set ;
let N be Petri_net of P;
let R1, R2 be non empty process of N;
clusterR1 concur R2 -> non empty ;
coherence
not R1 concur R2 is empty
proof
consider fs1 being set such that
A1: fs1 in R1 by XBOOLE_0:def_1;
consider fs2 being set such that
A2: fs2 in R2 by XBOOLE_0:def_1;
reconsider fs1 = fs1, fs2 = fs2 as firing-sequence of N by A1, A2;
reconsider C = fs1 ^ fs2 as firing-sequence of N ;
A3: C = fs1 \/ ((len fs1) Shift fs2) by Th61;
A4: fs1 misses (len fs1) Shift fs2 by Th62;
A5: fs1 = Seq fs1 by FINSEQ_3:116;
Seq ((len fs1) Shift fs2) in R2 by A2, Th58;
then C in R1 concur R2 by A1, A3, A4, A5;
hence not R1 concur R2 is empty ; ::_thesis: verum
end;
end;
begin
definition
let P be set ;
let N be Petri_net of P;
func NeutralProcess N -> non empty process of N equals :: PNPROC_1:def 15
{(<*> N)};
coherence
{(<*> N)} is non empty process of N ;
end;
:: deftheorem defines NeutralProcess PNPROC_1:def_15_:_
for P being set
for N being Petri_net of P holds NeutralProcess N = {(<*> N)};
definition
let P be set ;
let N be Petri_net of P;
let t be Element of N;
func ElementaryProcess t -> non empty process of N equals :: PNPROC_1:def 16
{<*t*>};
coherence
{<*t*>} is non empty process of N ;
end;
:: deftheorem defines ElementaryProcess PNPROC_1:def_16_:_
for P being set
for N being Petri_net of P
for t being Element of N holds ElementaryProcess t = {<*t*>};
theorem :: PNPROC_1:81
for P being set
for N being Petri_net of P
for R being process of N holds (NeutralProcess N) before R = R
proof
let P be set ; ::_thesis: for N being Petri_net of P
for R being process of N holds (NeutralProcess N) before R = R
let N be Petri_net of P; ::_thesis: for R being process of N holds (NeutralProcess N) before R = R
let R be process of N; ::_thesis: (NeutralProcess N) before R = R
thus (NeutralProcess N) before R c= R :: according to XBOOLE_0:def_10 ::_thesis: R c= (NeutralProcess N) before R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (NeutralProcess N) before R or x in R )
assume x in (NeutralProcess N) before R ; ::_thesis: x in R
then consider C1, C being firing-sequence of N such that
A1: x = C1 ^ C and
A2: C1 in NeutralProcess N and
A3: C in R ;
C1 = <*> N by A2, TARSKI:def_1;
hence x in R by A1, A3, FINSEQ_1:34; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R or x in (NeutralProcess N) before R )
assume A4: x in R ; ::_thesis: x in (NeutralProcess N) before R
then reconsider C = x as Element of N * ;
A5: <*> N in NeutralProcess N by TARSKI:def_1;
x = (<*> N) ^ C by FINSEQ_1:34;
hence x in (NeutralProcess N) before R by A4, A5; ::_thesis: verum
end;
theorem :: PNPROC_1:82
for P being set
for N being Petri_net of P
for R being process of N holds R before (NeutralProcess N) = R
proof
let P be set ; ::_thesis: for N being Petri_net of P
for R being process of N holds R before (NeutralProcess N) = R
let N be Petri_net of P; ::_thesis: for R being process of N holds R before (NeutralProcess N) = R
let R be process of N; ::_thesis: R before (NeutralProcess N) = R
thus R before (NeutralProcess N) c= R :: according to XBOOLE_0:def_10 ::_thesis: R c= R before (NeutralProcess N)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R before (NeutralProcess N) or x in R )
assume x in R before (NeutralProcess N) ; ::_thesis: x in R
then consider C1, C being firing-sequence of N such that
A1: x = C1 ^ C and
A2: C1 in R and
A3: C in NeutralProcess N ;
C = <*> N by A3, TARSKI:def_1;
hence x in R by A1, A2, FINSEQ_1:34; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R or x in R before (NeutralProcess N) )
assume A4: x in R ; ::_thesis: x in R before (NeutralProcess N)
then reconsider C = x as Element of N * ;
A5: <*> N in NeutralProcess N by TARSKI:def_1;
x = C ^ (<*> N) by FINSEQ_1:34;
hence x in R before (NeutralProcess N) by A4, A5; ::_thesis: verum
end;
theorem :: PNPROC_1:83
for P being set
for N being Petri_net of P
for R being process of N holds (NeutralProcess N) concur R = R
proof
let P be set ; ::_thesis: for N being Petri_net of P
for R being process of N holds (NeutralProcess N) concur R = R
let N be Petri_net of P; ::_thesis: for R being process of N holds (NeutralProcess N) concur R = R
let R be process of N; ::_thesis: (NeutralProcess N) concur R = R
thus (NeutralProcess N) concur R c= R :: according to XBOOLE_0:def_10 ::_thesis: R c= (NeutralProcess N) concur R
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (NeutralProcess N) concur R or x in R )
assume x in (NeutralProcess N) concur R ; ::_thesis: x in R
then consider C being firing-sequence of N such that
A1: x = C and
A2: ex q1, q2 being FinSubsequence st
( C = q1 \/ q2 & q1 misses q2 & Seq q1 in {(<*> N)} & Seq q2 in R ) ;
consider q1, q2 being FinSubsequence such that
A3: C = q1 \/ q2 and
q1 misses q2 and
A4: Seq q1 in {(<*> N)} and
A5: Seq q2 in R by A2;
Seq q1 = {} by A4, TARSKI:def_1;
then q1 = {} by Lm1;
hence x in R by A1, A3, A5, FINSEQ_3:116; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in R or x in (NeutralProcess N) concur R )
assume A6: x in R ; ::_thesis: x in (NeutralProcess N) concur R
then reconsider C = x as firing-sequence of N ;
reconsider q1 = <*> N, q2 = C as FinSubsequence ;
A7: q1 /\ q2 = {} ;
A8: Seq q2 = C by FINSEQ_3:116;
A9: {} \/ q2 = C ;
A10: Seq q1 = q1 by FINSEQ_3:116;
A11: q1 in {(<*> N)} by TARSKI:def_1;
q1 misses q2 by A7, XBOOLE_0:def_7;
hence x in (NeutralProcess N) concur R by A6, A8, A9, A10, A11; ::_thesis: verum
end;