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