Term Rewriting System R:
[x, y]
p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(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:

P(p(s(x))) -> P(x)
LE(p(s(x)), x) -> LE(x, x)
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 three SCCs. 


   R
     ↳DPs
       →DP Problem 1
         ↳Argument Filtering and Ordering
       →DP Problem 2
         ↳AFS
       →DP Problem 3
         ↳Remaining


Dependency Pair:

P(p(s(x))) -> P(x)


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(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))





The following dependency pair can be strictly oriented:

P(p(s(x))) -> P(x)


The following rules can be oriented:

p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(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))


Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(P(x1))=  1 + x1  
  POL(0)=  0  
  POL(false)=  0  
  POL(true)=  0  
  POL(s(x1))=  x1  
  POL(le(x1, x2))=  x1 + x2  
  POL(p(x1))=  1 + x1  

resulting in one new DP problem.
Used Argument Filtering System:
P(x1) -> P(x1)
p(x1) -> p(x1)
s(x1) -> s(x1)
le(x1, x2) -> le(x1, x2)
minus(x1, x2) -> x2
if(x1, x2, x3) -> x3


   R
     ↳DPs
       →DP Problem 1
         ↳AFS
           →DP Problem 4
             ↳Dependency Graph
       →DP Problem 2
         ↳AFS
       →DP Problem 3
         ↳Remaining


Dependency Pair:


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(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))





Using the Dependency Graph resulted in no new DP problems.


   R
     ↳DPs
       →DP Problem 1
         ↳AFS
       →DP Problem 2
         ↳Argument Filtering and Ordering
       →DP Problem 3
         ↳Remaining


Dependency Pairs:

LE(s(x), s(y)) -> LE(x, y)
LE(p(s(x)), x) -> LE(x, x)


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(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))





The following dependency pair can be strictly oriented:

LE(p(s(x)), x) -> LE(x, x)


The following rules can be oriented:

p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(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))


Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(LE(x1, x2))=  1 + x1 + x2  
  POL(0)=  0  
  POL(false)=  0  
  POL(true)=  0  
  POL(s(x1))=  x1  
  POL(le(x1, x2))=  x1 + x2  
  POL(p(x1))=  1 + x1  

resulting in one new DP problem.
Used Argument Filtering System:
LE(x1, x2) -> LE(x1, x2)
s(x1) -> s(x1)
p(x1) -> p(x1)
le(x1, x2) -> le(x1, x2)
minus(x1, x2) -> x2
if(x1, x2, x3) -> x3


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




The following remains to be proven:


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




The following remains to be proven:

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