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