TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (23478ms).
 | – Problem 2 was processed with processor SubtermCriterion (42ms).
 |    | – Problem 22 remains open; application of the following processors failed [DependencyGraph (3ms), PolynomialLinearRange4iUR (45ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (21ms), DependencyGraph (3ms)].
 | – Problem 3 was processed with processor SubtermCriterion (4ms).
 | – Problem 4 was processed with processor SubtermCriterion (3ms).
 | – Problem 5 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (10ms), PolynomialLinearRange4iUR (1250ms), DependencyGraph (8ms), PolynomialLinearRange8NegiUR (3750ms), DependencyGraph (8ms), ReductionPairSAT (timeout)].
 | – Problem 6 was processed with processor SubtermCriterion (2ms).
 |    | – Problem 23 remains open; application of the following processors failed [DependencyGraph (5ms), PolynomialLinearRange4iUR (15ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (20ms), DependencyGraph (2ms)].
 | – Problem 7 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 24 remains open; application of the following processors failed [DependencyGraph (4ms), PolynomialLinearRange4iUR (8ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (0ms), DependencyGraph (2ms)].
 | – Problem 8 was processed with processor SubtermCriterion (5ms).
 | – Problem 9 was processed with processor SubtermCriterion (2ms).
 | – Problem 10 was processed with processor DependencyGraph (938ms).
 |    | – Problem 27 remains open; application of the following processors failed [PolynomialLinearRange4iUR (37ms), DependencyGraph (573ms), PolynomialLinearRange8NegiUR (7ms), DependencyGraph (573ms)].
 | – Problem 11 was processed with processor SubtermCriterion (3ms).
 | – Problem 12 was processed with processor SubtermCriterion (2ms).
 | – Problem 13 was processed with processor DependencyGraph (870ms).
 |    | – Problem 28 remains open; application of the following processors failed [PolynomialLinearRange4iUR (61ms), DependencyGraph (577ms), PolynomialLinearRange8NegiUR (4ms), DependencyGraph (550ms)].
 | – Problem 14 was processed with processor SubtermCriterion (3ms).
 | – Problem 15 was processed with processor SubtermCriterion (2ms).
 | – Problem 16 was processed with processor SubtermCriterion (4ms).
 | – Problem 17 was processed with processor SubtermCriterion (1ms).
 | – Problem 18 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 26 remains open; application of the following processors failed [DependencyGraph (5ms), PolynomialLinearRange4iUR (31ms), DependencyGraph (4ms), PolynomialLinearRange8NegiUR (0ms), DependencyGraph (4ms)].
 | – Problem 19 was processed with processor SubtermCriterion (2ms).
 |    | – Problem 25 remains open; application of the following processors failed [DependencyGraph (3ms), PolynomialLinearRange4iUR (4ms), DependencyGraph (3ms), PolynomialLinearRange8NegiUR (25ms), DependencyGraph (3ms)].
 | – Problem 20 was processed with processor SubtermCriterion (1ms).
 | – Problem 21 was processed with processor SubtermCriterion (5ms).

The following open problems remain:



Open Dependency Pair Problem 5

Dependency Pairs

top#(mark(X))top#(proper(X))top#(ok(X))top#(active(X))

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, ok, U12, proper, afterNth, head, sel, top, nil, cons, snd




Open Dependency Pair Problem 23

Dependency Pairs

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

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top




Open Dependency Pair Problem 22

Dependency Pairs

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

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top




Open Dependency Pair Problem 25

Dependency Pairs

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

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top




Open Dependency Pair Problem 24

Dependency Pairs

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

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top




Open Dependency Pair Problem 27

Dependency Pairs

active#(U12(X1, X2))active#(X1)active#(take(X1, X2))active#(X2)
active#(fst(X))active#(X)active#(take(X1, X2))active#(X1)
active#(natsFrom(X))active#(X)active#(afterNth(X1, X2))active#(X2)
active#(U11(X1, X2, X3, X4))active#(X1)active#(afterNth(X1, X2))active#(X1)
active#(sel(X1, X2))active#(X2)active#(pair(X1, X2))active#(X2)
active#(s(X))active#(X)active#(sel(X1, X2))active#(X1)
active#(splitAt(X1, X2))active#(X2)active#(pair(X1, X2))active#(X1)
active#(tail(X))active#(X)active#(head(X))active#(X)
active#(splitAt(X1, X2))active#(X1)active#(and(X1, X2))active#(X1)
active#(snd(X))active#(X)active#(cons(X1, X2))active#(X1)

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, ok, U12, proper, afterNth, head, sel, top, nil, cons, snd




Open Dependency Pair Problem 26

Dependency Pairs

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

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top




Open Dependency Pair Problem 28

Dependency Pairs

active#(U12(X1, X2))active#(X1)active#(take(X1, X2))active#(X2)
active#(fst(X))active#(X)active#(take(X1, X2))active#(X1)
active#(natsFrom(X))active#(X)active#(afterNth(X1, X2))active#(X2)
active#(U11(X1, X2, X3, X4))active#(X1)active#(afterNth(X1, X2))active#(X1)
active#(sel(X1, X2))active#(X2)active#(pair(X1, X2))active#(X2)
active#(s(X))active#(X)active#(sel(X1, X2))active#(X1)
active#(splitAt(X1, X2))active#(X2)active#(pair(X1, X2))active#(X1)
active#(tail(X))active#(X)active#(head(X))active#(X)
active#(splitAt(X1, X2))active#(X1)active#(and(X1, X2))active#(X1)
active#(snd(X))active#(X)active#(cons(X1, X2))active#(X1)

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, ok, U12, proper, afterNth, head, sel, top, nil, cons, snd


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

proper#(cons(X1, X2))proper#(X1)active#(take(N, XS))splitAt#(N, XS)
proper#(tail(X))proper#(X)proper#(snd(X))snd#(proper(X))
splitAt#(mark(X1), X2)splitAt#(X1, X2)active#(afterNth(N, XS))snd#(splitAt(N, XS))
active#(take(X1, X2))take#(active(X1), X2)tail#(ok(X))tail#(X)
active#(splitAt(X1, X2))splitAt#(active(X1), X2)active#(splitAt(X1, X2))splitAt#(X1, active(X2))
active#(splitAt(0, XS))pair#(nil, XS)top#(mark(X))proper#(X)
active#(take(X1, X2))active#(X2)pair#(X1, mark(X2))pair#(X1, X2)
splitAt#(X1, mark(X2))splitAt#(X1, X2)and#(mark(X1), X2)and#(X1, X2)
sel#(X1, mark(X2))sel#(X1, X2)active#(afterNth(X1, X2))afterNth#(active(X1), X2)
active#(sel(N, XS))head#(afterNth(N, XS))head#(ok(X))head#(X)
active#(U12(X1, X2))U12#(active(X1), X2)sel#(ok(X1), ok(X2))sel#(X1, X2)
proper#(splitAt(X1, X2))proper#(X2)U11#(ok(X1), ok(X2), ok(X3), ok(X4))U11#(X1, X2, X3, X4)
pair#(mark(X1), X2)pair#(X1, X2)proper#(head(X))proper#(X)
active#(afterNth(N, XS))splitAt#(N, XS)natsFrom#(mark(X))natsFrom#(X)
proper#(U11(X1, X2, X3, X4))U11#(proper(X1), proper(X2), proper(X3), proper(X4))cons#(mark(X1), X2)cons#(X1, X2)
active#(U12(pair(YS, ZS), X))pair#(cons(X, YS), ZS)active#(afterNth(X1, X2))afterNth#(X1, active(X2))
top#(ok(X))active#(X)active#(and(X1, X2))and#(active(X1), X2)
active#(snd(X))snd#(active(X))active#(sel(X1, X2))active#(X1)
active#(pair(X1, X2))active#(X1)natsFrom#(ok(X))natsFrom#(X)
proper#(sel(X1, X2))proper#(X2)take#(ok(X1), ok(X2))take#(X1, X2)
active#(sel(X1, X2))sel#(active(X1), X2)active#(sel(X1, X2))sel#(X1, active(X2))
snd#(mark(X))snd#(X)head#(mark(X))head#(X)
active#(U12(X1, X2))active#(X1)pair#(ok(X1), ok(X2))pair#(X1, X2)
active#(head(X))head#(active(X))active#(afterNth(X1, X2))active#(X2)
active#(s(X))s#(active(X))s#(ok(X))s#(X)
proper#(pair(X1, X2))pair#(proper(X1), proper(X2))proper#(sel(X1, X2))proper#(X1)
proper#(tail(X))tail#(proper(X))active#(take(X1, X2))take#(X1, active(X2))
proper#(s(X))s#(proper(X))active#(splitAt(X1, X2))active#(X1)
active#(natsFrom(N))natsFrom#(s(N))top#(ok(X))top#(active(X))
proper#(natsFrom(X))proper#(X)U12#(ok(X1), ok(X2))U12#(X1, X2)
afterNth#(X1, mark(X2))afterNth#(X1, X2)cons#(ok(X1), ok(X2))cons#(X1, X2)
active#(U11(tt, N, X, XS))splitAt#(N, XS)proper#(U12(X1, X2))proper#(X2)
proper#(and(X1, X2))and#(proper(X1), proper(X2))active#(cons(X1, X2))cons#(active(X1), X2)
active#(U11(X1, X2, X3, X4))U11#(active(X1), X2, X3, X4)active#(tail(X))tail#(active(X))
active#(sel(N, XS))afterNth#(N, XS)active#(sel(X1, X2))active#(X2)
proper#(and(X1, X2))proper#(X2)active#(pair(X1, X2))active#(X2)
snd#(ok(X))snd#(X)U12#(mark(X1), X2)U12#(X1, X2)
active#(head(X))active#(X)afterNth#(mark(X1), X2)afterNth#(X1, X2)
proper#(afterNth(X1, X2))proper#(X1)top#(mark(X))top#(proper(X))
proper#(fst(X))fst#(proper(X))proper#(cons(X1, X2))proper#(X2)
active#(U11(tt, N, X, XS))U12#(splitAt(N, XS), X)proper#(pair(X1, X2))proper#(X2)
active#(pair(X1, X2))pair#(active(X1), X2)tail#(mark(X))tail#(X)
take#(X1, mark(X2))take#(X1, X2)proper#(afterNth(X1, X2))proper#(X2)
proper#(pair(X1, X2))proper#(X1)proper#(s(X))proper#(X)
proper#(snd(X))proper#(X)proper#(head(X))head#(proper(X))
active#(U11(X1, X2, X3, X4))active#(X1)proper#(U11(X1, X2, X3, X4))proper#(X2)
proper#(splitAt(X1, X2))splitAt#(proper(X1), proper(X2))proper#(natsFrom(X))natsFrom#(proper(X))
proper#(take(X1, X2))take#(proper(X1), proper(X2))active#(snd(X))active#(X)
proper#(U12(X1, X2))U12#(proper(X1), proper(X2))active#(cons(X1, X2))active#(X1)
sel#(mark(X1), X2)sel#(X1, X2)U11#(mark(X1), X2, X3, X4)U11#(X1, X2, X3, X4)
take#(mark(X1), X2)take#(X1, X2)active#(splitAt(s(N), cons(X, XS)))U11#(tt, N, X, XS)
active#(natsFrom(N))s#(N)active#(pair(X1, X2))pair#(X1, active(X2))
proper#(U11(X1, X2, X3, X4))proper#(X1)active#(natsFrom(X))active#(X)
and#(ok(X1), ok(X2))and#(X1, X2)proper#(U11(X1, X2, X3, X4))proper#(X4)
proper#(and(X1, X2))proper#(X1)proper#(fst(X))proper#(X)
proper#(sel(X1, X2))sel#(proper(X1), proper(X2))afterNth#(ok(X1), ok(X2))afterNth#(X1, X2)
active#(U12(pair(YS, ZS), X))cons#(X, YS)active#(afterNth(X1, X2))active#(X1)
splitAt#(ok(X1), ok(X2))splitAt#(X1, X2)active#(splitAt(X1, X2))active#(X2)
proper#(take(X1, X2))proper#(X1)fst#(mark(X))fst#(X)
active#(take(N, XS))fst#(splitAt(N, XS))active#(natsFrom(X))natsFrom#(active(X))
proper#(U11(X1, X2, X3, X4))proper#(X3)proper#(U12(X1, X2))proper#(X1)
active#(fst(X))fst#(active(X))active#(fst(X))active#(X)
active#(take(X1, X2))active#(X1)proper#(take(X1, X2))proper#(X2)
fst#(ok(X))fst#(X)s#(mark(X))s#(X)
proper#(cons(X1, X2))cons#(proper(X1), proper(X2))active#(s(X))active#(X)
active#(tail(X))active#(X)proper#(afterNth(X1, X2))afterNth#(proper(X1), proper(X2))
active#(natsFrom(N))cons#(N, natsFrom(s(N)))active#(and(X1, X2))active#(X1)
proper#(splitAt(X1, X2))proper#(X1)

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


The following SCCs where found

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

head#(ok(X)) → head#(X)head#(mark(X)) → head#(X)

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

active#(natsFrom(N)) → natsFrom#(s(N))active#(splitAt(s(N), cons(X, XS))) → U11#(tt, N, X, XS)
active#(natsFrom(X)) → active#(X)active#(afterNth(N, XS)) → snd#(splitAt(N, XS))
active#(afterNth(X1, X2)) → active#(X1)active#(sel(X1, X2)) → active#(X2)
active#(pair(X1, X2)) → active#(X2)active#(sel(X1, X2)) → active#(X1)
active#(splitAt(X1, X2)) → active#(X2)active#(pair(X1, X2)) → active#(X1)
active#(head(X)) → active#(X)active#(splitAt(0, XS)) → pair#(nil, XS)
active#(natsFrom(X)) → natsFrom#(active(X))active#(U12(X1, X2)) → active#(X1)
active#(take(X1, X2)) → active#(X2)active#(fst(X)) → fst#(active(X))
active#(fst(X)) → active#(X)active#(take(X1, X2)) → active#(X1)
active#(afterNth(X1, X2)) → active#(X2)active#(U11(X1, X2, X3, X4)) → active#(X1)
active#(s(X)) → active#(X)active#(tail(X)) → active#(X)
active#(and(X1, X2)) → active#(X1)active#(splitAt(X1, X2)) → active#(X1)
active#(snd(X)) → active#(X)active#(cons(X1, X2)) → active#(X1)

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

U11#(ok(X1), ok(X2), ok(X3), ok(X4)) → U11#(X1, X2, X3, X4)U11#(mark(X1), X2, X3, X4) → U11#(X1, X2, X3, X4)

s#(mark(X)) → s#(X)s#(ok(X)) → s#(X)

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

natsFrom#(mark(X)) → natsFrom#(X)natsFrom#(ok(X)) → natsFrom#(X)

tail#(ok(X)) → tail#(X)tail#(mark(X)) → tail#(X)

U12#(ok(X1), ok(X2)) → U12#(X1, X2)U12#(mark(X1), X2) → U12#(X1, X2)

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

active#(natsFrom(N)) → natsFrom#(s(N))active#(splitAt(s(N), cons(X, XS))) → U11#(tt, N, X, XS)
active#(natsFrom(X)) → active#(X)active#(afterNth(N, XS)) → snd#(splitAt(N, XS))
active#(afterNth(X1, X2)) → active#(X1)active#(sel(X1, X2)) → active#(X2)
active#(pair(X1, X2)) → active#(X2)active#(sel(X1, X2)) → active#(X1)
active#(splitAt(X1, X2)) → active#(X2)active#(pair(X1, X2)) → active#(X1)
active#(head(X)) → active#(X)active#(splitAt(0, XS)) → pair#(nil, XS)
active#(U12(X1, X2)) → active#(X1)active#(take(X1, X2)) → active#(X2)
active#(fst(X)) → fst#(active(X))active#(fst(X)) → active#(X)
active#(take(X1, X2)) → active#(X1)active#(afterNth(X1, X2)) → active#(X2)
active#(U11(X1, X2, X3, X4)) → active#(X1)active#(s(X)) → active#(X)
active#(tail(X)) → active#(X)active#(and(X1, X2)) → active#(X1)
active#(splitAt(X1, X2)) → active#(X1)active#(snd(X)) → active#(X)
active#(cons(X1, X2)) → active#(X1)

active#(U12(X1, X2)) → active#(X1)active#(take(X1, X2)) → active#(X2)
active#(fst(X)) → active#(X)active#(take(X1, X2)) → active#(X1)
active#(afterNth(X1, X2)) → active#(X2)active#(natsFrom(X)) → active#(X)
active#(U11(X1, X2, X3, X4)) → active#(X1)active#(sel(X1, X2)) → active#(X2)
active#(afterNth(X1, X2)) → active#(X1)active#(splitAt(X1, X2)) → active#(X2)
active#(pair(X1, X2)) → active#(X2)active#(sel(X1, X2)) → active#(X1)
active#(s(X)) → active#(X)active#(pair(X1, X2)) → active#(X1)
active#(tail(X)) → active#(X)active#(head(X)) → active#(X)
active#(splitAt(X1, X2)) → active#(X1)active#(and(X1, X2)) → active#(X1)
active#(snd(X)) → active#(X)active#(cons(X1, X2)) → active#(X1)

fst#(mark(X)) → fst#(X)fst#(ok(X)) → fst#(X)

snd#(mark(X)) → snd#(X)snd#(ok(X)) → snd#(X)

proper#(head(X)) → proper#(X)proper#(cons(X1, X2)) → proper#(X1)
proper#(tail(X)) → proper#(X)proper#(natsFrom(X)) → proper#(X)
proper#(U12(X1, X2)) → proper#(X2)proper#(U11(X1, X2, X3, X4)) → proper#(X1)
proper#(U11(X1, X2, X3, X4)) → proper#(X4)proper#(and(X1, X2)) → proper#(X1)
proper#(fst(X)) → proper#(X)proper#(and(X1, X2)) → proper#(X2)
proper#(take(X1, X2)) → proper#(X1)proper#(sel(X1, X2)) → proper#(X2)
proper#(afterNth(X1, X2)) → proper#(X1)proper#(U11(X1, X2, X3, X4)) → proper#(X3)
proper#(U12(X1, X2)) → proper#(X1)proper#(cons(X1, X2)) → proper#(X2)
proper#(pair(X1, X2)) → proper#(X2)proper#(take(X1, X2)) → proper#(X2)
proper#(afterNth(X1, X2)) → proper#(X2)proper#(pair(X1, X2)) → proper#(X1)
proper#(sel(X1, X2)) → proper#(X1)proper#(snd(X)) → proper#(X)
proper#(s(X)) → proper#(X)proper#(U11(X1, X2, X3, X4)) → proper#(X2)
proper#(splitAt(X1, X2)) → proper#(X2)proper#(splitAt(X1, X2)) → proper#(X1)

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

and#(ok(X1), ok(X2)) → and#(X1, X2)and#(mark(X1), X2) → and#(X1, X2)

top#(mark(X)) → top#(proper(X))top#(ok(X)) → top#(active(X))

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

proper#(head(X))proper#(X)proper#(cons(X1, X2))proper#(X1)
proper#(tail(X))proper#(X)proper#(natsFrom(X))proper#(X)
proper#(U12(X1, X2))proper#(X2)proper#(U11(X1, X2, X3, X4))proper#(X1)
proper#(U11(X1, X2, X3, X4))proper#(X4)proper#(and(X1, X2))proper#(X1)
proper#(fst(X))proper#(X)proper#(and(X1, X2))proper#(X2)
proper#(take(X1, X2))proper#(X1)proper#(sel(X1, X2))proper#(X2)
proper#(afterNth(X1, X2))proper#(X1)proper#(U11(X1, X2, X3, X4))proper#(X3)
proper#(U12(X1, X2))proper#(X1)proper#(cons(X1, X2))proper#(X2)
proper#(pair(X1, X2))proper#(X2)proper#(take(X1, X2))proper#(X2)
proper#(afterNth(X1, X2))proper#(X2)proper#(pair(X1, X2))proper#(X1)
proper#(sel(X1, X2))proper#(X1)proper#(s(X))proper#(X)
proper#(snd(X))proper#(X)proper#(U11(X1, X2, X3, X4))proper#(X2)
proper#(splitAt(X1, X2))proper#(X2)proper#(splitAt(X1, X2))proper#(X1)

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

proper#(cons(X1, X2))proper#(X1)proper#(head(X))proper#(X)
proper#(tail(X))proper#(X)proper#(natsFrom(X))proper#(X)
proper#(U11(X1, X2, X3, X4))proper#(X1)proper#(U12(X1, X2))proper#(X2)
proper#(U11(X1, X2, X3, X4))proper#(X4)proper#(fst(X))proper#(X)
proper#(and(X1, X2))proper#(X1)proper#(and(X1, X2))proper#(X2)
proper#(take(X1, X2))proper#(X1)proper#(sel(X1, X2))proper#(X2)
proper#(afterNth(X1, X2))proper#(X1)proper#(U11(X1, X2, X3, X4))proper#(X3)
proper#(U12(X1, X2))proper#(X1)proper#(cons(X1, X2))proper#(X2)
proper#(pair(X1, X2))proper#(X2)proper#(take(X1, X2))proper#(X2)
proper#(afterNth(X1, X2))proper#(X2)proper#(pair(X1, X2))proper#(X1)
proper#(sel(X1, X2))proper#(X1)proper#(s(X))proper#(X)
proper#(snd(X))proper#(X)proper#(U11(X1, X2, X3, X4))proper#(X2)
proper#(splitAt(X1, X2))proper#(X2)proper#(splitAt(X1, X2))proper#(X1)

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

tail#(ok(X))tail#(X)tail#(mark(X))tail#(X)

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

tail#(ok(X))tail#(X)tail#(mark(X))tail#(X)

Problem 6: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 7: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 8: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

active#(U12(X1, X2))active#(X1)active#(take(X1, X2))active#(X2)
active#(fst(X))active#(X)active#(take(X1, X2))active#(X1)
active#(natsFrom(X))active#(X)active#(afterNth(X1, X2))active#(X2)
active#(U11(X1, X2, X3, X4))active#(X1)active#(afterNth(X1, X2))active#(X1)
active#(sel(X1, X2))active#(X2)active#(s(X))active#(X)
active#(sel(X1, X2))active#(X1)active#(pair(X1, X2))active#(X2)
active#(splitAt(X1, X2))active#(X2)active#(pair(X1, X2))active#(X1)
active#(tail(X))active#(X)active#(head(X))active#(X)
active#(splitAt(X1, X2))active#(X1)active#(and(X1, X2))active#(X1)
active#(snd(X))active#(X)active#(cons(X1, X2))active#(X1)

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

active#(U12(X1, X2))active#(X1)active#(take(X1, X2))active#(X2)
active#(fst(X))active#(X)active#(take(X1, X2))active#(X1)
active#(natsFrom(X))active#(X)active#(afterNth(X1, X2))active#(X2)
active#(U11(X1, X2, X3, X4))active#(X1)active#(sel(X1, X2))active#(X2)
active#(afterNth(X1, X2))active#(X1)active#(sel(X1, X2))active#(X1)
active#(splitAt(X1, X2))active#(X2)active#(pair(X1, X2))active#(X2)
active#(s(X))active#(X)active#(pair(X1, X2))active#(X1)
active#(tail(X))active#(X)active#(head(X))active#(X)
active#(and(X1, X2))active#(X1)active#(splitAt(X1, X2))active#(X1)
active#(snd(X))active#(X)active#(cons(X1, X2))active#(X1)

Problem 9: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

head#(ok(X))head#(X)head#(mark(X))head#(X)

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

head#(ok(X))head#(X)head#(mark(X))head#(X)

Problem 10: DependencyGraph



Dependency Pair Problem

Dependency Pairs

active#(natsFrom(N))natsFrom#(s(N))active#(splitAt(s(N), cons(X, XS)))U11#(tt, N, X, XS)
active#(natsFrom(X))active#(X)active#(afterNth(N, XS))snd#(splitAt(N, XS))
active#(afterNth(X1, X2))active#(X1)active#(sel(X1, X2))active#(X2)
active#(pair(X1, X2))active#(X2)active#(sel(X1, X2))active#(X1)
active#(splitAt(X1, X2))active#(X2)active#(pair(X1, X2))active#(X1)
active#(head(X))active#(X)active#(splitAt(0, XS))pair#(nil, XS)
active#(natsFrom(X))natsFrom#(active(X))active#(U12(X1, X2))active#(X1)
active#(take(X1, X2))active#(X2)active#(fst(X))active#(X)
active#(fst(X))fst#(active(X))active#(take(X1, X2))active#(X1)
active#(afterNth(X1, X2))active#(X2)active#(U11(X1, X2, X3, X4))active#(X1)
active#(s(X))active#(X)active#(tail(X))active#(X)
active#(splitAt(X1, X2))active#(X1)active#(and(X1, X2))active#(X1)
active#(snd(X))active#(X)active#(cons(X1, X2))active#(X1)

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


The following SCCs where found

active#(U12(X1, X2)) → active#(X1)active#(take(X1, X2)) → active#(X2)
active#(fst(X)) → active#(X)active#(take(X1, X2)) → active#(X1)
active#(afterNth(X1, X2)) → active#(X2)active#(natsFrom(X)) → active#(X)
active#(U11(X1, X2, X3, X4)) → active#(X1)active#(sel(X1, X2)) → active#(X2)
active#(afterNth(X1, X2)) → active#(X1)active#(splitAt(X1, X2)) → active#(X2)
active#(sel(X1, X2)) → active#(X1)active#(s(X)) → active#(X)
active#(pair(X1, X2)) → active#(X2)active#(pair(X1, X2)) → active#(X1)
active#(tail(X)) → active#(X)active#(head(X)) → active#(X)
active#(and(X1, X2)) → active#(X1)active#(splitAt(X1, X2)) → active#(X1)
active#(snd(X)) → active#(X)active#(cons(X1, X2)) → active#(X1)

Problem 11: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

fst#(mark(X))fst#(X)fst#(ok(X))fst#(X)

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

fst#(mark(X))fst#(X)fst#(ok(X))fst#(X)

Problem 12: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U12#(ok(X1), ok(X2))U12#(X1, X2)U12#(mark(X1), X2)U12#(X1, X2)

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U12#(ok(X1), ok(X2))U12#(X1, X2)U12#(mark(X1), X2)U12#(X1, X2)

Problem 13: DependencyGraph



Dependency Pair Problem

Dependency Pairs

active#(natsFrom(N))natsFrom#(s(N))active#(splitAt(s(N), cons(X, XS)))U11#(tt, N, X, XS)
active#(natsFrom(X))active#(X)active#(afterNth(N, XS))snd#(splitAt(N, XS))
active#(afterNth(X1, X2))active#(X1)active#(sel(X1, X2))active#(X2)
active#(pair(X1, X2))active#(X2)active#(sel(X1, X2))active#(X1)
active#(splitAt(X1, X2))active#(X2)active#(pair(X1, X2))active#(X1)
active#(head(X))active#(X)active#(splitAt(0, XS))pair#(nil, XS)
active#(U12(X1, X2))active#(X1)active#(take(X1, X2))active#(X2)
active#(fst(X))active#(X)active#(fst(X))fst#(active(X))
active#(take(X1, X2))active#(X1)active#(afterNth(X1, X2))active#(X2)
active#(U11(X1, X2, X3, X4))active#(X1)active#(s(X))active#(X)
active#(tail(X))active#(X)active#(splitAt(X1, X2))active#(X1)
active#(and(X1, X2))active#(X1)active#(snd(X))active#(X)
active#(cons(X1, X2))active#(X1)

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


The following SCCs where found

active#(U12(X1, X2)) → active#(X1)active#(take(X1, X2)) → active#(X2)
active#(fst(X)) → active#(X)active#(take(X1, X2)) → active#(X1)
active#(afterNth(X1, X2)) → active#(X2)active#(natsFrom(X)) → active#(X)
active#(U11(X1, X2, X3, X4)) → active#(X1)active#(sel(X1, X2)) → active#(X2)
active#(afterNth(X1, X2)) → active#(X1)active#(splitAt(X1, X2)) → active#(X2)
active#(sel(X1, X2)) → active#(X1)active#(s(X)) → active#(X)
active#(pair(X1, X2)) → active#(X2)active#(pair(X1, X2)) → active#(X1)
active#(tail(X)) → active#(X)active#(head(X)) → active#(X)
active#(and(X1, X2)) → active#(X1)active#(splitAt(X1, X2)) → active#(X1)
active#(snd(X)) → active#(X)active#(cons(X1, X2)) → active#(X1)

Problem 14: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

snd#(mark(X))snd#(X)snd#(ok(X))snd#(X)

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

snd#(mark(X))snd#(X)snd#(ok(X))snd#(X)

Problem 15: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

s#(mark(X))s#(X)s#(ok(X))s#(X)

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

s#(mark(X))s#(X)s#(ok(X))s#(X)

Problem 16: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

natsFrom#(mark(X))natsFrom#(X)natsFrom#(ok(X))natsFrom#(X)

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

natsFrom#(mark(X))natsFrom#(X)natsFrom#(ok(X))natsFrom#(X)

Problem 17: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 18: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 19: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 20: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U11#(ok(X1), ok(X2), ok(X3), ok(X4))U11#(X1, X2, X3, X4)U11#(mark(X1), X2, X3, X4)U11#(X1, X2, X3, X4)

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U11#(ok(X1), ok(X2), ok(X3), ok(X4))U11#(X1, X2, X3, X4)U11#(mark(X1), X2, X3, X4)U11#(X1, X2, X3, X4)

Problem 21: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

and#(ok(X1), ok(X2))and#(X1, X2)and#(mark(X1), X2)and#(X1, X2)

Rewrite Rules

active(U11(tt, N, X, XS))mark(U12(splitAt(N, XS), X))active(U12(pair(YS, ZS), X))mark(pair(cons(X, YS), ZS))
active(afterNth(N, XS))mark(snd(splitAt(N, XS)))active(and(tt, X))mark(X)
active(fst(pair(X, Y)))mark(X)active(head(cons(N, XS)))mark(N)
active(natsFrom(N))mark(cons(N, natsFrom(s(N))))active(sel(N, XS))mark(head(afterNth(N, XS)))
active(snd(pair(X, Y)))mark(Y)active(splitAt(0, XS))mark(pair(nil, XS))
active(splitAt(s(N), cons(X, XS)))mark(U11(tt, N, X, XS))active(tail(cons(N, XS)))mark(XS)
active(take(N, XS))mark(fst(splitAt(N, XS)))active(U11(X1, X2, X3, X4))U11(active(X1), X2, X3, X4)
active(U12(X1, X2))U12(active(X1), X2)active(splitAt(X1, X2))splitAt(active(X1), X2)
active(splitAt(X1, X2))splitAt(X1, active(X2))active(pair(X1, X2))pair(active(X1), X2)
active(pair(X1, X2))pair(X1, active(X2))active(cons(X1, X2))cons(active(X1), X2)
active(afterNth(X1, X2))afterNth(active(X1), X2)active(afterNth(X1, X2))afterNth(X1, active(X2))
active(snd(X))snd(active(X))active(and(X1, X2))and(active(X1), X2)
active(fst(X))fst(active(X))active(head(X))head(active(X))
active(natsFrom(X))natsFrom(active(X))active(s(X))s(active(X))
active(sel(X1, X2))sel(active(X1), X2)active(sel(X1, X2))sel(X1, active(X2))
active(tail(X))tail(active(X))active(take(X1, X2))take(active(X1), X2)
active(take(X1, X2))take(X1, active(X2))U11(mark(X1), X2, X3, X4)mark(U11(X1, X2, X3, X4))
U12(mark(X1), X2)mark(U12(X1, X2))splitAt(mark(X1), X2)mark(splitAt(X1, X2))
splitAt(X1, mark(X2))mark(splitAt(X1, X2))pair(mark(X1), X2)mark(pair(X1, X2))
pair(X1, mark(X2))mark(pair(X1, X2))cons(mark(X1), X2)mark(cons(X1, X2))
afterNth(mark(X1), X2)mark(afterNth(X1, X2))afterNth(X1, mark(X2))mark(afterNth(X1, X2))
snd(mark(X))mark(snd(X))and(mark(X1), X2)mark(and(X1, X2))
fst(mark(X))mark(fst(X))head(mark(X))mark(head(X))
natsFrom(mark(X))mark(natsFrom(X))s(mark(X))mark(s(X))
sel(mark(X1), X2)mark(sel(X1, X2))sel(X1, mark(X2))mark(sel(X1, X2))
tail(mark(X))mark(tail(X))take(mark(X1), X2)mark(take(X1, X2))
take(X1, mark(X2))mark(take(X1, X2))proper(U11(X1, X2, X3, X4))U11(proper(X1), proper(X2), proper(X3), proper(X4))
proper(tt)ok(tt)proper(U12(X1, X2))U12(proper(X1), proper(X2))
proper(splitAt(X1, X2))splitAt(proper(X1), proper(X2))proper(pair(X1, X2))pair(proper(X1), proper(X2))
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(afterNth(X1, X2))afterNth(proper(X1), proper(X2))
proper(snd(X))snd(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(fst(X))fst(proper(X))proper(head(X))head(proper(X))
proper(natsFrom(X))natsFrom(proper(X))proper(s(X))s(proper(X))
proper(sel(X1, X2))sel(proper(X1), proper(X2))proper(0)ok(0)
proper(nil)ok(nil)proper(tail(X))tail(proper(X))
proper(take(X1, X2))take(proper(X1), proper(X2))U11(ok(X1), ok(X2), ok(X3), ok(X4))ok(U11(X1, X2, X3, X4))
U12(ok(X1), ok(X2))ok(U12(X1, X2))splitAt(ok(X1), ok(X2))ok(splitAt(X1, X2))
pair(ok(X1), ok(X2))ok(pair(X1, X2))cons(ok(X1), ok(X2))ok(cons(X1, X2))
afterNth(ok(X1), ok(X2))ok(afterNth(X1, X2))snd(ok(X))ok(snd(X))
and(ok(X1), ok(X2))ok(and(X1, X2))fst(ok(X))ok(fst(X))
head(ok(X))ok(head(X))natsFrom(ok(X))ok(natsFrom(X))
s(ok(X))ok(s(X))sel(ok(X1), ok(X2))ok(sel(X1, X2))
tail(ok(X))ok(tail(X))take(ok(X1), ok(X2))ok(take(X1, X2))
top(mark(X))top(proper(X))top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: pair, natsFrom, mark, tail, splitAt, and, fst, 0, s, tt, take, active, U11, U12, ok, afterNth, proper, head, sel, snd, cons, nil, top

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

and#(ok(X1), ok(X2))and#(X1, X2)and#(mark(X1), X2)and#(X1, X2)