Termination Proof using AProVE

Term Rewriting System R:
[X, Y, Z, X1, X2]
a_{_first}(0, X) -> nil
a_{_first}(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
a_{_first}(X1, X2) -> first(X1, X2)
a_{_from}(X) -> cons(mark(X), from(s(X)))
a_{_from}(X) -> from(X)
mark(first(X1, X2)) -> a_{_first}(mark(X1), mark(X2))
mark(from(X)) -> a_{_from}(mark(X))
mark(0) -> 0
mark(nil) -> nil
mark(s(X)) -> s(mark(X))
mark(cons(X1, X2)) -> cons(mark(X1), X2)

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

A_{_FIRST}(s(X), cons(Y, Z)) -> MARK(Y)
A_{_FROM}(X) -> MARK(X)
MARK(first(X1, X2)) -> A_{_FIRST}(mark(X1), mark(X2))
MARK(first(X1, X2)) -> MARK(X1)
MARK(first(X1, X2)) -> MARK(X2)
MARK(from(X)) -> A_{_FROM}(mark(X))
MARK(from(X)) -> MARK(X)
MARK(s(X)) -> MARK(X)
MARK(cons(X1, X2)) -> MARK(X1)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Argument Filtering and Ordering

Dependency Pairs:

MARK(cons(X1, X2)) -> MARK(X1)
MARK(s(X)) -> MARK(X)
MARK(from(X)) -> MARK(X)
A_{_FROM}(X) -> MARK(X)
MARK(from(X)) -> A_{_FROM}(mark(X))
MARK(first(X1, X2)) -> MARK(X2)
MARK(first(X1, X2)) -> MARK(X1)
MARK(first(X1, X2)) -> A_{_FIRST}(mark(X1), mark(X2))
A_{_FIRST}(s(X), cons(Y, Z)) -> MARK(Y)

Rules:

a_{_first}(0, X) -> nil
a_{_first}(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
a_{_first}(X1, X2) -> first(X1, X2)
a_{_from}(X) -> cons(mark(X), from(s(X)))
a_{_from}(X) -> from(X)
mark(first(X1, X2)) -> a_{_first}(mark(X1), mark(X2))
mark(from(X)) -> a_{_from}(mark(X))
mark(0) -> 0
mark(nil) -> nil
mark(s(X)) -> s(mark(X))
mark(cons(X1, X2)) -> cons(mark(X1), X2)

Strategy:

innermost

The following dependency pairs can be strictly oriented:

MARK(s(X)) -> MARK(X)
MARK(from(X)) -> MARK(X)
A_{_FROM}(X) -> MARK(X)
MARK(from(X)) -> A_{_FROM}(mark(X))
MARK(first(X1, X2)) -> MARK(X2)
MARK(first(X1, X2)) -> MARK(X1)
MARK(first(X1, X2)) -> A_{_FIRST}(mark(X1), mark(X2))
A_{_FIRST}(s(X), cons(Y, Z)) -> MARK(Y)

The following usable rules for innermost can be oriented:

mark(first(X1, X2)) -> a_{_first}(mark(X1), mark(X2))
mark(from(X)) -> a_{_from}(mark(X))
mark(0) -> 0
mark(nil) -> nil
mark(s(X)) -> s(mark(X))
mark(cons(X1, X2)) -> cons(mark(X1), X2)
a_{_from}(X) -> cons(mark(X), from(s(X)))
a_{_from}(X) -> from(X)
a_{_first}(0, X) -> nil
a_{_first}(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
a_{_first}(X1, X2) -> first(X1, X2)

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

{A_{_FIRST}, a_{_first}, first} > MARK
{a_{_from}, from} > A_{_FROM} > MARK
0 > nil

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

MARK(x₁) -> MARK(x₁)
from(x₁) -> from(x₁)
first(x₁, x₂) -> first(x₁, x₂)
A_{_FROM}(x₁) -> A_{_FROM}(x₁)
s(x₁) -> s(x₁)
cons(x₁, x₂) -> x₁
A_{_FIRST}(x₁, x₂) -> A_{_FIRST}(x₁, x₂)
mark(x₁) -> x₁
a_{_first}(x₁, x₂) -> a_{_first}(x₁, x₂)
a_{_from}(x₁) -> a_{_from}(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 2

             ↳Argument Filtering and Ordering

Dependency Pair:

MARK(cons(X1, X2)) -> MARK(X1)

Rules:

a_{_first}(0, X) -> nil
a_{_first}(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
a_{_first}(X1, X2) -> first(X1, X2)
a_{_from}(X) -> cons(mark(X), from(s(X)))
a_{_from}(X) -> from(X)
mark(first(X1, X2)) -> a_{_first}(mark(X1), mark(X2))
mark(from(X)) -> a_{_from}(mark(X))
mark(0) -> 0
mark(nil) -> nil
mark(s(X)) -> s(mark(X))
mark(cons(X1, X2)) -> cons(mark(X1), X2)

Strategy:

innermost

The following dependency pair can be strictly oriented:

MARK(cons(X1, X2)) -> MARK(X1)

There are no usable rules for innermost 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:

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

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 2

             ↳AFS

...

               →DP Problem 3

                 ↳Dependency Graph

Dependency Pair:

Rules:

a_{_first}(0, X) -> nil
a_{_first}(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z))
a_{_first}(X1, X2) -> first(X1, X2)
a_{_from}(X) -> cons(mark(X), from(s(X)))
a_{_from}(X) -> from(X)
mark(first(X1, X2)) -> a_{_first}(mark(X1), mark(X2))
mark(from(X)) -> a_{_from}(mark(X))
mark(0) -> 0
mark(nil) -> nil
mark(s(X)) -> s(mark(X))
mark(cons(X1, X2)) -> cons(mark(X1), X2)

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:42 minutes