YES TRS: {f(g(x), g(y)) -> f(p(f(g(x), s(y))), g(s(p(x)))), p(0()) -> g(0()), g(s(p(x))) -> p(x)} DP: Strict: {f#(g(x), g(y)) -> f#(p(f(g(x), s(y))), g(s(p(x)))), f#(g(x), g(y)) -> f#(g(x), s(y)), f#(g(x), g(y)) -> p#(x), f#(g(x), g(y)) -> p#(f(g(x), s(y))), f#(g(x), g(y)) -> g#(s(p(x))), p#(0()) -> g#(0())} Weak: {f(g(x), g(y)) -> f(p(f(g(x), s(y))), g(s(p(x)))), p(0()) -> g(0()), g(s(p(x))) -> p(x)} EDG: {(f#(g(x), g(y)) -> p#(x), p#(0()) -> g#(0()))} SCCS: Qed