YES O(n^2) TRS: { half(0()) -> 0(), half(s(s(x))) -> s(half(x)), log(s(0())) -> 0(), log(s(s(x))) -> s(log(s(half(x)))) } DUP: We consider a non-duplicating system. Trs: { half(0()) -> 0(), half(s(s(x))) -> s(half(x)), log(s(0())) -> 0(), log(s(s(x))) -> s(log(s(half(x)))) } Matrix Interpretation: Interpretation class: triangular [X1] [1 2][X1] [0] [log]([X0]) = [0 1][X0] + [0] [X1] [1 0][X1] [1] [s]([X0]) = [0 1][X0] + [2] [X1] [1 0][X1] [1] [half]([X0]) = [0 1][X0] + [0] [0] [0] = [0] Qed