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))))} BOUND: Bound: match(-raise)-DP-bounded by 0 Automaton: { g_0() -> 11* f_0() -> 10* a#_0(10, 14) -> 5* a_0(14, 14) -> 9* a_0(14, 13) -> 9* a_0(14, 12) -> 9* a_0(14, 11) -> 9* a_0(14, 10) -> 9* a_0(14, 9) -> 9* a_0(13, 14) -> 9* a_0(13, 13) -> 9* a_0(13, 12) -> 9* a_0(13, 11) -> 9* a_0(13, 10) -> 9* a_0(13, 9) -> 9* a_0(12, 14) -> 9* a_0(12, 13) -> 9* a_0(12, 12) -> 9* a_0(12, 11) -> 9* a_0(12, 10) -> 9* a_0(12, 9) -> 9* a_0(11, 14) -> 9* a_0(11, 13) -> 14* a_0(11, 12) -> 13* a_0(11, 11) -> 9* a_0(11, 10) -> 9* a_0(11, 9) -> 9* a_0(10, 14) -> 12* a_0(10, 13) -> 12* a_0(10, 12) -> 12* a_0(10, 11) -> 12* a_0(10, 10) -> 12* a_0(10, 9) -> 12* a_0(9, 14) -> 9* a_0(9, 13) -> 9* a_0(9, 12) -> 9* a_0(9, 11) -> 9* a_0(9, 10) -> 9* a_0(9, 9) -> 9*} Strict: {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))))} EDG: {(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#(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#(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#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), x)))))} SCCS: Scc: {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#(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))))} BOUND: Bound: match(-raise)-DP-bounded by 0 Automaton: { g_0() -> 10* f_0() -> 9* a#_0(10, 12) -> 5* a_0(12, 12) -> 8* a_0(12, 11) -> 8* a_0(12, 10) -> 8* a_0(12, 9) -> 8* a_0(12, 8) -> 8* a_0(11, 12) -> 8* a_0(11, 11) -> 8* a_0(11, 10) -> 8* a_0(11, 9) -> 8* a_0(11, 8) -> 8* a_0(10, 12) -> 8* a_0(10, 11) -> 12* a_0(10, 10) -> 8* a_0(10, 9) -> 8* a_0(10, 8) -> 8* a_0(9, 12) -> 11* a_0(9, 11) -> 11* a_0(9, 10) -> 11* a_0(9, 9) -> 11* a_0(9, 8) -> 11* a_0(8, 12) -> 8* a_0(8, 11) -> 8* a_0(8, 10) -> 8* a_0(8, 9) -> 8* a_0(8, 8) -> 8*} Strict: {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#(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))))} SCCS: Scc: {a#(g(), a(f(), a(g(), x))) -> a#(g(), a(f(), a(f(), a(g(), 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))))} BOUND: Bound: match(-raise)-DP-bounded by 0 Automaton: { g_0() -> 11* f_0() -> 10* a#_0(11, 14) -> 5* a_0(14, 14) -> 9* a_0(14, 13) -> 9* a_0(14, 12) -> 9* a_0(14, 11) -> 9* a_0(14, 10) -> 9* a_0(14, 9) -> 9* a_0(13, 14) -> 9* a_0(13, 13) -> 9* a_0(13, 12) -> 9* a_0(13, 11) -> 9* a_0(13, 10) -> 9* a_0(13, 9) -> 9* a_0(12, 14) -> 9* a_0(12, 13) -> 9* a_0(12, 12) -> 9* a_0(12, 11) -> 9* a_0(12, 10) -> 9* a_0(12, 9) -> 9* a_0(11, 14) -> 12* a_0(11, 13) -> 12* a_0(11, 12) -> 12* a_0(11, 11) -> 12* a_0(11, 10) -> 12* a_0(11, 9) -> 12* a_0(10, 14) -> 9* a_0(10, 13) -> 14* a_0(10, 12) -> 13* a_0(10, 11) -> 9* a_0(10, 10) -> 9* a_0(10, 9) -> 9* a_0(9, 14) -> 9* a_0(9, 13) -> 9* a_0(9, 12) -> 9* a_0(9, 11) -> 9* a_0(9, 10) -> 9* a_0(9, 9) -> 9*} Strict: {} Qed