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