YES O(n) 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: Automaton: { f_2(34) -> 35, f_2(22) -> 23, f_2(21) -> 22, f_1(10) -> 11, f_1(9) -> 10, f_0(3) -> 3, 0_3() -> 36, 0_2() -> 24, 0_1() -> 4, 0_0() -> 3, s_3(36) -> 37, s_2(24) -> 25, s_2(20) -> 21, s_1(30) -> 31, s_1(8) -> 9, s_1(4) -> 5, s_0(3) -> 3, 37 -> 35 | 23, 35 -> 10, 31 -> 10, 25 -> 22 | 11, 24 -> 30, 23 -> 34 | 10, 11 -> 10 | 3, 5 -> 10 | 3, 4 -> 20, 3 -> 8 } Strict: {} Qed