YES(?,O(n^1)) TRS: { f f x -> f c f x, f f x -> f d f x, g c x -> x, g c 1() -> g d 0(), g c 0() -> g d 1(), g d x -> x } DUP: We consider a non-duplicating system. Trs: { f f x -> f c f x, f f x -> f d f x, g c x -> x, g c 1() -> g d 0(), g c 0() -> g d 1(), g d x -> x } BOUND: Bound: match(-raise)-bounded by 2 Automaton: { 0_1() -> 5* 0_0() -> 1* 1_1() -> 2* 1_0() -> 1* d_2(16) -> 17* d_1(10) -> 11* d_1(2) -> 3* d_0(1) -> 1* c_2(13) -> 14* c_1(7) -> 8* c_0(1) -> 1* g_1(3) -> 4* g_0(1) -> 1* f_2(14) -> 15* f_2(12) -> 13* f_1(8) -> 9* f_1(6) -> 7* f_0(1) -> 1* 17 -> 14* 15 -> 7* 13 -> 16* 11 -> 8* 9 -> 7 | 1 8 -> 12* 7 -> 10* 5 -> 2* 4 -> 1* 2 -> 4* 1 -> 6* } Strict: {} Qed