YES

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

The following DP Processors were used


Problem 1 was processed with processor PolynomialLinearRange4iUR (168ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (40ms).

Problem 1: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

average#(x, s(s(s(y)))) → average#(s(x), y)average#(s(x), y) → average#(x, s(y))

Rewrite Rules

average(s(x), y) → average(x, s(y))average(x, s(s(s(y)))) → s(average(s(x), y))
average(0, 0) → 0average(0, s(0)) → 0
average(0, s(s(0))) → s(0)

Original Signature

Termination of terms over the following signature is verified: 0, s, average

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:

average#(x, s(s(s(y)))) → average#(s(x), y)

Problem 2: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

average#(s(x), y) → average#(x, s(y))

Rewrite Rules

average(s(x), y) → average(x, s(y))average(x, s(s(s(y)))) → s(average(s(x), y))
average(0, 0) → 0average(0, s(0)) → 0
average(0, s(s(0))) → s(0)

Original Signature

Termination of terms over the following signature is verified: 0, s, average

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:

average#(s(x), y) → average#(x, s(y))