YES O(n) TRS: {f(s(X), Y) -> h(s(f(h(Y), X)))} DUP: We consider a non-duplicating system. Trs: {f(s(X), Y) -> h(s(f(h(Y), X)))} BOUND: Automaton: { f_1(4, 3) -> 5, f_0(3, 3) -> 3, s_1(5) -> 6, s_0(3) -> 3, h_1(6) -> 3, h_1(3) -> 4, h_0(3) -> 3 } Strict: {} Qed