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