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