(VAR x y)
(RULES
cond1(true,x,y) -> cond2(gr(y,0),x,y)
cond2(true,x,y) -> cond2(gr(y,0),p(x),p(y))
cond2(false,x,y) -> cond1(and(eq(x,y),gr(x,0)),x,y)
gr(0,x) -> false
gr(s(x),0) -> true
gr(s(x),s(y)) -> gr(x,y)
p(0) -> 0
p(s(x)) -> x
eq(0,0) -> true
eq(s(x),0) -> false
eq(0,s(x)) -> false
eq(s(x),s(y)) -> eq(x,y)
and(true,true) -> true
and(false,x) -> false
and(x,false) -> false
)
(COMMENT
while and(eq(x,y),gr(x,0))
do
  while gr(y,0)
  do
    y:=p(y)
    x:=p(x)
  od;
od
)