YES(?,O(n^1)) 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: Bound: match(-raise)-bounded by 1 Automaton: { d_1() -> 3* d_0() -> 1* b_1() -> 2* b_0() -> 1* c_1() -> 3* c_0() -> 1* a_1() -> 2* a_0() -> 1* f_1(2, 3) -> 1* f_0(1, 1) -> 1* } Strict: {} Qed