YES

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (7ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4 (89ms).

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

and#(tt, X) → T(X)plus#(N, s(M)) → plus#(N, M)

Rewrite Rules

and(tt, X) → Xplus(N, 0) → N
plus(N, s(M)) → s(plus(N, M))

Original Signature

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

Strategy

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

The following SCCs where found

plus#(N, s(M)) → plus#(N, M)

Problem 2: PolynomialLinearRange4

Dependency Pair Problem

Dependency Pairs

plus#(N, s(M)) → plus#(N, M)

Rewrite Rules

and(tt, X) → Xplus(N, 0) → N
plus(N, s(M)) → s(plus(N, M))

Original Signature

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

Strategy

Context-sensitive strategy:
μ(T) = μ(0) = μ(tt) = ∅
μ(s) = μ(and#) = μ(and) = {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#(N, s(M)) → plus#(N, M)