YES TRS: from(X) -> cons(X,n__from(s(X))) sel(0(),cons(X,Y)) -> X sel(s(X),cons(Y,Z)) -> sel(X,activate(Z)) from(X) -> n__from(X) activate(n__from(X)) -> from(X) activate(X) -> X max/plus interpretations on N: from_A(x1) = max{4, 1 + x1} from#_A(x1) = max{1, 3} cons_A(x1,x2) = max{4, 1 + x1, 2 + x2} cons#_A(x1,x2) = max{2, 3, 2} n__from_A(x1) = max{2, 1 + x1} n__from#_A(x1) = max{0, 1} s_A(x1) = max{1, 1} s#_A(x1) = max{3, 0} sel_A(x1,x2) = max{4, 0, -1 + x2} sel#_A(x1,x2) = max{5, 8, 6} 0_A = 0 0#_A = 0 activate_A(x1) = max{5, 1 + x1} activate#_A(x1) = max{7, 4} precedence: from > cons = n__from = s = sel = 0 > activate