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