MAYBE

The TRS could not be proven terminating. The proof attempt took 363 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 (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)0p(s(X))X
leq(0, Y)trueleq(s(X), 0)false
leq(s(X), s(Y))leq(X, Y)if(true, X, Y)X
if(false, X, Y)Ydiff(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)0p(s(X))X
leq(0, Y)trueleq(s(X), 0)false
leq(s(X), s(Y))leq(X, Y)if(true, X, Y)X
if(false, X, Y)Ydiff(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)0p(s(X))X
leq(0, Y)trueleq(s(X), 0)false
leq(s(X), s(Y))leq(X, Y)if(true, X, Y)X
if(false, X, Y)Ydiff(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:

Thus, the following dependency pairs are removed:

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