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, x1} terms#_A(x1) = max{0, x1} cons_A(x1) = max{0, x1} cons#_A(x1) = max{0, x1} recip_A(x1) = max{0, x1} recip#_A(x1) = max{0, x1} sqr_A(x1) = max{0, x1} sqr#_A(x1) = max{0, x1} 0_A = 0 0#_A = 0 s_A = 0 s#_A = 0 dbl_A(x1) = max{0, x1} dbl#_A(x1) = max{0, x1} add_A(x1,x2) = max{0, x1, x2} add#_A(x1,x2) = max{0, x1, x2} first_A(x1,x2) = max{0, x1, x2} first#_A(x1,x2) = max{0, x1, x2} nil_A = 0 nil#_A = 0 precedence: terms = first = nil > cons = recip = sqr > 0 > dbl > s = add