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

Furthermore, R contains four SCCs.


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


Dependency Pair:

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


Rules:


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





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

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

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
Modular Removal of Rules
       →DP Problem 3
MRR
       →DP Problem 4
Neg POLO


Dependency Pairs:

MINUS(x, plus(y, z)) -> MINUS(x, y)
MINUS(x, plus(y, z)) -> MINUS(minus(x, y), z)
MINUS(s(x), s(y)) -> MINUS(p(s(x)), p(s(y)))


Rules:


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





We have the following set of usable rules:

minus(x, 0) -> x
minus(0, y) -> 0
minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(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))=  x1 + x2  
  POL(0)=  0  
  POL(MINUS(x1, x2))=  x1 + x2  
  POL(minus(x1, x2))=  x1 + x2  
  POL(s(x1))=  x1  
  POL(p(x1))=  x1  

We have the following set D of usable symbols: {0, MINUS, minus, s, p}
The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

MINUS(x, plus(y, z)) -> MINUS(x, y)
MINUS(x, plus(y, z)) -> MINUS(minus(x, y), z)

The following rules can be deleted as they contain symbols in their lhs which do not occur in D:

minus(x, plus(y, z)) -> minus(minus(x, y), z)
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
MRR
           →DP Problem 5
Modular Removal of Rules
       →DP Problem 3
MRR
       →DP Problem 4
Neg POLO


Dependency Pair:

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


Rules:


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





We have the following set of usable rules:

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

We have the following set D of usable symbols: {MINUS, s, p}
No Dependency Pairs can be deleted.
3 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
MRR
           →DP Problem 5
MRR
             ...
               →DP Problem 6
Non-Overlappingness Check
       →DP Problem 3
MRR
       →DP Problem 4
Neg POLO


Dependency Pair:

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


Rule:


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





R does not overlap into P. Moreover, R is locally confluent (all critical pairs are trivially joinable).Hence we can switch to innermost.
The transformation is resulting in one subcycle:


   R
DPs
       →DP Problem 1
SCP
       →DP Problem 2
MRR
           →DP Problem 5
MRR
             ...
               →DP Problem 7
Narrowing Transformation
       →DP Problem 3
MRR
       →DP Problem 4
Neg POLO


Dependency Pair:

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


Rule:


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


Strategy:

innermost




On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

MINUS(s(x), s(y)) -> MINUS(p(s(x)), p(s(y)))
two new Dependency Pairs are created:

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

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
SCP
       →DP Problem 2
MRR
           →DP Problem 5
MRR
             ...
               →DP Problem 8
Negative Polynomial Order
       →DP Problem 3
MRR
       →DP Problem 4
Neg POLO


Dependency Pairs:

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


Rule:


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


Strategy:

innermost




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

MINUS(s(x), s(s(x''))) -> MINUS(p(s(x)), s(p(s(x''))))


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

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


Used ordering:
Polynomial Order with Interpretation:

POL( MINUS(x1, x2) ) = max{0, x2 - 1}

POL( s(x1) ) = x1 + 1

POL( p(x1) ) = max{0, x1 - 1}


This results in one new DP problem.


   R
DPs
       →DP Problem 1
SCP
       →DP Problem 2
MRR
           →DP Problem 5
MRR
             ...
               →DP Problem 9
Negative Polynomial Order
       →DP Problem 3
MRR
       →DP Problem 4
Neg POLO


Dependency Pair:

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


Rule:


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


Strategy:

innermost




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

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


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

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


Used ordering:
Polynomial Order with Interpretation:

POL( MINUS(x1, x2) ) = x2

POL( s(x1) ) = x1 + 1

POL( p(x1) ) = max{0, x1 - 1}


This results in one new DP problem.


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


Dependency Pair:


Rule:


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


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


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


Dependency Pair:

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


Rules:


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





We have the following set of usable rules:

minus(s(x), s(y)) -> minus(p(s(x)), p(s(y)))
minus(x, 0) -> x
minus(0, y) -> 0
minus(x, plus(y, z)) -> minus(minus(x, y), z)
p(s(s(x))) -> s(p(s(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))=  x1 + x2  
  POL(plus(x1, x2))=  x1 + x2  
  POL(0)=  0  
  POL(minus(x1, x2))=  x1 + x2  
  POL(s(x1))=  x1  
  POL(p(x1))=  x1  

We have the following set D of usable symbols: {PLUS, 0, minus, s, p}
No Dependency Pairs can be deleted.
The following rules can be deleted as they contain symbols in their lhs which do not occur in D:

minus(x, plus(y, z)) -> minus(minus(x, y), z)
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
MRR
       →DP Problem 3
MRR
           →DP Problem 11
Non-Overlappingness Check
       →DP Problem 4
Neg POLO


Dependency Pair:

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


Rules:


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





R does not overlap into P. Moreover, R is locally confluent (all critical pairs are trivially joinable).Hence we can switch to innermost.
The transformation is resulting in one subcycle:


   R
DPs
       →DP Problem 1
SCP
       →DP Problem 2
MRR
       →DP Problem 3
MRR
           →DP Problem 11
NOC
             ...
               →DP Problem 12
Narrowing Transformation
       →DP Problem 4
Neg POLO


Dependency Pair:

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


Rules:


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


Strategy:

innermost




On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

PLUS(s(x), y) -> PLUS(y, minus(s(x), s(0)))
one new Dependency Pair is created:

PLUS(s(x''), y) -> PLUS(y, minus(p(s(x'')), p(s(0))))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
SCP
       →DP Problem 2
MRR
       →DP Problem 3
MRR
           →DP Problem 11
NOC
             ...
               →DP Problem 13
Usable Rules (Innermost)
       →DP Problem 4
Neg POLO


Dependency Pair:

PLUS(s(x''), y) -> PLUS(y, minus(p(s(x'')), p(s(0))))


Rules:


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


Strategy:

innermost




As we are in the innermost case, we can delete all 2 non-usable-rules.


   R
DPs
       →DP Problem 1
SCP
       →DP Problem 2
MRR
       →DP Problem 3
MRR
           →DP Problem 11
NOC
             ...
               →DP Problem 14
Negative Polynomial Order
       →DP Problem 4
Neg POLO


Dependency Pair:

PLUS(s(x''), y) -> PLUS(y, minus(p(s(x'')), p(s(0))))


Rules:


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


Strategy:

innermost




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

PLUS(s(x''), y) -> PLUS(y, minus(p(s(x'')), p(s(0))))


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

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


Used ordering:
Polynomial Order with Interpretation:

POL( PLUS(x1, x2) ) = x1 + x2

POL( s(x1) ) = 1

POL( minus(x1, x2) ) = 0

POL( 0 ) = 0

POL( p(x1) ) = 1


This results in one new DP problem.


   R
DPs
       →DP Problem 1
SCP
       →DP Problem 2
MRR
       →DP Problem 3
MRR
           →DP Problem 11
NOC
             ...
               →DP Problem 15
Dependency Graph
       →DP Problem 4
Neg POLO


Dependency Pair:


Rules:


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


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


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


Dependency Pairs:

DIV(plus(x, y), z) -> DIV(y, z)
DIV(plus(x, y), z) -> DIV(x, z)
DIV(s(x), s(y)) -> DIV(minus(x, y), s(y))


Rules:


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





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

DIV(plus(x, y), z) -> DIV(y, z)
DIV(plus(x, y), z) -> DIV(x, z)


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

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


Used ordering:
Polynomial Order with Interpretation:

POL( DIV(x1, x2) ) = x1

POL( plus(x1, x2) ) = x1 + x2 + 1

POL( s(x1) ) = x1

POL( minus(x1, x2) ) = x1

POL( 0 ) = 0

POL( p(x1) ) = 0


This results in one new DP problem.


   R
DPs
       →DP Problem 1
SCP
       →DP Problem 2
MRR
       →DP Problem 3
MRR
       →DP Problem 4
Neg POLO
           →DP Problem 16
Negative Polynomial Order


Dependency Pair:

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


Rules:


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





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

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


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

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


Used ordering:
Polynomial Order with Interpretation:

POL( DIV(x1, x2) ) = x1

POL( s(x1) ) = x1 + 1

POL( minus(x1, x2) ) = x1

POL( 0 ) = 0

POL( p(x1) ) = x1


This results in one new DP problem.


   R
DPs
       →DP Problem 1
SCP
       →DP Problem 2
MRR
       →DP Problem 3
MRR
       →DP Problem 4
Neg POLO
           →DP Problem 16
Neg POLO
             ...
               →DP Problem 17
Dependency Graph


Dependency Pair:


Rules:


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





Using the Dependency Graph resulted in no new DP problems.

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