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