TRS: { -(x, 0()) -> x, -(0(), s(y)) -> 0(), -(s(x), s(y)) -> -(x, y), lt(x, 0()) -> false(), lt(0(), s(y)) -> true(), lt(s(x), s(y)) -> lt(x, y), if(true(), x, y) -> x, if(false(), x, y) -> y, div(x, 0()) -> 0(), div(0(), y) -> 0(), div(s(x), s(y)) -> if(lt(x, y), 0(), s(div(-(x, y), s(y))))} Fail