YES TRS: first(0(),X) -> nil() first(s(X),cons(Y)) -> cons(Y) from(X) -> cons(X) max/plus interpretations on N: first_A(x1,x2) = max{2, -1 + x1, 1} first#_A(x1,x2) = max{0, -1 + x1, 0} 0_A = 1 0#_A = 2 nil_A = 2 nil#_A = 1 s_A(x1) = max{1, -1} s#_A(x1) = max{0, 0} cons_A(x1) = max{2, 1} cons#_A(x1) = max{1, 2} from_A(x1) = max{0, 2} from#_A(x1) = max{3, 3} precedence: first = s = from > nil = cons > 0