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