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