YES

TRS:

  rev(nil()) -> nil()
  rev(rev(x)) -> x
  rev(++(x,y)) -> ++(rev(y),rev(x))
  ++(nil(),y) -> y
  ++(x,nil()) -> x
  ++(.(x,y),z) -> .(x,++(y,z))
  ++(x,++(y,z)) -> ++(++(x,y),z)
  make(x) -> .(x,nil())

linear polynomial interpretations on N:

  rev_A(x1) = x1
  rev#_A(x1) = x1 + 2
  nil_A = 1
  nil#_A = 0
  ++_A(x1,x2) = x1 + x2 + 1
  ++#_A(x1,x2) = x2 + 1
  ._A(x1,x2) = x1 + 1
  .#_A(x1,x2) = 0
  make_A(x1) = x1 + 1
  make#_A(x1) = x1 + 1

precedence:

  ++ > rev = make > nil = .