YES Time: 0.000883 TRS: { f(x, 0()) -> s 0(), f(s x, s y) -> s f(x, y), g(0(), x) -> g(f(x, x), x)} DP: DP: {f#(s x, s y) -> f#(x, y), g#(0(), x) -> f#(x, x), g#(0(), x) -> g#(f(x, x), x)} TRS: { 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 (1): Scc: {f#(s x, s y) -> f#(x, y)} SCC (1): 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#) = 1 Strict: {} Qed