MAYBE

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (0ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (2ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (213ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (2057ms), DependencyGraph (2ms), ReductionPairSAT (170ms), DependencyGraph (3ms), SizeChangePrinciple (20ms)].

The following open problems remain:



Open Dependency Pair Problem 2

Dependency Pairs

length#(cons(N, L))U11#(tt, activate(L))U12#(tt, L)length#(activate(L))
U11#(tt, L)U12#(tt, activate(L))

Rewrite Rules

zeroscons(0, n__zeros)U11(tt, L)U12(tt, activate(L))
U12(tt, L)s(length(activate(L)))length(nil)0
length(cons(N, L))U11(tt, activate(L))zerosn__zeros
activate(n__zeros)zerosactivate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, 0, s, tt, zeros, length, U11, U12, n__zeros, nil, cons


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

activate#(n__zeros)zeros#U12#(tt, L)activate#(L)
length#(cons(N, L))U11#(tt, activate(L))U12#(tt, L)length#(activate(L))
U11#(tt, L)activate#(L)U11#(tt, L)U12#(tt, activate(L))
length#(cons(N, L))activate#(L)

Rewrite Rules

zeroscons(0, n__zeros)U11(tt, L)U12(tt, activate(L))
U12(tt, L)s(length(activate(L)))length(nil)0
length(cons(N, L))U11(tt, activate(L))zerosn__zeros
activate(n__zeros)zerosactivate(X)X

Original Signature

Termination of terms over the following signature is verified: activate, 0, s, zeros, tt, length, U11, U12, n__zeros, cons, nil

Strategy


The following SCCs where found

length#(cons(N, L)) → U11#(tt, activate(L))U12#(tt, L) → length#(activate(L))
U11#(tt, L) → U12#(tt, activate(L))