YES TRS: terms(N) -> cons(recip(sqr(N))) sqr(0()) -> 0() sqr(s(X)) -> s(add(sqr(X),dbl(X))) dbl(0()) -> 0() dbl(s(X)) -> s(s(dbl(X))) add(0(),X) -> X add(s(X),Y) -> s(add(X,Y)) first(0(),X) -> nil() first(s(X),cons(Y)) -> cons(Y) max/plus interpretations on N: terms_A(x1) = max{4, 3 + x1} terms#_A(x1) = max{5, 6} cons_A(x1) = max{1, 2 + x1} cons#_A(x1) = max{6, -1} recip_A(x1) = max{2, 1} recip#_A(x1) = max{6, 4} sqr_A(x1) = max{3, -1 + x1} sqr#_A(x1) = max{4, 0} 0_A = 2 0#_A = 2 s_A(x1) = max{3, 2} s#_A(x1) = max{0, -1} add_A(x1,x2) = max{2, 3, 1 + x2} add#_A(x1,x2) = max{4, 1, 4} dbl_A(x1) = max{3, 1} dbl#_A(x1) = max{1, 3} first_A(x1,x2) = max{2, 0, x2} first#_A(x1,x2) = max{7, 0, x2} nil_A = 2 nil#_A = 1 precedence: terms = first > cons = recip = sqr > dbl > 0 = s > add = nil