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))

linear polynomial interpretations on N:

  rev_A(x1) = x1 + 2
  rev#_A(x1) = x1 + 2
  nil_A = 0
  nil#_A = 0
  ._A(x1,x2) = x1 + x2 + 1
  .#_A(x1,x2) = x1 + x2 + 1
  ++_A(x1,x2) = x1 + x2
  ++#_A(x1,x2) = x1 + x2
  car_A(x1) = x1
  car#_A(x1) = x1
  cdr_A(x1) = x1
  cdr#_A(x1) = x1
  null_A(x1) = x1 + 1
  null#_A(x1) = x1 + 1
  true_A = 0
  true#_A = 0
  false_A = 0
  false#_A = 0

precedence:

  rev > ++ > . = car = cdr > nil > true = false > null