Termination Proof using AProVE

Term Rewriting System R:
[k, l, x, y]
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))
sum(plus(cons(0, x), cons(y, l))) -> pred(sum(cons(s(x), cons(y, l))))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
pred(cons(s(x), nil)) -> cons(x, nil)

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

APP(cons(x, l), k) -> APP(l, k)
SUM(cons(x, cons(y, l))) -> SUM(cons(plus(x, y), l))
SUM(cons(x, cons(y, l))) -> PLUS(x, y)
SUM(app(l, cons(x, cons(y, k)))) -> SUM(app(l, sum(cons(x, cons(y, k)))))
SUM(app(l, cons(x, cons(y, k)))) -> APP(l, sum(cons(x, cons(y, k))))
SUM(app(l, cons(x, cons(y, k)))) -> SUM(cons(x, cons(y, k)))
SUM(plus(cons(0, x), cons(y, l))) -> PRED(sum(cons(s(x), cons(y, l))))
SUM(plus(cons(0, x), cons(y, l))) -> SUM(cons(s(x), cons(y, l)))
PLUS(s(x), y) -> PLUS(x, y)

Furthermore, R contains four SCCs.

     ↳DPs

       →DP Problem 1

         ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

Dependency Pair:

APP(cons(x, l), k) -> APP(l, k)

Rules:

app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))
sum(plus(cons(0, x), cons(y, l))) -> pred(sum(cons(s(x), cons(y, l))))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
pred(cons(s(x), nil)) -> cons(x, nil)

The following dependency pair can be strictly oriented:

APP(cons(x, l), k) -> APP(l, k)

There are no usable rules using the Ce-refinement that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

resulting in one new DP problem.
Used Argument Filtering System:

APP(x₁, x₂) -> APP(x₁, x₂)
cons(x₁, x₂) -> cons(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 5

             ↳Dependency Graph

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

Dependency Pair:

Rules:

app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))
sum(plus(cons(0, x), cons(y, l))) -> pred(sum(cons(s(x), cons(y, l))))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
pred(cons(s(x), nil)) -> cons(x, nil)

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

Dependency Pair:

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

Rules:

app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))
sum(plus(cons(0, x), cons(y, l))) -> pred(sum(cons(s(x), cons(y, l))))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
pred(cons(s(x), nil)) -> cons(x, nil)

The following dependency pair can be strictly oriented:

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

There are no usable rules using the Ce-refinement that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

resulting in one new DP problem.
Used Argument Filtering System:

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

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

           →DP Problem 6

             ↳Dependency Graph

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

Dependency Pair:

Rules:

app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))
sum(plus(cons(0, x), cons(y, l))) -> pred(sum(cons(s(x), cons(y, l))))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
pred(cons(s(x), nil)) -> cons(x, nil)

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

Dependency Pair:

SUM(cons(x, cons(y, l))) -> SUM(cons(plus(x, y), l))

Rules:

app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))
sum(plus(cons(0, x), cons(y, l))) -> pred(sum(cons(s(x), cons(y, l))))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
pred(cons(s(x), nil)) -> cons(x, nil)

The following dependency pair can be strictly oriented:

SUM(cons(x, cons(y, l))) -> SUM(cons(plus(x, y), l))

The following usable rules using the Ce-refinement can be oriented:

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

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

POL(0) = 1

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

POL(s(x₁)) = x₁

resulting in one new DP problem.
Used Argument Filtering System:

SUM(x₁) -> SUM(x₁)
cons(x₁, x₂) -> cons(x₁, x₂)
plus(x₁, x₂) -> plus(x₁, x₂)
s(x₁) -> s(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

           →DP Problem 7

             ↳Dependency Graph

       →DP Problem 4

         ↳AFS

Dependency Pair:

Rules:

app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))
sum(plus(cons(0, x), cons(y, l))) -> pred(sum(cons(s(x), cons(y, l))))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
pred(cons(s(x), nil)) -> cons(x, nil)

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

Dependency Pair:

SUM(app(l, cons(x, cons(y, k)))) -> SUM(app(l, sum(cons(x, cons(y, k)))))

Rules:

app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))
sum(plus(cons(0, x), cons(y, l))) -> pred(sum(cons(s(x), cons(y, l))))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
pred(cons(s(x), nil)) -> cons(x, nil)

The following dependency pair can be strictly oriented:

SUM(app(l, cons(x, cons(y, k)))) -> SUM(app(l, sum(cons(x, cons(y, k)))))

The following usable rules using the Ce-refinement can be oriented:

app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))
sum(plus(cons(0, x), cons(y, l))) -> pred(sum(cons(s(x), cons(y, l))))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
pred(cons(s(x), nil)) -> cons(x, nil)

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

POL(0) = 0

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

POL(pred(x₁)) = x₁

POL(nil) = 0

POL(sum) = 1

POL(s(x₁)) = x₁

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

resulting in one new DP problem.
Used Argument Filtering System:

SUM(x₁) -> SUM(x₁)
app(x₁, x₂) -> app(x₁, x₂)
cons(x₁, x₂) -> cons(x₂)
sum(x₁) -> sum
pred(x₁) -> pred(x₁)
plus(x₁, x₂) -> plus(x₁, x₂)
s(x₁) -> s(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳AFS

           →DP Problem 8

             ↳Dependency Graph

Dependency Pair:

Rules:

app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))
sum(plus(cons(0, x), cons(y, l))) -> pred(sum(cons(s(x), cons(y, l))))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
pred(cons(s(x), nil)) -> cons(x, nil)

Using the Dependency Graph resulted in no new DP problems.

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

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

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

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