YES

The TRS could be proven terminating. The proof took 956 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (122ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (183ms).
 |    | – Problem 3 was processed with processor PolynomialLinearRange4 (79ms).
 |    |    | – Problem 4 was processed with processor PolynomialLinearRange4 (95ms).
 |    |    |    | – Problem 5 was processed with processor PolynomialLinearRange4 (38ms).
 |    |    |    |    | – Problem 6 was processed with processor PolynomialLinearRange4 (13ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

T(first(x_1, x_2)) → T(x_2)T(add(x_1, x_2)) → T(x_2)
T(s(x_1)) → T(x_1)T(first(X, Z)) → first#(X, Z)
T(dbl(X)) → dbl#(X)T(dbl(X)) → dbl#(X)
terms#(N) → sqr#(N)T(terms(s(N))) → terms#(s(N))
T(first(x_1, x_2)) → T(x_1)T(add(X, Y)) → add#(X, Y)
T(sqr(x_1)) → T(x_1)T(sqr(X)) → sqr#(X)
T(add(sqr(X), dbl(X))) → add#(sqr(X), dbl(X))T(add(x_1, x_2)) → T(x_1)
T(dbl(x_1)) → T(x_1)

Rewrite Rules

terms(N) → cons(recip(sqr(N)), terms(s(N)))sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))add(0, X) → X
add(s(X), Y) → s(add(X, Y))first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))

Original Signature

Termination of terms over the following signature is verified: 0, s, terms, sqr, dbl, recip, add, first, cons, nil

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(s) = μ(nil) = ∅
μ(terms#) = μ(terms) = μ(sqr) = μ(dbl) = μ(recip) = μ(dbl#) = μ(sqr#) = μ(cons) = {1}
μ(add) = μ(first#) = μ(add#) = μ(first) = {1, 2}

The following SCCs where found

T(first(x_1, x_2)) → T(x_2)T(sqr(x_1)) → T(x_1)
T(add(x_1, x_2)) → T(x_2)T(add(x_1, x_2)) → T(x_1)
T(s(x_1)) → T(x_1)T(dbl(x_1)) → T(x_1)
T(first(x_1, x_2)) → T(x_1)

Problem 2: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(first(x_1, x_2)) → T(x_2)T(sqr(x_1)) → T(x_1)
T(add(x_1, x_2)) → T(x_2)T(add(x_1, x_2)) → T(x_1)
T(s(x_1)) → T(x_1)T(dbl(x_1)) → T(x_1)
T(first(x_1, x_2)) → T(x_1)

Rewrite Rules

terms(N) → cons(recip(sqr(N)), terms(s(N)))sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))add(0, X) → X
add(s(X), Y) → s(add(X, Y))first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))

Original Signature

Termination of terms over the following signature is verified: 0, s, terms, sqr, dbl, recip, add, first, cons, nil

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(s) = μ(nil) = ∅
μ(terms#) = μ(terms) = μ(sqr) = μ(dbl) = μ(recip) = μ(dbl#) = μ(sqr#) = μ(cons) = {1}
μ(add) = μ(first#) = μ(add#) = μ(first) = {1, 2}

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

T(dbl(x_1)) → T(x_1)

Problem 3: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(first(x_1, x_2)) → T(x_2)T(add(x_1, x_2)) → T(x_2)
T(sqr(x_1)) → T(x_1)T(add(x_1, x_2)) → T(x_1)
T(s(x_1)) → T(x_1)T(first(x_1, x_2)) → T(x_1)

Rewrite Rules

terms(N) → cons(recip(sqr(N)), terms(s(N)))sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))add(0, X) → X
add(s(X), Y) → s(add(X, Y))first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))

Original Signature

Termination of terms over the following signature is verified: 0, s, terms, sqr, dbl, recip, add, first, nil, cons

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(s) = μ(nil) = ∅
μ(terms#) = μ(terms) = μ(sqr) = μ(dbl) = μ(recip) = μ(dbl#) = μ(sqr#) = μ(cons) = {1}
μ(add) = μ(first#) = μ(add#) = μ(first) = {1, 2}

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

T(s(x_1)) → T(x_1)

Problem 4: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(first(x_1, x_2)) → T(x_2)T(sqr(x_1)) → T(x_1)
T(add(x_1, x_2)) → T(x_2)T(add(x_1, x_2)) → T(x_1)
T(first(x_1, x_2)) → T(x_1)

Rewrite Rules

terms(N) → cons(recip(sqr(N)), terms(s(N)))sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))add(0, X) → X
add(s(X), Y) → s(add(X, Y))first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))

Original Signature

Termination of terms over the following signature is verified: 0, s, terms, sqr, dbl, recip, add, first, cons, nil

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(s) = μ(nil) = ∅
μ(terms#) = μ(terms) = μ(sqr) = μ(dbl) = μ(recip) = μ(dbl#) = μ(sqr#) = μ(cons) = {1}
μ(add) = μ(first#) = μ(add#) = μ(first) = {1, 2}

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

T(sqr(x_1)) → T(x_1)

Problem 5: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(first(x_1, x_2)) → T(x_2)T(add(x_1, x_2)) → T(x_2)
T(add(x_1, x_2)) → T(x_1)T(first(x_1, x_2)) → T(x_1)

Rewrite Rules

terms(N) → cons(recip(sqr(N)), terms(s(N)))sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))add(0, X) → X
add(s(X), Y) → s(add(X, Y))first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))

Original Signature

Termination of terms over the following signature is verified: 0, s, terms, sqr, dbl, recip, add, first, nil, cons

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(s) = μ(nil) = ∅
μ(terms#) = μ(terms) = μ(sqr) = μ(dbl) = μ(recip) = μ(dbl#) = μ(sqr#) = μ(cons) = {1}
μ(add) = μ(first#) = μ(add#) = μ(first) = {1, 2}

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

T(add(x_1, x_2)) → T(x_2)T(add(x_1, x_2)) → T(x_1)

Problem 6: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(first(x_1, x_2)) → T(x_2)T(first(x_1, x_2)) → T(x_1)

Rewrite Rules

terms(N) → cons(recip(sqr(N)), terms(s(N)))sqr(0) → 0
sqr(s(X)) → s(add(sqr(X), dbl(X)))dbl(0) → 0
dbl(s(X)) → s(s(dbl(X)))add(0, X) → X
add(s(X), Y) → s(add(X, Y))first(0, X) → nil
first(s(X), cons(Y, Z)) → cons(Y, first(X, Z))

Original Signature

Termination of terms over the following signature is verified: 0, s, terms, sqr, dbl, recip, add, first, cons, nil

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(s) = μ(nil) = ∅
μ(terms#) = μ(terms) = μ(sqr) = μ(dbl) = μ(recip) = μ(dbl#) = μ(sqr#) = μ(cons) = {1}
μ(add) = μ(first#) = μ(add#) = μ(first) = {1, 2}

Polynomial Interpretation

There are no usable rules

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

T(first(x_1, x_2)) → T(x_2)T(first(x_1, x_2)) → T(x_1)