MAYBE

The TRS could not be proven terminating. The proof attempt took 651 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (0ms).
 | – Problem 2 was processed with processor SubtermCriterion (0ms).
 | – Problem 3 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (134ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (195ms), DependencyGraph (2ms), ReductionPairSAT (153ms), DependencyGraph (2ms), SizeChangePrinciple (18ms)].

The following open problems remain:



Open Dependency Pair Problem 3

Dependency Pairs

minus#(x, y)cond#(min(x, y), x, y)cond#(y, x, y)minus#(x, s(y))

Rewrite Rules

minus(x, y)cond(min(x, y), x, y)cond(y, x, y)s(minus(x, s(y)))
min(0, v)0min(u, 0)0
min(s(u), s(v))s(min(u, v))

Original Signature

Termination of terms over the following signature is verified: min, 0, minus, s, cond


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

minus#(x, y)min#(x, y)minus#(x, y)cond#(min(x, y), x, y)
cond#(y, x, y)minus#(x, s(y))min#(s(u), s(v))min#(u, v)

Rewrite Rules

minus(x, y)cond(min(x, y), x, y)cond(y, x, y)s(minus(x, s(y)))
min(0, v)0min(u, 0)0
min(s(u), s(v))s(min(u, v))

Original Signature

Termination of terms over the following signature is verified: min, minus, 0, s, cond

Strategy


The following SCCs where found

minus#(x, y) → cond#(min(x, y), x, y)cond#(y, x, y) → minus#(x, s(y))

min#(s(u), s(v)) → min#(u, v)

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

min#(s(u), s(v))min#(u, v)

Rewrite Rules

minus(x, y)cond(min(x, y), x, y)cond(y, x, y)s(minus(x, s(y)))
min(0, v)0min(u, 0)0
min(s(u), s(v))s(min(u, v))

Original Signature

Termination of terms over the following signature is verified: min, minus, 0, s, cond

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

min#(s(u), s(v))min#(u, v)