YES TRS: {a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), x)))), a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))} DP: Strict: {a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))), a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))), a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))), a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))} Weak: {a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), x)))), a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))} EDG: {(a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))), a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))) (a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))), a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x)))) (a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))), a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))) (a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))), a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x)))) (a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))), a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x))))) (a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))), a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x)))) (a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))), a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x))))) (a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))), a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))))} SCCS: Scc: {a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))), a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))), a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))), a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))} SCC: Strict: {a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))), a#(f(), a(g(), a(f(), x))) -> a#(g(), a(g(), a(f(), x))), a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))), a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))} Weak: {a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), x)))), a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))} UR: {a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), x)))), a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))} BOUND: Bound: match(-raise)-DP-bounded by 0 Automaton: { b_0() -> 4* g_0() -> 2* f_0() -> 3* a#_0(2, 6) -> 1* a_0(3, 5) -> 5* a_0(3, 4) -> 5* a_0(2, 6) -> 4* a_0(2, 5) -> 6* a_0(2, 4) -> 5* 6 -> 5*} Strict: {a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))), a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))), a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))} EDG: {(a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x))), a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x))))) (a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))), a#(g(), a(f(), a(g(), x))) -> a#(f(), a(f(), a(g(), x)))) (a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))), a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))) (a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))), a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x)))))} SCCS: Scc: {a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))} Scc: {a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x))))} SCC: Strict: {a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x))))} Weak: {a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), x)))), a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))} UR: {a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), x)))), a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))} BOUND: Bound: match(-raise)-DP-bounded by 0 Automaton: { c_0() -> 4* g_0() -> 2* f_0() -> 3* a#_0(2, 7) -> 1* a_0(3, 8) -> 8* a_0(3, 6) -> 7* a_0(3, 5) -> 8 | 6 a_0(3, 4) -> 8* a_0(2, 8) -> 4* a_0(2, 4) -> 5* 4 -> 5*} Strict: {} Qed SCC: Strict: {a#(f(), a(g(), a(f(), x))) -> a#(f(), a(g(), a(g(), a(f(), x))))} Weak: {a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), x)))), a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))} UR: {a(f(), a(g(), a(f(), x))) -> a(f(), a(g(), a(g(), a(f(), x)))), a(g(), a(f(), a(g(), x))) -> a(g(), a(f(), a(f(), a(g(), x))))} BOUND: Bound: match(-raise)-DP-bounded by 1 Automaton: { d_0() -> 4* g_1() -> 9* g_0() -> 3* f_1() -> 8* f_0() -> 2* a#_1(8, 12) -> 1* a#_0(2, 7) -> 1* a_1(9, 11) -> 12* a_1(9, 10) -> 13 | 11 a_1(9, 6) -> 13* a_1(9, 5) -> 13* a_1(9, 4) -> 13* a_1(8, 13) -> 12* a_1(8, 12) -> 12 | 10 a_1(8, 7) -> 10* a_1(8, 5) -> 10* a_1(8, 4) -> 10* a_0(3, 6) -> 7* a_0(3, 5) -> 6* a_0(3, 4) -> 7* a_0(2, 7) -> 5* a_0(2, 5) -> 5* a_0(2, 4) -> 5* 6 -> 13 | 11 | 7 5 -> 12 | 10} Strict: {} Qed