MAYBE

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (0ms).
 | – Problem 2 was processed with processor PolynomialLinearRange4iUR (0ms).
 |    | – Problem 3 remains open; application of the following processors failed [DependencyGraph (8ms), PolynomialLinearRange4iUR (2682ms), DependencyGraph (6ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (6ms), ReductionPairSAT (1150ms), DependencyGraph (46ms), SizeChangePrinciple (1990ms)].

The following open problems remain:



Open Dependency Pair Problem 3

Dependency Pairs

incr#(cons(X, Y))activate#(X)adx#(cons(X, Y))incr#(cons(activate(X), n__adx(activate(Y))))
activate#(n__adx(X))adx#(X)activate#(n__incr(X))incr#(X)
incr#(cons(X, Y))activate#(Y)

Rewrite Rules

natsadx(zeros)zeroscons(n__0, n__zeros)
incr(cons(X, Y))cons(n__s(activate(X)), n__incr(activate(Y)))adx(cons(X, Y))incr(cons(activate(X), n__adx(activate(Y))))
hd(cons(X, Y))activate(X)tl(cons(X, Y))activate(Y)
0n__0zerosn__zeros
s(X)n__s(X)incr(X)n__incr(X)
adx(X)n__adx(X)activate(n__0)0
activate(n__zeros)zerosactivate(n__s(X))s(X)
activate(n__incr(X))incr(X)activate(n__adx(X))adx(X)
activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__incr, tl, hd, n__adx, activate, n__s, nats, 0, n__0, s, zeros, adx, incr, n__zeros, cons


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

incr#(cons(X, Y))activate#(X)adx#(cons(X, Y))incr#(cons(activate(X), n__adx(activate(Y))))
activate#(n__zeros)zeros#nats#zeros#
tl#(cons(X, Y))activate#(Y)hd#(cons(X, Y))activate#(X)
activate#(n__incr(X))incr#(X)nats#adx#(zeros)
activate#(n__s(X))s#(X)adx#(cons(X, Y))activate#(Y)
activate#(n__adx(X))adx#(X)adx#(cons(X, Y))activate#(X)
activate#(n__0)0#incr#(cons(X, Y))activate#(Y)

Rewrite Rules

natsadx(zeros)zeroscons(n__0, n__zeros)
incr(cons(X, Y))cons(n__s(activate(X)), n__incr(activate(Y)))adx(cons(X, Y))incr(cons(activate(X), n__adx(activate(Y))))
hd(cons(X, Y))activate(X)tl(cons(X, Y))activate(Y)
0n__0zerosn__zeros
s(X)n__s(X)incr(X)n__incr(X)
adx(X)n__adx(X)activate(n__0)0
activate(n__zeros)zerosactivate(n__s(X))s(X)
activate(n__incr(X))incr(X)activate(n__adx(X))adx(X)
activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__incr, tl, hd, n__adx, activate, n__s, nats, 0, n__0, s, zeros, adx, incr, n__zeros, cons

Strategy


The following SCCs where found

incr#(cons(X, Y)) → activate#(X)adx#(cons(X, Y)) → incr#(cons(activate(X), n__adx(activate(Y))))
adx#(cons(X, Y)) → activate#(Y)activate#(n__adx(X)) → adx#(X)
adx#(cons(X, Y)) → activate#(X)activate#(n__incr(X)) → incr#(X)
incr#(cons(X, Y)) → activate#(Y)

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

incr#(cons(X, Y))activate#(X)adx#(cons(X, Y))incr#(cons(activate(X), n__adx(activate(Y))))
adx#(cons(X, Y))activate#(Y)activate#(n__adx(X))adx#(X)
adx#(cons(X, Y))activate#(X)activate#(n__incr(X))incr#(X)
incr#(cons(X, Y))activate#(Y)

Rewrite Rules

natsadx(zeros)zeroscons(n__0, n__zeros)
incr(cons(X, Y))cons(n__s(activate(X)), n__incr(activate(Y)))adx(cons(X, Y))incr(cons(activate(X), n__adx(activate(Y))))
hd(cons(X, Y))activate(X)tl(cons(X, Y))activate(Y)
0n__0zerosn__zeros
s(X)n__s(X)incr(X)n__incr(X)
adx(X)n__adx(X)activate(n__0)0
activate(n__zeros)zerosactivate(n__s(X))s(X)
activate(n__incr(X))incr(X)activate(n__adx(X))adx(X)
activate(X)X

Original Signature

Termination of terms over the following signature is verified: n__incr, tl, hd, n__adx, activate, n__s, nats, 0, n__0, s, zeros, adx, incr, n__zeros, cons

Strategy


Polynomial Interpretation

Improved Usable rules

activate(n__zeros)zeroszeroscons(n__0, n__zeros)
activate(n__s(X))s(X)activate(n__0)0
zerosn__zeros0n__0
s(X)n__s(X)activate(X)X
adx(cons(X, Y))incr(cons(activate(X), n__adx(activate(Y))))incr(X)n__incr(X)
activate(n__incr(X))incr(X)activate(n__adx(X))adx(X)
incr(cons(X, Y))cons(n__s(activate(X)), n__incr(activate(Y)))adx(X)n__adx(X)

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

adx#(cons(X, Y))activate#(Y)adx#(cons(X, Y))activate#(X)