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), g s f x -> g f x} 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), g s f x -> g f x } BOUND: Bound: match(-raise)-bounded by 1 Automaton: { s_1(3) -> 3* s_1(1) -> 3* s_0(1) -> 1* c_1(3, 1) -> 2* c_1(1, 3) -> 4* c_0(1, 1) -> 1* g_1(2) -> 1* g_1(1) -> 1* g_0(1) -> 1* f_1(4) -> 2 | 1 f_1(1) -> 2* f_0(1) -> 1* } Strict: {} Qed