YES TRS: a__terms(N) -> cons(recip(a__sqr(mark(N))),terms(s(N))) a__sqr(0()) -> 0() a__sqr(s(X)) -> s(add(sqr(X),dbl(X))) a__dbl(0()) -> 0() a__dbl(s(X)) -> s(s(dbl(X))) a__add(0(),X) -> mark(X) a__add(s(X),Y) -> s(add(X,Y)) a__first(0(),X) -> nil() a__first(s(X),cons(Y,Z)) -> cons(mark(Y),first(X,Z)) mark(terms(X)) -> a__terms(mark(X)) mark(sqr(X)) -> a__sqr(mark(X)) mark(add(X1,X2)) -> a__add(mark(X1),mark(X2)) mark(dbl(X)) -> a__dbl(mark(X)) mark(first(X1,X2)) -> a__first(mark(X1),mark(X2)) mark(cons(X1,X2)) -> cons(mark(X1),X2) mark(recip(X)) -> recip(mark(X)) mark(s(X)) -> s(X) mark(0()) -> 0() mark(nil()) -> nil() a__terms(X) -> terms(X) a__sqr(X) -> sqr(X) a__add(X1,X2) -> add(X1,X2) a__dbl(X) -> dbl(X) a__first(X1,X2) -> first(X1,X2) max/plus interpretations on N: a__terms_A(x1) = max{39, 101 + x1} a__terms#_A(x1) = max{49, 33 + x1} cons_A(x1,x2) = max{39, 39 + x1, 39} cons#_A(x1,x2) = max{49, 30, 49} recip_A(x1) = max{18, 21 + x1} recip#_A(x1) = max{34, 49} a__sqr_A(x1) = max{18, 22 + x1} a__sqr#_A(x1) = max{45, 34} mark_A(x1) = max{17, 19 + x1} mark#_A(x1) = max{46, 32 + x1} terms_A(x1) = max{16, 101 + x1} terms#_A(x1) = max{31, 0} s_A(x1) = max{0, -23} s#_A(x1) = max{38, 37} 0_A = 22 0#_A = 35 add_A(x1,x2) = max{28, 12 + x1, 27 + x2} add#_A(x1,x2) = max{0, 44, 40} sqr_A(x1) = max{19, 22 + x1} sqr#_A(x1) = max{45, 34} dbl_A(x1) = max{25, 24 + x1} dbl#_A(x1) = max{45, 31} a__dbl_A(x1) = max{44, 24 + x1} a__dbl#_A(x1) = max{47, 36} a__add_A(x1,x2) = max{47, 12 + x1, 27 + x2} a__add#_A(x1,x2) = max{45, 24 + x1, 39 + x2} a__first_A(x1,x2) = max{42, 22 + x1, 19 + x2} a__first#_A(x1,x2) = max{49, 31 + x1, 10 + x2} nil_A = 43 nil#_A = 53 first_A(x1,x2) = max{23, 22 + x1, 19 + x2} first#_A(x1,x2) = max{30, 47, 49} precedence: terms > a__terms = add > a__sqr = a__first > cons = sqr = a__add = first > mark > recip = a__dbl > 0 = dbl > s = nil