(COMMENT numbers is similar to digits, unless that the bound if by far larger, so while it may be
  possible to narrow 10 steps, it is not possible to narrow "nr"-steps
)
(VAR x y)
(RULES
 numbers -> d(0)
 d(x) -> if(le(x,nr),x)
 if(true,x) -> cons(x,d(s(x)))
 if(false,x) -> nil

 le(0,y) -> true
 le(s(x),0) -> false
 le(s(x),s(y)) -> le(x,y)

 nr -> ack(s(s(s(s(s(s(0)))))),0)
 ack(0,x) -> s(x)
 ack(s(x),0) -> ack(x,s(0))
 ack(s(x),s(y)) -> ack(x,ack(s(x),y))
)