YES
(ignored inputs)COMMENT translated from Cops 83
*** Computating Strongly Quasi-Reducible Parts ***
TRS:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     d(0) -> 0,
     d(s(?x)) -> s(s(d(?x))),
     f(0) -> 0,
     f(s(?x)) -> +(+(s(?x),s(?x)),s(?x)),
     f(g(0)) -> +(+(g(0),g(0)),g(0)),
     g(?x) -> s(d(?x)) ]
Constructors: {0,s}
Defined function symbols: {+,d,f,g}
Constructor subsystem:
   [ ]
Rule part & Conj Part:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     d(0) -> 0,
     d(s(?x)) -> s(s(d(?x))),
     f(0) -> 0,
     f(s(?x)) -> +(+(s(?x),s(?x)),s(?x)),
     g(?x) -> s(d(?x)) ]
   [ f(g(0)) -> +(+(g(0),g(0)),g(0)) ]
*** Ground Confluence Check by Rewriting Induction ***
Sort: {Nat}
Signature:
   [ + : Nat,Nat -> Nat,
     0 : Nat,
     d : Nat -> Nat,
     f : Nat -> Nat,
     g : Nat -> Nat,
     s : Nat -> Nat ]
Rule Part:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     d(0) -> 0,
     d(s(?x)) -> s(s(d(?x))),
     f(0) -> 0,
     f(s(?x)) -> +(+(s(?x),s(?x)),s(?x)),
     g(?x) -> s(d(?x)) ]
Conjecture Part:
   [ f(g(0)) = +(+(g(0),g(0)),g(0)) ]
Precedence (by weight): {(+,1),(0,4),(d,2),(f,5),(g,6),(s,0)}
Rule part is confluent.
R0 is ground confluent.
Check conj part consists of inductive theorems of R0.
Rules:
   [ +(?x,0) -> ?x,
     +(?x,s(?y)) -> s(+(?x,?y)),
     d(0) -> 0,
     d(s(?x)) -> s(s(d(?x))),
     f(0) -> 0,
     f(s(?x)) -> +(+(s(?x),s(?x)),s(?x)),
     g(?x) -> s(d(?x)) ]
Conjectures:
   [ f(g(0)) = +(+(g(0),g(0)),g(0)) ]
STEP 0
ES:
   [ f(g(0)) = +(+(g(0),g(0)),g(0)) ]
HS:
   [ ]
ES0:
   [ s(s(s(0))) = s(s(s(0))) ]
HS0:
   [ ]
ES1:
   [ ]
HS1:
   [ ]
Conj part consisits of inductive theorems of R0.
examples/fromCops/cr/83.trs: Success(GCR)
(19 msec.)