YES TRS: app(nil(),YS) -> YS app(cons(X),YS) -> cons(X) from(X) -> cons(X) zWadr(nil(),YS) -> nil() zWadr(XS,nil()) -> nil() zWadr(cons(X),cons(Y)) -> cons(app(Y,cons(X))) prefix(L) -> cons(nil()) max/plus interpretations on N: app_A(x1,x2) = max{5, 1 + x1, x2} app#_A(x1,x2) = max{0, 0, 7 + x2} nil_A = 2 nil#_A = 7 cons_A(x1) = max{4, -1 + x1} cons#_A(x1) = max{7, 2} from_A(x1) = max{4, x1} from#_A(x1) = max{7, 3} zWadr_A(x1,x2) = max{2, -1 + x1, 1 + x2} zWadr#_A(x1,x2) = max{1, 13 + x1, 4 + x2} prefix_A(x1) = max{4, 0} prefix#_A(x1) = max{8, 1} precedence: zWadr > app = from = prefix > nil = cons