Termination Proof using AProVE

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.

     ↳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.

     ↳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:

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

D_P: empty set
Oriented Rules: none

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

trivial

with Argument Filtering System:

s(x₁) -> s(x₁)

We obtain no new DP problems.

     ↳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 C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

POL(plus(x₁, x₂)) = x₁ + x₂

POL(0) = 0

POL(MINUS(x₁, x₂)) = x₁ + x₂

POL(minus(x₁, x₂)) = x₁ + x₂

POL(s(x₁)) = x₁

POL(p(x₁)) = x₁

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.

     ↳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 C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

POL(MINUS(x₁, x₂)) = x₁ + x₂

POL(s(x₁)) = x₁

POL(p(x₁)) = x₁

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.

     ↳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:

     ↳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:

     ↳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(x₁, x₂) ) = max{0, x₂ - 1}

POL( s(x₁) ) = x₁ + 1

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

This results in one new DP problem.

     ↳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(x₁, x₂) ) = x₂

POL( s(x₁) ) = x₁ + 1

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

This results in one new DP problem.

     ↳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.

     ↳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 C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

POL(PLUS(x₁, x₂)) = x₁ + x₂

POL(plus(x₁, x₂)) = x₁ + x₂

POL(0) = 0

POL(minus(x₁, x₂)) = x₁ + x₂

POL(s(x₁)) = x₁

POL(p(x₁)) = x₁

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.

     ↳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:

     ↳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:

     ↳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.

     ↳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(x₁, x₂) ) = x₁ + x₂

POL( s(x₁) ) = 1

POL( minus(x₁, x₂) ) = 0

POL( 0 ) = 0

POL( p(x₁) ) = 1

This results in one new DP problem.

     ↳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.

     ↳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(x₁, x₂) ) = x₁

POL( plus(x₁, x₂) ) = x₁ + x₂ + 1

POL( s(x₁) ) = x₁

POL( minus(x₁, x₂) ) = x₁

POL( 0 ) = 0

POL( p(x₁) ) = 0

This results in one new DP problem.

     ↳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(x₁, x₂) ) = x₁

POL( s(x₁) ) = x₁ + 1

POL( minus(x₁, x₂) ) = x₁

POL( 0 ) = 0

POL( p(x₁) ) = x₁

This results in one new DP problem.

     ↳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

POL(plus(x₁, x₂))	= x₁ + x₂
POL(0)	= 0
POL(MINUS(x₁, x₂))	= x₁ + x₂
POL(minus(x₁, x₂))	= x₁ + x₂
POL(s(x₁))	= x₁
POL(p(x₁))	= x₁