TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (177ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (72ms), PolynomialLinearRange4iUR (timeout), PolynomialLinearRange4iUR (-1ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (70ms), ReductionPairSAT (10937ms), DependencyGraph (57ms), SizeChangePrinciple (timeout)].

The following open problems remain:



Open Dependency Pair Problem 2

Dependency Pairs

activate#(n__div(X1, X2))activate#(X1)activate#(n__div(X1, X2))div#(activate(X1), X2)
activate#(n__s(X))activate#(X)activate#(n__minus(X1, X2))minus#(X1, X2)
minus#(n__s(X), n__s(Y))minus#(activate(X), activate(Y))minus#(n__s(X), n__s(Y))activate#(Y)
geq#(n__s(X), n__s(Y))activate#(X)div#(s(X), n__s(Y))activate#(Y)
geq#(n__s(X), n__s(Y))geq#(activate(X), activate(Y))if#(true, X, Y)activate#(X)
if#(false, X, Y)activate#(Y)div#(s(X), n__s(Y))if#(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
div#(s(X), n__s(Y))geq#(X, activate(Y))geq#(n__s(X), n__s(Y))activate#(Y)
minus#(n__s(X), n__s(Y))activate#(X)

Rewrite Rules

minus(n__0, Y)0minus(n__s(X), n__s(Y))minus(activate(X), activate(Y))
geq(X, n__0)truegeq(n__0, n__s(Y))false
geq(n__s(X), n__s(Y))geq(activate(X), activate(Y))div(0, n__s(Y))0
div(s(X), n__s(Y))if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)if(true, X, Y)activate(X)
if(false, X, Y)activate(Y)0n__0
s(X)n__s(X)div(X1, X2)n__div(X1, X2)
minus(X1, X2)n__minus(X1, X2)activate(n__0)0
activate(n__s(X))s(activate(X))activate(n__div(X1, X2))div(activate(X1), X2)
activate(n__minus(X1, X2))minus(X1, X2)activate(X)X

Original Signature

Termination of terms over the following signature is verified: geq, minus, div, true, n__div, activate, n__s, 0, n__0, n__minus, s, if, false


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

activate#(n__div(X1, X2))activate#(X1)activate#(n__div(X1, X2))div#(activate(X1), X2)
activate#(n__s(X))activate#(X)activate#(n__minus(X1, X2))minus#(X1, X2)
minus#(n__s(X), n__s(Y))minus#(activate(X), activate(Y))minus#(n__s(X), n__s(Y))activate#(Y)
geq#(n__s(X), n__s(Y))activate#(X)div#(s(X), n__s(Y))activate#(Y)
minus#(n__0, Y)0#geq#(n__s(X), n__s(Y))geq#(activate(X), activate(Y))
if#(true, X, Y)activate#(X)if#(false, X, Y)activate#(Y)
div#(0, n__s(Y))0#activate#(n__0)0#
activate#(n__s(X))s#(activate(X))div#(s(X), n__s(Y))if#(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
div#(s(X), n__s(Y))geq#(X, activate(Y))geq#(n__s(X), n__s(Y))activate#(Y)
minus#(n__s(X), n__s(Y))activate#(X)

Rewrite Rules

minus(n__0, Y)0minus(n__s(X), n__s(Y))minus(activate(X), activate(Y))
geq(X, n__0)truegeq(n__0, n__s(Y))false
geq(n__s(X), n__s(Y))geq(activate(X), activate(Y))div(0, n__s(Y))0
div(s(X), n__s(Y))if(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)if(true, X, Y)activate(X)
if(false, X, Y)activate(Y)0n__0
s(X)n__s(X)div(X1, X2)n__div(X1, X2)
minus(X1, X2)n__minus(X1, X2)activate(n__0)0
activate(n__s(X))s(activate(X))activate(n__div(X1, X2))div(activate(X1), X2)
activate(n__minus(X1, X2))minus(X1, X2)activate(X)X

Original Signature

Termination of terms over the following signature is verified: geq, minus, div, true, n__div, activate, n__s, 0, n__0, n__minus, s, if, false

Strategy


The following SCCs where found

activate#(n__div(X1, X2)) → activate#(X1)activate#(n__div(X1, X2)) → div#(activate(X1), X2)
activate#(n__s(X)) → activate#(X)activate#(n__minus(X1, X2)) → minus#(X1, X2)
minus#(n__s(X), n__s(Y)) → minus#(activate(X), activate(Y))geq#(n__s(X), n__s(Y)) → activate#(X)
minus#(n__s(X), n__s(Y)) → activate#(Y)div#(s(X), n__s(Y)) → activate#(Y)
geq#(n__s(X), n__s(Y)) → geq#(activate(X), activate(Y))if#(false, X, Y) → activate#(Y)
if#(true, X, Y) → activate#(X)div#(s(X), n__s(Y)) → if#(geq(X, activate(Y)), n__s(n__div(n__minus(X, activate(Y)), n__s(activate(Y)))), n__0)
minus#(n__s(X), n__s(Y)) → activate#(X)geq#(n__s(X), n__s(Y)) → activate#(Y)
div#(s(X), n__s(Y)) → geq#(X, activate(Y))