Term Rewriting System R:
[x, y, z]
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(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)
QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))
QUOT(s(x), s(y)) -> MINUS(x, y)
PLUS(s(x), y) -> PLUS(x, y)
PLUS(minus(x, s(0)), minus(y, s(s(z)))) -> PLUS(minus(y, s(s(z))), minus(x, s(0)))

Furthermore, R contains three SCCs. 


   R
     ↳DPs
       →DP Problem 1
         ↳Size-Change Principle
       →DP Problem 2
         ↳Neg POLO
       →DP Problem 3
         ↳MRR


Dependency Pair:

MINUS(s(x), s(y)) -> MINUS(x, y)


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0)))





We number the DPs as follows:
  1. MINUS(s(x), s(y)) -> MINUS(x, y)
and get the following Size-Change Graph(s):
{1} , {1}
1>1
2>2

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1>1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
s(x1) -> s(x1)

We obtain no new DP problems. 


   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳Negative Polynomial Order
       →DP Problem 3
         ↳MRR


Dependency Pair:

QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0)))





The following Dependency Pair can be strictly oriented using the given order.

QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)


Used ordering:
Polynomial Order with Interpretation:

POL( QUOT(x1, x2) ) = x1

POL( s(x1) ) = x1 + 1

POL( minus(x1, x2) ) = x1


This results in one new DP problem. 


   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳Neg POLO
           →DP Problem 4
             ↳Dependency Graph
       →DP Problem 3
         ↳MRR


Dependency Pair:


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0)))





Using the Dependency Graph resulted in no new DP problems.


   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳Neg POLO
       →DP Problem 3
         ↳Modular Removal of Rules


Dependency Pairs:

PLUS(minus(x, s(0)), minus(y, s(s(z)))) -> PLUS(minus(y, s(s(z))), minus(x, s(0)))
PLUS(s(x), y) -> PLUS(x, y)


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0)))





We have the following set of usable rules:

minus(s(x), s(y)) -> minus(x, y)
minus(x, 0) -> x
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(PLUS(x1, x2))=  1 + x1 + x2  
  POL(0)=  0  
  POL(minus(x1, x2))=  1 + x1 + x2  
  POL(s(x1))=  x1  

We have the following set D of usable symbols: {PLUS, 0, minus, s}
No Dependency Pairs can be deleted.
The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

minus(x, 0) -> x
5 non usable rules have been deleted.

The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳Neg POLO
       →DP Problem 3
         ↳MRR
           →DP Problem 5
             ↳Modular Removal of Rules


Dependency Pairs:

PLUS(minus(x, s(0)), minus(y, s(s(z)))) -> PLUS(minus(y, s(s(z))), minus(x, s(0)))
PLUS(s(x), y) -> PLUS(x, y)


Rule:


minus(s(x), s(y)) -> minus(x, y)





We have the following set of usable rules:

minus(s(x), s(y)) -> minus(x, y)
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
Polynomial interpretation:
  POL(PLUS(x1, x2))=  1 + x1 + x2  
  POL(0)=  0  
  POL(minus(x1, x2))=  1 + x1 + x2  
  POL(s(x1))=  1 + x1  

We have the following set D of usable symbols: {PLUS, 0, minus, s}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

PLUS(s(x), y) -> PLUS(x, y)

The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

minus(s(x), s(y)) -> minus(x, y)


The result of this processor delivers one new DP problem.



   R
     ↳DPs
       →DP Problem 1
         ↳SCP
       →DP Problem 2
         ↳Neg POLO
       →DP Problem 3
         ↳MRR
           →DP Problem 5
             ↳MRR
             ...
               →DP Problem 6
                 ↳Dependency Graph


Dependency Pair:

PLUS(minus(x, s(0)), minus(y, s(s(z)))) -> PLUS(minus(y, s(s(z))), minus(x, s(0)))


Rule:

none





Using the Dependency Graph resulted in no new DP problems.

Termination of R successfully shown.
Duration:
0:00 minutes