YES

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

The following DP Processors were used


Problem 1 was processed with processor PolynomialLinearRange4iUR (1710ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (1199ms).
 |    | – Problem 3 was processed with processor DependencyGraph (2ms).
 |    |    | – Problem 4 was processed with processor PolynomialLinearRange4iUR (15ms).
 |    |    |    | – Problem 5 was processed with processor PolynomialLinearRange4iUR (10ms).

Problem 1: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(plus(X1, X2))a__plus#(mark(X1), mark(X2))a__plus#(N, s(M))a__U11#(tt, M, N)
a__U12#(tt, M, N)mark#(M)mark#(plus(X1, X2))mark#(X1)
a__U11#(tt, M, N)a__U12#(tt, M, N)mark#(plus(X1, X2))mark#(X2)
a__U12#(tt, M, N)mark#(N)mark#(U12(X1, X2, X3))a__U12#(mark(X1), X2, X3)
mark#(s(X))mark#(X)a__plus#(N, 0)mark#(N)
mark#(U12(X1, X2, X3))mark#(X1)mark#(U11(X1, X2, X3))a__U11#(mark(X1), X2, X3)
mark#(U11(X1, X2, X3))mark#(X1)a__U12#(tt, M, N)a__plus#(mark(N), mark(M))

Rewrite Rules

a__U11(tt, M, N)a__U12(tt, M, N)a__U12(tt, M, N)s(a__plus(mark(N), mark(M)))
a__plus(N, 0)mark(N)a__plus(N, s(M))a__U11(tt, M, N)
mark(U11(X1, X2, X3))a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3))a__U12(mark(X1), X2, X3)
mark(plus(X1, X2))a__plus(mark(X1), mark(X2))mark(tt)tt
mark(s(X))s(mark(X))mark(0)0
a__U11(X1, X2, X3)U11(X1, X2, X3)a__U12(X1, X2, X3)U12(X1, X2, X3)
a__plus(X1, X2)plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: plus, 0, s, tt, a__plus, U11, a__U12, mark, U12, a__U11

Strategy


Polynomial Interpretation

Improved Usable rules

mark(tt)tta__U11(X1, X2, X3)U11(X1, X2, X3)
mark(0)0a__plus(N, 0)mark(N)
a__plus(X1, X2)plus(X1, X2)a__U12(X1, X2, X3)U12(X1, X2, X3)
mark(U12(X1, X2, X3))a__U12(mark(X1), X2, X3)a__plus(N, s(M))a__U11(tt, M, N)
a__U11(tt, M, N)a__U12(tt, M, N)mark(s(X))s(mark(X))
a__U12(tt, M, N)s(a__plus(mark(N), mark(M)))mark(plus(X1, X2))a__plus(mark(X1), mark(X2))
mark(U11(X1, X2, X3))a__U11(mark(X1), X2, X3)

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

a__plus#(N, 0)mark#(N)

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(plus(X1, X2))a__plus#(mark(X1), mark(X2))a__plus#(N, s(M))a__U11#(tt, M, N)
a__U12#(tt, M, N)mark#(M)mark#(plus(X1, X2))mark#(X1)
a__U11#(tt, M, N)a__U12#(tt, M, N)mark#(plus(X1, X2))mark#(X2)
a__U12#(tt, M, N)mark#(N)mark#(U12(X1, X2, X3))a__U12#(mark(X1), X2, X3)
mark#(s(X))mark#(X)mark#(U12(X1, X2, X3))mark#(X1)
mark#(U11(X1, X2, X3))a__U11#(mark(X1), X2, X3)mark#(U11(X1, X2, X3))mark#(X1)
a__U12#(tt, M, N)a__plus#(mark(N), mark(M))

Rewrite Rules

a__U11(tt, M, N)a__U12(tt, M, N)a__U12(tt, M, N)s(a__plus(mark(N), mark(M)))
a__plus(N, 0)mark(N)a__plus(N, s(M))a__U11(tt, M, N)
mark(U11(X1, X2, X3))a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3))a__U12(mark(X1), X2, X3)
mark(plus(X1, X2))a__plus(mark(X1), mark(X2))mark(tt)tt
mark(s(X))s(mark(X))mark(0)0
a__U11(X1, X2, X3)U11(X1, X2, X3)a__U12(X1, X2, X3)U12(X1, X2, X3)
a__plus(X1, X2)plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: plus, 0, s, tt, a__plus, U11, U12, mark, a__U12, a__U11

Strategy


Polynomial Interpretation

Improved Usable rules

mark(tt)tta__U11(X1, X2, X3)U11(X1, X2, X3)
mark(0)0a__plus(N, 0)mark(N)
a__plus(X1, X2)plus(X1, X2)a__U12(X1, X2, X3)U12(X1, X2, X3)
mark(U12(X1, X2, X3))a__U12(mark(X1), X2, X3)a__plus(N, s(M))a__U11(tt, M, N)
a__U11(tt, M, N)a__U12(tt, M, N)mark(s(X))s(mark(X))
a__U12(tt, M, N)s(a__plus(mark(N), mark(M)))mark(plus(X1, X2))a__plus(mark(X1), mark(X2))
mark(U11(X1, X2, X3))a__U11(mark(X1), X2, X3)

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

mark#(plus(X1, X2))a__plus#(mark(X1), mark(X2))a__U12#(tt, M, N)mark#(M)
mark#(plus(X1, X2))mark#(X1)mark#(plus(X1, X2))mark#(X2)
a__U12#(tt, M, N)mark#(N)mark#(s(X))mark#(X)
a__U12#(tt, M, N)a__plus#(mark(N), mark(M))

Problem 3: DependencyGraph



Dependency Pair Problem

Dependency Pairs

a__U11#(tt, M, N)a__U12#(tt, M, N)mark#(U12(X1, X2, X3))a__U12#(mark(X1), X2, X3)
mark#(U12(X1, X2, X3))mark#(X1)a__plus#(N, s(M))a__U11#(tt, M, N)
mark#(U11(X1, X2, X3))a__U11#(mark(X1), X2, X3)mark#(U11(X1, X2, X3))mark#(X1)

Rewrite Rules

a__U11(tt, M, N)a__U12(tt, M, N)a__U12(tt, M, N)s(a__plus(mark(N), mark(M)))
a__plus(N, 0)mark(N)a__plus(N, s(M))a__U11(tt, M, N)
mark(U11(X1, X2, X3))a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3))a__U12(mark(X1), X2, X3)
mark(plus(X1, X2))a__plus(mark(X1), mark(X2))mark(tt)tt
mark(s(X))s(mark(X))mark(0)0
a__U11(X1, X2, X3)U11(X1, X2, X3)a__U12(X1, X2, X3)U12(X1, X2, X3)
a__plus(X1, X2)plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: plus, 0, s, tt, a__plus, U11, a__U12, mark, U12, a__U11

Strategy


The following SCCs where found

mark#(U12(X1, X2, X3)) → mark#(X1)mark#(U11(X1, X2, X3)) → mark#(X1)

Problem 4: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(U12(X1, X2, X3))mark#(X1)mark#(U11(X1, X2, X3))mark#(X1)

Rewrite Rules

a__U11(tt, M, N)a__U12(tt, M, N)a__U12(tt, M, N)s(a__plus(mark(N), mark(M)))
a__plus(N, 0)mark(N)a__plus(N, s(M))a__U11(tt, M, N)
mark(U11(X1, X2, X3))a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3))a__U12(mark(X1), X2, X3)
mark(plus(X1, X2))a__plus(mark(X1), mark(X2))mark(tt)tt
mark(s(X))s(mark(X))mark(0)0
a__U11(X1, X2, X3)U11(X1, X2, X3)a__U12(X1, X2, X3)U12(X1, X2, X3)
a__plus(X1, X2)plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: plus, 0, s, tt, a__plus, U11, a__U12, mark, U12, a__U11

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#(U11(X1, X2, X3))mark#(X1)

Problem 5: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

mark#(U12(X1, X2, X3))mark#(X1)

Rewrite Rules

a__U11(tt, M, N)a__U12(tt, M, N)a__U12(tt, M, N)s(a__plus(mark(N), mark(M)))
a__plus(N, 0)mark(N)a__plus(N, s(M))a__U11(tt, M, N)
mark(U11(X1, X2, X3))a__U11(mark(X1), X2, X3)mark(U12(X1, X2, X3))a__U12(mark(X1), X2, X3)
mark(plus(X1, X2))a__plus(mark(X1), mark(X2))mark(tt)tt
mark(s(X))s(mark(X))mark(0)0
a__U11(X1, X2, X3)U11(X1, X2, X3)a__U12(X1, X2, X3)U12(X1, X2, X3)
a__plus(X1, X2)plus(X1, X2)

Original Signature

Termination of terms over the following signature is verified: plus, 0, s, tt, a__plus, U11, U12, mark, a__U12, a__U11

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#(U12(X1, X2, X3))mark#(X1)