(VAR x y z)
(RULES
  from(x) -> :(x,from(s(x)))
  sel(0,:(y,z)) -> y
  sel(s(x),:(y,z)) -> sel(x,z)
)
(COMMENT
doi:10.1007/11805618_6
[7] Example 6
submitted by: Takahito Aoto, Junichi Yoshida, and Yoshihito Toyama
)