Termination Proof using AProVE

Term Rewriting System R:
[x, y, z]
p(s(x)) -> x
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> s(plus(p(s(x)), y))
plus(x, s(y)) -> s(plus(x, p(s(y))))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
div(div(x, y), z) -> div(x, times(y, z))
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
eq(0, 0) -> true
eq(s(x), 0) -> false
eq(0, s(y)) -> false
eq(s(x), s(y)) -> eq(x, y)
divides(y, x) -> eq(x, times(div(x, y), y))
prime(s(s(x))) -> pr(s(s(x)), s(x))
pr(x, s(0)) -> true
pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y))
if(true, x, y) -> false
if(false, x, y) -> pr(x, y)

Innermost Termination of R to be shown.

     ↳Removing Redundant Rules for Innermost Termination

Removing the following rules from R which left hand sides contain non normal subterms

div(div(x, y), z) -> div(x, times(y, z))

     ↳RRRI

       →TRS2

         ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

PLUS(s(x), y) -> PLUS(x, y)
PLUS(s(x), y) -> PLUS(p(s(x)), y)
PLUS(s(x), y) -> P(s(x))
PLUS(x, s(y)) -> PLUS(x, p(s(y)))
PLUS(x, s(y)) -> P(s(y))
TIMES(s(x), y) -> PLUS(y, times(x, y))
TIMES(s(x), y) -> TIMES(x, y)
DIV(x, y) -> QUOT(x, y, y)
QUOT(s(x), s(y), z) -> QUOT(x, y, z)
QUOT(x, 0, s(z)) -> DIV(x, s(z))
EQ(s(x), s(y)) -> EQ(x, y)
DIVIDES(y, x) -> EQ(x, times(div(x, y), y))
DIVIDES(y, x) -> TIMES(div(x, y), y)
DIVIDES(y, x) -> DIV(x, y)
PRIME(s(s(x))) -> PR(s(s(x)), s(x))
PR(x, s(s(y))) -> IF(divides(s(s(y)), x), x, s(y))
PR(x, s(s(y))) -> DIVIDES(s(s(y)), x)
IF(false, x, y) -> PR(x, y)

Furthermore, R contains five SCCs.

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳Modular Removal of Rules

           →DP Problem 2

             ↳Neg POLO

           →DP Problem 3

             ↳SCP

           →DP Problem 4

             ↳SCP

           →DP Problem 5

             ↳SCP

Dependency Pairs:

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

Rules:

p(s(x)) -> x
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> s(plus(p(s(x)), y))
plus(x, s(y)) -> s(plus(x, p(s(y))))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
eq(0, 0) -> true
eq(s(x), 0) -> false
eq(0, s(y)) -> false
eq(s(x), s(y)) -> eq(x, y)
divides(y, x) -> eq(x, times(div(x, y), y))
prime(s(s(x))) -> pr(s(s(x)), s(x))
pr(x, s(0)) -> true
pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y))
if(true, x, y) -> false
if(false, x, y) -> pr(x, y)

We have the following set of usable rules:

p(s(x)) -> 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₂)) = 1 + x₁ + x₂

POL(s(x₁)) = x₁

POL(p(x₁)) = x₁

We have the following set D of usable symbols: {PLUS, s, p}
No Dependency Pairs can be deleted.
23 non usable rules have been deleted.

The result of this processor delivers one new DP problem.

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳MRR

...

               →DP Problem 6

                 ↳Modular Removal of Rules

           →DP Problem 2

             ↳Neg POLO

           →DP Problem 3

             ↳SCP

           →DP Problem 4

             ↳SCP

           →DP Problem 5

             ↳SCP

Dependency Pairs:

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

Rule:

p(s(x)) -> x

We have the following set of usable rules:

p(s(x)) -> 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₂)) = 1 + x₁ + x₂

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

POL(p(x₁)) = x₁

We have the following set D of usable symbols: {PLUS, s, p}
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:

p(s(x)) -> x

The result of this processor delivers one new DP problem.

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳MRR

...

               →DP Problem 7

                 ↳Dependency Graph

           →DP Problem 2

             ↳Neg POLO

           →DP Problem 3

             ↳SCP

           →DP Problem 4

             ↳SCP

           →DP Problem 5

             ↳SCP

Dependency Pairs:

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

Rule:

none

Using the Dependency Graph the DP problem was split into 1 DP problems.

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳MRR

...

               →DP Problem 8

                 ↳Non-Overlappingness Check

           →DP Problem 2

             ↳Neg POLO

           →DP Problem 3

             ↳SCP

           →DP Problem 4

             ↳SCP

           →DP Problem 5

             ↳SCP

Dependency Pairs:

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

Rule:

none

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:

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳MRR

...

               →DP Problem 9

                 ↳Instantiation Transformation

           →DP Problem 2

             ↳Neg POLO

           →DP Problem 3

             ↳SCP

           →DP Problem 4

             ↳SCP

           →DP Problem 5

             ↳SCP

Dependency Pairs:

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

Rule:

none

Strategy:

innermost

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

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

one new Dependency Pair is created:

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

The transformation is resulting in no new DP problems.

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳MRR

           →DP Problem 2

             ↳Negative Polynomial Order

           →DP Problem 3

             ↳SCP

           →DP Problem 4

             ↳SCP

           →DP Problem 5

             ↳SCP

Dependency Pairs:

QUOT(x, 0, s(z)) -> DIV(x, s(z))
QUOT(s(x), s(y), z) -> QUOT(x, y, z)
DIV(x, y) -> QUOT(x, y, y)

Rules:

p(s(x)) -> x
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> s(plus(p(s(x)), y))
plus(x, s(y)) -> s(plus(x, p(s(y))))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
eq(0, 0) -> true
eq(s(x), 0) -> false
eq(0, s(y)) -> false
eq(s(x), s(y)) -> eq(x, y)
divides(y, x) -> eq(x, times(div(x, y), y))
prime(s(s(x))) -> pr(s(s(x)), s(x))
pr(x, s(0)) -> true
pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y))
if(true, x, y) -> false
if(false, x, y) -> pr(x, y)

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

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

There are no usable rules (regarding the implicit AFS).
Used ordering:
Polynomial Order with Interpretation:

POL( QUOT(x₁, ..., x₃) ) = x₁

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

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

This results in one new DP problem.

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳MRR

           →DP Problem 2

             ↳Neg POLO

...

               →DP Problem 10

                 ↳Instantiation Transformation

           →DP Problem 3

             ↳SCP

           →DP Problem 4

             ↳SCP

           →DP Problem 5

             ↳SCP

Dependency Pairs:

QUOT(x, 0, s(z)) -> DIV(x, s(z))
DIV(x, y) -> QUOT(x, y, y)

Rules:

p(s(x)) -> x
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> s(plus(p(s(x)), y))
plus(x, s(y)) -> s(plus(x, p(s(y))))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
eq(0, 0) -> true
eq(s(x), 0) -> false
eq(0, s(y)) -> false
eq(s(x), s(y)) -> eq(x, y)
divides(y, x) -> eq(x, times(div(x, y), y))
prime(s(s(x))) -> pr(s(s(x)), s(x))
pr(x, s(0)) -> true
pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y))
if(true, x, y) -> false
if(false, x, y) -> pr(x, y)

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

DIV(x, y) -> QUOT(x, y, y)

one new Dependency Pair is created:

DIV(x'', s(z'')) -> QUOT(x'', s(z''), s(z''))

The transformation is resulting in no new DP problems.

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳MRR

           →DP Problem 2

             ↳Neg POLO

           →DP Problem 3

             ↳Size-Change Principle

           →DP Problem 4

             ↳SCP

           →DP Problem 5

             ↳SCP

Dependency Pair:

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

Rules:

p(s(x)) -> x
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> s(plus(p(s(x)), y))
plus(x, s(y)) -> s(plus(x, p(s(y))))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
eq(0, 0) -> true
eq(s(x), 0) -> false
eq(0, s(y)) -> false
eq(s(x), s(y)) -> eq(x, y)
divides(y, x) -> eq(x, times(div(x, y), y))
prime(s(s(x))) -> pr(s(s(x)), s(x))
pr(x, s(0)) -> true
pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y))
if(true, x, y) -> false
if(false, x, y) -> pr(x, y)

We number the DPs as follows:

EQ(s(x), s(y)) -> EQ(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

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.

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳MRR

           →DP Problem 2

             ↳Neg POLO

           →DP Problem 3

             ↳SCP

           →DP Problem 4

             ↳Size-Change Principle

           →DP Problem 5

             ↳SCP

Dependency Pair:

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

Rules:

p(s(x)) -> x
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> s(plus(p(s(x)), y))
plus(x, s(y)) -> s(plus(x, p(s(y))))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
eq(0, 0) -> true
eq(s(x), 0) -> false
eq(0, s(y)) -> false
eq(s(x), s(y)) -> eq(x, y)
divides(y, x) -> eq(x, times(div(x, y), y))
prime(s(s(x))) -> pr(s(s(x)), s(x))
pr(x, s(0)) -> true
pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y))
if(true, x, y) -> false
if(false, x, y) -> pr(x, y)

We number the DPs as follows:

TIMES(s(x), y) -> TIMES(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

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.

     ↳RRRI

       →TRS2

         ↳DPs

           →DP Problem 1

             ↳MRR

           →DP Problem 2

             ↳Neg POLO

           →DP Problem 3

             ↳SCP

           →DP Problem 4

             ↳SCP

           →DP Problem 5

             ↳Size-Change Principle

Dependency Pairs:

IF(false, x, y) -> PR(x, y)
PR(x, s(s(y))) -> IF(divides(s(s(y)), x), x, s(y))

Rules:

p(s(x)) -> x
plus(x, 0) -> x
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
plus(s(x), y) -> s(plus(p(s(x)), y))
plus(x, s(y)) -> s(plus(x, p(s(y))))
times(0, y) -> 0
times(s(0), y) -> y
times(s(x), y) -> plus(y, times(x, y))
div(0, y) -> 0
div(x, y) -> quot(x, y, y)
quot(0, s(y), z) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(div(x, s(z)))
eq(0, 0) -> true
eq(s(x), 0) -> false
eq(0, s(y)) -> false
eq(s(x), s(y)) -> eq(x, y)
divides(y, x) -> eq(x, times(div(x, y), y))
prime(s(s(x))) -> pr(s(s(x)), s(x))
pr(x, s(0)) -> true
pr(x, s(s(y))) -> if(divides(s(s(y)), x), x, s(y))
if(true, x, y) -> false
if(false, x, y) -> pr(x, y)

We number the DPs as follows:

IF(false, x, y) -> PR(x, y)
PR(x, s(s(y))) -> IF(divides(s(s(y)), x), x, s(y))

and get the following Size-Change Graph(s):

{1}	,	{1}
2	=	1
3	=	2

{2}	,	{2}
1	=	2
2	>	3

which lead(s) to this/these maximal multigraph(s):

{2}	,	{1}
1	=	1
2	>	2

{1}	,	{2}
2	=	2
3	>	3

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.

Innermost Termination of R successfully shown.
Duration:
0:02 minutes

POL(PLUS(x₁, x₂))	= 1 + x₁ + x₂
POL(s(x₁))	= x₁
POL(p(x₁))	= x₁