TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (56964ms).
 | – Problem 2 was processed with processor SubtermCriterion (3ms).
 | – Problem 3 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (13ms)].
 | – Problem 4 was processed with processor SubtermCriterion (4ms).
 | – Problem 5 was processed with processor SubtermCriterion (3ms).
 | – Problem 6 was processed with processor SubtermCriterion (5ms).
 | – Problem 7 was processed with processor SubtermCriterion (3ms).
 | – Problem 8 was processed with processor SubtermCriterion (4ms).
 | – Problem 9 was processed with processor SubtermCriterion (2ms).
 | – Problem 10 was processed with processor SubtermCriterion (4ms).
 | – Problem 11 was processed with processor SubtermCriterion (3ms).
 | – Problem 12 was processed with processor SubtermCriterion (4ms).
 | – Problem 13 was processed with processor SubtermCriterion (3ms).
 |    | – Problem 29 remains open; application of the following processors failed [].
 | – Problem 14 remains open; application of the following processors failed [SubtermCriterion (3ms)].
 | – Problem 15 was processed with processor SubtermCriterion (4ms).
 | – Problem 16 was processed with processor SubtermCriterion (4ms).
 | – Problem 17 was processed with processor SubtermCriterion (2ms).
 | – Problem 18 was processed with processor SubtermCriterion (4ms).
 | – Problem 19 was processed with processor SubtermCriterion (2ms).
 | – Problem 20 was processed with processor SubtermCriterion (4ms).
 | – Problem 21 was processed with processor SubtermCriterion (3ms).
 | – Problem 22 remains open; application of the following processors failed [SubtermCriterion (3ms), DependencyGraph (timeout)].
 | – Problem 23 was processed with processor SubtermCriterion (3ms).
 | – Problem 24 was processed with processor SubtermCriterion (4ms).
 | – Problem 25 was processed with processor SubtermCriterion (7ms).
 | – Problem 26 was processed with processor SubtermCriterion (2ms).
 | – Problem 27 was processed with processor SubtermCriterion (3ms).
 | – Problem 28 was processed with processor SubtermCriterion (4ms).

The following open problems remain:



Open Dependency Pair Problem 3

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U93, U42, U41, U92, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U52, U81, U11, active, U31, nil




Open Dependency Pair Problem 13

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(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U93, U42, U41, U92, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U52, U81, U11, active, U31, nil




Open Dependency Pair Problem 14

Dependency Pairs

active#(U91(X1, X2, X3, X4)) → U91#(active(X1), X2, X3, X4)active#(U71(X1, X2, X3)) → U71#(active(X1), X2, X3)
active#(take(s(M), cons(N, IL))) → U91#(isNatIList(IL), IL, M, N)active#(U72(tt, L)) → length#(L)
active#(U51(X1, X2)) → active#(X1)active#(isNatIList(cons(V1, V2))) → U41#(isNat(V1), V2)
active#(take(s(M), cons(N, IL))) → isNatIList#(IL)active#(U81(X)) → U81#(active(X))
active#(U51(tt, V2)) → isNatList#(V2)active#(cons(X1, X2)) → cons#(active(X1), X2)
active#(U41(X1, X2)) → U41#(active(X1), X2)active#(U93(X1, X2, X3, X4)) → active#(X1)
active#(take(X1, X2)) → take#(active(X1), X2)active#(U61(X1, X2)) → U61#(active(X1), X2)
active#(isNat(length(V1))) → isNatList#(V1)active#(U31(X)) → U31#(active(X))
active#(U51(X1, X2)) → U51#(active(X1), X2)active#(length(cons(N, L))) → U71#(isNatList(L), L, N)
active#(U62(X)) → U62#(active(X))active#(U31(X)) → active#(X)
active#(U11(X)) → U11#(active(X))active#(take(X1, X2)) → active#(X2)
active#(U71(X1, X2, X3)) → active#(X1)active#(U61(X1, X2)) → active#(X1)
active#(length(X)) → active#(X)active#(U92(X1, X2, X3, X4)) → U92#(active(X1), X2, X3, X4)
active#(U62(X)) → active#(X)active#(U91(X1, X2, X3, X4)) → active#(X1)
active#(U81(X)) → active#(X)active#(isNatList(take(V1, V2))) → U61#(isNat(V1), V2)
active#(isNatIList(cons(V1, V2))) → isNat#(V1)active#(U41(X1, X2)) → active#(X1)
active#(U72(X1, X2)) → active#(X1)active#(cons(X1, X2)) → active#(X1)
active#(U91(tt, IL, M, N)) → U92#(isNat(M), IL, M, N)active#(U11(X)) → active#(X)
active#(U42(X)) → active#(X)active#(U21(X)) → active#(X)
active#(isNat(length(V1))) → U11#(isNatList(V1))active#(U41(tt, V2)) → U42#(isNatIList(V2))
active#(U93(tt, IL, M, N)) → take#(M, IL)active#(U92(tt, IL, M, N)) → isNat#(N)
active#(U61(tt, V2)) → U62#(isNatIList(V2))active#(U52(X)) → active#(X)
active#(isNat(s(V1))) → isNat#(V1)active#(U71(tt, L, N)) → isNat#(N)
active#(U93(X1, X2, X3, X4)) → U93#(active(X1), X2, X3, X4)active#(isNat(s(V1))) → U21#(isNat(V1))
active#(U61(tt, V2)) → isNatIList#(V2)active#(take(X1, X2)) → active#(X1)
active#(s(X)) → s#(active(X))active#(take(0, IL)) → U81#(isNatIList(IL))
active#(U91(tt, IL, M, N)) → isNat#(M)active#(s(X)) → active#(X)
active#(take(X1, X2)) → take#(X1, active(X2))active#(zeros) → cons#(0, zeros)
active#(U93(tt, IL, M, N)) → cons#(N, take(M, IL))active#(take(0, IL)) → isNatIList#(IL)
active#(U92(X1, X2, X3, X4)) → active#(X1)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U93, U42, U41, U92, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U52, U81, U11, active, U31, nil




Open Dependency Pair Problem 22

Dependency Pairs

active#(U91(X1, X2, X3, X4)) → U91#(active(X1), X2, X3, X4)active#(U71(X1, X2, X3)) → U71#(active(X1), X2, X3)
active#(take(s(M), cons(N, IL))) → U91#(isNatIList(IL), IL, M, N)active#(U72(tt, L)) → length#(L)
active#(U51(X1, X2)) → active#(X1)active#(isNatIList(cons(V1, V2))) → U41#(isNat(V1), V2)
active#(take(s(M), cons(N, IL))) → isNatIList#(IL)active#(U81(X)) → U81#(active(X))
active#(U51(tt, V2)) → isNatList#(V2)active#(cons(X1, X2)) → cons#(active(X1), X2)
active#(U41(X1, X2)) → U41#(active(X1), X2)active#(U93(X1, X2, X3, X4)) → active#(X1)
active#(take(X1, X2)) → take#(active(X1), X2)active#(U61(X1, X2)) → U61#(active(X1), X2)
active#(isNat(length(V1))) → isNatList#(V1)active#(U31(X)) → U31#(active(X))
active#(U51(X1, X2)) → U51#(active(X1), X2)active#(length(cons(N, L))) → U71#(isNatList(L), L, N)
active#(U62(X)) → U62#(active(X))active#(U31(X)) → active#(X)
active#(U11(X)) → U11#(active(X))active#(take(X1, X2)) → active#(X2)
active#(U71(X1, X2, X3)) → active#(X1)active#(U61(X1, X2)) → active#(X1)
active#(length(X)) → active#(X)active#(U92(X1, X2, X3, X4)) → U92#(active(X1), X2, X3, X4)
active#(U62(X)) → active#(X)active#(U91(X1, X2, X3, X4)) → active#(X1)
active#(U81(X)) → active#(X)active#(isNatList(take(V1, V2))) → U61#(isNat(V1), V2)
active#(isNatIList(cons(V1, V2))) → isNat#(V1)active#(U41(X1, X2)) → active#(X1)
active#(U72(X1, X2)) → active#(X1)active#(cons(X1, X2)) → active#(X1)
active#(U91(tt, IL, M, N)) → U92#(isNat(M), IL, M, N)active#(U11(X)) → active#(X)
active#(U42(X)) → active#(X)active#(U21(X)) → active#(X)
active#(U41(tt, V2)) → U42#(isNatIList(V2))active#(U93(tt, IL, M, N)) → take#(M, IL)
active#(U92(tt, IL, M, N)) → isNat#(N)active#(U61(tt, V2)) → U62#(isNatIList(V2))
active#(U52(X)) → active#(X)active#(isNat(s(V1))) → isNat#(V1)
active#(U71(tt, L, N)) → isNat#(N)active#(U93(X1, X2, X3, X4)) → U93#(active(X1), X2, X3, X4)
active#(isNat(s(V1))) → U21#(isNat(V1))active#(U61(tt, V2)) → isNatIList#(V2)
active#(take(X1, X2)) → active#(X1)active#(s(X)) → s#(active(X))
active#(take(0, IL)) → U81#(isNatIList(IL))active#(U91(tt, IL, M, N)) → isNat#(M)
active#(s(X)) → active#(X)active#(take(X1, X2)) → take#(X1, active(X2))
active#(zeros) → cons#(0, zeros)active#(U93(tt, IL, M, N)) → cons#(N, take(M, IL))
active#(take(0, IL)) → isNatIList#(IL)active#(U92(X1, X2, X3, X4)) → active#(X1)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U93, U42, U41, U92, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U52, U81, U11, active, U31, nil


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

active#(U71(X1, X2, X3)) → U71#(active(X1), X2, X3)proper#(U41(X1, X2)) → proper#(X2)
proper#(cons(X1, X2)) → proper#(X1)active#(take(s(M), cons(N, IL))) → U91#(isNatIList(IL), IL, M, N)
active#(U72(tt, L)) → length#(L)proper#(U41(X1, X2)) → proper#(X1)
proper#(length(X)) → length#(proper(X))active#(U92(tt, IL, M, N)) → U93#(isNat(N), IL, M, N)
active#(U51(X1, X2)) → active#(X1)U92#(ok(X1), ok(X2), ok(X3), ok(X4)) → U92#(X1, X2, X3, X4)
active#(U41(tt, V2)) → isNatIList#(V2)active#(U72(tt, L)) → s#(length(L))
proper#(U52(X)) → U52#(proper(X))active#(U21(X)) → U21#(active(X))
active#(U51(tt, V2)) → isNatList#(V2)active#(U51(tt, V2)) → U52#(isNatList(V2))
proper#(U93(X1, X2, X3, X4)) → U93#(proper(X1), proper(X2), proper(X3), proper(X4))active#(take(X1, X2)) → take#(active(X1), X2)
U51#(mark(X1), X2) → U51#(X1, X2)proper#(U93(X1, X2, X3, X4)) → proper#(X3)
proper#(U71(X1, X2, X3)) → proper#(X1)proper#(U71(X1, X2, X3)) → U71#(proper(X1), proper(X2), proper(X3))
proper#(U62(X)) → proper#(X)active#(isNat(length(V1))) → isNatList#(V1)
U72#(mark(X1), X2) → U72#(X1, X2)active#(U31(X)) → U31#(active(X))
proper#(U42(X)) → U42#(proper(X))proper#(U93(X1, X2, X3, X4)) → proper#(X1)
active#(U42(X)) → U42#(active(X))top#(mark(X)) → proper#(X)
proper#(U93(X1, X2, X3, X4)) → proper#(X2)proper#(U72(X1, X2)) → proper#(X2)
length#(mark(X)) → length#(X)U81#(mark(X)) → U81#(X)
active#(U11(X)) → U11#(active(X))active#(take(X1, X2)) → active#(X2)
active#(U71(X1, X2, X3)) → active#(X1)active#(U61(X1, X2)) → active#(X1)
U71#(mark(X1), X2, X3) → U71#(X1, X2, X3)active#(U92(X1, X2, X3, X4)) → U92#(active(X1), X2, X3, X4)
active#(length(X)) → active#(X)active#(U62(X)) → active#(X)
proper#(U71(X1, X2, X3)) → proper#(X3)isNat#(ok(X)) → isNat#(X)
active#(isNatIList(cons(V1, V2))) → isNat#(V1)isNatIList#(ok(X)) → isNatIList#(X)
active#(U41(X1, X2)) → active#(X1)proper#(U21(X)) → U21#(proper(X))
active#(U72(X1, X2)) → active#(X1)proper#(U62(X)) → U62#(proper(X))
active#(U91(tt, IL, M, N)) → U92#(isNat(M), IL, M, N)cons#(mark(X1), X2) → cons#(X1, X2)
proper#(U11(X)) → proper#(X)top#(ok(X)) → active#(X)
active#(isNat(length(V1))) → U11#(isNatList(V1))active#(U41(tt, V2)) → U42#(isNatIList(V2))
active#(U93(tt, IL, M, N)) → take#(M, IL)U62#(mark(X)) → U62#(X)
active#(U61(tt, V2)) → U62#(isNatIList(V2))active#(U52(X)) → active#(X)
proper#(isNatList(X)) → proper#(X)proper#(isNat(X)) → isNat#(proper(X))
proper#(U51(X1, X2)) → proper#(X2)take#(ok(X1), ok(X2)) → take#(X1, X2)
U42#(ok(X)) → U42#(X)proper#(U92(X1, X2, X3, X4)) → proper#(X4)
proper#(U21(X)) → proper#(X)active#(isNat(s(V1))) → isNat#(V1)
U11#(mark(X)) → U11#(X)proper#(U81(X)) → U81#(proper(X))
U51#(ok(X1), ok(X2)) → U51#(X1, X2)proper#(isNat(X)) → proper#(X)
active#(U52(X)) → U52#(active(X))active#(isNat(s(V1))) → U21#(isNat(V1))
active#(U61(tt, V2)) → isNatIList#(V2)proper#(U91(X1, X2, X3, X4)) → proper#(X3)
proper#(U72(X1, X2)) → proper#(X1)active#(s(X)) → s#(active(X))
U31#(ok(X)) → U31#(X)active#(isNatList(cons(V1, V2))) → U51#(isNat(V1), V2)
s#(ok(X)) → s#(X)proper#(U92(X1, X2, X3, X4)) → U92#(proper(X1), proper(X2), proper(X3), proper(X4))
U91#(mark(X1), X2, X3, X4) → U91#(X1, X2, X3, X4)proper#(length(X)) → proper#(X)
active#(U91(tt, IL, M, N)) → isNat#(M)active#(U72(X1, X2)) → U72#(active(X1), X2)
active#(take(X1, X2)) → take#(X1, active(X2))proper#(s(X)) → s#(proper(X))
active#(zeros) → cons#(0, zeros)active#(isNatIList(V)) → U31#(isNatList(V))
U81#(ok(X)) → U81#(X)proper#(U91(X1, X2, X3, X4)) → proper#(X1)
active#(U92(X1, X2, X3, X4)) → active#(X1)U92#(mark(X1), X2, X3, X4) → U92#(X1, X2, X3, X4)
active#(U91(X1, X2, X3, X4)) → U91#(active(X1), X2, X3, X4)top#(ok(X)) → top#(active(X))
proper#(U91(X1, X2, X3, X4)) → proper#(X2)active#(isNatIList(cons(V1, V2))) → U41#(isNat(V1), V2)
active#(take(s(M), cons(N, IL))) → isNatIList#(IL)proper#(U93(X1, X2, X3, X4)) → proper#(X4)
active#(U81(X)) → U81#(active(X))proper#(isNatIList(X)) → isNatIList#(proper(X))
cons#(ok(X1), ok(X2)) → cons#(X1, X2)proper#(U72(X1, X2)) → U72#(proper(X1), proper(X2))
proper#(U92(X1, X2, X3, X4)) → proper#(X2)active#(cons(X1, X2)) → cons#(active(X1), X2)
U42#(mark(X)) → U42#(X)proper#(U51(X1, X2)) → U51#(proper(X1), proper(X2))
active#(U93(X1, X2, X3, X4)) → active#(X1)active#(U41(X1, X2)) → U41#(active(X1), X2)
active#(U61(X1, X2)) → U61#(active(X1), X2)U91#(ok(X1), ok(X2), ok(X3), ok(X4)) → U91#(X1, X2, X3, X4)
proper#(U61(X1, X2)) → proper#(X2)U61#(mark(X1), X2) → U61#(X1, X2)
active#(U51(X1, X2)) → U51#(active(X1), X2)active#(length(cons(N, L))) → U71#(isNatList(L), L, N)
length#(ok(X)) → length#(X)active#(U62(X)) → U62#(active(X))
U21#(ok(X)) → U21#(X)U61#(ok(X1), ok(X2)) → U61#(X1, X2)
U71#(ok(X1), ok(X2), ok(X3)) → U71#(X1, X2, X3)active#(U31(X)) → active#(X)
top#(mark(X)) → top#(proper(X))proper#(cons(X1, X2)) → proper#(X2)
proper#(isNatIList(X)) → proper#(X)take#(X1, mark(X2)) → take#(X1, X2)
active#(U91(X1, X2, X3, X4)) → active#(X1)U52#(ok(X)) → U52#(X)
active#(U81(X)) → active#(X)isNatList#(ok(X)) → isNatList#(X)
U62#(ok(X)) → U62#(X)active#(isNatList(take(V1, V2))) → U61#(isNat(V1), V2)
proper#(s(X)) → proper#(X)proper#(U92(X1, X2, X3, X4)) → proper#(X3)
proper#(isNatList(X)) → isNatList#(proper(X))proper#(U91(X1, X2, X3, X4)) → proper#(X4)
proper#(take(X1, X2)) → take#(proper(X1), proper(X2))active#(isNatList(cons(V1, V2))) → isNat#(V1)
U31#(mark(X)) → U31#(X)proper#(U61(X1, X2)) → U61#(proper(X1), proper(X2))
active#(cons(X1, X2)) → active#(X1)take#(mark(X1), X2) → take#(X1, X2)
active#(U11(X)) → active#(X)active#(U42(X)) → active#(X)
proper#(U31(X)) → U31#(proper(X))U93#(mark(X1), X2, X3, X4) → U93#(X1, X2, X3, X4)
proper#(U42(X)) → proper#(X)proper#(U51(X1, X2)) → proper#(X1)
active#(U21(X)) → active#(X)active#(length(cons(N, L))) → isNatList#(L)
active#(U92(tt, IL, M, N)) → isNat#(N)U41#(ok(X1), ok(X2)) → U41#(X1, X2)
proper#(take(X1, X2)) → proper#(X1)active#(isNatList(take(V1, V2))) → isNat#(V1)
proper#(U11(X)) → U11#(proper(X))U41#(mark(X1), X2) → U41#(X1, X2)
active#(U71(tt, L, N)) → isNat#(N)active#(U93(X1, X2, X3, X4)) → U93#(active(X1), X2, X3, X4)
active#(length(X)) → length#(active(X))U21#(mark(X)) → U21#(X)
active#(take(X1, X2)) → active#(X1)proper#(U92(X1, X2, X3, X4)) → proper#(X1)
proper#(take(X1, X2)) → proper#(X2)proper#(U91(X1, X2, X3, X4)) → U91#(proper(X1), proper(X2), proper(X3), proper(X4))
proper#(U81(X)) → proper#(X)proper#(U41(X1, X2)) → U41#(proper(X1), proper(X2))
active#(isNatIList(V)) → isNatList#(V)proper#(U61(X1, X2)) → proper#(X1)
U72#(ok(X1), ok(X2)) → U72#(X1, X2)s#(mark(X)) → s#(X)
active#(take(0, IL)) → U81#(isNatIList(IL))proper#(cons(X1, X2)) → cons#(proper(X1), proper(X2))
active#(s(X)) → active#(X)U93#(ok(X1), ok(X2), ok(X3), ok(X4)) → U93#(X1, X2, X3, X4)
U52#(mark(X)) → U52#(X)active#(U93(tt, IL, M, N)) → cons#(N, take(M, IL))
U11#(ok(X)) → U11#(X)proper#(U71(X1, X2, X3)) → proper#(X2)
active#(U71(tt, L, N)) → U72#(isNat(N), L)active#(take(0, IL)) → isNatIList#(IL)
proper#(U52(X)) → proper#(X)proper#(U31(X)) → proper#(X)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


The following SCCs where found

U31#(ok(X)) → U31#(X)U31#(mark(X)) → U31#(X)

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

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

U21#(ok(X)) → U21#(X)U21#(mark(X)) → U21#(X)

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

U62#(mark(X)) → U62#(X)U62#(ok(X)) → U62#(X)

proper#(U41(X1, X2)) → proper#(X2)proper#(cons(X1, X2)) → proper#(X1)
proper#(U41(X1, X2)) → proper#(X1)proper#(U91(X1, X2, X3, X4)) → proper#(X2)
proper#(U93(X1, X2, X3, X4)) → proper#(X4)proper#(U11(X)) → proper#(X)
proper#(U51(X1, X2)) → proper#(X1)proper#(U42(X)) → proper#(X)
proper#(U92(X1, X2, X3, X4)) → proper#(X2)proper#(U93(X1, X2, X3, X4)) → proper#(X3)
proper#(U71(X1, X2, X3)) → proper#(X1)proper#(U62(X)) → proper#(X)
proper#(U93(X1, X2, X3, X4)) → proper#(X1)proper#(U61(X1, X2)) → proper#(X2)
proper#(take(X1, X2)) → proper#(X1)proper#(isNatList(X)) → proper#(X)
proper#(U51(X1, X2)) → proper#(X2)proper#(U92(X1, X2, X3, X4)) → proper#(X4)
proper#(U21(X)) → proper#(X)proper#(U93(X1, X2, X3, X4)) → proper#(X2)
proper#(U72(X1, X2)) → proper#(X2)proper#(isNat(X)) → proper#(X)
proper#(cons(X1, X2)) → proper#(X2)proper#(isNatIList(X)) → proper#(X)
proper#(U92(X1, X2, X3, X4)) → proper#(X1)proper#(U91(X1, X2, X3, X4)) → proper#(X3)
proper#(take(X1, X2)) → proper#(X2)proper#(U71(X1, X2, X3)) → proper#(X3)
proper#(U72(X1, X2)) → proper#(X1)proper#(U81(X)) → proper#(X)
proper#(U61(X1, X2)) → proper#(X1)proper#(U92(X1, X2, X3, X4)) → proper#(X3)
proper#(s(X)) → proper#(X)proper#(length(X)) → proper#(X)
proper#(U91(X1, X2, X3, X4)) → proper#(X4)proper#(U71(X1, X2, X3)) → proper#(X2)
proper#(U52(X)) → proper#(X)proper#(U91(X1, X2, X3, X4)) → proper#(X1)
proper#(U31(X)) → proper#(X)

U11#(ok(X)) → U11#(X)U11#(mark(X)) → U11#(X)

U71#(ok(X1), ok(X2), ok(X3)) → U71#(X1, X2, X3)U71#(mark(X1), X2, X3) → U71#(X1, X2, X3)

active#(U71(X1, X2, X3)) → U71#(active(X1), X2, X3)active#(U91(X1, X2, X3, X4)) → U91#(active(X1), X2, X3, X4)
active#(take(s(M), cons(N, IL))) → U91#(isNatIList(IL), IL, M, N)active#(U72(tt, L)) → length#(L)
active#(U51(X1, X2)) → active#(X1)active#(take(s(M), cons(N, IL))) → isNatIList#(IL)
active#(isNatIList(cons(V1, V2))) → U41#(isNat(V1), V2)active#(U81(X)) → U81#(active(X))
active#(U51(tt, V2)) → isNatList#(V2)active#(cons(X1, X2)) → cons#(active(X1), X2)
active#(take(X1, X2)) → take#(active(X1), X2)active#(U93(X1, X2, X3, X4)) → active#(X1)
active#(U41(X1, X2)) → U41#(active(X1), X2)active#(U61(X1, X2)) → U61#(active(X1), X2)
active#(isNat(length(V1))) → isNatList#(V1)active#(U31(X)) → U31#(active(X))
active#(U51(X1, X2)) → U51#(active(X1), X2)active#(length(cons(N, L))) → U71#(isNatList(L), L, N)
active#(U62(X)) → U62#(active(X))active#(U31(X)) → active#(X)
active#(U11(X)) → U11#(active(X))active#(U71(X1, X2, X3)) → active#(X1)
active#(take(X1, X2)) → active#(X2)active#(U61(X1, X2)) → active#(X1)
active#(U92(X1, X2, X3, X4)) → U92#(active(X1), X2, X3, X4)active#(length(X)) → active#(X)
active#(U62(X)) → active#(X)active#(U91(X1, X2, X3, X4)) → active#(X1)
active#(U81(X)) → active#(X)active#(isNatIList(cons(V1, V2))) → isNat#(V1)
active#(isNatList(take(V1, V2))) → U61#(isNat(V1), V2)active#(U41(X1, X2)) → active#(X1)
active#(U72(X1, X2)) → active#(X1)active#(cons(X1, X2)) → active#(X1)
active#(U91(tt, IL, M, N)) → U92#(isNat(M), IL, M, N)active#(U11(X)) → active#(X)
active#(U42(X)) → active#(X)active#(U21(X)) → active#(X)
active#(isNat(length(V1))) → U11#(isNatList(V1))active#(U93(tt, IL, M, N)) → take#(M, IL)
active#(U41(tt, V2)) → U42#(isNatIList(V2))active#(U92(tt, IL, M, N)) → isNat#(N)
active#(U52(X)) → active#(X)active#(U61(tt, V2)) → U62#(isNatIList(V2))
active#(isNat(s(V1))) → isNat#(V1)active#(U71(tt, L, N)) → isNat#(N)
active#(U93(X1, X2, X3, X4)) → U93#(active(X1), X2, X3, X4)active#(isNat(s(V1))) → U21#(isNat(V1))
active#(U61(tt, V2)) → isNatIList#(V2)active#(take(X1, X2)) → active#(X1)
active#(s(X)) → s#(active(X))active#(take(0, IL)) → U81#(isNatIList(IL))
active#(U91(tt, IL, M, N)) → isNat#(M)active#(take(X1, X2)) → take#(X1, active(X2))
active#(s(X)) → active#(X)active#(zeros) → cons#(0, zeros)
active#(U93(tt, IL, M, N)) → cons#(N, take(M, IL))active#(U92(X1, X2, X3, X4)) → active#(X1)
active#(take(0, IL)) → isNatIList#(IL)

active#(U71(X1, X2, X3)) → U71#(active(X1), X2, X3)active#(U91(X1, X2, X3, X4)) → U91#(active(X1), X2, X3, X4)
active#(take(s(M), cons(N, IL))) → U91#(isNatIList(IL), IL, M, N)active#(U72(tt, L)) → length#(L)
active#(U51(X1, X2)) → active#(X1)active#(take(s(M), cons(N, IL))) → isNatIList#(IL)
active#(isNatIList(cons(V1, V2))) → U41#(isNat(V1), V2)active#(U81(X)) → U81#(active(X))
active#(U51(tt, V2)) → isNatList#(V2)active#(cons(X1, X2)) → cons#(active(X1), X2)
active#(take(X1, X2)) → take#(active(X1), X2)active#(U93(X1, X2, X3, X4)) → active#(X1)
active#(U41(X1, X2)) → U41#(active(X1), X2)active#(U61(X1, X2)) → U61#(active(X1), X2)
active#(isNat(length(V1))) → isNatList#(V1)active#(U31(X)) → U31#(active(X))
active#(U51(X1, X2)) → U51#(active(X1), X2)active#(length(cons(N, L))) → U71#(isNatList(L), L, N)
active#(U62(X)) → U62#(active(X))active#(U31(X)) → active#(X)
active#(U11(X)) → U11#(active(X))active#(U71(X1, X2, X3)) → active#(X1)
active#(take(X1, X2)) → active#(X2)active#(U61(X1, X2)) → active#(X1)
active#(U92(X1, X2, X3, X4)) → U92#(active(X1), X2, X3, X4)active#(length(X)) → active#(X)
active#(U62(X)) → active#(X)active#(U91(X1, X2, X3, X4)) → active#(X1)
active#(U81(X)) → active#(X)active#(isNatIList(cons(V1, V2))) → isNat#(V1)
active#(isNatList(take(V1, V2))) → U61#(isNat(V1), V2)active#(U41(X1, X2)) → active#(X1)
active#(U72(X1, X2)) → active#(X1)active#(cons(X1, X2)) → active#(X1)
active#(U91(tt, IL, M, N)) → U92#(isNat(M), IL, M, N)active#(U11(X)) → active#(X)
active#(U42(X)) → active#(X)active#(U21(X)) → active#(X)
active#(U93(tt, IL, M, N)) → take#(M, IL)active#(U41(tt, V2)) → U42#(isNatIList(V2))
active#(U92(tt, IL, M, N)) → isNat#(N)active#(U52(X)) → active#(X)
active#(U61(tt, V2)) → U62#(isNatIList(V2))active#(isNat(s(V1))) → isNat#(V1)
active#(U71(tt, L, N)) → isNat#(N)active#(U93(X1, X2, X3, X4)) → U93#(active(X1), X2, X3, X4)
active#(isNat(s(V1))) → U21#(isNat(V1))active#(U61(tt, V2)) → isNatIList#(V2)
active#(take(X1, X2)) → active#(X1)active#(s(X)) → s#(active(X))
active#(take(0, IL)) → U81#(isNatIList(IL))active#(U91(tt, IL, M, N)) → isNat#(M)
active#(take(X1, X2)) → take#(X1, active(X2))active#(s(X)) → active#(X)
active#(zeros) → cons#(0, zeros)active#(U93(tt, IL, M, N)) → cons#(N, take(M, IL))
active#(U92(X1, X2, X3, X4)) → active#(X1)active#(take(0, IL)) → isNatIList#(IL)

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

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

U81#(mark(X)) → U81#(X)U81#(ok(X)) → U81#(X)

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

U42#(mark(X)) → U42#(X)U42#(ok(X)) → U42#(X)

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

isNat#(ok(X)) → isNat#(X)

isNatList#(ok(X)) → isNatList#(X)

isNatIList#(ok(X)) → isNatIList#(X)

length#(mark(X)) → length#(X)length#(ok(X)) → length#(X)

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

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

U52#(mark(X)) → U52#(X)U52#(ok(X)) → U52#(X)

active#(U11(X)) → active#(X)active#(U31(X)) → active#(X)
active#(U42(X)) → active#(X)active#(U51(X1, X2)) → active#(X1)
active#(U71(X1, X2, X3)) → active#(X1)active#(take(X1, X2)) → active#(X2)
active#(U61(X1, X2)) → active#(X1)active#(take(X1, X2)) → active#(X1)
active#(length(X)) → active#(X)active#(U62(X)) → active#(X)
active#(U91(X1, X2, X3, X4)) → active#(X1)active#(U81(X)) → active#(X)
active#(U21(X)) → active#(X)active#(U93(X1, X2, X3, X4)) → active#(X1)
active#(U41(X1, X2)) → active#(X1)active#(s(X)) → active#(X)
active#(U52(X)) → active#(X)active#(U72(X1, X2)) → active#(X1)
active#(U92(X1, X2, X3, X4)) → active#(X1)active#(cons(X1, X2)) → active#(X1)

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

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

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

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 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U42#(mark(X)) → U42#(X)U42#(ok(X)) → U42#(X)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U42#(mark(X)) → U42#(X)U42#(ok(X)) → U42#(X)

Problem 5: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

isNat#(ok(X)) → isNat#(X)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNat#(ok(X)) → isNat#(X)

Problem 6: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

active#(U11(X)) → active#(X)active#(U42(X)) → active#(X)
active#(U31(X)) → active#(X)active#(U51(X1, X2)) → active#(X1)
active#(take(X1, X2)) → active#(X2)active#(U71(X1, X2, X3)) → active#(X1)
active#(U61(X1, X2)) → active#(X1)active#(length(X)) → active#(X)
active#(take(X1, X2)) → active#(X1)active#(U62(X)) → active#(X)
active#(U91(X1, X2, X3, X4)) → active#(X1)active#(U81(X)) → active#(X)
active#(U21(X)) → active#(X)active#(U93(X1, X2, X3, X4)) → active#(X1)
active#(U41(X1, X2)) → active#(X1)active#(s(X)) → active#(X)
active#(U52(X)) → active#(X)active#(U72(X1, X2)) → active#(X1)
active#(U92(X1, X2, X3, X4)) → active#(X1)active#(cons(X1, X2)) → active#(X1)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

active#(U11(X)) → active#(X)active#(U42(X)) → active#(X)
active#(U31(X)) → active#(X)active#(U51(X1, X2)) → active#(X1)
active#(take(X1, X2)) → active#(X2)active#(U71(X1, X2, X3)) → active#(X1)
active#(U61(X1, X2)) → active#(X1)active#(take(X1, X2)) → active#(X1)
active#(length(X)) → active#(X)active#(U62(X)) → active#(X)
active#(U91(X1, X2, X3, X4)) → active#(X1)active#(U81(X)) → active#(X)
active#(U21(X)) → active#(X)active#(U93(X1, X2, X3, X4)) → active#(X1)
active#(U41(X1, X2)) → active#(X1)active#(s(X)) → active#(X)
active#(U52(X)) → active#(X)active#(U72(X1, X2)) → active#(X1)
active#(U92(X1, X2, X3, X4)) → active#(X1)active#(cons(X1, X2)) → active#(X1)

Problem 7: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 8: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 9: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

isNatIList#(ok(X)) → isNatIList#(X)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNatIList#(ok(X)) → isNatIList#(X)

Problem 10: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

length#(mark(X)) → length#(X)length#(ok(X)) → length#(X)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

length#(mark(X)) → length#(X)length#(ok(X)) → length#(X)

Problem 11: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

isNatList#(ok(X)) → isNatList#(X)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNatList#(ok(X)) → isNatList#(X)

Problem 12: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 13: 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(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

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 15: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U81#(mark(X)) → U81#(X)U81#(ok(X)) → U81#(X)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U81#(mark(X)) → U81#(X)U81#(ok(X)) → U81#(X)

Problem 16: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

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 17: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U31#(ok(X)) → U31#(X)U31#(mark(X)) → U31#(X)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U31#(ok(X)) → U31#(X)U31#(mark(X)) → U31#(X)

Problem 18: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U11#(ok(X)) → U11#(X)U11#(mark(X)) → U11#(X)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U11#(ok(X)) → U11#(X)U11#(mark(X)) → U11#(X)

Problem 19: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 20: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U21#(ok(X)) → U21#(X)U21#(mark(X)) → U21#(X)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U21#(ok(X)) → U21#(X)U21#(mark(X)) → U21#(X)

Problem 21: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U71#(ok(X1), ok(X2), ok(X3)) → U71#(X1, X2, X3)U71#(mark(X1), X2, X3) → U71#(X1, X2, X3)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U71#(ok(X1), ok(X2), ok(X3)) → U71#(X1, X2, X3)U71#(mark(X1), X2, X3) → U71#(X1, X2, X3)

Problem 23: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 24: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 25: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

proper#(U41(X1, X2)) → proper#(X2)proper#(cons(X1, X2)) → proper#(X1)
proper#(U41(X1, X2)) → proper#(X1)proper#(U91(X1, X2, X3, X4)) → proper#(X2)
proper#(U93(X1, X2, X3, X4)) → proper#(X4)proper#(U11(X)) → proper#(X)
proper#(U51(X1, X2)) → proper#(X1)proper#(U42(X)) → proper#(X)
proper#(U92(X1, X2, X3, X4)) → proper#(X2)proper#(U93(X1, X2, X3, X4)) → proper#(X3)
proper#(U71(X1, X2, X3)) → proper#(X1)proper#(U62(X)) → proper#(X)
proper#(U93(X1, X2, X3, X4)) → proper#(X1)proper#(take(X1, X2)) → proper#(X1)
proper#(U61(X1, X2)) → proper#(X2)proper#(isNatList(X)) → proper#(X)
proper#(U51(X1, X2)) → proper#(X2)proper#(U21(X)) → proper#(X)
proper#(U92(X1, X2, X3, X4)) → proper#(X4)proper#(U93(X1, X2, X3, X4)) → proper#(X2)
proper#(U72(X1, X2)) → proper#(X2)proper#(isNat(X)) → proper#(X)
proper#(cons(X1, X2)) → proper#(X2)proper#(isNatIList(X)) → proper#(X)
proper#(U92(X1, X2, X3, X4)) → proper#(X1)proper#(U91(X1, X2, X3, X4)) → proper#(X3)
proper#(take(X1, X2)) → proper#(X2)proper#(U71(X1, X2, X3)) → proper#(X3)
proper#(U72(X1, X2)) → proper#(X1)proper#(U81(X)) → proper#(X)
proper#(U61(X1, X2)) → proper#(X1)proper#(U92(X1, X2, X3, X4)) → proper#(X3)
proper#(s(X)) → proper#(X)proper#(length(X)) → proper#(X)
proper#(U91(X1, X2, X3, X4)) → proper#(X4)proper#(U71(X1, X2, X3)) → proper#(X2)
proper#(U52(X)) → proper#(X)proper#(U91(X1, X2, X3, X4)) → proper#(X1)
proper#(U31(X)) → proper#(X)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

proper#(U41(X1, X2)) → proper#(X2)proper#(cons(X1, X2)) → proper#(X1)
proper#(U41(X1, X2)) → proper#(X1)proper#(U91(X1, X2, X3, X4)) → proper#(X2)
proper#(U93(X1, X2, X3, X4)) → proper#(X4)proper#(U11(X)) → proper#(X)
proper#(U92(X1, X2, X3, X4)) → proper#(X2)proper#(U51(X1, X2)) → proper#(X1)
proper#(U42(X)) → proper#(X)proper#(U93(X1, X2, X3, X4)) → proper#(X3)
proper#(U62(X)) → proper#(X)proper#(U71(X1, X2, X3)) → proper#(X1)
proper#(U93(X1, X2, X3, X4)) → proper#(X1)proper#(take(X1, X2)) → proper#(X1)
proper#(U61(X1, X2)) → proper#(X2)proper#(isNatList(X)) → proper#(X)
proper#(U51(X1, X2)) → proper#(X2)proper#(U92(X1, X2, X3, X4)) → proper#(X4)
proper#(U21(X)) → proper#(X)proper#(U93(X1, X2, X3, X4)) → proper#(X2)
proper#(U72(X1, X2)) → proper#(X2)proper#(isNat(X)) → proper#(X)
proper#(cons(X1, X2)) → proper#(X2)proper#(isNatIList(X)) → proper#(X)
proper#(U92(X1, X2, X3, X4)) → proper#(X1)proper#(U91(X1, X2, X3, X4)) → proper#(X3)
proper#(take(X1, X2)) → proper#(X2)proper#(U71(X1, X2, X3)) → proper#(X3)
proper#(U72(X1, X2)) → proper#(X1)proper#(U81(X)) → proper#(X)
proper#(U61(X1, X2)) → proper#(X1)proper#(U92(X1, X2, X3, X4)) → proper#(X3)
proper#(s(X)) → proper#(X)proper#(length(X)) → proper#(X)
proper#(U91(X1, X2, X3, X4)) → proper#(X4)proper#(U71(X1, X2, X3)) → proper#(X2)
proper#(U91(X1, X2, X3, X4)) → proper#(X1)proper#(U52(X)) → proper#(X)
proper#(U31(X)) → proper#(X)

Problem 26: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 27: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U62#(mark(X)) → U62#(X)U62#(ok(X)) → U62#(X)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U62#(mark(X)) → U62#(X)U62#(ok(X)) → U62#(X)

Problem 28: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U52#(mark(X)) → U52#(X)U52#(ok(X)) → U52#(X)

Rewrite Rules

active(zeros) → mark(cons(0, zeros))active(U11(tt)) → mark(tt)
active(U21(tt)) → mark(tt)active(U31(tt)) → mark(tt)
active(U41(tt, V2)) → mark(U42(isNatIList(V2)))active(U42(tt)) → mark(tt)
active(U51(tt, V2)) → mark(U52(isNatList(V2)))active(U52(tt)) → mark(tt)
active(U61(tt, V2)) → mark(U62(isNatIList(V2)))active(U62(tt)) → mark(tt)
active(U71(tt, L, N)) → mark(U72(isNat(N), L))active(U72(tt, L)) → mark(s(length(L)))
active(U81(tt)) → mark(nil)active(U91(tt, IL, M, N)) → mark(U92(isNat(M), IL, M, N))
active(U92(tt, IL, M, N)) → mark(U93(isNat(N), IL, M, N))active(U93(tt, IL, M, N)) → mark(cons(N, take(M, IL)))
active(isNat(0)) → mark(tt)active(isNat(length(V1))) → mark(U11(isNatList(V1)))
active(isNat(s(V1))) → mark(U21(isNat(V1)))active(isNatIList(V)) → mark(U31(isNatList(V)))
active(isNatIList(zeros)) → mark(tt)active(isNatIList(cons(V1, V2))) → mark(U41(isNat(V1), V2))
active(isNatList(nil)) → mark(tt)active(isNatList(cons(V1, V2))) → mark(U51(isNat(V1), V2))
active(isNatList(take(V1, V2))) → mark(U61(isNat(V1), V2))active(length(nil)) → mark(0)
active(length(cons(N, L))) → mark(U71(isNatList(L), L, N))active(take(0, IL)) → mark(U81(isNatIList(IL)))
active(take(s(M), cons(N, IL))) → mark(U91(isNatIList(IL), IL, M, N))active(cons(X1, X2)) → cons(active(X1), X2)
active(U11(X)) → U11(active(X))active(U21(X)) → U21(active(X))
active(U31(X)) → U31(active(X))active(U41(X1, X2)) → U41(active(X1), X2)
active(U42(X)) → U42(active(X))active(U51(X1, X2)) → U51(active(X1), X2)
active(U52(X)) → U52(active(X))active(U61(X1, X2)) → U61(active(X1), X2)
active(U62(X)) → U62(active(X))active(U71(X1, X2, X3)) → U71(active(X1), X2, X3)
active(U72(X1, X2)) → U72(active(X1), X2)active(s(X)) → s(active(X))
active(length(X)) → length(active(X))active(U81(X)) → U81(active(X))
active(U91(X1, X2, X3, X4)) → U91(active(X1), X2, X3, X4)active(U92(X1, X2, X3, X4)) → U92(active(X1), X2, X3, X4)
active(U93(X1, X2, X3, X4)) → U93(active(X1), X2, X3, X4)active(take(X1, X2)) → take(active(X1), X2)
active(take(X1, X2)) → take(X1, active(X2))cons(mark(X1), X2) → mark(cons(X1, X2))
U11(mark(X)) → mark(U11(X))U21(mark(X)) → mark(U21(X))
U31(mark(X)) → mark(U31(X))U41(mark(X1), X2) → mark(U41(X1, X2))
U42(mark(X)) → mark(U42(X))U51(mark(X1), X2) → mark(U51(X1, X2))
U52(mark(X)) → mark(U52(X))U61(mark(X1), X2) → mark(U61(X1, X2))
U62(mark(X)) → mark(U62(X))U71(mark(X1), X2, X3) → mark(U71(X1, X2, X3))
U72(mark(X1), X2) → mark(U72(X1, X2))s(mark(X)) → mark(s(X))
length(mark(X)) → mark(length(X))U81(mark(X)) → mark(U81(X))
U91(mark(X1), X2, X3, X4) → mark(U91(X1, X2, X3, X4))U92(mark(X1), X2, X3, X4) → mark(U92(X1, X2, X3, X4))
U93(mark(X1), X2, X3, X4) → mark(U93(X1, X2, X3, X4))take(mark(X1), X2) → mark(take(X1, X2))
take(X1, mark(X2)) → mark(take(X1, X2))proper(zeros) → ok(zeros)
proper(cons(X1, X2)) → cons(proper(X1), proper(X2))proper(0) → ok(0)
proper(U11(X)) → U11(proper(X))proper(tt) → ok(tt)
proper(U21(X)) → U21(proper(X))proper(U31(X)) → U31(proper(X))
proper(U41(X1, X2)) → U41(proper(X1), proper(X2))proper(U42(X)) → U42(proper(X))
proper(isNatIList(X)) → isNatIList(proper(X))proper(U51(X1, X2)) → U51(proper(X1), proper(X2))
proper(U52(X)) → U52(proper(X))proper(isNatList(X)) → isNatList(proper(X))
proper(U61(X1, X2)) → U61(proper(X1), proper(X2))proper(U62(X)) → U62(proper(X))
proper(U71(X1, X2, X3)) → U71(proper(X1), proper(X2), proper(X3))proper(U72(X1, X2)) → U72(proper(X1), proper(X2))
proper(isNat(X)) → isNat(proper(X))proper(s(X)) → s(proper(X))
proper(length(X)) → length(proper(X))proper(U81(X)) → U81(proper(X))
proper(nil) → ok(nil)proper(U91(X1, X2, X3, X4)) → U91(proper(X1), proper(X2), proper(X3), proper(X4))
proper(U92(X1, X2, X3, X4)) → U92(proper(X1), proper(X2), proper(X3), proper(X4))proper(U93(X1, X2, X3, X4)) → U93(proper(X1), proper(X2), proper(X3), proper(X4))
proper(take(X1, X2)) → take(proper(X1), proper(X2))cons(ok(X1), ok(X2)) → ok(cons(X1, X2))
U11(ok(X)) → ok(U11(X))U21(ok(X)) → ok(U21(X))
U31(ok(X)) → ok(U31(X))U41(ok(X1), ok(X2)) → ok(U41(X1, X2))
U42(ok(X)) → ok(U42(X))isNatIList(ok(X)) → ok(isNatIList(X))
U51(ok(X1), ok(X2)) → ok(U51(X1, X2))U52(ok(X)) → ok(U52(X))
isNatList(ok(X)) → ok(isNatList(X))U61(ok(X1), ok(X2)) → ok(U61(X1, X2))
U62(ok(X)) → ok(U62(X))U71(ok(X1), ok(X2), ok(X3)) → ok(U71(X1, X2, X3))
U72(ok(X1), ok(X2)) → ok(U72(X1, X2))isNat(ok(X)) → ok(isNat(X))
s(ok(X)) → ok(s(X))length(ok(X)) → ok(length(X))
U81(ok(X)) → ok(U81(X))U91(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U91(X1, X2, X3, X4))
U92(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U92(X1, X2, X3, X4))U93(ok(X1), ok(X2), ok(X3), ok(X4)) → ok(U93(X1, X2, X3, X4))
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: isNat, U62, U61, U42, U93, U92, U41, U91, length, ok, proper, U21, top, cons, isNatIList, mark, U71, U72, 0, isNatList, U51, s, tt, zeros, take, U81, U52, active, U11, U31, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U52#(mark(X)) → U52#(X)U52#(ok(X)) → U52#(X)