YES

(VAR x y)
(RULES
  a(s(x),s(y)) -> a(x,a(s(x),y))
  a(s(x),z()) -> a(x,s(z()))
  a(z(),x) -> s(x)
)

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

  a_A(x1,x2) = 1
  z_A = 1
  s_A(x1) = 1
  z#_A = 0

and precedence:

a > s > z
)