(VAR x y z u v)

(DATATYPES
   a = < div'(c,c) >
   b = µX. < nil, app(c,X) >
   c = µX. < 0, s(X), mult(X,X), minus(X,X) >
 )

(SIGNATURES
   div :: c x c -> c
   h :: c x c x c -> c
   egypt :: a -> b
   i :: a x a -> a
 )


(RULES
  div(x, y) -> h(x, y, y)

  egypt(div'(0, y))    -> nil
  egypt(div'(s(x), y)) -> app(div(y, s(x)),  egypt(i(div'(s(x), y), div'(s(0), div(y, s(x))))))

  h(s(0), y, z)	         -> s(0)
  h(s(s(x)), s(0), z)	 -> s(h(s(x), z, z))
  h(s(s(x)), s(s(y)), z) -> h(s(x), s(y), z)

  i(div'(x, y),  div'(u, v)) -> div'(minus(mult(x, v), mult(y, u)), mult(y, v))
)