YES O(n) TRS: { f(x, x) -> a(), f(g(x), y) -> f(x, y)} DUP: We consider a non-duplicating system. Trs: { f(x, x) -> a(), f(g(x), y) -> f(x, y)} BOUND: Automaton: { g_0(4) -> 4, g_0(3) -> 4, f_1(4, 4) -> 3, f_1(4, 3) -> 3, f_1(3, 4) -> 3, f_1(3, 3) -> 3, f_0(4, 4) -> 3, f_0(4, 3) -> 3, f_0(3, 4) -> 3, f_0(3, 3) -> 3, a_2() -> 3, a_1() -> 3, a_0() -> 3 } Strict: {} Qed