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 KBO with weight

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

and precedence:

  @ > . > rev > reviter > nil
)