YES
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ +(0,?y) -> ?y,
     +(s(0),?y) -> s(?y),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     s(s(?x)) -> s(?x),
     s(?x) -> s(s(?x)) ]
Constructors: {0,s}
Defined function symbols: {+}
Constructor subsystem:
   [ s(s(?x)) -> s(?x) ]
Rule part & Conj Part:
   [ s(s(?x)) -> s(?x),
     +(0,?y) -> ?y,
     +(s(0),?y) -> s(?y) ]
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?x,?y) -> +(?y,?x),
     s(?x) -> s(s(?x)) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat}
Signature:
   [ + : Nat,Nat -> Nat,
     0 : Nat,
     s : Nat -> Nat ]
Rule Part:
   [ s(s(?x)) -> s(?x),
     +(0,?y) -> ?y,
     +(s(0),?y) -> s(?y) ]
Conjecture Part:
   [ +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,?y) = +(?y,?x),
     s(?x) = s(s(?x)) ]
Precedence (by weight): {(+,3),(0,1),(s,0)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ s(s(?x)) -> s(?x),
     +(0,?y) -> ?y,
     +(s(0),?y) -> s(?y) ]
Conjectures:
   [ +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,?y) = +(?y,?x),
     s(?x) = s(s(?x)) ]
STEP 0
ES:
   [ +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,?y) = +(?y,?x),
     s(?x) = s(s(?x)) ]
HS:
   [ ]
ES0:
   [ +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,?y) = +(?y,?x),
     s(?x) = s(?x) ]
HS0:
   [ ]
ES1:
   [ +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     +(?x,?y) = +(?y,?x) ]
HS1:
   [ ]
Expand +(?x,?y) = +(?y,?x)
   [ ?y_2 = +(?y_2,0),
     s(?y_3) = +(?y_3,s(0)),
     +(s(?x_5),?x_4) = +(?x_4,s(s(?x_5))) ]
ES2:
   [ ?y_2 = +(?y_2,0),
     s(?y_3) = +(?y_3,s(0)),
     +(s(?x_5),?x_4) = +(?x_4,s(s(?x_5))),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS2:
   [ +(?x,?y) -> +(?y,?x) ]
STEP 1
ES:
   [ ?y_2 = +(?y_2,0),
     s(?y_3) = +(?y_3,s(0)),
     +(s(?x_5),?x_4) = +(?x_4,s(s(?x_5))),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS:
   [ +(?x,?y) -> +(?y,?x) ]
ES0:
   [ ?y_2 = +(?y_2,0),
     s(?y_3) = +(?y_3,s(0)),
     +(s(?x_5),?x_4) = +(?x_4,s(?x_5)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS0:
   [ +(?x,?y) -> +(?y,?x) ]
ES1:
   [ ?y_2 = +(?y_2,0),
     s(?y_3) = +(?y_3,s(0)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS1:
   [ +(?x,?y) -> +(?y,?x) ]
Expand +(?y_2,0) = ?y_2
   [ 0 = 0,
     s(0) = s(0),
     +(s(?x_5),0) = s(s(?x_5)) ]
ES2:
   [ 0 = 0,
     s(0) = s(0),
     +(s(?x_5),0) = s(s(?x_5)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     s(?y_3) = +(?y_3,s(0)) ]
HS2:
   [ +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
STEP 2
ES:
   [ 0 = 0,
     s(0) = s(0),
     +(s(?x_5),0) = s(s(?x_5)),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     s(?y_3) = +(?y_3,s(0)) ]
HS:
   [ +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
ES0:
   [ 0 = 0,
     s(0) = s(0),
     s(?x_5) = s(?x_5),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     s(?y_3) = +(?y_3,s(0)) ]
HS0:
   [ +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
ES1:
   [ +(+(?x,?y),?z) = +(?x,+(?y,?z)),
     s(?y_3) = +(?y_3,s(0)) ]
HS1:
   [ +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
Expand +(?y_3,s(0)) = s(?y_3)
   [ s(0) = s(0),
     s(s(0)) = s(s(0)),
     +(s(?x_5),s(0)) = s(s(s(?x_5))) ]
ES2:
   [ s(0) = s(0),
     s(0) = s(s(0)),
     +(s(?x_5),s(0)) = s(s(s(?x_5))),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS2:
   [ +(?y_3,s(0)) -> s(?y_3),
     +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
STEP 3
ES:
   [ s(0) = s(0),
     s(0) = s(s(0)),
     +(s(?x_5),s(0)) = s(s(s(?x_5))),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS:
   [ +(?y_3,s(0)) -> s(?y_3),
     +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
ES0:
   [ s(0) = s(0),
     s(0) = s(0),
     s(?x_5) = s(?x_5),
     +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS0:
   [ +(?y_3,s(0)) -> s(?y_3),
     +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
ES1:
   [ +(+(?x,?y),?z) = +(?x,+(?y,?z)) ]
HS1:
   [ +(?y_3,s(0)) -> s(?y_3),
     +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
Expand +(+(?x,?y),?z) = +(?x,+(?y,?z))
   [ +(?y_2,?z) = +(0,+(?y_2,?z)),
     +(s(?y_3),?z) = +(s(0),+(?y_3,?z)),
     +(+(s(?x_5),?x_4),?z) = +(s(s(?x_5)),+(?x_4,?z)) ]
ES2:
   [ +(?y_2,?z) = +(0,+(?y_2,?z)),
     +(s(?y_3),?z) = +(s(0),+(?y_3,?z)),
     +(+(s(?x_5),?x_4),?z) = +(s(s(?x_5)),+(?x_4,?z)) ]
HS2:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y_3,s(0)) -> s(?y_3),
     +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
STEP 4
ES:
   [ +(?y_2,?z) = +(0,+(?y_2,?z)),
     +(s(?y_3),?z) = +(s(0),+(?y_3,?z)),
     +(+(s(?x_5),?x_4),?z) = +(s(s(?x_5)),+(?x_4,?z)) ]
HS:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y_3,s(0)) -> s(?y_3),
     +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
ES0:
   [ +(?y_2,?z) = +(?y_2,?z),
     +(s(?y_3),?z) = s(+(?y_3,?z)),
     +(+(s(?x_5),?x_4),?z) = +(s(?x_5),+(?x_4,?z)) ]
HS0:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y_3,s(0)) -> s(?y_3),
     +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
ES1:
   [ +(s(?y_3),?z) = s(+(?y_3,?z)) ]
HS1:
   [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y_3,s(0)) -> s(?y_3),
     +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
Expand +(s(?y_3),?z) = s(+(?y_3,?z))
   [ s(?y_6) = s(+(0,?y_6)),
     +(s(?x_8),?x_7) = s(+(s(?x_8),?x_7)),
     +(s(?y_3),s(?x_11)) = s(+(?y_3,s(s(?x_11)))) ]
ES2:
   [ s(?y_6) = s(+(0,?y_6)),
     +(s(?x_8),?x_7) = s(+(s(?x_8),?x_7)),
     +(s(?y_3),s(?x_11)) = s(+(?y_3,s(s(?x_11)))) ]
HS2:
   [ +(s(?y_3),?z) -> s(+(?y_3,?z)),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y_3,s(0)) -> s(?y_3),
     +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
STEP 5
ES:
   [ s(?y_6) = s(+(0,?y_6)),
     +(s(?x_8),?x_7) = s(+(s(?x_8),?x_7)),
     +(s(?y_3),s(?x_11)) = s(+(?y_3,s(s(?x_11)))) ]
HS:
   [ +(s(?y_3),?z) -> s(+(?y_3,?z)),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y_3,s(0)) -> s(?y_3),
     +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
ES0:
   [ s(?y_6) = s(?y_6),
     s(+(?x_8,?x_7)) = s(+(?x_8,?x_7)),
     s(+(?x_11,?y_3)) = s(+(?y_3,s(?x_11))) ]
HS0:
   [ +(s(?y_3),?z) -> s(+(?y_3,?z)),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y_3,s(0)) -> s(?y_3),
     +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
ES1:
   [ s(+(?x_11,?y_3)) = s(+(?y_3,s(?x_11))) ]
HS1:
   [ +(s(?y_3),?z) -> s(+(?y_3,?z)),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y_3,s(0)) -> s(?y_3),
     +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
Expand s(+(?y_3,s(?x_11))) = s(+(?x_11,?y_3))
   [ s(s(?x_8)) = s(+(?x_8,0)),
     s(s(s(?x_8))) = s(+(?x_8,s(0))),
     s(+(s(?x_13),s(?x_8))) = s(+(?x_8,s(s(?x_13)))) ]
ES2:
   [ s(?x_8) = s(+(?x_8,0)),
     s(?x_8) = s(+(?x_8,s(0))),
     s(+(?x_8,?x_13)) = s(+(?x_8,s(s(?x_13)))) ]
HS2:
   [ s(+(?y_3,s(?x_11))) -> s(+(?x_11,?y_3)),
     +(s(?y_3),?z) -> s(+(?y_3,?z)),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y_3,s(0)) -> s(?y_3),
     +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
STEP 6
ES:
   [ s(?x_8) = s(+(?x_8,0)),
     s(?x_8) = s(+(?x_8,s(0))),
     s(+(?x_8,?x_13)) = s(+(?x_8,s(s(?x_13)))) ]
HS:
   [ s(+(?y_3,s(?x_11))) -> s(+(?x_11,?y_3)),
     +(s(?y_3),?z) -> s(+(?y_3,?z)),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y_3,s(0)) -> s(?y_3),
     +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
ES0:
   [ s(?x_8) = s(?x_8),
     s(?x_8) = s(?x_8),
     s(+(?x_8,?x_13)) = s(+(?x_13,?x_8)) ]
HS0:
   [ s(+(?y_3,s(?x_11))) -> s(+(?x_11,?y_3)),
     +(s(?y_3),?z) -> s(+(?y_3,?z)),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y_3,s(0)) -> s(?y_3),
     +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
ES1:
   [ ]
HS1:
   [ s(+(?y_3,s(?x_11))) -> s(+(?x_11,?y_3)),
     +(s(?y_3),?z) -> s(+(?y_3,?z)),
     +(+(?x,?y),?z) -> +(?x,+(?y,?z)),
     +(?y_3,s(0)) -> s(?y_3),
     +(?y_2,0) -> ?y_2,
     +(?x,?y) -> +(?y,?x) ]
Conj part consisits of inductive theorems of R0.
examples/additions/plus14.trs: Success(GCR)
(10 msec.)