:: REWRITE2 semantic presentation begin theorem Th1: :: REWRITE2:1 for k being Nat for p being FinSequence st not k in dom p & k + 1 in dom p holds k = 0 proof let k be Nat; ::_thesis: for p being FinSequence st not k in dom p & k + 1 in dom p holds k = 0 let p be FinSequence; ::_thesis: ( not k in dom p & k + 1 in dom p implies k = 0 ) assume that A1: not k in dom p and A2: k + 1 in dom p ; ::_thesis: k = 0 A3: k + 1 <= len p by A2, FINSEQ_3:25; percases ( k < 1 or k > len p ) by A1, FINSEQ_3:25; suppose k < 1 ; ::_thesis: k = 0 hence k = 0 by NAT_1:14; ::_thesis: verum end; suppose k > len p ; ::_thesis: k = 0 hence k = 0 by A3, NAT_1:13; ::_thesis: verum end; end; end; theorem Th2: :: REWRITE2:2 for k being Nat for p, q being FinSequence st k > len p & k <= len (p ^ q) holds ex l being Nat st ( k = (len p) + l & l >= 1 & l <= len q ) proof let k be Nat; ::_thesis: for p, q being FinSequence st k > len p & k <= len (p ^ q) holds ex l being Nat st ( k = (len p) + l & l >= 1 & l <= len q ) let p, q be FinSequence; ::_thesis: ( k > len p & k <= len (p ^ q) implies ex l being Nat st ( k = (len p) + l & l >= 1 & l <= len q ) ) A1: 0 + 1 = 1 ; assume that A2: k > len p and A3: k <= len (p ^ q) ; ::_thesis: ex l being Nat st ( k = (len p) + l & l >= 1 & l <= len q ) consider l being Nat such that A4: k = (len p) + l by A2, NAT_1:10; take l ; ::_thesis: ( k = (len p) + l & l >= 1 & l <= len q ) thus k = (len p) + l by A4; ::_thesis: ( l >= 1 & l <= len q ) (len p) + l > (len p) + 0 by A2, A4; then l > 0 ; hence l >= 1 by A1, NAT_1:13; ::_thesis: l <= len q (len p) + l <= (len p) + (len q) by A3, A4, FINSEQ_1:22; hence l <= len q by XREAL_1:6; ::_thesis: verum end; theorem Th3: :: REWRITE2:3 for k being Nat for R being Relation for p being RedSequence of R st k >= 1 holds p | k is RedSequence of R proof let k be Nat; ::_thesis: for R being Relation for p being RedSequence of R st k >= 1 holds p | k is RedSequence of R let R be Relation; ::_thesis: for p being RedSequence of R st k >= 1 holds p | k is RedSequence of R let p be RedSequence of R; ::_thesis: ( k >= 1 implies p | k is RedSequence of R ) assume A1: k >= 1 ; ::_thesis: p | k is RedSequence of R percases ( k >= len p or k < len p ) ; suppose k >= len p ; ::_thesis: p | k is RedSequence of R hence p | k is RedSequence of R by FINSEQ_1:58; ::_thesis: verum end; supposeA2: k < len p ; ::_thesis: p | k is RedSequence of R A3: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(p_|_k)_&_i_+_1_in_dom_(p_|_k)_holds_ [((p_|_k)_._i),((p_|_k)_._(i_+_1))]_in_R A4: dom (p | k) c= dom p by RELAT_1:60; let i be Element of NAT ; ::_thesis: ( i in dom (p | k) & i + 1 in dom (p | k) implies [((p | k) . i),((p | k) . (i + 1))] in R ) assume A5: ( i in dom (p | k) & i + 1 in dom (p | k) ) ; ::_thesis: [((p | k) . i),((p | k) . (i + 1))] in R ( (p | k) . i = p . i & (p | k) . (i + 1) = p . (i + 1) ) by A5, FUNCT_1:47; hence [((p | k) . i),((p | k) . (i + 1))] in R by A5, A4, REWRITE1:def_2; ::_thesis: verum end; len (p | k) > 0 by A1, A2, FINSEQ_1:59; hence p | k is RedSequence of R by A3, REWRITE1:def_2; ::_thesis: verum end; end; end; theorem Th4: :: REWRITE2:4 for k being Nat for R being Relation for p being RedSequence of R st k in dom p holds ex q being RedSequence of R st ( len q = k & q . 1 = p . 1 & q . (len q) = p . k ) proof let k be Nat; ::_thesis: for R being Relation for p being RedSequence of R st k in dom p holds ex q being RedSequence of R st ( len q = k & q . 1 = p . 1 & q . (len q) = p . k ) let R be Relation; ::_thesis: for p being RedSequence of R st k in dom p holds ex q being RedSequence of R st ( len q = k & q . 1 = p . 1 & q . (len q) = p . k ) let p be RedSequence of R; ::_thesis: ( k in dom p implies ex q being RedSequence of R st ( len q = k & q . 1 = p . 1 & q . (len q) = p . k ) ) assume A1: k in dom p ; ::_thesis: ex q being RedSequence of R st ( len q = k & q . 1 = p . 1 & q . (len q) = p . k ) set q = p | k; take p | k ; ::_thesis: ( p | k is RedSequence of R & len (p | k) = k & (p | k) . 1 = p . 1 & (p | k) . (len (p | k)) = p . k ) A2: 1 <= k by A1, FINSEQ_3:25; hence p | k is RedSequence of R by Th3; ::_thesis: ( len (p | k) = k & (p | k) . 1 = p . 1 & (p | k) . (len (p | k)) = p . k ) k <= len p by A1, FINSEQ_3:25; hence len (p | k) = k by FINSEQ_1:59; ::_thesis: ( (p | k) . 1 = p . 1 & (p | k) . (len (p | k)) = p . k ) hence ( (p | k) . 1 = p . 1 & (p | k) . (len (p | k)) = p . k ) by A2, FINSEQ_3:112; ::_thesis: verum end; begin definition let f be Function; attrf is XFinSequence-yielding means :Def1: :: REWRITE2:def 1 for x being set st x in dom f holds f . x is XFinSequence; end; :: deftheorem Def1 defines XFinSequence-yielding REWRITE2:def_1_:_ for f being Function holds ( f is XFinSequence-yielding iff for x being set st x in dom f holds f . x is XFinSequence ); registration cluster empty Relation-like Function-like -> XFinSequence-yielding for set ; coherence for b1 being Function st b1 is empty holds b1 is XFinSequence-yielding proof let X be Function; ::_thesis: ( X is empty implies X is XFinSequence-yielding ) assume A1: X is empty ; ::_thesis: X is XFinSequence-yielding let x be set ; :: according to REWRITE2:def_1 ::_thesis: ( x in dom X implies X . x is XFinSequence ) thus ( x in dom X implies X . x is XFinSequence ) by A1; ::_thesis: verum end; end; registration let f be XFinSequence; cluster<*f*> -> XFinSequence-yielding ; coherence <*f*> is XFinSequence-yielding proof let x be set ; :: according to REWRITE2:def_1 ::_thesis: ( x in dom <*f*> implies <*f*> . x is XFinSequence ) assume x in dom <*f*> ; ::_thesis: <*f*> . x is XFinSequence then x in {1} by FINSEQ_1:2, FINSEQ_1:38; then x = 1 by TARSKI:def_1; hence <*f*> . x is XFinSequence by FINSEQ_1:40; ::_thesis: verum end; end; registration let p be XFinSequence-yielding Function; let x be set ; clusterp . x -> Relation-like Function-like finite ; coherence ( p . x is finite & p . x is Function-like & p . x is Relation-like ) proof percases ( x in dom p or not x in dom p ) ; suppose x in dom p ; ::_thesis: ( p . x is finite & p . x is Function-like & p . x is Relation-like ) hence ( p . x is finite & p . x is Function-like & p . x is Relation-like ) by Def1; ::_thesis: verum end; suppose not x in dom p ; ::_thesis: ( p . x is finite & p . x is Function-like & p . x is Relation-like ) hence ( p . x is finite & p . x is Function-like & p . x is Relation-like ) by FUNCT_1:def_2; ::_thesis: verum end; end; end; end; registration let p be XFinSequence-yielding Function; let x be set ; clusterp . x -> T-Sequence-like ; coherence p . x is T-Sequence-like proof percases ( x in dom p or not x in dom p ) ; suppose x in dom p ; ::_thesis: p . x is T-Sequence-like hence p . x is T-Sequence-like by Def1; ::_thesis: verum end; suppose not x in dom p ; ::_thesis: p . x is T-Sequence-like hence p . x is T-Sequence-like by FUNCT_1:def_2; ::_thesis: verum end; end; end; end; registration cluster Relation-like NAT -defined Function-like finite FinSequence-like FinSubsequence-like XFinSequence-yielding for set ; existence ex b1 being FinSequence st b1 is XFinSequence-yielding proof take {} ; ::_thesis: {} is XFinSequence-yielding thus {} is XFinSequence-yielding ; ::_thesis: verum end; end; registration let E be set ; cluster -> XFinSequence-yielding for FinSequence of E ^omega ; coherence for b1 being FinSequence of E ^omega holds b1 is XFinSequence-yielding proof let f be FinSequence of E ^omega ; ::_thesis: f is XFinSequence-yielding let x be set ; :: according to REWRITE2:def_1 ::_thesis: ( x in dom f implies f . x is XFinSequence ) assume A1: x in dom f ; ::_thesis: f . x is XFinSequence then reconsider x = x as Element of NAT ; f . x in E ^omega by A1, FINSEQ_2:11; hence f . x is XFinSequence ; ::_thesis: verum end; end; registration let p, q be XFinSequence-yielding FinSequence; clusterp ^ q -> XFinSequence-yielding ; coherence p ^ q is XFinSequence-yielding proof now__::_thesis:_for_x_being_set_st_x_in_dom_(p_^_q)_holds_ (p_^_q)_._x_is_XFinSequence let x be set ; ::_thesis: ( x in dom (p ^ q) implies (p ^ q) . b1 is XFinSequence ) assume A1: x in dom (p ^ q) ; ::_thesis: (p ^ q) . b1 is XFinSequence then reconsider x1 = x as Element of NAT ; percases ( x1 in dom p or ex l being Nat st ( l in dom q & x1 = (len p) + l ) ) by A1, FINSEQ_1:25; suppose x1 in dom p ; ::_thesis: (p ^ q) . b1 is XFinSequence then p . x1 = (p ^ q) . x1 by FINSEQ_1:def_7; hence (p ^ q) . x is XFinSequence ; ::_thesis: verum end; suppose ex l being Nat st ( l in dom q & x1 = (len p) + l ) ; ::_thesis: (p ^ q) . b1 is XFinSequence then consider l being Element of NAT such that A2: l in dom q and A3: x = (len p) + l ; (p ^ q) . ((len p) + l) = q . l by A2, FINSEQ_1:def_7; hence (p ^ q) . x is XFinSequence by A3; ::_thesis: verum end; end; end; hence p ^ q is XFinSequence-yielding by Def1; ::_thesis: verum end; end; begin definition let s be XFinSequence; let p be XFinSequence-yielding Function; funcs ^+ p -> XFinSequence-yielding Function means :Def2: :: REWRITE2:def 2 ( dom it = dom p & ( for x being set st x in dom p holds it . x = s ^ (p . x) ) ); existence ex b1 being XFinSequence-yielding Function st ( dom b1 = dom p & ( for x being set st x in dom p holds b1 . x = s ^ (p . x) ) ) proof defpred S1[ set , set ] means for x being set st x = \$1 holds \$2 = s ^ (p . x); A1: for x being set st x in dom p holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in dom p implies ex y being set st S1[x,y] ) assume x in dom p ; ::_thesis: ex y being set st S1[x,y] take s ^ (p . x) ; ::_thesis: S1[x,s ^ (p . x)] thus S1[x,s ^ (p . x)] ; ::_thesis: verum end; consider f being Function such that A2: ( dom f = dom p & ( for x being set st x in dom p holds S1[x,f . x] ) ) from CLASSES1:sch_1(A1); now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_is_XFinSequence let x be set ; ::_thesis: ( x in dom f implies f . x is XFinSequence ) assume x in dom f ; ::_thesis: f . x is XFinSequence then f . x = s ^ (p . x) by A2; hence f . x is XFinSequence ; ::_thesis: verum end; then reconsider g = f as XFinSequence-yielding Function by Def1; take g ; ::_thesis: ( dom g = dom p & ( for x being set st x in dom p holds g . x = s ^ (p . x) ) ) thus ( dom g = dom p & ( for x being set st x in dom p holds g . x = s ^ (p . x) ) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being XFinSequence-yielding Function st dom b1 = dom p & ( for x being set st x in dom p holds b1 . x = s ^ (p . x) ) & dom b2 = dom p & ( for x being set st x in dom p holds b2 . x = s ^ (p . x) ) holds b1 = b2 proof let f, g be XFinSequence-yielding Function; ::_thesis: ( dom f = dom p & ( for x being set st x in dom p holds f . x = s ^ (p . x) ) & dom g = dom p & ( for x being set st x in dom p holds g . x = s ^ (p . x) ) implies f = g ) assume that A3: dom f = dom p and A4: for x being set st x in dom p holds f . x = s ^ (p . x) and A5: dom g = dom p and A6: for x being set st x in dom p holds g . x = s ^ (p . x) ; ::_thesis: f = g now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_=_g_._x let x be set ; ::_thesis: ( x in dom f implies f . x = g . x ) assume A7: x in dom f ; ::_thesis: f . x = g . x then f . x = s ^ (p . x) by A3, A4; hence f . x = g . x by A3, A6, A7; ::_thesis: verum end; hence f = g by A3, A5, FUNCT_1:2; ::_thesis: verum end; funcp +^ s -> XFinSequence-yielding Function means :Def3: :: REWRITE2:def 3 ( dom it = dom p & ( for x being set st x in dom p holds it . x = (p . x) ^ s ) ); existence ex b1 being XFinSequence-yielding Function st ( dom b1 = dom p & ( for x being set st x in dom p holds b1 . x = (p . x) ^ s ) ) proof defpred S1[ set , set ] means for x being set st x = \$1 holds \$2 = (p . x) ^ s; A8: for x being set st x in dom p holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in dom p implies ex y being set st S1[x,y] ) assume x in dom p ; ::_thesis: ex y being set st S1[x,y] take (p . x) ^ s ; ::_thesis: S1[x,(p . x) ^ s] thus S1[x,(p . x) ^ s] ; ::_thesis: verum end; consider f being Function such that A9: ( dom f = dom p & ( for x being set st x in dom p holds S1[x,f . x] ) ) from CLASSES1:sch_1(A8); now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_is_XFinSequence let x be set ; ::_thesis: ( x in dom f implies f . x is XFinSequence ) assume x in dom f ; ::_thesis: f . x is XFinSequence then f . x = (p . x) ^ s by A9; hence f . x is XFinSequence ; ::_thesis: verum end; then reconsider g = f as XFinSequence-yielding Function by Def1; take g ; ::_thesis: ( dom g = dom p & ( for x being set st x in dom p holds g . x = (p . x) ^ s ) ) thus ( dom g = dom p & ( for x being set st x in dom p holds g . x = (p . x) ^ s ) ) by A9; ::_thesis: verum end; uniqueness for b1, b2 being XFinSequence-yielding Function st dom b1 = dom p & ( for x being set st x in dom p holds b1 . x = (p . x) ^ s ) & dom b2 = dom p & ( for x being set st x in dom p holds b2 . x = (p . x) ^ s ) holds b1 = b2 proof let f, g be XFinSequence-yielding Function; ::_thesis: ( dom f = dom p & ( for x being set st x in dom p holds f . x = (p . x) ^ s ) & dom g = dom p & ( for x being set st x in dom p holds g . x = (p . x) ^ s ) implies f = g ) assume that A10: dom f = dom p and A11: for x being set st x in dom p holds f . x = (p . x) ^ s and A12: dom g = dom p and A13: for x being set st x in dom p holds g . x = (p . x) ^ s ; ::_thesis: f = g now__::_thesis:_for_x_being_set_st_x_in_dom_f_holds_ f_._x_=_g_._x let x be set ; ::_thesis: ( x in dom f implies f . x = g . x ) assume A14: x in dom f ; ::_thesis: f . x = g . x then f . x = (p . x) ^ s by A10, A11; hence f . x = g . x by A10, A13, A14; ::_thesis: verum end; hence f = g by A10, A12, FUNCT_1:2; ::_thesis: verum end; end; :: deftheorem Def2 defines ^+ REWRITE2:def_2_:_ for s being XFinSequence for p, b3 being XFinSequence-yielding Function holds ( b3 = s ^+ p iff ( dom b3 = dom p & ( for x being set st x in dom p holds b3 . x = s ^ (p . x) ) ) ); :: deftheorem Def3 defines +^ REWRITE2:def_3_:_ for s being XFinSequence for p, b3 being XFinSequence-yielding Function holds ( b3 = p +^ s iff ( dom b3 = dom p & ( for x being set st x in dom p holds b3 . x = (p . x) ^ s ) ) ); registration let s be XFinSequence; let p be XFinSequence-yielding FinSequence; clusters ^+ p -> FinSequence-like XFinSequence-yielding ; coherence s ^+ p is FinSequence-like proof consider n being Nat such that A1: dom p = Seg n by FINSEQ_1:def_2; dom (s ^+ p) = Seg n by A1, Def2; hence s ^+ p is FinSequence-like by FINSEQ_1:def_2; ::_thesis: verum end; clusterp +^ s -> FinSequence-like XFinSequence-yielding ; coherence p +^ s is FinSequence-like proof consider n being Nat such that A2: dom p = Seg n by FINSEQ_1:def_2; dom (p +^ s) = Seg n by A2, Def3; hence p +^ s is FinSequence-like by FINSEQ_1:def_2; ::_thesis: verum end; end; theorem Th5: :: REWRITE2:5 for s being XFinSequence for p being XFinSequence-yielding FinSequence holds ( len (s ^+ p) = len p & len (p +^ s) = len p ) proof let s be XFinSequence; ::_thesis: for p being XFinSequence-yielding FinSequence holds ( len (s ^+ p) = len p & len (p +^ s) = len p ) let p be XFinSequence-yielding FinSequence; ::_thesis: ( len (s ^+ p) = len p & len (p +^ s) = len p ) ( dom (s ^+ p) = dom p & dom (p +^ s) = dom p ) by Def2, Def3; hence ( len (s ^+ p) = len p & len (p +^ s) = len p ) by FINSEQ_3:29; ::_thesis: verum end; theorem :: REWRITE2:6 for E being set for p being XFinSequence-yielding FinSequence holds ( (<%> E) ^+ p = p & p +^ (<%> E) = p ) proof let E be set ; ::_thesis: for p being XFinSequence-yielding FinSequence holds ( (<%> E) ^+ p = p & p +^ (<%> E) = p ) let p be XFinSequence-yielding FinSequence; ::_thesis: ( (<%> E) ^+ p = p & p +^ (<%> E) = p ) A1: now__::_thesis:_for_k_being_Nat_st_k_in_dom_p_holds_ ((<%>_E)_^+_p)_._k_=_p_._k let k be Nat; ::_thesis: ( k in dom p implies ((<%> E) ^+ p) . k = p . k ) assume k in dom p ; ::_thesis: ((<%> E) ^+ p) . k = p . k hence ((<%> E) ^+ p) . k = {} ^ (p . k) by Def2 .= p . k ; ::_thesis: verum end; dom ((<%> E) ^+ p) = dom p by Def2; hence (<%> E) ^+ p = p by A1, FINSEQ_1:13; ::_thesis: p +^ (<%> E) = p A2: now__::_thesis:_for_k_being_Nat_st_k_in_dom_p_holds_ (p_+^_(<%>_E))_._k_=_p_._k let k be Nat; ::_thesis: ( k in dom p implies (p +^ (<%> E)) . k = p . k ) assume k in dom p ; ::_thesis: (p +^ (<%> E)) . k = p . k hence (p +^ (<%> E)) . k = (p . k) ^ {} by Def3 .= p . k ; ::_thesis: verum end; dom (p +^ (<%> E)) = dom p by Def3; hence p +^ (<%> E) = p by A2, FINSEQ_1:13; ::_thesis: verum end; theorem :: REWRITE2:7 for s, t being XFinSequence for p being XFinSequence-yielding FinSequence holds ( s ^+ (t ^+ p) = (s ^ t) ^+ p & (p +^ t) +^ s = p +^ (t ^ s) ) proof let s, t be XFinSequence; ::_thesis: for p being XFinSequence-yielding FinSequence holds ( s ^+ (t ^+ p) = (s ^ t) ^+ p & (p +^ t) +^ s = p +^ (t ^ s) ) let p be XFinSequence-yielding FinSequence; ::_thesis: ( s ^+ (t ^+ p) = (s ^ t) ^+ p & (p +^ t) +^ s = p +^ (t ^ s) ) A1: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(s_^+_(t_^+_p))_holds_ (s_^+_(t_^+_p))_._k_=_((s_^_t)_^+_p)_._k let k be Nat; ::_thesis: ( k in dom (s ^+ (t ^+ p)) implies (s ^+ (t ^+ p)) . k = ((s ^ t) ^+ p) . k ) assume k in dom (s ^+ (t ^+ p)) ; ::_thesis: (s ^+ (t ^+ p)) . k = ((s ^ t) ^+ p) . k then A2: k in dom (t ^+ p) by Def2; then A3: k in dom p by Def2; thus (s ^+ (t ^+ p)) . k = s ^ ((t ^+ p) . k) by A2, Def2 .= s ^ (t ^ (p . k)) by A3, Def2 .= (s ^ t) ^ (p . k) by AFINSQ_1:27 .= ((s ^ t) ^+ p) . k by A3, Def2 ; ::_thesis: verum end; dom (s ^+ (t ^+ p)) = dom (t ^+ p) by Def2 .= dom p by Def2 .= dom ((s ^ t) ^+ p) by Def2 ; hence s ^+ (t ^+ p) = (s ^ t) ^+ p by A1, FINSEQ_1:13; ::_thesis: (p +^ t) +^ s = p +^ (t ^ s) A4: now__::_thesis:_for_k_being_Nat_st_k_in_dom_((p_+^_t)_+^_s)_holds_ ((p_+^_t)_+^_s)_._k_=_(p_+^_(t_^_s))_._k let k be Nat; ::_thesis: ( k in dom ((p +^ t) +^ s) implies ((p +^ t) +^ s) . k = (p +^ (t ^ s)) . k ) assume k in dom ((p +^ t) +^ s) ; ::_thesis: ((p +^ t) +^ s) . k = (p +^ (t ^ s)) . k then A5: k in dom (p +^ t) by Def3; then A6: k in dom p by Def3; thus ((p +^ t) +^ s) . k = ((p +^ t) . k) ^ s by A5, Def3 .= ((p . k) ^ t) ^ s by A6, Def3 .= (p . k) ^ (t ^ s) by AFINSQ_1:27 .= (p +^ (t ^ s)) . k by A6, Def3 ; ::_thesis: verum end; dom ((p +^ t) +^ s) = dom (p +^ t) by Def3 .= dom p by Def3 .= dom (p +^ (t ^ s)) by Def3 ; hence (p +^ t) +^ s = p +^ (t ^ s) by A4, FINSEQ_1:13; ::_thesis: verum end; theorem :: REWRITE2:8 for s, t being XFinSequence for p being XFinSequence-yielding FinSequence holds s ^+ (p +^ t) = (s ^+ p) +^ t proof let s, t be XFinSequence; ::_thesis: for p being XFinSequence-yielding FinSequence holds s ^+ (p +^ t) = (s ^+ p) +^ t let p be XFinSequence-yielding FinSequence; ::_thesis: s ^+ (p +^ t) = (s ^+ p) +^ t A1: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(s_^+_(p_+^_t))_holds_ (s_^+_(p_+^_t))_._k_=_((s_^+_p)_+^_t)_._k let k be Nat; ::_thesis: ( k in dom (s ^+ (p +^ t)) implies (s ^+ (p +^ t)) . k = ((s ^+ p) +^ t) . k ) assume k in dom (s ^+ (p +^ t)) ; ::_thesis: (s ^+ (p +^ t)) . k = ((s ^+ p) +^ t) . k then A2: k in dom (p +^ t) by Def2; then A3: k in dom p by Def3; then A4: k in dom (s ^+ p) by Def2; thus (s ^+ (p +^ t)) . k = s ^ ((p +^ t) . k) by A2, Def2 .= s ^ ((p . k) ^ t) by A3, Def3 .= (s ^ (p . k)) ^ t by AFINSQ_1:27 .= ((s ^+ p) . k) ^ t by A3, Def2 .= ((s ^+ p) +^ t) . k by A4, Def3 ; ::_thesis: verum end; dom (s ^+ (p +^ t)) = dom (p +^ t) by Def2 .= dom p by Def3 .= dom (s ^+ p) by Def2 .= dom ((s ^+ p) +^ t) by Def3 ; hence s ^+ (p +^ t) = (s ^+ p) +^ t by A1, FINSEQ_1:13; ::_thesis: verum end; theorem :: REWRITE2:9 for s being XFinSequence for p, q being XFinSequence-yielding FinSequence holds ( s ^+ (p ^ q) = (s ^+ p) ^ (s ^+ q) & (p ^ q) +^ s = (p +^ s) ^ (q +^ s) ) proof let s be XFinSequence; ::_thesis: for p, q being XFinSequence-yielding FinSequence holds ( s ^+ (p ^ q) = (s ^+ p) ^ (s ^+ q) & (p ^ q) +^ s = (p +^ s) ^ (q +^ s) ) let p, q be XFinSequence-yielding FinSequence; ::_thesis: ( s ^+ (p ^ q) = (s ^+ p) ^ (s ^+ q) & (p ^ q) +^ s = (p +^ s) ^ (q +^ s) ) A1: now__::_thesis:_for_k_being_Nat_st_k_in_dom_(s_^+_(p_^_q))_holds_ (s_^+_(p_^_q))_._k_=_((s_^+_p)_^_(s_^+_q))_._k let k be Nat; ::_thesis: ( k in dom (s ^+ (p ^ q)) implies (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k ) assume A2: k in dom (s ^+ (p ^ q)) ; ::_thesis: (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k then A3: k in dom (p ^ q) by Def2; now__::_thesis:_(s_^+_(p_^_q))_._k_=_((s_^+_p)_^_(s_^+_q))_._k percases ( k in dom p or not k in dom p ) ; supposeA4: k in dom p ; ::_thesis: (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k then A5: k in dom (s ^+ p) by Def2; thus (s ^+ (p ^ q)) . k = s ^ ((p ^ q) . k) by A3, Def2 .= s ^ (p . k) by A4, FINSEQ_1:def_7 .= (s ^+ p) . k by A4, Def2 .= ((s ^+ p) ^ (s ^+ q)) . k by A5, FINSEQ_1:def_7 ; ::_thesis: verum end; supposeA6: not k in dom p ; ::_thesis: (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k A7: k <= len (p ^ q) by A3, FINSEQ_3:25; ( k < 1 or k > len p ) by A6, FINSEQ_3:25; then consider i being Nat such that A8: k = (len p) + i and A9: ( i >= 1 & i <= len q ) by A2, A7, Th2, FINSEQ_3:25; A10: i in dom q by A9, FINSEQ_3:25; then A11: i in dom (s ^+ q) by Def2; A12: len (s ^+ p) = len p by Th5; thus (s ^+ (p ^ q)) . k = s ^ ((p ^ q) . ((len p) + i)) by A3, A8, Def2 .= s ^ (q . i) by A10, FINSEQ_1:def_7 .= (s ^+ q) . i by A10, Def2 .= ((s ^+ p) ^ (s ^+ q)) . k by A8, A11, A12, FINSEQ_1:def_7 ; ::_thesis: verum end; end; end; hence (s ^+ (p ^ q)) . k = ((s ^+ p) ^ (s ^+ q)) . k ; ::_thesis: verum end; len (s ^+ (p ^ q)) = len (p ^ q) by Th5 .= (len p) + (len q) by FINSEQ_1:22 .= (len (s ^+ p)) + (len q) by Th5 .= (len (s ^+ p)) + (len (s ^+ q)) by Th5 .= len ((s ^+ p) ^ (s ^+ q)) by FINSEQ_1:22 ; then dom (s ^+ (p ^ q)) = dom ((s ^+ p) ^ (s ^+ q)) by FINSEQ_3:29; hence s ^+ (p ^ q) = (s ^+ p) ^ (s ^+ q) by A1, FINSEQ_1:13; ::_thesis: (p ^ q) +^ s = (p +^ s) ^ (q +^ s) A13: now__::_thesis:_for_k_being_Nat_st_k_in_dom_((p_^_q)_+^_s)_holds_ ((p_^_q)_+^_s)_._k_=_((p_+^_s)_^_(q_+^_s))_._k let k be Nat; ::_thesis: ( k in dom ((p ^ q) +^ s) implies ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k ) assume A14: k in dom ((p ^ q) +^ s) ; ::_thesis: ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k then A15: k in dom (p ^ q) by Def3; now__::_thesis:_((p_^_q)_+^_s)_._k_=_((p_+^_s)_^_(q_+^_s))_._k percases ( k in dom p or not k in dom p ) ; supposeA16: k in dom p ; ::_thesis: ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k then A17: k in dom (p +^ s) by Def3; thus ((p ^ q) +^ s) . k = ((p ^ q) . k) ^ s by A15, Def3 .= (p . k) ^ s by A16, FINSEQ_1:def_7 .= (p +^ s) . k by A16, Def3 .= ((p +^ s) ^ (q +^ s)) . k by A17, FINSEQ_1:def_7 ; ::_thesis: verum end; supposeA18: not k in dom p ; ::_thesis: ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k A19: k <= len (p ^ q) by A15, FINSEQ_3:25; ( k < 1 or k > len p ) by A18, FINSEQ_3:25; then consider i being Nat such that A20: k = (len p) + i and A21: ( i >= 1 & i <= len q ) by A14, A19, Th2, FINSEQ_3:25; A22: i in dom q by A21, FINSEQ_3:25; then A23: i in dom (q +^ s) by Def3; A24: len (p +^ s) = len p by Th5; thus ((p ^ q) +^ s) . k = ((p ^ q) . ((len p) + i)) ^ s by A15, A20, Def3 .= (q . i) ^ s by A22, FINSEQ_1:def_7 .= (q +^ s) . i by A22, Def3 .= ((p +^ s) ^ (q +^ s)) . k by A20, A23, A24, FINSEQ_1:def_7 ; ::_thesis: verum end; end; end; hence ((p ^ q) +^ s) . k = ((p +^ s) ^ (q +^ s)) . k ; ::_thesis: verum end; len ((p ^ q) +^ s) = len (p ^ q) by Th5 .= (len p) + (len q) by FINSEQ_1:22 .= (len (p +^ s)) + (len q) by Th5 .= (len (p +^ s)) + (len (q +^ s)) by Th5 .= len ((p +^ s) ^ (q +^ s)) by FINSEQ_1:22 ; then dom ((p ^ q) +^ s) = dom ((p +^ s) ^ (q +^ s)) by FINSEQ_3:29; hence (p ^ q) +^ s = (p +^ s) ^ (q +^ s) by A13, FINSEQ_1:13; ::_thesis: verum end; begin definition let E be set ; let p be FinSequence of E ^omega ; let k be Nat; :: original: . redefine funcp . k -> Element of E ^omega ; coherence p . k is Element of E ^omega proof percases ( k in dom p or not k in dom p ) ; suppose k in dom p ; ::_thesis: p . k is Element of E ^omega hence p . k is Element of E ^omega by FINSEQ_2:11; ::_thesis: verum end; suppose not k in dom p ; ::_thesis: p . k is Element of E ^omega then p . k = {} by FUNCT_1:def_2; then p . k is XFinSequence of by AFINSQ_1:16; hence p . k is Element of E ^omega by AFINSQ_1:def_7; ::_thesis: verum end; end; end; end; definition let E be set ; let s be Element of E ^omega ; let p be FinSequence of E ^omega ; :: original: ^+ redefine funcs ^+ p -> FinSequence of E ^omega ; coherence s ^+ p is FinSequence of E ^omega proof now__::_thesis:_for_i_being_Nat_st_i_in_dom_(s_^+_p)_holds_ (s_^+_p)_._i_in_E_^omega let i be Nat; ::_thesis: ( i in dom (s ^+ p) implies (s ^+ p) . i in E ^omega ) assume i in dom (s ^+ p) ; ::_thesis: (s ^+ p) . i in E ^omega then i in dom p by Def2; then (s ^+ p) . i = s ^ (p . i) by Def2; hence (s ^+ p) . i in E ^omega ; ::_thesis: verum end; hence s ^+ p is FinSequence of E ^omega by FINSEQ_2:12; ::_thesis: verum end; :: original: +^ redefine funcp +^ s -> FinSequence of E ^omega ; coherence p +^ s is FinSequence of E ^omega proof now__::_thesis:_for_i_being_Nat_st_i_in_dom_(p_+^_s)_holds_ (p_+^_s)_._i_in_E_^omega let i be Nat; ::_thesis: ( i in dom (p +^ s) implies (p +^ s) . i in E ^omega ) assume i in dom (p +^ s) ; ::_thesis: (p +^ s) . i in E ^omega then i in dom p by Def3; then (p +^ s) . i = (p . i) ^ s by Def3; hence (p +^ s) . i in E ^omega ; ::_thesis: verum end; hence p +^ s is FinSequence of E ^omega by FINSEQ_2:12; ::_thesis: verum end; end; definition let E be set ; mode semi-Thue-system of E is Relation of (E ^omega); end; registration let S be Relation; clusterS \/ (S ~) -> symmetric ; coherence S \/ (S ~) is symmetric proof S \/ (S ~) = (((S ~) ~) \/ (S ~)) ~ by RELAT_1:23 .= (S \/ (S ~)) ~ ; hence S \/ (S ~) is symmetric by RELAT_2:13; ::_thesis: verum end; end; registration let E be set ; cluster Relation-like symmetric for Element of K6(([#] ((E ^omega),(E ^omega)))); existence ex b1 being semi-Thue-system of E st b1 is symmetric proof set S = the semi-Thue-system of E; take the semi-Thue-system of E \/ ( the semi-Thue-system of E ~) ; ::_thesis: the semi-Thue-system of E \/ ( the semi-Thue-system of E ~) is symmetric thus the semi-Thue-system of E \/ ( the semi-Thue-system of E ~) is symmetric ; ::_thesis: verum end; end; definition let E be set ; mode Thue-system of E is symmetric semi-Thue-system of E; end; begin definition let E be set ; let S be semi-Thue-system of E; let s, t be Element of E ^omega ; preds -->. t,S means :Def4: :: REWRITE2:def 4 [s,t] in S; end; :: deftheorem Def4 defines -->. REWRITE2:def_4_:_ for E being set for S being semi-Thue-system of E for s, t being Element of E ^omega holds ( s -->. t,S iff [s,t] in S ); definition let E be set ; let S be semi-Thue-system of E; let s, t be Element of E ^omega ; preds ==>. t,S means :Def5: :: REWRITE2:def 5 ex v, w, s1, t1 being Element of E ^omega st ( s = (v ^ s1) ^ w & t = (v ^ t1) ^ w & s1 -->. t1,S ); end; :: deftheorem Def5 defines ==>. REWRITE2:def_5_:_ for E being set for S being semi-Thue-system of E for s, t being Element of E ^omega holds ( s ==>. t,S iff ex v, w, s1, t1 being Element of E ^omega st ( s = (v ^ s1) ^ w & t = (v ^ t1) ^ w & s1 -->. t1,S ) ); theorem Th10: :: REWRITE2:10 for E being set for S being semi-Thue-system of E for s, t being Element of E ^omega st s -->. t,S holds s ==>. t,S proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t being Element of E ^omega st s -->. t,S holds s ==>. t,S let S be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st s -->. t,S holds s ==>. t,S let s, t be Element of E ^omega ; ::_thesis: ( s -->. t,S implies s ==>. t,S ) assume A1: s -->. t,S ; ::_thesis: s ==>. t,S take e = <%> E; :: according to REWRITE2:def_5 ::_thesis: ex w, s1, t1 being Element of E ^omega st ( s = (e ^ s1) ^ w & t = (e ^ t1) ^ w & s1 -->. t1,S ) A2: t = ({} ^ t) ^ {} .= (e ^ t) ^ e ; s = ({} ^ s) ^ {} .= (e ^ s) ^ e ; hence ex w, s1, t1 being Element of E ^omega st ( s = (e ^ s1) ^ w & t = (e ^ t1) ^ w & s1 -->. t1,S ) by A1, A2; ::_thesis: verum end; theorem :: REWRITE2:11 for E being set for S being semi-Thue-system of E for s being Element of E ^omega st s ==>. s,S holds ex v, w, s1 being Element of E ^omega st ( s = (v ^ s1) ^ w & s1 -->. s1,S ) proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s being Element of E ^omega st s ==>. s,S holds ex v, w, s1 being Element of E ^omega st ( s = (v ^ s1) ^ w & s1 -->. s1,S ) let S be semi-Thue-system of E; ::_thesis: for s being Element of E ^omega st s ==>. s,S holds ex v, w, s1 being Element of E ^omega st ( s = (v ^ s1) ^ w & s1 -->. s1,S ) let s be Element of E ^omega ; ::_thesis: ( s ==>. s,S implies ex v, w, s1 being Element of E ^omega st ( s = (v ^ s1) ^ w & s1 -->. s1,S ) ) given v, w, s1, t1 being Element of E ^omega such that A1: s = (v ^ s1) ^ w and A2: s = (v ^ t1) ^ w and A3: s1 -->. t1,S ; :: according to REWRITE2:def_5 ::_thesis: ex v, w, s1 being Element of E ^omega st ( s = (v ^ s1) ^ w & s1 -->. s1,S ) v ^ s1 = v ^ t1 by A1, A2, AFINSQ_1:28; then s1 = t1 by AFINSQ_1:28; hence ex v, w, s1 being Element of E ^omega st ( s = (v ^ s1) ^ w & s1 -->. s1,S ) by A1, A3; ::_thesis: verum end; theorem Th12: :: REWRITE2:12 for E being set for S being semi-Thue-system of E for s, t, u being Element of E ^omega st s ==>. t,S holds ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t, u being Element of E ^omega st s ==>. t,S holds ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) let S be semi-Thue-system of E; ::_thesis: for s, t, u being Element of E ^omega st s ==>. t,S holds ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) let s, t, u be Element of E ^omega ; ::_thesis: ( s ==>. t,S implies ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) ) given v, w, s1, t1 being Element of E ^omega such that A1: s = (v ^ s1) ^ w and A2: t = (v ^ t1) ^ w and A3: s1 -->. t1,S ; :: according to REWRITE2:def_5 ::_thesis: ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) A4: u ^ t = (u ^ (v ^ t1)) ^ w by A2, AFINSQ_1:27 .= ((u ^ v) ^ t1) ^ w by AFINSQ_1:27 ; u ^ s = (u ^ (v ^ s1)) ^ w by A1, AFINSQ_1:27 .= ((u ^ v) ^ s1) ^ w by AFINSQ_1:27 ; hence u ^ s ==>. u ^ t,S by A3, A4, Def5; ::_thesis: s ^ u ==>. t ^ u,S ( s ^ u = (v ^ s1) ^ (w ^ u) & t ^ u = (v ^ t1) ^ (w ^ u) ) by A1, A2, AFINSQ_1:27; hence s ^ u ==>. t ^ u,S by A3, Def5; ::_thesis: verum end; theorem Th13: :: REWRITE2:13 for E being set for S being semi-Thue-system of E for s, t, u, v being Element of E ^omega st s ==>. t,S holds (u ^ s) ^ v ==>. (u ^ t) ^ v,S proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t, u, v being Element of E ^omega st s ==>. t,S holds (u ^ s) ^ v ==>. (u ^ t) ^ v,S let S be semi-Thue-system of E; ::_thesis: for s, t, u, v being Element of E ^omega st s ==>. t,S holds (u ^ s) ^ v ==>. (u ^ t) ^ v,S let s, t, u, v be Element of E ^omega ; ::_thesis: ( s ==>. t,S implies (u ^ s) ^ v ==>. (u ^ t) ^ v,S ) assume s ==>. t,S ; ::_thesis: (u ^ s) ^ v ==>. (u ^ t) ^ v,S then u ^ s ==>. u ^ t,S by Th12; hence (u ^ s) ^ v ==>. (u ^ t) ^ v,S by Th12; ::_thesis: verum end; theorem Th14: :: REWRITE2:14 for E being set for S being semi-Thue-system of E for s, t, u being Element of E ^omega st s -->. t,S holds ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t, u being Element of E ^omega st s -->. t,S holds ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) let S be semi-Thue-system of E; ::_thesis: for s, t, u being Element of E ^omega st s -->. t,S holds ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) let s, t, u be Element of E ^omega ; ::_thesis: ( s -->. t,S implies ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) ) assume s -->. t,S ; ::_thesis: ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) then s ==>. t,S by Th10; hence ( u ^ s ==>. u ^ t,S & s ^ u ==>. t ^ u,S ) by Th12; ::_thesis: verum end; theorem Th15: :: REWRITE2:15 for E being set for S being semi-Thue-system of E for s, t, u, v being Element of E ^omega st s -->. t,S holds (u ^ s) ^ v ==>. (u ^ t) ^ v,S proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t, u, v being Element of E ^omega st s -->. t,S holds (u ^ s) ^ v ==>. (u ^ t) ^ v,S let S be semi-Thue-system of E; ::_thesis: for s, t, u, v being Element of E ^omega st s -->. t,S holds (u ^ s) ^ v ==>. (u ^ t) ^ v,S let s, t, u, v be Element of E ^omega ; ::_thesis: ( s -->. t,S implies (u ^ s) ^ v ==>. (u ^ t) ^ v,S ) assume s -->. t,S ; ::_thesis: (u ^ s) ^ v ==>. (u ^ t) ^ v,S then u ^ s ==>. u ^ t,S by Th14; hence (u ^ s) ^ v ==>. (u ^ t) ^ v,S by Th12; ::_thesis: verum end; theorem Th16: :: REWRITE2:16 for E being set for S being semi-Thue-system of E for s, t being Element of E ^omega st S is Thue-system of E & s -->. t,S holds t -->. s,S proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t being Element of E ^omega st S is Thue-system of E & s -->. t,S holds t -->. s,S let S be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st S is Thue-system of E & s -->. t,S holds t -->. s,S let s, t be Element of E ^omega ; ::_thesis: ( S is Thue-system of E & s -->. t,S implies t -->. s,S ) assume ( S is Thue-system of E & s -->. t,S ) ; ::_thesis: t -->. s,S then ( S = S ~ & [s,t] in S ) by Def4, RELAT_2:13; then [t,s] in S by RELAT_1:def_7; hence t -->. s,S by Def4; ::_thesis: verum end; theorem Th17: :: REWRITE2:17 for E being set for S being semi-Thue-system of E for s, t being Element of E ^omega st S is Thue-system of E & s ==>. t,S holds t ==>. s,S proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t being Element of E ^omega st S is Thue-system of E & s ==>. t,S holds t ==>. s,S let S be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st S is Thue-system of E & s ==>. t,S holds t ==>. s,S let s, t be Element of E ^omega ; ::_thesis: ( S is Thue-system of E & s ==>. t,S implies t ==>. s,S ) assume that A1: S is Thue-system of E and A2: s ==>. t,S ; ::_thesis: t ==>. s,S consider v, w, s1, t1 being Element of E ^omega such that A3: ( s = (v ^ s1) ^ w & t = (v ^ t1) ^ w ) and A4: s1 -->. t1,S by A2, Def5; t1 -->. s1,S by A1, A4, Th16; hence t ==>. s,S by A3, Def5; ::_thesis: verum end; theorem Th18: :: REWRITE2:18 for E being set for S, T being semi-Thue-system of E for s, t being Element of E ^omega st S c= T & s -->. t,S holds s -->. t,T proof let E be set ; ::_thesis: for S, T being semi-Thue-system of E for s, t being Element of E ^omega st S c= T & s -->. t,S holds s -->. t,T let S, T be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st S c= T & s -->. t,S holds s -->. t,T let s, t be Element of E ^omega ; ::_thesis: ( S c= T & s -->. t,S implies s -->. t,T ) assume that A1: S c= T and A2: s -->. t,S ; ::_thesis: s -->. t,T [s,t] in S by A2, Def4; hence s -->. t,T by A1, Def4; ::_thesis: verum end; theorem Th19: :: REWRITE2:19 for E being set for S, T being semi-Thue-system of E for s, t being Element of E ^omega st S c= T & s ==>. t,S holds s ==>. t,T proof let E be set ; ::_thesis: for S, T being semi-Thue-system of E for s, t being Element of E ^omega st S c= T & s ==>. t,S holds s ==>. t,T let S, T be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st S c= T & s ==>. t,S holds s ==>. t,T let s, t be Element of E ^omega ; ::_thesis: ( S c= T & s ==>. t,S implies s ==>. t,T ) assume that A1: S c= T and A2: s ==>. t,S ; ::_thesis: s ==>. t,T consider v, w, s1, t1 being Element of E ^omega such that A3: ( s = (v ^ s1) ^ w & t = (v ^ t1) ^ w ) and A4: s1 -->. t1,S by A2, Def5; s1 -->. t1,T by A1, A4, Th18; hence s ==>. t,T by A3, Def5; ::_thesis: verum end; theorem Th20: :: REWRITE2:20 for E being set for s, t being Element of E ^omega holds not s ==>. t, {} ((E ^omega),(E ^omega)) proof let E be set ; ::_thesis: for s, t being Element of E ^omega holds not s ==>. t, {} ((E ^omega),(E ^omega)) let s, t be Element of E ^omega ; ::_thesis: not s ==>. t, {} ((E ^omega),(E ^omega)) assume s ==>. t, {} ((E ^omega),(E ^omega)) ; ::_thesis: contradiction then consider v, w, s1, t1 being Element of E ^omega such that s = (v ^ s1) ^ w and t = (v ^ t1) ^ w and A1: s1 -->. t1, {} ((E ^omega),(E ^omega)) by Def5; [s1,t1] in {} ((E ^omega),(E ^omega)) by A1, Def4; hence contradiction by PARTIT_2:def_1; ::_thesis: verum end; theorem Th21: :: REWRITE2:21 for E being set for S, T being semi-Thue-system of E for s, t being Element of E ^omega holds ( not s ==>. t,S \/ T or s ==>. t,S or s ==>. t,T ) proof let E be set ; ::_thesis: for S, T being semi-Thue-system of E for s, t being Element of E ^omega holds ( not s ==>. t,S \/ T or s ==>. t,S or s ==>. t,T ) let S, T be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega holds ( not s ==>. t,S \/ T or s ==>. t,S or s ==>. t,T ) let s, t be Element of E ^omega ; ::_thesis: ( not s ==>. t,S \/ T or s ==>. t,S or s ==>. t,T ) assume s ==>. t,S \/ T ; ::_thesis: ( s ==>. t,S or s ==>. t,T ) then consider v, w, s1, t1 being Element of E ^omega such that A1: ( s = (v ^ s1) ^ w & t = (v ^ t1) ^ w ) and A2: s1 -->. t1,S \/ T by Def5; A3: [s1,t1] in S \/ T by A2, Def4; percases ( [s1,t1] in S or [s1,t1] in T ) by A3, XBOOLE_0:def_3; suppose [s1,t1] in S ; ::_thesis: ( s ==>. t,S or s ==>. t,T ) then s1 -->. t1,S by Def4; hence ( s ==>. t,S or s ==>. t,T ) by A1, Def5; ::_thesis: verum end; suppose [s1,t1] in T ; ::_thesis: ( s ==>. t,S or s ==>. t,T ) then s1 -->. t1,T by Def4; hence ( s ==>. t,S or s ==>. t,T ) by A1, Def5; ::_thesis: verum end; end; end; begin definition let E be set ; :: original: id redefine func id E -> Relation of E; coherence id E is Relation of E by RELSET_1:14; end; definition let E be set ; let S be semi-Thue-system of E; func ==>.-relation S -> Relation of (E ^omega) means :Def6: :: REWRITE2:def 6 for s, t being Element of E ^omega holds ( [s,t] in it iff s ==>. t,S ); existence ex b1 being Relation of (E ^omega) st for s, t being Element of E ^omega holds ( [s,t] in b1 iff s ==>. t,S ) proof defpred S1[ Element of E ^omega , Element of E ^omega ] means \$1 ==>. \$2,S; consider R being Relation of (E ^omega) such that A1: for s, t being Element of E ^omega holds ( [s,t] in R iff S1[s,t] ) from RELSET_1:sch_2(); take R ; ::_thesis: for s, t being Element of E ^omega holds ( [s,t] in R iff s ==>. t,S ) thus for s, t being Element of E ^omega holds ( [s,t] in R iff s ==>. t,S ) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Relation of (E ^omega) st ( for s, t being Element of E ^omega holds ( [s,t] in b1 iff s ==>. t,S ) ) & ( for s, t being Element of E ^omega holds ( [s,t] in b2 iff s ==>. t,S ) ) holds b1 = b2 proof let R1, R2 be Relation of (E ^omega); ::_thesis: ( ( for s, t being Element of E ^omega holds ( [s,t] in R1 iff s ==>. t,S ) ) & ( for s, t being Element of E ^omega holds ( [s,t] in R2 iff s ==>. t,S ) ) implies R1 = R2 ) assume that A2: for s, t being Element of E ^omega holds ( [s,t] in R1 iff s ==>. t,S ) and A3: for s, t being Element of E ^omega holds ( [s,t] in R2 iff s ==>. t,S ) ; ::_thesis: R1 = R2 now__::_thesis:_for_s,_t_being_Element_of_E_^omega_holds_ (_[s,t]_in_R1_iff_[s,t]_in_R2_) let s, t be Element of E ^omega ; ::_thesis: ( [s,t] in R1 iff [s,t] in R2 ) ( [s,t] in R1 iff s ==>. t,S ) by A2; hence ( [s,t] in R1 iff [s,t] in R2 ) by A3; ::_thesis: verum end; hence R1 = R2 by RELSET_1:def_2; ::_thesis: verum end; end; :: deftheorem Def6 defines ==>.-relation REWRITE2:def_6_:_ for E being set for S being semi-Thue-system of E for b3 being Relation of (E ^omega) holds ( b3 = ==>.-relation S iff for s, t being Element of E ^omega holds ( [s,t] in b3 iff s ==>. t,S ) ); theorem Th22: :: REWRITE2:22 for E being set for S being semi-Thue-system of E holds S c= ==>.-relation S proof let E be set ; ::_thesis: for S being semi-Thue-system of E holds S c= ==>.-relation S let S be semi-Thue-system of E; ::_thesis: S c= ==>.-relation S thus for x being set st x in S holds x in ==>.-relation S :: according to TARSKI:def_3 ::_thesis: verum proof let x be set ; ::_thesis: ( x in S implies x in ==>.-relation S ) assume A1: x in S ; ::_thesis: x in ==>.-relation S then consider a, b being set such that A2: ( a in E ^omega & b in E ^omega ) and A3: x = [a,b] by ZFMISC_1:def_2; reconsider a = a, b = b as Element of E ^omega by A2; a -->. b,S by A1, A3, Def4; then a ==>. b,S by Th10; hence x in ==>.-relation S by A3, Def6; ::_thesis: verum end; end; theorem Th23: :: REWRITE2:23 for E being set for S being semi-Thue-system of E for u being Element of E ^omega for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds ( p +^ u is RedSequence of ==>.-relation S & u ^+ p is RedSequence of ==>.-relation S ) proof let E be set ; ::_thesis: for S being semi-Thue-system of E for u being Element of E ^omega for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds ( p +^ u is RedSequence of ==>.-relation S & u ^+ p is RedSequence of ==>.-relation S ) let S be semi-Thue-system of E; ::_thesis: for u being Element of E ^omega for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds ( p +^ u is RedSequence of ==>.-relation S & u ^+ p is RedSequence of ==>.-relation S ) let u be Element of E ^omega ; ::_thesis: for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds ( p +^ u is RedSequence of ==>.-relation S & u ^+ p is RedSequence of ==>.-relation S ) let p be FinSequence of E ^omega ; ::_thesis: ( p is RedSequence of ==>.-relation S implies ( p +^ u is RedSequence of ==>.-relation S & u ^+ p is RedSequence of ==>.-relation S ) ) assume A1: p is RedSequence of ==>.-relation S ; ::_thesis: ( p +^ u is RedSequence of ==>.-relation S & u ^+ p is RedSequence of ==>.-relation S ) A2: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(p_+^_u)_&_i_+_1_in_dom_(p_+^_u)_holds_ [((p_+^_u)_._i),((p_+^_u)_._(i_+_1))]_in_==>.-relation_S let i be Element of NAT ; ::_thesis: ( i in dom (p +^ u) & i + 1 in dom (p +^ u) implies [((p +^ u) . i),((p +^ u) . (i + 1))] in ==>.-relation S ) assume that A3: i in dom (p +^ u) and A4: i + 1 in dom (p +^ u) ; ::_thesis: [((p +^ u) . i),((p +^ u) . (i + 1))] in ==>.-relation S A5: i + 1 in dom p by A4, Def3; then A6: (p +^ u) . (i + 1) = (p . (i + 1)) ^ u by Def3; A7: i in dom p by A3, Def3; then [(p . i),(p . (i + 1))] in ==>.-relation S by A1, A5, REWRITE1:def_2; then p . i ==>. p . (i + 1),S by Def6; then A8: (p . i) ^ u ==>. (p . (i + 1)) ^ u,S by Th12; (p +^ u) . i = (p . i) ^ u by A7, Def3; hence [((p +^ u) . i),((p +^ u) . (i + 1))] in ==>.-relation S by A6, A8, Def6; ::_thesis: verum end; A9: now__::_thesis:_for_i_being_Element_of_NAT_st_i_in_dom_(u_^+_p)_&_i_+_1_in_dom_(u_^+_p)_holds_ [((u_^+_p)_._i),((u_^+_p)_._(i_+_1))]_in_==>.-relation_S let i be Element of NAT ; ::_thesis: ( i in dom (u ^+ p) & i + 1 in dom (u ^+ p) implies [((u ^+ p) . i),((u ^+ p) . (i + 1))] in ==>.-relation S ) assume that A10: i in dom (u ^+ p) and A11: i + 1 in dom (u ^+ p) ; ::_thesis: [((u ^+ p) . i),((u ^+ p) . (i + 1))] in ==>.-relation S A12: i + 1 in dom p by A11, Def2; then A13: (u ^+ p) . (i + 1) = u ^ (p . (i + 1)) by Def2; A14: i in dom p by A10, Def2; then [(p . i),(p . (i + 1))] in ==>.-relation S by A1, A12, REWRITE1:def_2; then p . i ==>. p . (i + 1),S by Def6; then A15: u ^ (p . i) ==>. u ^ (p . (i + 1)),S by Th12; (u ^+ p) . i = u ^ (p . i) by A14, Def2; hence [((u ^+ p) . i),((u ^+ p) . (i + 1))] in ==>.-relation S by A13, A15, Def6; ::_thesis: verum end; len (p +^ u) = len p by Th5; hence p +^ u is RedSequence of ==>.-relation S by A1, A2, REWRITE1:def_2; ::_thesis: u ^+ p is RedSequence of ==>.-relation S len (u ^+ p) = len p by Th5; hence u ^+ p is RedSequence of ==>.-relation S by A1, A9, REWRITE1:def_2; ::_thesis: verum end; theorem :: REWRITE2:24 for E being set for S being semi-Thue-system of E for t, u being Element of E ^omega for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds (t ^+ p) +^ u is RedSequence of ==>.-relation S proof let E be set ; ::_thesis: for S being semi-Thue-system of E for t, u being Element of E ^omega for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds (t ^+ p) +^ u is RedSequence of ==>.-relation S let S be semi-Thue-system of E; ::_thesis: for t, u being Element of E ^omega for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds (t ^+ p) +^ u is RedSequence of ==>.-relation S let t, u be Element of E ^omega ; ::_thesis: for p being FinSequence of E ^omega st p is RedSequence of ==>.-relation S holds (t ^+ p) +^ u is RedSequence of ==>.-relation S let p be FinSequence of E ^omega ; ::_thesis: ( p is RedSequence of ==>.-relation S implies (t ^+ p) +^ u is RedSequence of ==>.-relation S ) assume p is RedSequence of ==>.-relation S ; ::_thesis: (t ^+ p) +^ u is RedSequence of ==>.-relation S then t ^+ p is RedSequence of ==>.-relation S by Th23; hence (t ^+ p) +^ u is RedSequence of ==>.-relation S by Th23; ::_thesis: verum end; theorem Th25: :: REWRITE2:25 for E being set for S being semi-Thue-system of E st S is Thue-system of E holds ==>.-relation S = (==>.-relation S) ~ proof let E be set ; ::_thesis: for S being semi-Thue-system of E st S is Thue-system of E holds ==>.-relation S = (==>.-relation S) ~ let S be semi-Thue-system of E; ::_thesis: ( S is Thue-system of E implies ==>.-relation S = (==>.-relation S) ~ ) assume A1: S is Thue-system of E ; ::_thesis: ==>.-relation S = (==>.-relation S) ~ now__::_thesis:_for_x_being_set_holds_ (_(_x_in_==>.-relation_S_implies_x_in_(==>.-relation_S)_~_)_&_(_x_in_(==>.-relation_S)_~_implies_x_in_==>.-relation_S_)_) let x be set ; ::_thesis: ( ( x in ==>.-relation S implies x in (==>.-relation S) ~ ) & ( x in (==>.-relation S) ~ implies x in ==>.-relation S ) ) thus ( x in ==>.-relation S implies x in (==>.-relation S) ~ ) ::_thesis: ( x in (==>.-relation S) ~ implies x in ==>.-relation S ) proof assume A2: x in ==>.-relation S ; ::_thesis: x in (==>.-relation S) ~ then consider a, b being set such that A3: ( a in E ^omega & b in E ^omega ) and A4: x = [a,b] by ZFMISC_1:def_2; reconsider a = a, b = b as Element of E ^omega by A3; a ==>. b,S by A2, A4, Def6; then b ==>. a,S by A1, Th17; then [b,a] in ==>.-relation S by Def6; hence x in (==>.-relation S) ~ by A4, RELAT_1:def_7; ::_thesis: verum end; thus ( x in (==>.-relation S) ~ implies x in ==>.-relation S ) ::_thesis: verum proof assume A5: x in (==>.-relation S) ~ ; ::_thesis: x in ==>.-relation S then consider a, b being set such that A6: ( a in E ^omega & b in E ^omega ) and A7: x = [a,b] by ZFMISC_1:def_2; reconsider a = a, b = b as Element of E ^omega by A6; [b,a] in ==>.-relation S by A5, A7, RELAT_1:def_7; then b ==>. a,S by Def6; then a ==>. b,S by A1, Th17; hence x in ==>.-relation S by A7, Def6; ::_thesis: verum end; end; hence ==>.-relation S = (==>.-relation S) ~ by TARSKI:1; ::_thesis: verum end; theorem Th26: :: REWRITE2:26 for E being set for S, T being semi-Thue-system of E st S c= T holds ==>.-relation S c= ==>.-relation T proof let E be set ; ::_thesis: for S, T being semi-Thue-system of E st S c= T holds ==>.-relation S c= ==>.-relation T let S, T be semi-Thue-system of E; ::_thesis: ( S c= T implies ==>.-relation S c= ==>.-relation T ) assume A1: S c= T ; ::_thesis: ==>.-relation S c= ==>.-relation T thus for x being set st x in ==>.-relation S holds x in ==>.-relation T :: according to TARSKI:def_3 ::_thesis: verum proof let x be set ; ::_thesis: ( x in ==>.-relation S implies x in ==>.-relation T ) assume A2: x in ==>.-relation S ; ::_thesis: x in ==>.-relation T then consider s, t being set such that A3: x = [s,t] and A4: ( s in E ^omega & t in E ^omega ) by RELSET_1:2; reconsider s = s, t = t as Element of E ^omega by A4; s ==>. t,S by A2, A3, Def6; then s ==>. t,T by A1, Th19; hence x in ==>.-relation T by A3, Def6; ::_thesis: verum end; end; theorem Th27: :: REWRITE2:27 for E being set holds ==>.-relation (id (E ^omega)) = id (E ^omega) proof let E be set ; ::_thesis: ==>.-relation (id (E ^omega)) = id (E ^omega) A1: ==>.-relation (id (E ^omega)) c= id (E ^omega) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ==>.-relation (id (E ^omega)) or x in id (E ^omega) ) assume A2: x in ==>.-relation (id (E ^omega)) ; ::_thesis: x in id (E ^omega) then consider a, b being set such that A3: ( a in E ^omega & b in E ^omega ) and A4: x = [a,b] by ZFMISC_1:def_2; reconsider a = a, b = b as Element of E ^omega by A3; a ==>. b, id (E ^omega) by A2, A4, Def6; then consider v, w, s1, t1 being Element of E ^omega such that A5: ( a = (v ^ s1) ^ w & b = (v ^ t1) ^ w ) and A6: s1 -->. t1, id (E ^omega) by Def5; [s1,t1] in id (E ^omega) by A6, Def4; then s1 = t1 by RELAT_1:def_10; hence x in id (E ^omega) by A4, A5, RELAT_1:def_10; ::_thesis: verum end; id (E ^omega) c= ==>.-relation (id (E ^omega)) by Th22; hence ==>.-relation (id (E ^omega)) = id (E ^omega) by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th28: :: REWRITE2:28 for E being set for S being semi-Thue-system of E holds ==>.-relation (S \/ (id (E ^omega))) = (==>.-relation S) \/ (id (E ^omega)) proof let E be set ; ::_thesis: for S being semi-Thue-system of E holds ==>.-relation (S \/ (id (E ^omega))) = (==>.-relation S) \/ (id (E ^omega)) let S be semi-Thue-system of E; ::_thesis: ==>.-relation (S \/ (id (E ^omega))) = (==>.-relation S) \/ (id (E ^omega)) A1: ==>.-relation (S \/ (id (E ^omega))) c= (==>.-relation S) \/ (id (E ^omega)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ==>.-relation (S \/ (id (E ^omega))) or x in (==>.-relation S) \/ (id (E ^omega)) ) assume A2: x in ==>.-relation (S \/ (id (E ^omega))) ; ::_thesis: x in (==>.-relation S) \/ (id (E ^omega)) then consider a, b being set such that A3: ( a in E ^omega & b in E ^omega ) and A4: x = [a,b] by ZFMISC_1:def_2; reconsider a = a, b = b as Element of E ^omega by A3; a ==>. b,S \/ (id (E ^omega)) by A2, A4, Def6; then consider v, w, s1, t1 being Element of E ^omega such that A5: ( a = (v ^ s1) ^ w & b = (v ^ t1) ^ w ) and A6: s1 -->. t1,S \/ (id (E ^omega)) by Def5; A7: [s1,t1] in S \/ (id (E ^omega)) by A6, Def4; percases ( [s1,t1] in S or [s1,t1] in id (E ^omega) ) by A7, XBOOLE_0:def_3; suppose [s1,t1] in S ; ::_thesis: x in (==>.-relation S) \/ (id (E ^omega)) then s1 -->. t1,S by Def4; then (v ^ s1) ^ w ==>. (v ^ t1) ^ w,S by Th15; then x in ==>.-relation S by A4, A5, Def6; hence x in (==>.-relation S) \/ (id (E ^omega)) by XBOOLE_0:def_3; ::_thesis: verum end; suppose [s1,t1] in id (E ^omega) ; ::_thesis: x in (==>.-relation S) \/ (id (E ^omega)) then s1 = t1 by RELAT_1:def_10; then x in id (E ^omega) by A4, A5, RELAT_1:def_10; hence x in (==>.-relation S) \/ (id (E ^omega)) by XBOOLE_0:def_3; ::_thesis: verum end; end; end; (==>.-relation S) \/ (id (E ^omega)) c= ==>.-relation (S \/ (id (E ^omega))) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (==>.-relation S) \/ (id (E ^omega)) or x in ==>.-relation (S \/ (id (E ^omega))) ) assume A8: x in (==>.-relation S) \/ (id (E ^omega)) ; ::_thesis: x in ==>.-relation (S \/ (id (E ^omega))) percases ( x in ==>.-relation S or x in id (E ^omega) ) by A8, XBOOLE_0:def_3; supposeA9: x in ==>.-relation S ; ::_thesis: x in ==>.-relation (S \/ (id (E ^omega))) ==>.-relation S c= ==>.-relation (S \/ (id (E ^omega))) by Th26, XBOOLE_1:7; hence x in ==>.-relation (S \/ (id (E ^omega))) by A9; ::_thesis: verum end; supposeA10: x in id (E ^omega) ; ::_thesis: x in ==>.-relation (S \/ (id (E ^omega))) A11: ==>.-relation (id (E ^omega)) c= ==>.-relation (S \/ (id (E ^omega))) by Th26, XBOOLE_1:7; x in ==>.-relation (id (E ^omega)) by A10, Th27; hence x in ==>.-relation (S \/ (id (E ^omega))) by A11; ::_thesis: verum end; end; end; hence ==>.-relation (S \/ (id (E ^omega))) = (==>.-relation S) \/ (id (E ^omega)) by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th29: :: REWRITE2:29 for E being set holds ==>.-relation ({} ((E ^omega),(E ^omega))) = {} ((E ^omega),(E ^omega)) proof let E be set ; ::_thesis: ==>.-relation ({} ((E ^omega),(E ^omega))) = {} ((E ^omega),(E ^omega)) A1: ==>.-relation ({} ((E ^omega),(E ^omega))) c= {} ((E ^omega),(E ^omega)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ==>.-relation ({} ((E ^omega),(E ^omega))) or x in {} ((E ^omega),(E ^omega)) ) assume A2: x in ==>.-relation ({} ((E ^omega),(E ^omega))) ; ::_thesis: x in {} ((E ^omega),(E ^omega)) then consider a, b being set such that A3: ( a in E ^omega & b in E ^omega ) and A4: x = [a,b] by ZFMISC_1:def_2; reconsider a = a, b = b as Element of E ^omega by A3; a ==>. b, {} ((E ^omega),(E ^omega)) by A2, A4, Def6; hence x in {} ((E ^omega),(E ^omega)) by Th20; ::_thesis: verum end; {} ((E ^omega),(E ^omega)) = {} by PARTIT_2:def_1; then {} ((E ^omega),(E ^omega)) c= ==>.-relation ({} ((E ^omega),(E ^omega))) by XBOOLE_1:2; hence ==>.-relation ({} ((E ^omega),(E ^omega))) = {} ((E ^omega),(E ^omega)) by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th30: :: REWRITE2:30 for E being set for S being semi-Thue-system of E for s, t being Element of E ^omega st s ==>. t, ==>.-relation S holds s ==>. t,S proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t being Element of E ^omega st s ==>. t, ==>.-relation S holds s ==>. t,S let S be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st s ==>. t, ==>.-relation S holds s ==>. t,S let s, t be Element of E ^omega ; ::_thesis: ( s ==>. t, ==>.-relation S implies s ==>. t,S ) assume s ==>. t, ==>.-relation S ; ::_thesis: s ==>. t,S then consider v, w, s1, t1 being Element of E ^omega such that A1: ( s = (v ^ s1) ^ w & t = (v ^ t1) ^ w ) and A2: s1 -->. t1, ==>.-relation S by Def5; [s1,t1] in ==>.-relation S by A2, Def4; then s1 ==>. t1,S by Def6; hence s ==>. t,S by A1, Th13; ::_thesis: verum end; theorem Th31: :: REWRITE2:31 for E being set for S being semi-Thue-system of E holds ==>.-relation (==>.-relation S) = ==>.-relation S proof let E be set ; ::_thesis: for S being semi-Thue-system of E holds ==>.-relation (==>.-relation S) = ==>.-relation S let S be semi-Thue-system of E; ::_thesis: ==>.-relation (==>.-relation S) = ==>.-relation S A1: ==>.-relation (==>.-relation S) c= ==>.-relation S proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in ==>.-relation (==>.-relation S) or x in ==>.-relation S ) assume A2: x in ==>.-relation (==>.-relation S) ; ::_thesis: x in ==>.-relation S then consider a, b being set such that A3: ( a in E ^omega & b in E ^omega ) and A4: x = [a,b] by ZFMISC_1:def_2; reconsider a = a, b = b as Element of E ^omega by A3; a ==>. b, ==>.-relation S by A2, A4, Def6; then a ==>. b,S by Th30; hence x in ==>.-relation S by A4, Def6; ::_thesis: verum end; ==>.-relation S c= ==>.-relation (==>.-relation S) by Th22; hence ==>.-relation (==>.-relation S) = ==>.-relation S by A1, XBOOLE_0:def_10; ::_thesis: verum end; begin definition let E be set ; let S be semi-Thue-system of E; let s, t be Element of E ^omega ; preds ==>* t,S means :Def7: :: REWRITE2:def 7 ==>.-relation S reduces s,t; end; :: deftheorem Def7 defines ==>* REWRITE2:def_7_:_ for E being set for S being semi-Thue-system of E for s, t being Element of E ^omega holds ( s ==>* t,S iff ==>.-relation S reduces s,t ); theorem Th32: :: REWRITE2:32 for E being set for S being semi-Thue-system of E for s being Element of E ^omega holds s ==>* s,S proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s being Element of E ^omega holds s ==>* s,S let S be semi-Thue-system of E; ::_thesis: for s being Element of E ^omega holds s ==>* s,S let s be Element of E ^omega ; ::_thesis: s ==>* s,S ==>.-relation S reduces s,s by REWRITE1:12; hence s ==>* s,S by Def7; ::_thesis: verum end; theorem Th33: :: REWRITE2:33 for E being set for S being semi-Thue-system of E for s, t being Element of E ^omega st s ==>. t,S holds s ==>* t,S proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t being Element of E ^omega st s ==>. t,S holds s ==>* t,S let S be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st s ==>. t,S holds s ==>* t,S let s, t be Element of E ^omega ; ::_thesis: ( s ==>. t,S implies s ==>* t,S ) assume s ==>. t,S ; ::_thesis: s ==>* t,S then [s,t] in ==>.-relation S by Def6; then ==>.-relation S reduces s,t by REWRITE1:15; hence s ==>* t,S by Def7; ::_thesis: verum end; theorem :: REWRITE2:34 for E being set for S being semi-Thue-system of E for s, t being Element of E ^omega st s -->. t,S holds s ==>* t,S by Th10, Th33; theorem Th35: :: REWRITE2:35 for E being set for S being semi-Thue-system of E for s, t, u being Element of E ^omega st s ==>* t,S & t ==>* u,S holds s ==>* u,S proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t, u being Element of E ^omega st s ==>* t,S & t ==>* u,S holds s ==>* u,S let S be semi-Thue-system of E; ::_thesis: for s, t, u being Element of E ^omega st s ==>* t,S & t ==>* u,S holds s ==>* u,S let s, t, u be Element of E ^omega ; ::_thesis: ( s ==>* t,S & t ==>* u,S implies s ==>* u,S ) assume ( s ==>* t,S & t ==>* u,S ) ; ::_thesis: s ==>* u,S then ( ==>.-relation S reduces s,t & ==>.-relation S reduces t,u ) by Def7; then ==>.-relation S reduces s,u by REWRITE1:16; hence s ==>* u,S by Def7; ::_thesis: verum end; theorem Th36: :: REWRITE2:36 for E being set for S being semi-Thue-system of E for s, t, u being Element of E ^omega st s ==>* t,S holds ( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S ) proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t, u being Element of E ^omega st s ==>* t,S holds ( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S ) let S be semi-Thue-system of E; ::_thesis: for s, t, u being Element of E ^omega st s ==>* t,S holds ( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S ) let s, t, u be Element of E ^omega ; ::_thesis: ( s ==>* t,S implies ( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S ) ) assume s ==>* t,S ; ::_thesis: ( s ^ u ==>* t ^ u,S & u ^ s ==>* u ^ t,S ) then ==>.-relation S reduces s,t by Def7; then consider p being RedSequence of ==>.-relation S such that A1: p . 1 = s and A2: p . (len p) = t by REWRITE1:def_3; reconsider p = p as FinSequence of E ^omega by A1, ABCMIZ_0:73; 1 in dom p by FINSEQ_5:6; then A3: (p +^ u) . 1 = s ^ u by A1, Def3; A4: len p = len (p +^ u) by Th5; then len (p +^ u) in dom p by FINSEQ_5:6; then A5: (p +^ u) . (len (p +^ u)) = t ^ u by A2, A4, Def3; p +^ u is RedSequence of ==>.-relation S by Th23; then ==>.-relation S reduces s ^ u,t ^ u by A3, A5, REWRITE1:def_3; hence s ^ u ==>* t ^ u,S by Def7; ::_thesis: u ^ s ==>* u ^ t,S 1 in dom p by FINSEQ_5:6; then A6: (u ^+ p) . 1 = u ^ s by A1, Def2; A7: len p = len (u ^+ p) by Th5; then len (u ^+ p) in dom p by FINSEQ_5:6; then A8: (u ^+ p) . (len (u ^+ p)) = u ^ t by A2, A7, Def2; u ^+ p is RedSequence of ==>.-relation S by Th23; then ==>.-relation S reduces u ^ s,u ^ t by A6, A8, REWRITE1:def_3; hence u ^ s ==>* u ^ t,S by Def7; ::_thesis: verum end; theorem Th37: :: REWRITE2:37 for E being set for S being semi-Thue-system of E for s, t, u, v being Element of E ^omega st s ==>* t,S holds (u ^ s) ^ v ==>* (u ^ t) ^ v,S proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t, u, v being Element of E ^omega st s ==>* t,S holds (u ^ s) ^ v ==>* (u ^ t) ^ v,S let S be semi-Thue-system of E; ::_thesis: for s, t, u, v being Element of E ^omega st s ==>* t,S holds (u ^ s) ^ v ==>* (u ^ t) ^ v,S let s, t, u, v be Element of E ^omega ; ::_thesis: ( s ==>* t,S implies (u ^ s) ^ v ==>* (u ^ t) ^ v,S ) assume s ==>* t,S ; ::_thesis: (u ^ s) ^ v ==>* (u ^ t) ^ v,S then u ^ s ==>* u ^ t,S by Th36; hence (u ^ s) ^ v ==>* (u ^ t) ^ v,S by Th36; ::_thesis: verum end; theorem :: REWRITE2:38 for E being set for S being semi-Thue-system of E for s, t, u, v being Element of E ^omega st s ==>* t,S & u ==>* v,S holds ( s ^ u ==>* t ^ v,S & u ^ s ==>* v ^ t,S ) proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t, u, v being Element of E ^omega st s ==>* t,S & u ==>* v,S holds ( s ^ u ==>* t ^ v,S & u ^ s ==>* v ^ t,S ) let S be semi-Thue-system of E; ::_thesis: for s, t, u, v being Element of E ^omega st s ==>* t,S & u ==>* v,S holds ( s ^ u ==>* t ^ v,S & u ^ s ==>* v ^ t,S ) let s, t, u, v be Element of E ^omega ; ::_thesis: ( s ==>* t,S & u ==>* v,S implies ( s ^ u ==>* t ^ v,S & u ^ s ==>* v ^ t,S ) ) assume A1: ( s ==>* t,S & u ==>* v,S ) ; ::_thesis: ( s ^ u ==>* t ^ v,S & u ^ s ==>* v ^ t,S ) then ( s ^ u ==>* t ^ u,S & t ^ u ==>* t ^ v,S ) by Th36; hence s ^ u ==>* t ^ v,S by Th35; ::_thesis: u ^ s ==>* v ^ t,S ( u ^ s ==>* u ^ t,S & u ^ t ==>* v ^ t,S ) by A1, Th36; hence u ^ s ==>* v ^ t,S by Th35; ::_thesis: verum end; theorem :: REWRITE2:39 for E being set for S being semi-Thue-system of E for s, t being Element of E ^omega st S is Thue-system of E & s ==>* t,S holds t ==>* s,S proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t being Element of E ^omega st S is Thue-system of E & s ==>* t,S holds t ==>* s,S let S be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st S is Thue-system of E & s ==>* t,S holds t ==>* s,S let s, t be Element of E ^omega ; ::_thesis: ( S is Thue-system of E & s ==>* t,S implies t ==>* s,S ) assume that A1: S is Thue-system of E and A2: s ==>* t,S ; ::_thesis: t ==>* s,S ==>.-relation S reduces s,t by A2, Def7; then consider p being RedSequence of ==>.-relation S such that A3: p . 1 = s and A4: p . (len p) = t by REWRITE1:def_3; set q = Rev p; (Rev p) . (len p) = s by A3, FINSEQ_5:62; then A5: (Rev p) . (len (Rev p)) = s by FINSEQ_5:def_3; Rev p is RedSequence of (==>.-relation S) ~ by REWRITE1:9; then A6: Rev p is RedSequence of ==>.-relation S by A1, Th25; (Rev p) . 1 = t by A4, FINSEQ_5:62; then ==>.-relation S reduces t,s by A6, A5, REWRITE1:def_3; hence t ==>* s,S by Def7; ::_thesis: verum end; theorem Th40: :: REWRITE2:40 for E being set for S, T being semi-Thue-system of E for s, t being Element of E ^omega st S c= T & s ==>* t,S holds s ==>* t,T proof let E be set ; ::_thesis: for S, T being semi-Thue-system of E for s, t being Element of E ^omega st S c= T & s ==>* t,S holds s ==>* t,T let S, T be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st S c= T & s ==>* t,S holds s ==>* t,T let s, t be Element of E ^omega ; ::_thesis: ( S c= T & s ==>* t,S implies s ==>* t,T ) assume that A1: S c= T and A2: s ==>* t,S ; ::_thesis: s ==>* t,T ==>.-relation S reduces s,t by A2, Def7; then ==>.-relation T reduces s,t by A1, Th26, REWRITE1:22; hence s ==>* t,T by Def7; ::_thesis: verum end; theorem Th41: :: REWRITE2:41 for E being set for S being semi-Thue-system of E for s, t being Element of E ^omega holds ( s ==>* t,S iff s ==>* t,S \/ (id (E ^omega)) ) proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t being Element of E ^omega holds ( s ==>* t,S iff s ==>* t,S \/ (id (E ^omega)) ) let S be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega holds ( s ==>* t,S iff s ==>* t,S \/ (id (E ^omega)) ) let s, t be Element of E ^omega ; ::_thesis: ( s ==>* t,S iff s ==>* t,S \/ (id (E ^omega)) ) thus ( s ==>* t,S implies s ==>* t,S \/ (id (E ^omega)) ) by Th40, XBOOLE_1:7; ::_thesis: ( s ==>* t,S \/ (id (E ^omega)) implies s ==>* t,S ) assume s ==>* t,S \/ (id (E ^omega)) ; ::_thesis: s ==>* t,S then ==>.-relation (S \/ (id (E ^omega))) reduces s,t by Def7; then (==>.-relation S) \/ (id (E ^omega)) reduces s,t by Th28; then ==>.-relation S reduces s,t by REWRITE1:23; hence s ==>* t,S by Def7; ::_thesis: verum end; theorem Th42: :: REWRITE2:42 for E being set for s, t being Element of E ^omega st s ==>* t, {} ((E ^omega),(E ^omega)) holds s = t proof let E be set ; ::_thesis: for s, t being Element of E ^omega st s ==>* t, {} ((E ^omega),(E ^omega)) holds s = t let s, t be Element of E ^omega ; ::_thesis: ( s ==>* t, {} ((E ^omega),(E ^omega)) implies s = t ) assume s ==>* t, {} ((E ^omega),(E ^omega)) ; ::_thesis: s = t then ==>.-relation ({} ((E ^omega),(E ^omega))) reduces s,t by Def7; then {} ((E ^omega),(E ^omega)) reduces s,t by Th29; then {} reduces s,t by PARTIT_2:def_1; hence s = t by REWRITE1:13; ::_thesis: verum end; theorem Th43: :: REWRITE2:43 for E being set for S being semi-Thue-system of E for s, t being Element of E ^omega st s ==>* t, ==>.-relation S holds s ==>* t,S proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t being Element of E ^omega st s ==>* t, ==>.-relation S holds s ==>* t,S let S be semi-Thue-system of E; ::_thesis: for s, t being Element of E ^omega st s ==>* t, ==>.-relation S holds s ==>* t,S let s, t be Element of E ^omega ; ::_thesis: ( s ==>* t, ==>.-relation S implies s ==>* t,S ) assume s ==>* t, ==>.-relation S ; ::_thesis: s ==>* t,S then ==>.-relation (==>.-relation S) reduces s,t by Def7; then ==>.-relation S reduces s,t by Th31; hence s ==>* t,S by Def7; ::_thesis: verum end; theorem Th44: :: REWRITE2:44 for E being set for S being semi-Thue-system of E for s, t, u, v being Element of E ^omega st s ==>* t,S & u ==>. v,{[s,t]} holds u ==>* v,S proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t, u, v being Element of E ^omega st s ==>* t,S & u ==>. v,{[s,t]} holds u ==>* v,S let S be semi-Thue-system of E; ::_thesis: for s, t, u, v being Element of E ^omega st s ==>* t,S & u ==>. v,{[s,t]} holds u ==>* v,S let s, t, u, v be Element of E ^omega ; ::_thesis: ( s ==>* t,S & u ==>. v,{[s,t]} implies u ==>* v,S ) assume that A1: s ==>* t,S and A2: u ==>. v,{[s,t]} ; ::_thesis: u ==>* v,S consider u1, v1, s1, t1 being Element of E ^omega such that A3: ( u = (u1 ^ s1) ^ v1 & v = (u1 ^ t1) ^ v1 ) and A4: s1 -->. t1,{[s,t]} by A2, Def5; [s1,t1] in {[s,t]} by A4, Def4; then [s1,t1] = [s,t] by TARSKI:def_1; then ( s1 = s & t1 = t ) by XTUPLE_0:1; hence u ==>* v,S by A1, A3, Th37; ::_thesis: verum end; theorem Th45: :: REWRITE2:45 for E being set for S being semi-Thue-system of E for s, t, u, v being Element of E ^omega st s ==>* t,S & u ==>* v,S \/ {[s,t]} holds u ==>* v,S proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t, u, v being Element of E ^omega st s ==>* t,S & u ==>* v,S \/ {[s,t]} holds u ==>* v,S let S be semi-Thue-system of E; ::_thesis: for s, t, u, v being Element of E ^omega st s ==>* t,S & u ==>* v,S \/ {[s,t]} holds u ==>* v,S let s, t, u, v be Element of E ^omega ; ::_thesis: ( s ==>* t,S & u ==>* v,S \/ {[s,t]} implies u ==>* v,S ) assume that A1: s ==>* t,S and A2: u ==>* v,S \/ {[s,t]} ; ::_thesis: u ==>* v,S ==>.-relation (S \/ {[s,t]}) reduces u,v by A2, Def7; then A3: ex p2 being RedSequence of ==>.-relation (S \/ {[s,t]}) st ( p2 . 1 = u & p2 . (len p2) = v ) by REWRITE1:def_3; defpred S1[ Nat] means for p being RedSequence of ==>.-relation (S \/ {[s,t]}) for s1, t1 being Element of E ^omega st len p = \$1 & p . 1 = s1 & p . (len p) = t1 holds ex q being RedSequence of ==>.-relation S st ( q . 1 = s1 & q . (len q) = t1 ); A4: 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 A5: S1[k] ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof let p be RedSequence of ==>.-relation (S \/ {[s,t]}); ::_thesis: for s1, t1 being Element of E ^omega st len p = k + 1 & p . 1 = s1 & p . (len p) = t1 holds ex q being RedSequence of ==>.-relation S st ( q . 1 = s1 & q . (len q) = t1 ) let s1, t1 be Element of E ^omega ; ::_thesis: ( len p = k + 1 & p . 1 = s1 & p . (len p) = t1 implies ex q being RedSequence of ==>.-relation S st ( q . 1 = s1 & q . (len q) = t1 ) ) assume that A6: len p = k + 1 and A7: p . 1 = s1 and A8: p . (len p) = t1 ; ::_thesis: ex q being RedSequence of ==>.-relation S st ( q . 1 = s1 & q . (len q) = t1 ) percases ( ( not k in dom p & k + 1 in dom p ) or not k + 1 in dom p or ( k in dom p & k + 1 in dom p ) ) ; suppose ( not k in dom p & k + 1 in dom p ) ; ::_thesis: ex q being RedSequence of ==>.-relation S st ( q . 1 = s1 & q . (len q) = t1 ) then k = 0 by Th1; then p = <*s1*> by A6, A7, FINSEQ_1:40; then reconsider p = p as RedSequence of ==>.-relation S by REWRITE1:6; take p ; ::_thesis: ( p . 1 = s1 & p . (len p) = t1 ) thus ( p . 1 = s1 & p . (len p) = t1 ) by A7, A8; ::_thesis: verum end; suppose not k + 1 in dom p ; ::_thesis: ex q being RedSequence of ==>.-relation S st ( q . 1 = s1 & q . (len q) = t1 ) then 0 + 1 > k + 1 by A6, FINSEQ_3:25; hence ex q being RedSequence of ==>.-relation S st ( q . 1 = s1 & q . (len q) = t1 ) by XREAL_1:6; ::_thesis: verum end; supposeA9: ( k in dom p & k + 1 in dom p ) ; ::_thesis: ex q being RedSequence of ==>.-relation S st ( q . 1 = s1 & q . (len q) = t1 ) set w = p . k; A10: [(p . k),(p . (k + 1))] in ==>.-relation (S \/ {[s,t]}) by A9, REWRITE1:def_2; then reconsider w = p . k as Element of E ^omega by ZFMISC_1:87; A11: w ==>. t1,S \/ {[s,t]} by A6, A8, A10, Def6; A12: w ==>* t1,S proof percases ( w ==>. t1,S or w ==>. t1,{[s,t]} ) by A11, Th21; suppose w ==>. t1,S ; ::_thesis: w ==>* t1,S hence w ==>* t1,S by Th33; ::_thesis: verum end; suppose w ==>. t1,{[s,t]} ; ::_thesis: w ==>* t1,S hence w ==>* t1,S by A1, Th44; ::_thesis: verum end; end; end; ex p1 being RedSequence of ==>.-relation (S \/ {[s,t]}) st ( len p1 = k & p1 . 1 = s1 & p1 . (len p1) = w ) by A7, A9, Th4; then ex q being RedSequence of ==>.-relation S st ( q . 1 = s1 & q . (len q) = w ) by A5; then ==>.-relation S reduces s1,w by REWRITE1:def_3; then s1 ==>* w,S by Def7; then s1 ==>* t1,S by A12, Th35; then ==>.-relation S reduces s1,t1 by Def7; hence ex q being RedSequence of ==>.-relation S st ( q . 1 = s1 & q . (len q) = t1 ) by REWRITE1:def_3; ::_thesis: verum end; end; end; end; A13: S1[ 0 ] by REWRITE1:def_2; for k being Nat holds S1[k] from NAT_1:sch_2(A13, A4); then ex q being RedSequence of ==>.-relation S st ( q . 1 = u & q . (len q) = v ) by A3; then ==>.-relation S reduces u,v by REWRITE1:def_3; hence u ==>* v,S by Def7; ::_thesis: verum end; begin definition let E be set ; let S be semi-Thue-system of E; let w be Element of E ^omega ; func Lang (w,S) -> Subset of (E ^omega) equals :: REWRITE2:def 8 { s where s is Element of E ^omega : w ==>* s,S } ; coherence { s where s is Element of E ^omega : w ==>* s,S } is Subset of (E ^omega) proof set X = { s where s is Element of E ^omega : w ==>* s,S } ; { s where s is Element of E ^omega : w ==>* s,S } c= E ^omega proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { s where s is Element of E ^omega : w ==>* s,S } or x in E ^omega ) assume x in { s where s is Element of E ^omega : w ==>* s,S } ; ::_thesis: x in E ^omega then ex t being Element of E ^omega st ( t = x & w ==>* t,S ) ; hence x in E ^omega ; ::_thesis: verum end; hence { s where s is Element of E ^omega : w ==>* s,S } is Subset of (E ^omega) ; ::_thesis: verum end; end; :: deftheorem defines Lang REWRITE2:def_8_:_ for E being set for S being semi-Thue-system of E for w being Element of E ^omega holds Lang (w,S) = { s where s is Element of E ^omega : w ==>* s,S } ; theorem Th46: :: REWRITE2:46 for E being set for S being semi-Thue-system of E for s, w being Element of E ^omega holds ( s in Lang (w,S) iff w ==>* s,S ) proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, w being Element of E ^omega holds ( s in Lang (w,S) iff w ==>* s,S ) let S be semi-Thue-system of E; ::_thesis: for s, w being Element of E ^omega holds ( s in Lang (w,S) iff w ==>* s,S ) let s, w be Element of E ^omega ; ::_thesis: ( s in Lang (w,S) iff w ==>* s,S ) thus ( s in Lang (w,S) implies w ==>* s,S ) ::_thesis: ( w ==>* s,S implies s in Lang (w,S) ) proof assume s in Lang (w,S) ; ::_thesis: w ==>* s,S then ex t being Element of E ^omega st ( t = s & w ==>* t,S ) ; hence w ==>* s,S ; ::_thesis: verum end; thus ( w ==>* s,S implies s in Lang (w,S) ) ; ::_thesis: verum end; theorem Th47: :: REWRITE2:47 for E being set for S being semi-Thue-system of E for w being Element of E ^omega holds w in Lang (w,S) proof let E be set ; ::_thesis: for S being semi-Thue-system of E for w being Element of E ^omega holds w in Lang (w,S) let S be semi-Thue-system of E; ::_thesis: for w being Element of E ^omega holds w in Lang (w,S) let w be Element of E ^omega ; ::_thesis: w in Lang (w,S) w ==>* w,S by Th32; hence w in Lang (w,S) ; ::_thesis: verum end; registration let E be non empty set ; let S be semi-Thue-system of E; let w be Element of E ^omega ; cluster Lang (w,S) -> non empty ; coherence not Lang (w,S) is empty by Th47; end; theorem Th48: :: REWRITE2:48 for E being set for S, T being semi-Thue-system of E for w being Element of E ^omega st S c= T holds Lang (w,S) c= Lang (w,T) proof let E be set ; ::_thesis: for S, T being semi-Thue-system of E for w being Element of E ^omega st S c= T holds Lang (w,S) c= Lang (w,T) let S, T be semi-Thue-system of E; ::_thesis: for w being Element of E ^omega st S c= T holds Lang (w,S) c= Lang (w,T) let w be Element of E ^omega ; ::_thesis: ( S c= T implies Lang (w,S) c= Lang (w,T) ) assume A1: S c= T ; ::_thesis: Lang (w,S) c= Lang (w,T) thus for x being set st x in Lang (w,S) holds x in Lang (w,T) :: according to TARSKI:def_3 ::_thesis: verum proof let x be set ; ::_thesis: ( x in Lang (w,S) implies x in Lang (w,T) ) assume A2: x in Lang (w,S) ; ::_thesis: x in Lang (w,T) then reconsider y = x as Element of E ^omega ; w ==>* y,S by A2, Th46; then w ==>* y,T by A1, Th40; hence x in Lang (w,T) ; ::_thesis: verum end; end; theorem Th49: :: REWRITE2:49 for E being set for S being semi-Thue-system of E for w being Element of E ^omega holds Lang (w,S) = Lang (w,(S \/ (id (E ^omega)))) proof let E be set ; ::_thesis: for S being semi-Thue-system of E for w being Element of E ^omega holds Lang (w,S) = Lang (w,(S \/ (id (E ^omega)))) let S be semi-Thue-system of E; ::_thesis: for w being Element of E ^omega holds Lang (w,S) = Lang (w,(S \/ (id (E ^omega)))) let w be Element of E ^omega ; ::_thesis: Lang (w,S) = Lang (w,(S \/ (id (E ^omega)))) A1: Lang (w,(S \/ (id (E ^omega)))) c= Lang (w,S) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lang (w,(S \/ (id (E ^omega)))) or x in Lang (w,S) ) assume A2: x in Lang (w,(S \/ (id (E ^omega)))) ; ::_thesis: x in Lang (w,S) then reconsider s = x as Element of E ^omega ; w ==>* s,S \/ (id (E ^omega)) by A2, Th46; then w ==>* s,S by Th41; hence x in Lang (w,S) ; ::_thesis: verum end; Lang (w,S) c= Lang (w,(S \/ (id (E ^omega)))) by Th48, XBOOLE_1:7; hence Lang (w,S) = Lang (w,(S \/ (id (E ^omega)))) by A1, XBOOLE_0:def_10; ::_thesis: verum end; theorem Th50: :: REWRITE2:50 for E being set for w being Element of E ^omega holds Lang (w,({} ((E ^omega),(E ^omega)))) = {w} proof let E be set ; ::_thesis: for w being Element of E ^omega holds Lang (w,({} ((E ^omega),(E ^omega)))) = {w} let w be Element of E ^omega ; ::_thesis: Lang (w,({} ((E ^omega),(E ^omega)))) = {w} now__::_thesis:_for_x_being_set_st_x_<>_w_holds_ not_x_in_Lang_(w,({}_((E_^omega),(E_^omega)))) let x be set ; ::_thesis: ( x <> w implies not x in Lang (w,({} ((E ^omega),(E ^omega)))) ) assume that A1: x <> w and A2: x in Lang (w,({} ((E ^omega),(E ^omega)))) ; ::_thesis: contradiction reconsider t = x as Element of E ^omega by A2; w ==>* t, {} ((E ^omega),(E ^omega)) by A2, Th46; hence contradiction by A1, Th42; ::_thesis: verum end; then for x being set holds ( x in Lang (w,({} ((E ^omega),(E ^omega)))) iff x = w ) by Th47; hence Lang (w,({} ((E ^omega),(E ^omega)))) = {w} by TARSKI:def_1; ::_thesis: verum end; theorem :: REWRITE2:51 for E being set for w being Element of E ^omega holds Lang (w,(id (E ^omega))) = {w} proof let E be set ; ::_thesis: for w being Element of E ^omega holds Lang (w,(id (E ^omega))) = {w} let w be Element of E ^omega ; ::_thesis: Lang (w,(id (E ^omega))) = {w} ({} ((E ^omega),(E ^omega))) \/ (id (E ^omega)) = {} \/ (id (E ^omega)) by PARTIT_2:def_1 .= id (E ^omega) ; hence Lang (w,(id (E ^omega))) = Lang (w,({} ((E ^omega),(E ^omega)))) by Th49 .= {w} by Th50 ; ::_thesis: verum end; begin definition let E be set ; let S, T be semi-Thue-system of E; let w be Element of E ^omega ; predS,T are_equivalent_wrt w means :Def9: :: REWRITE2:def 9 Lang (w,S) = Lang (w,T); end; :: deftheorem Def9 defines are_equivalent_wrt REWRITE2:def_9_:_ for E being set for S, T being semi-Thue-system of E for w being Element of E ^omega holds ( S,T are_equivalent_wrt w iff Lang (w,S) = Lang (w,T) ); theorem :: REWRITE2:52 for E being set for S being semi-Thue-system of E for w being Element of E ^omega holds S,S are_equivalent_wrt w proof let E be set ; ::_thesis: for S being semi-Thue-system of E for w being Element of E ^omega holds S,S are_equivalent_wrt w let S be semi-Thue-system of E; ::_thesis: for w being Element of E ^omega holds S,S are_equivalent_wrt w let w be Element of E ^omega ; ::_thesis: S,S are_equivalent_wrt w thus Lang (w,S) = Lang (w,S) ; :: according to REWRITE2:def_9 ::_thesis: verum end; theorem :: REWRITE2:53 for E being set for S, T being semi-Thue-system of E for w being Element of E ^omega st S,T are_equivalent_wrt w holds T,S are_equivalent_wrt w proof let E be set ; ::_thesis: for S, T being semi-Thue-system of E for w being Element of E ^omega st S,T are_equivalent_wrt w holds T,S are_equivalent_wrt w let S, T be semi-Thue-system of E; ::_thesis: for w being Element of E ^omega st S,T are_equivalent_wrt w holds T,S are_equivalent_wrt w let w be Element of E ^omega ; ::_thesis: ( S,T are_equivalent_wrt w implies T,S are_equivalent_wrt w ) assume Lang (w,S) = Lang (w,T) ; :: according to REWRITE2:def_9 ::_thesis: T,S are_equivalent_wrt w hence T,S are_equivalent_wrt w by Def9; ::_thesis: verum end; theorem :: REWRITE2:54 for E being set for S, T, U being semi-Thue-system of E for w being Element of E ^omega st S,T are_equivalent_wrt w & T,U are_equivalent_wrt w holds S,U are_equivalent_wrt w proof let E be set ; ::_thesis: for S, T, U being semi-Thue-system of E for w being Element of E ^omega st S,T are_equivalent_wrt w & T,U are_equivalent_wrt w holds S,U are_equivalent_wrt w let S, T, U be semi-Thue-system of E; ::_thesis: for w being Element of E ^omega st S,T are_equivalent_wrt w & T,U are_equivalent_wrt w holds S,U are_equivalent_wrt w let w be Element of E ^omega ; ::_thesis: ( S,T are_equivalent_wrt w & T,U are_equivalent_wrt w implies S,U are_equivalent_wrt w ) assume ( Lang (w,S) = Lang (w,T) & Lang (w,T) = Lang (w,U) ) ; :: according to REWRITE2:def_9 ::_thesis: S,U are_equivalent_wrt w hence S,U are_equivalent_wrt w by Def9; ::_thesis: verum end; theorem :: REWRITE2:55 for E being set for S being semi-Thue-system of E for w being Element of E ^omega holds S,S \/ (id (E ^omega)) are_equivalent_wrt w proof let E be set ; ::_thesis: for S being semi-Thue-system of E for w being Element of E ^omega holds S,S \/ (id (E ^omega)) are_equivalent_wrt w let S be semi-Thue-system of E; ::_thesis: for w being Element of E ^omega holds S,S \/ (id (E ^omega)) are_equivalent_wrt w let w be Element of E ^omega ; ::_thesis: S,S \/ (id (E ^omega)) are_equivalent_wrt w Lang (w,S) = Lang (w,(S \/ (id (E ^omega)))) by Th49; hence S,S \/ (id (E ^omega)) are_equivalent_wrt w by Def9; ::_thesis: verum end; theorem Th56: :: REWRITE2:56 for E being set for S, T, U being semi-Thue-system of E for w being Element of E ^omega st S,T are_equivalent_wrt w & S c= U & U c= T holds ( S,U are_equivalent_wrt w & U,T are_equivalent_wrt w ) proof let E be set ; ::_thesis: for S, T, U being semi-Thue-system of E for w being Element of E ^omega st S,T are_equivalent_wrt w & S c= U & U c= T holds ( S,U are_equivalent_wrt w & U,T are_equivalent_wrt w ) let S, T, U be semi-Thue-system of E; ::_thesis: for w being Element of E ^omega st S,T are_equivalent_wrt w & S c= U & U c= T holds ( S,U are_equivalent_wrt w & U,T are_equivalent_wrt w ) let w be Element of E ^omega ; ::_thesis: ( S,T are_equivalent_wrt w & S c= U & U c= T implies ( S,U are_equivalent_wrt w & U,T are_equivalent_wrt w ) ) assume that A1: Lang (w,S) = Lang (w,T) and A2: ( S c= U & U c= T ) ; :: according to REWRITE2:def_9 ::_thesis: ( S,U are_equivalent_wrt w & U,T are_equivalent_wrt w ) ( Lang (w,S) c= Lang (w,U) & Lang (w,U) c= Lang (w,T) ) by A2, Th48; hence Lang (w,S) = Lang (w,U) by A1, XBOOLE_0:def_10; :: according to REWRITE2:def_9 ::_thesis: U,T are_equivalent_wrt w hence U,T are_equivalent_wrt w by A1, Def9; ::_thesis: verum end; theorem Th57: :: REWRITE2:57 for E being set for S being semi-Thue-system of E for w being Element of E ^omega holds S, ==>.-relation S are_equivalent_wrt w proof let E be set ; ::_thesis: for S being semi-Thue-system of E for w being Element of E ^omega holds S, ==>.-relation S are_equivalent_wrt w let S be semi-Thue-system of E; ::_thesis: for w being Element of E ^omega holds S, ==>.-relation S are_equivalent_wrt w let w be Element of E ^omega ; ::_thesis: S, ==>.-relation S are_equivalent_wrt w A1: Lang (w,(==>.-relation S)) c= Lang (w,S) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lang (w,(==>.-relation S)) or x in Lang (w,S) ) assume A2: x in Lang (w,(==>.-relation S)) ; ::_thesis: x in Lang (w,S) reconsider s = x as Element of E ^omega by A2; w ==>* s, ==>.-relation S by A2, Th46; then w ==>* s,S by Th43; hence x in Lang (w,S) ; ::_thesis: verum end; Lang (w,S) c= Lang (w,(==>.-relation S)) by Th22, Th48; hence Lang (w,S) = Lang (w,(==>.-relation S)) by A1, XBOOLE_0:def_10; :: according to REWRITE2:def_9 ::_thesis: verum end; theorem Th58: :: REWRITE2:58 for E being set for S, T being semi-Thue-system of E for w, s being Element of E ^omega st S,T are_equivalent_wrt w & ==>.-relation (S \/ T) reduces w,s holds ==>.-relation S reduces w,s proof let E be set ; ::_thesis: for S, T being semi-Thue-system of E for w, s being Element of E ^omega st S,T are_equivalent_wrt w & ==>.-relation (S \/ T) reduces w,s holds ==>.-relation S reduces w,s let S, T be semi-Thue-system of E; ::_thesis: for w, s being Element of E ^omega st S,T are_equivalent_wrt w & ==>.-relation (S \/ T) reduces w,s holds ==>.-relation S reduces w,s let w, s be Element of E ^omega ; ::_thesis: ( S,T are_equivalent_wrt w & ==>.-relation (S \/ T) reduces w,s implies ==>.-relation S reduces w,s ) assume that A1: Lang (w,S) = Lang (w,T) and A2: ==>.-relation (S \/ T) reduces w,s ; :: according to REWRITE2:def_9 ::_thesis: ==>.-relation S reduces w,s A3: ex p being RedSequence of ==>.-relation (S \/ T) st ( p . 1 = w & p . (len p) = s ) by A2, REWRITE1:def_3; defpred S1[ Nat] means for p being RedSequence of ==>.-relation (S \/ T) for t being Element of E ^omega st len p = \$1 & p . 1 = w & p . (len p) = t holds ex q being RedSequence of ==>.-relation S st ( q . 1 = w & q . (len q) = t ); A4: 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 A5: S1[k] ; ::_thesis: S1[k + 1] thus S1[k + 1] ::_thesis: verum proof let p be RedSequence of ==>.-relation (S \/ T); ::_thesis: for t being Element of E ^omega st len p = k + 1 & p . 1 = w & p . (len p) = t holds ex q being RedSequence of ==>.-relation S st ( q . 1 = w & q . (len q) = t ) let t be Element of E ^omega ; ::_thesis: ( len p = k + 1 & p . 1 = w & p . (len p) = t implies ex q being RedSequence of ==>.-relation S st ( q . 1 = w & q . (len q) = t ) ) assume that A6: len p = k + 1 and A7: p . 1 = w and A8: p . (len p) = t ; ::_thesis: ex q being RedSequence of ==>.-relation S st ( q . 1 = w & q . (len q) = t ) percases ( ( not k in dom p & k + 1 in dom p ) or not k + 1 in dom p or ( k in dom p & k + 1 in dom p ) ) ; suppose ( not k in dom p & k + 1 in dom p ) ; ::_thesis: ex q being RedSequence of ==>.-relation S st ( q . 1 = w & q . (len q) = t ) then k = 0 by Th1; then p = <*w*> by A6, A7, FINSEQ_1:40; then reconsider p = p as RedSequence of ==>.-relation S by REWRITE1:6; take p ; ::_thesis: ( p . 1 = w & p . (len p) = t ) thus ( p . 1 = w & p . (len p) = t ) by A7, A8; ::_thesis: verum end; suppose not k + 1 in dom p ; ::_thesis: ex q being RedSequence of ==>.-relation S st ( q . 1 = w & q . (len q) = t ) then 0 + 1 > k + 1 by A6, FINSEQ_3:25; hence ex q being RedSequence of ==>.-relation S st ( q . 1 = w & q . (len q) = t ) by XREAL_1:6; ::_thesis: verum end; supposeA9: ( k in dom p & k + 1 in dom p ) ; ::_thesis: ex q being RedSequence of ==>.-relation S st ( q . 1 = w & q . (len q) = t ) set u = p . k; A10: [(p . k),(p . (k + 1))] in ==>.-relation (S \/ T) by A9, REWRITE1:def_2; then reconsider u = p . k as Element of E ^omega by ZFMISC_1:87; A11: u ==>. t,S \/ T by A6, A8, A10, Def6; ex p1 being RedSequence of ==>.-relation (S \/ T) st ( len p1 = k & p1 . 1 = w & p1 . (len p1) = u ) by A7, A9, Th4; then ex q being RedSequence of ==>.-relation S st ( q . 1 = w & q . (len q) = u ) by A5; then ==>.-relation S reduces w,u by REWRITE1:def_3; then A12: w ==>* u,S by Def7; percases ( u ==>. t,S or u ==>. t,T ) by A11, Th21; suppose u ==>. t,S ; ::_thesis: ex q being RedSequence of ==>.-relation S st ( q . 1 = w & q . (len q) = t ) then u ==>* t,S by Th33; then w ==>* t,S by A12, Th35; then ==>.-relation S reduces w,t by Def7; hence ex q being RedSequence of ==>.-relation S st ( q . 1 = w & q . (len q) = t ) by REWRITE1:def_3; ::_thesis: verum end; supposeA13: u ==>. t,T ; ::_thesis: ex q being RedSequence of ==>.-relation S st ( q . 1 = w & q . (len q) = t ) u in Lang (w,S) by A12; then A14: w ==>* u,T by A1, Th46; u ==>* t,T by A13, Th33; then w ==>* t,T by A14, Th35; then t in Lang (w,T) ; then w ==>* t,S by A1, Th46; then ==>.-relation S reduces w,t by Def7; hence ex q being RedSequence of ==>.-relation S st ( q . 1 = w & q . (len q) = t ) by REWRITE1:def_3; ::_thesis: verum end; end; end; end; end; end; A15: S1[ 0 ] by REWRITE1:def_2; for k being Nat holds S1[k] from NAT_1:sch_2(A15, A4); then ex q being RedSequence of ==>.-relation S st ( q . 1 = w & q . (len q) = s ) by A3; hence ==>.-relation S reduces w,s by REWRITE1:def_3; ::_thesis: verum end; theorem Th59: :: REWRITE2:59 for E being set for S, T being semi-Thue-system of E for w, s being Element of E ^omega st S,T are_equivalent_wrt w & w ==>* s,S \/ T holds w ==>* s,S proof let E be set ; ::_thesis: for S, T being semi-Thue-system of E for w, s being Element of E ^omega st S,T are_equivalent_wrt w & w ==>* s,S \/ T holds w ==>* s,S let S, T be semi-Thue-system of E; ::_thesis: for w, s being Element of E ^omega st S,T are_equivalent_wrt w & w ==>* s,S \/ T holds w ==>* s,S let w, s be Element of E ^omega ; ::_thesis: ( S,T are_equivalent_wrt w & w ==>* s,S \/ T implies w ==>* s,S ) assume that A1: S,T are_equivalent_wrt w and A2: w ==>* s,S \/ T ; ::_thesis: w ==>* s,S ==>.-relation (S \/ T) reduces w,s by A2, Def7; then ==>.-relation S reduces w,s by A1, Th58; hence w ==>* s,S by Def7; ::_thesis: verum end; theorem Th60: :: REWRITE2:60 for E being set for S, T being semi-Thue-system of E for w being Element of E ^omega st S,T are_equivalent_wrt w holds S,S \/ T are_equivalent_wrt w proof let E be set ; ::_thesis: for S, T being semi-Thue-system of E for w being Element of E ^omega st S,T are_equivalent_wrt w holds S,S \/ T are_equivalent_wrt w let S, T be semi-Thue-system of E; ::_thesis: for w being Element of E ^omega st S,T are_equivalent_wrt w holds S,S \/ T are_equivalent_wrt w let w be Element of E ^omega ; ::_thesis: ( S,T are_equivalent_wrt w implies S,S \/ T are_equivalent_wrt w ) assume A1: S,T are_equivalent_wrt w ; ::_thesis: S,S \/ T are_equivalent_wrt w A2: Lang (w,(S \/ T)) c= Lang (w,S) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lang (w,(S \/ T)) or x in Lang (w,S) ) assume A3: x in Lang (w,(S \/ T)) ; ::_thesis: x in Lang (w,S) reconsider s = x as Element of E ^omega by A3; w ==>* s,S \/ T by A3, Th46; then w ==>* s,S by A1, Th59; hence x in Lang (w,S) ; ::_thesis: verum end; Lang (w,S) c= Lang (w,(S \/ T)) by Th48, XBOOLE_1:7; hence Lang (w,S) = Lang (w,(S \/ T)) by A2, XBOOLE_0:def_10; :: according to REWRITE2:def_9 ::_thesis: verum end; theorem :: REWRITE2:61 for E being set for S being semi-Thue-system of E for s, t, w being Element of E ^omega st s ==>. t,S holds S,S \/ {[s,t]} are_equivalent_wrt w proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t, w being Element of E ^omega st s ==>. t,S holds S,S \/ {[s,t]} are_equivalent_wrt w let S be semi-Thue-system of E; ::_thesis: for s, t, w being Element of E ^omega st s ==>. t,S holds S,S \/ {[s,t]} are_equivalent_wrt w let s, t, w be Element of E ^omega ; ::_thesis: ( s ==>. t,S implies S,S \/ {[s,t]} are_equivalent_wrt w ) assume s ==>. t,S ; ::_thesis: S,S \/ {[s,t]} are_equivalent_wrt w then [s,t] in ==>.-relation S by Def6; then {[s,t]} c= ==>.-relation S by ZFMISC_1:31; then A1: S \/ {[s,t]} c= S \/ (==>.-relation S) by XBOOLE_1:9; ( S,S \/ (==>.-relation S) are_equivalent_wrt w & S c= S \/ {[s,t]} ) by Th57, Th60, XBOOLE_1:7; hence S,S \/ {[s,t]} are_equivalent_wrt w by A1, Th56; ::_thesis: verum end; theorem :: REWRITE2:62 for E being set for S being semi-Thue-system of E for s, t, w being Element of E ^omega st s ==>* t,S holds S,S \/ {[s,t]} are_equivalent_wrt w proof let E be set ; ::_thesis: for S being semi-Thue-system of E for s, t, w being Element of E ^omega st s ==>* t,S holds S,S \/ {[s,t]} are_equivalent_wrt w let S be semi-Thue-system of E; ::_thesis: for s, t, w being Element of E ^omega st s ==>* t,S holds S,S \/ {[s,t]} are_equivalent_wrt w let s, t, w be Element of E ^omega ; ::_thesis: ( s ==>* t,S implies S,S \/ {[s,t]} are_equivalent_wrt w ) assume A1: s ==>* t,S ; ::_thesis: S,S \/ {[s,t]} are_equivalent_wrt w A2: Lang (w,(S \/ {[s,t]})) c= Lang (w,S) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Lang (w,(S \/ {[s,t]})) or x in Lang (w,S) ) assume A3: x in Lang (w,(S \/ {[s,t]})) ; ::_thesis: x in Lang (w,S) reconsider u = x as Element of E ^omega by A3; w ==>* u,S \/ {[s,t]} by A3, Th46; then w ==>* u,S by A1, Th45; hence x in Lang (w,S) ; ::_thesis: verum end; Lang (w,S) c= Lang (w,(S \/ {[s,t]})) by Th48, XBOOLE_1:7; hence Lang (w,S) = Lang (w,(S \/ {[s,t]})) by A2, XBOOLE_0:def_10; :: according to REWRITE2:def_9 ::_thesis: verum end;