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 (16268ms).
 | – Problem 2 was processed with processor SubtermCriterion (2ms).
 |    | – Problem 16 was processed with processor PolynomialLinearRange4iUR (42ms).
 |    |    | – Problem 24 was processed with processor PolynomialLinearRange4iUR (16ms).
 | – Problem 3 was processed with processor SubtermCriterion (4ms).
 | – Problem 4 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 17 was processed with processor PolynomialLinearRange4iUR (126ms).
 |    |    | – Problem 23 was processed with processor PolynomialLinearRange4iUR (76ms).
 | – Problem 5 was processed with processor SubtermCriterion (1ms).
 | – Problem 6 was processed with processor SubtermCriterion (1ms).
 | – Problem 7 was processed with processor SubtermCriterion (2ms).
 | – Problem 8 was processed with processor SubtermCriterion (3ms).
 |    | – Problem 18 was processed with processor PolynomialLinearRange4iUR (69ms).
 |    |    | – Problem 26 remains open; application of the following processors failed [DependencyGraph (3ms), PolynomialLinearRange4iUR (5ms), DependencyGraph (2ms), PolynomialLinearRange4iUR (5ms), DependencyGraph (3ms), PolynomialLinearRange4iUR (0ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (8ms), DependencyGraph (3ms)].
 | – Problem 9 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (2746ms), PolynomialLinearRange4iUR (1283ms), DependencyGraph (2749ms), PolynomialLinearRange4iUR (1428ms), DependencyGraph (2762ms), PolynomialLinearRange4iUR (2000ms), DependencyGraph (2857ms), PolynomialLinearRange4iUR (2512ms), DependencyGraph (2841ms), PolynomialLinearRange8NegiUR (7500ms), DependencyGraph (2915ms), ReductionPairSAT (timeout)].
 | – Problem 10 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 19 was processed with processor PolynomialLinearRange4iUR (51ms).
 |    |    | – Problem 25 was processed with processor PolynomialLinearRange4iUR (29ms).
 | – Problem 11 was processed with processor SubtermCriterion (2ms).
 | – Problem 12 was processed with processor SubtermCriterion (3ms).
 |    | – Problem 20 was processed with processor PolynomialLinearRange4iUR (77ms).
 | – Problem 13 was processed with processor SubtermCriterion (2ms).
 |    | – Problem 21 was processed with processor PolynomialLinearRange4iUR (28ms).
 |    |    | – Problem 27 remains open; application of the following processors failed [DependencyGraph (2ms), PolynomialLinearRange4iUR (4ms), DependencyGraph (2ms), PolynomialLinearRange4iUR (21ms), DependencyGraph (2ms), PolynomialLinearRange4iUR (9ms), DependencyGraph (2ms), PolynomialLinearRange8NegiUR (16ms), DependencyGraph (3ms)].
 | – Problem 14 was processed with processor SubtermCriterion (1ms).
 | – Problem 15 was processed with processor SubtermCriterion (2ms).
 |    | – Problem 22 was processed with processor PolynomialLinearRange4iUR (57ms).
 |    |    | – Problem 28 remains open; application of the following processors failed [DependencyGraph (24ms), PolynomialLinearRange4iUR (3ms), DependencyGraph (26ms), PolynomialLinearRange4iUR (6ms), DependencyGraph (23ms), PolynomialLinearRange4iUR (10ms), DependencyGraph (26ms), PolynomialLinearRange8NegiUR (6ms), DependencyGraph (24ms)].

The following open problems remain:

Open Dependency Pair Problem 9

Dependency Pairs

active#(take(N, XS)) → mark#(fst(splitAt(N, XS)))mark#(fst(X)) → active#(fst(mark(X)))
mark#(head(X)) → active#(head(mark(X)))mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))
mark#(take(X1, X2)) → mark#(X1)active#(u(pair(YS, ZS), N, X, XS)) → mark#(pair(cons(X, YS), ZS))
active#(splitAt(0, XS)) → mark#(pair(nil, XS))mark#(pair(X1, X2)) → mark#(X2)
mark#(u(X1, X2, X3, X4)) → active#(u(mark(X1), X2, X3, X4))mark#(take(X1, X2)) → active#(take(mark(X1), mark(X2)))
active#(head(cons(N, XS))) → mark#(N)mark#(tail(X)) → active#(tail(mark(X)))
mark#(head(X)) → mark#(X)mark#(nil) → active#(nil)
mark#(splitAt(X1, X2)) → mark#(X1)active#(natsFrom(N)) → mark#(cons(N, natsFrom(s(N))))
active#(tail(cons(N, XS))) → mark#(XS)mark#(snd(X)) → active#(snd(mark(X)))
mark#(sel(X1, X2)) → mark#(X2)mark#(s(X)) → mark#(X)
mark#(natsFrom(X)) → active#(natsFrom(mark(X)))mark#(sel(X1, X2)) → mark#(X1)
mark#(fst(X)) → mark#(X)active#(afterNth(N, XS)) → mark#(snd(splitAt(N, XS)))
mark#(0) → active#(0)mark#(s(X)) → active#(s(mark(X)))
mark#(cons(X1, X2)) → mark#(X1)mark#(splitAt(X1, X2)) → mark#(X2)
mark#(snd(X)) → mark#(X)mark#(afterNth(X1, X2)) → mark#(X1)
mark#(natsFrom(X)) → mark#(X)mark#(splitAt(X1, X2)) → active#(splitAt(mark(X1), mark(X2)))
mark#(sel(X1, X2)) → active#(sel(mark(X1), mark(X2)))mark#(afterNth(X1, X2)) → active#(afterNth(mark(X1), mark(X2)))
mark#(pair(X1, X2)) → mark#(X1)active#(splitAt(s(N), cons(X, XS))) → mark#(u(splitAt(N, XS), N, X, XS))
mark#(tail(X)) → mark#(X)mark#(u(X1, X2, X3, X4)) → mark#(X1)
active#(sel(N, XS)) → mark#(head(afterNth(N, XS)))mark#(take(X1, X2)) → mark#(X2)
active#(snd(pair(XS, YS))) → mark#(YS)active#(fst(pair(XS, YS))) → mark#(XS)
mark#(afterNth(X1, X2)) → mark#(X2)mark#(pair(X1, X2)) → active#(pair(mark(X1), mark(X2)))

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil

Open Dependency Pair Problem 27

Dependency Pairs

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

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil

Open Dependency Pair Problem 26

Dependency Pairs

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

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil

Open Dependency Pair Problem 28

Dependency Pairs

u#(X1, mark(X2), X3, X4) → u#(X1, X2, X3, X4)u#(X1, X2, active(X3), X4) → u#(X1, X2, X3, X4)
u#(X1, X2, X3, active(X4)) → u#(X1, X2, X3, X4)u#(X1, active(X2), X3, X4) → u#(X1, X2, X3, X4)
u#(X1, X2, mark(X3), X4) → u#(X1, X2, X3, X4)

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

mark#(fst(X)) → active#(fst(mark(X)))active#(u(pair(YS, ZS), N, X, XS)) → mark#(pair(cons(X, YS), ZS))
active#(take(N, XS)) → splitAt#(N, XS)mark#(pair(X1, X2)) → mark#(X2)
mark#(take(X1, X2)) → active#(take(mark(X1), mark(X2)))u#(X1, X2, X3, active(X4)) → u#(X1, X2, X3, X4)
splitAt#(mark(X1), X2) → splitAt#(X1, X2)active#(afterNth(N, XS)) → snd#(splitAt(N, XS))
mark#(snd(X)) → active#(snd(mark(X)))active#(splitAt(0, XS)) → pair#(nil, XS)
mark#(s(X)) → mark#(X)mark#(sel(X1, X2)) → mark#(X1)
afterNth#(active(X1), X2) → afterNth#(X1, X2)mark#(cons(X1, X2)) → mark#(X1)
pair#(X1, mark(X2)) → pair#(X1, X2)splitAt#(X1, mark(X2)) → splitAt#(X1, X2)
mark#(afterNth(X1, X2)) → mark#(X1)fst#(active(X)) → fst#(X)
sel#(X1, mark(X2)) → sel#(X1, X2)active#(sel(N, XS)) → head#(afterNth(N, XS))
u#(active(X1), X2, X3, X4) → u#(X1, X2, X3, X4)mark#(pair(X1, X2)) → mark#(X1)
sel#(X1, active(X2)) → sel#(X1, X2)mark#(tail(X)) → mark#(X)
active#(u(pair(YS, ZS), N, X, XS)) → cons#(X, YS)head#(active(X)) → head#(X)
mark#(afterNth(X1, X2)) → mark#(X2)active#(take(N, XS)) → mark#(fst(splitAt(N, XS)))
pair#(mark(X1), X2) → pair#(X1, X2)active#(afterNth(N, XS)) → splitAt#(N, XS)
natsFrom#(mark(X)) → natsFrom#(X)cons#(mark(X1), X2) → cons#(X1, X2)
active#(splitAt(0, XS)) → mark#(pair(nil, XS))mark#(tail(X)) → tail#(mark(X))
mark#(splitAt(X1, X2)) → splitAt#(mark(X1), mark(X2))mark#(u(X1, X2, X3, X4)) → u#(mark(X1), X2, X3, X4)
mark#(head(X)) → mark#(X)mark#(splitAt(X1, X2)) → mark#(X1)
u#(X1, X2, active(X3), X4) → u#(X1, X2, X3, X4)splitAt#(X1, active(X2)) → splitAt#(X1, X2)
cons#(X1, mark(X2)) → cons#(X1, X2)mark#(fst(X)) → mark#(X)
active#(afterNth(N, XS)) → mark#(snd(splitAt(N, XS)))mark#(0) → active#(0)
mark#(s(X)) → active#(s(mark(X)))snd#(mark(X)) → snd#(X)
head#(mark(X)) → head#(X)pair#(X1, active(X2)) → pair#(X1, X2)
mark#(snd(X)) → mark#(X)mark#(natsFrom(X)) → mark#(X)
cons#(active(X1), X2) → cons#(X1, X2)mark#(afterNth(X1, X2)) → active#(afterNth(mark(X1), mark(X2)))
snd#(active(X)) → snd#(X)u#(mark(X1), X2, X3, X4) → u#(X1, X2, X3, X4)
active#(natsFrom(N)) → natsFrom#(s(N))mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))
mark#(fst(X)) → fst#(mark(X))mark#(take(X1, X2)) → mark#(X1)
active#(splitAt(s(N), cons(X, XS))) → u#(splitAt(N, XS), N, X, XS)mark#(snd(X)) → snd#(mark(X))
afterNth#(X1, mark(X2)) → afterNth#(X1, X2)mark#(u(X1, X2, X3, X4)) → active#(u(mark(X1), X2, X3, X4))
mark#(s(X)) → s#(mark(X))mark#(tail(X)) → active#(tail(mark(X)))
active#(sel(N, XS)) → afterNth#(N, XS)active#(natsFrom(N)) → mark#(cons(N, natsFrom(s(N))))
active#(tail(cons(N, XS))) → mark#(XS)afterNth#(mark(X1), X2) → afterNth#(X1, X2)
mark#(natsFrom(X)) → active#(natsFrom(mark(X)))pair#(active(X1), X2) → pair#(X1, X2)
mark#(sel(X1, X2)) → sel#(mark(X1), mark(X2))tail#(mark(X)) → tail#(X)
take#(X1, mark(X2)) → take#(X1, X2)mark#(splitAt(X1, X2)) → active#(splitAt(mark(X1), mark(X2)))
mark#(sel(X1, X2)) → active#(sel(mark(X1), mark(X2)))sel#(active(X1), X2) → sel#(X1, X2)
cons#(X1, active(X2)) → cons#(X1, X2)mark#(u(X1, X2, X3, X4)) → mark#(X1)
active#(snd(pair(XS, YS))) → mark#(YS)mark#(afterNth(X1, X2)) → afterNth#(mark(X1), mark(X2))
active#(splitAt(s(N), cons(X, XS))) → splitAt#(N, XS)sel#(mark(X1), X2) → sel#(X1, X2)
active#(u(pair(YS, ZS), N, X, XS)) → pair#(cons(X, YS), ZS)mark#(head(X)) → active#(head(mark(X)))
take#(mark(X1), X2) → take#(X1, X2)active#(natsFrom(N)) → s#(N)
mark#(pair(X1, X2)) → pair#(mark(X1), mark(X2))u#(X1, X2, X3, mark(X4)) → u#(X1, X2, X3, X4)
u#(X1, active(X2), X3, X4) → u#(X1, X2, X3, X4)splitAt#(active(X1), X2) → splitAt#(X1, X2)
u#(X1, X2, mark(X3), X4) → u#(X1, X2, X3, X4)active#(head(cons(N, XS))) → mark#(N)
mark#(nil) → active#(nil)take#(X1, active(X2)) → take#(X1, X2)
tail#(active(X)) → tail#(X)mark#(sel(X1, X2)) → mark#(X2)
fst#(mark(X)) → fst#(X)active#(take(N, XS)) → fst#(splitAt(N, XS))
afterNth#(X1, active(X2)) → afterNth#(X1, X2)mark#(cons(X1, X2)) → cons#(mark(X1), X2)
natsFrom#(active(X)) → natsFrom#(X)u#(X1, mark(X2), X3, X4) → u#(X1, X2, X3, X4)
mark#(splitAt(X1, X2)) → mark#(X2)mark#(head(X)) → head#(mark(X))
mark#(take(X1, X2)) → take#(mark(X1), mark(X2))s#(mark(X)) → s#(X)
active#(splitAt(s(N), cons(X, XS))) → mark#(u(splitAt(N, XS), N, X, XS))mark#(take(X1, X2)) → mark#(X2)
active#(sel(N, XS)) → mark#(head(afterNth(N, XS)))s#(active(X)) → s#(X)
active#(natsFrom(N)) → cons#(N, natsFrom(s(N)))active#(fst(pair(XS, YS))) → mark#(XS)
mark#(natsFrom(X)) → natsFrom#(mark(X))mark#(pair(X1, X2)) → active#(pair(mark(X1), mark(X2)))
take#(active(X1), X2) → take#(X1, X2)

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons

Strategy

The following SCCs where found

active#(take(N, XS)) → mark#(fst(splitAt(N, XS)))mark#(cons(X1, X2)) → active#(cons(mark(X1), X2))
mark#(head(X)) → active#(head(mark(X)))mark#(fst(X)) → active#(fst(mark(X)))
mark#(take(X1, X2)) → mark#(X1)active#(u(pair(YS, ZS), N, X, XS)) → mark#(pair(cons(X, YS), ZS))
active#(splitAt(0, XS)) → mark#(pair(nil, XS))mark#(pair(X1, X2)) → mark#(X2)
mark#(u(X1, X2, X3, X4)) → active#(u(mark(X1), X2, X3, X4))mark#(take(X1, X2)) → active#(take(mark(X1), mark(X2)))
active#(head(cons(N, XS))) → mark#(N)mark#(tail(X)) → active#(tail(mark(X)))
mark#(nil) → active#(nil)mark#(head(X)) → mark#(X)
active#(natsFrom(N)) → mark#(cons(N, natsFrom(s(N))))mark#(splitAt(X1, X2)) → mark#(X1)
active#(tail(cons(N, XS))) → mark#(XS)mark#(snd(X)) → active#(snd(mark(X)))
mark#(sel(X1, X2)) → mark#(X2)mark#(s(X)) → mark#(X)
mark#(sel(X1, X2)) → mark#(X1)mark#(natsFrom(X)) → active#(natsFrom(mark(X)))
mark#(fst(X)) → mark#(X)active#(afterNth(N, XS)) → mark#(snd(splitAt(N, XS)))
mark#(0) → active#(0)mark#(s(X)) → active#(s(mark(X)))
mark#(cons(X1, X2)) → mark#(X1)mark#(snd(X)) → mark#(X)
mark#(splitAt(X1, X2)) → mark#(X2)mark#(natsFrom(X)) → mark#(X)
mark#(afterNth(X1, X2)) → mark#(X1)mark#(sel(X1, X2)) → active#(sel(mark(X1), mark(X2)))
mark#(splitAt(X1, X2)) → active#(splitAt(mark(X1), mark(X2)))mark#(afterNth(X1, X2)) → active#(afterNth(mark(X1), mark(X2)))
mark#(pair(X1, X2)) → mark#(X1)active#(splitAt(s(N), cons(X, XS))) → mark#(u(splitAt(N, XS), N, X, XS))
mark#(tail(X)) → mark#(X)mark#(u(X1, X2, X3, X4)) → mark#(X1)
mark#(take(X1, X2)) → mark#(X2)active#(sel(N, XS)) → mark#(head(afterNth(N, XS)))
active#(snd(pair(XS, YS))) → mark#(YS)mark#(afterNth(X1, X2)) → mark#(X2)
active#(fst(pair(XS, YS))) → mark#(XS)mark#(pair(X1, X2)) → active#(pair(mark(X1), mark(X2)))
u#(mark(X1), X2, X3, X4) → u#(X1, X2, X3, X4)u#(active(X1), X2, X3, X4) → u#(X1, X2, X3, X4)
u#(X1, mark(X2), X3, X4) → u#(X1, X2, X3, X4)u#(X1, X2, active(X3), X4) → u#(X1, X2, X3, X4)
u#(X1, X2, X3, mark(X4)) → u#(X1, X2, X3, X4)u#(X1, active(X2), X3, X4) → u#(X1, X2, X3, X4)
u#(X1, X2, X3, active(X4)) → u#(X1, X2, X3, X4)u#(X1, X2, mark(X3), X4) → u#(X1, X2, X3, X4)
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)
sel#(active(X1), X2) → sel#(X1, X2)sel#(mark(X1), X2) → sel#(X1, X2)
sel#(X1, active(X2)) → sel#(X1, X2)sel#(X1, mark(X2)) → sel#(X1, X2)
pair#(mark(X1), X2) → pair#(X1, X2)pair#(X1, active(X2)) → pair#(X1, X2)
pair#(X1, mark(X2)) → pair#(X1, X2)pair#(active(X1), X2) → pair#(X1, X2)
afterNth#(active(X1), X2) → afterNth#(X1, X2)afterNth#(X1, mark(X2)) → afterNth#(X1, X2)
afterNth#(X1, active(X2)) → afterNth#(X1, X2)afterNth#(mark(X1), X2) → afterNth#(X1, X2)
fst#(mark(X)) → fst#(X)fst#(active(X)) → fst#(X)
natsFrom#(mark(X)) → natsFrom#(X)natsFrom#(active(X)) → natsFrom#(X)
tail#(active(X)) → tail#(X)tail#(mark(X)) → tail#(X)
snd#(active(X)) → snd#(X)snd#(mark(X)) → snd#(X)
s#(mark(X)) → s#(X)s#(active(X)) → s#(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)
splitAt#(X1, mark(X2)) → splitAt#(X1, X2)splitAt#(X1, active(X2)) → splitAt#(X1, X2)
splitAt#(active(X1), X2) → splitAt#(X1, X2)splitAt#(mark(X1), X2) → splitAt#(X1, X2)
head#(mark(X)) → head#(X)head#(active(X)) → head#(X)

Problem 2: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 16: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil

Strategy

Polynomial Interpretation

There are no usable rules

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

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

Problem 24: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons

Strategy

Polynomial Interpretation

There are no usable rules

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

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

Problem 3: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, 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 4: 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(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, 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 17: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil

Strategy

Polynomial Interpretation

There are no usable rules

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

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

Problem 23: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons

Strategy

Polynomial Interpretation

There are no usable rules

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

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

Problem 5: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

natsFrom#(mark(X)) → natsFrom#(X)natsFrom#(active(X)) → natsFrom#(X)

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

natsFrom#(mark(X)) → natsFrom#(X)natsFrom#(active(X)) → natsFrom#(X)

Problem 6: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, 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 7: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, 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 8: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, 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 18: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil

Strategy

Polynomial Interpretation

There are no usable rules

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

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

Problem 10: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 19: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil

Strategy

Polynomial Interpretation

There are no usable rules

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

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

Problem 25: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons

Strategy

Polynomial Interpretation

There are no usable rules

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

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

Problem 11: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

fst#(mark(X)) → fst#(X)fst#(active(X)) → fst#(X)

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

fst#(mark(X)) → fst#(X)fst#(active(X)) → fst#(X)

Problem 12: 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(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, 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 20: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil

Strategy

Polynomial Interpretation

There are no usable rules

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

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

Problem 13: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 21: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil

Strategy

Polynomial Interpretation

There are no usable rules

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

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

Problem 14: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

snd#(active(X)) → snd#(X)snd#(mark(X)) → snd#(X)

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

snd#(active(X)) → snd#(X)snd#(mark(X)) → snd#(X)

Problem 15: SubtermCriterion

Dependency Pair Problem

Dependency Pairs

u#(mark(X1), X2, X3, X4) → u#(X1, X2, X3, X4)u#(active(X1), X2, X3, X4) → u#(X1, X2, X3, X4)
u#(X1, mark(X2), X3, X4) → u#(X1, X2, X3, X4)u#(X1, X2, active(X3), X4) → u#(X1, X2, X3, X4)
u#(X1, X2, X3, mark(X4)) → u#(X1, X2, X3, X4)u#(X1, active(X2), X3, X4) → u#(X1, X2, X3, X4)
u#(X1, X2, X3, active(X4)) → u#(X1, X2, X3, X4)u#(X1, X2, mark(X3), X4) → u#(X1, X2, X3, X4)

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, nil, snd, cons

Strategy

Projection

The following projection was used:

Thus, the following dependency pairs are removed:

u#(mark(X1), X2, X3, X4) → u#(X1, X2, X3, X4)u#(active(X1), X2, X3, X4) → u#(X1, X2, X3, X4)

Problem 22: PolynomialLinearRange4iUR

Dependency Pair Problem

Dependency Pairs

u#(X1, mark(X2), X3, X4) → u#(X1, X2, X3, X4)u#(X1, X2, active(X3), X4) → u#(X1, X2, X3, X4)
u#(X1, X2, X3, mark(X4)) → u#(X1, X2, X3, X4)u#(X1, X2, X3, active(X4)) → u#(X1, X2, X3, X4)
u#(X1, active(X2), X3, X4) → u#(X1, X2, X3, X4)u#(X1, X2, mark(X3), X4) → u#(X1, X2, X3, X4)

Rewrite Rules

active(natsFrom(N)) → mark(cons(N, natsFrom(s(N))))active(fst(pair(XS, YS))) → mark(XS)
active(snd(pair(XS, YS))) → mark(YS)active(splitAt(0, XS)) → mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS))) → mark(u(splitAt(N, XS), N, X, XS))active(u(pair(YS, ZS), N, X, XS)) → mark(pair(cons(X, YS), ZS))
active(head(cons(N, XS))) → mark(N)active(tail(cons(N, XS))) → mark(XS)
active(sel(N, XS)) → mark(head(afterNth(N, XS)))active(take(N, XS)) → mark(fst(splitAt(N, XS)))
active(afterNth(N, XS)) → mark(snd(splitAt(N, XS)))mark(natsFrom(X)) → active(natsFrom(mark(X)))
mark(cons(X1, X2)) → active(cons(mark(X1), X2))mark(s(X)) → active(s(mark(X)))
mark(fst(X)) → active(fst(mark(X)))mark(pair(X1, X2)) → active(pair(mark(X1), mark(X2)))
mark(snd(X)) → active(snd(mark(X)))mark(splitAt(X1, X2)) → active(splitAt(mark(X1), mark(X2)))
mark(0) → active(0)mark(nil) → active(nil)
mark(u(X1, X2, X3, X4)) → active(u(mark(X1), X2, X3, X4))mark(head(X)) → active(head(mark(X)))
mark(tail(X)) → active(tail(mark(X)))mark(sel(X1, X2)) → active(sel(mark(X1), mark(X2)))
mark(afterNth(X1, X2)) → active(afterNth(mark(X1), mark(X2)))mark(take(X1, X2)) → active(take(mark(X1), mark(X2)))
natsFrom(mark(X)) → natsFrom(X)natsFrom(active(X)) → natsFrom(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)
fst(mark(X)) → fst(X)fst(active(X)) → fst(X)
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)
snd(mark(X)) → snd(X)snd(active(X)) → snd(X)
splitAt(mark(X1), X2) → splitAt(X1, X2)splitAt(X1, mark(X2)) → splitAt(X1, X2)
splitAt(active(X1), X2) → splitAt(X1, X2)splitAt(X1, active(X2)) → splitAt(X1, X2)
u(mark(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, mark(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, mark(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, mark(X4)) → u(X1, X2, X3, X4)
u(active(X1), X2, X3, X4) → u(X1, X2, X3, X4)u(X1, active(X2), X3, X4) → u(X1, X2, X3, X4)
u(X1, X2, active(X3), X4) → u(X1, X2, X3, X4)u(X1, X2, X3, active(X4)) → u(X1, X2, X3, X4)
head(mark(X)) → head(X)head(active(X)) → head(X)
tail(mark(X)) → tail(X)tail(active(X)) → tail(X)
sel(mark(X1), X2) → sel(X1, X2)sel(X1, mark(X2)) → sel(X1, X2)
sel(active(X1), X2) → sel(X1, X2)sel(X1, active(X2)) → sel(X1, X2)
afterNth(mark(X1), X2) → afterNth(X1, X2)afterNth(X1, mark(X2)) → afterNth(X1, X2)
afterNth(active(X1), X2) → afterNth(X1, X2)afterNth(X1, active(X2)) → afterNth(X1, X2)
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)

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, fst, u, 0, s, take, active, afterNth, head, sel, cons, snd, nil

Strategy

Polynomial Interpretation

There are no usable rules

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

u#(X1, X2, X3, mark(X4)) → u#(X1, X2, X3, X4)