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