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

Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

LE(s(x), s(y)) -> LE(x, y)
MINUS(x, y) -> IF(le(x, y), x, y)
MINUS(x, y) -> LE(x, y)
IF(false, x, y) -> MINUS(p(x), y)
IF(false, x, y) -> P(x)

Furthermore, R contains two SCCs. 


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




The following remains to be proven:


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




The following remains to be proven:

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