Termination Proof using AProVE

Term Rewriting System R:
[x, y, z]
app(app(minus, x), 0) -> x
app(app(minus, app(s, x)), app(s, y)) -> app(app(minus, x), y)
app(app(quot, 0), app(s, y)) -> 0
app(app(quot, app(s, x)), app(s, y)) -> app(s, app(app(quot, app(app(minus, x), y)), app(s, y)))
app(app(plus, 0), y) -> y
app(app(plus, app(s, x)), y) -> app(s, app(app(plus, x), y))
app(app(plus, app(app(minus, x), app(s, 0))), app(app(minus, y), app(s, app(s, z)))) -> app(app(plus, app(app(minus, y), app(s, app(s, z)))), app(app(minus, x), app(s, 0)))
app(app(plus, app(app(plus, x), app(s, 0))), app(app(plus, y), app(s, app(s, z)))) -> app(app(plus, app(app(plus, y), app(s, app(s, z)))), app(app(plus, x), app(s, 0)))

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

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

Furthermore, R contains three SCCs.

     ↳DPs

       →DP Problem 1

         ↳Size-Change Principle

       →DP Problem 2

         ↳Neg POLO

       →DP Problem 3

         ↳MRR

Dependency Pair:

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

Rules:

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

The original DP problem is in applicative form. Its DPs and usable rules are the following.

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

none

It is proper and hence, it can be A-transformed which results in the DP problem

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

none

We number the DPs as follows:

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

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

         ↳Negative Polynomial Order

       →DP Problem 3

         ↳MRR

Dependency Pair:

APP(app(quot, app(s, x)), app(s, y)) -> APP(app(quot, app(app(minus, x), y)), app(s, y))

Rules:

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

The original DP problem is in applicative form. Its DPs and usable rules are the following.

APP(app(quot, app(s, x)), app(s, y)) -> APP(app(quot, app(app(minus, x), y)), app(s, y))

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

It is proper and hence, it can be A-transformed which results in the DP problem

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

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

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

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

This corresponds to the following dependency pair in applicative form:

APP(app(quot, app(s, x)), app(s, y)) -> APP(app(quot, app(app(minus, x), y)), app(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(x₁, x₂) ) = x₁

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

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

This results in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳Neg POLO

           →DP Problem 4

             ↳Dependency Graph

       →DP Problem 3

         ↳MRR

Dependency Pair:

Rules:

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

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳Neg POLO

       →DP Problem 3

         ↳Modular Removal of Rules

Dependency Pairs:

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

Rules:

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

The original DP problem is in applicative form. Its DPs and usable rules are the following.

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

It is proper and hence, it can be A-transformed which results in the DP problem

PLUS(plus(x, s(0)), plus(y, s(s(z)))) -> PLUS(plus(y, s(s(z))), plus(x, s(0)))
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)

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)))
plus(plus(x, s(0)), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0)))
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 C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

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

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

POL(0) = 0

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

POL(s(x₁)) = x₁

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

2 non usable rules have been deleted.

The result of this processor delivers one new DP problem.
Note that we keep the A-transformed DP problem as result of this processor.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳Neg POLO

       →DP Problem 3

         ↳MRR

           →DP Problem 5

             ↳Modular Removal of Rules

Dependency Pairs:

Rules:

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)))
plus(plus(x, s(0)), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0)))
minus(s(x), s(y)) -> minus(x, y)

We have the following set of usable rules:

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

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

POL(0) = 0

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

POL(s(x₁)) = x₁

plus(0, y) -> y

The result of this processor delivers one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳Neg POLO

       →DP Problem 3

         ↳MRR

           →DP Problem 5

             ↳MRR

...

               →DP Problem 6

                 ↳Modular Removal of Rules

Dependency Pairs:

Rules:

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)))
plus(plus(x, s(0)), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0)))
minus(s(x), s(y)) -> minus(x, y)

We have the following set of usable rules:

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

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

POL(0) = 0

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

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

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

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳Neg POLO

       →DP Problem 3

         ↳MRR

           →DP Problem 5

             ↳MRR

...

               →DP Problem 7

                 ↳Dependency Graph

Dependency Pairs:

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

Rules:

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)))
plus(plus(x, s(0)), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0)))

Using the Dependency Graph resulted in no new DP problems.

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

POL(PLUS(x₁, x₂))	= 1 + x₁ + x₂
POL(plus(x₁, x₂))	= x₁ + x₂
POL(0)	= 0
POL(minus(x₁, x₂))	= 1 + x₁ + x₂
POL(s(x₁))	= x₁