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