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))

Innermost 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

         ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳Nar

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))

Strategy:

innermost

The following dependency pair can be strictly oriented:

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

There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:

+'(x₁, x₂) -> +'(x₁, x₂)
s(x₁) -> s(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 8

             ↳Dependency Graph

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳Nar

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))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Argument Filtering and Ordering

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳Nar

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))

Strategy:

innermost

The following dependency pair can be strictly oriented:

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

There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:

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

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

           →DP Problem 9

             ↳Dependency Graph

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳Nar

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))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Argument Filtering and Ordering

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳Nar

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))

Strategy:

innermost

The following dependency pair can be strictly oriented:

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

There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:

-'(x₁, x₂) -> -'(x₁, x₂)
s(x₁) -> s(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

           →DP Problem 10

             ↳Dependency Graph

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳Nar

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))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳Argument Filtering and Ordering

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳Nar

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))

Strategy:

innermost

The following dependency pair can be strictly oriented:

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

There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:

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

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

           →DP Problem 11

             ↳Dependency Graph

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳Nar

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))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳Argument Filtering and Ordering

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳Nar

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))

Strategy:

innermost

The following dependency pair can be strictly oriented:

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

The following usable rules for innermost can be oriented:

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

Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:

SUM(x₁) -> SUM(x₁)
:(x₁, x₂) -> :(x₁, x₂)
+(x₁, x₂) -> x₂
s(x₁) -> x₁

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

           →DP Problem 12

             ↳Dependency Graph

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳Nar

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))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳Argument Filtering and Ordering

       →DP Problem 7

         ↳Nar

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))

Strategy:

innermost

The following dependency pair can be strictly oriented:

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

The following usable rules for innermost can be oriented:

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

Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:

QUOT(x₁, x₂) -> QUOT(x₁, x₂)
s(x₁) -> s(x₁)
-(x₁, x₂) -> x₁

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

           →DP Problem 13

             ↳Dependency Graph

       →DP Problem 7

         ↳Nar

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))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳Narrowing Transformation

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))

Strategy:

innermost

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(++(xs, :(x'', :(y'', ys')))) -> SUM(++(xs, sum(:(+(x'', y''), ys'))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

       →DP Problem 5

         ↳AFS

       →DP Problem 6

         ↳AFS

       →DP Problem 7

         ↳Nar

           →DP Problem 14

             ↳Remaining Obligation(s)

The following remains to be proven:
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))

Strategy:

innermost

Innermost Termination of R could not be shown.
Duration:
0:00 minutes