YES TRS: { h(g(x)) -> g(h(f(x))), f(a()) -> g(h(a())), k(x, h(x), a()) -> h(x), k(f(x), y, x) -> f(x)} RUF: Strict: {h(g(x)) -> g(h(f(x))), f(a()) -> g(h(a()))} Weak: {} DP: Strict: {h#(g(x)) -> h#(f(x)), h#(g(x)) -> f#(x), f#(a()) -> h#(a())} Weak: {h(g(x)) -> g(h(f(x))), f(a()) -> g(h(a()))} EDG: {(h#(g(x)) -> f#(x), f#(a()) -> h#(a())) (h#(g(x)) -> h#(f(x)), h#(g(x)) -> h#(f(x))) (h#(g(x)) -> h#(f(x)), h#(g(x)) -> f#(x))} SCCS: Scc: {h#(g(x)) -> h#(f(x))} SCC: Strict: {h#(g(x)) -> h#(f(x))} Weak: {h(g(x)) -> g(h(f(x))), f(a()) -> g(h(a()))} BOUND: Bound: match(-raise)-DP-bounded by 2 Automaton: { f_2(25) -> 26* f_1(20) -> 21* f_1(18) -> 19* f_1(16) -> 17* f_1(13) -> 14* f_0(12) -> 12* f_0(11) -> 12* f_0(9) -> 12* f_0(8) -> 12* a_1() -> 22* a_0() -> 11* h#_2(26) -> 27* h#_1(14) -> 15* h#_0(12) -> 6* h_1(22) -> 23* h_0(12) -> 9* h_0(11) -> 9* h_0(9) -> 9* h_0(8) -> 9* g_1(23) -> 24* g_0(12) -> 8* g_0(11) -> 8* g_0(9) -> 8* g_0(8) -> 8* 27 -> 15* 24 -> 19* 23 -> 25* 21 -> 14* 19 -> 14* 17 -> 14* 15 -> 6* 12 -> 20* 11 -> 18* 9 -> 16* 8 -> 13 | 12 | 9} Strict: {} Qed