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

         ↳Usable Rules (Innermost)

       →DP Problem 2

         ↳UsableRules

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

As we are in the innermost case, we can delete all 22 non-usable-rules.

     ↳DPs

       →DP Problem 1

         ↳UsableRules

           →DP Problem 3

             ↳Size-Change Principle

       →DP Problem 2

         ↳UsableRules

Dependency Pair:

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

Rule:

none

Strategy:

innermost

We number the DPs as follows:

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

and get the following Size-Change Graph(s):

{1}	,	{1}
1	>	1
2	>	2

which lead(s) to this/these maximal multigraph(s):

{1}	,	{1}
1	>	1
2	>	2

D_P: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.

trivial

with Argument Filtering System:

s(x₁) -> s(x₁)

We obtain no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳Usable Rules (Innermost)

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

As we are in the innermost case, we can delete all 22 non-usable-rules.

     ↳DPs

       →DP Problem 1

         ↳UsableRules

       →DP Problem 2

         ↳UsableRules

           →DP Problem 4

             ↳Size-Change Principle

Dependency Pairs:

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

Rule:

none

Strategy:

innermost

We number the DPs as follows:

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

and get the following Size-Change Graph(s):

{1, 2, 3, 4}	,	{1, 2, 3, 4}
1	>	1

which lead(s) to this/these maximal multigraph(s):

{1, 2, 3, 4}	,	{1, 2, 3, 4}
1	>	1

D_P: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.

trivial

with Argument Filtering System:

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

We obtain no new DP problems.

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