TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (5813ms).
 | – Problem 2 was processed with processor SubtermCriterion (1ms).
 | – Problem 3 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 11 was processed with processor ReductionPairSAT (58ms).
 |    |    | – Problem 15 remains open; application of the following processors failed [DependencyGraph (2ms), ReductionPairSAT (timeout)].
 | – Problem 4 was processed with processor SubtermCriterion (4ms).
 |    | – Problem 12 was processed with processor ReductionPairSAT (50ms).
 |    |    | – Problem 16 was processed with processor ReductionPairSAT (68ms).
 | – Problem 5 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (988ms), PolynomialLinearRange4iUR (2000ms), DependencyGraph (1024ms), PolynomialLinearRange8NegiUR (6000ms), DependencyGraph (1044ms), ReductionPairSAT (28814ms), DependencyGraph (981ms), ReductionPairSAT (12559ms)].
 | – Problem 6 was processed with processor SubtermCriterion (1ms).
 | – Problem 7 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 13 was processed with processor ReductionPairSAT (77ms).
 |    |    | – Problem 17 was processed with processor ReductionPairSAT (25ms).
 | – Problem 8 was processed with processor SubtermCriterion (1ms).
 | – Problem 9 was processed with processor SubtermCriterion (1ms).
 | – Problem 10 was processed with processor SubtermCriterion (3ms).
 |    | – Problem 14 was processed with processor ReductionPairSAT (35ms).
 |    |    | – Problem 18 was processed with processor ReductionPairSAT (32ms).

The following open problems remain:

Open Dependency Pair Problem 5

Dependency Pairs

mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))mark#(zip(X1, X2)) → mark#(X2)
active#(repItems(cons(X, XS))) → mark#(cons(X, cons(X, repItems(XS))))mark#(take(X1, X2)) → mark#(X1)
mark#(pairNs) → active#(pairNs)active#(zip(X, nil)) → mark#(nil)
mark#(repItems(X)) → active#(repItems(mark(X)))mark#(pair(X1, X2)) → mark#(X2)
mark#(zip(X1, X2)) → mark#(X1)mark#(take(X1, X2)) → active#(take(mark(X1), mark(X2)))
mark#(tail(X)) → active#(tail(mark(X)))mark#(nil) → active#(nil)
mark#(oddNs) → active#(oddNs)mark#(s(X)) → mark#(X)
active#(zip(nil, XS)) → mark#(nil)active#(tail(cons(X, XS))) → mark#(XS)
mark#(repItems(X)) → mark#(X)active#(pairNs) → mark#(cons(0, incr(oddNs)))
mark#(0) → active#(0)mark#(s(X)) → active#(s(mark(X)))
active#(incr(cons(X, XS))) → mark#(cons(s(X), incr(XS)))mark#(cons(X1, X2)) → mark#(X1)
active#(take(0, XS)) → mark#(nil)active#(oddNs) → mark#(incr(pairNs))
mark#(incr(X)) → active#(incr(mark(X)))mark#(incr(X)) → mark#(X)
mark#(zip(X1, X2)) → active#(zip(mark(X1), mark(X2)))mark#(pair(X1, X2)) → mark#(X1)
active#(repItems(nil)) → mark#(nil)mark#(tail(X)) → mark#(X)
active#(zip(cons(X, XS), cons(Y, YS))) → mark#(cons(pair(X, Y), zip(XS, YS)))mark#(take(X1, X2)) → mark#(X2)
active#(take(s(N), cons(X, XS))) → mark#(cons(X, take(N, XS)))mark#(pair(X1, X2)) → active#(pair(mark(X1), mark(X2)))

Rewrite Rules

active(pairNs) → mark(cons(0, incr(oddNs)))active(oddNs) → mark(incr(pairNs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))active(take(0, XS)) → mark(nil)
active(take(s(N), cons(X, XS))) → mark(cons(X, take(N, XS)))active(zip(nil, XS)) → mark(nil)
active(zip(X, nil)) → mark(nil)active(zip(cons(X, XS), cons(Y, YS))) → mark(cons(pair(X, Y), zip(XS, YS)))
active(tail(cons(X, XS))) → mark(XS)active(repItems(nil)) → mark(nil)
active(repItems(cons(X, XS))) → mark(cons(X, cons(X, repItems(XS))))mark(pairNs) → active(pairNs)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))mark(oddNs) → active(oddNs)
mark(s(X)) → active(s(mark(X)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(zip(X1, X2)) → active(zip(mark(X1), mark(X2)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))mark(tail(X)) → active(tail(mark(X)))
mark(repItems(X)) → active(repItems(mark(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)incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)s(mark(X)) → s(X)
s(active(X)) → s(X)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)zip(mark(X1), X2) → zip(X1, X2)
zip(X1, mark(X2)) → zip(X1, X2)zip(active(X1), X2) → zip(X1, X2)
zip(X1, active(X2)) → zip(X1, X2)pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)repItems(mark(X)) → repItems(X)
repItems(active(X)) → repItems(X)

Original Signature

Termination of terms over the following signature is verified: zip, pair, mark, tail, 0, pairNs, s, repItems, take, active, incr, oddNs, cons, nil

Open Dependency Pair Problem 15

Dependency Pairs

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

Rewrite Rules

active(pairNs) → mark(cons(0, incr(oddNs)))active(oddNs) → mark(incr(pairNs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))active(take(0, XS)) → mark(nil)
active(take(s(N), cons(X, XS))) → mark(cons(X, take(N, XS)))active(zip(nil, XS)) → mark(nil)
active(zip(X, nil)) → mark(nil)active(zip(cons(X, XS), cons(Y, YS))) → mark(cons(pair(X, Y), zip(XS, YS)))
active(tail(cons(X, XS))) → mark(XS)active(repItems(nil)) → mark(nil)
active(repItems(cons(X, XS))) → mark(cons(X, cons(X, repItems(XS))))mark(pairNs) → active(pairNs)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))mark(oddNs) → active(oddNs)
mark(s(X)) → active(s(mark(X)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(zip(X1, X2)) → active(zip(mark(X1), mark(X2)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))mark(tail(X)) → active(tail(mark(X)))
mark(repItems(X)) → active(repItems(mark(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)incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)s(mark(X)) → s(X)
s(active(X)) → s(X)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)zip(mark(X1), X2) → zip(X1, X2)
zip(X1, mark(X2)) → zip(X1, X2)zip(active(X1), X2) → zip(X1, X2)
zip(X1, active(X2)) → zip(X1, X2)pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)repItems(mark(X)) → repItems(X)
repItems(active(X)) → repItems(X)

Original Signature

Termination of terms over the following signature is verified: zip, pair, mark, tail, 0, pairNs, s, repItems, take, active, incr, oddNs, cons, nil

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

active#(zip(cons(X, XS), cons(Y, YS))) → pair#(X, Y)mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))
active#(repItems(cons(X, XS))) → mark#(cons(X, cons(X, repItems(XS))))mark#(take(X1, X2)) → mark#(X1)
active#(zip(X, nil)) → mark#(nil)mark#(pairNs) → active#(pairNs)
mark#(pair(X1, X2)) → mark#(X2)mark#(take(X1, X2)) → active#(take(mark(X1), mark(X2)))
mark#(zip(X1, X2)) → mark#(X1)zip#(active(X1), X2) → zip#(X1, X2)
mark#(s(X)) → s#(mark(X))active#(repItems(cons(X, XS))) → cons#(X, repItems(XS))
active#(pairNs) → incr#(oddNs)active#(take(s(N), cons(X, XS))) → cons#(X, take(N, XS))
mark#(tail(X)) → active#(tail(mark(X)))mark#(s(X)) → mark#(X)
active#(pairNs) → cons#(0, incr(oddNs))active#(zip(nil, XS)) → mark#(nil)
pair#(active(X1), X2) → pair#(X1, X2)active#(incr(cons(X, XS))) → mark#(cons(s(X), incr(XS)))
active#(incr(cons(X, XS))) → cons#(s(X), incr(XS))mark#(zip(X1, X2)) → zip#(mark(X1), mark(X2))
mark#(cons(X1, X2)) → mark#(X1)active#(take(0, XS)) → mark#(nil)
pair#(X1, mark(X2)) → pair#(X1, X2)active#(oddNs) → mark#(incr(pairNs))
tail#(mark(X)) → tail#(X)take#(X1, mark(X2)) → take#(X1, X2)
mark#(repItems(X)) → repItems#(mark(X))mark#(incr(X)) → active#(incr(mark(X)))
mark#(zip(X1, X2)) → active#(zip(mark(X1), mark(X2)))cons#(X1, active(X2)) → cons#(X1, X2)
mark#(pair(X1, X2)) → mark#(X1)active#(repItems(nil)) → mark#(nil)
mark#(tail(X)) → mark#(X)active#(zip(cons(X, XS), cons(Y, YS))) → cons#(pair(X, Y), zip(XS, YS))
active#(incr(cons(X, XS))) → incr#(XS)active#(take(s(N), cons(X, XS))) → mark#(cons(X, take(N, XS)))
pair#(mark(X1), X2) → pair#(X1, X2)mark#(zip(X1, X2)) → mark#(X2)
take#(mark(X1), X2) → take#(X1, X2)incr#(active(X)) → incr#(X)
zip#(X1, active(X2)) → zip#(X1, X2)cons#(mark(X1), X2) → cons#(X1, X2)
mark#(repItems(X)) → active#(repItems(mark(X)))mark#(pair(X1, X2)) → pair#(mark(X1), mark(X2))
zip#(mark(X1), X2) → zip#(X1, X2)mark#(tail(X)) → tail#(mark(X))
repItems#(mark(X)) → repItems#(X)active#(zip(cons(X, XS), cons(Y, YS))) → zip#(XS, YS)
mark#(nil) → active#(nil)active#(repItems(cons(X, XS))) → repItems#(XS)
take#(X1, active(X2)) → take#(X1, X2)tail#(active(X)) → tail#(X)
mark#(oddNs) → active#(oddNs)incr#(mark(X)) → incr#(X)
zip#(X1, mark(X2)) → zip#(X1, X2)mark#(incr(X)) → incr#(mark(X))
active#(take(s(N), cons(X, XS))) → take#(N, XS)cons#(X1, mark(X2)) → cons#(X1, X2)
mark#(cons(X1, X2)) → cons#(mark(X1), X2)active#(tail(cons(X, XS))) → mark#(XS)
mark#(repItems(X)) → mark#(X)mark#(0) → active#(0)
active#(pairNs) → mark#(cons(0, incr(oddNs)))mark#(s(X)) → active#(s(mark(X)))
pair#(X1, active(X2)) → pair#(X1, X2)cons#(active(X1), X2) → cons#(X1, X2)
mark#(incr(X)) → mark#(X)mark#(take(X1, X2)) → take#(mark(X1), mark(X2))
active#(incr(cons(X, XS))) → s#(X)s#(mark(X)) → s#(X)
active#(repItems(cons(X, XS))) → cons#(X, cons(X, repItems(XS)))active#(zip(cons(X, XS), cons(Y, YS))) → mark#(cons(pair(X, Y), zip(XS, YS)))
active#(oddNs) → incr#(pairNs)mark#(take(X1, X2)) → mark#(X2)
repItems#(active(X)) → repItems#(X)s#(active(X)) → s#(X)
mark#(pair(X1, X2)) → active#(pair(mark(X1), mark(X2)))take#(active(X1), X2) → take#(X1, X2)

Rewrite Rules

active(pairNs) → mark(cons(0, incr(oddNs)))active(oddNs) → mark(incr(pairNs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))active(take(0, XS)) → mark(nil)
active(take(s(N), cons(X, XS))) → mark(cons(X, take(N, XS)))active(zip(nil, XS)) → mark(nil)
active(zip(X, nil)) → mark(nil)active(zip(cons(X, XS), cons(Y, YS))) → mark(cons(pair(X, Y), zip(XS, YS)))
active(tail(cons(X, XS))) → mark(XS)active(repItems(nil)) → mark(nil)
active(repItems(cons(X, XS))) → mark(cons(X, cons(X, repItems(XS))))mark(pairNs) → active(pairNs)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))mark(oddNs) → active(oddNs)
mark(s(X)) → active(s(mark(X)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(zip(X1, X2)) → active(zip(mark(X1), mark(X2)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))mark(tail(X)) → active(tail(mark(X)))
mark(repItems(X)) → active(repItems(mark(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)incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)s(mark(X)) → s(X)
s(active(X)) → s(X)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)zip(mark(X1), X2) → zip(X1, X2)
zip(X1, mark(X2)) → zip(X1, X2)zip(active(X1), X2) → zip(X1, X2)
zip(X1, active(X2)) → zip(X1, X2)pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)repItems(mark(X)) → repItems(X)
repItems(active(X)) → repItems(X)

Original Signature

Termination of terms over the following signature is verified: zip, pair, mark, tail, 0, pairNs, s, repItems, take, active, incr, oddNs, nil, cons

Strategy

The following SCCs where found

repItems#(active(X)) → repItems#(X)repItems#(mark(X)) → repItems#(X)
mark#(zip(X1, X2)) → mark#(X2)mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))
mark#(take(X1, X2)) → mark#(X1)active#(repItems(cons(X, XS))) → mark#(cons(X, cons(X, repItems(XS))))
active#(zip(X, nil)) → mark#(nil)mark#(pairNs) → active#(pairNs)
mark#(repItems(X)) → active#(repItems(mark(X)))mark#(pair(X1, X2)) → mark#(X2)
mark#(take(X1, X2)) → active#(take(mark(X1), mark(X2)))mark#(zip(X1, X2)) → mark#(X1)
mark#(tail(X)) → active#(tail(mark(X)))mark#(nil) → active#(nil)
mark#(oddNs) → active#(oddNs)mark#(s(X)) → mark#(X)
active#(zip(nil, XS)) → mark#(nil)mark#(repItems(X)) → mark#(X)
active#(tail(cons(X, XS))) → mark#(XS)mark#(0) → active#(0)
active#(pairNs) → mark#(cons(0, incr(oddNs)))mark#(s(X)) → active#(s(mark(X)))
active#(incr(cons(X, XS))) → mark#(cons(s(X), incr(XS)))active#(take(0, XS)) → mark#(nil)
mark#(cons(X1, X2)) → mark#(X1)active#(oddNs) → mark#(incr(pairNs))
mark#(incr(X)) → active#(incr(mark(X)))mark#(incr(X)) → mark#(X)
mark#(zip(X1, X2)) → active#(zip(mark(X1), mark(X2)))mark#(pair(X1, X2)) → mark#(X1)
active#(repItems(nil)) → mark#(nil)mark#(tail(X)) → mark#(X)
active#(zip(cons(X, XS), cons(Y, YS))) → mark#(cons(pair(X, Y), zip(XS, YS)))mark#(take(X1, X2)) → mark#(X2)
active#(take(s(N), cons(X, XS))) → mark#(cons(X, take(N, XS)))mark#(pair(X1, X2)) → active#(pair(mark(X1), mark(X2)))
tail#(active(X)) → tail#(X)tail#(mark(X)) → tail#(X)
cons#(X1, active(X2)) → cons#(X1, X2)cons#(mark(X1), X2) → cons#(X1, X2)
cons#(active(X1), X2) → cons#(X1, X2)cons#(X1, mark(X2)) → cons#(X1, X2)
s#(mark(X)) → s#(X)s#(active(X)) → s#(X)
incr#(active(X)) → incr#(X)incr#(mark(X)) → incr#(X)
take#(mark(X1), X2) → take#(X1, X2)take#(X1, active(X2)) → take#(X1, X2)
take#(X1, mark(X2)) → take#(X1, X2)take#(active(X1), X2) → take#(X1, X2)
pair#(mark(X1), X2) → pair#(X1, X2)pair#(X1, mark(X2)) → pair#(X1, X2)
pair#(X1, active(X2)) → pair#(X1, X2)pair#(active(X1), X2) → pair#(X1, X2)
zip#(X1, active(X2)) → zip#(X1, X2)zip#(mark(X1), X2) → zip#(X1, X2)
zip#(X1, mark(X2)) → zip#(X1, X2)zip#(active(X1), X2) → zip#(X1, X2)

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(pairNs) → mark(cons(0, incr(oddNs)))active(oddNs) → mark(incr(pairNs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))active(take(0, XS)) → mark(nil)
active(take(s(N), cons(X, XS))) → mark(cons(X, take(N, XS)))active(zip(nil, XS)) → mark(nil)
active(zip(X, nil)) → mark(nil)active(zip(cons(X, XS), cons(Y, YS))) → mark(cons(pair(X, Y), zip(XS, YS)))
active(tail(cons(X, XS))) → mark(XS)active(repItems(nil)) → mark(nil)
active(repItems(cons(X, XS))) → mark(cons(X, cons(X, repItems(XS))))mark(pairNs) → active(pairNs)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))mark(oddNs) → active(oddNs)
mark(s(X)) → active(s(mark(X)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(zip(X1, X2)) → active(zip(mark(X1), mark(X2)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))mark(tail(X)) → active(tail(mark(X)))
mark(repItems(X)) → active(repItems(mark(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)incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)s(mark(X)) → s(X)
s(active(X)) → s(X)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)zip(mark(X1), X2) → zip(X1, X2)
zip(X1, mark(X2)) → zip(X1, X2)zip(active(X1), X2) → zip(X1, X2)
zip(X1, active(X2)) → zip(X1, X2)pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)repItems(mark(X)) → repItems(X)
repItems(active(X)) → repItems(X)

Original Signature

Termination of terms over the following signature is verified: zip, pair, mark, tail, 0, pairNs, s, repItems, take, active, incr, oddNs, 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)

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(pairNs) → mark(cons(0, incr(oddNs)))active(oddNs) → mark(incr(pairNs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))active(take(0, XS)) → mark(nil)
active(take(s(N), cons(X, XS))) → mark(cons(X, take(N, XS)))active(zip(nil, XS)) → mark(nil)
active(zip(X, nil)) → mark(nil)active(zip(cons(X, XS), cons(Y, YS))) → mark(cons(pair(X, Y), zip(XS, YS)))
active(tail(cons(X, XS))) → mark(XS)active(repItems(nil)) → mark(nil)
active(repItems(cons(X, XS))) → mark(cons(X, cons(X, repItems(XS))))mark(pairNs) → active(pairNs)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))mark(oddNs) → active(oddNs)
mark(s(X)) → active(s(mark(X)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(zip(X1, X2)) → active(zip(mark(X1), mark(X2)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))mark(tail(X)) → active(tail(mark(X)))
mark(repItems(X)) → active(repItems(mark(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)incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)s(mark(X)) → s(X)
s(active(X)) → s(X)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)zip(mark(X1), X2) → zip(X1, X2)
zip(X1, mark(X2)) → zip(X1, X2)zip(active(X1), X2) → zip(X1, X2)
zip(X1, active(X2)) → zip(X1, X2)pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)repItems(mark(X)) → repItems(X)
repItems(active(X)) → repItems(X)

Original Signature

Termination of terms over the following signature is verified: zip, pair, mark, tail, 0, pairNs, s, repItems, take, active, incr, oddNs, 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 11: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(pairNs) → mark(cons(0, incr(oddNs)))active(oddNs) → mark(incr(pairNs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))active(take(0, XS)) → mark(nil)
active(take(s(N), cons(X, XS))) → mark(cons(X, take(N, XS)))active(zip(nil, XS)) → mark(nil)
active(zip(X, nil)) → mark(nil)active(zip(cons(X, XS), cons(Y, YS))) → mark(cons(pair(X, Y), zip(XS, YS)))
active(tail(cons(X, XS))) → mark(XS)active(repItems(nil)) → mark(nil)
active(repItems(cons(X, XS))) → mark(cons(X, cons(X, repItems(XS))))mark(pairNs) → active(pairNs)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))mark(oddNs) → active(oddNs)
mark(s(X)) → active(s(mark(X)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(zip(X1, X2)) → active(zip(mark(X1), mark(X2)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))mark(tail(X)) → active(tail(mark(X)))
mark(repItems(X)) → active(repItems(mark(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)incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)s(mark(X)) → s(X)
s(active(X)) → s(X)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)zip(mark(X1), X2) → zip(X1, X2)
zip(X1, mark(X2)) → zip(X1, X2)zip(active(X1), X2) → zip(X1, X2)
zip(X1, active(X2)) → zip(X1, X2)pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)repItems(mark(X)) → repItems(X)
repItems(active(X)) → repItems(X)

Original Signature

Termination of terms over the following signature is verified: zip, pair, mark, tail, 0, pairNs, s, repItems, take, active, incr, oddNs, cons, nil

Strategy

Function Precedence

mark < zip = pair = tail = cons# = 0 = s = pairNs = repItems = take = active = incr = oddNs = cons = nil

Argument Filtering

zip: collapses to 1
pair: 1 2
mark: collapses to 1
tail: collapses to 1
cons#: collapses to 2
0: all arguments are removed from 0
s: all arguments are removed from s
pairNs: all arguments are removed from pairNs
repItems: all arguments are removed from repItems
take: 1 2
active: 1
incr: collapses to 1
oddNs: all arguments are removed from oddNs
cons: all arguments are removed from cons
nil: all arguments are removed from nil

Status

pair: lexicographic with permutation 1 → 1 2 → 2
0: multiset
s: multiset
pairNs: multiset
repItems: multiset
take: lexicographic with permutation 1 → 2 2 → 1
active: multiset
oddNs: multiset
cons: multiset
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 4: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(pairNs) → mark(cons(0, incr(oddNs)))active(oddNs) → mark(incr(pairNs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))active(take(0, XS)) → mark(nil)
active(take(s(N), cons(X, XS))) → mark(cons(X, take(N, XS)))active(zip(nil, XS)) → mark(nil)
active(zip(X, nil)) → mark(nil)active(zip(cons(X, XS), cons(Y, YS))) → mark(cons(pair(X, Y), zip(XS, YS)))
active(tail(cons(X, XS))) → mark(XS)active(repItems(nil)) → mark(nil)
active(repItems(cons(X, XS))) → mark(cons(X, cons(X, repItems(XS))))mark(pairNs) → active(pairNs)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))mark(oddNs) → active(oddNs)
mark(s(X)) → active(s(mark(X)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(zip(X1, X2)) → active(zip(mark(X1), mark(X2)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))mark(tail(X)) → active(tail(mark(X)))
mark(repItems(X)) → active(repItems(mark(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)incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)s(mark(X)) → s(X)
s(active(X)) → s(X)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)zip(mark(X1), X2) → zip(X1, X2)
zip(X1, mark(X2)) → zip(X1, X2)zip(active(X1), X2) → zip(X1, X2)
zip(X1, active(X2)) → zip(X1, X2)pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)repItems(mark(X)) → repItems(X)
repItems(active(X)) → repItems(X)

Original Signature

Termination of terms over the following signature is verified: zip, pair, mark, tail, 0, pairNs, s, repItems, take, active, incr, oddNs, nil, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 12: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(pairNs) → mark(cons(0, incr(oddNs)))active(oddNs) → mark(incr(pairNs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))active(take(0, XS)) → mark(nil)
active(take(s(N), cons(X, XS))) → mark(cons(X, take(N, XS)))active(zip(nil, XS)) → mark(nil)
active(zip(X, nil)) → mark(nil)active(zip(cons(X, XS), cons(Y, YS))) → mark(cons(pair(X, Y), zip(XS, YS)))
active(tail(cons(X, XS))) → mark(XS)active(repItems(nil)) → mark(nil)
active(repItems(cons(X, XS))) → mark(cons(X, cons(X, repItems(XS))))mark(pairNs) → active(pairNs)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))mark(oddNs) → active(oddNs)
mark(s(X)) → active(s(mark(X)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(zip(X1, X2)) → active(zip(mark(X1), mark(X2)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))mark(tail(X)) → active(tail(mark(X)))
mark(repItems(X)) → active(repItems(mark(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)incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)s(mark(X)) → s(X)
s(active(X)) → s(X)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)zip(mark(X1), X2) → zip(X1, X2)
zip(X1, mark(X2)) → zip(X1, X2)zip(active(X1), X2) → zip(X1, X2)
zip(X1, active(X2)) → zip(X1, X2)pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)repItems(mark(X)) → repItems(X)
repItems(active(X)) → repItems(X)

Original Signature

Termination of terms over the following signature is verified: zip, pair, mark, tail, 0, pairNs, s, repItems, take, active, incr, oddNs, cons, nil

Strategy

Function Precedence

active < mark < zip = pair = zip# = tail = 0 = s = pairNs = repItems = take = incr = oddNs = cons = nil

Argument Filtering

zip: all arguments are removed from zip
pair: all arguments are removed from pair
zip#: 1 2
mark: 1
tail: collapses to 1
0: all arguments are removed from 0
s: 1
pairNs: all arguments are removed from pairNs
repItems: all arguments are removed from repItems
take: all arguments are removed from take
active: collapses to 1
incr: all arguments are removed from incr
oddNs: all arguments are removed from oddNs
cons: 1 2
nil: all arguments are removed from nil

Status

zip: multiset
pair: multiset
zip#: lexicographic with permutation 1 → 2 2 → 1
mark: multiset
0: multiset
s: lexicographic with permutation 1 → 1
pairNs: multiset
repItems: multiset
take: multiset
incr: multiset
oddNs: multiset
cons: lexicographic with permutation 1 → 2 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.

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

Problem 16: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(pairNs) → mark(cons(0, incr(oddNs)))active(oddNs) → mark(incr(pairNs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))active(take(0, XS)) → mark(nil)
active(take(s(N), cons(X, XS))) → mark(cons(X, take(N, XS)))active(zip(nil, XS)) → mark(nil)
active(zip(X, nil)) → mark(nil)active(zip(cons(X, XS), cons(Y, YS))) → mark(cons(pair(X, Y), zip(XS, YS)))
active(tail(cons(X, XS))) → mark(XS)active(repItems(nil)) → mark(nil)
active(repItems(cons(X, XS))) → mark(cons(X, cons(X, repItems(XS))))mark(pairNs) → active(pairNs)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))mark(oddNs) → active(oddNs)
mark(s(X)) → active(s(mark(X)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(zip(X1, X2)) → active(zip(mark(X1), mark(X2)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))mark(tail(X)) → active(tail(mark(X)))
mark(repItems(X)) → active(repItems(mark(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)incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)s(mark(X)) → s(X)
s(active(X)) → s(X)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)zip(mark(X1), X2) → zip(X1, X2)
zip(X1, mark(X2)) → zip(X1, X2)zip(active(X1), X2) → zip(X1, X2)
zip(X1, active(X2)) → zip(X1, X2)pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)repItems(mark(X)) → repItems(X)
repItems(active(X)) → repItems(X)

Original Signature

Termination of terms over the following signature is verified: zip, pair, mark, tail, 0, pairNs, s, repItems, take, active, incr, oddNs, nil, cons

Strategy

Function Precedence

zip = pair = zip# = mark = tail = 0 = s = pairNs = repItems = take = active = incr = oddNs = cons = nil

Argument Filtering

zip: all arguments are removed from zip
pair: 1 2
zip#: collapses to 2
mark: collapses to 1
tail: all arguments are removed from tail
0: all arguments are removed from 0
s: collapses to 1
pairNs: all arguments are removed from pairNs
repItems: collapses to 1
take: 1
active: 1
incr: all arguments are removed from incr
oddNs: all arguments are removed from oddNs
cons: all arguments are removed from cons
nil: all arguments are removed from nil

Status

zip: multiset
pair: lexicographic with permutation 1 → 1 2 → 2
tail: multiset
0: multiset
pairNs: multiset
take: lexicographic with permutation 1 → 1
active: multiset
incr: multiset
oddNs: multiset
cons: multiset
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.

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

Problem 6: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

repItems#(active(X)) → repItems#(X)repItems#(mark(X)) → repItems#(X)

Rewrite Rules

active(pairNs) → mark(cons(0, incr(oddNs)))active(oddNs) → mark(incr(pairNs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))active(take(0, XS)) → mark(nil)
active(take(s(N), cons(X, XS))) → mark(cons(X, take(N, XS)))active(zip(nil, XS)) → mark(nil)
active(zip(X, nil)) → mark(nil)active(zip(cons(X, XS), cons(Y, YS))) → mark(cons(pair(X, Y), zip(XS, YS)))
active(tail(cons(X, XS))) → mark(XS)active(repItems(nil)) → mark(nil)
active(repItems(cons(X, XS))) → mark(cons(X, cons(X, repItems(XS))))mark(pairNs) → active(pairNs)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))mark(oddNs) → active(oddNs)
mark(s(X)) → active(s(mark(X)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(zip(X1, X2)) → active(zip(mark(X1), mark(X2)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))mark(tail(X)) → active(tail(mark(X)))
mark(repItems(X)) → active(repItems(mark(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)incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)s(mark(X)) → s(X)
s(active(X)) → s(X)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)zip(mark(X1), X2) → zip(X1, X2)
zip(X1, mark(X2)) → zip(X1, X2)zip(active(X1), X2) → zip(X1, X2)
zip(X1, active(X2)) → zip(X1, X2)pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)repItems(mark(X)) → repItems(X)
repItems(active(X)) → repItems(X)

Original Signature

Termination of terms over the following signature is verified: zip, pair, mark, tail, 0, pairNs, s, repItems, take, active, incr, oddNs, nil, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

repItems#(active(X)) → repItems#(X)repItems#(mark(X)) → repItems#(X)

Problem 7: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(pairNs) → mark(cons(0, incr(oddNs)))active(oddNs) → mark(incr(pairNs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))active(take(0, XS)) → mark(nil)
active(take(s(N), cons(X, XS))) → mark(cons(X, take(N, XS)))active(zip(nil, XS)) → mark(nil)
active(zip(X, nil)) → mark(nil)active(zip(cons(X, XS), cons(Y, YS))) → mark(cons(pair(X, Y), zip(XS, YS)))
active(tail(cons(X, XS))) → mark(XS)active(repItems(nil)) → mark(nil)
active(repItems(cons(X, XS))) → mark(cons(X, cons(X, repItems(XS))))mark(pairNs) → active(pairNs)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))mark(oddNs) → active(oddNs)
mark(s(X)) → active(s(mark(X)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(zip(X1, X2)) → active(zip(mark(X1), mark(X2)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))mark(tail(X)) → active(tail(mark(X)))
mark(repItems(X)) → active(repItems(mark(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)incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)s(mark(X)) → s(X)
s(active(X)) → s(X)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)zip(mark(X1), X2) → zip(X1, X2)
zip(X1, mark(X2)) → zip(X1, X2)zip(active(X1), X2) → zip(X1, X2)
zip(X1, active(X2)) → zip(X1, X2)pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)repItems(mark(X)) → repItems(X)
repItems(active(X)) → repItems(X)

Original Signature

Termination of terms over the following signature is verified: zip, pair, mark, tail, 0, pairNs, s, repItems, take, active, incr, oddNs, nil, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 13: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(pairNs) → mark(cons(0, incr(oddNs)))active(oddNs) → mark(incr(pairNs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))active(take(0, XS)) → mark(nil)
active(take(s(N), cons(X, XS))) → mark(cons(X, take(N, XS)))active(zip(nil, XS)) → mark(nil)
active(zip(X, nil)) → mark(nil)active(zip(cons(X, XS), cons(Y, YS))) → mark(cons(pair(X, Y), zip(XS, YS)))
active(tail(cons(X, XS))) → mark(XS)active(repItems(nil)) → mark(nil)
active(repItems(cons(X, XS))) → mark(cons(X, cons(X, repItems(XS))))mark(pairNs) → active(pairNs)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))mark(oddNs) → active(oddNs)
mark(s(X)) → active(s(mark(X)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(zip(X1, X2)) → active(zip(mark(X1), mark(X2)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))mark(tail(X)) → active(tail(mark(X)))
mark(repItems(X)) → active(repItems(mark(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)incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)s(mark(X)) → s(X)
s(active(X)) → s(X)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)zip(mark(X1), X2) → zip(X1, X2)
zip(X1, mark(X2)) → zip(X1, X2)zip(active(X1), X2) → zip(X1, X2)
zip(X1, active(X2)) → zip(X1, X2)pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)repItems(mark(X)) → repItems(X)
repItems(active(X)) → repItems(X)

Original Signature

Termination of terms over the following signature is verified: zip, pair, mark, tail, 0, pairNs, s, repItems, take, active, incr, oddNs, cons, nil

Strategy

Function Precedence

mark < active < zip = pair = tail = pair# = 0 = s = pairNs = repItems = take = incr = oddNs = cons = nil

Argument Filtering

zip: all arguments are removed from zip
pair: all arguments are removed from pair
mark: collapses to 1
tail: all arguments are removed from tail
pair#: collapses to 2
0: all arguments are removed from 0
s: collapses to 1
pairNs: all arguments are removed from pairNs
repItems: all arguments are removed from repItems
take: all arguments are removed from take
active: 1
incr: collapses to 1
oddNs: all arguments are removed from oddNs
cons: 1
nil: all arguments are removed from nil

Status

zip: multiset
pair: multiset
tail: multiset
0: multiset
pairNs: multiset
repItems: multiset
take: multiset
active: lexicographic with permutation 1 → 1
oddNs: multiset
cons: lexicographic with permutation 1 → 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.

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

Problem 17: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(pairNs) → mark(cons(0, incr(oddNs)))active(oddNs) → mark(incr(pairNs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))active(take(0, XS)) → mark(nil)
active(take(s(N), cons(X, XS))) → mark(cons(X, take(N, XS)))active(zip(nil, XS)) → mark(nil)
active(zip(X, nil)) → mark(nil)active(zip(cons(X, XS), cons(Y, YS))) → mark(cons(pair(X, Y), zip(XS, YS)))
active(tail(cons(X, XS))) → mark(XS)active(repItems(nil)) → mark(nil)
active(repItems(cons(X, XS))) → mark(cons(X, cons(X, repItems(XS))))mark(pairNs) → active(pairNs)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))mark(oddNs) → active(oddNs)
mark(s(X)) → active(s(mark(X)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(zip(X1, X2)) → active(zip(mark(X1), mark(X2)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))mark(tail(X)) → active(tail(mark(X)))
mark(repItems(X)) → active(repItems(mark(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)incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)s(mark(X)) → s(X)
s(active(X)) → s(X)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)zip(mark(X1), X2) → zip(X1, X2)
zip(X1, mark(X2)) → zip(X1, X2)zip(active(X1), X2) → zip(X1, X2)
zip(X1, active(X2)) → zip(X1, X2)pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)repItems(mark(X)) → repItems(X)
repItems(active(X)) → repItems(X)

Original Signature

Termination of terms over the following signature is verified: zip, pair, mark, tail, 0, pairNs, s, repItems, take, active, incr, oddNs, nil, cons

Strategy

Function Precedence

mark < zip = pair = tail = pair# = 0 = s = pairNs = repItems = take = active = incr = oddNs = cons = nil

Argument Filtering

zip: collapses to 2
pair: collapses to 2
mark: 1
tail: collapses to 1
pair#: collapses to 2
0: all arguments are removed from 0
s: collapses to 1
pairNs: all arguments are removed from pairNs
repItems: collapses to 1
take: all arguments are removed from take
active: all arguments are removed from active
incr: all arguments are removed from incr
oddNs: all arguments are removed from oddNs
cons: all arguments are removed from cons
nil: all arguments are removed from nil

Status

mark: multiset
0: multiset
pairNs: multiset
take: multiset
active: multiset
incr: multiset
oddNs: multiset
cons: multiset
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.

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

Problem 8: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(pairNs) → mark(cons(0, incr(oddNs)))active(oddNs) → mark(incr(pairNs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))active(take(0, XS)) → mark(nil)
active(take(s(N), cons(X, XS))) → mark(cons(X, take(N, XS)))active(zip(nil, XS)) → mark(nil)
active(zip(X, nil)) → mark(nil)active(zip(cons(X, XS), cons(Y, YS))) → mark(cons(pair(X, Y), zip(XS, YS)))
active(tail(cons(X, XS))) → mark(XS)active(repItems(nil)) → mark(nil)
active(repItems(cons(X, XS))) → mark(cons(X, cons(X, repItems(XS))))mark(pairNs) → active(pairNs)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))mark(oddNs) → active(oddNs)
mark(s(X)) → active(s(mark(X)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(zip(X1, X2)) → active(zip(mark(X1), mark(X2)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))mark(tail(X)) → active(tail(mark(X)))
mark(repItems(X)) → active(repItems(mark(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)incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)s(mark(X)) → s(X)
s(active(X)) → s(X)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)zip(mark(X1), X2) → zip(X1, X2)
zip(X1, mark(X2)) → zip(X1, X2)zip(active(X1), X2) → zip(X1, X2)
zip(X1, active(X2)) → zip(X1, X2)pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)repItems(mark(X)) → repItems(X)
repItems(active(X)) → repItems(X)

Original Signature

Termination of terms over the following signature is verified: zip, pair, mark, tail, 0, pairNs, s, repItems, take, active, incr, oddNs, 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 9: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(pairNs) → mark(cons(0, incr(oddNs)))active(oddNs) → mark(incr(pairNs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))active(take(0, XS)) → mark(nil)
active(take(s(N), cons(X, XS))) → mark(cons(X, take(N, XS)))active(zip(nil, XS)) → mark(nil)
active(zip(X, nil)) → mark(nil)active(zip(cons(X, XS), cons(Y, YS))) → mark(cons(pair(X, Y), zip(XS, YS)))
active(tail(cons(X, XS))) → mark(XS)active(repItems(nil)) → mark(nil)
active(repItems(cons(X, XS))) → mark(cons(X, cons(X, repItems(XS))))mark(pairNs) → active(pairNs)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))mark(oddNs) → active(oddNs)
mark(s(X)) → active(s(mark(X)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(zip(X1, X2)) → active(zip(mark(X1), mark(X2)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))mark(tail(X)) → active(tail(mark(X)))
mark(repItems(X)) → active(repItems(mark(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)incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)s(mark(X)) → s(X)
s(active(X)) → s(X)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)zip(mark(X1), X2) → zip(X1, X2)
zip(X1, mark(X2)) → zip(X1, X2)zip(active(X1), X2) → zip(X1, X2)
zip(X1, active(X2)) → zip(X1, X2)pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)repItems(mark(X)) → repItems(X)
repItems(active(X)) → repItems(X)

Original Signature

Termination of terms over the following signature is verified: zip, pair, mark, tail, 0, pairNs, s, repItems, take, active, incr, oddNs, 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 10: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(pairNs) → mark(cons(0, incr(oddNs)))active(oddNs) → mark(incr(pairNs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))active(take(0, XS)) → mark(nil)
active(take(s(N), cons(X, XS))) → mark(cons(X, take(N, XS)))active(zip(nil, XS)) → mark(nil)
active(zip(X, nil)) → mark(nil)active(zip(cons(X, XS), cons(Y, YS))) → mark(cons(pair(X, Y), zip(XS, YS)))
active(tail(cons(X, XS))) → mark(XS)active(repItems(nil)) → mark(nil)
active(repItems(cons(X, XS))) → mark(cons(X, cons(X, repItems(XS))))mark(pairNs) → active(pairNs)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))mark(oddNs) → active(oddNs)
mark(s(X)) → active(s(mark(X)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(zip(X1, X2)) → active(zip(mark(X1), mark(X2)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))mark(tail(X)) → active(tail(mark(X)))
mark(repItems(X)) → active(repItems(mark(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)incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)s(mark(X)) → s(X)
s(active(X)) → s(X)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)zip(mark(X1), X2) → zip(X1, X2)
zip(X1, mark(X2)) → zip(X1, X2)zip(active(X1), X2) → zip(X1, X2)
zip(X1, active(X2)) → zip(X1, X2)pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)repItems(mark(X)) → repItems(X)
repItems(active(X)) → repItems(X)

Original Signature

Termination of terms over the following signature is verified: zip, pair, mark, tail, 0, pairNs, s, repItems, take, active, incr, oddNs, nil, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 14: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(pairNs) → mark(cons(0, incr(oddNs)))active(oddNs) → mark(incr(pairNs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))active(take(0, XS)) → mark(nil)
active(take(s(N), cons(X, XS))) → mark(cons(X, take(N, XS)))active(zip(nil, XS)) → mark(nil)
active(zip(X, nil)) → mark(nil)active(zip(cons(X, XS), cons(Y, YS))) → mark(cons(pair(X, Y), zip(XS, YS)))
active(tail(cons(X, XS))) → mark(XS)active(repItems(nil)) → mark(nil)
active(repItems(cons(X, XS))) → mark(cons(X, cons(X, repItems(XS))))mark(pairNs) → active(pairNs)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))mark(oddNs) → active(oddNs)
mark(s(X)) → active(s(mark(X)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(zip(X1, X2)) → active(zip(mark(X1), mark(X2)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))mark(tail(X)) → active(tail(mark(X)))
mark(repItems(X)) → active(repItems(mark(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)incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)s(mark(X)) → s(X)
s(active(X)) → s(X)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)zip(mark(X1), X2) → zip(X1, X2)
zip(X1, mark(X2)) → zip(X1, X2)zip(active(X1), X2) → zip(X1, X2)
zip(X1, active(X2)) → zip(X1, X2)pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)repItems(mark(X)) → repItems(X)
repItems(active(X)) → repItems(X)

Original Signature

Termination of terms over the following signature is verified: zip, pair, mark, tail, 0, pairNs, s, repItems, take, active, incr, oddNs, cons, nil

Strategy

Function Precedence

active < mark < zip = pair = take# = tail = 0 = s = pairNs = repItems = take = incr = oddNs = cons = nil

Argument Filtering

zip: all arguments are removed from zip
pair: all arguments are removed from pair
mark: collapses to 1
take#: collapses to 2
tail: collapses to 1
0: all arguments are removed from 0
s: collapses to 1
pairNs: all arguments are removed from pairNs
repItems: all arguments are removed from repItems
take: collapses to 1
active: 1
incr: collapses to 1
oddNs: all arguments are removed from oddNs
cons: 1
nil: all arguments are removed from nil

Status

zip: multiset
pair: multiset
0: multiset
pairNs: multiset
repItems: multiset
active: multiset
oddNs: multiset
cons: lexicographic with permutation 1 → 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.

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

Problem 18: ReductionPairSAT

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(pairNs) → mark(cons(0, incr(oddNs)))active(oddNs) → mark(incr(pairNs))
active(incr(cons(X, XS))) → mark(cons(s(X), incr(XS)))active(take(0, XS)) → mark(nil)
active(take(s(N), cons(X, XS))) → mark(cons(X, take(N, XS)))active(zip(nil, XS)) → mark(nil)
active(zip(X, nil)) → mark(nil)active(zip(cons(X, XS), cons(Y, YS))) → mark(cons(pair(X, Y), zip(XS, YS)))
active(tail(cons(X, XS))) → mark(XS)active(repItems(nil)) → mark(nil)
active(repItems(cons(X, XS))) → mark(cons(X, cons(X, repItems(XS))))mark(pairNs) → active(pairNs)
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(0) → active(0)
mark(incr(X)) → active(incr(mark(X)))mark(oddNs) → active(oddNs)
mark(s(X)) → active(s(mark(X)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
mark(nil) → active(nil)mark(zip(X1, X2)) → active(zip(mark(X1), mark(X2)))
mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))mark(tail(X)) → active(tail(mark(X)))
mark(repItems(X)) → active(repItems(mark(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)incr(mark(X)) → incr(X)
incr(active(X)) → incr(X)s(mark(X)) → s(X)
s(active(X)) → s(X)take(mark(X1), X2) → take(X1, X2)
take(X1, mark(X2)) → take(X1, X2)take(active(X1), X2) → take(X1, X2)
take(X1, active(X2)) → take(X1, X2)zip(mark(X1), X2) → zip(X1, X2)
zip(X1, mark(X2)) → zip(X1, X2)zip(active(X1), X2) → zip(X1, X2)
zip(X1, active(X2)) → zip(X1, X2)pair(mark(X1), X2) → pair(X1, X2)
pair(X1, mark(X2)) → pair(X1, X2)pair(active(X1), X2) → pair(X1, X2)
pair(X1, active(X2)) → pair(X1, X2)tail(mark(X)) → tail(X)
tail(active(X)) → tail(X)repItems(mark(X)) → repItems(X)
repItems(active(X)) → repItems(X)

Original Signature

Termination of terms over the following signature is verified: zip, pair, mark, tail, 0, pairNs, s, repItems, take, active, incr, oddNs, nil, cons

Strategy

Function Precedence

mark < zip = pair = take# = tail = 0 = s = pairNs = repItems = take = active = incr = oddNs = cons = nil

Argument Filtering

zip: all arguments are removed from zip
pair: all arguments are removed from pair
mark: 1
take#: collapses to 2
tail: 1
0: all arguments are removed from 0
s: collapses to 1
pairNs: all arguments are removed from pairNs
repItems: collapses to 1
take: 1 2
active: collapses to 1
incr: all arguments are removed from incr
oddNs: all arguments are removed from oddNs
cons: all arguments are removed from cons
nil: all arguments are removed from nil

Status

zip: multiset
pair: multiset
mark: multiset
tail: lexicographic with permutation 1 → 1
0: multiset
pairNs: multiset
take: lexicographic with permutation 1 → 2 2 → 1
incr: multiset
oddNs: multiset
cons: multiset
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.

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