MAYBE

The TRS could not be proven terminating. The proof attempt took 396 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 (97ms), DependencyGraph (1ms), PolynomialLinearRange8NegiUR (104ms), DependencyGraph (2ms), ReductionPairSAT (36ms), 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)activate(X)
if(false, X, Y)activate(Y)diff(X, Y)if(leq(X, Y), n__0, n__s(diff(p(X), Y)))
0n__0s(X)n__s(X)
activate(n__0)0activate(n__s(X))s(X)
activate(X)X

Original Signature

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


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

leq#(s(X), s(Y))leq#(X, Y)if#(true, X, Y)activate#(X)
if#(false, X, Y)activate#(Y)activate#(n__0)0#
diff#(X, Y)diff#(p(X), Y)diff#(X, Y)if#(leq(X, Y), n__0, n__s(diff(p(X), Y)))
p#(0)0#diff#(X, Y)p#(X)
diff#(X, Y)leq#(X, Y)activate#(n__s(X))s#(X)

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)activate(X)
if(false, X, Y)activate(Y)diff(X, Y)if(leq(X, Y), n__0, n__s(diff(p(X), Y)))
0n__0s(X)n__s(X)
activate(n__0)0activate(n__s(X))s(X)
activate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, n__s, 0, n__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)activate(X)
if(false, X, Y)activate(Y)diff(X, Y)if(leq(X, Y), n__0, n__s(diff(p(X), Y)))
0n__0s(X)n__s(X)
activate(n__0)0activate(n__s(X))s(X)
activate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, n__s, 0, n__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)