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