YES TRS: { g(x, s(y)) -> g(f(x, y), 0()), g(0(), f(x, x)) -> x, g(f(x, y), 0()) -> f(g(x, 0()), g(y, 0())), g(s(x), y) -> g(f(x, y), 0())} RUF: Strict: {g(0(), f(x, x)) -> x, g(f(x, y), 0()) -> f(g(x, 0()), g(y, 0()))} Weak: {} DP: Strict: {g#(f(x, y), 0()) -> g#(x, 0()), g#(f(x, y), 0()) -> g#(y, 0())} Weak: {g(0(), f(x, x)) -> x, g(f(x, y), 0()) -> f(g(x, 0()), g(y, 0()))} EDG: {(g#(f(x, y), 0()) -> g#(y, 0()), g#(f(x, y), 0()) -> g#(y, 0())) (g#(f(x, y), 0()) -> g#(y, 0()), g#(f(x, y), 0()) -> g#(x, 0())) (g#(f(x, y), 0()) -> g#(x, 0()), g#(f(x, y), 0()) -> g#(x, 0())) (g#(f(x, y), 0()) -> g#(x, 0()), g#(f(x, y), 0()) -> g#(y, 0()))} SCCS: Scc: {g#(f(x, y), 0()) -> g#(x, 0()), g#(f(x, y), 0()) -> g#(y, 0())} SCC: Strict: {g#(f(x, y), 0()) -> g#(x, 0()), g#(f(x, y), 0()) -> g#(y, 0())} Weak: {g(0(), f(x, x)) -> x, g(f(x, y), 0()) -> f(g(x, 0()), g(y, 0()))} SPSC: Simple Projection: pi(g#) = 0 Strict: {g#(f(x, y), 0()) -> g#(x, 0())} EDG: {(g#(f(x, y), 0()) -> g#(x, 0()), g#(f(x, y), 0()) -> g#(x, 0()))} SCCS: Scc: {g#(f(x, y), 0()) -> g#(x, 0())} SCC: Strict: {g#(f(x, y), 0()) -> g#(x, 0())} Weak: {g(0(), f(x, x)) -> x, g(f(x, y), 0()) -> f(g(x, 0()), g(y, 0()))} SPSC: Simple Projection: pi(g#) = 0 Strict: {} Qed