YES

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

The following DP Processors were used


Problem 1 was processed with processor PolynomialLinearRange4iUR (294ms).
 | – Problem 2 was processed with processor ReductionPairSAT (14688ms).

Problem 1: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

p#(a(x0), p(a(b(x1)), x2)) → p#(a(b(a(x2))), p(a(a(x1)), x2))p#(a(x0), p(a(b(x1)), x2)) → p#(a(a(x1)), x2)

Rewrite Rules

p(a(x0), p(a(b(x1)), x2)) → p(a(b(a(x2))), p(a(a(x1)), x2))

Original Signature

Termination of terms over the following signature is verified: b, p, a

Strategy

Polynomial Interpretation

Improved Usable rules

p(a(x0), p(a(b(x1)), x2)) → p(a(b(a(x2))), p(a(a(x1)), x2))

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

p#(a(x0), p(a(b(x1)), x2)) → p#(a(a(x1)), x2)

Problem 2: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

p#(a(x0), p(a(b(x1)), x2)) → p#(a(b(a(x2))), p(a(a(x1)), x2))

Rewrite Rules

p(a(x0), p(a(b(x1)), x2)) → p(a(b(a(x2))), p(a(a(x1)), x2))

Original Signature

Termination of terms over the following signature is verified: b, a, p

Strategy

Function Precedence

p < p# = b = a

Argument Filtering

p#: 1 2
b: 1
a: collapses to 1
p: 1 2

Status

p#: multiset
b: multiset
p: multiset

Usable Rules

p(a(x0), p(a(b(x1)), x2)) → p(a(b(a(x2))), p(a(a(x1)), x2))

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

p#(a(x0), p(a(b(x1)), x2)) → p#(a(b(a(x2))), p(a(a(x1)), x2))