Term Rewriting System R:
[x, y]
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
quot(x, s(y)) -> ifquot(le(s(y), x), x, s(y))
ifquot(true, x, y) -> s(quot(minus(x, y), y))
ifquot(false, x, y) -> 0

Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

MINUS(s(x), s(y)) -> MINUS(x, y)
LE(s(x), s(y)) -> LE(x, y)
QUOT(x, s(y)) -> IFQUOT(le(s(y), x), x, s(y))
QUOT(x, s(y)) -> LE(s(y), x)
IFQUOT(true, x, y) -> QUOT(minus(x, y), y)
IFQUOT(true, x, y) -> MINUS(x, y)

Furthermore, R contains three SCCs.


   R
DPs
       →DP Problem 1
Remaining Obligation(s)
       →DP Problem 2
Remaining Obligation(s)
       →DP Problem 3
Remaining Obligation(s)




The following remains to be proven:


   R
DPs
       →DP Problem 1
Remaining Obligation(s)
       →DP Problem 2
Remaining Obligation(s)
       →DP Problem 3
Remaining Obligation(s)




The following remains to be proven:


   R
DPs
       →DP Problem 1
Remaining Obligation(s)
       →DP Problem 2
Remaining Obligation(s)
       →DP Problem 3
Remaining Obligation(s)




The following remains to be proven:

Termination of R could not be shown.
Duration:
0:23 minutes