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