YES TRS: rev(nil()) -> nil() rev(.(x,y)) -> ++(rev(y),.(x,nil())) car(.(x,y)) -> x cdr(.(x,y)) -> y null(nil()) -> true() null(.(x,y)) -> false() ++(nil(),y) -> y ++(.(x,y),z) -> .(x,++(y,z)) max/plus interpretations on N: rev_A(x1) = max{0, x1} rev#_A(x1) = max{0, x1} nil_A = 0 nil#_A = 0 ._A(x1,x2) = max{0, x1, x2} .#_A(x1,x2) = max{0, x1, x2} ++_A(x1,x2) = max{0, x1, x2} ++#_A(x1,x2) = max{0, x1, x2} car_A(x1) = max{0, x1} car#_A(x1) = max{0, x1} cdr_A(x1) = max{0, x1} cdr#_A(x1) = max{0, x1} null_A(x1) = max{0, x1} null#_A(x1) = max{0, x1} true_A = 0 true#_A = 0 false_A = 0 false#_A = 0 precedence: rev = car = cdr > . = ++ = false > nil > true > null