YES(?,O(n^1)) TRS: {f a() -> f b(), g b() -> g a()} DUP: We consider a non-duplicating system. Trs: {f a() -> f b(), g b() -> g a()} BOUND: Bound: match(-raise)-bounded by 1 Automaton: { a_1() -> 4* a_0() -> 1* b_1() -> 2* b_0() -> 1* g_1(4) -> 5* g_0(1) -> 1* f_1(2) -> 3* f_0(1) -> 1* 5 -> 1* 3 -> 1* } Strict: {} Qed