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