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)	→	0	min(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)	→	0	min(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)	→	0	min(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:

π (min#): 1

Thus, the following dependency pairs are removed:

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

→

min^#(u, v)