YES TRS: { a(x, g()) -> a(f(), a(g(), a(f(), x))), a(f(), a(f(), x)) -> a(x, g())} DP: Strict: { a#(x, g()) -> a#(g(), a(f(), x)), a#(x, g()) -> a#(f(), x), a#(x, g()) -> a#(f(), a(g(), a(f(), x))), a#(f(), a(f(), x)) -> a#(x, g())} Weak: { a(x, g()) -> a(f(), a(g(), a(f(), x))), a(f(), a(f(), x)) -> a(x, g())} EDG: {(a#(f(), a(f(), x)) -> a#(x, g()), a#(x, g()) -> a#(f(), a(g(), a(f(), x)))) (a#(f(), a(f(), x)) -> a#(x, g()), a#(x, g()) -> a#(f(), x)) (a#(f(), a(f(), x)) -> a#(x, g()), a#(x, g()) -> a#(g(), a(f(), x))) (a#(x, g()) -> a#(f(), x), a#(f(), a(f(), x)) -> a#(x, g())) (a#(x, g()) -> a#(f(), x), a#(x, g()) -> a#(f(), a(g(), a(f(), x)))) (a#(x, g()) -> a#(f(), x), a#(x, g()) -> a#(f(), x)) (a#(x, g()) -> a#(f(), x), a#(x, g()) -> a#(g(), a(f(), x))) (a#(x, g()) -> a#(f(), a(g(), a(f(), x))), a#(f(), a(f(), x)) -> a#(x, g()))} SCCS: Scc: { a#(x, g()) -> a#(f(), x), a#(x, g()) -> a#(f(), a(g(), a(f(), x))), a#(f(), a(f(), x)) -> a#(x, g())} SCC: Strict: { a#(x, g()) -> a#(f(), x), a#(x, g()) -> a#(f(), a(g(), a(f(), x))), a#(f(), a(f(), x)) -> a#(x, g())} Weak: { a(x, g()) -> a(f(), a(g(), a(f(), x))), a(f(), a(f(), x)) -> a(x, g())} BOUND: Bound: match(-raise)-bounded by 4 Automaton: { f_4() -> 16* f_3() -> 11* f_2() -> 7* f_1() -> 3* f_0() -> 1* g_4() -> 17* g_3() -> 10* g_2() -> 6* g_1() -> 2* g_0() -> 1* a#_4(16, 21) -> 1* a#_4(16, 19) -> 1* a#_4(16, 9) -> 1* a#_3(21, 10) -> 1* a#_3(11, 21) -> 1* a#_3(11, 15) -> 1* a#_3(11, 11) -> 1* a#_3(11, 9) -> 1* a#_3(11, 7) -> 1* a#_3(11, 6) -> 1* a#_3(11, 5) -> 1* a#_3(11, 3) -> 1* a#_3(11, 2) -> 1* a#_3(9, 10) -> 1* a#_2(21, 6) -> 1* a#_2(9, 6) -> 1* a#_2(7, 23) -> 1* a#_2(7, 21) -> 1* a#_2(7, 11) -> 1* a#_2(7, 9) -> 1* a#_2(7, 7) -> 1* a#_2(7, 6) -> 1* a#_2(7, 5) -> 1* a#_2(7, 3) -> 1* a#_2(7, 2) -> 1* a#_2(7, 1) -> 1* a#_2(6, 6) -> 1* a#_2(5, 6) -> 1* a#_2(3, 6) -> 1* a#_2(2, 6) -> 1* a#_1(21, 2) -> 1* a#_1(9, 2) -> 1* a#_1(6, 2) -> 1* a#_1(5, 2) -> 1* a#_1(3, 13) -> 1* a#_1(3, 7) -> 1* a#_1(3, 5) -> 1* a#_1(3, 3) -> 1* a#_1(3, 2) -> 1* a#_1(3, 1) -> 1* a#_1(2, 2) -> 1* a#_1(1, 2) -> 1* a#_0(1, 1) -> 1* a_4(17, 18) -> 19* a_4(16, 21) -> 18* a_4(16, 19) -> 8* a_4(16, 9) -> 18* a_3(21, 10) -> 8* a_3(11, 21) -> 14 | 8 | 4 | 1 a_3(11, 15) -> 8 | 4 a_3(11, 11) -> 24* a_3(11, 9) -> 14* a_3(11, 7) -> 20* a_3(11, 6) -> 20* a_3(11, 5) -> 14* a_3(11, 3) -> 20* a_3(11, 2) -> 14* a_3(10, 24) -> 7* a_3(10, 20) -> 21* a_3(10, 14) -> 15* a_3(9, 10) -> 8* a_2(21, 6) -> 4* a_2(9, 6) -> 4* a_2(7, 23) -> 14* a_2(7, 21) -> 8* a_2(7, 11) -> 22* a_2(7, 9) -> 8 | 4 | 1 a_2(7, 7) -> 8* a_2(7, 6) -> 8* a_2(7, 5) -> 8* a_2(7, 3) -> 8* a_2(7, 2) -> 8* a_2(7, 1) -> 8* a_2(6, 22) -> 23* a_2(6, 8) -> 9* a_2(6, 6) -> 8 | 4 a_2(5, 6) -> 8 | 4 a_2(3, 6) -> 14 | 8 | 4 | 1 a_2(2, 6) -> 8 | 4 a_1(21, 2) -> 1* a_1(9, 2) -> 1* a_1(6, 2) -> 1* a_1(5, 2) -> 1* a_1(3, 13) -> 8* a_1(3, 7) -> 12* a_1(3, 5) -> 1* a_1(3, 3) -> 2* a_1(3, 2) -> 8 | 4 | 1 a_1(3, 1) -> 4* a_1(2, 12) -> 13* a_1(2, 4) -> 5* a_1(2, 2) -> 8 | 4 | 1 a_1(1, 2) -> 8 | 4 | 1 a_0(1, 1) -> 1*} Strict: {} Qed