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