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