/home/nowonder/forschung/aprove/TPDB05/TRS/AProVE/IJCAR_1.trs

The program

(VAR x y z)
(RULES
  div(0,y) -> 0
  div(x,y) -> quot(x,y,y)
  quot(0,s(y),z) -> 0
  quot(s(x),s(y),z) -> quot(x,y,z)
  quot(x,0,s(z)) -> s(div(x,s(z)))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend