YES TRS: { a__f(X, X) -> a__f(a(), b()), a__f(X1, X2) -> f(X1, X2), a__b() -> a(), a__b() -> b(), mark(a()) -> a(), mark(b()) -> a__b(), mark(f(X1, X2)) -> a__f(mark(X1), X2)} DP: Strict: { a__f#(X, X) -> a__f#(a(), b()), mark#(b()) -> a__b#(), mark#(f(X1, X2)) -> a__f#(mark(X1), X2), mark#(f(X1, X2)) -> mark#(X1)} Weak: { a__f(X, X) -> a__f(a(), b()), a__f(X1, X2) -> f(X1, X2), a__b() -> a(), a__b() -> b(), mark(a()) -> a(), mark(b()) -> a__b(), mark(f(X1, X2)) -> a__f(mark(X1), X2)} EDG: {(mark#(f(X1, X2)) -> mark#(X1), mark#(f(X1, X2)) -> mark#(X1)) (mark#(f(X1, X2)) -> mark#(X1), mark#(f(X1, X2)) -> a__f#(mark(X1), X2)) (mark#(f(X1, X2)) -> mark#(X1), mark#(b()) -> a__b#()) (mark#(f(X1, X2)) -> a__f#(mark(X1), X2), a__f#(X, X) -> a__f#(a(), b()))} SCCS: Scc: {mark#(f(X1, X2)) -> mark#(X1)} SCC: Strict: {mark#(f(X1, X2)) -> mark#(X1)} Weak: { a__f(X, X) -> a__f(a(), b()), a__f(X1, X2) -> f(X1, X2), a__b() -> a(), a__b() -> b(), mark(a()) -> a(), mark(b()) -> a__b(), mark(f(X1, X2)) -> a__f(mark(X1), X2)} SPSC: Simple Projection: pi(mark#) = 0 Strict: {} Qed