YES(?,O(n^1)) TRS: {f s s x -> f f s x, f s 0() -> s 0(), f 0() -> s 0()} DUP: We consider a non-duplicating system. Trs: {f s s x -> f f s x, f s 0() -> s 0(), f 0() -> s 0()} BOUND: Bound: match(-raise)-bounded by 3 Automaton: { 0_3() -> 14* 0_2() -> 12* 0_1() -> 2* 0_0() -> 1* s_3(14) -> 15* s_2(12) -> 13* s_2(8) -> 9* s_1(16) -> 17* s_1(4) -> 5* s_1(2) -> 3* s_0(1) -> 1* f_2(18) -> 19* f_2(10) -> 11* f_2(9) -> 10* f_1(6) -> 7* f_1(5) -> 6* f_0(1) -> 1* 19 -> 6* 17 -> 6* 15 -> 19 | 11 13 -> 10 | 7 12 -> 16* 11 -> 18 | 6 7 -> 6 | 1 3 -> 6 | 1 2 -> 8* 1 -> 4* } Strict: {} Qed