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

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

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

The following remains to be proven:

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

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

The following remains to be proven:

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

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