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