Termination Proof using AProVE

Term Rewriting System R:
[y, x, ys, xs]
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(-(x, y), s(y)))
length(nil) -> 0
length(:(x, xs)) -> s(length(xs))
hd(:(x, xs)) -> x
avg(xs) -> quot(hd(sum(xs)), length(xs))

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

+'(s(x), y) -> +'(x, y)
++'(:(x, xs), ys) -> ++'(xs, ys)
SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))
SUM(:(x, :(y, xs))) -> +'(x, y)
SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(x, :(y, ys)))))
SUM(++(xs, :(x, :(y, ys)))) -> ++'(xs, sum(:(x, :(y, ys))))
SUM(++(xs, :(x, :(y, ys)))) -> SUM(:(x, :(y, ys)))
-'(s(x), s(y)) -> -'(x, y)
QUOT(s(x), s(y)) -> QUOT(-(x, y), s(y))
QUOT(s(x), s(y)) -> -'(x, y)
LENGTH(:(x, xs)) -> LENGTH(xs)
AVG(xs) -> QUOT(hd(sum(xs)), length(xs))
AVG(xs) -> HD(sum(xs))
AVG(xs) -> SUM(xs)
AVG(xs) -> LENGTH(xs)

Furthermore, R contains seven SCCs.

     ↳DPs

       →DP Problem 1

         ↳Size-Change Principle

       →DP Problem 2

         ↳SCP

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳SCP

       →DP Problem 5

         ↳MRR

       →DP Problem 6

         ↳Neg POLO

       →DP Problem 7

         ↳MRR

Dependency Pair:

+'(s(x), y) -> +'(x, y)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(-(x, y), s(y)))
length(nil) -> 0
length(:(x, xs)) -> s(length(xs))
hd(:(x, xs)) -> x
avg(xs) -> quot(hd(sum(xs)), length(xs))

We number the DPs as follows:

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

         ↳Size-Change Principle

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳SCP

       →DP Problem 5

         ↳MRR

       →DP Problem 6

         ↳Neg POLO

       →DP Problem 7

         ↳MRR

Dependency Pair:

++'(:(x, xs), ys) -> ++'(xs, ys)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(-(x, y), s(y)))
length(nil) -> 0
length(:(x, xs)) -> s(length(xs))
hd(:(x, xs)) -> x
avg(xs) -> quot(hd(sum(xs)), length(xs))

We number the DPs as follows:

++'(:(x, xs), ys) -> ++'(xs, ys)

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:

:(x₁, x₂) -> :(x₁, x₂)

We obtain no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳SCP

       →DP Problem 3

         ↳Size-Change Principle

       →DP Problem 4

         ↳SCP

       →DP Problem 5

         ↳MRR

       →DP Problem 6

         ↳Neg POLO

       →DP Problem 7

         ↳MRR

Dependency Pair:

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

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(-(x, y), s(y)))
length(nil) -> 0
length(:(x, xs)) -> s(length(xs))
hd(:(x, xs)) -> x
avg(xs) -> quot(hd(sum(xs)), length(xs))

We number the DPs as follows:

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

         ↳SCP

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳Size-Change Principle

       →DP Problem 5

         ↳MRR

       →DP Problem 6

         ↳Neg POLO

       →DP Problem 7

         ↳MRR

Dependency Pair:

LENGTH(:(x, xs)) -> LENGTH(xs)

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(-(x, y), s(y)))
length(nil) -> 0
length(:(x, xs)) -> s(length(xs))
hd(:(x, xs)) -> x
avg(xs) -> quot(hd(sum(xs)), length(xs))

We number the DPs as follows:

LENGTH(:(x, xs)) -> LENGTH(xs)

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:

:(x₁, x₂) -> :(x₁, x₂)

We obtain no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳SCP

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳SCP

       →DP Problem 5

         ↳Modular Removal of Rules

       →DP Problem 6

         ↳Neg POLO

       →DP Problem 7

         ↳MRR

Dependency Pair:

SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(-(x, y), s(y)))
length(nil) -> 0
length(:(x, xs)) -> s(length(xs))
hd(:(x, xs)) -> x
avg(xs) -> quot(hd(sum(xs)), length(xs))

We have the following set of usable rules:

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

To remove rules and DPs from this DP problem we used the following monotonic and C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

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

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

POL(0) = 1

POL(s(x₁)) = x₁

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

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

+(0, y) -> y

14 non usable rules have been deleted.

The result of this processor delivers one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳SCP

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳SCP

       →DP Problem 5

         ↳MRR

           →DP Problem 8

             ↳Modular Removal of Rules

       →DP Problem 6

         ↳Neg POLO

       →DP Problem 7

         ↳MRR

Dependency Pair:

SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))

Rule:

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

We have the following set of usable rules:

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

To remove rules and DPs from this DP problem we used the following monotonic and C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

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

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

POL(s(x₁)) = x₁

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

We have the following set D of usable symbols: {:, SUM, s, +}
The following Dependency Pairs can be deleted as the lhs is strictly greater than the corresponding rhs:

SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳SCP

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳SCP

       →DP Problem 5

         ↳MRR

       →DP Problem 6

         ↳Negative Polynomial Order

       →DP Problem 7

         ↳MRR

Dependency Pair:

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

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(-(x, y), s(y)))
length(nil) -> 0
length(:(x, xs)) -> s(length(xs))
hd(:(x, xs)) -> x
avg(xs) -> quot(hd(sum(xs)), length(xs))

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

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

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

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

Used ordering:
Polynomial Order with Interpretation:

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

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

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

POL( 0 ) = 0

This results in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳SCP

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳SCP

       →DP Problem 5

         ↳MRR

       →DP Problem 6

         ↳Neg POLO

           →DP Problem 9

             ↳Dependency Graph

       →DP Problem 7

         ↳MRR

Dependency Pair:

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(-(x, y), s(y)))
length(nil) -> 0
length(:(x, xs)) -> s(length(xs))
hd(:(x, xs)) -> x
avg(xs) -> quot(hd(sum(xs)), length(xs))

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳SCP

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳SCP

       →DP Problem 5

         ↳MRR

       →DP Problem 6

         ↳Neg POLO

       →DP Problem 7

         ↳Modular Removal of Rules

Dependency Pair:

SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(x, :(y, ys)))))

Rules:

+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(-(x, y), s(y)))
length(nil) -> 0
length(:(x, xs)) -> s(length(xs))
hd(:(x, xs)) -> x
avg(xs) -> quot(hd(sum(xs)), length(xs))

We have the following set of usable rules:

++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(:(x, nil)) -> :(x, nil)
+(0, y) -> y
+(s(x), y) -> s(+(x, y))

To remove rules and DPs from this DP problem we used the following monotonic and C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

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

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

POL(0) = 1

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

POL(nil) = 0

POL(sum(x₁)) = x₁

POL(s(x₁)) = x₁

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

We have the following set D of usable symbols: {:, SUM, ++, nil, s, sum, +}
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:

+(0, y) -> y

10 non usable rules have been deleted.

The result of this processor delivers one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳SCP

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳SCP

       →DP Problem 5

         ↳MRR

       →DP Problem 6

         ↳Neg POLO

       →DP Problem 7

         ↳MRR

           →DP Problem 10

             ↳Modular Removal of Rules

Dependency Pair:

SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(x, :(y, ys)))))

Rules:

++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(:(x, nil)) -> :(x, nil)
+(s(x), y) -> s(+(x, y))

We have the following set of usable rules:

++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(:(x, nil)) -> :(x, nil)
+(s(x), y) -> s(+(x, y))

To remove rules and DPs from this DP problem we used the following monotonic and C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

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

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

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

POL(nil) = 0

POL(sum(x₁)) = x₁

POL(s(x₁)) = x₁

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

We have the following set D of usable symbols: {:, SUM, ++, nil, s, sum, +}
No Dependency Pairs can be deleted.
The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

++(nil, ys) -> ys

The result of this processor delivers one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳SCP

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳SCP

       →DP Problem 5

         ↳MRR

       →DP Problem 6

         ↳Neg POLO

       →DP Problem 7

         ↳MRR

           →DP Problem 10

             ↳MRR

...

               →DP Problem 11

                 ↳Modular Removal of Rules

Dependency Pair:

SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(x, :(y, ys)))))

Rules:

++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(:(x, nil)) -> :(x, nil)
+(s(x), y) -> s(+(x, y))

We have the following set of usable rules:

++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(:(x, nil)) -> :(x, nil)
+(s(x), y) -> s(+(x, y))

To remove rules and DPs from this DP problem we used the following monotonic and C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

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

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

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

POL(nil) = 0

POL(sum(x₁)) = x₁

POL(s(x₁)) = x₁

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

sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))

The result of this processor delivers one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳SCP

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳SCP

       →DP Problem 5

         ↳MRR

       →DP Problem 6

         ↳Neg POLO

       →DP Problem 7

         ↳MRR

           →DP Problem 10

             ↳MRR

...

               →DP Problem 12

                 ↳Modular Removal of Rules

Dependency Pair:

SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(x, :(y, ys)))))

Rules:

++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
+(s(x), y) -> s(+(x, y))

We have the following set of usable rules:

++(:(x, xs), ys) -> :(x, ++(xs, ys))

To remove rules and DPs from this DP problem we used the following monotonic and C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

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

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

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

POL(sum(x₁)) = x₁

We have the following set D of usable symbols: {:, SUM, ++, sum}
No Dependency Pairs can be deleted.
2 non usable rules have been deleted.

The result of this processor delivers one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳SCP

       →DP Problem 2

         ↳SCP

       →DP Problem 3

         ↳SCP

       →DP Problem 4

         ↳SCP

       →DP Problem 5

         ↳MRR

       →DP Problem 6

         ↳Neg POLO

       →DP Problem 7

         ↳MRR

           →DP Problem 10

             ↳MRR

...

               →DP Problem 13

                 ↳Narrowing Transformation

Dependency Pair:

SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(x, :(y, ys)))))

Rule:

++(:(x, xs), ys) -> :(x, ++(xs, ys))

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

SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(x, :(y, ys)))))

one new Dependency Pair is created:

SUM(++(:(x'', xs''), :(x0, :(y', ys'')))) -> SUM(:(x'', ++(xs'', sum(:(x0, :(y', ys''))))))

The transformation is resulting in no new DP problems.

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

POL(:(x₁, x₂))	= x₁ + x₂
POL(SUM(x₁))	= 1 + x₁
POL(0)	= 1
POL(s(x₁))	= x₁
POL(+(x₁, x₂))	= x₁ + x₂

POL(:(x₁, x₂))	= 1 + x₁ + x₂
POL(SUM(x₁))	= 1 + x₁
POL(s(x₁))	= x₁
POL(+(x₁, x₂))	= x₁ + x₂