YES

(VAR x0 x1 x2 x y z)
(RULES
  @(reviter(x0,x1),x2) -> reviter(x0,@(x1,x2))
  rev(x) -> reviter(x,nil())
  reviter(.(x,y),z) -> reviter(y,.(x,z))
  reviter(nil(),y) -> y
  @(@(x,y),z) -> @(x,@(y,z))
  @(.(x,y),z) -> .(x,@(y,z))
  @(nil(),y) -> y
)

(COMMENT
Termination is shown by EKBO with interpretations on natural numbers

  @_A(x1,x2) = x1 + x2
  nil_A = 0
  ._A(x1,x2) = 0
  reviter_A(x1,x2) = x2 + 1
  rev_A(x1) = 1
  @#_A(x1,x2) = 0
  nil#_A = 0
  .#_A(x1,x2) = 0

weights

  w0 = 1
  w(@) = 0
  w(nil) = 1
  w(.) = 0
  w(reviter) = 0
  w(rev) = 2

and precedence:

@ > reviter > rev > . > nil
)