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

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

         ↳Nar

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

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: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:

trivial

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

         ↳Nar

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

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

         ↳Nar

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

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: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:

trivial

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

         ↳Nar

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

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

         ↳Nar

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

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: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:

trivial

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

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

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

           →DP Problem 7

             ↳Dependency Graph

       →DP Problem 4

         ↳Nar

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

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

         ↳Narrowing Transformation

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

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

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

three new Dependency Pairs are created:

SUM(app(nil, cons(x', cons(y', k'')))) -> SUM(sum(cons(x', cons(y', k''))))
SUM(app(cons(x'', l''), cons(x0, cons(y', k'')))) -> SUM(cons(x'', app(l'', sum(cons(x0, cons(y', k''))))))
SUM(app(l, cons(x'', cons(y'', k')))) -> SUM(app(l, sum(cons(plus(x'', y''), k'))))

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

         ↳Nar

           →DP Problem 8

             ↳Narrowing Transformation

Dependency Pairs:

SUM(app(l, cons(x'', cons(y'', k')))) -> SUM(app(l, sum(cons(plus(x'', y''), k'))))
SUM(app(nil, cons(x', cons(y', k'')))) -> SUM(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)))))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))

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

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

one new Dependency Pair is created:

SUM(app(nil, cons(x'', cons(y'', k''')))) -> SUM(sum(cons(plus(x'', y''), k''')))

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

         ↳Nar

           →DP Problem 8

             ↳Nar

...

               →DP Problem 9

                 ↳Narrowing Transformation

Dependency Pairs:

SUM(app(nil, cons(x'', cons(y'', k''')))) -> SUM(sum(cons(plus(x'', y''), k''')))
SUM(app(l, cons(x'', cons(y'', k')))) -> SUM(app(l, sum(cons(plus(x'', 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)))))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))

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

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

six new Dependency Pairs are created:

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

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

         ↳Nar

           →DP Problem 8

             ↳Nar

...

               →DP Problem 10

                 ↳Argument Filtering and Ordering

Dependency Pairs:

SUM(app(l, cons(s(x'), cons(y''', k')))) -> SUM(app(l, sum(cons(s(plus(x', y''')), k'))))
SUM(app(l, cons(0, cons(y''', k')))) -> SUM(app(l, sum(cons(y''', k'))))
SUM(app(l, cons(x''', cons(y''', cons(y', l''))))) -> SUM(app(l, sum(cons(plus(plus(x''', y'''), y'), l''))))
SUM(app(l, cons(x''', cons(y''', nil)))) -> SUM(app(l, cons(plus(x''', y'''), nil)))
SUM(app(nil, cons(x''', cons(y''', k'')))) -> SUM(sum(cons(plus(x''', y'''), k'')))
SUM(app(nil, cons(x'', cons(y'', k''')))) -> SUM(sum(cons(plus(x'', 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)))))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))

The following dependency pairs can be strictly oriented:

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

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

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)))))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))

Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:

app > cons

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

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

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

       →DP Problem 4

         ↳Nar

           →DP Problem 8

             ↳Nar

...

               →DP Problem 11

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

Using the Dependency Graph resulted in no new DP problems.

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