YES TRS: {h(f(x, y)) -> f(f(a(), h(h(y))), x)} DP: Strict: {h#(f(x, y)) -> h#(y), h#(f(x, y)) -> h#(h(y))} Weak: {h(f(x, y)) -> f(f(a(), h(h(y))), x)} EDG: {(h#(f(x, y)) -> h#(h(y)), h#(f(x, y)) -> h#(h(y))) (h#(f(x, y)) -> h#(h(y)), h#(f(x, y)) -> h#(y)) (h#(f(x, y)) -> h#(y), h#(f(x, y)) -> h#(y)) (h#(f(x, y)) -> h#(y), h#(f(x, y)) -> h#(h(y)))} SCCS: Scc: {h#(f(x, y)) -> h#(y), h#(f(x, y)) -> h#(h(y))} SCC: Strict: {h#(f(x, y)) -> h#(y), h#(f(x, y)) -> h#(h(y))} Weak: {h(f(x, y)) -> f(f(a(), h(h(y))), x)} BOUND: Bound: match(-raise)-DP-bounded by 1 Automaton: { b_0() -> 2* h#_1(7) -> 1* h#_1(2) -> 1* h#_0(3) -> 1* h#_0(2) -> 1* h_1(2) -> 7* h_0(3) -> 5* h_0(2) -> 3* a_0() -> 4* f_0(6, 6) -> 5* f_0(6, 2) -> 3* f_0(4, 5) -> 6* 3 -> 7*} Strict: {h#(f(x, y)) -> h#(y)} EDG: {(h#(f(x, y)) -> h#(y), h#(f(x, y)) -> h#(y))} SCCS: Scc: {h#(f(x, y)) -> h#(y)} SCC: Strict: {h#(f(x, y)) -> h#(y)} Weak: {h(f(x, y)) -> f(f(a(), h(h(y))), x)} SPSC: Simple Projection: pi(h#) = 0 Strict: {} Qed