(VAR x y)
(RULES
f(t,x,y) -> f(g(x,y),x,s(y))
g(s(x),0) -> t
g(s(x),s(y)) -> g(x,y)
)
(COMMENT coding of while x<y do y := y+1 )