YES O(n) TRS: {f(a(), b()) -> f(a(), c()), f(c(), d()) -> f(b(), d())} DUP: We consider a non-duplicating system. Trs: {f(a(), b()) -> f(a(), c()), f(c(), d()) -> f(b(), d())} BOUND: Automaton: { d_1() -> 7, d_0() -> 5, b_1() -> 6, b_0() -> 5, c_1() -> 7, c_0() -> 5, a_1() -> 6, a_0() -> 5, f_1(6, 7) -> 5, f_0(5, 5) -> 5 } Strict: {} Qed