(VAR x y z) (RULES ge(0,0) -> true ge(s(x),0) -> ge(x,0) ge(0,s(0)) -> false ge(0,s(s(x))) -> ge(0,s(x)) ge(s(x),s(y)) -> ge(x,y) minus(0,0) -> 0 minus(0,s(x)) -> minus(0,x) minus(s(x),0) -> s(minus(x,0)) minus(s(x),s(y)) -> minus(x,y) plus(0,0) -> 0 plus(0,s(x)) -> s(plus(0,x)) plus(s(x),y) -> s(plus(x,y)) div(x,y) -> ify( ge(y,s(0)), x, y) ify( false, x, y) -> divByZeroError ify( true, x, y) -> if( ge(x,y), x, y) if ( false, x, y) -> 0 if ( true, x, y) -> s(div( minus(x,y), y)) )