TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (1517ms).
 | – Problem 2 was processed with processor SubtermCriterion (2ms).
 | – Problem 3 was processed with processor SubtermCriterion (6ms).
 | – Problem 4 was processed with processor SubtermCriterion (1ms).
 | – Problem 5 was processed with processor SubtermCriterion (0ms).
 |    | – Problem 9 was processed with processor ReductionPairSAT (78ms).
 |    |    | – Problem 10 was processed with processor ReductionPairSAT (69ms).
 | – Problem 6 was processed with processor SubtermCriterion (1ms).
 | – Problem 7 was processed with processor SubtermCriterion (1ms).
 | – Problem 8 remains open; application of the following processors failed [SubtermCriterion (0ms), DependencyGraph (356ms), PolynomialLinearRange4iUR (5000ms), DependencyGraph (280ms), PolynomialLinearRange8NegiUR (15000ms), DependencyGraph (270ms), ReductionPairSAT (6583ms), DependencyGraph (276ms), ReductionPairSAT (6657ms), DependencyGraph (271ms), ReductionPairSAT (6365ms), DependencyGraph (281ms), SizeChangePrinciple (timeout)].

The following open problems remain:



Open Dependency Pair Problem 8

Dependency Pairs

mark#(cons(X1, X2))active#(cons(mark(X1), X2))mark#(head(X))active#(head(mark(X)))
active#(tail(cons(X, L)))mark#(L)mark#(tail(X))active#(tail(mark(X)))
mark#(nil)active#(nil)mark#(head(X))mark#(X)
active#(nats)mark#(adx(zeros))mark#(s(X))mark#(X)
mark#(zeros)active#(zeros)active#(incr(nil))mark#(nil)
active#(adx(nil))mark#(nil)mark#(0)active#(0)
mark#(s(X))active#(s(mark(X)))active#(incr(cons(X, L)))mark#(cons(s(X), incr(L)))
mark#(nats)active#(nats)mark#(cons(X1, X2))mark#(X1)
mark#(incr(X))active#(incr(mark(X)))mark#(incr(X))mark#(X)
active#(adx(cons(X, L)))mark#(incr(cons(X, adx(L))))active#(head(cons(X, L)))mark#(X)
mark#(adx(X))mark#(X)mark#(tail(X))mark#(X)
active#(zeros)mark#(cons(0, zeros))mark#(adx(X))active#(adx(mark(X)))

Rewrite Rules

active(incr(nil))mark(nil)active(incr(cons(X, L)))mark(cons(s(X), incr(L)))
active(adx(nil))mark(nil)active(adx(cons(X, L)))mark(incr(cons(X, adx(L))))
active(nats)mark(adx(zeros))active(zeros)mark(cons(0, zeros))
active(head(cons(X, L)))mark(X)active(tail(cons(X, L)))mark(L)
mark(incr(X))active(incr(mark(X)))mark(nil)active(nil)
mark(cons(X1, X2))active(cons(mark(X1), X2))mark(s(X))active(s(mark(X)))
mark(adx(X))active(adx(mark(X)))mark(nats)active(nats)
mark(zeros)active(zeros)mark(0)active(0)
mark(head(X))active(head(mark(X)))mark(tail(X))active(tail(mark(X)))
incr(mark(X))incr(X)incr(active(X))incr(X)
cons(mark(X1), X2)cons(X1, X2)cons(X1, mark(X2))cons(X1, X2)
cons(active(X1), X2)cons(X1, X2)cons(X1, active(X2))cons(X1, X2)
s(mark(X))s(X)s(active(X))s(X)
adx(mark(X))adx(X)adx(active(X))adx(X)
head(mark(X))head(X)head(active(X))head(X)
tail(mark(X))tail(X)tail(active(X))tail(X)

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, zeros, adx, active, mark, incr, head, tail, cons, nil


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

mark#(cons(X1, X2))active#(cons(mark(X1), X2))active#(incr(cons(X, L)))incr#(L)
mark#(s(X))s#(mark(X))mark#(tail(X))active#(tail(mark(X)))
active#(incr(cons(X, L)))cons#(s(X), incr(L))active#(nats)mark#(adx(zeros))
mark#(s(X))mark#(X)adx#(active(X))adx#(X)
mark#(cons(X1, X2))mark#(X1)tail#(mark(X))tail#(X)
mark#(incr(X))active#(incr(mark(X)))cons#(X1, active(X2))cons#(X1, X2)
mark#(adx(X))mark#(X)mark#(tail(X))mark#(X)
head#(active(X))head#(X)active#(adx(cons(X, L)))incr#(cons(X, adx(L)))
mark#(adx(X))active#(adx(mark(X)))mark#(head(X))active#(head(mark(X)))
incr#(active(X))incr#(X)cons#(mark(X1), X2)cons#(X1, X2)
mark#(tail(X))tail#(mark(X))active#(tail(cons(X, L)))mark#(L)
mark#(head(X))mark#(X)mark#(nil)active#(nil)
active#(incr(cons(X, L)))s#(X)tail#(active(X))tail#(X)
incr#(mark(X))incr#(X)mark#(incr(X))incr#(mark(X))
cons#(X1, mark(X2))cons#(X1, X2)mark#(adx(X))adx#(mark(X))
mark#(zeros)active#(zeros)mark#(cons(X1, X2))cons#(mark(X1), X2)
active#(incr(nil))mark#(nil)active#(adx(nil))mark#(nil)
mark#(0)active#(0)mark#(s(X))active#(s(mark(X)))
active#(incr(cons(X, L)))mark#(cons(s(X), incr(L)))mark#(nats)active#(nats)
head#(mark(X))head#(X)active#(adx(cons(X, L)))cons#(X, adx(L))
active#(adx(cons(X, L)))adx#(L)cons#(active(X1), X2)cons#(X1, X2)
mark#(incr(X))mark#(X)mark#(head(X))head#(mark(X))
active#(nats)adx#(zeros)s#(mark(X))s#(X)
adx#(mark(X))adx#(X)active#(adx(cons(X, L)))mark#(incr(cons(X, adx(L))))
active#(head(cons(X, L)))mark#(X)active#(zeros)cons#(0, zeros)
active#(zeros)mark#(cons(0, zeros))s#(active(X))s#(X)

Rewrite Rules

active(incr(nil))mark(nil)active(incr(cons(X, L)))mark(cons(s(X), incr(L)))
active(adx(nil))mark(nil)active(adx(cons(X, L)))mark(incr(cons(X, adx(L))))
active(nats)mark(adx(zeros))active(zeros)mark(cons(0, zeros))
active(head(cons(X, L)))mark(X)active(tail(cons(X, L)))mark(L)
mark(incr(X))active(incr(mark(X)))mark(nil)active(nil)
mark(cons(X1, X2))active(cons(mark(X1), X2))mark(s(X))active(s(mark(X)))
mark(adx(X))active(adx(mark(X)))mark(nats)active(nats)
mark(zeros)active(zeros)mark(0)active(0)
mark(head(X))active(head(mark(X)))mark(tail(X))active(tail(mark(X)))
incr(mark(X))incr(X)incr(active(X))incr(X)
cons(mark(X1), X2)cons(X1, X2)cons(X1, mark(X2))cons(X1, X2)
cons(active(X1), X2)cons(X1, X2)cons(X1, active(X2))cons(X1, X2)
s(mark(X))s(X)s(active(X))s(X)
adx(mark(X))adx(X)adx(active(X))adx(X)
head(mark(X))head(X)head(active(X))head(X)
tail(mark(X))tail(X)tail(active(X))tail(X)

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, zeros, active, adx, mark, incr, head, tail, nil, cons

Strategy


The following SCCs where found

active#(adx(nil)) → mark#(nil)mark#(head(X)) → active#(head(mark(X)))
mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))mark#(0) → active#(0)
mark#(s(X)) → active#(s(mark(X)))mark#(nats) → active#(nats)
active#(incr(cons(X, L))) → mark#(cons(s(X), incr(L)))mark#(cons(X1, X2)) → mark#(X1)
mark#(incr(X)) → active#(incr(mark(X)))mark#(incr(X)) → mark#(X)
active#(tail(cons(X, L))) → mark#(L)mark#(tail(X)) → active#(tail(mark(X)))
mark#(head(X)) → mark#(X)mark#(nil) → active#(nil)
active#(adx(cons(X, L))) → mark#(incr(cons(X, adx(L))))mark#(adx(X)) → mark#(X)
active#(head(cons(X, L))) → mark#(X)mark#(tail(X)) → mark#(X)
active#(nats) → mark#(adx(zeros))active#(zeros) → mark#(cons(0, zeros))
mark#(s(X)) → mark#(X)mark#(zeros) → active#(zeros)
mark#(adx(X)) → active#(adx(mark(X)))active#(incr(nil)) → mark#(nil)

adx#(mark(X)) → adx#(X)adx#(active(X)) → adx#(X)

tail#(active(X)) → tail#(X)tail#(mark(X)) → tail#(X)

s#(mark(X)) → s#(X)s#(active(X)) → s#(X)

cons#(X1, active(X2)) → cons#(X1, X2)cons#(mark(X1), X2) → cons#(X1, X2)
cons#(X1, mark(X2)) → cons#(X1, X2)cons#(active(X1), X2) → cons#(X1, X2)

incr#(active(X)) → incr#(X)incr#(mark(X)) → incr#(X)

head#(mark(X)) → head#(X)head#(active(X)) → head#(X)

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

s#(mark(X))s#(X)s#(active(X))s#(X)

Rewrite Rules

active(incr(nil))mark(nil)active(incr(cons(X, L)))mark(cons(s(X), incr(L)))
active(adx(nil))mark(nil)active(adx(cons(X, L)))mark(incr(cons(X, adx(L))))
active(nats)mark(adx(zeros))active(zeros)mark(cons(0, zeros))
active(head(cons(X, L)))mark(X)active(tail(cons(X, L)))mark(L)
mark(incr(X))active(incr(mark(X)))mark(nil)active(nil)
mark(cons(X1, X2))active(cons(mark(X1), X2))mark(s(X))active(s(mark(X)))
mark(adx(X))active(adx(mark(X)))mark(nats)active(nats)
mark(zeros)active(zeros)mark(0)active(0)
mark(head(X))active(head(mark(X)))mark(tail(X))active(tail(mark(X)))
incr(mark(X))incr(X)incr(active(X))incr(X)
cons(mark(X1), X2)cons(X1, X2)cons(X1, mark(X2))cons(X1, X2)
cons(active(X1), X2)cons(X1, X2)cons(X1, active(X2))cons(X1, X2)
s(mark(X))s(X)s(active(X))s(X)
adx(mark(X))adx(X)adx(active(X))adx(X)
head(mark(X))head(X)head(active(X))head(X)
tail(mark(X))tail(X)tail(active(X))tail(X)

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, zeros, active, adx, mark, incr, head, tail, nil, cons

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

s#(mark(X))s#(X)s#(active(X))s#(X)

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

head#(mark(X))head#(X)head#(active(X))head#(X)

Rewrite Rules

active(incr(nil))mark(nil)active(incr(cons(X, L)))mark(cons(s(X), incr(L)))
active(adx(nil))mark(nil)active(adx(cons(X, L)))mark(incr(cons(X, adx(L))))
active(nats)mark(adx(zeros))active(zeros)mark(cons(0, zeros))
active(head(cons(X, L)))mark(X)active(tail(cons(X, L)))mark(L)
mark(incr(X))active(incr(mark(X)))mark(nil)active(nil)
mark(cons(X1, X2))active(cons(mark(X1), X2))mark(s(X))active(s(mark(X)))
mark(adx(X))active(adx(mark(X)))mark(nats)active(nats)
mark(zeros)active(zeros)mark(0)active(0)
mark(head(X))active(head(mark(X)))mark(tail(X))active(tail(mark(X)))
incr(mark(X))incr(X)incr(active(X))incr(X)
cons(mark(X1), X2)cons(X1, X2)cons(X1, mark(X2))cons(X1, X2)
cons(active(X1), X2)cons(X1, X2)cons(X1, active(X2))cons(X1, X2)
s(mark(X))s(X)s(active(X))s(X)
adx(mark(X))adx(X)adx(active(X))adx(X)
head(mark(X))head(X)head(active(X))head(X)
tail(mark(X))tail(X)tail(active(X))tail(X)

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, zeros, active, adx, mark, incr, head, tail, nil, cons

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

head#(mark(X))head#(X)head#(active(X))head#(X)

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

incr#(active(X))incr#(X)incr#(mark(X))incr#(X)

Rewrite Rules

active(incr(nil))mark(nil)active(incr(cons(X, L)))mark(cons(s(X), incr(L)))
active(adx(nil))mark(nil)active(adx(cons(X, L)))mark(incr(cons(X, adx(L))))
active(nats)mark(adx(zeros))active(zeros)mark(cons(0, zeros))
active(head(cons(X, L)))mark(X)active(tail(cons(X, L)))mark(L)
mark(incr(X))active(incr(mark(X)))mark(nil)active(nil)
mark(cons(X1, X2))active(cons(mark(X1), X2))mark(s(X))active(s(mark(X)))
mark(adx(X))active(adx(mark(X)))mark(nats)active(nats)
mark(zeros)active(zeros)mark(0)active(0)
mark(head(X))active(head(mark(X)))mark(tail(X))active(tail(mark(X)))
incr(mark(X))incr(X)incr(active(X))incr(X)
cons(mark(X1), X2)cons(X1, X2)cons(X1, mark(X2))cons(X1, X2)
cons(active(X1), X2)cons(X1, X2)cons(X1, active(X2))cons(X1, X2)
s(mark(X))s(X)s(active(X))s(X)
adx(mark(X))adx(X)adx(active(X))adx(X)
head(mark(X))head(X)head(active(X))head(X)
tail(mark(X))tail(X)tail(active(X))tail(X)

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, zeros, active, adx, mark, incr, head, tail, nil, cons

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

incr#(active(X))incr#(X)incr#(mark(X))incr#(X)

Problem 5: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

cons#(X1, active(X2))cons#(X1, X2)cons#(mark(X1), X2)cons#(X1, X2)
cons#(X1, mark(X2))cons#(X1, X2)cons#(active(X1), X2)cons#(X1, X2)

Rewrite Rules

active(incr(nil))mark(nil)active(incr(cons(X, L)))mark(cons(s(X), incr(L)))
active(adx(nil))mark(nil)active(adx(cons(X, L)))mark(incr(cons(X, adx(L))))
active(nats)mark(adx(zeros))active(zeros)mark(cons(0, zeros))
active(head(cons(X, L)))mark(X)active(tail(cons(X, L)))mark(L)
mark(incr(X))active(incr(mark(X)))mark(nil)active(nil)
mark(cons(X1, X2))active(cons(mark(X1), X2))mark(s(X))active(s(mark(X)))
mark(adx(X))active(adx(mark(X)))mark(nats)active(nats)
mark(zeros)active(zeros)mark(0)active(0)
mark(head(X))active(head(mark(X)))mark(tail(X))active(tail(mark(X)))
incr(mark(X))incr(X)incr(active(X))incr(X)
cons(mark(X1), X2)cons(X1, X2)cons(X1, mark(X2))cons(X1, X2)
cons(active(X1), X2)cons(X1, X2)cons(X1, active(X2))cons(X1, X2)
s(mark(X))s(X)s(active(X))s(X)
adx(mark(X))adx(X)adx(active(X))adx(X)
head(mark(X))head(X)head(active(X))head(X)
tail(mark(X))tail(X)tail(active(X))tail(X)

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, zeros, active, adx, mark, incr, head, tail, nil, cons

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

cons#(mark(X1), X2)cons#(X1, X2)cons#(active(X1), X2)cons#(X1, X2)

Problem 9: ReductionPairSAT



Dependency Pair Problem

Dependency Pairs

cons#(X1, active(X2))cons#(X1, X2)cons#(X1, mark(X2))cons#(X1, X2)

Rewrite Rules

active(incr(nil))mark(nil)active(incr(cons(X, L)))mark(cons(s(X), incr(L)))
active(adx(nil))mark(nil)active(adx(cons(X, L)))mark(incr(cons(X, adx(L))))
active(nats)mark(adx(zeros))active(zeros)mark(cons(0, zeros))
active(head(cons(X, L)))mark(X)active(tail(cons(X, L)))mark(L)
mark(incr(X))active(incr(mark(X)))mark(nil)active(nil)
mark(cons(X1, X2))active(cons(mark(X1), X2))mark(s(X))active(s(mark(X)))
mark(adx(X))active(adx(mark(X)))mark(nats)active(nats)
mark(zeros)active(zeros)mark(0)active(0)
mark(head(X))active(head(mark(X)))mark(tail(X))active(tail(mark(X)))
incr(mark(X))incr(X)incr(active(X))incr(X)
cons(mark(X1), X2)cons(X1, X2)cons(X1, mark(X2))cons(X1, X2)
cons(active(X1), X2)cons(X1, X2)cons(X1, active(X2))cons(X1, X2)
s(mark(X))s(X)s(active(X))s(X)
adx(mark(X))adx(X)adx(active(X))adx(X)
head(mark(X))head(X)head(active(X))head(X)
tail(mark(X))tail(X)tail(active(X))tail(X)

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, zeros, adx, active, mark, incr, head, tail, cons, nil

Strategy


Function Precedence

cons# < active < mark < tail = nats = 0 = s = zeros = adx = incr = head = cons = nil

Argument Filtering

mark: collapses to 1
tail: 1
nats: all arguments are removed from nats
cons#: 1 2
0: all arguments are removed from 0
s: collapses to 1
zeros: all arguments are removed from zeros
adx: all arguments are removed from adx
active: 1
incr: 1
head: collapses to 1
cons: 1 2
nil: all arguments are removed from nil

Status

tail: lexicographic with permutation 1 → 1
nats: multiset
cons#: lexicographic with permutation 1 → 1 2 → 2
0: multiset
zeros: multiset
adx: multiset
active: multiset
incr: lexicographic with permutation 1 → 1
cons: lexicographic with permutation 1 → 1 2 → 2
nil: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

cons#(X1, active(X2)) → cons#(X1, X2)

Problem 10: ReductionPairSAT



Dependency Pair Problem

Dependency Pairs

cons#(X1, mark(X2))cons#(X1, X2)

Rewrite Rules

active(incr(nil))mark(nil)active(incr(cons(X, L)))mark(cons(s(X), incr(L)))
active(adx(nil))mark(nil)active(adx(cons(X, L)))mark(incr(cons(X, adx(L))))
active(nats)mark(adx(zeros))active(zeros)mark(cons(0, zeros))
active(head(cons(X, L)))mark(X)active(tail(cons(X, L)))mark(L)
mark(incr(X))active(incr(mark(X)))mark(nil)active(nil)
mark(cons(X1, X2))active(cons(mark(X1), X2))mark(s(X))active(s(mark(X)))
mark(adx(X))active(adx(mark(X)))mark(nats)active(nats)
mark(zeros)active(zeros)mark(0)active(0)
mark(head(X))active(head(mark(X)))mark(tail(X))active(tail(mark(X)))
incr(mark(X))incr(X)incr(active(X))incr(X)
cons(mark(X1), X2)cons(X1, X2)cons(X1, mark(X2))cons(X1, X2)
cons(active(X1), X2)cons(X1, X2)cons(X1, active(X2))cons(X1, X2)
s(mark(X))s(X)s(active(X))s(X)
adx(mark(X))adx(X)adx(active(X))adx(X)
head(mark(X))head(X)head(active(X))head(X)
tail(mark(X))tail(X)tail(active(X))tail(X)

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, zeros, active, adx, mark, incr, head, tail, nil, cons

Strategy


Function Precedence

mark < tail = nats = cons# = 0 = s = zeros = adx = active = incr = head = cons = nil

Argument Filtering

mark: 1
tail: collapses to 1
nats: all arguments are removed from nats
cons#: collapses to 2
0: all arguments are removed from 0
s: collapses to 1
zeros: all arguments are removed from zeros
adx: collapses to 1
active: all arguments are removed from active
incr: collapses to 1
head: collapses to 1
cons: 2
nil: all arguments are removed from nil

Status

mark: lexicographic with permutation 1 → 1
nats: multiset
0: multiset
zeros: multiset
active: multiset
cons: lexicographic with permutation 2 → 1
nil: multiset

Usable Rules

There are no usable rules.

The dependency pairs and usable rules are stronlgy conservative!

Eliminated dependency pairs

The following dependency pairs (at least) can be eliminated according to the given precedence.

cons#(X1, mark(X2)) → cons#(X1, X2)

Problem 6: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

adx#(mark(X))adx#(X)adx#(active(X))adx#(X)

Rewrite Rules

active(incr(nil))mark(nil)active(incr(cons(X, L)))mark(cons(s(X), incr(L)))
active(adx(nil))mark(nil)active(adx(cons(X, L)))mark(incr(cons(X, adx(L))))
active(nats)mark(adx(zeros))active(zeros)mark(cons(0, zeros))
active(head(cons(X, L)))mark(X)active(tail(cons(X, L)))mark(L)
mark(incr(X))active(incr(mark(X)))mark(nil)active(nil)
mark(cons(X1, X2))active(cons(mark(X1), X2))mark(s(X))active(s(mark(X)))
mark(adx(X))active(adx(mark(X)))mark(nats)active(nats)
mark(zeros)active(zeros)mark(0)active(0)
mark(head(X))active(head(mark(X)))mark(tail(X))active(tail(mark(X)))
incr(mark(X))incr(X)incr(active(X))incr(X)
cons(mark(X1), X2)cons(X1, X2)cons(X1, mark(X2))cons(X1, X2)
cons(active(X1), X2)cons(X1, X2)cons(X1, active(X2))cons(X1, X2)
s(mark(X))s(X)s(active(X))s(X)
adx(mark(X))adx(X)adx(active(X))adx(X)
head(mark(X))head(X)head(active(X))head(X)
tail(mark(X))tail(X)tail(active(X))tail(X)

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, zeros, active, adx, mark, incr, head, tail, nil, cons

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

adx#(mark(X))adx#(X)adx#(active(X))adx#(X)

Problem 7: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

tail#(active(X))tail#(X)tail#(mark(X))tail#(X)

Rewrite Rules

active(incr(nil))mark(nil)active(incr(cons(X, L)))mark(cons(s(X), incr(L)))
active(adx(nil))mark(nil)active(adx(cons(X, L)))mark(incr(cons(X, adx(L))))
active(nats)mark(adx(zeros))active(zeros)mark(cons(0, zeros))
active(head(cons(X, L)))mark(X)active(tail(cons(X, L)))mark(L)
mark(incr(X))active(incr(mark(X)))mark(nil)active(nil)
mark(cons(X1, X2))active(cons(mark(X1), X2))mark(s(X))active(s(mark(X)))
mark(adx(X))active(adx(mark(X)))mark(nats)active(nats)
mark(zeros)active(zeros)mark(0)active(0)
mark(head(X))active(head(mark(X)))mark(tail(X))active(tail(mark(X)))
incr(mark(X))incr(X)incr(active(X))incr(X)
cons(mark(X1), X2)cons(X1, X2)cons(X1, mark(X2))cons(X1, X2)
cons(active(X1), X2)cons(X1, X2)cons(X1, active(X2))cons(X1, X2)
s(mark(X))s(X)s(active(X))s(X)
adx(mark(X))adx(X)adx(active(X))adx(X)
head(mark(X))head(X)head(active(X))head(X)
tail(mark(X))tail(X)tail(active(X))tail(X)

Original Signature

Termination of terms over the following signature is verified: nats, 0, s, zeros, active, adx, mark, incr, head, tail, nil, cons

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

tail#(active(X))tail#(X)tail#(mark(X))tail#(X)