YES(?,O(n^1)) TRS: {f c(s x, y) -> f c(x, s y), g c(x, s y) -> g c(s x, y)} DUP: We consider a non-duplicating system. Trs: {f c(s x, y) -> f c(x, s y), g c(x, s y) -> g c(s x, y)} BOUND: Bound: match(-raise)-bounded by 1 Automaton: { s_1(2) -> 2* s_1(1) -> 2* s_0(1) -> 1* c_1(2, 1) -> 4* c_1(1, 2) -> 3* c_0(1, 1) -> 1* g_1(4) -> 1* g_0(1) -> 1* f_1(3) -> 1* f_0(1) -> 1* } Strict: {} Qed