Termination Proof using AProVE

Term Rewriting System R:
[X, Y, X1, X2, L]
a_{_eq}(0, 0) -> true
a_{_eq}(s(X), s(Y)) -> a_{_eq}(X, Y)
a_{_eq}(X, Y) -> false
a_{_eq}(X1, X2) -> eq(X1, X2)
a_{_inf}(X) -> cons(X, inf(s(X)))
a_{_inf}(X) -> inf(X)
a_{_take}(0, X) -> nil
a_{_take}(s(X), cons(Y, L)) -> cons(Y, take(X, L))
a_{_take}(X1, X2) -> take(X1, X2)
a_{_length}(nil) -> 0
a_{_length}(cons(X, L)) -> s(length(L))
a_{_length}(X) -> length(X)
mark(eq(X1, X2)) -> a_{_eq}(X1, X2)
mark(inf(X)) -> a_{_inf}(mark(X))
mark(take(X1, X2)) -> a_{_take}(mark(X1), mark(X2))
mark(length(X)) -> a_{_length}(mark(X))
mark(0) -> 0
mark(true) -> true
mark(s(X)) -> s(X)
mark(false) -> false
mark(cons(X1, X2)) -> cons(X1, X2)
mark(nil) -> nil

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

A_{_EQ}(s(X), s(Y)) -> A_{_EQ}(X, Y)
MARK(eq(X1, X2)) -> A_{_EQ}(X1, X2)
MARK(inf(X)) -> A_{_INF}(mark(X))
MARK(inf(X)) -> MARK(X)
MARK(take(X1, X2)) -> A_{_TAKE}(mark(X1), mark(X2))
MARK(take(X1, X2)) -> MARK(X1)
MARK(take(X1, X2)) -> MARK(X2)
MARK(length(X)) -> A_{_LENGTH}(mark(X))
MARK(length(X)) -> MARK(X)

Furthermore, R contains two SCCs.

     ↳DPs

       →DP Problem 1

         ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

Dependency Pair:

A_{_EQ}(s(X), s(Y)) -> A_{_EQ}(X, Y)

Rules:

a_{_eq}(0, 0) -> true
a_{_eq}(s(X), s(Y)) -> a_{_eq}(X, Y)
a_{_eq}(X, Y) -> false
a_{_eq}(X1, X2) -> eq(X1, X2)
a_{_inf}(X) -> cons(X, inf(s(X)))
a_{_inf}(X) -> inf(X)
a_{_take}(0, X) -> nil
a_{_take}(s(X), cons(Y, L)) -> cons(Y, take(X, L))
a_{_take}(X1, X2) -> take(X1, X2)
a_{_length}(nil) -> 0
a_{_length}(cons(X, L)) -> s(length(L))
a_{_length}(X) -> length(X)
mark(eq(X1, X2)) -> a_{_eq}(X1, X2)
mark(inf(X)) -> a_{_inf}(mark(X))
mark(take(X1, X2)) -> a_{_take}(mark(X1), mark(X2))
mark(length(X)) -> a_{_length}(mark(X))
mark(0) -> 0
mark(true) -> true
mark(s(X)) -> s(X)
mark(false) -> false
mark(cons(X1, X2)) -> cons(X1, X2)
mark(nil) -> nil

Strategy:

innermost

The following dependency pair can be strictly oriented:

A_{_EQ}(s(X), s(Y)) -> A_{_EQ}(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:

A_{_EQ}(x₁, x₂) -> A_{_EQ}(x₁, x₂)
s(x₁) -> s(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 3

             ↳Dependency Graph

       →DP Problem 2

         ↳AFS

Dependency Pair:

Rules:

a_{_eq}(0, 0) -> true
a_{_eq}(s(X), s(Y)) -> a_{_eq}(X, Y)
a_{_eq}(X, Y) -> false
a_{_eq}(X1, X2) -> eq(X1, X2)
a_{_inf}(X) -> cons(X, inf(s(X)))
a_{_inf}(X) -> inf(X)
a_{_take}(0, X) -> nil
a_{_take}(s(X), cons(Y, L)) -> cons(Y, take(X, L))
a_{_take}(X1, X2) -> take(X1, X2)
a_{_length}(nil) -> 0
a_{_length}(cons(X, L)) -> s(length(L))
a_{_length}(X) -> length(X)
mark(eq(X1, X2)) -> a_{_eq}(X1, X2)
mark(inf(X)) -> a_{_inf}(mark(X))
mark(take(X1, X2)) -> a_{_take}(mark(X1), mark(X2))
mark(length(X)) -> a_{_length}(mark(X))
mark(0) -> 0
mark(true) -> true
mark(s(X)) -> s(X)
mark(false) -> false
mark(cons(X1, X2)) -> cons(X1, X2)
mark(nil) -> nil

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Argument Filtering and Ordering

Dependency Pairs:

MARK(length(X)) -> MARK(X)
MARK(take(X1, X2)) -> MARK(X2)
MARK(take(X1, X2)) -> MARK(X1)
MARK(inf(X)) -> MARK(X)

Rules:

a_{_eq}(0, 0) -> true
a_{_eq}(s(X), s(Y)) -> a_{_eq}(X, Y)
a_{_eq}(X, Y) -> false
a_{_eq}(X1, X2) -> eq(X1, X2)
a_{_inf}(X) -> cons(X, inf(s(X)))
a_{_inf}(X) -> inf(X)
a_{_take}(0, X) -> nil
a_{_take}(s(X), cons(Y, L)) -> cons(Y, take(X, L))
a_{_take}(X1, X2) -> take(X1, X2)
a_{_length}(nil) -> 0
a_{_length}(cons(X, L)) -> s(length(L))
a_{_length}(X) -> length(X)
mark(eq(X1, X2)) -> a_{_eq}(X1, X2)
mark(inf(X)) -> a_{_inf}(mark(X))
mark(take(X1, X2)) -> a_{_take}(mark(X1), mark(X2))
mark(length(X)) -> a_{_length}(mark(X))
mark(0) -> 0
mark(true) -> true
mark(s(X)) -> s(X)
mark(false) -> false
mark(cons(X1, X2)) -> cons(X1, X2)
mark(nil) -> nil

Strategy:

innermost

The following dependency pairs can be strictly oriented:

MARK(length(X)) -> MARK(X)
MARK(take(X1, X2)) -> MARK(X2)
MARK(take(X1, X2)) -> MARK(X1)
MARK(inf(X)) -> MARK(X)

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:

MARK(x₁) -> MARK(x₁)
inf(x₁) -> inf(x₁)
take(x₁, x₂) -> take(x₁, x₂)
length(x₁) -> length(x₁)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

           →DP Problem 4

             ↳Dependency Graph

Dependency Pair:

Rules:

a_{_eq}(0, 0) -> true
a_{_eq}(s(X), s(Y)) -> a_{_eq}(X, Y)
a_{_eq}(X, Y) -> false
a_{_eq}(X1, X2) -> eq(X1, X2)
a_{_inf}(X) -> cons(X, inf(s(X)))
a_{_inf}(X) -> inf(X)
a_{_take}(0, X) -> nil
a_{_take}(s(X), cons(Y, L)) -> cons(Y, take(X, L))
a_{_take}(X1, X2) -> take(X1, X2)
a_{_length}(nil) -> 0
a_{_length}(cons(X, L)) -> s(length(L))
a_{_length}(X) -> length(X)
mark(eq(X1, X2)) -> a_{_eq}(X1, X2)
mark(inf(X)) -> a_{_inf}(mark(X))
mark(take(X1, X2)) -> a_{_take}(mark(X1), mark(X2))
mark(length(X)) -> a_{_length}(mark(X))
mark(0) -> 0
mark(true) -> true
mark(s(X)) -> s(X)
mark(false) -> false
mark(cons(X1, X2)) -> cons(X1, X2)
mark(nil) -> nil

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

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