YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (219ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (2018ms).
 |    | – Problem 3 was processed with processor DependencyGraph (10ms).
 |    |    | – Problem 4 was processed with processor PolynomialLinearRange4iUR (684ms).
 |    |    |    | – Problem 5 was processed with processor PolynomialLinearRange4iUR (23ms).
 |    |    |    |    | – Problem 6 was processed with processor PolynomialLinearRange4iUR (22ms).
 |    |    |    |    |    | – Problem 7 was processed with processor PolynomialLinearRange4iUR (11ms).
 |    |    |    |    |    |    | – Problem 8 was processed with processor PolynomialLinearRange4iUR (8ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

mark#(first(X1, X2))mark#(X2)mark#(terms(X))a__terms#(mark(X))
a__terms#(N)mark#(N)mark#(first(X1, X2))a__first#(mark(X1), mark(X2))
mark#(add(X1, X2))a__add#(mark(X1), mark(X2))mark#(cons(X1, X2))mark#(X1)
mark#(dbl(X))a__dbl#(mark(X))a__add#(0, X)mark#(X)
mark#(dbl(X))mark#(X)mark#(terms(X))mark#(X)
mark#(recip(X))mark#(X)mark#(sqr(X))mark#(X)
a__first#(s(X), cons(Y, Z))mark#(Y)mark#(sqr(X))a__sqr#(mark(X))
mark#(add(X1, X2))mark#(X2)mark#(first(X1, X2))mark#(X1)
a__terms#(N)a__sqr#(mark(N))mark#(add(X1, X2))mark#(X1)

Rewrite Rules

a__terms(N)cons(recip(a__sqr(mark(N))), terms(s(N)))a__sqr(0)0
a__sqr(s(X))s(add(sqr(X), dbl(X)))a__dbl(0)0
a__dbl(s(X))s(s(dbl(X)))a__add(0, X)mark(X)
a__add(s(X), Y)s(add(X, Y))a__first(0, X)nil
a__first(s(X), cons(Y, Z))cons(mark(Y), first(X, Z))mark(terms(X))a__terms(mark(X))
mark(sqr(X))a__sqr(mark(X))mark(add(X1, X2))a__add(mark(X1), mark(X2))
mark(dbl(X))a__dbl(mark(X))mark(first(X1, X2))a__first(mark(X1), mark(X2))
mark(cons(X1, X2))cons(mark(X1), X2)mark(recip(X))recip(mark(X))
mark(s(X))s(X)mark(0)0
mark(nil)nila__terms(X)terms(X)
a__sqr(X)sqr(X)a__add(X1, X2)add(X1, X2)
a__dbl(X)dbl(X)a__first(X1, X2)first(X1, X2)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, mark, dbl, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, cons, nil

Strategy


The following SCCs where found

mark#(terms(X)) → a__terms#(mark(X))mark#(first(X1, X2)) → mark#(X2)
a__terms#(N) → mark#(N)mark#(first(X1, X2)) → a__first#(mark(X1), mark(X2))
mark#(add(X1, X2)) → a__add#(mark(X1), mark(X2))mark#(cons(X1, X2)) → mark#(X1)
a__add#(0, X) → mark#(X)mark#(dbl(X)) → mark#(X)
mark#(terms(X)) → mark#(X)mark#(sqr(X)) → mark#(X)
mark#(recip(X)) → mark#(X)a__first#(s(X), cons(Y, Z)) → mark#(Y)
mark#(first(X1, X2)) → mark#(X1)mark#(add(X1, X2)) → mark#(X2)
mark#(add(X1, X2)) → mark#(X1)

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(first(X1, X2))mark#(X2)mark#(terms(X))a__terms#(mark(X))
a__terms#(N)mark#(N)mark#(add(X1, X2))a__add#(mark(X1), mark(X2))
mark#(first(X1, X2))a__first#(mark(X1), mark(X2))mark#(cons(X1, X2))mark#(X1)
a__add#(0, X)mark#(X)mark#(dbl(X))mark#(X)
mark#(terms(X))mark#(X)mark#(recip(X))mark#(X)
mark#(sqr(X))mark#(X)a__first#(s(X), cons(Y, Z))mark#(Y)
mark#(first(X1, X2))mark#(X1)mark#(add(X1, X2))mark#(X2)
mark#(add(X1, X2))mark#(X1)

Rewrite Rules

a__terms(N)cons(recip(a__sqr(mark(N))), terms(s(N)))a__sqr(0)0
a__sqr(s(X))s(add(sqr(X), dbl(X)))a__dbl(0)0
a__dbl(s(X))s(s(dbl(X)))a__add(0, X)mark(X)
a__add(s(X), Y)s(add(X, Y))a__first(0, X)nil
a__first(s(X), cons(Y, Z))cons(mark(Y), first(X, Z))mark(terms(X))a__terms(mark(X))
mark(sqr(X))a__sqr(mark(X))mark(add(X1, X2))a__add(mark(X1), mark(X2))
mark(dbl(X))a__dbl(mark(X))mark(first(X1, X2))a__first(mark(X1), mark(X2))
mark(cons(X1, X2))cons(mark(X1), X2)mark(recip(X))recip(mark(X))
mark(s(X))s(X)mark(0)0
mark(nil)nila__terms(X)terms(X)
a__sqr(X)sqr(X)a__add(X1, X2)add(X1, X2)
a__dbl(X)dbl(X)a__first(X1, X2)first(X1, X2)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, mark, dbl, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, cons, nil

Strategy


Polynomial Interpretation

Improved Usable rules

a__terms(X)terms(X)a__first(X1, X2)first(X1, X2)
mark(cons(X1, X2))cons(mark(X1), X2)mark(s(X))s(X)
mark(terms(X))a__terms(mark(X))mark(0)0
a__dbl(s(X))s(s(dbl(X)))mark(first(X1, X2))a__first(mark(X1), mark(X2))
mark(sqr(X))a__sqr(mark(X))a__sqr(s(X))s(add(sqr(X), dbl(X)))
a__first(0, X)nila__dbl(0)0
a__sqr(0)0a__add(X1, X2)add(X1, X2)
mark(dbl(X))a__dbl(mark(X))a__add(s(X), Y)s(add(X, Y))
a__sqr(X)sqr(X)mark(recip(X))recip(mark(X))
mark(nil)nila__terms(N)cons(recip(a__sqr(mark(N))), terms(s(N)))
mark(add(X1, X2))a__add(mark(X1), mark(X2))a__first(s(X), cons(Y, Z))cons(mark(Y), first(X, Z))
a__dbl(X)dbl(X)a__add(0, X)mark(X)

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

mark#(first(X1, X2))mark#(X2)mark#(terms(X))a__terms#(mark(X))
mark#(first(X1, X2))a__first#(mark(X1), mark(X2))mark#(dbl(X))mark#(X)
mark#(terms(X))mark#(X)a__first#(s(X), cons(Y, Z))mark#(Y)
mark#(first(X1, X2))mark#(X1)

Problem 3: DependencyGraph



Dependency Pair Problem

Dependency Pairs

mark#(sqr(X))mark#(X)mark#(recip(X))mark#(X)
a__terms#(N)mark#(N)mark#(add(X1, X2))a__add#(mark(X1), mark(X2))
mark#(cons(X1, X2))mark#(X1)mark#(add(X1, X2))mark#(X2)
mark#(add(X1, X2))mark#(X1)a__add#(0, X)mark#(X)

Rewrite Rules

a__terms(N)cons(recip(a__sqr(mark(N))), terms(s(N)))a__sqr(0)0
a__sqr(s(X))s(add(sqr(X), dbl(X)))a__dbl(0)0
a__dbl(s(X))s(s(dbl(X)))a__add(0, X)mark(X)
a__add(s(X), Y)s(add(X, Y))a__first(0, X)nil
a__first(s(X), cons(Y, Z))cons(mark(Y), first(X, Z))mark(terms(X))a__terms(mark(X))
mark(sqr(X))a__sqr(mark(X))mark(add(X1, X2))a__add(mark(X1), mark(X2))
mark(dbl(X))a__dbl(mark(X))mark(first(X1, X2))a__first(mark(X1), mark(X2))
mark(cons(X1, X2))cons(mark(X1), X2)mark(recip(X))recip(mark(X))
mark(s(X))s(X)mark(0)0
mark(nil)nila__terms(X)terms(X)
a__sqr(X)sqr(X)a__add(X1, X2)add(X1, X2)
a__dbl(X)dbl(X)a__first(X1, X2)first(X1, X2)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, mark, dbl, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, nil, cons

Strategy


The following SCCs where found

mark#(sqr(X)) → mark#(X)mark#(recip(X)) → mark#(X)
mark#(add(X1, X2)) → a__add#(mark(X1), mark(X2))mark#(cons(X1, X2)) → mark#(X1)
mark#(add(X1, X2)) → mark#(X2)mark#(add(X1, X2)) → mark#(X1)
a__add#(0, X) → mark#(X)

Problem 4: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(sqr(X))mark#(X)mark#(recip(X))mark#(X)
mark#(add(X1, X2))a__add#(mark(X1), mark(X2))mark#(cons(X1, X2))mark#(X1)
mark#(add(X1, X2))mark#(X2)mark#(add(X1, X2))mark#(X1)
a__add#(0, X)mark#(X)

Rewrite Rules

a__terms(N)cons(recip(a__sqr(mark(N))), terms(s(N)))a__sqr(0)0
a__sqr(s(X))s(add(sqr(X), dbl(X)))a__dbl(0)0
a__dbl(s(X))s(s(dbl(X)))a__add(0, X)mark(X)
a__add(s(X), Y)s(add(X, Y))a__first(0, X)nil
a__first(s(X), cons(Y, Z))cons(mark(Y), first(X, Z))mark(terms(X))a__terms(mark(X))
mark(sqr(X))a__sqr(mark(X))mark(add(X1, X2))a__add(mark(X1), mark(X2))
mark(dbl(X))a__dbl(mark(X))mark(first(X1, X2))a__first(mark(X1), mark(X2))
mark(cons(X1, X2))cons(mark(X1), X2)mark(recip(X))recip(mark(X))
mark(s(X))s(X)mark(0)0
mark(nil)nila__terms(X)terms(X)
a__sqr(X)sqr(X)a__add(X1, X2)add(X1, X2)
a__dbl(X)dbl(X)a__first(X1, X2)first(X1, X2)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, mark, dbl, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, nil, cons

Strategy


Polynomial Interpretation

Improved Usable rules

a__terms(X)terms(X)a__first(X1, X2)first(X1, X2)
mark(cons(X1, X2))cons(mark(X1), X2)mark(s(X))s(X)
mark(terms(X))a__terms(mark(X))mark(0)0
a__dbl(s(X))s(s(dbl(X)))mark(first(X1, X2))a__first(mark(X1), mark(X2))
mark(sqr(X))a__sqr(mark(X))a__sqr(s(X))s(add(sqr(X), dbl(X)))
a__first(0, X)nila__dbl(0)0
a__sqr(0)0a__add(X1, X2)add(X1, X2)
mark(dbl(X))a__dbl(mark(X))a__add(s(X), Y)s(add(X, Y))
a__sqr(X)sqr(X)mark(recip(X))recip(mark(X))
mark(nil)nila__terms(N)cons(recip(a__sqr(mark(N))), terms(s(N)))
mark(add(X1, X2))a__add(mark(X1), mark(X2))a__first(s(X), cons(Y, Z))cons(mark(Y), first(X, Z))
a__dbl(X)dbl(X)a__add(0, X)mark(X)

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

mark#(add(X1, X2))a__add#(mark(X1), mark(X2))a__add#(0, X)mark#(X)

Problem 5: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(recip(X))mark#(X)mark#(sqr(X))mark#(X)
mark#(cons(X1, X2))mark#(X1)mark#(add(X1, X2))mark#(X2)
mark#(add(X1, X2))mark#(X1)

Rewrite Rules

a__terms(N)cons(recip(a__sqr(mark(N))), terms(s(N)))a__sqr(0)0
a__sqr(s(X))s(add(sqr(X), dbl(X)))a__dbl(0)0
a__dbl(s(X))s(s(dbl(X)))a__add(0, X)mark(X)
a__add(s(X), Y)s(add(X, Y))a__first(0, X)nil
a__first(s(X), cons(Y, Z))cons(mark(Y), first(X, Z))mark(terms(X))a__terms(mark(X))
mark(sqr(X))a__sqr(mark(X))mark(add(X1, X2))a__add(mark(X1), mark(X2))
mark(dbl(X))a__dbl(mark(X))mark(first(X1, X2))a__first(mark(X1), mark(X2))
mark(cons(X1, X2))cons(mark(X1), X2)mark(recip(X))recip(mark(X))
mark(s(X))s(X)mark(0)0
mark(nil)nila__terms(X)terms(X)
a__sqr(X)sqr(X)a__add(X1, X2)add(X1, X2)
a__dbl(X)dbl(X)a__first(X1, X2)first(X1, X2)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, mark, dbl, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, cons, nil

Strategy


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:

mark#(sqr(X))mark#(X)

Problem 6: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(recip(X))mark#(X)mark#(cons(X1, X2))mark#(X1)
mark#(add(X1, X2))mark#(X2)mark#(add(X1, X2))mark#(X1)

Rewrite Rules

a__terms(N)cons(recip(a__sqr(mark(N))), terms(s(N)))a__sqr(0)0
a__sqr(s(X))s(add(sqr(X), dbl(X)))a__dbl(0)0
a__dbl(s(X))s(s(dbl(X)))a__add(0, X)mark(X)
a__add(s(X), Y)s(add(X, Y))a__first(0, X)nil
a__first(s(X), cons(Y, Z))cons(mark(Y), first(X, Z))mark(terms(X))a__terms(mark(X))
mark(sqr(X))a__sqr(mark(X))mark(add(X1, X2))a__add(mark(X1), mark(X2))
mark(dbl(X))a__dbl(mark(X))mark(first(X1, X2))a__first(mark(X1), mark(X2))
mark(cons(X1, X2))cons(mark(X1), X2)mark(recip(X))recip(mark(X))
mark(s(X))s(X)mark(0)0
mark(nil)nila__terms(X)terms(X)
a__sqr(X)sqr(X)a__add(X1, X2)add(X1, X2)
a__dbl(X)dbl(X)a__first(X1, X2)first(X1, X2)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, mark, dbl, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, nil, cons

Strategy


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:

mark#(add(X1, X2))mark#(X2)mark#(add(X1, X2))mark#(X1)

Problem 7: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(recip(X))mark#(X)mark#(cons(X1, X2))mark#(X1)

Rewrite Rules

a__terms(N)cons(recip(a__sqr(mark(N))), terms(s(N)))a__sqr(0)0
a__sqr(s(X))s(add(sqr(X), dbl(X)))a__dbl(0)0
a__dbl(s(X))s(s(dbl(X)))a__add(0, X)mark(X)
a__add(s(X), Y)s(add(X, Y))a__first(0, X)nil
a__first(s(X), cons(Y, Z))cons(mark(Y), first(X, Z))mark(terms(X))a__terms(mark(X))
mark(sqr(X))a__sqr(mark(X))mark(add(X1, X2))a__add(mark(X1), mark(X2))
mark(dbl(X))a__dbl(mark(X))mark(first(X1, X2))a__first(mark(X1), mark(X2))
mark(cons(X1, X2))cons(mark(X1), X2)mark(recip(X))recip(mark(X))
mark(s(X))s(X)mark(0)0
mark(nil)nila__terms(X)terms(X)
a__sqr(X)sqr(X)a__add(X1, X2)add(X1, X2)
a__dbl(X)dbl(X)a__first(X1, X2)first(X1, X2)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, mark, dbl, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, cons, nil

Strategy


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:

mark#(recip(X))mark#(X)

Problem 8: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(cons(X1, X2))mark#(X1)

Rewrite Rules

a__terms(N)cons(recip(a__sqr(mark(N))), terms(s(N)))a__sqr(0)0
a__sqr(s(X))s(add(sqr(X), dbl(X)))a__dbl(0)0
a__dbl(s(X))s(s(dbl(X)))a__add(0, X)mark(X)
a__add(s(X), Y)s(add(X, Y))a__first(0, X)nil
a__first(s(X), cons(Y, Z))cons(mark(Y), first(X, Z))mark(terms(X))a__terms(mark(X))
mark(sqr(X))a__sqr(mark(X))mark(add(X1, X2))a__add(mark(X1), mark(X2))
mark(dbl(X))a__dbl(mark(X))mark(first(X1, X2))a__first(mark(X1), mark(X2))
mark(cons(X1, X2))cons(mark(X1), X2)mark(recip(X))recip(mark(X))
mark(s(X))s(X)mark(0)0
mark(nil)nila__terms(X)terms(X)
a__sqr(X)sqr(X)a__add(X1, X2)add(X1, X2)
a__dbl(X)dbl(X)a__first(X1, X2)first(X1, X2)

Original Signature

Termination of terms over the following signature is verified: terms, sqr, mark, dbl, recip, add, a__add, a__terms, 0, s, a__dbl, first, a__first, a__sqr, nil, cons

Strategy


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:

mark#(cons(X1, X2))mark#(X1)