(VAR Y X X1 X2 X3)
(RULES 
a__minus(0,Y) -> 0
a__minus(s(X),s(Y)) -> a__minus(X,Y)
a__geq(X,0) -> true
a__geq(0,s(Y)) -> false
a__geq(s(X),s(Y)) -> a__geq(X,Y)
a__div(0,s(Y)) -> 0
a__div(s(X),s(Y)) -> a__if(a__geq(X,Y),s(div(minus(X,Y),s(Y))),0)
a__if(true,X,Y) -> mark(X)
a__if(false,X,Y) -> mark(Y)
mark(minus(X1,X2)) -> a__minus(X1,X2)
mark(geq(X1,X2)) -> a__geq(X1,X2)
mark(div(X1,X2)) -> a__div(mark(X1),X2)
mark(if(X1,X2,X3)) -> a__if(mark(X1),X2,X3)
mark(0) -> 0
mark(s(X)) -> s(mark(X))
mark(true) -> true
mark(false) -> false
a__minus(X1,X2) -> minus(X1,X2)
a__geq(X1,X2) -> geq(X1,X2)
a__div(X1,X2) -> div(X1,X2)
a__if(X1,X2,X3) -> if(X1,X2,X3)
)