(VAR x y)
(RULES
cond1(true,x,y) -> cond2(gr(x,y),x,y)
cond2(true,x,y) -> cond1(neq(x,0),y,y)
cond2(false,x,y) -> cond1(neq(x,0),p(x),y)
gr(0,x) -> false
gr(s(x),0) -> true
gr(s(x),s(y)) -> gr(x,y)
neq(0,0) -> false
neq(0,s(x)) -> true
neq(s(x),0) -> true
neq(s(x),s(y)) -> neq(x,y)
p(0) -> 0
p(s(x)) -> x
)
(COMMENT
while neq(x,0)
do
  if gr(x,y) then x:=y
	     else x:=p(x)
  fi
od
)