YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (169ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (2457ms).
 |    | – Problem 3 was processed with processor PolynomialLinearRange4iUR (2685ms).
 |    |    | – Problem 4 was processed with processor DependencyGraph (11ms).
 |    |    |    | – Problem 5 was processed with processor PolynomialLinearRange4iUR (1279ms).
 |    |    |    |    | – Problem 6 was processed with processor DependencyGraph (4ms).
 |    |    |    |    |    | – Problem 7 was processed with processor PolynomialLinearRange4iUR (313ms).
 |    |    |    |    |    |    | – Problem 8 was processed with processor PolynomialLinearRange4iUR (12ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

a__from#(X)mark#(X)a__zWadr#(cons(X, XS), cons(Y, YS))mark#(Y)
mark#(zWadr(X1, X2))a__zWadr#(mark(X1), mark(X2))mark#(from(X))a__from#(mark(X))
mark#(zWadr(X1, X2))mark#(X2)mark#(prefix(X))a__prefix#(mark(X))
mark#(from(X))mark#(X)mark#(cons(X1, X2))mark#(X1)
mark#(prefix(X))mark#(X)a__zWadr#(cons(X, XS), cons(Y, YS))mark#(X)
mark#(app(X1, X2))a__app#(mark(X1), mark(X2))a__app#(cons(X, XS), YS)mark#(X)
mark#(app(X1, X2))mark#(X1)a__zWadr#(cons(X, XS), cons(Y, YS))a__app#(mark(Y), cons(mark(X), nil))
mark#(zWadr(X1, X2))mark#(X1)mark#(s(X))mark#(X)
a__app#(nil, YS)mark#(YS)mark#(app(X1, X2))mark#(X2)

Rewrite Rules

a__app(nil, YS)mark(YS)a__app(cons(X, XS), YS)cons(mark(X), app(XS, YS))
a__from(X)cons(mark(X), from(s(X)))a__zWadr(nil, YS)nil
a__zWadr(XS, nil)nila__zWadr(cons(X, XS), cons(Y, YS))cons(a__app(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))
a__prefix(L)cons(nil, zWadr(L, prefix(L)))mark(app(X1, X2))a__app(mark(X1), mark(X2))
mark(from(X))a__from(mark(X))mark(zWadr(X1, X2))a__zWadr(mark(X1), mark(X2))
mark(prefix(X))a__prefix(mark(X))mark(nil)nil
mark(cons(X1, X2))cons(mark(X1), X2)mark(s(X))s(mark(X))
a__app(X1, X2)app(X1, X2)a__from(X)from(X)
a__zWadr(X1, X2)zWadr(X1, X2)a__prefix(X)prefix(X)

Original Signature

Termination of terms over the following signature is verified: app, zWadr, a__app, s, prefix, mark, from, a__zWadr, a__prefix, a__from, nil, cons

Strategy


The following SCCs where found

a__from#(X) → mark#(X)a__zWadr#(cons(X, XS), cons(Y, YS)) → mark#(Y)
mark#(zWadr(X1, X2)) → a__zWadr#(mark(X1), mark(X2))mark#(from(X)) → a__from#(mark(X))
mark#(zWadr(X1, X2)) → mark#(X2)mark#(from(X)) → mark#(X)
mark#(cons(X1, X2)) → mark#(X1)mark#(prefix(X)) → mark#(X)
a__zWadr#(cons(X, XS), cons(Y, YS)) → mark#(X)mark#(app(X1, X2)) → a__app#(mark(X1), mark(X2))
a__app#(cons(X, XS), YS) → mark#(X)mark#(app(X1, X2)) → mark#(X1)
a__zWadr#(cons(X, XS), cons(Y, YS)) → a__app#(mark(Y), cons(mark(X), nil))mark#(zWadr(X1, X2)) → mark#(X1)
mark#(s(X)) → mark#(X)a__app#(nil, YS) → mark#(YS)
mark#(app(X1, X2)) → mark#(X2)

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

a__from#(X)mark#(X)mark#(zWadr(X1, X2))a__zWadr#(mark(X1), mark(X2))
a__zWadr#(cons(X, XS), cons(Y, YS))mark#(Y)mark#(from(X))a__from#(mark(X))
mark#(zWadr(X1, X2))mark#(X2)mark#(from(X))mark#(X)
mark#(cons(X1, X2))mark#(X1)mark#(prefix(X))mark#(X)
mark#(app(X1, X2))a__app#(mark(X1), mark(X2))a__zWadr#(cons(X, XS), cons(Y, YS))mark#(X)
mark#(app(X1, X2))mark#(X1)a__app#(cons(X, XS), YS)mark#(X)
a__zWadr#(cons(X, XS), cons(Y, YS))a__app#(mark(Y), cons(mark(X), nil))mark#(zWadr(X1, X2))mark#(X1)
mark#(s(X))mark#(X)a__app#(nil, YS)mark#(YS)
mark#(app(X1, X2))mark#(X2)

Rewrite Rules

a__app(nil, YS)mark(YS)a__app(cons(X, XS), YS)cons(mark(X), app(XS, YS))
a__from(X)cons(mark(X), from(s(X)))a__zWadr(nil, YS)nil
a__zWadr(XS, nil)nila__zWadr(cons(X, XS), cons(Y, YS))cons(a__app(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))
a__prefix(L)cons(nil, zWadr(L, prefix(L)))mark(app(X1, X2))a__app(mark(X1), mark(X2))
mark(from(X))a__from(mark(X))mark(zWadr(X1, X2))a__zWadr(mark(X1), mark(X2))
mark(prefix(X))a__prefix(mark(X))mark(nil)nil
mark(cons(X1, X2))cons(mark(X1), X2)mark(s(X))s(mark(X))
a__app(X1, X2)app(X1, X2)a__from(X)from(X)
a__zWadr(X1, X2)zWadr(X1, X2)a__prefix(X)prefix(X)

Original Signature

Termination of terms over the following signature is verified: app, zWadr, a__app, s, prefix, mark, from, a__zWadr, a__prefix, a__from, nil, cons

Strategy


Polynomial Interpretation

Improved Usable rules

a__prefix(L)cons(nil, zWadr(L, prefix(L)))a__zWadr(nil, YS)nil
mark(cons(X1, X2))cons(mark(X1), X2)a__from(X)from(X)
a__from(X)cons(mark(X), from(s(X)))a__app(X1, X2)app(X1, X2)
mark(app(X1, X2))a__app(mark(X1), mark(X2))a__zWadr(XS, nil)nil
a__zWadr(cons(X, XS), cons(Y, YS))cons(a__app(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))a__zWadr(X1, X2)zWadr(X1, X2)
mark(s(X))s(mark(X))mark(from(X))a__from(mark(X))
mark(zWadr(X1, X2))a__zWadr(mark(X1), mark(X2))mark(nil)nil
a__app(nil, YS)mark(YS)mark(prefix(X))a__prefix(mark(X))
a__app(cons(X, XS), YS)cons(mark(X), app(XS, YS))a__prefix(X)prefix(X)

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

mark#(prefix(X))mark#(X)a__app#(nil, YS)mark#(YS)

Problem 3: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

a__from#(X)mark#(X)mark#(zWadr(X1, X2))a__zWadr#(mark(X1), mark(X2))
a__zWadr#(cons(X, XS), cons(Y, YS))mark#(Y)mark#(from(X))a__from#(mark(X))
mark#(zWadr(X1, X2))mark#(X2)mark#(from(X))mark#(X)
mark#(cons(X1, X2))mark#(X1)mark#(app(X1, X2))a__app#(mark(X1), mark(X2))
a__zWadr#(cons(X, XS), cons(Y, YS))mark#(X)mark#(app(X1, X2))mark#(X1)
a__app#(cons(X, XS), YS)mark#(X)a__zWadr#(cons(X, XS), cons(Y, YS))a__app#(mark(Y), cons(mark(X), nil))
mark#(zWadr(X1, X2))mark#(X1)mark#(s(X))mark#(X)
mark#(app(X1, X2))mark#(X2)

Rewrite Rules

a__app(nil, YS)mark(YS)a__app(cons(X, XS), YS)cons(mark(X), app(XS, YS))
a__from(X)cons(mark(X), from(s(X)))a__zWadr(nil, YS)nil
a__zWadr(XS, nil)nila__zWadr(cons(X, XS), cons(Y, YS))cons(a__app(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))
a__prefix(L)cons(nil, zWadr(L, prefix(L)))mark(app(X1, X2))a__app(mark(X1), mark(X2))
mark(from(X))a__from(mark(X))mark(zWadr(X1, X2))a__zWadr(mark(X1), mark(X2))
mark(prefix(X))a__prefix(mark(X))mark(nil)nil
mark(cons(X1, X2))cons(mark(X1), X2)mark(s(X))s(mark(X))
a__app(X1, X2)app(X1, X2)a__from(X)from(X)
a__zWadr(X1, X2)zWadr(X1, X2)a__prefix(X)prefix(X)

Original Signature

Termination of terms over the following signature is verified: app, zWadr, a__app, s, prefix, mark, a__zWadr, from, a__prefix, a__from, cons, nil

Strategy


Polynomial Interpretation

Improved Usable rules

a__prefix(L)cons(nil, zWadr(L, prefix(L)))a__zWadr(nil, YS)nil
mark(cons(X1, X2))cons(mark(X1), X2)a__from(X)from(X)
a__from(X)cons(mark(X), from(s(X)))a__app(X1, X2)app(X1, X2)
mark(app(X1, X2))a__app(mark(X1), mark(X2))a__zWadr(XS, nil)nil
a__zWadr(cons(X, XS), cons(Y, YS))cons(a__app(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))a__zWadr(X1, X2)zWadr(X1, X2)
mark(s(X))s(mark(X))mark(from(X))a__from(mark(X))
mark(zWadr(X1, X2))a__zWadr(mark(X1), mark(X2))mark(nil)nil
a__app(nil, YS)mark(YS)mark(prefix(X))a__prefix(mark(X))
a__app(cons(X, XS), YS)cons(mark(X), app(XS, YS))a__prefix(X)prefix(X)

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

a__from#(X)mark#(X)mark#(from(X))mark#(X)

Problem 4: DependencyGraph



Dependency Pair Problem

Dependency Pairs

mark#(zWadr(X1, X2))a__zWadr#(mark(X1), mark(X2))a__zWadr#(cons(X, XS), cons(Y, YS))mark#(Y)
mark#(from(X))a__from#(mark(X))mark#(zWadr(X1, X2))mark#(X2)
mark#(cons(X1, X2))mark#(X1)mark#(app(X1, X2))a__app#(mark(X1), mark(X2))
a__zWadr#(cons(X, XS), cons(Y, YS))mark#(X)mark#(app(X1, X2))mark#(X1)
a__app#(cons(X, XS), YS)mark#(X)a__zWadr#(cons(X, XS), cons(Y, YS))a__app#(mark(Y), cons(mark(X), nil))
mark#(zWadr(X1, X2))mark#(X1)mark#(s(X))mark#(X)
mark#(app(X1, X2))mark#(X2)

Rewrite Rules

a__app(nil, YS)mark(YS)a__app(cons(X, XS), YS)cons(mark(X), app(XS, YS))
a__from(X)cons(mark(X), from(s(X)))a__zWadr(nil, YS)nil
a__zWadr(XS, nil)nila__zWadr(cons(X, XS), cons(Y, YS))cons(a__app(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))
a__prefix(L)cons(nil, zWadr(L, prefix(L)))mark(app(X1, X2))a__app(mark(X1), mark(X2))
mark(from(X))a__from(mark(X))mark(zWadr(X1, X2))a__zWadr(mark(X1), mark(X2))
mark(prefix(X))a__prefix(mark(X))mark(nil)nil
mark(cons(X1, X2))cons(mark(X1), X2)mark(s(X))s(mark(X))
a__app(X1, X2)app(X1, X2)a__from(X)from(X)
a__zWadr(X1, X2)zWadr(X1, X2)a__prefix(X)prefix(X)

Original Signature

Termination of terms over the following signature is verified: app, zWadr, a__app, s, prefix, mark, from, a__zWadr, a__prefix, a__from, nil, cons

Strategy


The following SCCs where found

a__zWadr#(cons(X, XS), cons(Y, YS)) → mark#(Y)mark#(zWadr(X1, X2)) → a__zWadr#(mark(X1), mark(X2))
mark#(app(X1, X2)) → a__app#(mark(X1), mark(X2))a__zWadr#(cons(X, XS), cons(Y, YS)) → mark#(X)
a__app#(cons(X, XS), YS) → mark#(X)mark#(zWadr(X1, X2)) → mark#(X2)
mark#(app(X1, X2)) → mark#(X1)a__zWadr#(cons(X, XS), cons(Y, YS)) → a__app#(mark(Y), cons(mark(X), nil))
mark#(cons(X1, X2)) → mark#(X1)mark#(zWadr(X1, X2)) → mark#(X1)
mark#(s(X)) → mark#(X)mark#(app(X1, X2)) → mark#(X2)

Problem 5: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

a__zWadr#(cons(X, XS), cons(Y, YS))mark#(Y)mark#(zWadr(X1, X2))a__zWadr#(mark(X1), mark(X2))
mark#(app(X1, X2))a__app#(mark(X1), mark(X2))a__zWadr#(cons(X, XS), cons(Y, YS))mark#(X)
a__app#(cons(X, XS), YS)mark#(X)mark#(app(X1, X2))mark#(X1)
mark#(zWadr(X1, X2))mark#(X2)a__zWadr#(cons(X, XS), cons(Y, YS))a__app#(mark(Y), cons(mark(X), nil))
mark#(cons(X1, X2))mark#(X1)mark#(zWadr(X1, X2))mark#(X1)
mark#(s(X))mark#(X)mark#(app(X1, X2))mark#(X2)

Rewrite Rules

a__app(nil, YS)mark(YS)a__app(cons(X, XS), YS)cons(mark(X), app(XS, YS))
a__from(X)cons(mark(X), from(s(X)))a__zWadr(nil, YS)nil
a__zWadr(XS, nil)nila__zWadr(cons(X, XS), cons(Y, YS))cons(a__app(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))
a__prefix(L)cons(nil, zWadr(L, prefix(L)))mark(app(X1, X2))a__app(mark(X1), mark(X2))
mark(from(X))a__from(mark(X))mark(zWadr(X1, X2))a__zWadr(mark(X1), mark(X2))
mark(prefix(X))a__prefix(mark(X))mark(nil)nil
mark(cons(X1, X2))cons(mark(X1), X2)mark(s(X))s(mark(X))
a__app(X1, X2)app(X1, X2)a__from(X)from(X)
a__zWadr(X1, X2)zWadr(X1, X2)a__prefix(X)prefix(X)

Original Signature

Termination of terms over the following signature is verified: app, zWadr, a__app, s, prefix, mark, from, a__zWadr, a__prefix, a__from, nil, cons

Strategy


Polynomial Interpretation

Improved Usable rules

a__prefix(L)cons(nil, zWadr(L, prefix(L)))a__zWadr(nil, YS)nil
mark(cons(X1, X2))cons(mark(X1), X2)a__from(X)from(X)
a__from(X)cons(mark(X), from(s(X)))a__app(X1, X2)app(X1, X2)
mark(app(X1, X2))a__app(mark(X1), mark(X2))a__zWadr(XS, nil)nil
a__zWadr(cons(X, XS), cons(Y, YS))cons(a__app(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))a__zWadr(X1, X2)zWadr(X1, X2)
mark(s(X))s(mark(X))mark(from(X))a__from(mark(X))
mark(zWadr(X1, X2))a__zWadr(mark(X1), mark(X2))mark(nil)nil
a__app(nil, YS)mark(YS)mark(prefix(X))a__prefix(mark(X))
a__app(cons(X, XS), YS)cons(mark(X), app(XS, YS))a__prefix(X)prefix(X)

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

mark#(zWadr(X1, X2))a__zWadr#(mark(X1), mark(X2))mark#(zWadr(X1, X2))mark#(X2)
mark#(zWadr(X1, X2))mark#(X1)mark#(s(X))mark#(X)

Problem 6: DependencyGraph



Dependency Pair Problem

Dependency Pairs

a__zWadr#(cons(X, XS), cons(Y, YS))mark#(Y)a__zWadr#(cons(X, XS), cons(Y, YS))mark#(X)
mark#(app(X1, X2))a__app#(mark(X1), mark(X2))mark#(app(X1, X2))mark#(X1)
a__app#(cons(X, XS), YS)mark#(X)a__zWadr#(cons(X, XS), cons(Y, YS))a__app#(mark(Y), cons(mark(X), nil))
mark#(cons(X1, X2))mark#(X1)mark#(app(X1, X2))mark#(X2)

Rewrite Rules

a__app(nil, YS)mark(YS)a__app(cons(X, XS), YS)cons(mark(X), app(XS, YS))
a__from(X)cons(mark(X), from(s(X)))a__zWadr(nil, YS)nil
a__zWadr(XS, nil)nila__zWadr(cons(X, XS), cons(Y, YS))cons(a__app(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))
a__prefix(L)cons(nil, zWadr(L, prefix(L)))mark(app(X1, X2))a__app(mark(X1), mark(X2))
mark(from(X))a__from(mark(X))mark(zWadr(X1, X2))a__zWadr(mark(X1), mark(X2))
mark(prefix(X))a__prefix(mark(X))mark(nil)nil
mark(cons(X1, X2))cons(mark(X1), X2)mark(s(X))s(mark(X))
a__app(X1, X2)app(X1, X2)a__from(X)from(X)
a__zWadr(X1, X2)zWadr(X1, X2)a__prefix(X)prefix(X)

Original Signature

Termination of terms over the following signature is verified: app, zWadr, a__app, s, prefix, mark, a__zWadr, from, a__prefix, a__from, cons, nil

Strategy


The following SCCs where found

mark#(app(X1, X2)) → a__app#(mark(X1), mark(X2))a__app#(cons(X, XS), YS) → mark#(X)
mark#(app(X1, X2)) → mark#(X1)mark#(cons(X1, X2)) → mark#(X1)
mark#(app(X1, X2)) → mark#(X2)

Problem 7: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(app(X1, X2))a__app#(mark(X1), mark(X2))a__app#(cons(X, XS), YS)mark#(X)
mark#(app(X1, X2))mark#(X1)mark#(cons(X1, X2))mark#(X1)
mark#(app(X1, X2))mark#(X2)

Rewrite Rules

a__app(nil, YS)mark(YS)a__app(cons(X, XS), YS)cons(mark(X), app(XS, YS))
a__from(X)cons(mark(X), from(s(X)))a__zWadr(nil, YS)nil
a__zWadr(XS, nil)nila__zWadr(cons(X, XS), cons(Y, YS))cons(a__app(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))
a__prefix(L)cons(nil, zWadr(L, prefix(L)))mark(app(X1, X2))a__app(mark(X1), mark(X2))
mark(from(X))a__from(mark(X))mark(zWadr(X1, X2))a__zWadr(mark(X1), mark(X2))
mark(prefix(X))a__prefix(mark(X))mark(nil)nil
mark(cons(X1, X2))cons(mark(X1), X2)mark(s(X))s(mark(X))
a__app(X1, X2)app(X1, X2)a__from(X)from(X)
a__zWadr(X1, X2)zWadr(X1, X2)a__prefix(X)prefix(X)

Original Signature

Termination of terms over the following signature is verified: app, zWadr, a__app, s, prefix, mark, a__zWadr, from, a__prefix, a__from, cons, nil

Strategy


Polynomial Interpretation

Improved Usable rules

a__prefix(L)cons(nil, zWadr(L, prefix(L)))a__zWadr(nil, YS)nil
mark(cons(X1, X2))cons(mark(X1), X2)a__from(X)from(X)
a__from(X)cons(mark(X), from(s(X)))a__app(X1, X2)app(X1, X2)
mark(app(X1, X2))a__app(mark(X1), mark(X2))a__zWadr(XS, nil)nil
a__zWadr(cons(X, XS), cons(Y, YS))cons(a__app(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))a__zWadr(X1, X2)zWadr(X1, X2)
mark(s(X))s(mark(X))mark(from(X))a__from(mark(X))
mark(zWadr(X1, X2))a__zWadr(mark(X1), mark(X2))mark(nil)nil
a__app(nil, YS)mark(YS)mark(prefix(X))a__prefix(mark(X))
a__app(cons(X, XS), YS)cons(mark(X), app(XS, YS))a__prefix(X)prefix(X)

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

mark#(app(X1, X2))a__app#(mark(X1), mark(X2))mark#(app(X1, X2))mark#(X1)
a__app#(cons(X, XS), YS)mark#(X)mark#(app(X1, X2))mark#(X2)

Problem 8: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

a__app(nil, YS)mark(YS)a__app(cons(X, XS), YS)cons(mark(X), app(XS, YS))
a__from(X)cons(mark(X), from(s(X)))a__zWadr(nil, YS)nil
a__zWadr(XS, nil)nila__zWadr(cons(X, XS), cons(Y, YS))cons(a__app(mark(Y), cons(mark(X), nil)), zWadr(XS, YS))
a__prefix(L)cons(nil, zWadr(L, prefix(L)))mark(app(X1, X2))a__app(mark(X1), mark(X2))
mark(from(X))a__from(mark(X))mark(zWadr(X1, X2))a__zWadr(mark(X1), mark(X2))
mark(prefix(X))a__prefix(mark(X))mark(nil)nil
mark(cons(X1, X2))cons(mark(X1), X2)mark(s(X))s(mark(X))
a__app(X1, X2)app(X1, X2)a__from(X)from(X)
a__zWadr(X1, X2)zWadr(X1, X2)a__prefix(X)prefix(X)

Original Signature

Termination of terms over the following signature is verified: app, zWadr, a__app, s, prefix, mark, from, a__zWadr, a__prefix, a__from, 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)