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{1, x1, x2} app#_A(x1,x2) = max{1, x1, x2} nil_A = 1 nil#_A = 1 cons_A(x1) = max{1, x1} cons#_A(x1) = max{1, x1} from_A(x1) = max{2, 2 + x1} from#_A(x1) = max{2, 2 + x1} zWadr_A(x1,x2) = max{0, x1, x2} zWadr#_A(x1,x2) = max{0, x1, x2} prefix_A(x1) = max{1, x1} prefix#_A(x1) = max{1, x1} precedence: zWadr > app = prefix > nil = cons > from