YES O(n) TRS: {h(x, x) -> x, f(x, y) -> h(x, y), f(x, y) -> h(y, x)} DUP: We consider a non-duplicating system. Trs: {h(x, x) -> x, f(x, y) -> h(x, y), f(x, y) -> h(y, x)} BOUND: Automaton: {f_0(2, 2) -> 2, h_1(2, 2) -> 2, h_0(2, 2) -> 2} Strict: {} Qed