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 (0ms), DependencyGraph (1ms), PolynomialLinearRange4iUR (95ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (100ms), DependencyGraph (1ms), ReductionPairSAT (31ms), DependencyGraph (1ms), SizeChangePrinciple (4ms)].

The following open problems remain:

Open Dependency Pair Problem 3

Dependency Pairs

diff^#(X, Y)

→

diff^#(p(X), Y)

Rewrite Rules

p(0)	→	0	p(s(X))	→	X
leq(0, Y)	→	true	leq(s(X), 0)	→	false
leq(s(X), s(Y))	→	leq(X, Y)	if(true, X, Y)	→	X
if(false, X, Y)	→	Y	diff(X, Y)	→	if(leq(X, Y), 0, s(diff(p(X), Y)))

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, if, leq, p, false, true

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

leq^#(s(X), s(Y))	→	leq^#(X, Y)	diff^#(X, Y)	→	if^#(leq(X, Y), 0, s(diff(p(X), Y)))
diff^#(X, Y)	→	diff^#(p(X), Y)	diff^#(X, Y)	→	p^#(X)
diff^#(X, Y)	→	leq^#(X, Y)

Rewrite Rules

p(0)	→	0	p(s(X))	→	X
leq(0, Y)	→	true	leq(s(X), 0)	→	false
leq(s(X), s(Y))	→	leq(X, Y)	if(true, X, Y)	→	X
if(false, X, Y)	→	Y	diff(X, Y)	→	if(leq(X, Y), 0, s(diff(p(X), Y)))

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, leq, if, p, true, false

Strategy

The following SCCs where found

leq^#(s(X), s(Y)) → leq^#(X, Y)

diff^#(X, Y) → diff^#(p(X), Y)

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

leq^#(s(X), s(Y))

→

leq^#(X, Y)

Rewrite Rules

p(0)	→	0	p(s(X))	→	X
leq(0, Y)	→	true	leq(s(X), 0)	→	false
leq(s(X), s(Y))	→	leq(X, Y)	if(true, X, Y)	→	X
if(false, X, Y)	→	Y	diff(X, Y)	→	if(leq(X, Y), 0, s(diff(p(X), Y)))

Original Signature

Termination of terms over the following signature is verified: 0, s, diff, leq, if, p, true, false

Strategy

Projection

The following projection was used:

π (leq#): 1

Thus, the following dependency pairs are removed:

leq^#(s(X), s(Y))

→

leq^#(X, Y)