YES
(ignored inputs)COMMENT translated from Cops 169
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     *(?x,0) -> 0,
     *(?x,s(?y)) -> +(*(?x,?y),?x),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(*(?x,?y),?y),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x) ]
Constructors: {0,s}
Defined function symbols: {*,+}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(*(?x,?y),?y) ]
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     *(?x,0) -> 0,
     *(?x,s(?y)) -> +(*(?x,?y),?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x) ]
Rule part & Conj Part:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     *(?x,0) -> 0,
     *(?x,s(?y)) -> +(*(?x,?y),?x) ]
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(*(?x,?y),?y),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x) ]
Rule part & Conj Part:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(*(?x,?y),?y) ]
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     *(?x,0) -> 0,
     *(?x,s(?y)) -> +(*(?x,?y),?x),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x) ]
Rule part & Conj Part:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     *(?x,0) -> 0,
     *(?x,s(?y)) -> +(*(?x,?y),?x) ]
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(*(?x,?y),?y),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat}
Signature:
   [ * : Nat,Nat -> Nat,
     + : Nat,Nat -> Nat,
     0 : Nat,
     s : Nat -> Nat ]
Rule Part:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(*(?x,?y),?y) ]
Conjecture Part:
   [ +(?x,0) = ?x,
     +(?x,s(?y)) = s(+(?x,?y)),
     *(?x,0) = 0,
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,?y) = +(?y,?x),
     *(?x,?y) = *(?y,?x) ]
Precedence (by weight): {(*,3),(+,2),(0,1),(s,0)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ +(0,?y) -> ?y,
     +(s(?x),?y) -> s(+(?x,?y)),
     *(0,?y) -> 0,
     *(s(?x),?y) -> +(*(?x,?y),?y) ]
Conjectures:
   [ +(?x,0) = ?x,
     +(?x,s(?y)) = s(+(?x,?y)),
     *(?x,0) = 0,
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,?y) = +(?y,?x),
     *(?x,?y) = *(?y,?x) ]
STEP 0
ES:
   [ +(?x,0) = ?x,
     +(?x,s(?y)) = s(+(?x,?y)),
     *(?x,0) = 0,
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,?y) = +(?y,?x),
     *(?x,?y) = *(?y,?x) ]
HS:
   [ ]
ES0:
   [ +(?x,0) = ?x,
     +(?x,s(?y)) = s(+(?x,?y)),
     *(?x,0) = 0,
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,?y) = +(?y,?x),
     *(?x,?y) = *(?y,?x) ]
HS0:
   [ ]
ES1:
   [ +(?x,0) = ?x,
     +(?x,s(?y)) = s(+(?x,?y)),
     *(?x,0) = 0,
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,?y) = +(?y,?x),
     *(?x,?y) = *(?y,?x) ]
HS1:
   [ ]
Expand +(?x,0) = ?x
   [ 0 = 0,
     s(+(?x_2,0)) = s(?x_2) ]
ES2:
   [ 0 = 0,
     s(+(?x_2,0)) = s(?x_2),
     *(?x,?y) = *(?y,?x),
     +(?x,?y) = +(?y,?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     *(?x,0) = 0,
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS2:
   [ +(?x,0) -> ?x ]
STEP 1
ES:
   [ 0 = 0,
     s(+(?x_2,0)) = s(?x_2),
     *(?x,?y) = *(?y,?x),
     +(?x,?y) = +(?y,?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     *(?x,0) = 0,
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS:
   [ +(?x,0) -> ?x ]
ES0:
   [ 0 = 0,
     s(?x_2) = s(?x_2),
     *(?x,?y) = *(?y,?x),
     +(?x,?y) = +(?y,?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     *(?x,0) = 0,
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS0:
   [ +(?x,0) -> ?x ]
ES1:
   [ *(?x,?y) = *(?y,?x),
     +(?x,?y) = +(?y,?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     *(?x,0) = 0,
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS1:
   [ +(?x,0) -> ?x ]
Expand *(?x,0) = 0
   [ 0 = 0,
     +(*(?x_4,0),0) = 0 ]
ES2:
   [ 0 = 0,
     *(?x_4,0) = 0,
     +(?x,s(?y)) = s(+(?x,?y)),
     *(?x,?y) = *(?y,?x),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,?y) = +(?y,?x) ]
HS2:
   [ *(?x,0) -> 0,
     +(?x,0) -> ?x ]
STEP 2
ES:
   [ 0 = 0,
     *(?x_4,0) = 0,
     +(?x,s(?y)) = s(+(?x,?y)),
     *(?x,?y) = *(?y,?x),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,?y) = +(?y,?x) ]
HS:
   [ *(?x,0) -> 0,
     +(?x,0) -> ?x ]
ES0:
   [ 0 = 0,
     0 = 0,
     +(?x,s(?y)) = s(+(?x,?y)),
     *(?x,?y) = *(?y,?x),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,?y) = +(?y,?x) ]
HS0:
   [ *(?x,0) -> 0,
     +(?x,0) -> ?x ]
ES1:
   [ +(?x,s(?y)) = s(+(?x,?y)),
     *(?x,?y) = *(?y,?x),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,?y) = +(?y,?x) ]
HS1:
   [ *(?x,0) -> 0,
     +(?x,0) -> ?x ]
Expand *(?x,?y) = *(?y,?x)
   [ 0 = *(?y_3,0),
     +(*(?x_4,?y_4),?y_4) = *(?y_4,s(?x_4)) ]
ES2:
   [ 0 = *(?y_3,0),
     +(*(?x_4,?y_4),?y_4) = *(?y_4,s(?x_4)),
     +(?x,?y) = +(?y,?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS2:
   [ *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
STEP 3
ES:
   [ 0 = *(?y_3,0),
     +(*(?x_4,?y_4),?y_4) = *(?y_4,s(?x_4)),
     +(?x,?y) = +(?y,?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS:
   [ *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
ES0:
   [ 0 = 0,
     +(*(?x_4,?y_4),?y_4) = *(?y_4,s(?x_4)),
     +(?x,?y) = +(?y,?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS0:
   [ *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
ES1:
   [ +(*(?x_4,?y_4),?y_4) = *(?y_4,s(?x_4)),
     +(?x,?y) = +(?y,?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS1:
   [ *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
Expand +(?x,?y) = +(?y,?x)
   [ ?y_1 = +(?y_1,0),
     s(+(?x_2,?y_2)) = +(?y_2,s(?x_2)) ]
ES2:
   [ ?y_1 = +(?y_1,0),
     s(+(?x_2,?y_2)) = +(?y_2,s(?x_2)),
     +(?x,s(?y)) = s(+(?x,?y)),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(*(?x_4,?y_4),?y_4) = *(?y_4,s(?x_4)) ]
HS2:
   [ +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
STEP 4
ES:
   [ ?y_1 = +(?y_1,0),
     s(+(?x_2,?y_2)) = +(?y_2,s(?x_2)),
     +(?x,s(?y)) = s(+(?x,?y)),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(*(?x_4,?y_4),?y_4) = *(?y_4,s(?x_4)) ]
HS:
   [ +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
ES0:
   [ ?y_1 = ?y_1,
     s(+(?x_2,?y_2)) = +(?y_2,s(?x_2)),
     +(?x,s(?y)) = s(+(?x,?y)),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(*(?x_4,?y_4),?y_4) = *(?y_4,s(?x_4)) ]
HS0:
   [ +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
ES1:
   [ s(+(?x_2,?y_2)) = +(?y_2,s(?x_2)),
     +(?x,s(?y)) = s(+(?x,?y)),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(*(?x_4,?y_4),?y_4) = *(?y_4,s(?x_4)) ]
HS1:
   [ +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
Expand +(?y_2,s(?x_2)) = s(+(?x_2,?y_2))
   [ s(?x) = s(+(?x,0)),
     s(+(?x_2,s(?x))) = s(+(?x,s(?x_2))) ]
ES2:
   [ s(?x) = s(+(?x,0)),
     s(+(?x_2,s(?x))) = s(+(?x,s(?x_2))),
     +(*(?x_4,?y_4),?y_4) = *(?y_4,s(?x_4)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS2:
   [ +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
STEP 5
ES:
   [ s(?x) = s(+(?x,0)),
     s(+(?x_2,s(?x))) = s(+(?x,s(?x_2))),
     +(*(?x_4,?y_4),?y_4) = *(?y_4,s(?x_4)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(?x,s(?y)) = s(+(?x,?y)) ]
HS:
   [ +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
ES0:
   [ s(?x) = s(?x),
     s(s(+(?x,?x_2))) = s(s(+(?x_2,?x))),
     +(*(?x_4,?y_4),?y_4) = *(?y_4,s(?x_4)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     s(+(?y,?x)) = s(+(?x,?y)) ]
HS0:
   [ +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
ES1:
   [ +(*(?x_4,?y_4),?y_4) = *(?y_4,s(?x_4)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     *(?x,s(?y)) = +(*(?x,?y),?x) ]
HS1:
   [ +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
Expand *(?y_4,s(?x_4)) = +(*(?x_4,?y_4),?y_4)
   [ 0 = +(*(?x,0),0),
     +(*(?x_4,s(?x)),s(?x)) = +(*(?x,s(?x_4)),s(?x_4)) ]
ES2:
   [ 0 = +(*(?x,0),0),
     s(+(?x,*(?x_4,s(?x)))) = +(*(?x,s(?x_4)),s(?x_4)),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS2:
   [ *(?y_4,s(?x_4)) -> +(*(?x_4,?y_4),?y_4),
     +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
STEP 6
ES:
   [ 0 = +(*(?x,0),0),
     s(+(?x,*(?x_4,s(?x)))) = +(*(?x,s(?x_4)),s(?x_4)),
     *(?x,s(?y)) = +(*(?x,?y),?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS:
   [ *(?y_4,s(?x_4)) -> +(*(?x_4,?y_4),?y_4),
     +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
ES0:
   [ 0 = 0,
     s(+(?x,+(*(?x,?x_4),?x_4))) = s(+(?x_4,+(*(?x_4,?x),?x))),
     +(*(?y,?x),?x) = +(*(?x,?y),?x),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS0:
   [ *(?y_4,s(?x_4)) -> +(*(?x_4,?y_4),?y_4),
     +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
ES1:
   [ s(+(?x,+(*(?x,?x_4),?x_4))) = s(+(?x_4,+(*(?x_4,?x),?x))),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS1:
   [ *(?y_4,s(?x_4)) -> +(*(?x_4,?y_4),?y_4),
     +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
Expand +(+(?x,?y),?z) = +(?x,+(?y,?z))
   [ +(?y_1,?z) = +(0,+(?y_1,?z)),
     +(s(+(?x_2,?y_2)),?z) = +(s(?x_2),+(?y_2,?z)) ]
ES2:
   [ +(?y_1,?z) = +(0,+(?y_1,?z)),
     s(+(+(?x_2,?y_2),?z)) = +(s(?x_2),+(?y_2,?z)),
     s(+(?x,+(*(?x,?x_4),?x_4))) = s(+(?x_4,+(*(?x_4,?x),?x))) ]
HS2:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(?y_4,s(?x_4)) -> +(*(?x_4,?y_4),?y_4),
     +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
STEP 7
ES:
   [ +(?y_1,?z) = +(0,+(?y_1,?z)),
     s(+(+(?x_2,?y_2),?z)) = +(s(?x_2),+(?y_2,?z)),
     s(+(?x,+(*(?x,?x_4),?x_4))) = s(+(?x_4,+(*(?x_4,?x),?x))) ]
HS:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(?y_4,s(?x_4)) -> +(*(?x_4,?y_4),?y_4),
     +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
ES0:
   [ +(?y_1,?z) = +(?y_1,?z),
     s(+(+(?x_2,?y_2),?z)) = s(+(?x_2,+(?y_2,?z))),
     s(+(?x,+(*(?x,?x_4),?x_4))) = s(+(?x_4,+(*(?x_4,?x),?x))) ]
HS0:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(?y_4,s(?x_4)) -> +(*(?x_4,?y_4),?y_4),
     +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
ES1:
   [ s(+(?x,+(*(?x,?x_4),?x_4))) = s(+(?x_4,+(*(?x_4,?x),?x))) ]
HS1:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(?y_4,s(?x_4)) -> +(*(?x_4,?y_4),?y_4),
     +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
Expand s(+(?x,+(*(?x,?x_4),?x_4))) = s(+(?x_4,+(*(?x_4,?x),?x)))
   [ s(+(0,+(0,?y_7))) = s(+(?y_7,+(*(?y_7,0),0))),
     s(+(s(?x_8),+(+(*(?x_8,?y_8),?y_8),?y_8))) = s(+(?y_8,+(*(?y_8,s(?x_8)),s(?x_8)))) ]
ES2:
   [ s(?y_7) = s(+(?y_7,+(*(?y_7,0),0))),
     s(s(+(*(?x_8,?y_8),+(+(?y_8,?y_8),?x_8)))) = s(+(?y_8,+(*(?y_8,s(?x_8)),s(?x_8)))) ]
HS2:
   [ s(+(?x,+(*(?x,?x_4),?x_4))) -> s(+(?x_4,+(*(?x_4,?x),?x))),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(?y_4,s(?x_4)) -> +(*(?x_4,?y_4),?y_4),
     +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
STEP 8
ES:
   [ s(?y_7) = s(+(?y_7,+(*(?y_7,0),0))),
     s(s(+(*(?x_8,?y_8),+(+(?y_8,?y_8),?x_8)))) = s(+(?y_8,+(*(?y_8,s(?x_8)),s(?x_8)))) ]
HS:
   [ s(+(?x,+(*(?x,?x_4),?x_4))) -> s(+(?x_4,+(*(?x_4,?x),?x))),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(?y_4,s(?x_4)) -> +(*(?x_4,?y_4),?y_4),
     +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
ES0:
   [ s(?y_7) = s(?y_7),
     s(s(+(*(?x_8,?y_8),+(+(?y_8,?y_8),?x_8)))) = s(s(+(*(?x_8,?y_8),+(?y_8,+(?x_8,?y_8))))) ]
HS0:
   [ s(+(?x,+(*(?x,?x_4),?x_4))) -> s(+(?x_4,+(*(?x_4,?x),?x))),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(?y_4,s(?x_4)) -> +(*(?x_4,?y_4),?y_4),
     +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
ES1:
   [ s(s(+(*(?x_8,?y_8),+(+(?y_8,?y_8),?x_8)))) = s(s(+(*(?x_8,?y_8),+(?y_8,+(?x_8,?y_8))))) ]
HS1:
   [ s(+(?x,+(*(?x,?x_4),?x_4))) -> s(+(?x_4,+(*(?x_4,?x),?x))),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(?y_4,s(?x_4)) -> +(*(?x_4,?y_4),?y_4),
     +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
Expand s(s(+(*(?x_8,?y_8),+(+(?y_8,?y_8),?x_8)))) = s(s(+(*(?x_8,?y_8),+(?y_8,+(?x_8,?y_8)))))
   [ s(s(+(0,+(+(?y_3,?y_3),0)))) = s(s(+(*(0,?y_3),+(?y_3,+(0,?y_3))))),
     s(s(+(+(*(?x_4,?y_4),?y_4),+(+(?y_4,?y_4),s(?x_4))))) = s(s(+(*(s(?x_4),?y_4),+(?y_4,+(s(?x_4),?y_4))))) ]
ES2:
   [ s(s(+(?y_3,?y_3))) = s(s(+(*(0,?y_3),+(?y_3,+(0,?y_3))))),
     s(s(s(+(+(+(?y_4,?y_4),+(?x_4,?y_4)),*(?x_4,?y_4))))) = s(s(+(*(s(?x_4),?y_4),+(?y_4,+(s(?x_4),?y_4))))) ]
HS2:
   [ s(s(+(*(?x_8,?y_8),+(+(?y_8,?y_8),?x_8)))) -> s(s(+(*(?x_8,?y_8),+(?y_8,+(?x_8,?y_8))))),
     s(+(?x,+(*(?x,?x_4),?x_4))) -> s(+(?x_4,+(*(?x_4,?x),?x))),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(?y_4,s(?x_4)) -> +(*(?x_4,?y_4),?y_4),
     +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
STEP 9
ES:
   [ s(s(+(?y_3,?y_3))) = s(s(+(*(0,?y_3),+(?y_3,+(0,?y_3))))),
     s(s(s(+(+(+(?y_4,?y_4),+(?x_4,?y_4)),*(?x_4,?y_4))))) = s(s(+(*(s(?x_4),?y_4),+(?y_4,+(s(?x_4),?y_4))))) ]
HS:
   [ s(s(+(*(?x_8,?y_8),+(+(?y_8,?y_8),?x_8)))) -> s(s(+(*(?x_8,?y_8),+(?y_8,+(?x_8,?y_8))))),
     s(+(?x,+(*(?x,?x_4),?x_4))) -> s(+(?x_4,+(*(?x_4,?x),?x))),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(?y_4,s(?x_4)) -> +(*(?x_4,?y_4),?y_4),
     +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
ES0:
   [ s(s(+(?y_3,?y_3))) = s(s(+(?y_3,?y_3))),
     s(s(s(+(+(+(?y_4,?y_4),+(?x_4,?y_4)),*(?x_4,?y_4))))) = s(s(s(+(+(+(?x_4,?y_4),+(?y_4,?y_4)),*(?x_4,?y_4))))) ]
HS0:
   [ s(s(+(*(?x_8,?y_8),+(+(?y_8,?y_8),?x_8)))) -> s(s(+(*(?x_8,?y_8),+(?y_8,+(?x_8,?y_8))))),
     s(+(?x,+(*(?x,?x_4),?x_4))) -> s(+(?x_4,+(*(?x_4,?x),?x))),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(?y_4,s(?x_4)) -> +(*(?x_4,?y_4),?y_4),
     +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
ES1:
   [ ]
HS1:
   [ s(s(+(*(?x_8,?y_8),+(+(?y_8,?y_8),?x_8)))) -> s(s(+(*(?x_8,?y_8),+(?y_8,+(?x_8,?y_8))))),
     s(+(?x,+(*(?x,?x_4),?x_4))) -> s(+(?x_4,+(*(?x_4,?x),?x))),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     *(?y_4,s(?x_4)) -> +(*(?x_4,?y_4),?y_4),
     +(?y_2,s(?x_2)) -> s(+(?x_2,?y_2)),
     +(?x,?y) -> +(?y,?x),
     *(?x,?y) -> *(?y,?x),
     *(?x,0) -> 0,
     +(?x,0) -> ?x ]
Conj part consisits of inductive theorems of R0.
examples/fromCops/cr/169.trs: Success(GCR)
(53 msec.)