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