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