:: REWRITE3 semantic presentation begin theorem Th1: :: REWRITE3:1 for x being set for k being Nat for p being FinSequence st k in dom p holds (<*x*> ^ p) . (k + 1) = p . k proof let x be set ; ::_thesis: for k being Nat for p being FinSequence st k in dom p holds (<*x*> ^ p) . (k + 1) = p . k let k be Nat; ::_thesis: for p being FinSequence st k in dom p holds (<*x*> ^ p) . (k + 1) = p . k let p be FinSequence; ::_thesis: ( k in dom p implies (<*x*> ^ p) . (k + 1) = p . k ) assume A1: k in dom p ; ::_thesis: (<*x*> ^ p) . (k + 1) = p . k k >= 1 by A1, FINSEQ_3:25; then k >= len <*x*> by FINSEQ_1:39; then A2: (len <*x*>) + 0 < k + 1 by XREAL_1:8; (len <*x*>) + k in dom (<*x*> ^ p) by A1, FINSEQ_1:28; then k + 1 in dom (<*x*> ^ p) by FINSEQ_1:39; then k + 1 <= len (<*x*> ^ p) by FINSEQ_3:25; then (<*x*> ^ p) . (k + 1) = p . ((k + 1) - (len <*x*>)) by A2, FINSEQ_1:24 .= p . ((k + 1) - 1) by FINSEQ_1:39 .= p . (k + (1 - 1)) ; hence (<*x*> ^ p) . (k + 1) = p . k ; ::_thesis: verum end; theorem Th2: :: REWRITE3:2 for p being FinSequence st p <> {} holds ex q being FinSequence ex x being set st ( p = q ^ <*x*> & len p = (len q) + 1 ) proof let p be FinSequence; ::_thesis: ( p <> {} implies ex q being FinSequence ex x being set st ( p = q ^ <*x*> & len p = (len q) + 1 ) ) assume p <> {} ; ::_thesis: ex q being FinSequence ex x being set st ( p = q ^ <*x*> & len p = (len q) + 1 ) then consider q being FinSequence, x being set such that A1: p = q ^ <*x*> by FINSEQ_1:46; take q ; ::_thesis: ex x being set st ( p = q ^ <*x*> & len p = (len q) + 1 ) take x ; ::_thesis: ( p = q ^ <*x*> & len p = (len q) + 1 ) len p = (len q) + (len <*x*>) by A1, FINSEQ_1:22 .= (len q) + 1 by FINSEQ_1:40 ; hence ( p = q ^ <*x*> & len p = (len q) + 1 ) by A1; ::_thesis: verum end; theorem Th3: :: REWRITE3:3 for k being Nat for p being FinSequence st k in dom p & not k + 1 in dom p holds len p = k proof let k be Nat; ::_thesis: for p being FinSequence st k in dom p & not k + 1 in dom p holds len p = k let p be FinSequence; ::_thesis: ( k in dom p & not k + 1 in dom p implies len p = k ) assume that A1: k in dom p and A2: not k + 1 in dom p ; ::_thesis: len p = k A3: ( 1 > k + 1 or k + 1 > len p ) by A2, FINSEQ_3:25; A4: 1 + 0 <= k + 1 by XREAL_1:7; k <= len p by A1, FINSEQ_3:25; hence len p = k by A3, A4, NAT_1:22; ::_thesis: verum end; begin theorem Th4: :: REWRITE3:4 for R being Relation for P being RedSequence of R for q1, q2 being FinSequence st P = q1 ^ q2 & len q1 > 0 & len q2 > 0 holds ( q1 is RedSequence of R & q2 is RedSequence of R ) proof let R be Relation; ::_thesis: for P being RedSequence of R for q1, q2 being FinSequence st P = q1 ^ q2 & len q1 > 0 & len q2 > 0 holds ( q1 is RedSequence of R & q2 is RedSequence of R ) let P be RedSequence of R; ::_thesis: for q1, q2 being FinSequence st P = q1 ^ q2 & len q1 > 0 & len q2 > 0 holds ( q1 is RedSequence of R & q2 is RedSequence of R ) let q1, q2 be FinSequence; ::_thesis: ( P = q1 ^ q2 & len q1 > 0 & len q2 > 0 implies ( q1 is RedSequence of R & q2 is RedSequence of R ) ) assume that A1: P = q1 ^ q2 and A2: len q1 > 0 and A3: len q2 > 0 ; ::_thesis: ( q1 is RedSequence of R & q2 is RedSequence of R ) now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_q1_&_i_+_1_in_dom_q1_holds_ [(q1_._i),(q1_._(i_+_1))]_in_R let i be Element of NAT ; ::_thesis: ( i in dom q1 & i + 1 in dom q1 implies [(q1 . i),(q1 . (i + 1))] in R ) assume that A4: i in dom q1 and A5: i + 1 in dom q1 ; ::_thesis: [(q1 . i),(q1 . (i + 1))] in R A6: i + 1 <= len q1 by A5, FINSEQ_3:25; A7: 1 <= i + 1 by A5, FINSEQ_3:25; then A8: q1 . (i + 1) = (q1 ^ q2) . (i + 1) by A6, FINSEQ_1:64; A9: len q1 <= len P by A1, CALCUL_1:6; then i + 1 <= len P by A6, XXREAL_0:2; then A10: i + 1 in dom P by A7, FINSEQ_3:25; A11: 1 <= i by A4, FINSEQ_3:25; A12: i <= len q1 by A4, FINSEQ_3:25; then i <= len P by A9, XXREAL_0:2; then A13: i in dom P by A11, FINSEQ_3:25; q1 . i = (q1 ^ q2) . i by A11, A12, FINSEQ_1:64; hence [(q1 . i),(q1 . (i + 1))] in R by A1, A8, A13, A10, REWRITE1:def_2; ::_thesis: verum end; hence q1 is RedSequence of R by A2, REWRITE1:def_2; ::_thesis: q2 is RedSequence of R now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_q2_&_i_+_1_in_dom_q2_holds_ [(q2_._i),(q2_._(i_+_1))]_in_R let i be Element of NAT ; ::_thesis: ( i in dom q2 & i + 1 in dom q2 implies [(q2 . i),(q2 . (i + 1))] in R ) assume that A14: i in dom q2 and A15: i + 1 in dom q2 ; ::_thesis: [(q2 . i),(q2 . (i + 1))] in R A16: 1 <= i + 1 by A15, FINSEQ_3:25; then A17: 1 <= (i + 1) + (len q1) by NAT_1:12; A18: 1 <= i by A14, FINSEQ_3:25; then A19: 1 <= i + (len q1) by NAT_1:12; A20: i + 1 <= len q2 by A15, FINSEQ_3:25; then A21: q2 . (i + 1) = (q1 ^ q2) . ((len q1) + (i + 1)) by A16, FINSEQ_1:65; A22: (len q1) + (len q2) = len P by A1, FINSEQ_1:22; then (len q1) + (i + 1) <= ((len P) - (len q2)) + (len q2) by A20, XREAL_1:7; then A23: ((len q1) + i) + 1 in dom P by A17, FINSEQ_3:25; A24: i <= len q2 by A14, FINSEQ_3:25; then (len q1) + i <= ((len P) - (len q2)) + (len q2) by A22, XREAL_1:7; then A25: (len q1) + i in dom P by A19, FINSEQ_3:25; q2 . i = (q1 ^ q2) . ((len q1) + i) by A18, A24, FINSEQ_1:65; hence [(q2 . i),(q2 . (i + 1))] in R by A1, A21, A25, A23, REWRITE1:def_2; ::_thesis: verum end; hence q2 is RedSequence of R by A3, REWRITE1:def_2; ::_thesis: verum end; theorem Th5: :: REWRITE3:5 for R being Relation for P being RedSequence of R st len P > 1 holds ex Q being RedSequence of R st ( <*(P . 1)*> ^ Q = P & (len Q) + 1 = len P ) proof let R be Relation; ::_thesis: for P being RedSequence of R st len P > 1 holds ex Q being RedSequence of R st ( <*(P . 1)*> ^ Q = P & (len Q) + 1 = len P ) let P be RedSequence of R; ::_thesis: ( len P > 1 implies ex Q being RedSequence of R st ( <*(P . 1)*> ^ Q = P & (len Q) + 1 = len P ) ) assume A1: len P > 1 ; ::_thesis: ex Q being RedSequence of R st ( <*(P . 1)*> ^ Q = P & (len Q) + 1 = len P ) consider x being set , Q being FinSequence such that A2: P = <*x*> ^ Q and A3: len P = (len Q) + 1 by REWRITE1:5; 1 + (len Q) > 1 + 0 by A1, A3; then ( len <*x*> = 1 & len Q > 0 ) by FINSEQ_1:39; then A4: Q is RedSequence of R by A2, Th4; P . 1 = x by A2, FINSEQ_1:41; hence ex Q being RedSequence of R st ( <*(P . 1)*> ^ Q = P & (len Q) + 1 = len P ) by A2, A3, A4; ::_thesis: verum end; theorem :: REWRITE3:6 for R being Relation for P being RedSequence of R st len P > 1 holds ex Q being RedSequence of R st ( Q ^ <*(P . (len P))*> = P & (len Q) + 1 = len P ) proof let R be Relation; ::_thesis: for P being RedSequence of R st len P > 1 holds ex Q being RedSequence of R st ( Q ^ <*(P . (len P))*> = P & (len Q) + 1 = len P ) let P be RedSequence of R; ::_thesis: ( len P > 1 implies ex Q being RedSequence of R st ( Q ^ <*(P . (len P))*> = P & (len Q) + 1 = len P ) ) assume A1: len P > 1 ; ::_thesis: ex Q being RedSequence of R st ( Q ^ <*(P . (len P))*> = P & (len Q) + 1 = len P ) consider Q being FinSequence, x being set such that A2: P = Q ^ <*x*> and A3: (len Q) + 1 = len P by Th2; 1 + (len Q) > 1 + 0 by A1, A3; then ( len <*x*> = 1 & len Q > 0 ) by FINSEQ_1:39; then A4: Q is RedSequence of R by A2, Th4; P . (len P) = x by A2, A3, FINSEQ_1:42; hence ex Q being RedSequence of R st ( Q ^ <*(P . (len P))*> = P & (len Q) + 1 = len P ) by A2, A3, A4; ::_thesis: verum end; theorem :: REWRITE3:7 for R being Relation for P being RedSequence of R st len P > 1 holds ex Q being RedSequence of R st ( (len Q) + 1 = len P & ( for k being Nat st k in dom Q holds Q . k = P . (k + 1) ) ) proof let R be Relation; ::_thesis: for P being RedSequence of R st len P > 1 holds ex Q being RedSequence of R st ( (len Q) + 1 = len P & ( for k being Nat st k in dom Q holds Q . k = P . (k + 1) ) ) let P be RedSequence of R; ::_thesis: ( len P > 1 implies ex Q being RedSequence of R st ( (len Q) + 1 = len P & ( for k being Nat st k in dom Q holds Q . k = P . (k + 1) ) ) ) assume len P > 1 ; ::_thesis: ex Q being RedSequence of R st ( (len Q) + 1 = len P & ( for k being Nat st k in dom Q holds Q . k = P . (k + 1) ) ) then consider Q being RedSequence of R such that A1: ( P = <*(P . 1)*> ^ Q & (len Q) + 1 = len P ) by Th5; take Q ; ::_thesis: ( (len Q) + 1 = len P & ( for k being Nat st k in dom Q holds Q . k = P . (k + 1) ) ) thus ( (len Q) + 1 = len P & ( for k being Nat st k in dom Q holds Q . k = P . (k + 1) ) ) by A1, Th1; ::_thesis: verum end; theorem Th8: :: REWRITE3:8 for x, y being set for R being Relation st <*x,y*> is RedSequence of R holds [x,y] in R proof let x, y be set ; ::_thesis: for R being Relation st <*x,y*> is RedSequence of R holds [x,y] in R let R be Relation; ::_thesis: ( <*x,y*> is RedSequence of R implies [x,y] in R ) set P = <*x,y*>; A1: ( <*x,y*> . 1 = x & <*x,y*> . 2 = y ) by FINSEQ_1:44; len <*x,y*> = 2 by FINSEQ_1:44; then A2: ( 1 in dom <*x,y*> & 1 + 1 in dom <*x,y*> ) by FINSEQ_3:25; assume <*x,y*> is RedSequence of R ; ::_thesis: [x,y] in R hence [x,y] in R by A1, A2, REWRITE1:def_2; ::_thesis: verum end; begin theorem Th9: :: REWRITE3:9 for E being non empty set for w, u, v being Element of E ^omega st w = u ^ v holds ( len u <= len w & len v <= len w ) proof let E be non empty set ; ::_thesis: for w, u, v being Element of E ^omega st w = u ^ v holds ( len u <= len w & len v <= len w ) let w, u, v be Element of E ^omega ; ::_thesis: ( w = u ^ v implies ( len u <= len w & len v <= len w ) ) assume w = u ^ v ; ::_thesis: ( len u <= len w & len v <= len w ) then len w = (len u) + (len v) by AFINSQ_1:17; then ( (len w) + (len u) >= ((len u) + (len v)) + 0 & (len w) + (len v) >= ((len u) + (len v)) + 0 ) by XREAL_1:7; hence ( len u <= len w & len v <= len w ) by XREAL_1:6; ::_thesis: verum end; theorem Th10: :: REWRITE3:10 for E being non empty set for w, u, v being Element of E ^omega st w = u ^ v & u <> <%> E & v <> <%> E holds ( len u < len w & len v < len w ) proof let E be non empty set ; ::_thesis: for w, u, v being Element of E ^omega st w = u ^ v & u <> <%> E & v <> <%> E holds ( len u < len w & len v < len w ) let w, u, v be Element of E ^omega ; ::_thesis: ( w = u ^ v & u <> <%> E & v <> <%> E implies ( len u < len w & len v < len w ) ) assume that A1: w = u ^ v and A2: u <> <%> E and A3: v <> <%> E ; ::_thesis: ( len u < len w & len v < len w ) A4: len w = (len u) + (len v) by A1, AFINSQ_1:17; then (len w) + (len u) > ((len u) + (len v)) + 0 by A2, XREAL_1:8; hence ( len u < len w & len v < len w ) by A3, A4, XREAL_1:6, XREAL_1:8; ::_thesis: verum end; theorem :: REWRITE3:11 for E being non empty set for w1, v1, w2, v2 being Element of E ^omega st w1 ^ v1 = w2 ^ v2 & ( len w1 = len w2 or len v1 = len v2 ) holds ( w1 = w2 & v1 = v2 ) proof let E be non empty set ; ::_thesis: for w1, v1, w2, v2 being Element of E ^omega st w1 ^ v1 = w2 ^ v2 & ( len w1 = len w2 or len v1 = len v2 ) holds ( w1 = w2 & v1 = v2 ) let w1, v1, w2, v2 be Element of E ^omega ; ::_thesis: ( w1 ^ v1 = w2 ^ v2 & ( len w1 = len w2 or len v1 = len v2 ) implies ( w1 = w2 & v1 = v2 ) ) assume that A1: w1 ^ v1 = w2 ^ v2 and A2: ( len w1 = len w2 or len v1 = len v2 ) ; ::_thesis: ( w1 = w2 & v1 = v2 ) A3: (len w1) + (len v1) = len (w2 ^ v2) by A1, AFINSQ_1:17 .= (len w2) + (len v2) by AFINSQ_1:17 ; now__::_thesis:_for_k_being_Nat_st_k_in_dom_w1_holds_ w1_._k_=_w2_._k let k be Nat; ::_thesis: ( k in dom w1 implies w1 . k = w2 . k ) assume A4: k in dom w1 ; ::_thesis: w1 . k = w2 . k hence w1 . k = (w2 ^ v2) . k by A1, AFINSQ_1:def_3 .= w2 . k by A2, A3, A4, AFINSQ_1:def_3 ; ::_thesis: verum end; hence w1 = w2 by A2, A3, AFINSQ_1:8; ::_thesis: v1 = v2 hence v1 = v2 by A1, AFINSQ_1:28; ::_thesis: verum end; theorem Th12: :: REWRITE3:12 for E being non empty set for w1, v1, w2, v2 being Element of E ^omega st w1 ^ v1 = w2 ^ v2 & ( len w1 <= len w2 or len v1 >= len v2 ) holds ex u being Element of E ^omega st ( w1 ^ u = w2 & v1 = u ^ v2 ) proof let E be non empty set ; ::_thesis: for w1, v1, w2, v2 being Element of E ^omega st w1 ^ v1 = w2 ^ v2 & ( len w1 <= len w2 or len v1 >= len v2 ) holds ex u being Element of E ^omega st ( w1 ^ u = w2 & v1 = u ^ v2 ) let w1, v1, w2, v2 be Element of E ^omega ; ::_thesis: ( w1 ^ v1 = w2 ^ v2 & ( len w1 <= len w2 or len v1 >= len v2 ) implies ex u being Element of E ^omega st ( w1 ^ u = w2 & v1 = u ^ v2 ) ) assume that A1: w1 ^ v1 = w2 ^ v2 and A2: ( len w1 <= len w2 or len v1 >= len v2 ) ; ::_thesis: ex u being Element of E ^omega st ( w1 ^ u = w2 & v1 = u ^ v2 ) (len w1) + (len v1) = len (w2 ^ v2) by A1, AFINSQ_1:17 .= (len w2) + (len v2) by AFINSQ_1:17 ; then ( len v1 >= len v2 implies ((len w1) + (len v1)) - (len v1) <= ((len w2) + (len v2)) - (len v2) ) by XREAL_1:13; then consider u9 being XFinSequence such that A3: w1 ^ u9 = w2 by A1, A2, AFINSQ_1:41; reconsider u = u9 as Element of E ^omega by A3, FLANG_1:5; take u ; ::_thesis: ( w1 ^ u = w2 & v1 = u ^ v2 ) thus w1 ^ u = w2 by A3; ::_thesis: v1 = u ^ v2 w2 ^ v2 = w1 ^ (u ^ v2) by A3, AFINSQ_1:27; hence v1 = u ^ v2 by A1, AFINSQ_1:28; ::_thesis: verum end; theorem Th13: :: REWRITE3:13 for E being non empty set for w1, v1, w2, v2 being Element of E ^omega holds ( not w1 ^ v1 = w2 ^ v2 or ex u being Element of E ^omega st ( w1 ^ u = w2 & v1 = u ^ v2 ) or ex u being Element of E ^omega st ( w2 ^ u = w1 & v2 = u ^ v1 ) ) proof let E be non empty set ; ::_thesis: for w1, v1, w2, v2 being Element of E ^omega holds ( not w1 ^ v1 = w2 ^ v2 or ex u being Element of E ^omega st ( w1 ^ u = w2 & v1 = u ^ v2 ) or ex u being Element of E ^omega st ( w2 ^ u = w1 & v2 = u ^ v1 ) ) let w1, v1, w2, v2 be Element of E ^omega ; ::_thesis: ( not w1 ^ v1 = w2 ^ v2 or ex u being Element of E ^omega st ( w1 ^ u = w2 & v1 = u ^ v2 ) or ex u being Element of E ^omega st ( w2 ^ u = w1 & v2 = u ^ v1 ) ) A1: ( len w1 < len w2 or len w1 >= len w2 ) ; assume w1 ^ v1 = w2 ^ v2 ; ::_thesis: ( ex u being Element of E ^omega st ( w1 ^ u = w2 & v1 = u ^ v2 ) or ex u being Element of E ^omega st ( w2 ^ u = w1 & v2 = u ^ v1 ) ) hence ( ex u being Element of E ^omega st ( w1 ^ u = w2 & v1 = u ^ v2 ) or ex u being Element of E ^omega st ( w2 ^ u = w1 & v2 = u ^ v1 ) ) by A1, Th12; ::_thesis: verum end; begin definition let X be set ; attrc2 is strict ; struct transition-system over X -> 1-sorted ; aggrtransition-system(# carrier, Tran #) -> transition-system over X; sel Tran c2 -> Relation of [: the carrier of c2,X:], the carrier of c2; end; definition let E be non empty set ; let F be Subset of (E ^omega); let TS be transition-system over F; attrTS is deterministic means :Def1: :: REWRITE3:def 1 ( the Tran of TS is Function & not <%> E in rng (dom the Tran of TS) & ( for s being Element of TS for u, v being Element of E ^omega st u <> v & [s,u] in dom the Tran of TS & [s,v] in dom the Tran of TS holds for w being Element of E ^omega holds ( not u ^ w = v & not v ^ w = u ) ) ); end; :: deftheorem Def1 defines deterministic REWRITE3:def_1_:_ for E being non empty set for F being Subset of (E ^omega) for TS being transition-system over F holds ( TS is deterministic iff ( the Tran of TS is Function & not <%> E in rng (dom the Tran of TS) & ( for s being Element of TS for u, v being Element of E ^omega st u <> v & [s,u] in dom the Tran of TS & [s,v] in dom the Tran of TS holds for w being Element of E ^omega holds ( not u ^ w = v & not v ^ w = u ) ) ) ); theorem Th14: :: REWRITE3:14 for E being non empty set for F being Subset of (E ^omega) for TS being transition-system over F st dom the Tran of TS = {} holds TS is deterministic proof let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being transition-system over F st dom the Tran of TS = {} holds TS is deterministic let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st dom the Tran of TS = {} holds TS is deterministic let TS be transition-system over F; ::_thesis: ( dom the Tran of TS = {} implies TS is deterministic ) assume dom the Tran of TS = {} ; ::_thesis: TS is deterministic then ( the Tran of TS = {} & ( for s being Element of TS for u, v being Element of E ^omega st u <> v & [s,u] in dom the Tran of TS & [s,v] in dom the Tran of TS holds for w being Element of E ^omega holds ( not u ^ w = v & not v ^ w = u ) ) ) ; hence TS is deterministic by Def1, RELAT_1:38; ::_thesis: verum end; registration let E be non empty set ; let F be Subset of (E ^omega); cluster non empty finite strict deterministic for transition-system over F; existence ex b1 being transition-system over F st ( b1 is strict & not b1 is empty & b1 is finite & b1 is deterministic ) proof set X = the non empty finite set ; reconsider T = {} as Relation of [: the non empty finite set ,F:], the non empty finite set by RELSET_1:12; take TS = transition-system(# the non empty finite set ,T #); ::_thesis: ( TS is strict & not TS is empty & TS is finite & TS is deterministic ) thus TS is strict ; ::_thesis: ( not TS is empty & TS is finite & TS is deterministic ) thus not TS is empty ; ::_thesis: ( TS is finite & TS is deterministic ) thus the carrier of TS is finite ; :: according to STRUCT_0:def_11 ::_thesis: TS is deterministic thus TS is deterministic by Th14, RELAT_1:38; ::_thesis: verum end; end; begin definition let X be set ; let TS be transition-system over X; let x, y, z be set ; predx,y -->. z,TS means :Def2: :: REWRITE3:def 2 [[x,y],z] in the Tran of TS; end; :: deftheorem Def2 defines -->. REWRITE3:def_2_:_ for X being set for TS being transition-system over X for x, y, z being set holds ( x,y -->. z,TS iff [[x,y],z] in the Tran of TS ); theorem Th15: :: REWRITE3:15 for X, x, y, z being set for TS being transition-system over X st x,y -->. z,TS holds ( x in TS & y in X & z in TS & x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS ) proof let X, x, y, z be set ; ::_thesis: for TS being transition-system over X st x,y -->. z,TS holds ( x in TS & y in X & z in TS & x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS ) let TS be transition-system over X; ::_thesis: ( x,y -->. z,TS implies ( x in TS & y in X & z in TS & x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS ) ) assume x,y -->. z,TS ; ::_thesis: ( x in TS & y in X & z in TS & x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS ) then A1: [[x,y],z] in the Tran of TS by Def2; then [x,y] in [: the carrier of TS,X:] by ZFMISC_1:87; hence ( x in the carrier of TS & y in X & z in the carrier of TS ) by A1, ZFMISC_1:87; :: according to STRUCT_0:def_5 ::_thesis: ( x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS ) [x,y] in dom the Tran of TS by A1, XTUPLE_0:def_12; hence ( x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) ) by XTUPLE_0:def_12, XTUPLE_0:def_13; ::_thesis: z in rng the Tran of TS thus z in rng the Tran of TS by A1, XTUPLE_0:def_13; ::_thesis: verum end; theorem Th16: :: REWRITE3:16 for X1, X2, x, y, z being set for TS1 being transition-system over X1 for TS2 being transition-system over X2 st the Tran of TS1 = the Tran of TS2 & x,y -->. z,TS1 holds x,y -->. z,TS2 proof let X1, X2, x, y, z be set ; ::_thesis: for TS1 being transition-system over X1 for TS2 being transition-system over X2 st the Tran of TS1 = the Tran of TS2 & x,y -->. z,TS1 holds x,y -->. z,TS2 let TS1 be transition-system over X1; ::_thesis: for TS2 being transition-system over X2 st the Tran of TS1 = the Tran of TS2 & x,y -->. z,TS1 holds x,y -->. z,TS2 let TS2 be transition-system over X2; ::_thesis: ( the Tran of TS1 = the Tran of TS2 & x,y -->. z,TS1 implies x,y -->. z,TS2 ) assume A1: the Tran of TS1 = the Tran of TS2 ; ::_thesis: ( not x,y -->. z,TS1 or x,y -->. z,TS2 ) assume x,y -->. z,TS1 ; ::_thesis: x,y -->. z,TS2 then [[x,y],z] in the Tran of TS1 by Def2; hence x,y -->. z,TS2 by A1, Def2; ::_thesis: verum end; theorem Th17: :: REWRITE3:17 for x, y, z1, z2 being set for E being non empty set for F being Subset of (E ^omega) for TS being transition-system over F st the Tran of TS is Function & x,y -->. z1,TS & x,y -->. z2,TS holds z1 = z2 proof let x, y, z1, z2 be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being transition-system over F st the Tran of TS is Function & x,y -->. z1,TS & x,y -->. z2,TS holds z1 = z2 let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being transition-system over F st the Tran of TS is Function & x,y -->. z1,TS & x,y -->. z2,TS holds z1 = z2 let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st the Tran of TS is Function & x,y -->. z1,TS & x,y -->. z2,TS holds z1 = z2 let TS be transition-system over F; ::_thesis: ( the Tran of TS is Function & x,y -->. z1,TS & x,y -->. z2,TS implies z1 = z2 ) assume A1: the Tran of TS is Function ; ::_thesis: ( not x,y -->. z1,TS or not x,y -->. z2,TS or z1 = z2 ) assume ( x,y -->. z1,TS & x,y -->. z2,TS ) ; ::_thesis: z1 = z2 then ( [[x,y],z1] in the Tran of TS & [[x,y],z2] in the Tran of TS ) by Def2; hence z1 = z2 by A1, FUNCT_1:def_1; ::_thesis: verum end; theorem :: REWRITE3:18 for x, y being set for E being non empty set for F being Subset of (E ^omega) for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds not x, <%> E -->. y,TS proof let x, y be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds not x, <%> E -->. y,TS let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds not x, <%> E -->. y,TS let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds not x, <%> E -->. y,TS let TS be transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies not x, <%> E -->. y,TS ) assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: not x, <%> E -->. y,TS assume x, <%> E -->. y,TS ; ::_thesis: contradiction then [[x,(<%> E)],y] in the Tran of TS by Def2; then [x,(<%> E)] in dom the Tran of TS by XTUPLE_0:def_12; hence contradiction by A1, XTUPLE_0:def_13; ::_thesis: verum end; theorem Th19: :: REWRITE3:19 for x, z1, z2 being set for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being deterministic transition-system over F st u <> v & x,u -->. z1,TS & x,v -->. z2,TS holds for w being Element of E ^omega holds ( not u ^ w = v & not v ^ w = u ) proof let x, z1, z2 be set ; ::_thesis: for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being deterministic transition-system over F st u <> v & x,u -->. z1,TS & x,v -->. z2,TS holds for w being Element of E ^omega holds ( not u ^ w = v & not v ^ w = u ) let E be non empty set ; ::_thesis: for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being deterministic transition-system over F st u <> v & x,u -->. z1,TS & x,v -->. z2,TS holds for w being Element of E ^omega holds ( not u ^ w = v & not v ^ w = u ) let u, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being deterministic transition-system over F st u <> v & x,u -->. z1,TS & x,v -->. z2,TS holds for w being Element of E ^omega holds ( not u ^ w = v & not v ^ w = u ) let F be Subset of (E ^omega); ::_thesis: for TS being deterministic transition-system over F st u <> v & x,u -->. z1,TS & x,v -->. z2,TS holds for w being Element of E ^omega holds ( not u ^ w = v & not v ^ w = u ) let TS be deterministic transition-system over F; ::_thesis: ( u <> v & x,u -->. z1,TS & x,v -->. z2,TS implies for w being Element of E ^omega holds ( not u ^ w = v & not v ^ w = u ) ) assume that A1: u <> v and A2: x,u -->. z1,TS and A3: x,v -->. z2,TS ; ::_thesis: for w being Element of E ^omega holds ( not u ^ w = v & not v ^ w = u ) x in TS by A2, Th15; then reconsider x = x as Element of TS by STRUCT_0:def_5; [[x,v],z2] in the Tran of TS by A3, Def2; then A4: [x,v] in dom the Tran of TS by XTUPLE_0:def_12; [[x,u],z1] in the Tran of TS by A2, Def2; then [x,u] in dom the Tran of TS by XTUPLE_0:def_12; hence for w being Element of E ^omega holds ( not u ^ w = v & not v ^ w = u ) by A1, A4, Def1; ::_thesis: verum end; begin definition let E be non empty set ; let F be Subset of (E ^omega); let TS be transition-system over F; let x1, x2, y1, y2 be set ; predx1,x2 ==>. y1,y2,TS means :Def3: :: REWRITE3:def 3 ex v, w being Element of E ^omega st ( v = y2 & x1,w -->. y1,TS & x2 = w ^ v ); end; :: deftheorem Def3 defines ==>. REWRITE3:def_3_:_ for E being non empty set for F being Subset of (E ^omega) for TS being transition-system over F for x1, x2, y1, y2 being set holds ( x1,x2 ==>. y1,y2,TS iff ex v, w being Element of E ^omega st ( v = y2 & x1,w -->. y1,TS & x2 = w ^ v ) ); theorem Th20: :: REWRITE3:20 for x1, x2, y1, y2 being set for E being non empty set for F being Subset of (E ^omega) for TS being transition-system over F st x1,x2 ==>. y1,y2,TS holds ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) proof let x1, x2, y1, y2 be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being transition-system over F st x1,x2 ==>. y1,y2,TS holds ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being transition-system over F st x1,x2 ==>. y1,y2,TS holds ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st x1,x2 ==>. y1,y2,TS holds ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) let TS be transition-system over F; ::_thesis: ( x1,x2 ==>. y1,y2,TS implies ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) ) assume x1,x2 ==>. y1,y2,TS ; ::_thesis: ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) then ex v, w being Element of E ^omega st ( v = y2 & x1,w -->. y1,TS & x2 = w ^ v ) by Def3; hence ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) by Th15; ::_thesis: verum end; theorem Th21: :: REWRITE3:21 for x1, x2, y1, y2 being set for E being non empty set for F1, F2 being Subset of (E ^omega) for TS1 being transition-system over F1 for TS2 being transition-system over F2 st the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 holds x1,x2 ==>. y1,y2,TS2 proof let x1, x2, y1, y2 be set ; ::_thesis: for E being non empty set for F1, F2 being Subset of (E ^omega) for TS1 being transition-system over F1 for TS2 being transition-system over F2 st the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 holds x1,x2 ==>. y1,y2,TS2 let E be non empty set ; ::_thesis: for F1, F2 being Subset of (E ^omega) for TS1 being transition-system over F1 for TS2 being transition-system over F2 st the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 holds x1,x2 ==>. y1,y2,TS2 let F1, F2 be Subset of (E ^omega); ::_thesis: for TS1 being transition-system over F1 for TS2 being transition-system over F2 st the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 holds x1,x2 ==>. y1,y2,TS2 let TS1 be transition-system over F1; ::_thesis: for TS2 being transition-system over F2 st the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 holds x1,x2 ==>. y1,y2,TS2 let TS2 be transition-system over F2; ::_thesis: ( the Tran of TS1 = the Tran of TS2 & x1,x2 ==>. y1,y2,TS1 implies x1,x2 ==>. y1,y2,TS2 ) assume that A1: the Tran of TS1 = the Tran of TS2 and A2: x1,x2 ==>. y1,y2,TS1 ; ::_thesis: x1,x2 ==>. y1,y2,TS2 consider v, w being Element of E ^omega such that A3: ( v = y2 & x1,w -->. y1,TS1 & x2 = w ^ v ) by A2, Def3; take v ; :: according to REWRITE3:def_3 ::_thesis: ex w being Element of E ^omega st ( v = y2 & x1,w -->. y1,TS2 & x2 = w ^ v ) take w ; ::_thesis: ( v = y2 & x1,w -->. y1,TS2 & x2 = w ^ v ) thus ( v = y2 & x1,w -->. y1,TS2 & x2 = w ^ v ) by A1, A3, Th16; ::_thesis: verum end; theorem Th22: :: REWRITE3:22 for x, y being set for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being transition-system over F st x,u ==>. y,v,TS holds ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) proof let x, y be set ; ::_thesis: for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being transition-system over F st x,u ==>. y,v,TS holds ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) let E be non empty set ; ::_thesis: for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being transition-system over F st x,u ==>. y,v,TS holds ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) let u, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being transition-system over F st x,u ==>. y,v,TS holds ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st x,u ==>. y,v,TS holds ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) let TS be transition-system over F; ::_thesis: ( x,u ==>. y,v,TS implies ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) ) assume x,u ==>. y,v,TS ; ::_thesis: ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) then consider v1, w being Element of E ^omega such that A1: ( v1 = v & x,w -->. y,TS & u = w ^ v1 ) by Def3; take w ; ::_thesis: ( x,w -->. y,TS & u = w ^ v ) thus ( x,w -->. y,TS & u = w ^ v ) by A1; ::_thesis: verum end; theorem Th23: :: REWRITE3:23 for x, y, z being set for E being non empty set for F being Subset of (E ^omega) for TS being transition-system over F holds ( x,y -->. z,TS iff x,y ==>. z, <%> E,TS ) proof let x, y, z be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being transition-system over F holds ( x,y -->. z,TS iff x,y ==>. z, <%> E,TS ) let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being transition-system over F holds ( x,y -->. z,TS iff x,y ==>. z, <%> E,TS ) let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F holds ( x,y -->. z,TS iff x,y ==>. z, <%> E,TS ) let TS be transition-system over F; ::_thesis: ( x,y -->. z,TS iff x,y ==>. z, <%> E,TS ) thus ( x,y -->. z,TS implies x,y ==>. z, <%> E,TS ) ::_thesis: ( x,y ==>. z, <%> E,TS implies x,y -->. z,TS ) proof assume A1: x,y -->. z,TS ; ::_thesis: x,y ==>. z, <%> E,TS then y in F by Th15; then reconsider w = y as Element of E ^omega ; w = w ^ {} ; hence x,y ==>. z, <%> E,TS by A1, Def3; ::_thesis: verum end; B: for w being Element of E ^omega holds w ^ {} = w ; assume x,y ==>. z, <%> E,TS ; ::_thesis: x,y -->. z,TS then ex v, w being Element of E ^omega st ( v = <%> E & x,w -->. z,TS & y = w ^ v ) by Def3; hence x,y -->. z,TS by B; ::_thesis: verum end; theorem Th24: :: REWRITE3:24 for x, y being set for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being transition-system over F holds ( x,v -->. y,TS iff x,v ^ w ==>. y,w,TS ) proof let x, y be set ; ::_thesis: for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being transition-system over F holds ( x,v -->. y,TS iff x,v ^ w ==>. y,w,TS ) let E be non empty set ; ::_thesis: for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being transition-system over F holds ( x,v -->. y,TS iff x,v ^ w ==>. y,w,TS ) let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being transition-system over F holds ( x,v -->. y,TS iff x,v ^ w ==>. y,w,TS ) let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F holds ( x,v -->. y,TS iff x,v ^ w ==>. y,w,TS ) let TS be transition-system over F; ::_thesis: ( x,v -->. y,TS iff x,v ^ w ==>. y,w,TS ) thus ( x,v -->. y,TS implies x,v ^ w ==>. y,w,TS ) by Def3; ::_thesis: ( x,v ^ w ==>. y,w,TS implies x,v -->. y,TS ) assume x,v ^ w ==>. y,w,TS ; ::_thesis: x,v -->. y,TS then ex u being Element of E ^omega st ( x,u -->. y,TS & v ^ w = u ^ w ) by Th22; hence x,v -->. y,TS by AFINSQ_1:28; ::_thesis: verum end; theorem Th25: :: REWRITE3:25 for x, y being set for E being non empty set for u, v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being transition-system over F st x,u ==>. y,v,TS holds x,u ^ w ==>. y,v ^ w,TS proof let x, y be set ; ::_thesis: for E being non empty set for u, v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being transition-system over F st x,u ==>. y,v,TS holds x,u ^ w ==>. y,v ^ w,TS let E be non empty set ; ::_thesis: for u, v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being transition-system over F st x,u ==>. y,v,TS holds x,u ^ w ==>. y,v ^ w,TS let u, v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being transition-system over F st x,u ==>. y,v,TS holds x,u ^ w ==>. y,v ^ w,TS let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st x,u ==>. y,v,TS holds x,u ^ w ==>. y,v ^ w,TS let TS be transition-system over F; ::_thesis: ( x,u ==>. y,v,TS implies x,u ^ w ==>. y,v ^ w,TS ) assume x,u ==>. y,v,TS ; ::_thesis: x,u ^ w ==>. y,v ^ w,TS then consider u1 being Element of E ^omega such that A1: x,u1 -->. y,TS and A2: u = u1 ^ v by Th22; u ^ w = u1 ^ (v ^ w) by A2, AFINSQ_1:27; hence x,u ^ w ==>. y,v ^ w,TS by A1, Def3; ::_thesis: verum end; theorem Th26: :: REWRITE3:26 for x, y being set for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being transition-system over F st x,u ==>. y,v,TS holds len u >= len v proof let x, y be set ; ::_thesis: for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being transition-system over F st x,u ==>. y,v,TS holds len u >= len v let E be non empty set ; ::_thesis: for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being transition-system over F st x,u ==>. y,v,TS holds len u >= len v let u, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being transition-system over F st x,u ==>. y,v,TS holds len u >= len v let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st x,u ==>. y,v,TS holds len u >= len v let TS be transition-system over F; ::_thesis: ( x,u ==>. y,v,TS implies len u >= len v ) assume x,u ==>. y,v,TS ; ::_thesis: len u >= len v then ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) by Th22; hence len u >= len v by Th9; ::_thesis: verum end; theorem Th27: :: REWRITE3:27 for x1, x2, y1, z, y2 being set for E being non empty set for F being Subset of (E ^omega) for TS being transition-system over F st the Tran of TS is Function & x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS holds y1 = y2 proof let x1, x2, y1, z, y2 be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being transition-system over F st the Tran of TS is Function & x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS holds y1 = y2 let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being transition-system over F st the Tran of TS is Function & x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS holds y1 = y2 let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st the Tran of TS is Function & x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS holds y1 = y2 let TS be transition-system over F; ::_thesis: ( the Tran of TS is Function & x1,x2 ==>. y1,z,TS & x1,x2 ==>. y2,z,TS implies y1 = y2 ) assume A1: the Tran of TS is Function ; ::_thesis: ( not x1,x2 ==>. y1,z,TS or not x1,x2 ==>. y2,z,TS or y1 = y2 ) assume that A2: x1,x2 ==>. y1,z,TS and A3: x1,x2 ==>. y2,z,TS ; ::_thesis: y1 = y2 consider v1, w1 being Element of E ^omega such that A4: v1 = z and A5: x1,w1 -->. y1,TS and A6: x2 = w1 ^ v1 by A2, Def3; consider v2, w2 being Element of E ^omega such that A7: v2 = z and A8: x1,w2 -->. y2,TS and A9: x2 = w2 ^ v2 by A3, Def3; w1 = w2 by A4, A6, A7, A9, AFINSQ_1:28; hence y1 = y2 by A1, A5, A8, Th17; ::_thesis: verum end; theorem Th28: :: REWRITE3:28 for x, z, y being set for E being non empty set for F being Subset of (E ^omega) for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds not x,z ==>. y,z,TS proof let x, z, y be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds not x,z ==>. y,z,TS let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds not x,z ==>. y,z,TS let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) holds not x,z ==>. y,z,TS let TS be transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies not x,z ==>. y,z,TS ) assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: not x,z ==>. y,z,TS assume x,z ==>. y,z,TS ; ::_thesis: contradiction then consider v, w being Element of E ^omega such that A2: v = z and A3: x,w -->. y,TS and A4: z = w ^ v by Def3; [[x,w],y] in the Tran of TS by A3, Def2; then A5: [x,w] in dom the Tran of TS by XTUPLE_0:def_12; w = <%> E by A2, A4, FLANG_2:4; hence contradiction by A1, A5, XTUPLE_0:def_13; ::_thesis: verum end; theorem Th29: :: REWRITE3:29 for x, y being set for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) & x,u ==>. y,v,TS holds len u > len v proof let x, y be set ; ::_thesis: for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) & x,u ==>. y,v,TS holds len u > len v let E be non empty set ; ::_thesis: for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) & x,u ==>. y,v,TS holds len u > len v let u, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) & x,u ==>. y,v,TS holds len u > len v let F be Subset of (E ^omega); ::_thesis: for TS being transition-system over F st not <%> E in rng (dom the Tran of TS) & x,u ==>. y,v,TS holds len u > len v let TS be transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) & x,u ==>. y,v,TS implies len u > len v ) assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: ( not x,u ==>. y,v,TS or len u > len v ) assume A2: x,u ==>. y,v,TS ; ::_thesis: len u > len v then consider w being Element of E ^omega such that A3: x,w -->. y,TS and A4: u = w ^ v by Th22; A5: w in rng (dom the Tran of TS) by A3, Th15; percases ( v = <%> E or v <> <%> E ) ; supposeA6: v = <%> E ; ::_thesis: len u > len v then u <> <%> E by A1, A2, Th28; then len u > 0 ; hence len u > len v by A6; ::_thesis: verum end; suppose v <> <%> E ; ::_thesis: len u > len v hence len u > len v by A1, A4, A5, Th10; ::_thesis: verum end; end; end; theorem Th30: :: REWRITE3:30 for x1, x2, y1, z1, y2, z2 being set for E being non empty set for F being Subset of (E ^omega) for TS being deterministic transition-system over F st x1,x2 ==>. y1,z1,TS & x1,x2 ==>. y2,z2,TS holds ( y1 = y2 & z1 = z2 ) proof let x1, x2, y1, z1, y2, z2 be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being deterministic transition-system over F st x1,x2 ==>. y1,z1,TS & x1,x2 ==>. y2,z2,TS holds ( y1 = y2 & z1 = z2 ) let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being deterministic transition-system over F st x1,x2 ==>. y1,z1,TS & x1,x2 ==>. y2,z2,TS holds ( y1 = y2 & z1 = z2 ) let F be Subset of (E ^omega); ::_thesis: for TS being deterministic transition-system over F st x1,x2 ==>. y1,z1,TS & x1,x2 ==>. y2,z2,TS holds ( y1 = y2 & z1 = z2 ) let TS be deterministic transition-system over F; ::_thesis: ( x1,x2 ==>. y1,z1,TS & x1,x2 ==>. y2,z2,TS implies ( y1 = y2 & z1 = z2 ) ) assume that A1: x1,x2 ==>. y1,z1,TS and A2: x1,x2 ==>. y2,z2,TS ; ::_thesis: ( y1 = y2 & z1 = z2 ) consider v2, w2 being Element of E ^omega such that A3: v2 = z2 and A4: x1,w2 -->. y2,TS and A5: x2 = w2 ^ v2 by A2, Def3; consider v1, w1 being Element of E ^omega such that A6: v1 = z1 and A7: x1,w1 -->. y1,TS and A8: x2 = w1 ^ v1 by A1, Def3; A9: the Tran of TS is Function by Def1; ( ex u9 being Element of E ^omega st ( w1 ^ u9 = w2 & v1 = u9 ^ v2 ) or ex u9 being Element of E ^omega st ( w2 ^ u9 = w1 & v2 = u9 ^ v1 ) ) by A8, A5, Th13; then w1 = w2 by A7, A4, Th19; then v1 = v2 by A8, A5, AFINSQ_1:28; hence ( y1 = y2 & z1 = z2 ) by A1, A2, A6, A3, A9, Th27; ::_thesis: verum end; begin definition let E be non empty set ; let F be Subset of (E ^omega); let TS be non empty transition-system over F; func ==>.-relation TS -> Relation of [: the carrier of TS,(E ^omega):] means :Def4: :: REWRITE3:def 4 for x1, x2, y1, y2 being set holds ( [[x1,x2],[y1,y2]] in it iff x1,x2 ==>. y1,y2,TS ); existence ex b1 being Relation of [: the carrier of TS,(E ^omega):] st for x1, x2, y1, y2 being set holds ( [[x1,x2],[y1,y2]] in b1 iff x1,x2 ==>. y1,y2,TS ) proof defpred S1[ Element of [: the carrier of TS,(E ^omega):], Element of [: the carrier of TS,(E ^omega):]] means ex x1, x2, y1, y2 being set st ( [x1,x2] = \$1 & [y1,y2] = \$2 & x1,x2 ==>. y1,y2,TS ); consider R being Relation of [: the carrier of TS,(E ^omega):] such that A1: for s, t being Element of [: the carrier of TS,(E ^omega):] holds ( [s,t] in R iff S1[s,t] ) from RELSET_1:sch_2(); take R ; ::_thesis: for x1, x2, y1, y2 being set holds ( [[x1,x2],[y1,y2]] in R iff x1,x2 ==>. y1,y2,TS ) now__::_thesis:_for_x1,_x2,_y1,_y2_being_set_holds_ (_(_x1,x2_==>._y1,y2,TS_implies_[[x1,x2],[y1,y2]]_in_R_)_&_(_[[x1,x2],[y1,y2]]_in_R_implies_x1,x2_==>._y1,y2,TS_)_) let x1, x2, y1, y2 be set ; ::_thesis: ( ( x1,x2 ==>. y1,y2,TS implies [[x1,x2],[y1,y2]] in R ) & ( [[x1,x2],[y1,y2]] in R implies x1,x2 ==>. y1,y2,TS ) ) set s = [x1,x2]; set t = [y1,y2]; A2: ( dom R c= [: the carrier of TS,(E ^omega):] & rng R c= [: the carrier of TS,(E ^omega):] ) by RELAT_1:def_18, RELAT_1:def_19; thus ( x1,x2 ==>. y1,y2,TS implies [[x1,x2],[y1,y2]] in R ) ::_thesis: ( [[x1,x2],[y1,y2]] in R implies x1,x2 ==>. y1,y2,TS ) proof assume A3: x1,x2 ==>. y1,y2,TS ; ::_thesis: [[x1,x2],[y1,y2]] in R then y1 in TS by Th20; then A4: y1 in the carrier of TS by STRUCT_0:def_5; x1 in TS by A3, Th20; then A5: x1 in the carrier of TS by STRUCT_0:def_5; y2 in E ^omega by A3, Th20; then A6: [y1,y2] in [: the carrier of TS,(E ^omega):] by A4, ZFMISC_1:def_2; x2 in E ^omega by A3, Th20; then [x1,x2] in [: the carrier of TS,(E ^omega):] by A5, ZFMISC_1:def_2; hence [[x1,x2],[y1,y2]] in R by A1, A3, A6; ::_thesis: verum end; assume A7: [[x1,x2],[y1,y2]] in R ; ::_thesis: x1,x2 ==>. y1,y2,TS then ( [x1,x2] in dom R & [y1,y2] in rng R ) by XTUPLE_0:def_12, XTUPLE_0:def_13; then consider x19, x29, y19, y29 being set such that A8: [x19,x29] = [x1,x2] and A9: [y19,y29] = [y1,y2] and A10: x19,x29 ==>. y19,y29,TS by A1, A7, A2; A11: y1 = y19 by A9, XTUPLE_0:1; ( x1 = x19 & x2 = x29 ) by A8, XTUPLE_0:1; hence x1,x2 ==>. y1,y2,TS by A9, A10, A11, XTUPLE_0:1; ::_thesis: verum end; hence for x1, x2, y1, y2 being set holds ( [[x1,x2],[y1,y2]] in R iff x1,x2 ==>. y1,y2,TS ) ; ::_thesis: verum end; uniqueness for b1, b2 being Relation of [: the carrier of TS,(E ^omega):] st ( for x1, x2, y1, y2 being set holds ( [[x1,x2],[y1,y2]] in b1 iff x1,x2 ==>. y1,y2,TS ) ) & ( for x1, x2, y1, y2 being set holds ( [[x1,x2],[y1,y2]] in b2 iff x1,x2 ==>. y1,y2,TS ) ) holds b1 = b2 proof let R1, R2 be Relation of [: the carrier of TS,(E ^omega):]; ::_thesis: ( ( for x1, x2, y1, y2 being set holds ( [[x1,x2],[y1,y2]] in R1 iff x1,x2 ==>. y1,y2,TS ) ) & ( for x1, x2, y1, y2 being set holds ( [[x1,x2],[y1,y2]] in R2 iff x1,x2 ==>. y1,y2,TS ) ) implies R1 = R2 ) assume that A12: for x1, x2, y1, y2 being set holds ( [[x1,x2],[y1,y2]] in R1 iff x1,x2 ==>. y1,y2,TS ) and A13: for x1, x2, y1, y2 being set holds ( [[x1,x2],[y1,y2]] in R2 iff x1,x2 ==>. y1,y2,TS ) ; ::_thesis: R1 = R2 now__::_thesis:_for_s,_t_being_Element_of_[:_the_carrier_of_TS,(E_^omega):]_holds_ (_[s,t]_in_R1_iff_[s,t]_in_R2_) let s, t be Element of [: the carrier of TS,(E ^omega):]; ::_thesis: ( [s,t] in R1 iff [s,t] in R2 ) consider x, u being set such that A14: x in the carrier of TS and A15: u in E ^omega and A16: s = [x,u] by ZFMISC_1:def_2; reconsider u = u as Element of E ^omega by A15; reconsider x = x as Element of TS by A14; consider y, v being set such that A17: y in the carrier of TS and A18: v in E ^omega and A19: t = [y,v] by ZFMISC_1:def_2; reconsider v = v as Element of E ^omega by A18; reconsider y = y as Element of TS by A17; ( [s,t] in R1 iff x,u ==>. y,v,TS ) by A12, A16, A19; hence ( [s,t] in R1 iff [s,t] in R2 ) by A13, A16, A19; ::_thesis: verum end; hence R1 = R2 by RELSET_1:def_2; ::_thesis: verum end; end; :: deftheorem Def4 defines ==>.-relation REWRITE3:def_4_:_ for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F for b4 being Relation of [: the carrier of TS,(E ^omega):] holds ( b4 = ==>.-relation TS iff for x1, x2, y1, y2 being set holds ( [[x1,x2],[y1,y2]] in b4 iff x1,x2 ==>. y1,y2,TS ) ); theorem Th31: :: REWRITE3:31 for x, y being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st [x,y] in ==>.-relation TS holds ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st ( x = [s,v] & y = [t,w] ) proof let x, y be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st [x,y] in ==>.-relation TS holds ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st ( x = [s,v] & y = [t,w] ) let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st [x,y] in ==>.-relation TS holds ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st ( x = [s,v] & y = [t,w] ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st [x,y] in ==>.-relation TS holds ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st ( x = [s,v] & y = [t,w] ) let TS be non empty transition-system over F; ::_thesis: ( [x,y] in ==>.-relation TS implies ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st ( x = [s,v] & y = [t,w] ) ) assume A1: [x,y] in ==>.-relation TS ; ::_thesis: ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st ( x = [s,v] & y = [t,w] ) then y in [: the carrier of TS,(E ^omega):] by ZFMISC_1:87; then A2: ex y1, y2 being set st ( y1 in the carrier of TS & y2 in E ^omega & y = [y1,y2] ) by ZFMISC_1:def_2; x in [: the carrier of TS,(E ^omega):] by A1, ZFMISC_1:87; then ex x1, x2 being set st ( x1 in the carrier of TS & x2 in E ^omega & x = [x1,x2] ) by ZFMISC_1:def_2; hence ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st ( x = [s,v] & y = [t,w] ) by A2; ::_thesis: verum end; theorem Th32: :: REWRITE3:32 for x1, x2, y1, y2 being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st [[x1,x2],[y1,y2]] in ==>.-relation TS holds ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) proof let x1, x2, y1, y2 be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st [[x1,x2],[y1,y2]] in ==>.-relation TS holds ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st [[x1,x2],[y1,y2]] in ==>.-relation TS holds ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st [[x1,x2],[y1,y2]] in ==>.-relation TS holds ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) let TS be non empty transition-system over F; ::_thesis: ( [[x1,x2],[y1,y2]] in ==>.-relation TS implies ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) ) assume [[x1,x2],[y1,y2]] in ==>.-relation TS ; ::_thesis: ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) then x1,x2 ==>. y1,y2,TS by Def4; hence ( x1 in TS & y1 in TS & x2 in E ^omega & y2 in E ^omega & x1 in dom (dom the Tran of TS) & y1 in rng the Tran of TS ) by Th20; ::_thesis: verum end; theorem Th33: :: REWRITE3:33 for x being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st x in ==>.-relation TS holds ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]] proof let x be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st x in ==>.-relation TS holds ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]] let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st x in ==>.-relation TS holds ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]] let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x in ==>.-relation TS holds ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]] let TS be non empty transition-system over F; ::_thesis: ( x in ==>.-relation TS implies ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]] ) assume A1: x in ==>.-relation TS ; ::_thesis: ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]] then consider y, z being set such that A2: x = [y,z] by RELAT_1:def_1; ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st ( y = [s,v] & z = [t,w] ) by A1, A2, Th31; hence ex s, t being Element of TS ex v, w being Element of E ^omega st x = [[s,v],[t,w]] by A2; ::_thesis: verum end; theorem Th34: :: REWRITE3:34 for E being non empty set for F1, F2 being Subset of (E ^omega) for TS1 being non empty transition-system over F1 for TS2 being non empty transition-system over F2 st the Tran of TS1 = the Tran of TS2 holds ==>.-relation TS1 = ==>.-relation TS2 proof let E be non empty set ; ::_thesis: for F1, F2 being Subset of (E ^omega) for TS1 being non empty transition-system over F1 for TS2 being non empty transition-system over F2 st the Tran of TS1 = the Tran of TS2 holds ==>.-relation TS1 = ==>.-relation TS2 let F1, F2 be Subset of (E ^omega); ::_thesis: for TS1 being non empty transition-system over F1 for TS2 being non empty transition-system over F2 st the Tran of TS1 = the Tran of TS2 holds ==>.-relation TS1 = ==>.-relation TS2 let TS1 be non empty transition-system over F1; ::_thesis: for TS2 being non empty transition-system over F2 st the Tran of TS1 = the Tran of TS2 holds ==>.-relation TS1 = ==>.-relation TS2 let TS2 be non empty transition-system over F2; ::_thesis: ( the Tran of TS1 = the Tran of TS2 implies ==>.-relation TS1 = ==>.-relation TS2 ) assume A1: the Tran of TS1 = the Tran of TS2 ; ::_thesis: ==>.-relation TS1 = ==>.-relation TS2 A2: now__::_thesis:_for_x_being_set_st_x_in_==>.-relation_TS1_holds_ x_in_==>.-relation_TS2 let x be set ; ::_thesis: ( x in ==>.-relation TS1 implies x in ==>.-relation TS2 ) assume A3: x in ==>.-relation TS1 ; ::_thesis: x in ==>.-relation TS2 then consider s, t being Element of TS1, v, w being Element of E ^omega such that A4: x = [[s,v],[t,w]] by Th33; s,v ==>. t,w,TS1 by A3, A4, Def4; then s,v ==>. t,w,TS2 by A1, Th21; hence x in ==>.-relation TS2 by A4, Def4; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_==>.-relation_TS2_holds_ x_in_==>.-relation_TS1 let x be set ; ::_thesis: ( x in ==>.-relation TS2 implies x in ==>.-relation TS1 ) assume A5: x in ==>.-relation TS2 ; ::_thesis: x in ==>.-relation TS1 then consider s, t being Element of TS2, v, w being Element of E ^omega such that A6: x = [[s,v],[t,w]] by Th33; s,v ==>. t,w,TS2 by A5, A6, Def4; then s,v ==>. t,w,TS1 by A1, Th21; hence x in ==>.-relation TS1 by A6, Def4; ::_thesis: verum end; hence ==>.-relation TS1 = ==>.-relation TS2 by A2, TARSKI:1; ::_thesis: verum end; theorem Th35: :: REWRITE3:35 for x1, x2, y1, y2 being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st [[x1,x2],[y1,y2]] in ==>.-relation TS holds ex v, w being Element of E ^omega st ( v = y2 & x1,w -->. y1,TS & x2 = w ^ v ) proof let x1, x2, y1, y2 be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st [[x1,x2],[y1,y2]] in ==>.-relation TS holds ex v, w being Element of E ^omega st ( v = y2 & x1,w -->. y1,TS & x2 = w ^ v ) let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st [[x1,x2],[y1,y2]] in ==>.-relation TS holds ex v, w being Element of E ^omega st ( v = y2 & x1,w -->. y1,TS & x2 = w ^ v ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st [[x1,x2],[y1,y2]] in ==>.-relation TS holds ex v, w being Element of E ^omega st ( v = y2 & x1,w -->. y1,TS & x2 = w ^ v ) let TS be non empty transition-system over F; ::_thesis: ( [[x1,x2],[y1,y2]] in ==>.-relation TS implies ex v, w being Element of E ^omega st ( v = y2 & x1,w -->. y1,TS & x2 = w ^ v ) ) assume [[x1,x2],[y1,y2]] in ==>.-relation TS ; ::_thesis: ex v, w being Element of E ^omega st ( v = y2 & x1,w -->. y1,TS & x2 = w ^ v ) then x1,x2 ==>. y1,y2,TS by Def4; hence ex v, w being Element of E ^omega st ( v = y2 & x1,w -->. y1,TS & x2 = w ^ v ) by Def3; ::_thesis: verum end; theorem Th36: :: REWRITE3:36 for x, y being set for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) proof let x, y be set ; ::_thesis: for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) let E be non empty set ; ::_thesis: for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) let u, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) let TS be non empty transition-system over F; ::_thesis: ( [[x,u],[y,v]] in ==>.-relation TS implies ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) ) assume [[x,u],[y,v]] in ==>.-relation TS ; ::_thesis: ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) then x,u ==>. y,v,TS by Def4; hence ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) by Th22; ::_thesis: verum end; theorem Th37: :: REWRITE3:37 for x, y, z being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F holds ( x,y -->. z,TS iff [[x,y],[z,(<%> E)]] in ==>.-relation TS ) proof let x, y, z be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F holds ( x,y -->. z,TS iff [[x,y],[z,(<%> E)]] in ==>.-relation TS ) let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F holds ( x,y -->. z,TS iff [[x,y],[z,(<%> E)]] in ==>.-relation TS ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F holds ( x,y -->. z,TS iff [[x,y],[z,(<%> E)]] in ==>.-relation TS ) let TS be non empty transition-system over F; ::_thesis: ( x,y -->. z,TS iff [[x,y],[z,(<%> E)]] in ==>.-relation TS ) thus ( x,y -->. z,TS implies [[x,y],[z,(<%> E)]] in ==>.-relation TS ) ::_thesis: ( [[x,y],[z,(<%> E)]] in ==>.-relation TS implies x,y -->. z,TS ) proof assume x,y -->. z,TS ; ::_thesis: [[x,y],[z,(<%> E)]] in ==>.-relation TS then x,y ==>. z, <%> E,TS by Th23; hence [[x,y],[z,(<%> E)]] in ==>.-relation TS by Def4; ::_thesis: verum end; assume [[x,y],[z,(<%> E)]] in ==>.-relation TS ; ::_thesis: x,y -->. z,TS then x,y ==>. z, <%> E,TS by Def4; hence x,y -->. z,TS by Th23; ::_thesis: verum end; theorem Th38: :: REWRITE3:38 for x, y being set for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F holds ( x,v -->. y,TS iff [[x,(v ^ w)],[y,w]] in ==>.-relation TS ) proof let x, y be set ; ::_thesis: for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F holds ( x,v -->. y,TS iff [[x,(v ^ w)],[y,w]] in ==>.-relation TS ) let E be non empty set ; ::_thesis: for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F holds ( x,v -->. y,TS iff [[x,(v ^ w)],[y,w]] in ==>.-relation TS ) let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F holds ( x,v -->. y,TS iff [[x,(v ^ w)],[y,w]] in ==>.-relation TS ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F holds ( x,v -->. y,TS iff [[x,(v ^ w)],[y,w]] in ==>.-relation TS ) let TS be non empty transition-system over F; ::_thesis: ( x,v -->. y,TS iff [[x,(v ^ w)],[y,w]] in ==>.-relation TS ) thus ( x,v -->. y,TS implies [[x,(v ^ w)],[y,w]] in ==>.-relation TS ) ::_thesis: ( [[x,(v ^ w)],[y,w]] in ==>.-relation TS implies x,v -->. y,TS ) proof assume x,v -->. y,TS ; ::_thesis: [[x,(v ^ w)],[y,w]] in ==>.-relation TS then x,v ^ w ==>. y,w,TS by Th24; hence [[x,(v ^ w)],[y,w]] in ==>.-relation TS by Def4; ::_thesis: verum end; assume [[x,(v ^ w)],[y,w]] in ==>.-relation TS ; ::_thesis: x,v -->. y,TS then x,v ^ w ==>. y,w,TS by Def4; hence x,v -->. y,TS by Th24; ::_thesis: verum end; theorem :: REWRITE3:39 for x, y being set for E being non empty set for u, v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds [[x,(u ^ w)],[y,(v ^ w)]] in ==>.-relation TS proof let x, y be set ; ::_thesis: for E being non empty set for u, v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds [[x,(u ^ w)],[y,(v ^ w)]] in ==>.-relation TS let E be non empty set ; ::_thesis: for u, v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds [[x,(u ^ w)],[y,(v ^ w)]] in ==>.-relation TS let u, v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds [[x,(u ^ w)],[y,(v ^ w)]] in ==>.-relation TS let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds [[x,(u ^ w)],[y,(v ^ w)]] in ==>.-relation TS let TS be non empty transition-system over F; ::_thesis: ( [[x,u],[y,v]] in ==>.-relation TS implies [[x,(u ^ w)],[y,(v ^ w)]] in ==>.-relation TS ) assume [[x,u],[y,v]] in ==>.-relation TS ; ::_thesis: [[x,(u ^ w)],[y,(v ^ w)]] in ==>.-relation TS then x,u ==>. y,v,TS by Def4; then x,u ^ w ==>. y,v ^ w,TS by Th25; hence [[x,(u ^ w)],[y,(v ^ w)]] in ==>.-relation TS by Def4; ::_thesis: verum end; theorem :: REWRITE3:40 for x, y being set for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds len u >= len v proof let x, y be set ; ::_thesis: for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds len u >= len v let E be non empty set ; ::_thesis: for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds len u >= len v let u, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds len u >= len v let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st [[x,u],[y,v]] in ==>.-relation TS holds len u >= len v let TS be non empty transition-system over F; ::_thesis: ( [[x,u],[y,v]] in ==>.-relation TS implies len u >= len v ) assume [[x,u],[y,v]] in ==>.-relation TS ; ::_thesis: len u >= len v then x,u ==>. y,v,TS by Def4; hence len u >= len v by Th26; ::_thesis: verum end; theorem :: REWRITE3:41 for x, y1, z, y2 being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st the Tran of TS is Function & [x,[y1,z]] in ==>.-relation TS & [x,[y2,z]] in ==>.-relation TS holds y1 = y2 proof let x, y1, z, y2 be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st the Tran of TS is Function & [x,[y1,z]] in ==>.-relation TS & [x,[y2,z]] in ==>.-relation TS holds y1 = y2 let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st the Tran of TS is Function & [x,[y1,z]] in ==>.-relation TS & [x,[y2,z]] in ==>.-relation TS holds y1 = y2 let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st the Tran of TS is Function & [x,[y1,z]] in ==>.-relation TS & [x,[y2,z]] in ==>.-relation TS holds y1 = y2 let TS be non empty transition-system over F; ::_thesis: ( the Tran of TS is Function & [x,[y1,z]] in ==>.-relation TS & [x,[y2,z]] in ==>.-relation TS implies y1 = y2 ) assume A1: the Tran of TS is Function ; ::_thesis: ( not [x,[y1,z]] in ==>.-relation TS or not [x,[y2,z]] in ==>.-relation TS or y1 = y2 ) assume that A2: [x,[y1,z]] in ==>.-relation TS and A3: [x,[y2,z]] in ==>.-relation TS ; ::_thesis: y1 = y2 consider s being Element of TS, v being Element of E ^omega , t being Element of TS, w being Element of E ^omega such that A4: x = [s,v] and [y1,z] = [t,w] by A2, Th31; ( s,v ==>. y1,z,TS & s,v ==>. y2,z,TS ) by A2, A3, A4, Def4; hence y1 = y2 by A1, Th27; ::_thesis: verum end; theorem :: REWRITE3:42 for x, y being set for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & [[x,u],[y,v]] in ==>.-relation TS holds len u > len v proof let x, y be set ; ::_thesis: for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & [[x,u],[y,v]] in ==>.-relation TS holds len u > len v let E be non empty set ; ::_thesis: for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & [[x,u],[y,v]] in ==>.-relation TS holds len u > len v let u, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & [[x,u],[y,v]] in ==>.-relation TS holds len u > len v let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & [[x,u],[y,v]] in ==>.-relation TS holds len u > len v let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) & [[x,u],[y,v]] in ==>.-relation TS implies len u > len v ) assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: ( not [[x,u],[y,v]] in ==>.-relation TS or len u > len v ) assume [[x,u],[y,v]] in ==>.-relation TS ; ::_thesis: len u > len v then x,u ==>. y,v,TS by Def4; hence len u > len v by A1, Th29; ::_thesis: verum end; theorem Th43: :: REWRITE3:43 for x, z, y being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds not [[x,z],[y,z]] in ==>.-relation TS proof let x, z, y be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds not [[x,z],[y,z]] in ==>.-relation TS let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds not [[x,z],[y,z]] in ==>.-relation TS let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds not [[x,z],[y,z]] in ==>.-relation TS let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies not [[x,z],[y,z]] in ==>.-relation TS ) assume not <%> E in rng (dom the Tran of TS) ; ::_thesis: not [[x,z],[y,z]] in ==>.-relation TS then not x,z ==>. y,z,TS by Th28; hence not [[x,z],[y,z]] in ==>.-relation TS by Def4; ::_thesis: verum end; theorem Th44: :: REWRITE3:44 for x, y1, y2 being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic & [x,y1] in ==>.-relation TS & [x,y2] in ==>.-relation TS holds y1 = y2 proof let x, y1, y2 be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic & [x,y1] in ==>.-relation TS & [x,y2] in ==>.-relation TS holds y1 = y2 let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic & [x,y1] in ==>.-relation TS & [x,y2] in ==>.-relation TS holds y1 = y2 let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st TS is deterministic & [x,y1] in ==>.-relation TS & [x,y2] in ==>.-relation TS holds y1 = y2 let TS be non empty transition-system over F; ::_thesis: ( TS is deterministic & [x,y1] in ==>.-relation TS & [x,y2] in ==>.-relation TS implies y1 = y2 ) assume A1: TS is deterministic ; ::_thesis: ( not [x,y1] in ==>.-relation TS or not [x,y2] in ==>.-relation TS or y1 = y2 ) assume that A2: [x,y1] in ==>.-relation TS and A3: [x,y2] in ==>.-relation TS ; ::_thesis: y1 = y2 consider s2 being Element of TS, v2 being Element of E ^omega , t2 being Element of TS, w2 being Element of E ^omega such that x = [s2,v2] and A4: y2 = [t2,w2] by A3, Th31; consider s1 being Element of TS, v1 being Element of E ^omega , t1 being Element of TS, w1 being Element of E ^omega such that A5: x = [s1,v1] and A6: y1 = [t1,w1] by A2, Th31; A7: s1,v1 ==>. t1,w1,TS by A2, A5, A6, Def4; A8: s1,v1 ==>. t2,w2,TS by A3, A5, A4, Def4; then t1 = t2 by A1, A7, Th30; hence y1 = y2 by A1, A6, A4, A7, A8, Th30; ::_thesis: verum end; theorem :: REWRITE3:45 for x, y1, z1, y2, z2 being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic & [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS holds ( y1 = y2 & z1 = z2 ) proof let x, y1, z1, y2, z2 be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic & [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS holds ( y1 = y2 & z1 = z2 ) let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic & [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS holds ( y1 = y2 & z1 = z2 ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st TS is deterministic & [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS holds ( y1 = y2 & z1 = z2 ) let TS be non empty transition-system over F; ::_thesis: ( TS is deterministic & [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS implies ( y1 = y2 & z1 = z2 ) ) assume A1: TS is deterministic ; ::_thesis: ( not [x,[y1,z1]] in ==>.-relation TS or not [x,[y2,z2]] in ==>.-relation TS or ( y1 = y2 & z1 = z2 ) ) assume ( [x,[y1,z1]] in ==>.-relation TS & [x,[y2,z2]] in ==>.-relation TS ) ; ::_thesis: ( y1 = y2 & z1 = z2 ) then [y1,z1] = [y2,z2] by A1, Th44; hence ( y1 = y2 & z1 = z2 ) by XTUPLE_0:1; ::_thesis: verum end; theorem :: REWRITE3:46 for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic holds ==>.-relation TS is Function-like proof let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic holds ==>.-relation TS is Function-like let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st TS is deterministic holds ==>.-relation TS is Function-like let TS be non empty transition-system over F; ::_thesis: ( TS is deterministic implies ==>.-relation TS is Function-like ) assume TS is deterministic ; ::_thesis: ==>.-relation TS is Function-like then for x, y, z being set st [x,y] in ==>.-relation TS & [x,z] in ==>.-relation TS holds y = z by Th44; hence ==>.-relation TS is Function-like by FUNCT_1:def_1; ::_thesis: verum end; begin definition let x be set ; let E be non empty set ; func dim2 (x,E) -> Element of E ^omega equals :Def5: :: REWRITE3:def 5 x `2 if ex y being set ex u being Element of E ^omega st x = [y,u] otherwise {} ; coherence ( ( ex y being set ex u being Element of E ^omega st x = [y,u] implies x `2 is Element of E ^omega ) & ( ( for y being set for u being Element of E ^omega holds not x = [y,u] ) implies {} is Element of E ^omega ) ) proof thus ( ex y being set ex u being Element of E ^omega st x = [y,u] implies x `2 is Element of E ^omega ) by MCART_1:7; ::_thesis: ( ( for y being set for u being Element of E ^omega holds not x = [y,u] ) implies {} is Element of E ^omega ) {} = <%> E ; hence ( ( for y being set for u being Element of E ^omega holds not x = [y,u] ) implies {} is Element of E ^omega ) ; ::_thesis: verum end; consistency for b1 being Element of E ^omega holds verum ; end; :: deftheorem Def5 defines dim2 REWRITE3:def_5_:_ for x being set for E being non empty set holds ( ( ex y being set ex u being Element of E ^omega st x = [y,u] implies dim2 (x,E) = x `2 ) & ( ( for y being set for u being Element of E ^omega holds not x = [y,u] ) implies dim2 (x,E) = {} ) ); theorem Th47: :: REWRITE3:47 for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st ( P . k = [s,v] & P . (k + 1) = [t,w] ) proof let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st ( P . k = [s,v] & P . (k + 1) = [t,w] ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st ( P . k = [s,v] & P . (k + 1) = [t,w] ) let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st ( P . k = [s,v] & P . (k + 1) = [t,w] ) let P be RedSequence of ==>.-relation TS; ::_thesis: for k being Nat st k in dom P & k + 1 in dom P holds ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st ( P . k = [s,v] & P . (k + 1) = [t,w] ) let k be Nat; ::_thesis: ( k in dom P & k + 1 in dom P implies ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st ( P . k = [s,v] & P . (k + 1) = [t,w] ) ) assume ( k in dom P & k + 1 in dom P ) ; ::_thesis: ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st ( P . k = [s,v] & P . (k + 1) = [t,w] ) then [(P . k),(P . (k + 1))] in ==>.-relation TS by REWRITE1:def_2; hence ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st ( P . k = [s,v] & P . (k + 1) = [t,w] ) by Th31; ::_thesis: verum end; theorem Th48: :: REWRITE3:48 for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds ( P . k = [((P . k) `1),((P . k) `2)] & P . (k + 1) = [((P . (k + 1)) `1),((P . (k + 1)) `2)] ) proof let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds ( P . k = [((P . k) `1),((P . k) `2)] & P . (k + 1) = [((P . (k + 1)) `1),((P . (k + 1)) `2)] ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds ( P . k = [((P . k) `1),((P . k) `2)] & P . (k + 1) = [((P . (k + 1)) `1),((P . (k + 1)) `2)] ) let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds ( P . k = [((P . k) `1),((P . k) `2)] & P . (k + 1) = [((P . (k + 1)) `1),((P . (k + 1)) `2)] ) let P be RedSequence of ==>.-relation TS; ::_thesis: for k being Nat st k in dom P & k + 1 in dom P holds ( P . k = [((P . k) `1),((P . k) `2)] & P . (k + 1) = [((P . (k + 1)) `1),((P . (k + 1)) `2)] ) let k be Nat; ::_thesis: ( k in dom P & k + 1 in dom P implies ( P . k = [((P . k) `1),((P . k) `2)] & P . (k + 1) = [((P . (k + 1)) `1),((P . (k + 1)) `2)] ) ) assume ( k in dom P & k + 1 in dom P ) ; ::_thesis: ( P . k = [((P . k) `1),((P . k) `2)] & P . (k + 1) = [((P . (k + 1)) `1),((P . (k + 1)) `2)] ) then ex s being Element of TS ex v being Element of E ^omega ex t being Element of TS ex w being Element of E ^omega st ( P . k = [s,v] & P . (k + 1) = [t,w] ) by Th47; hence ( P . k = [((P . k) `1),((P . k) `2)] & P . (k + 1) = [((P . (k + 1)) `1),((P . (k + 1)) `2)] ) by MCART_1:8; ::_thesis: verum end; theorem Th49: :: REWRITE3:49 for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds ( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS ) proof let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds ( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds ( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS ) let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds ( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS ) let P be RedSequence of ==>.-relation TS; ::_thesis: for k being Nat st k in dom P & k + 1 in dom P holds ( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS ) let k be Nat; ::_thesis: ( k in dom P & k + 1 in dom P implies ( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS ) ) assume ( k in dom P & k + 1 in dom P ) ; ::_thesis: ( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS ) then A1: [(P . k),(P . (k + 1))] in ==>.-relation TS by REWRITE1:def_2; then consider s being Element of TS, v being Element of E ^omega , t being Element of TS, w being Element of E ^omega such that A2: ( P . k = [s,v] & P . (k + 1) = [t,w] ) by Th31; A3: ( s in dom (dom the Tran of TS) & t in rng the Tran of TS ) by A1, A2, Th32; A4: ( v in E ^omega & w in E ^omega ) ; ( s in TS & t in TS ) by A1, A2, Th32; hence ( (P . k) `1 in TS & (P . k) `2 in E ^omega & (P . (k + 1)) `1 in TS & (P . (k + 1)) `2 in E ^omega & (P . k) `1 in dom (dom the Tran of TS) & (P . (k + 1)) `1 in rng the Tran of TS ) by A2, A4, A3, MCART_1:7; ::_thesis: verum end; theorem :: REWRITE3:50 for E being non empty set for F1, F2 being Subset of (E ^omega) for TS1 being non empty transition-system over F1 for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds for P being RedSequence of ==>.-relation TS1 holds P is RedSequence of ==>.-relation TS2 proof let E be non empty set ; ::_thesis: for F1, F2 being Subset of (E ^omega) for TS1 being non empty transition-system over F1 for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds for P being RedSequence of ==>.-relation TS1 holds P is RedSequence of ==>.-relation TS2 let F1, F2 be Subset of (E ^omega); ::_thesis: for TS1 being non empty transition-system over F1 for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds for P being RedSequence of ==>.-relation TS1 holds P is RedSequence of ==>.-relation TS2 let TS1 be non empty transition-system over F1; ::_thesis: for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds for P being RedSequence of ==>.-relation TS1 holds P is RedSequence of ==>.-relation TS2 let TS2 be non empty transition-system over F2; ::_thesis: ( the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 implies for P being RedSequence of ==>.-relation TS1 holds P is RedSequence of ==>.-relation TS2 ) assume A1: ( the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 ) ; ::_thesis: for P being RedSequence of ==>.-relation TS1 holds P is RedSequence of ==>.-relation TS2 let P be RedSequence of ==>.-relation TS1; ::_thesis: P is RedSequence of ==>.-relation TS2 A2: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_P_&_i_+_1_in_dom_P_holds_ [(P_._i),(P_._(i_+_1))]_in_==>.-relation_TS2 let i be Element of NAT ; ::_thesis: ( i in dom P & i + 1 in dom P implies [(P . i),(P . (i + 1))] in ==>.-relation TS2 ) assume ( i in dom P & i + 1 in dom P ) ; ::_thesis: [(P . i),(P . (i + 1))] in ==>.-relation TS2 then [(P . i),(P . (i + 1))] in ==>.-relation TS1 by REWRITE1:def_2; hence [(P . i),(P . (i + 1))] in ==>.-relation TS2 by A1, Th34; ::_thesis: verum end; len P > 0 ; hence P is RedSequence of ==>.-relation TS2 by A2, REWRITE1:def_2; ::_thesis: verum end; theorem Th51: :: REWRITE3:51 for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st ex x being set ex u being Element of E ^omega st P . 1 = [x,u] holds for k being Nat st k in dom P holds dim2 ((P . k),E) = (P . k) `2 proof let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st ex x being set ex u being Element of E ^omega st P . 1 = [x,u] holds for k being Nat st k in dom P holds dim2 ((P . k),E) = (P . k) `2 let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st ex x being set ex u being Element of E ^omega st P . 1 = [x,u] holds for k being Nat st k in dom P holds dim2 ((P . k),E) = (P . k) `2 let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS st ex x being set ex u being Element of E ^omega st P . 1 = [x,u] holds for k being Nat st k in dom P holds dim2 ((P . k),E) = (P . k) `2 let P be RedSequence of ==>.-relation TS; ::_thesis: ( ex x being set ex u being Element of E ^omega st P . 1 = [x,u] implies for k being Nat st k in dom P holds dim2 ((P . k),E) = (P . k) `2 ) given x being set , u being Element of E ^omega such that A1: P . 1 = [x,u] ; ::_thesis: for k being Nat st k in dom P holds dim2 ((P . k),E) = (P . k) `2 let k be Nat; ::_thesis: ( k in dom P implies dim2 ((P . k),E) = (P . k) `2 ) assume A2: k in dom P ; ::_thesis: dim2 ((P . k),E) = (P . k) `2 percases ( k > 1 or k <= 1 ) ; supposeA3: k > 1 ; ::_thesis: dim2 ((P . k),E) = (P . k) `2 A4: k <= len P by A2, FINSEQ_3:25; consider l being Nat such that A5: k = l + 1 by A3, NAT_1:6; l <= k by A5, NAT_1:11; then A6: l <= len P by A4, XXREAL_0:2; l >= 1 by A3, A5, NAT_1:19; then l in dom P by A6, FINSEQ_3:25; then [(P . l),(P . k)] in ==>.-relation TS by A2, A5, REWRITE1:def_2; then A7: P . k in rng (==>.-relation TS) by XTUPLE_0:def_13; rng (==>.-relation TS) c= [: the carrier of TS,(E ^omega):] by RELAT_1:def_19; then ex x1, y1 being set st ( x1 in the carrier of TS & y1 in E ^omega & P . k = [x1,y1] ) by A7, ZFMISC_1:def_2; hence dim2 ((P . k),E) = (P . k) `2 by Def5; ::_thesis: verum end; supposeA8: k <= 1 ; ::_thesis: dim2 ((P . k),E) = (P . k) `2 k >= 1 by A2, FINSEQ_3:25; then k = 1 by A8, XXREAL_0:1; hence dim2 ((P . k),E) = (P . k) `2 by A1, Def5; ::_thesis: verum end; end; end; theorem Th52: :: REWRITE3:52 for y being set for E being non empty set for w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . (len P) = [y,w] holds for k being Nat st k in dom P holds ex u being Element of E ^omega st (P . k) `2 = u ^ w proof let y be set ; ::_thesis: for E being non empty set for w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . (len P) = [y,w] holds for k being Nat st k in dom P holds ex u being Element of E ^omega st (P . k) `2 = u ^ w let E be non empty set ; ::_thesis: for w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . (len P) = [y,w] holds for k being Nat st k in dom P holds ex u being Element of E ^omega st (P . k) `2 = u ^ w let w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . (len P) = [y,w] holds for k being Nat st k in dom P holds ex u being Element of E ^omega st (P . k) `2 = u ^ w let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . (len P) = [y,w] holds for k being Nat st k in dom P holds ex u being Element of E ^omega st (P . k) `2 = u ^ w let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS st P . (len P) = [y,w] holds for k being Nat st k in dom P holds ex u being Element of E ^omega st (P . k) `2 = u ^ w let P be RedSequence of ==>.-relation TS; ::_thesis: ( P . (len P) = [y,w] implies for k being Nat st k in dom P holds ex u being Element of E ^omega st (P . k) `2 = u ^ w ) assume P . (len P) = [y,w] ; ::_thesis: for k being Nat st k in dom P holds ex u being Element of E ^omega st (P . k) `2 = u ^ w then A1: (P . (len P)) `2 = {} ^ w by MCART_1:7 .= (<%> E) ^ w ; defpred S1[ Nat] means ( (len P) - \$1 in dom P implies ex u being Element of E ^omega st (P . ((len P) - \$1)) `2 = u ^ w ); A2: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_ S1[k_+_1] let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A3: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_(_(len_P)_-_(k_+_1)_in_dom_P_implies_ex_u_being_Element_of_E_^omega_st_(P_._((len_P)_-_(k_+_1)))_`2_=_u_^_w_) set len2 = (len P) - k; set len1 = (len P) - (k + 1); A4: ((len P) - (k + 1)) + 1 = (len P) - k ; assume A5: (len P) - (k + 1) in dom P ; ::_thesis: ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ w thus ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ w ::_thesis: verum proof percases ( (len P) - k in dom P or not (len P) - k in dom P ) ; supposeA6: (len P) - k in dom P ; ::_thesis: ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ w then consider u1 being Element of E ^omega such that A7: (P . ((len P) - k)) `2 = u1 ^ w by A3; A8: [(P . ((len P) - (k + 1))),(P . ((len P) - k))] in ==>.-relation TS by A5, A4, A6, REWRITE1:def_2; then consider x being Element of TS, v1 being Element of E ^omega , y being Element of TS, v2 being Element of E ^omega such that A9: P . ((len P) - (k + 1)) = [x,v1] and A10: P . ((len P) - k) = [y,v2] by Th31; x,v1 ==>. y,v2,TS by A8, A9, A10, Def4; then consider u2 being Element of E ^omega such that x,u2 -->. y,TS and A11: v1 = u2 ^ v2 by Th22; take u2 ^ u1 ; ::_thesis: (P . ((len P) - (k + 1))) `2 = (u2 ^ u1) ^ w (P . ((len P) - (k + 1))) `2 = u2 ^ v2 by A9, A11, MCART_1:7 .= u2 ^ (u1 ^ w) by A7, A10, MCART_1:7 .= (u2 ^ u1) ^ w by AFINSQ_1:27 ; hence (P . ((len P) - (k + 1))) `2 = (u2 ^ u1) ^ w ; ::_thesis: verum end; suppose not (len P) - k in dom P ; ::_thesis: ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ w then (len P) - (k + 1) = (len P) - 0 by A5, A4, Th3; hence ex u being Element of E ^omega st (P . ((len P) - (k + 1))) `2 = u ^ w ; ::_thesis: verum end; end; end; end; hence S1[k + 1] ; ::_thesis: verum end; A12: S1[ 0 ] by A1; A13: for k being Nat holds S1[k] from NAT_1:sch_2(A12, A2); hereby ::_thesis: verum let k be Nat; ::_thesis: ( k in dom P implies ex u being Element of E ^omega st (P . k) `2 = u ^ w ) assume A14: k in dom P ; ::_thesis: ex u being Element of E ^omega st (P . k) `2 = u ^ w k <= len P by A14, FINSEQ_3:25; then consider l being Nat such that A15: k + l = len P by NAT_1:10; (k + l) - l = (len P) - l by A15; hence ex u being Element of E ^omega st (P . k) `2 = u ^ w by A13, A14; ::_thesis: verum end; end; theorem Th53: :: REWRITE3:53 for x, y being set for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds ex u being Element of E ^omega st v = u ^ w proof let x, y be set ; ::_thesis: for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds ex u being Element of E ^omega st v = u ^ w let E be non empty set ; ::_thesis: for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds ex u being Element of E ^omega st v = u ^ w let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds ex u being Element of E ^omega st v = u ^ w let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds ex u being Element of E ^omega st v = u ^ w let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds ex u being Element of E ^omega st v = u ^ w let P be RedSequence of ==>.-relation TS; ::_thesis: ( P . 1 = [x,v] & P . (len P) = [y,w] implies ex u being Element of E ^omega st v = u ^ w ) assume that A1: P . 1 = [x,v] and A2: P . (len P) = [y,w] ; ::_thesis: ex u being Element of E ^omega st v = u ^ w 0 + 1 <= len P by NAT_1:8; then 1 in dom P by FINSEQ_3:25; then consider u being Element of E ^omega such that A3: (P . 1) `2 = u ^ w by A2, Th52; take u ; ::_thesis: v = u ^ w thus v = u ^ w by A1, A3, MCART_1:7; ::_thesis: verum end; theorem Th54: :: REWRITE3:54 for x, y being set for E being non empty set for u being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds for k being Nat st k in dom P holds (P . k) `2 = u proof let x, y be set ; ::_thesis: for E being non empty set for u being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds for k being Nat st k in dom P holds (P . k) `2 = u let E be non empty set ; ::_thesis: for u being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds for k being Nat st k in dom P holds (P . k) `2 = u let u be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds for k being Nat st k in dom P holds (P . k) `2 = u let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds for k being Nat st k in dom P holds (P . k) `2 = u let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds for k being Nat st k in dom P holds (P . k) `2 = u defpred S1[ Nat] means for P being RedSequence of ==>.-relation TS for x, y being set st P . 1 = [x,u] & P . (len P) = [y,u] & len P = \$1 holds for k being Nat st k in dom P holds (P . k) `2 = u; A1: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_ S1[k_+_1] let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_for_P_being_RedSequence_of_==>.-relation_TS for_x,_y_being_set_st_P_._1_=_[x,u]_&_P_._(len_P)_=_[y,u]_&_len_P_=_k_+_1_holds_ for_l_being_Nat_st_l_in_dom_P_holds_ (P_._l)_`2_=_u let P be RedSequence of ==>.-relation TS; ::_thesis: for x, y being set st P . 1 = [x,u] & P . (len P) = [y,u] & len P = k + 1 holds for l being Nat st b6 in dom l holds (l . b6) `2 = u let x, y be set ; ::_thesis: ( P . 1 = [x,u] & P . (len P) = [y,u] & len P = k + 1 implies for l being Nat st b4 in dom l holds (l . b4) `2 = u ) assume that A3: P . 1 = [x,u] and A4: P . (len P) = [y,u] and A5: len P = k + 1 ; ::_thesis: for l being Nat st b4 in dom l holds (l . b4) `2 = u percases ( k = 0 or k <> 0 ) ; supposeA6: k = 0 ; ::_thesis: for l being Nat st b4 in dom l holds (l . b4) `2 = u hereby ::_thesis: verum let l be Nat; ::_thesis: ( l in dom P implies (P . l) `2 = u ) assume l in dom P ; ::_thesis: (P . l) `2 = u then ( l <= 1 & 1 <= l ) by A5, A6, FINSEQ_3:25; then l = 1 by XXREAL_0:1; hence (P . l) `2 = u by A3, MCART_1:7; ::_thesis: verum end; end; suppose k <> 0 ; ::_thesis: for l being Nat st b4 in dom l holds (l . b4) `2 = u then A7: k + 1 > 0 + 1 by XREAL_1:6; then A8: 1 in dom P by A5, FINSEQ_3:25; len P >= 1 + 1 by A5, A7, NAT_1:8; then A9: 1 + 1 in dom P by FINSEQ_3:25; then A10: P . (1 + 1) = [((P . (1 + 1)) `1),((P . (1 + 1)) `2)] by A8, Th48; reconsider u1 = (P . (1 + 1)) `2 as Element of E ^omega by A8, A9, Th49; ==>.-relation TS reduces P . 1,P . (1 + 1) by A8, A9, REWRITE1:17; then ex P9 being RedSequence of ==>.-relation TS st ( P9 . 1 = P . 1 & P9 . (len P9) = P . (1 + 1) ) by REWRITE1:def_3; then consider w being Element of E ^omega such that A11: u = w ^ u1 by A3, A10, Th53; A12: len <*(P . 1)*> = 1 by FINSEQ_1:40; consider Q being RedSequence of ==>.-relation TS such that A13: <*(P . 1)*> ^ Q = P and A14: len P = (len Q) + 1 by A5, A7, Th5; A15: len Q >= 0 + 1 by NAT_1:8; then A16: Q . 1 = [((P . (1 + 1)) `1),((P . (1 + 1)) `2)] by A13, A12, A10, FINSEQ_1:65; A17: Q . (len Q) = [y,u] by A4, A13, A14, A12, A15, FINSEQ_1:65; then consider v being Element of E ^omega such that A18: u1 = v ^ u by A16, Th53; B: {} ^ u1 = u1 ; u = (w ^ v) ^ u by A18, A11, AFINSQ_1:27; then w ^ v = {} by FLANG_2:4; then A19: Q . 1 = [((P . (1 + 1)) `1),u] by A16, A11, B, AFINSQ_1:30; hereby ::_thesis: verum let l be Nat; ::_thesis: ( l in dom P implies (P . b1) `2 = u ) assume A20: l in dom P ; ::_thesis: (P . b1) `2 = u then A21: 1 <= l by FINSEQ_3:25; then reconsider l9 = l - 1 as Element of NAT by NAT_1:21; 1 + 1 <= l + 1 by A21, XREAL_1:6; then A22: ( 1 + 1 = l + 1 or 1 + 1 <= l ) by NAT_1:8; l <= len P by A20, FINSEQ_3:25; then ( 1 = l or ( (1 + 1) - 1 <= l - 1 & l - 1 <= ((len Q) + 1) - 1 ) ) by A14, A22, XREAL_1:9; then A23: ( l = 1 or l9 in dom Q ) by FINSEQ_3:25; percases ( l = 1 or l - 1 in dom Q ) by A23; suppose l = 1 ; ::_thesis: (P . b1) `2 = u hence (P . l) `2 = u by A3, MCART_1:7; ::_thesis: verum end; supposeA24: l - 1 in dom Q ; ::_thesis: (P . b1) `2 = u then l - 1 <= len Q by FINSEQ_3:25; then A25: (l - 1) + 1 <= (len Q) + 1 by XREAL_1:6; 1 <= l - 1 by A24, FINSEQ_3:25; then A26: 1 + 0 < (l - 1) + 1 by XREAL_1:6; (Q . (l - 1)) `2 = u by A2, A5, A14, A17, A19, A24; hence (P . l) `2 = u by A13, A14, A12, A26, A25, FINSEQ_1:24; ::_thesis: verum end; end; end; end; end; end; hence S1[k + 1] ; ::_thesis: verum end; A27: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A27, A1); hence for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds for k being Nat st k in dom P holds (P . k) `2 = u ; ::_thesis: verum end; theorem :: REWRITE3:55 for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds ex v, w being Element of E ^omega st ( v = (P . (k + 1)) `2 & (P . k) `1 ,w -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w ^ v ) proof let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds ex v, w being Element of E ^omega st ( v = (P . (k + 1)) `2 & (P . k) `1 ,w -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w ^ v ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds ex v, w being Element of E ^omega st ( v = (P . (k + 1)) `2 & (P . k) `1 ,w -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w ^ v ) let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds ex v, w being Element of E ^omega st ( v = (P . (k + 1)) `2 & (P . k) `1 ,w -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w ^ v ) let P be RedSequence of ==>.-relation TS; ::_thesis: for k being Nat st k in dom P & k + 1 in dom P holds ex v, w being Element of E ^omega st ( v = (P . (k + 1)) `2 & (P . k) `1 ,w -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w ^ v ) let k be Nat; ::_thesis: ( k in dom P & k + 1 in dom P implies ex v, w being Element of E ^omega st ( v = (P . (k + 1)) `2 & (P . k) `1 ,w -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w ^ v ) ) assume A1: ( k in dom P & k + 1 in dom P ) ; ::_thesis: ex v, w being Element of E ^omega st ( v = (P . (k + 1)) `2 & (P . k) `1 ,w -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w ^ v ) consider s being Element of TS, u being Element of E ^omega , t being Element of TS, v being Element of E ^omega such that A2: P . k = [s,u] and A3: P . (k + 1) = [t,v] by A1, Th47; [[s,u],[t,v]] in ==>.-relation TS by A1, A2, A3, REWRITE1:def_2; then consider v1, w1 being Element of E ^omega such that A4: v1 = v and A5: s,w1 -->. t,TS and A6: u = w1 ^ v1 by Th35; take v1 ; ::_thesis: ex w being Element of E ^omega st ( v1 = (P . (k + 1)) `2 & (P . k) `1 ,w -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w ^ v1 ) take w1 ; ::_thesis: ( v1 = (P . (k + 1)) `2 & (P . k) `1 ,w1 -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w1 ^ v1 ) thus v1 = (P . (k + 1)) `2 by A3, A4, MCART_1:7; ::_thesis: ( (P . k) `1 ,w1 -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w1 ^ v1 ) (P . k) `1 ,w1 -->. t,TS by A2, A5, MCART_1:7; hence ( (P . k) `1 ,w1 -->. (P . (k + 1)) `1 ,TS & (P . k) `2 = w1 ^ v1 ) by A2, A3, A6, MCART_1:7; ::_thesis: verum end; theorem :: REWRITE3:56 for x, y being set for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P & P . k = [x,u] & P . (k + 1) = [y,v] holds ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) proof let x, y be set ; ::_thesis: for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P & P . k = [x,u] & P . (k + 1) = [y,v] holds ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) let E be non empty set ; ::_thesis: for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P & P . k = [x,u] & P . (k + 1) = [y,v] holds ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) let u, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P & P . k = [x,u] & P . (k + 1) = [y,v] holds ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P & P . k = [x,u] & P . (k + 1) = [y,v] holds ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P & P . k = [x,u] & P . (k + 1) = [y,v] holds ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) let P be RedSequence of ==>.-relation TS; ::_thesis: for k being Nat st k in dom P & k + 1 in dom P & P . k = [x,u] & P . (k + 1) = [y,v] holds ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) let k be Nat; ::_thesis: ( k in dom P & k + 1 in dom P & P . k = [x,u] & P . (k + 1) = [y,v] implies ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) ) assume ( k in dom P & k + 1 in dom P & P . k = [x,u] & P . (k + 1) = [y,v] ) ; ::_thesis: ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) then [[x,u],[y,v]] in ==>.-relation TS by REWRITE1:def_2; hence ex w being Element of E ^omega st ( x,w -->. y,TS & u = w ^ v ) by Th36; ::_thesis: verum end; theorem Th57: :: REWRITE3:57 for x, y, z being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F holds ( x,y -->. z,TS iff <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS ) proof let x, y, z be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F holds ( x,y -->. z,TS iff <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS ) let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F holds ( x,y -->. z,TS iff <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F holds ( x,y -->. z,TS iff <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS ) let TS be non empty transition-system over F; ::_thesis: ( x,y -->. z,TS iff <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS ) thus ( x,y -->. z,TS implies <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS ) ::_thesis: ( <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS implies x,y -->. z,TS ) proof assume x,y -->. z,TS ; ::_thesis: <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS then [[x,y],[z,(<%> E)]] in ==>.-relation TS by Th37; hence <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS by REWRITE1:7; ::_thesis: verum end; assume <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS ; ::_thesis: x,y -->. z,TS then [[x,y],[z,(<%> E)]] in ==>.-relation TS by Th8; hence x,y -->. z,TS by Th37; ::_thesis: verum end; theorem Th58: :: REWRITE3:58 for x, y being set for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F holds ( x,v -->. y,TS iff <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS ) proof let x, y be set ; ::_thesis: for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F holds ( x,v -->. y,TS iff <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS ) let E be non empty set ; ::_thesis: for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F holds ( x,v -->. y,TS iff <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS ) let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F holds ( x,v -->. y,TS iff <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F holds ( x,v -->. y,TS iff <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS ) let TS be non empty transition-system over F; ::_thesis: ( x,v -->. y,TS iff <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS ) thus ( x,v -->. y,TS implies <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS ) ::_thesis: ( <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS implies x,v -->. y,TS ) proof assume x,v -->. y,TS ; ::_thesis: <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS then [[x,(v ^ w)],[y,w]] in ==>.-relation TS by Th38; hence <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS by REWRITE1:7; ::_thesis: verum end; assume <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS ; ::_thesis: x,v -->. y,TS then [[x,(v ^ w)],[y,w]] in ==>.-relation TS by Th8; hence x,v -->. y,TS by Th38; ::_thesis: verum end; theorem Th59: :: REWRITE3:59 for x, y being set for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds len v >= len w proof let x, y be set ; ::_thesis: for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds len v >= len w let E be non empty set ; ::_thesis: for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds len v >= len w let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds len v >= len w let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds len v >= len w let TS be non empty transition-system over F; ::_thesis: for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] holds len v >= len w let P be RedSequence of ==>.-relation TS; ::_thesis: ( P . 1 = [x,v] & P . (len P) = [y,w] implies len v >= len w ) assume ( P . 1 = [x,v] & P . (len P) = [y,w] ) ; ::_thesis: len v >= len w then ex u being Element of E ^omega st v = u ^ w by Th53; hence len v >= len w by Th9; ::_thesis: verum end; theorem Th60: :: REWRITE3:60 for x, y being set for E being non empty set for u being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds ( len P = 1 & x = y ) proof let x, y be set ; ::_thesis: for E being non empty set for u being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds ( len P = 1 & x = y ) let E be non empty set ; ::_thesis: for u being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds ( len P = 1 & x = y ) let u be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds ( len P = 1 & x = y ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds ( len P = 1 & x = y ) let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds ( len P = 1 & x = y ) ) defpred S1[ Nat] means for P being RedSequence of ==>.-relation TS for x, y being set st P . 1 = [x,u] & P . (len P) = [y,u] & len P = \$1 holds not \$1 <> 1; assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,u] holds ( len P = 1 & x = y ) A2: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_ S1[k_+_1] let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_for_P_being_RedSequence_of_==>.-relation_TS for_x,_y_being_set_st_P_._1_=_[x,u]_&_P_._(len_P)_=_[y,u]_&_len_P_=_k_+_1_holds_ not_k_+_1_<>_1 let P be RedSequence of ==>.-relation TS; ::_thesis: for x, y being set st P . 1 = [x,u] & P . (len P) = [y,u] & len P = k + 1 holds not k + 1 <> 1 let x, y be set ; ::_thesis: ( P . 1 = [x,u] & P . (len P) = [y,u] & len P = k + 1 implies not k + 1 <> 1 ) assume that A3: P . 1 = [x,u] and A4: P . (len P) = [y,u] and A5: ( len P = k + 1 & k + 1 <> 1 ) ; ::_thesis: contradiction consider Q being RedSequence of ==>.-relation TS such that <*(P . 1)*> ^ Q = P and A6: len P = (len Q) + 1 by A5, Th5, NAT_1:25; len Q >= 0 + 1 by NAT_1:8; then (len Q) + 1 >= 1 + 1 by XREAL_1:6; then A7: 1 + 1 in dom P by A6, FINSEQ_3:25; len P > 1 by A5, NAT_1:25; then A8: 1 in dom P by FINSEQ_3:25; then P . (1 + 1) = [((P . (1 + 1)) `1),((P . (1 + 1)) `2)] by A7, Th48 .= [((P . (1 + 1)) `1),u] by A3, A4, A7, Th54 ; then [[x,u],[((P . (1 + 1)) `1),u]] in ==>.-relation TS by A3, A8, A7, REWRITE1:def_2; then x,u ==>. (P . (1 + 1)) `1 ,u,TS by Def4; hence contradiction by A1, Th28; ::_thesis: verum end; hence S1[k + 1] ; ::_thesis: verum end; let P be RedSequence of ==>.-relation TS; ::_thesis: ( P . 1 = [x,u] & P . (len P) = [y,u] implies ( len P = 1 & x = y ) ) assume A9: ( P . 1 = [x,u] & P . (len P) = [y,u] ) ; ::_thesis: ( len P = 1 & x = y ) A10: S1[ 0 ] ; for k being Nat holds S1[k] from NAT_1:sch_2(A10, A2); hence len P = 1 by A9; ::_thesis: x = y hence x = y by A9, XTUPLE_0:1; ::_thesis: verum end; theorem Th61: :: REWRITE3:61 for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st (P . 1) `2 = (P . (len P)) `2 holds len P = 1 proof let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st (P . 1) `2 = (P . (len P)) `2 holds len P = 1 let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st (P . 1) `2 = (P . (len P)) `2 holds len P = 1 let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies for P being RedSequence of ==>.-relation TS st (P . 1) `2 = (P . (len P)) `2 holds len P = 1 ) assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: for P being RedSequence of ==>.-relation TS st (P . 1) `2 = (P . (len P)) `2 holds len P = 1 let P be RedSequence of ==>.-relation TS; ::_thesis: ( (P . 1) `2 = (P . (len P)) `2 implies len P = 1 ) assume A2: (P . 1) `2 = (P . (len P)) `2 ; ::_thesis: len P = 1 percases ( len P <= 1 or len P > 1 ) ; supposeA3: len P <= 1 ; ::_thesis: len P = 1 len P >= 0 + 1 by NAT_1:13; hence len P = 1 by A3, XXREAL_0:1; ::_thesis: verum end; supposeA4: len P > 1 ; ::_thesis: len P = 1 then reconsider p1 = (len P) - 1 as Nat by NAT_1:21; A5: p1 + 1 = len P ; then A6: p1 <= len P by NAT_1:13; 1 + 1 <= len P by A4, NAT_1:13; then A7: 1 + 1 in dom P by FINSEQ_3:25; 0 + 1 <= p1 + 1 by XREAL_1:6; then A8: p1 + 1 in dom P by FINSEQ_3:25; 1 <= p1 by A4, A5, NAT_1:13; then p1 in dom P by A6, FINSEQ_3:25; then consider s2 being Element of TS, v2 being Element of E ^omega , t2 being Element of TS, w2 being Element of E ^omega such that P . p1 = [s2,v2] and A9: P . (p1 + 1) = [t2,w2] by A8, Th47; 1 in dom P by A4, FINSEQ_3:25; then consider s1 being Element of TS, v1 being Element of E ^omega , t1 being Element of TS, w1 being Element of E ^omega such that A10: P . 1 = [s1,v1] and P . (1 + 1) = [t1,w1] by A7, Th47; (P . (len P)) `2 = w2 by A9, MCART_1:7; then v1 = w2 by A2, A10, MCART_1:7; hence len P = 1 by A1, A10, A9, Th60; ::_thesis: verum end; end; end; theorem Th62: :: REWRITE3:62 for x, y being set for E being non empty set for u being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds len P <= (len u) + 1 proof let x, y be set ; ::_thesis: for E being non empty set for u being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds len P <= (len u) + 1 let E be non empty set ; ::_thesis: for u being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds len P <= (len u) + 1 let u be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds len P <= (len u) + 1 let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds len P <= (len u) + 1 let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds len P <= (len u) + 1 ) defpred S1[ Nat] means for P being RedSequence of ==>.-relation TS for u being Element of E ^omega for x being set st len u = \$1 & P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds len P <= (len u) + 1; assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds len P <= (len u) + 1 A2: now__::_thesis:_for_k_being_Nat_st_(_for_n_being_Nat_st_n_<_k_holds_ S1[n]_)_holds_ S1[k] let k be Nat; ::_thesis: ( ( for n being Nat st n < k holds S1[n] ) implies S1[k] ) assume A3: for n being Nat st n < k holds S1[n] ; ::_thesis: S1[k] now__::_thesis:_for_P_being_RedSequence_of_==>.-relation_TS for_u_being_Element_of_E_^omega_ for_x_being_set_st_len_u_=_k_&_P_._1_=_[x,u]_&_P_._(len_P)_=_[y,(<%>_E)]_holds_ len_P_<=_(len_u)_+_1 let P be RedSequence of ==>.-relation TS; ::_thesis: for u being Element of E ^omega for x being set st len u = k & P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds len b3 <= (len b4) + 1 let u be Element of E ^omega ; ::_thesis: for x being set st len u = k & P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds len b2 <= (len b3) + 1 let x be set ; ::_thesis: ( len u = k & P . 1 = [x,u] & P . (len P) = [y,(<%> E)] implies len b1 <= (len b2) + 1 ) assume that A4: len u = k and A5: P . 1 = [x,u] and A6: P . (len P) = [y,(<%> E)] ; ::_thesis: len b1 <= (len b2) + 1 percases ( len u < 1 or len u >= 1 ) ; suppose len u < 1 ; ::_thesis: len b1 <= (len b2) + 1 then u = <%> E by NAT_1:25; then len P = 1 by A1, A5, A6, Th60; hence len P <= (len u) + 1 by NAT_1:25; ::_thesis: verum end; supposeA7: len u >= 1 ; ::_thesis: len b1 <= (len b2) + 1 A8: len P <> 1 proof assume len P = 1 ; ::_thesis: contradiction then u = <%> E by A5, A6, XTUPLE_0:1; hence contradiction by A7; ::_thesis: verum end; then consider P9 being RedSequence of ==>.-relation TS such that A9: <*(P . 1)*> ^ P9 = P and A10: (len P9) + 1 = len P by Th5, NAT_1:25; A11: len P > 1 by A8, NAT_1:25; then len P >= 1 + 1 by NAT_1:13; then A12: 1 + 1 in dom P by FINSEQ_3:25; A13: 1 in dom P by A11, FINSEQ_3:25; then A14: P . (1 + 1) = [((P . (1 + 1)) `1),((P . (1 + 1)) `2)] by A12, Th48; then A15: [[x,u],[((P . (1 + 1)) `1),((P . (1 + 1)) `2)]] in ==>.-relation TS by A5, A13, A12, REWRITE1:def_2; then reconsider u1 = (P . (1 + 1)) `2 as Element of E ^omega by Th32; A16: ( len <*(P . 1)*> = 1 & len P9 >= 1 ) by FINSEQ_1:39, NAT_1:25; then A17: P9 . 1 = [((P . (1 + 1)) `1),u1] by A9, A14, FINSEQ_1:65; x,u ==>. (P . (1 + 1)) `1 ,u1,TS by A15, Def4; then consider v being Element of E ^omega such that A18: ( x,v -->. (P . (1 + 1)) `1 ,TS & u = v ^ u1 ) by Th22; ( v <> <%> E & len u = (len u1) + (len v) ) by A1, A18, Th15, AFINSQ_1:17; then A19: (len u) - 0 > ((len u1) + (len v)) - (len v) by XREAL_1:15; then A20: (len u1) + 1 <= len u by NAT_1:13; P9 . (len P9) = [y,(<%> E)] by A6, A9, A10, A16, FINSEQ_1:65; then len P9 <= (len u1) + 1 by A3, A4, A19, A17; then len P9 <= len u by A20, XXREAL_0:2; hence len P <= (len u) + 1 by A10, XREAL_1:6; ::_thesis: verum end; end; end; hence S1[k] ; ::_thesis: verum end; for k being Nat holds S1[k] from NAT_1:sch_4(A2); hence for P being RedSequence of ==>.-relation TS st P . 1 = [x,u] & P . (len P) = [y,(<%> E)] holds len P <= (len u) + 1 ; ::_thesis: verum end; theorem Th63: :: REWRITE3:63 for x, y being set for E being non empty set for e being Element of E for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] holds len P = 2 proof let x, y be set ; ::_thesis: for E being non empty set for e being Element of E for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] holds len P = 2 let E be non empty set ; ::_thesis: for e being Element of E for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] holds len P = 2 let e be Element of E; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] holds len P = 2 let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] holds len P = 2 let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies for P being RedSequence of ==>.-relation TS st P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] holds len P = 2 ) assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: for P being RedSequence of ==>.-relation TS st P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] holds len P = 2 let P be RedSequence of ==>.-relation TS; ::_thesis: ( P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] implies len P = 2 ) assume A2: ( P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] ) ; ::_thesis: len P = 2 len P <= (len <%e%>) + 1 by A1, A2, Th62; then A3: len P <= 1 + 1 by AFINSQ_1:34; len P <> 1 by A2, XTUPLE_0:1; hence len P = 2 by A3, NAT_1:26; ::_thesis: verum end; theorem Th64: :: REWRITE3:64 for x, y being set for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] & not len v > len w holds ( len P = 1 & x = y & v = w ) proof let x, y be set ; ::_thesis: for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] & not len v > len w holds ( len P = 1 & x = y & v = w ) let E be non empty set ; ::_thesis: for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] & not len v > len w holds ( len P = 1 & x = y & v = w ) let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] & not len v > len w holds ( len P = 1 & x = y & v = w ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] & not len v > len w holds ( len P = 1 & x = y & v = w ) let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] & not len v > len w holds ( len P = 1 & x = y & v = w ) ) assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: for P being RedSequence of ==>.-relation TS st P . 1 = [x,v] & P . (len P) = [y,w] & not len v > len w holds ( len P = 1 & x = y & v = w ) let P be RedSequence of ==>.-relation TS; ::_thesis: ( P . 1 = [x,v] & P . (len P) = [y,w] & not len v > len w implies ( len P = 1 & x = y & v = w ) ) assume A2: ( P . 1 = [x,v] & P . (len P) = [y,w] ) ; ::_thesis: ( len v > len w or ( len P = 1 & x = y & v = w ) ) consider u being Element of E ^omega such that A3: v = u ^ w by A2, Th53; A4: len v >= len w by A2, Th59; percases ( len v > len w or len v <= len w ) ; suppose len v > len w ; ::_thesis: ( len v > len w or ( len P = 1 & x = y & v = w ) ) hence ( len v > len w or ( len P = 1 & x = y & v = w ) ) ; ::_thesis: verum end; supposeA5: len v <= len w ; ::_thesis: ( len v > len w or ( len P = 1 & x = y & v = w ) ) A6: len v = (len u) + (len w) by A3, AFINSQ_1:17; B: {} ^ w = w ; len v = len w by A4, A5, XXREAL_0:1; then u = <%> E by A6; hence ( len v > len w or ( len P = 1 & x = y & v = w ) ) by A1, A2, Th60, A3, B; ::_thesis: verum end; end; end; theorem :: REWRITE3:65 for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds (P . k) `2 <> (P . (k + 1)) `2 proof let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds (P . k) `2 <> (P . (k + 1)) `2 let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds (P . k) `2 <> (P . (k + 1)) `2 let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds (P . k) `2 <> (P . (k + 1)) `2 ) assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: for P being RedSequence of ==>.-relation TS for k being Nat st k in dom P & k + 1 in dom P holds (P . k) `2 <> (P . (k + 1)) `2 let P be RedSequence of ==>.-relation TS; ::_thesis: for k being Nat st k in dom P & k + 1 in dom P holds (P . k) `2 <> (P . (k + 1)) `2 let k be Nat; ::_thesis: ( k in dom P & k + 1 in dom P implies (P . k) `2 <> (P . (k + 1)) `2 ) assume A2: ( k in dom P & k + 1 in dom P ) ; ::_thesis: (P . k) `2 <> (P . (k + 1)) `2 consider s being Element of TS, u being Element of E ^omega , t being Element of TS, v being Element of E ^omega such that A3: P . k = [s,u] and A4: P . (k + 1) = [t,v] by A2, Th47; [[s,u],[t,v]] in ==>.-relation TS by A2, A3, A4, REWRITE1:def_2; then u <> v by A1, Th43; then (P . k) `2 <> v by A3, MCART_1:7; hence (P . k) `2 <> (P . (k + 1)) `2 by A4, MCART_1:7; ::_thesis: verum end; theorem Th66: :: REWRITE3:66 for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS for k, l being Nat st k in dom P & l in dom P & k < l holds (P . k) `2 <> (P . l) `2 proof let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS for k, l being Nat st k in dom P & l in dom P & k < l holds (P . k) `2 <> (P . l) `2 let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds for P being RedSequence of ==>.-relation TS for k, l being Nat st k in dom P & l in dom P & k < l holds (P . k) `2 <> (P . l) `2 let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies for P being RedSequence of ==>.-relation TS for k, l being Nat st k in dom P & l in dom P & k < l holds (P . k) `2 <> (P . l) `2 ) defpred S1[ Nat] means for P being RedSequence of ==>.-relation TS for k, l being Nat st len P = \$1 & k in dom P & l in dom P & k < l holds (P . k) `2 <> (P . l) `2 ; assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: for P being RedSequence of ==>.-relation TS for k, l being Nat st k in dom P & l in dom P & k < l holds (P . k) `2 <> (P . l) `2 A2: now__::_thesis:_for_i_being_Nat_st_S1[i]_holds_ S1[i_+_1] let i be Nat; ::_thesis: ( S1[i] implies S1[i + 1] ) assume A3: S1[i] ; ::_thesis: S1[i + 1] now__::_thesis:_for_P_being_RedSequence_of_==>.-relation_TS for_k,_l_being_Nat_st_len_P_=_i_+_1_&_k_in_dom_P_&_l_in_dom_P_&_k_<_l_holds_ (P_._k)_`2_<>_(P_._l)_`2 let P be RedSequence of ==>.-relation TS; ::_thesis: for k, l being Nat st len P = i + 1 & k in dom P & l in dom P & k < l holds (b3 . b4) `2 <> (b3 . b5) `2 let k, l be Nat; ::_thesis: ( len P = i + 1 & k in dom P & l in dom P & k < l implies (b1 . b2) `2 <> (b1 . b3) `2 ) assume that A4: len P = i + 1 and A5: k in dom P and A6: l in dom P and A7: k < l ; ::_thesis: (b1 . b2) `2 <> (b1 . b3) `2 A8: i < len P by A4, NAT_1:13; A9: k <= len P by A5, FINSEQ_3:25; A10: 1 <= k by A5, FINSEQ_3:25; A11: 1 <= l by A6, FINSEQ_3:25; A12: l <= len P by A6, FINSEQ_3:25; percases ( ( k = 1 & l = len P ) or ( k <> 1 & l = len P ) or l <> len P ) ; suppose ( k = 1 & l = len P ) ; ::_thesis: (b1 . b2) `2 <> (b1 . b3) `2 hence (P . k) `2 <> (P . l) `2 by A1, A7, Th61; ::_thesis: verum end; supposeA13: ( k <> 1 & l = len P ) ; ::_thesis: (b1 . b2) `2 <> (b1 . b3) `2 reconsider k1 = k - 1 as Nat by A10, NAT_1:21; A14: k > 1 by A10, A13, XXREAL_0:1; then k1 > 1 - 1 by XREAL_1:9; then A15: k1 >= 0 + 1 by NAT_1:13; reconsider l1 = l - 1 as Nat by A11, NAT_1:21; A16: k1 < l1 by A7, XREAL_1:9; A17: l > 1 by A7, A10, A11, XXREAL_0:1; then consider Q being RedSequence of ==>.-relation TS such that A18: <*(P . 1)*> ^ Q = P and A19: (len Q) + 1 = len P by A13, Th5; l1 > 1 - 1 by A17, XREAL_1:9; then A20: l1 >= 0 + 1 by NAT_1:13; k1 <= ((len Q) + 1) - 1 by A9, A19, XREAL_1:9; then A21: k1 in dom Q by A15, FINSEQ_3:25; A22: len <*(P . 1)*> = 1 by FINSEQ_1:40; then A23: P . l = Q . l1 by A12, A17, A18, FINSEQ_1:24; l1 <= ((len Q) + 1) - 1 by A12, A19, XREAL_1:9; then A24: l1 in dom Q by A20, FINSEQ_3:25; P . k = Q . k1 by A9, A14, A18, A22, FINSEQ_1:24; hence (P . k) `2 <> (P . l) `2 by A3, A4, A19, A21, A24, A16, A23; ::_thesis: verum end; supposeA25: l <> len P ; ::_thesis: (b1 . b2) `2 <> (b1 . b3) `2 k < i + 1 by A4, A7, A12, XXREAL_0:2; then A26: k <= i by NAT_1:13; then reconsider Q = P | i as RedSequence of ==>.-relation TS by A10, REWRITE2:3, XXREAL_0:2; A27: P . k = Q . k by A26, FINSEQ_3:112; l < i + 1 by A4, A12, A25, XXREAL_0:1; then A28: l <= i by NAT_1:13; then A29: P . l = Q . l by FINSEQ_3:112; k <= len Q by A8, A26, FINSEQ_1:59; then A30: k in dom Q by A10, FINSEQ_3:25; l <= len Q by A8, A28, FINSEQ_1:59; then A31: l in dom Q by A11, FINSEQ_3:25; len Q = i by A8, FINSEQ_1:59; hence (P . k) `2 <> (P . l) `2 by A3, A7, A30, A31, A27, A29; ::_thesis: verum end; end; end; hence S1[i + 1] ; ::_thesis: verum end; A32: S1[ 0 ] ; A33: for i being Nat holds S1[i] from NAT_1:sch_2(A32, A2); let P be RedSequence of ==>.-relation TS; ::_thesis: for k, l being Nat st k in dom P & l in dom P & k < l holds (P . k) `2 <> (P . l) `2 let k, l be Nat; ::_thesis: ( k in dom P & l in dom P & k < l implies (P . k) `2 <> (P . l) `2 ) assume A34: ( k in dom P & l in dom P & k < l ) ; ::_thesis: (P . k) `2 <> (P . l) `2 len P = len P ; hence (P . k) `2 <> (P . l) `2 by A33, A34; ::_thesis: verum end; theorem Th67: :: REWRITE3:67 for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic holds for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 holds for k being Nat st k in dom P & k in dom Q holds P . k = Q . k proof let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic holds for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 holds for k being Nat st k in dom P & k in dom Q holds P . k = Q . k let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st TS is deterministic holds for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 holds for k being Nat st k in dom P & k in dom Q holds P . k = Q . k let TS be non empty transition-system over F; ::_thesis: ( TS is deterministic implies for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 holds for k being Nat st k in dom P & k in dom Q holds P . k = Q . k ) assume A1: TS is deterministic ; ::_thesis: for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 holds for k being Nat st k in dom P & k in dom Q holds P . k = Q . k let P, Q be RedSequence of ==>.-relation TS; ::_thesis: ( P . 1 = Q . 1 implies for k being Nat st k in dom P & k in dom Q holds P . k = Q . k ) assume A2: P . 1 = Q . 1 ; ::_thesis: for k being Nat st k in dom P & k in dom Q holds P . k = Q . k defpred S1[ Nat] means ( \$1 in dom P & \$1 in dom Q implies P . \$1 = Q . \$1 ); A3: now__::_thesis:_for_k_being_Nat_st_S1[k]_holds_ S1[k_+_1] let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A4: S1[k] ; ::_thesis: S1[k + 1] now__::_thesis:_(_k_+_1_in_dom_P_&_k_+_1_in_dom_Q_implies_P_._(k_+_1)_=_Q_._(k_+_1)_) assume A5: ( k + 1 in dom P & k + 1 in dom Q ) ; ::_thesis: P . (k + 1) = Q . (k + 1) percases ( ( k in dom P & k in dom Q ) or not k in dom P or not k in dom Q ) ; supposeA6: ( k in dom P & k in dom Q ) ; ::_thesis: P . (k + 1) = Q . (k + 1) then ( [(P . k),(P . (k + 1))] in ==>.-relation TS & [(Q . k),(Q . (k + 1))] in ==>.-relation TS ) by A5, REWRITE1:def_2; hence P . (k + 1) = Q . (k + 1) by A1, A4, A6, Th44; ::_thesis: verum end; suppose ( not k in dom P or not k in dom Q ) ; ::_thesis: P . (k + 1) = Q . (k + 1) then k = 0 by A5, REWRITE2:1; hence P . (k + 1) = Q . (k + 1) by A2; ::_thesis: verum end; end; end; hence S1[k + 1] ; ::_thesis: verum end; A7: S1[ 0 ] by FINSEQ_3:25; for k being Nat holds S1[k] from NAT_1:sch_2(A7, A3); hence for k being Nat st k in dom P & k in dom Q holds P . k = Q . k ; ::_thesis: verum end; theorem Th68: :: REWRITE3:68 for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic holds for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & len P = len Q holds P = Q proof let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic holds for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & len P = len Q holds P = Q let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st TS is deterministic holds for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & len P = len Q holds P = Q let TS be non empty transition-system over F; ::_thesis: ( TS is deterministic implies for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & len P = len Q holds P = Q ) assume A1: TS is deterministic ; ::_thesis: for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & len P = len Q holds P = Q let P, Q be RedSequence of ==>.-relation TS; ::_thesis: ( P . 1 = Q . 1 & len P = len Q implies P = Q ) assume that A2: P . 1 = Q . 1 and A3: len P = len Q ; ::_thesis: P = Q now__::_thesis:_for_k_being_Nat_st_k_in_dom_P_holds_ P_._k_=_Q_._k let k be Nat; ::_thesis: ( k in dom P implies P . k = Q . k ) assume A4: k in dom P ; ::_thesis: P . k = Q . k then ( 1 <= k & k <= len P ) by FINSEQ_3:25; then k in dom Q by A3, FINSEQ_3:25; hence P . k = Q . k by A1, A2, A4, Th67; ::_thesis: verum end; hence P = Q by A3, FINSEQ_2:9; ::_thesis: verum end; theorem Th69: :: REWRITE3:69 for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic holds for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & (P . (len P)) `2 = (Q . (len Q)) `2 holds P = Q proof let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic holds for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & (P . (len P)) `2 = (Q . (len Q)) `2 holds P = Q let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st TS is deterministic holds for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & (P . (len P)) `2 = (Q . (len Q)) `2 holds P = Q let TS be non empty transition-system over F; ::_thesis: ( TS is deterministic implies for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & (P . (len P)) `2 = (Q . (len Q)) `2 holds P = Q ) assume A1: TS is deterministic ; ::_thesis: for P, Q being RedSequence of ==>.-relation TS st P . 1 = Q . 1 & (P . (len P)) `2 = (Q . (len Q)) `2 holds P = Q then A2: not <%> E in rng (dom the Tran of TS) by Def1; let P, Q be RedSequence of ==>.-relation TS; ::_thesis: ( P . 1 = Q . 1 & (P . (len P)) `2 = (Q . (len Q)) `2 implies P = Q ) assume that A3: P . 1 = Q . 1 and A4: (P . (len P)) `2 = (Q . (len Q)) `2 ; ::_thesis: P = Q percases ( len P = len Q or len P > len Q or len P < len Q ) by XXREAL_0:1; suppose len P = len Q ; ::_thesis: P = Q hence P = Q by A1, A3, Th68; ::_thesis: verum end; supposeA5: len P > len Q ; ::_thesis: P = Q len P >= 0 + 1 by NAT_1:13; then A6: len P in dom P by FINSEQ_3:25; set k = len Q; A7: len Q >= 0 + 1 by NAT_1:13; then A8: len Q in dom P by A5, FINSEQ_3:25; len Q in dom Q by A7, FINSEQ_3:25; then (P . (len Q)) `2 = (P . (len P)) `2 by A1, A3, A4, A8, Th67; hence P = Q by A2, A5, A8, A6, Th66; ::_thesis: verum end; supposeA9: len P < len Q ; ::_thesis: P = Q len Q >= 0 + 1 by NAT_1:13; then A10: len Q in dom Q by FINSEQ_3:25; set k = len P; A11: len P >= 0 + 1 by NAT_1:13; then A12: len P in dom Q by A9, FINSEQ_3:25; len P in dom P by A11, FINSEQ_3:25; then (Q . (len P)) `2 = (Q . (len Q)) `2 by A1, A3, A4, A12, Th67; hence P = Q by A2, A9, A12, A10, Th66; ::_thesis: verum end; end; end; begin theorem Th70: :: REWRITE3:70 for x, y being set for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds ex u being Element of E ^omega st v = u ^ w proof let x, y be set ; ::_thesis: for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds ex u being Element of E ^omega st v = u ^ w let E be non empty set ; ::_thesis: for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds ex u being Element of E ^omega st v = u ^ w let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds ex u being Element of E ^omega st v = u ^ w let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds ex u being Element of E ^omega st v = u ^ w let TS be non empty transition-system over F; ::_thesis: ( ==>.-relation TS reduces [x,v],[y,w] implies ex u being Element of E ^omega st v = u ^ w ) assume ==>.-relation TS reduces [x,v],[y,w] ; ::_thesis: ex u being Element of E ^omega st v = u ^ w then ex P being RedSequence of ==>.-relation TS st ( P . 1 = [x,v] & P . (len P) = [y,w] ) by REWRITE1:def_3; hence ex u being Element of E ^omega st v = u ^ w by Th53; ::_thesis: verum end; theorem Th71: :: REWRITE3:71 for x, y being set for E being non empty set for u, v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st ==>.-relation TS reduces [x,u],[y,v] holds ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] proof let x, y be set ; ::_thesis: for E being non empty set for u, v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st ==>.-relation TS reduces [x,u],[y,v] holds ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] let E be non empty set ; ::_thesis: for u, v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st ==>.-relation TS reduces [x,u],[y,v] holds ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] let u, v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st ==>.-relation TS reduces [x,u],[y,v] holds ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st ==>.-relation TS reduces [x,u],[y,v] holds ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] let TS be non empty transition-system over F; ::_thesis: ( ==>.-relation TS reduces [x,u],[y,v] implies ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] ) assume ==>.-relation TS reduces [x,u],[y,v] ; ::_thesis: ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] then consider P being RedSequence of ==>.-relation TS such that A1: P . 1 = [x,u] and A2: P . (len P) = [y,v] by REWRITE1:def_3; A3: len P >= 0 + 1 by NAT_1:13; then len P in dom P by FINSEQ_3:25; then A4: dim2 ((P . (len P)),E) = (P . (len P)) `2 by A1, Th51 .= v by A2, MCART_1:7 ; deffunc H1( set ) -> set = [((P . \$1) `1),((dim2 ((P . \$1),E)) ^ w)]; consider Q being FinSequence such that A5: len Q = len P and A6: for k being Nat st k in dom Q holds Q . k = H1(k) from FINSEQ_1:sch_2(); for k being Element of NAT st k in dom Q & k + 1 in dom Q holds [(Q . k),(Q . (k + 1))] in ==>.-relation TS proof let k be Element of NAT ; ::_thesis: ( k in dom Q & k + 1 in dom Q implies [(Q . k),(Q . (k + 1))] in ==>.-relation TS ) assume that A7: k in dom Q and A8: k + 1 in dom Q ; ::_thesis: [(Q . k),(Q . (k + 1))] in ==>.-relation TS ( 1 <= k + 1 & k + 1 <= len Q ) by A8, FINSEQ_3:25; then A9: k + 1 in dom P by A5, FINSEQ_3:25; ( 1 <= k & k <= len Q ) by A7, FINSEQ_3:25; then A10: k in dom P by A5, FINSEQ_3:25; then [(P . k),(P . (k + 1))] in ==>.-relation TS by A9, REWRITE1:def_2; then [[((P . k) `1),((P . k) `2)],(P . (k + 1))] in ==>.-relation TS by A10, A9, Th48; then [[((P . k) `1),((P . k) `2)],[((P . (k + 1)) `1),((P . (k + 1)) `2)]] in ==>.-relation TS by A10, A9, Th48; then [[((P . k) `1),(dim2 ((P . k),E))],[((P . (k + 1)) `1),((P . (k + 1)) `2)]] in ==>.-relation TS by A1, A10, Th51; then [[((P . k) `1),(dim2 ((P . k),E))],[((P . (k + 1)) `1),(dim2 ((P . (k + 1)),E))]] in ==>.-relation TS by A1, A9, Th51; then (P . k) `1 , dim2 ((P . k),E) ==>. (P . (k + 1)) `1 , dim2 ((P . (k + 1)),E),TS by Def4; then (P . k) `1 ,(dim2 ((P . k),E)) ^ w ==>. (P . (k + 1)) `1 ,(dim2 ((P . (k + 1)),E)) ^ w,TS by Th25; then [[((P . k) `1),((dim2 ((P . k),E)) ^ w)],[((P . (k + 1)) `1),((dim2 ((P . (k + 1)),E)) ^ w)]] in ==>.-relation TS by Def4; then [[((P . k) `1),((dim2 ((P . k),E)) ^ w)],(Q . (k + 1))] in ==>.-relation TS by A6, A8; hence [(Q . k),(Q . (k + 1))] in ==>.-relation TS by A6, A7; ::_thesis: verum end; then reconsider Q = Q as RedSequence of ==>.-relation TS by A5, REWRITE1:def_2; A11: len Q >= 0 + 1 by NAT_1:13; then len Q in dom Q by FINSEQ_3:25; then Q . (len Q) = [((P . (len Q)) `1),((dim2 ((P . (len Q)),E)) ^ w)] by A6; then A12: Q . (len Q) = [y,(v ^ w)] by A2, A5, A4, MCART_1:7; 1 in dom P by A3, FINSEQ_3:25; then A13: dim2 ((P . 1),E) = (P . 1) `2 by A1, Th51 .= u by A1, MCART_1:7 ; 1 in dom Q by A11, FINSEQ_3:25; then Q . 1 = [((P . 1) `1),((dim2 ((P . 1),E)) ^ w)] by A6 .= [x,(u ^ w)] by A1, A13, MCART_1:7 ; hence ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] by A12, REWRITE1:def_3; ::_thesis: verum end; theorem Th72: :: REWRITE3:72 for x, y, z being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,y -->. z,TS holds ==>.-relation TS reduces [x,y],[z,(<%> E)] proof let x, y, z be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,y -->. z,TS holds ==>.-relation TS reduces [x,y],[z,(<%> E)] let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,y -->. z,TS holds ==>.-relation TS reduces [x,y],[z,(<%> E)] let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,y -->. z,TS holds ==>.-relation TS reduces [x,y],[z,(<%> E)] let TS be non empty transition-system over F; ::_thesis: ( x,y -->. z,TS implies ==>.-relation TS reduces [x,y],[z,(<%> E)] ) assume x,y -->. z,TS ; ::_thesis: ==>.-relation TS reduces [x,y],[z,(<%> E)] then <*[x,y],[z,(<%> E)]*> is RedSequence of ==>.-relation TS by Th57; then [[x,y],[z,(<%> E)]] in ==>.-relation TS by Th8; hence ==>.-relation TS reduces [x,y],[z,(<%> E)] by REWRITE1:15; ::_thesis: verum end; theorem Th73: :: REWRITE3:73 for x, y being set for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,v -->. y,TS holds ==>.-relation TS reduces [x,(v ^ w)],[y,w] proof let x, y be set ; ::_thesis: for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,v -->. y,TS holds ==>.-relation TS reduces [x,(v ^ w)],[y,w] let E be non empty set ; ::_thesis: for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,v -->. y,TS holds ==>.-relation TS reduces [x,(v ^ w)],[y,w] let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,v -->. y,TS holds ==>.-relation TS reduces [x,(v ^ w)],[y,w] let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,v -->. y,TS holds ==>.-relation TS reduces [x,(v ^ w)],[y,w] let TS be non empty transition-system over F; ::_thesis: ( x,v -->. y,TS implies ==>.-relation TS reduces [x,(v ^ w)],[y,w] ) assume x,v -->. y,TS ; ::_thesis: ==>.-relation TS reduces [x,(v ^ w)],[y,w] then <*[x,(v ^ w)],[y,w]*> is RedSequence of ==>.-relation TS by Th58; then [[x,(v ^ w)],[y,w]] in ==>.-relation TS by Th8; hence ==>.-relation TS reduces [x,(v ^ w)],[y,w] by REWRITE1:15; ::_thesis: verum end; theorem Th74: :: REWRITE3:74 for x1, x2, y1, y2 being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds ==>.-relation TS reduces [x1,x2],[y1,y2] proof let x1, x2, y1, y2 be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds ==>.-relation TS reduces [x1,x2],[y1,y2] let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds ==>.-relation TS reduces [x1,x2],[y1,y2] let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds ==>.-relation TS reduces [x1,x2],[y1,y2] let TS be non empty transition-system over F; ::_thesis: ( x1,x2 ==>. y1,y2,TS implies ==>.-relation TS reduces [x1,x2],[y1,y2] ) assume x1,x2 ==>. y1,y2,TS ; ::_thesis: ==>.-relation TS reduces [x1,x2],[y1,y2] then [[x1,x2],[y1,y2]] in ==>.-relation TS by Def4; hence ==>.-relation TS reduces [x1,x2],[y1,y2] by REWRITE1:15; ::_thesis: verum end; theorem Th75: :: REWRITE3:75 for x, y being set for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds len v >= len w proof let x, y be set ; ::_thesis: for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds len v >= len w let E be non empty set ; ::_thesis: for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds len v >= len w let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds len v >= len w let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st ==>.-relation TS reduces [x,v],[y,w] holds len v >= len w let TS be non empty transition-system over F; ::_thesis: ( ==>.-relation TS reduces [x,v],[y,w] implies len v >= len w ) assume ==>.-relation TS reduces [x,v],[y,w] ; ::_thesis: len v >= len w then ex P being RedSequence of ==>.-relation TS st ( P . 1 = [x,v] & P . (len P) = [y,w] ) by REWRITE1:def_3; hence len v >= len w by Th59; ::_thesis: verum end; theorem :: REWRITE3:76 for x, y being set for E being non empty set for w, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st ==>.-relation TS reduces [x,w],[y,(v ^ w)] holds v = <%> E proof let x, y be set ; ::_thesis: for E being non empty set for w, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st ==>.-relation TS reduces [x,w],[y,(v ^ w)] holds v = <%> E let E be non empty set ; ::_thesis: for w, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st ==>.-relation TS reduces [x,w],[y,(v ^ w)] holds v = <%> E let w, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st ==>.-relation TS reduces [x,w],[y,(v ^ w)] holds v = <%> E let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st ==>.-relation TS reduces [x,w],[y,(v ^ w)] holds v = <%> E let TS be non empty transition-system over F; ::_thesis: ( ==>.-relation TS reduces [x,w],[y,(v ^ w)] implies v = <%> E ) assume ==>.-relation TS reduces [x,w],[y,(v ^ w)] ; ::_thesis: v = <%> E then len w >= len (v ^ w) by Th75; then (len v) + (len w) <= 0 + (len w) by AFINSQ_1:17; hence v = <%> E by XREAL_1:6; ::_thesis: verum end; theorem Th77: :: REWRITE3:77 for x, y being set for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F holds ( <%> E in rng (dom the Tran of TS) or not ==>.-relation TS reduces [x,v],[y,w] or len v > len w or ( x = y & v = w ) ) proof let x, y be set ; ::_thesis: for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F holds ( <%> E in rng (dom the Tran of TS) or not ==>.-relation TS reduces [x,v],[y,w] or len v > len w or ( x = y & v = w ) ) let E be non empty set ; ::_thesis: for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F holds ( <%> E in rng (dom the Tran of TS) or not ==>.-relation TS reduces [x,v],[y,w] or len v > len w or ( x = y & v = w ) ) let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F holds ( <%> E in rng (dom the Tran of TS) or not ==>.-relation TS reduces [x,v],[y,w] or len v > len w or ( x = y & v = w ) ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F holds ( <%> E in rng (dom the Tran of TS) or not ==>.-relation TS reduces [x,v],[y,w] or len v > len w or ( x = y & v = w ) ) let TS be non empty transition-system over F; ::_thesis: ( <%> E in rng (dom the Tran of TS) or not ==>.-relation TS reduces [x,v],[y,w] or len v > len w or ( x = y & v = w ) ) assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: ( not ==>.-relation TS reduces [x,v],[y,w] or len v > len w or ( x = y & v = w ) ) assume ==>.-relation TS reduces [x,v],[y,w] ; ::_thesis: ( len v > len w or ( x = y & v = w ) ) then ex P being RedSequence of ==>.-relation TS st ( P . 1 = [x,v] & P . (len P) = [y,w] ) by REWRITE1:def_3; hence ( len v > len w or ( x = y & v = w ) ) by A1, Th64; ::_thesis: verum end; theorem :: REWRITE3:78 for x, y being set for E being non empty set for u being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,u],[y,u] holds x = y proof let x, y be set ; ::_thesis: for E being non empty set for u being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,u],[y,u] holds x = y let E be non empty set ; ::_thesis: for u being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,u],[y,u] holds x = y let u be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,u],[y,u] holds x = y let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,u],[y,u] holds x = y let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,u],[y,u] implies x = y ) assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: ( not ==>.-relation TS reduces [x,u],[y,u] or x = y ) assume ==>.-relation TS reduces [x,u],[y,u] ; ::_thesis: x = y then ( len u > len u or x = y ) by A1, Th77; hence x = y ; ::_thesis: verum end; theorem Th79: :: REWRITE3:79 for x, y being set for E being non empty set for e being Element of E for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] holds [[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS proof let x, y be set ; ::_thesis: for E being non empty set for e being Element of E for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] holds [[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS let E be non empty set ; ::_thesis: for e being Element of E for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] holds [[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS let e be Element of E; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] holds [[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] holds [[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) & ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] implies [[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS ) assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: ( not ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] or [[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS ) assume ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] ; ::_thesis: [[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS then consider P being RedSequence of ==>.-relation TS such that A2: ( P . 1 = [x,<%e%>] & P . (len P) = [y,(<%> E)] ) by REWRITE1:def_3; A3: len P = 1 + 1 by A1, A2, Th63; then ( 1 in dom P & 1 + 1 in dom P ) by FINSEQ_3:25; hence [[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS by A2, A3, REWRITE1:def_2; ::_thesis: verum end; theorem Th80: :: REWRITE3:80 for x, y1, z, y2 being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] holds y1 = y2 proof let x, y1, z, y2 be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] holds y1 = y2 let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] holds y1 = y2 let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st TS is deterministic & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] holds y1 = y2 let TS be non empty transition-system over F; ::_thesis: ( TS is deterministic & ==>.-relation TS reduces x,[y1,z] & ==>.-relation TS reduces x,[y2,z] implies y1 = y2 ) assume A1: TS is deterministic ; ::_thesis: ( not ==>.-relation TS reduces x,[y1,z] or not ==>.-relation TS reduces x,[y2,z] or y1 = y2 ) assume that A2: ==>.-relation TS reduces x,[y1,z] and A3: ==>.-relation TS reduces x,[y2,z] ; ::_thesis: y1 = y2 consider P being RedSequence of ==>.-relation TS such that A4: P . 1 = x and A5: P . (len P) = [y1,z] by A2, REWRITE1:def_3; consider Q being RedSequence of ==>.-relation TS such that A6: Q . 1 = x and A7: Q . (len Q) = [y2,z] by A3, REWRITE1:def_3; A8: (Q . (len Q)) `2 = z by A7, MCART_1:7; (P . (len P)) `2 = z by A5, MCART_1:7; then P = Q by A1, A4, A6, A8, Th69; hence y1 = y2 by A5, A7, XTUPLE_0:1; ::_thesis: verum end; begin definition let E be non empty set ; let F be Subset of (E ^omega); let TS be non empty transition-system over F; let x1, x2, y1, y2 be set ; predx1,x2 ==>* y1,y2,TS means :Def6: :: REWRITE3:def 6 ==>.-relation TS reduces [x1,x2],[y1,y2]; end; :: deftheorem Def6 defines ==>* REWRITE3:def_6_:_ for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F for x1, x2, y1, y2 being set holds ( x1,x2 ==>* y1,y2,TS iff ==>.-relation TS reduces [x1,x2],[y1,y2] ); theorem Th81: :: REWRITE3:81 for x1, x2, y1, y2 being set for E being non empty set for F1, F2 being Subset of (E ^omega) for TS1 being non empty transition-system over F1 for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x1,x2 ==>* y1,y2,TS1 holds x1,x2 ==>* y1,y2,TS2 proof let x1, x2, y1, y2 be set ; ::_thesis: for E being non empty set for F1, F2 being Subset of (E ^omega) for TS1 being non empty transition-system over F1 for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x1,x2 ==>* y1,y2,TS1 holds x1,x2 ==>* y1,y2,TS2 let E be non empty set ; ::_thesis: for F1, F2 being Subset of (E ^omega) for TS1 being non empty transition-system over F1 for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x1,x2 ==>* y1,y2,TS1 holds x1,x2 ==>* y1,y2,TS2 let F1, F2 be Subset of (E ^omega); ::_thesis: for TS1 being non empty transition-system over F1 for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x1,x2 ==>* y1,y2,TS1 holds x1,x2 ==>* y1,y2,TS2 let TS1 be non empty transition-system over F1; ::_thesis: for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x1,x2 ==>* y1,y2,TS1 holds x1,x2 ==>* y1,y2,TS2 let TS2 be non empty transition-system over F2; ::_thesis: ( the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x1,x2 ==>* y1,y2,TS1 implies x1,x2 ==>* y1,y2,TS2 ) assume A1: ( the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 ) ; ::_thesis: ( not x1,x2 ==>* y1,y2,TS1 or x1,x2 ==>* y1,y2,TS2 ) assume x1,x2 ==>* y1,y2,TS1 ; ::_thesis: x1,x2 ==>* y1,y2,TS2 then ==>.-relation TS1 reduces [x1,x2],[y1,y2] by Def6; then ==>.-relation TS2 reduces [x1,x2],[y1,y2] by A1, Th34; hence x1,x2 ==>* y1,y2,TS2 by Def6; ::_thesis: verum end; theorem Th82: :: REWRITE3:82 for x, y being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F holds x,y ==>* x,y,TS proof let x, y be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F holds x,y ==>* x,y,TS let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F holds x,y ==>* x,y,TS let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F holds x,y ==>* x,y,TS let TS be non empty transition-system over F; ::_thesis: x,y ==>* x,y,TS ==>.-relation TS reduces [x,y],[x,y] by REWRITE1:12; hence x,y ==>* x,y,TS by Def6; ::_thesis: verum end; theorem Th83: :: REWRITE3:83 for x1, x2, y1, y2, z1, z2 being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st x1,x2 ==>* y1,y2,TS & y1,y2 ==>* z1,z2,TS holds x1,x2 ==>* z1,z2,TS proof let x1, x2, y1, y2, z1, z2 be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st x1,x2 ==>* y1,y2,TS & y1,y2 ==>* z1,z2,TS holds x1,x2 ==>* z1,z2,TS let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st x1,x2 ==>* y1,y2,TS & y1,y2 ==>* z1,z2,TS holds x1,x2 ==>* z1,z2,TS let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x1,x2 ==>* y1,y2,TS & y1,y2 ==>* z1,z2,TS holds x1,x2 ==>* z1,z2,TS let TS be non empty transition-system over F; ::_thesis: ( x1,x2 ==>* y1,y2,TS & y1,y2 ==>* z1,z2,TS implies x1,x2 ==>* z1,z2,TS ) assume ( x1,x2 ==>* y1,y2,TS & y1,y2 ==>* z1,z2,TS ) ; ::_thesis: x1,x2 ==>* z1,z2,TS then ( ==>.-relation TS reduces [x1,x2],[y1,y2] & ==>.-relation TS reduces [y1,y2],[z1,z2] ) by Def6; then ==>.-relation TS reduces [x1,x2],[z1,z2] by REWRITE1:16; hence x1,x2 ==>* z1,z2,TS by Def6; ::_thesis: verum end; theorem Th84: :: REWRITE3:84 for x, y, z being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,y -->. z,TS holds x,y ==>* z, <%> E,TS proof let x, y, z be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,y -->. z,TS holds x,y ==>* z, <%> E,TS let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,y -->. z,TS holds x,y ==>* z, <%> E,TS let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,y -->. z,TS holds x,y ==>* z, <%> E,TS let TS be non empty transition-system over F; ::_thesis: ( x,y -->. z,TS implies x,y ==>* z, <%> E,TS ) assume x,y -->. z,TS ; ::_thesis: x,y ==>* z, <%> E,TS then ==>.-relation TS reduces [x,y],[z,(<%> E)] by Th72; hence x,y ==>* z, <%> E,TS by Def6; ::_thesis: verum end; theorem :: REWRITE3:85 for x, y being set for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,v -->. y,TS holds x,v ^ w ==>* y,w,TS proof let x, y be set ; ::_thesis: for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,v -->. y,TS holds x,v ^ w ==>* y,w,TS let E be non empty set ; ::_thesis: for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,v -->. y,TS holds x,v ^ w ==>* y,w,TS let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,v -->. y,TS holds x,v ^ w ==>* y,w,TS let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,v -->. y,TS holds x,v ^ w ==>* y,w,TS let TS be non empty transition-system over F; ::_thesis: ( x,v -->. y,TS implies x,v ^ w ==>* y,w,TS ) assume x,v -->. y,TS ; ::_thesis: x,v ^ w ==>* y,w,TS then ==>.-relation TS reduces [x,(v ^ w)],[y,w] by Th73; hence x,v ^ w ==>* y,w,TS by Def6; ::_thesis: verum end; theorem Th86: :: REWRITE3:86 for x, y being set for E being non empty set for u, v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,u ==>* y,v,TS holds x,u ^ w ==>* y,v ^ w,TS proof let x, y be set ; ::_thesis: for E being non empty set for u, v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,u ==>* y,v,TS holds x,u ^ w ==>* y,v ^ w,TS let E be non empty set ; ::_thesis: for u, v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,u ==>* y,v,TS holds x,u ^ w ==>* y,v ^ w,TS let u, v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,u ==>* y,v,TS holds x,u ^ w ==>* y,v ^ w,TS let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,u ==>* y,v,TS holds x,u ^ w ==>* y,v ^ w,TS let TS be non empty transition-system over F; ::_thesis: ( x,u ==>* y,v,TS implies x,u ^ w ==>* y,v ^ w,TS ) assume x,u ==>* y,v,TS ; ::_thesis: x,u ^ w ==>* y,v ^ w,TS then ==>.-relation TS reduces [x,u],[y,v] by Def6; then ==>.-relation TS reduces [x,(u ^ w)],[y,(v ^ w)] by Th71; hence x,u ^ w ==>* y,v ^ w,TS by Def6; ::_thesis: verum end; theorem Th87: :: REWRITE3:87 for x1, x2, y1, y2 being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds x1,x2 ==>* y1,y2,TS proof let x1, x2, y1, y2 be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds x1,x2 ==>* y1,y2,TS let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds x1,x2 ==>* y1,y2,TS let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x1,x2 ==>. y1,y2,TS holds x1,x2 ==>* y1,y2,TS let TS be non empty transition-system over F; ::_thesis: ( x1,x2 ==>. y1,y2,TS implies x1,x2 ==>* y1,y2,TS ) assume x1,x2 ==>. y1,y2,TS ; ::_thesis: x1,x2 ==>* y1,y2,TS then ==>.-relation TS reduces [x1,x2],[y1,y2] by Th74; hence x1,x2 ==>* y1,y2,TS by Def6; ::_thesis: verum end; theorem Th88: :: REWRITE3:88 for x, y being set for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,v ==>* y,w,TS holds ex u being Element of E ^omega st v = u ^ w proof let x, y be set ; ::_thesis: for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,v ==>* y,w,TS holds ex u being Element of E ^omega st v = u ^ w let E be non empty set ; ::_thesis: for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,v ==>* y,w,TS holds ex u being Element of E ^omega st v = u ^ w let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,v ==>* y,w,TS holds ex u being Element of E ^omega st v = u ^ w let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,v ==>* y,w,TS holds ex u being Element of E ^omega st v = u ^ w let TS be non empty transition-system over F; ::_thesis: ( x,v ==>* y,w,TS implies ex u being Element of E ^omega st v = u ^ w ) assume x,v ==>* y,w,TS ; ::_thesis: ex u being Element of E ^omega st v = u ^ w then ==>.-relation TS reduces [x,v],[y,w] by Def6; hence ex u being Element of E ^omega st v = u ^ w by Th70; ::_thesis: verum end; theorem Th89: :: REWRITE3:89 for x, y being set for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,v ==>* y,w,TS holds len w <= len v proof let x, y be set ; ::_thesis: for E being non empty set for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,v ==>* y,w,TS holds len w <= len v let E be non empty set ; ::_thesis: for v, w being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,v ==>* y,w,TS holds len w <= len v let v, w be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,v ==>* y,w,TS holds len w <= len v let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,v ==>* y,w,TS holds len w <= len v let TS be non empty transition-system over F; ::_thesis: ( x,v ==>* y,w,TS implies len w <= len v ) assume x,v ==>* y,w,TS ; ::_thesis: len w <= len v then ex u being Element of E ^omega st v = u ^ w by Th88; hence len w <= len v by Th9; ::_thesis: verum end; theorem :: REWRITE3:90 for x, y being set for E being non empty set for w, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,w ==>* y,v ^ w,TS holds v = <%> E proof let x, y be set ; ::_thesis: for E being non empty set for w, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,w ==>* y,v ^ w,TS holds v = <%> E let E be non empty set ; ::_thesis: for w, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,w ==>* y,v ^ w,TS holds v = <%> E let w, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,w ==>* y,v ^ w,TS holds v = <%> E let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,w ==>* y,v ^ w,TS holds v = <%> E let TS be non empty transition-system over F; ::_thesis: ( x,w ==>* y,v ^ w,TS implies v = <%> E ) assume x,w ==>* y,v ^ w,TS ; ::_thesis: v = <%> E then len (v ^ w) <= len w by Th89; then (len v) + (len w) <= 0 + (len w) by AFINSQ_1:17; hence v = <%> E by XREAL_1:6; ::_thesis: verum end; theorem Th91: :: REWRITE3:91 for x, y being set for E being non empty set for u being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds ( x,u ==>* y,u,TS iff x = y ) proof let x, y be set ; ::_thesis: for E being non empty set for u being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds ( x,u ==>* y,u,TS iff x = y ) let E be non empty set ; ::_thesis: for u being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds ( x,u ==>* y,u,TS iff x = y ) let u be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds ( x,u ==>* y,u,TS iff x = y ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds ( x,u ==>* y,u,TS iff x = y ) let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies ( x,u ==>* y,u,TS iff x = y ) ) assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: ( x,u ==>* y,u,TS iff x = y ) thus ( x,u ==>* y,u,TS implies x = y ) ::_thesis: ( x = y implies x,u ==>* y,u,TS ) proof assume x,u ==>* y,u,TS ; ::_thesis: x = y then ==>.-relation TS reduces [x,u],[y,u] by Def6; then ex p being RedSequence of ==>.-relation TS st ( p . 1 = [x,u] & p . (len p) = [y,u] ) by REWRITE1:def_3; hence x = y by A1, Th60; ::_thesis: verum end; assume x = y ; ::_thesis: x,u ==>* y,u,TS hence x,u ==>* y,u,TS by Th82; ::_thesis: verum end; theorem Th92: :: REWRITE3:92 for x, y being set for E being non empty set for e being Element of E for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y, <%> E,TS holds x,<%e%> ==>. y, <%> E,TS proof let x, y be set ; ::_thesis: for E being non empty set for e being Element of E for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y, <%> E,TS holds x,<%e%> ==>. y, <%> E,TS let E be non empty set ; ::_thesis: for e being Element of E for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y, <%> E,TS holds x,<%e%> ==>. y, <%> E,TS let e be Element of E; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y, <%> E,TS holds x,<%e%> ==>. y, <%> E,TS let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y, <%> E,TS holds x,<%e%> ==>. y, <%> E,TS let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y, <%> E,TS implies x,<%e%> ==>. y, <%> E,TS ) assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: ( not x,<%e%> ==>* y, <%> E,TS or x,<%e%> ==>. y, <%> E,TS ) assume x,<%e%> ==>* y, <%> E,TS ; ::_thesis: x,<%e%> ==>. y, <%> E,TS then ==>.-relation TS reduces [x,<%e%>],[y,(<%> E)] by Def6; then [[x,<%e%>],[y,(<%> E)]] in ==>.-relation TS by A1, Th79; hence x,<%e%> ==>. y, <%> E,TS by Def4; ::_thesis: verum end; theorem Th93: :: REWRITE3:93 for x1, x2, y1, z, y2 being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic & x1,x2 ==>* y1,z,TS & x1,x2 ==>* y2,z,TS holds y1 = y2 proof let x1, x2, y1, z, y2 be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic & x1,x2 ==>* y1,z,TS & x1,x2 ==>* y2,z,TS holds y1 = y2 let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic & x1,x2 ==>* y1,z,TS & x1,x2 ==>* y2,z,TS holds y1 = y2 let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st TS is deterministic & x1,x2 ==>* y1,z,TS & x1,x2 ==>* y2,z,TS holds y1 = y2 let TS be non empty transition-system over F; ::_thesis: ( TS is deterministic & x1,x2 ==>* y1,z,TS & x1,x2 ==>* y2,z,TS implies y1 = y2 ) assume A1: TS is deterministic ; ::_thesis: ( not x1,x2 ==>* y1,z,TS or not x1,x2 ==>* y2,z,TS or y1 = y2 ) assume ( x1,x2 ==>* y1,z,TS & x1,x2 ==>* y2,z,TS ) ; ::_thesis: y1 = y2 then ( ==>.-relation TS reduces [x1,x2],[y1,z] & ==>.-relation TS reduces [x1,x2],[y2,z] ) by Def6; hence y1 = y2 by A1, Th80; ::_thesis: verum end; begin definition let E be non empty set ; let F be Subset of (E ^omega); let TS be non empty transition-system over F; let x1, x2, y be set ; predx1,x2 ==>* y,TS means :Def7: :: REWRITE3:def 7 x1,x2 ==>* y, <%> E,TS; end; :: deftheorem Def7 defines ==>* REWRITE3:def_7_:_ for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F for x1, x2, y being set holds ( x1,x2 ==>* y,TS iff x1,x2 ==>* y, <%> E,TS ); theorem Th94: :: REWRITE3:94 for x, y, z being set for E being non empty set for F1, F2 being Subset of (E ^omega) for TS1 being non empty transition-system over F1 for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x,y ==>* z,TS1 holds x,y ==>* z,TS2 proof let x, y, z be set ; ::_thesis: for E being non empty set for F1, F2 being Subset of (E ^omega) for TS1 being non empty transition-system over F1 for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x,y ==>* z,TS1 holds x,y ==>* z,TS2 let E be non empty set ; ::_thesis: for F1, F2 being Subset of (E ^omega) for TS1 being non empty transition-system over F1 for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x,y ==>* z,TS1 holds x,y ==>* z,TS2 let F1, F2 be Subset of (E ^omega); ::_thesis: for TS1 being non empty transition-system over F1 for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x,y ==>* z,TS1 holds x,y ==>* z,TS2 let TS1 be non empty transition-system over F1; ::_thesis: for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x,y ==>* z,TS1 holds x,y ==>* z,TS2 let TS2 be non empty transition-system over F2; ::_thesis: ( the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 & x,y ==>* z,TS1 implies x,y ==>* z,TS2 ) assume A1: ( the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 ) ; ::_thesis: ( not x,y ==>* z,TS1 or x,y ==>* z,TS2 ) assume x,y ==>* z,TS1 ; ::_thesis: x,y ==>* z,TS2 then x,y ==>* z, <%> E,TS1 by Def7; then x,y ==>* z, <%> E,TS2 by A1, Th81; hence x,y ==>* z,TS2 by Def7; ::_thesis: verum end; theorem Th95: :: REWRITE3:95 for x being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F holds x, <%> E ==>* x,TS proof let x be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F holds x, <%> E ==>* x,TS let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F holds x, <%> E ==>* x,TS let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F holds x, <%> E ==>* x,TS let TS be non empty transition-system over F; ::_thesis: x, <%> E ==>* x,TS x, <%> E ==>* x, <%> E,TS by Th82; hence x, <%> E ==>* x,TS by Def7; ::_thesis: verum end; theorem Th96: :: REWRITE3:96 for x, y being set for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,u ==>* y,TS holds x,u ^ v ==>* y,v,TS proof let x, y be set ; ::_thesis: for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,u ==>* y,TS holds x,u ^ v ==>* y,v,TS let E be non empty set ; ::_thesis: for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,u ==>* y,TS holds x,u ^ v ==>* y,v,TS let u, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,u ==>* y,TS holds x,u ^ v ==>* y,v,TS let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,u ==>* y,TS holds x,u ^ v ==>* y,v,TS let TS be non empty transition-system over F; ::_thesis: ( x,u ==>* y,TS implies x,u ^ v ==>* y,v,TS ) assume x,u ==>* y,TS ; ::_thesis: x,u ^ v ==>* y,v,TS then x,u ==>* y, <%> E,TS by Def7; then x,u ^ v ==>* y,{} ^ v,TS by Th86; hence x,u ^ v ==>* y,v,TS ; ::_thesis: verum end; theorem :: REWRITE3:97 for x, y, z being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,y -->. z,TS holds x,y ==>* z,TS proof let x, y, z be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,y -->. z,TS holds x,y ==>* z,TS let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,y -->. z,TS holds x,y ==>* z,TS let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,y -->. z,TS holds x,y ==>* z,TS let TS be non empty transition-system over F; ::_thesis: ( x,y -->. z,TS implies x,y ==>* z,TS ) assume x,y -->. z,TS ; ::_thesis: x,y ==>* z,TS then x,y ==>* z, <%> E,TS by Th84; hence x,y ==>* z,TS by Def7; ::_thesis: verum end; theorem :: REWRITE3:98 for x1, x2, y being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st x1,x2 ==>. y, <%> E,TS holds x1,x2 ==>* y,TS proof let x1, x2, y be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st x1,x2 ==>. y, <%> E,TS holds x1,x2 ==>* y,TS let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st x1,x2 ==>. y, <%> E,TS holds x1,x2 ==>* y,TS let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x1,x2 ==>. y, <%> E,TS holds x1,x2 ==>* y,TS let TS be non empty transition-system over F; ::_thesis: ( x1,x2 ==>. y, <%> E,TS implies x1,x2 ==>* y,TS ) assume x1,x2 ==>. y, <%> E,TS ; ::_thesis: x1,x2 ==>* y,TS then x1,x2 ==>* y, <%> E,TS by Th87; hence x1,x2 ==>* y,TS by Def7; ::_thesis: verum end; theorem :: REWRITE3:99 for x, y, z being set for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,u ==>* y,TS & y,v ==>* z,TS holds x,u ^ v ==>* z,TS proof let x, y, z be set ; ::_thesis: for E being non empty set for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,u ==>* y,TS & y,v ==>* z,TS holds x,u ^ v ==>* z,TS let E be non empty set ; ::_thesis: for u, v being Element of E ^omega for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,u ==>* y,TS & y,v ==>* z,TS holds x,u ^ v ==>* z,TS let u, v be Element of E ^omega ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st x,u ==>* y,TS & y,v ==>* z,TS holds x,u ^ v ==>* z,TS let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st x,u ==>* y,TS & y,v ==>* z,TS holds x,u ^ v ==>* z,TS let TS be non empty transition-system over F; ::_thesis: ( x,u ==>* y,TS & y,v ==>* z,TS implies x,u ^ v ==>* z,TS ) assume that A1: x,u ==>* y,TS and A2: y,v ==>* z,TS ; ::_thesis: x,u ^ v ==>* z,TS x,(u ^ v) ^ {} ==>* y,v,TS by A1, Th96; then A3: x,(u ^ v) ^ (<%> E) ==>* y,v ^ {},TS ; y,v ==>* z, <%> E,TS by A2, Def7; then x,(u ^ v) ^ {} ==>* z, <%> E,TS by A3, Th83; hence x,u ^ v ==>* z,TS by Def7; ::_thesis: verum end; theorem Th100: :: REWRITE3:100 for x, y being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds ( x, <%> E ==>* y,TS iff x = y ) proof let x, y be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds ( x, <%> E ==>* y,TS iff x = y ) let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds ( x, <%> E ==>* y,TS iff x = y ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) holds ( x, <%> E ==>* y,TS iff x = y ) let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies ( x, <%> E ==>* y,TS iff x = y ) ) assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: ( x, <%> E ==>* y,TS iff x = y ) thus ( x, <%> E ==>* y,TS implies x = y ) ::_thesis: ( x = y implies x, <%> E ==>* y,TS ) proof assume x, <%> E ==>* y,TS ; ::_thesis: x = y then x, <%> E ==>* y, <%> E,TS by Def7; hence x = y by A1, Th91; ::_thesis: verum end; assume x = y ; ::_thesis: x, <%> E ==>* y,TS hence x, <%> E ==>* y,TS by Th95; ::_thesis: verum end; theorem :: REWRITE3:101 for x, y being set for E being non empty set for e being Element of E for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y,TS holds x,<%e%> ==>. y, <%> E,TS proof let x, y be set ; ::_thesis: for E being non empty set for e being Element of E for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y,TS holds x,<%e%> ==>. y, <%> E,TS let E be non empty set ; ::_thesis: for e being Element of E for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y,TS holds x,<%e%> ==>. y, <%> E,TS let e be Element of E; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y,TS holds x,<%e%> ==>. y, <%> E,TS let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y,TS holds x,<%e%> ==>. y, <%> E,TS let TS be non empty transition-system over F; ::_thesis: ( not <%> E in rng (dom the Tran of TS) & x,<%e%> ==>* y,TS implies x,<%e%> ==>. y, <%> E,TS ) assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: ( not x,<%e%> ==>* y,TS or x,<%e%> ==>. y, <%> E,TS ) assume x,<%e%> ==>* y,TS ; ::_thesis: x,<%e%> ==>. y, <%> E,TS then x,<%e%> ==>* y, <%> E,TS by Def7; hence x,<%e%> ==>. y, <%> E,TS by A1, Th92; ::_thesis: verum end; theorem :: REWRITE3:102 for x1, x2, y1, y2 being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic & x1,x2 ==>* y1,TS & x1,x2 ==>* y2,TS holds y1 = y2 proof let x1, x2, y1, y2 be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic & x1,x2 ==>* y1,TS & x1,x2 ==>* y2,TS holds y1 = y2 let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F st TS is deterministic & x1,x2 ==>* y1,TS & x1,x2 ==>* y2,TS holds y1 = y2 let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F st TS is deterministic & x1,x2 ==>* y1,TS & x1,x2 ==>* y2,TS holds y1 = y2 let TS be non empty transition-system over F; ::_thesis: ( TS is deterministic & x1,x2 ==>* y1,TS & x1,x2 ==>* y2,TS implies y1 = y2 ) assume A1: TS is deterministic ; ::_thesis: ( not x1,x2 ==>* y1,TS or not x1,x2 ==>* y2,TS or y1 = y2 ) assume ( x1,x2 ==>* y1,TS & x1,x2 ==>* y2,TS ) ; ::_thesis: y1 = y2 then ( x1,x2 ==>* y1, <%> E,TS & x1,x2 ==>* y2, <%> E,TS ) by Def7; hence y1 = y2 by A1, Th93; ::_thesis: verum end; begin definition let E be non empty set ; let F be Subset of (E ^omega); let TS be non empty transition-system over F; let x, X be set ; funcx -succ_of (X,TS) -> Subset of TS equals :: REWRITE3:def 8 { s where s is Element of TS : ex t being Element of TS st ( t in X & t,x ==>* s,TS ) } ; coherence { s where s is Element of TS : ex t being Element of TS st ( t in X & t,x ==>* s,TS ) } is Subset of TS proof set Y = { s where s is Element of TS : ex t being Element of TS st ( t in X & t,x ==>* s,TS ) } ; { s where s is Element of TS : ex t being Element of TS st ( t in X & t,x ==>* s,TS ) } c= the carrier of TS proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in { s where s is Element of TS : ex t being Element of TS st ( t in X & t,x ==>* s,TS ) } or y in the carrier of TS ) assume y in { s where s is Element of TS : ex t being Element of TS st ( t in X & t,x ==>* s,TS ) } ; ::_thesis: y in the carrier of TS then ex s being Element of TS st ( s = y & ex t being Element of TS st ( t in X & t,x ==>* s,TS ) ) ; hence y in the carrier of TS ; ::_thesis: verum end; hence { s where s is Element of TS : ex t being Element of TS st ( t in X & t,x ==>* s,TS ) } is Subset of TS ; ::_thesis: verum end; end; :: deftheorem defines -succ_of REWRITE3:def_8_:_ for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F for x, X being set holds x -succ_of (X,TS) = { s where s is Element of TS : ex t being Element of TS st ( t in X & t,x ==>* s,TS ) } ; theorem Th103: :: REWRITE3:103 for x, X being set for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F for s being Element of TS holds ( s in x -succ_of (X,TS) iff ex t being Element of TS st ( t in X & t,x ==>* s,TS ) ) proof let x, X be set ; ::_thesis: for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F for s being Element of TS holds ( s in x -succ_of (X,TS) iff ex t being Element of TS st ( t in X & t,x ==>* s,TS ) ) let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F for s being Element of TS holds ( s in x -succ_of (X,TS) iff ex t being Element of TS st ( t in X & t,x ==>* s,TS ) ) let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F for s being Element of TS holds ( s in x -succ_of (X,TS) iff ex t being Element of TS st ( t in X & t,x ==>* s,TS ) ) let TS be non empty transition-system over F; ::_thesis: for s being Element of TS holds ( s in x -succ_of (X,TS) iff ex t being Element of TS st ( t in X & t,x ==>* s,TS ) ) let s be Element of TS; ::_thesis: ( s in x -succ_of (X,TS) iff ex t being Element of TS st ( t in X & t,x ==>* s,TS ) ) thus ( s in x -succ_of (X,TS) implies ex t being Element of TS st ( t in X & t,x ==>* s,TS ) ) ::_thesis: ( ex t being Element of TS st ( t in X & t,x ==>* s,TS ) implies s in x -succ_of (X,TS) ) proof assume s in x -succ_of (X,TS) ; ::_thesis: ex t being Element of TS st ( t in X & t,x ==>* s,TS ) then ex s9 being Element of TS st ( s9 = s & ex t being Element of TS st ( t in X & t,x ==>* s9,TS ) ) ; hence ex t being Element of TS st ( t in X & t,x ==>* s,TS ) ; ::_thesis: verum end; thus ( ex t being Element of TS st ( t in X & t,x ==>* s,TS ) implies s in x -succ_of (X,TS) ) ; ::_thesis: verum end; theorem :: REWRITE3:104 for E being non empty set for F being Subset of (E ^omega) for TS being non empty transition-system over F for S being Subset of TS st not <%> E in rng (dom the Tran of TS) holds (<%> E) -succ_of (S,TS) = S proof let E be non empty set ; ::_thesis: for F being Subset of (E ^omega) for TS being non empty transition-system over F for S being Subset of TS st not <%> E in rng (dom the Tran of TS) holds (<%> E) -succ_of (S,TS) = S let F be Subset of (E ^omega); ::_thesis: for TS being non empty transition-system over F for S being Subset of TS st not <%> E in rng (dom the Tran of TS) holds (<%> E) -succ_of (S,TS) = S let TS be non empty transition-system over F; ::_thesis: for S being Subset of TS st not <%> E in rng (dom the Tran of TS) holds (<%> E) -succ_of (S,TS) = S let S be Subset of TS; ::_thesis: ( not <%> E in rng (dom the Tran of TS) implies (<%> E) -succ_of (S,TS) = S ) assume A1: not <%> E in rng (dom the Tran of TS) ; ::_thesis: (<%> E) -succ_of (S,TS) = S A2: now__::_thesis:_for_x_being_set_st_x_in_(<%>_E)_-succ_of_(S,TS)_holds_ x_in_S let x be set ; ::_thesis: ( x in (<%> E) -succ_of (S,TS) implies x in S ) assume x in (<%> E) -succ_of (S,TS) ; ::_thesis: x in S then ex s being Element of TS st ( s in S & s, <%> E ==>* x,TS ) by Th103; hence x in S by A1, Th100; ::_thesis: verum end; now__::_thesis:_for_x_being_set_st_x_in_S_holds_ x_in_(<%>_E)_-succ_of_(S,TS) let x be set ; ::_thesis: ( x in S implies x in (<%> E) -succ_of (S,TS) ) assume A3: x in S ; ::_thesis: x in (<%> E) -succ_of (S,TS) x, <%> E ==>* x,TS by Th95; hence x in (<%> E) -succ_of (S,TS) by A3; ::_thesis: verum end; hence (<%> E) -succ_of (S,TS) = S by A2, TARSKI:1; ::_thesis: verum end; theorem :: REWRITE3:105 for x, X being set for E being non empty set for F1, F2 being Subset of (E ^omega) for TS1 being non empty transition-system over F1 for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds x -succ_of (X,TS1) = x -succ_of (X,TS2) proof let x, X be set ; ::_thesis: for E being non empty set for F1, F2 being Subset of (E ^omega) for TS1 being non empty transition-system over F1 for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds x -succ_of (X,TS1) = x -succ_of (X,TS2) let E be non empty set ; ::_thesis: for F1, F2 being Subset of (E ^omega) for TS1 being non empty transition-system over F1 for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds x -succ_of (X,TS1) = x -succ_of (X,TS2) let F1, F2 be Subset of (E ^omega); ::_thesis: for TS1 being non empty transition-system over F1 for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds x -succ_of (X,TS1) = x -succ_of (X,TS2) let TS1 be non empty transition-system over F1; ::_thesis: for TS2 being non empty transition-system over F2 st the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 holds x -succ_of (X,TS1) = x -succ_of (X,TS2) let TS2 be non empty transition-system over F2; ::_thesis: ( the carrier of TS1 = the carrier of TS2 & the Tran of TS1 = the Tran of TS2 implies x -succ_of (X,TS1) = x -succ_of (X,TS2) ) assume that A1: the carrier of TS1 = the carrier of TS2 and A2: the Tran of TS1 = the Tran of TS2 ; ::_thesis: x -succ_of (X,TS1) = x -succ_of (X,TS2) A3: now__::_thesis:_for_y_being_set_st_y_in_x_-succ_of_(X,TS2)_holds_ y_in_x_-succ_of_(X,TS1) let y be set ; ::_thesis: ( y in x -succ_of (X,TS2) implies y in x -succ_of (X,TS1) ) assume A4: y in x -succ_of (X,TS2) ; ::_thesis: y in x -succ_of (X,TS1) then reconsider q = y as Element of TS2 ; consider p being Element of TS2 such that A5: p in X and A6: p,x ==>* q,TS2 by A4, Th103; reconsider q = q as Element of TS1 by A1; reconsider p = p as Element of TS1 by A1; p,x ==>* q,TS1 by A1, A2, A6, Th94; hence y in x -succ_of (X,TS1) by A5; ::_thesis: verum end; now__::_thesis:_for_y_being_set_st_y_in_x_-succ_of_(X,TS1)_holds_ y_in_x_-succ_of_(X,TS2) let y be set ; ::_thesis: ( y in x -succ_of (X,TS1) implies y in x -succ_of (X,TS2) ) assume A7: y in x -succ_of (X,TS1) ; ::_thesis: y in x -succ_of (X,TS2) then reconsider q = y as Element of TS1 ; consider p being Element of TS1 such that A8: p in X and A9: p,x ==>* q,TS1 by A7, Th103; reconsider q = q as Element of TS2 by A1; reconsider p = p as Element of TS2 by A1; p,x ==>* q,TS2 by A1, A2, A9, Th94; hence y in x -succ_of (X,TS2) by A8; ::_thesis: verum end; hence x -succ_of (X,TS1) = x -succ_of (X,TS2) by A3, TARSKI:1; ::_thesis: verum end;