YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (64ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (97ms).
 |    | – Problem 7 was processed with processor PolynomialLinearRange4 (88ms).
 |    |    | – Problem 8 was processed with processor PolynomialLinearRange4 (33ms).
 | – Problem 3 was processed with processor PolynomialLinearRange4 (9ms).
 | – Problem 4 was processed with processor PolynomialLinearRange4 (10ms).
 | – Problem 5 was processed with processor PolynomialLinearRange4 (16ms).
 | – Problem 6 was processed with processor PolynomialLinearRange4 (105ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

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

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))half(0) → 0
half(s(0)) → 0half(s(s(X))) → s(half(X))
half(dbl(X)) → X

Original Signature

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

Strategy

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

The following SCCs where found

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

Problem 2: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(first(x_1, x_2)) → T(x_2)T(s(x_1)) → T(x_1)
T(terms(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))half(0) → 0
half(s(0)) → 0half(s(s(X))) → s(half(X))
half(dbl(X)) → X

Original Signature

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

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(nil) = ∅
μ(terms#) = μ(terms) = μ(sqr) = μ(half) = μ(dbl) = μ(recip) = μ(half#) = μ(dbl#) = μ(s) = μ(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 7: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(first(x_1, x_2)) → T(x_2)T(terms(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))half(0) → 0
half(s(0)) → 0half(s(s(X))) → s(half(X))
half(dbl(X)) → X

Original Signature

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

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(nil) = ∅
μ(terms#) = μ(terms) = μ(sqr) = μ(half) = μ(dbl) = μ(recip) = μ(half#) = μ(dbl#) = μ(s) = μ(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)

Problem 8: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

T(terms(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))half(0) → 0
half(s(0)) → 0half(s(s(X))) → s(half(X))
half(dbl(X)) → X

Original Signature

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

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(nil) = ∅
μ(terms#) = μ(terms) = μ(sqr) = μ(half) = μ(dbl) = μ(recip) = μ(half#) = μ(dbl#) = μ(s) = μ(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(terms(x_1)) → T(x_1)

Problem 3: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

sqr#(s(X)) → sqr#(X)

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))half(0) → 0
half(s(0)) → 0half(s(s(X))) → s(half(X))
half(dbl(X)) → X

Original Signature

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

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(nil) = ∅
μ(terms#) = μ(terms) = μ(sqr) = μ(half) = μ(dbl) = μ(recip) = μ(half#) = μ(dbl#) = μ(s) = μ(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:

sqr#(s(X)) → sqr#(X)

Problem 4: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

dbl#(s(X)) → dbl#(X)

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))half(0) → 0
half(s(0)) → 0half(s(s(X))) → s(half(X))
half(dbl(X)) → X

Original Signature

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

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(nil) = ∅
μ(terms#) = μ(terms) = μ(sqr) = μ(half) = μ(dbl) = μ(recip) = μ(half#) = μ(dbl#) = μ(s) = μ(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:

dbl#(s(X)) → dbl#(X)

Problem 5: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

add#(s(X), Y) → add#(X, Y)

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))half(0) → 0
half(s(0)) → 0half(s(s(X))) → s(half(X))
half(dbl(X)) → X

Original Signature

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

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(nil) = ∅
μ(terms#) = μ(terms) = μ(sqr) = μ(half) = μ(dbl) = μ(recip) = μ(half#) = μ(dbl#) = μ(s) = μ(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:

add#(s(X), Y) → add#(X, Y)

Problem 6: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

half#(s(s(X))) → half#(X)

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))half(0) → 0
half(s(0)) → 0half(s(s(X))) → s(half(X))
half(dbl(X)) → X

Original Signature

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

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(nil) = ∅
μ(terms#) = μ(terms) = μ(sqr) = μ(half) = μ(dbl) = μ(recip) = μ(half#) = μ(dbl#) = μ(s) = μ(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:

half#(s(s(X))) → half#(X)