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 )

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

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 Nat st i in dom (p +^ u) & i + 1 in dom (p +^ u) holds

[((p +^ u) . i),((p +^ u) . (i + 1))] in ==>.-relation S

[((p +^ u) . i),((p +^ u) . (i + 1))] in ==>.-relation S

let i be 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;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

A9: now :: thesis: for i being Nat st i in dom (u ^+ p) & i + 1 in dom (u ^+ p) holds

[((u ^+ p) . i),((u ^+ p) . (i + 1))] in ==>.-relation S

len (p +^ u) = len p
by Th5;[((u ^+ p) . i),((u ^+ p) . (i + 1))] in ==>.-relation S

let i be 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;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

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