YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (4ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (58ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

plus#(s(x), y)plus#(x, y)plus#(s(x), y)U21#(plus(x, y), y, x)

Rewrite Rules

plus(x, 0)xplus(0, x)x
plus(s(x), y)U21(plus(x, y), y, x)U21(z, y, x)s(z)

Original Signature

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

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = ∅
μ(s) = μ(U21#) = μ(U21) = {1}
μ(plus) = μ(plus#) = {1, 2}


The following SCCs where found

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

Problem 2: PolynomialLinearRange4



Dependency Pair Problem

Dependency Pairs

plus#(s(x), y)plus#(x, y)

Rewrite Rules

plus(x, 0)xplus(0, x)x
plus(s(x), y)U21(plus(x, y), y, x)U21(z, y, x)s(z)

Original Signature

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

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = ∅
μ(s) = μ(U21#) = μ(U21) = {1}
μ(plus) = μ(plus#) = {1, 2}


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:

plus#(s(x), y)plus#(x, y)