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 (49735ms).
 | – Problem 2 was processed with processor SubtermCriterion (46ms).
 | – Problem 3 was processed with processor SubtermCriterion (2ms).
 | – Problem 4 was processed with processor SubtermCriterion (12ms).
 | – Problem 5 was processed with processor SubtermCriterion (2ms).
 | – Problem 6 was processed with processor SubtermCriterion (3ms).
 | – Problem 7 was processed with processor SubtermCriterion (3ms).
 | – Problem 8 was processed with processor DependencyGraph (4628ms).
 |    | – Problem 30 remains open; application of the following processors failed [].
 | – Problem 9 was processed with processor SubtermCriterion (4ms).
 | – Problem 10 was processed with processor SubtermCriterion (2ms).
 | – Problem 11 was processed with processor SubtermCriterion (2ms).
 | – Problem 12 was processed with processor SubtermCriterion (4ms).
 | – Problem 13 was processed with processor SubtermCriterion (2ms).
 | – Problem 14 remains open; application of the following processors failed [SubtermCriterion (3ms), DependencyGraph (9ms), PolynomialLinearRange4iUR (timeout)].
 | – Problem 15 was processed with processor SubtermCriterion (2ms).
 | – Problem 16 was processed with processor SubtermCriterion (4ms).
 | – Problem 17 was processed with processor SubtermCriterion (3ms).
 | – Problem 18 was processed with processor DependencyGraph (4529ms).
 |    | – Problem 29 was processed with processor PolynomialLinearRange4iUR (220ms).
 |    |    | – Problem 31 remains open; application of the following processors failed [].
 | – Problem 19 was processed with processor SubtermCriterion (2ms).
 | – Problem 20 was processed with processor SubtermCriterion (4ms).
 | – Problem 21 was processed with processor SubtermCriterion (2ms).
 | – Problem 22 was processed with processor SubtermCriterion (3ms).
 | – Problem 23 was processed with processor SubtermCriterion (2ms).
 | – Problem 24 was processed with processor SubtermCriterion (2ms).
 | – Problem 25 was processed with processor SubtermCriterion (4ms).
 | – Problem 26 was processed with processor SubtermCriterion (2ms).
 | – Problem 27 was processed with processor SubtermCriterion (6ms).
 | – Problem 28 was processed with processor SubtermCriterion (4ms).

The following open problems remain:



Open Dependency Pair Problem 29

Dependency Pairs

active#(U51(X1, X2, X3))active#(X1)active#(U32(X))active#(X)
active#(U61(X1, X2))active#(X1)active#(U42(X1, X2))active#(X1)
active#(U12(X))active#(X)active#(length(X))active#(X)
active#(U43(X))active#(X)active#(U52(X1, X2))active#(X1)
active#(U41(X1, X2, X3))active#(X1)active#(U21(X1, X2))active#(X1)
active#(U53(X))active#(X)active#(U22(X))active#(X)
active#(s(X))active#(X)active#(U31(X1, X2))active#(X1)
active#(and(X1, X2))active#(X1)active#(U11(X1, X2))active#(X1)
active#(cons(X1, X2))active#(X1)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U43, U61, U42, U41, length, ok, proper, U21, top, U22, cons, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, U11, active, U12, U31, U32, nil




Open Dependency Pair Problem 14

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, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U43, U61, U42, U41, length, ok, proper, U21, top, U22, cons, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, U11, active, U12, U31, U32, nil




Open Dependency Pair Problem 30

Dependency Pairs

active#(U51(X1, X2, X3))active#(X1)active#(U32(X))active#(X)
active#(U61(X1, X2))active#(X1)active#(U42(X1, X2))active#(X1)
active#(U12(X))active#(X)active#(length(X))active#(X)
active#(U43(X))active#(X)active#(U52(X1, X2))active#(X1)
active#(U41(X1, X2, X3))active#(X1)active#(U21(X1, X2))active#(X1)
active#(U53(X))active#(X)active#(U22(X))active#(X)
active#(s(X))active#(X)active#(U31(X1, X2))active#(X1)
active#(and(X1, X2))active#(X1)active#(U11(X1, X2))active#(X1)
active#(cons(X1, X2))active#(X1)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U43, U61, U42, U41, length, ok, proper, U21, top, U22, cons, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, U11, active, U12, U31, U32, nil


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

proper#(cons(X1, X2))proper#(X1)proper#(length(X))length#(proper(X))
proper#(U11(X1, X2))proper#(X1)active#(isNatIList(V))isNatIListKind#(V)
active#(U52(tt, V2))isNatList#(V2)active#(U12(X))active#(X)
U11#(mark(X1), X2)U11#(X1, X2)proper#(U41(X1, X2, X3))proper#(X2)
proper#(isNatKind(X))proper#(X)proper#(U11(X1, X2))proper#(X2)
active#(isNatIListKind(cons(V1, V2)))isNatKind#(V1)U43#(ok(X))U43#(X)
top#(mark(X))proper#(X)length#(mark(X))length#(X)
isNatKind#(ok(X))isNatKind#(X)active#(U51(tt, V1, V2))U52#(isNat(V1), V2)
active#(U32(X))active#(X)active#(U43(X))U43#(active(X))
active#(U61(X1, X2))active#(X1)active#(U52(tt, V2))U53#(isNatList(V2))
active#(U61(tt, L))length#(L)active#(length(X))active#(X)
proper#(U12(X))U12#(proper(X))isNat#(ok(X))isNat#(X)
and#(mark(X1), X2)and#(X1, X2)active#(U21(tt, V1))isNat#(V1)
U42#(mark(X1), X2)U42#(X1, X2)isNatIList#(ok(X))isNatIList#(X)
active#(U41(X1, X2, X3))active#(X1)active#(U42(X1, X2))U42#(active(X1), X2)
active#(isNat(s(V1)))isNatKind#(V1)active#(isNatKind(length(V1)))isNatIListKind#(V1)
active#(isNatList(cons(V1, V2)))isNatIListKind#(V2)proper#(U51(X1, X2, X3))proper#(X1)
U53#(mark(X))U53#(X)proper#(U32(X))U32#(proper(X))
active#(U31(tt, V))U32#(isNatList(V))proper#(U22(X))proper#(X)
active#(U53(X))U53#(active(X))active#(isNatList(cons(V1, V2)))U51#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
proper#(U51(X1, X2, X3))proper#(X2)proper#(U52(X1, X2))proper#(X1)
proper#(isNatKind(X))isNatKind#(proper(X))U51#(ok(X1), ok(X2), ok(X3))U51#(X1, X2, X3)
proper#(isNatIListKind(X))proper#(X)cons#(mark(X1), X2)cons#(X1, X2)
active#(U52(X1, X2))U52#(active(X1), X2)active#(U41(X1, X2, X3))U41#(active(X1), X2, X3)
U32#(mark(X))U32#(X)top#(ok(X))active#(X)
proper#(U42(X1, X2))proper#(X1)active#(isNatList(cons(V1, V2)))and#(isNatKind(V1), isNatIListKind(V2))
active#(U52(X1, X2))active#(X1)active#(U53(X))active#(X)
active#(and(X1, X2))and#(active(X1), X2)U52#(ok(X1), ok(X2))U52#(X1, X2)
proper#(U41(X1, X2, X3))proper#(X1)active#(isNatIListKind(cons(V1, V2)))and#(isNatKind(V1), isNatIListKind(V2))
active#(length(cons(N, L)))U61#(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)proper#(isNatList(X))proper#(X)
active#(U31(X1, X2))active#(X1)proper#(isNat(X))isNat#(proper(X))
active#(U41(tt, V1, V2))U42#(isNat(V1), V2)U41#(ok(X1), ok(X2), ok(X3))U41#(X1, X2, X3)
active#(isNatIList(cons(V1, V2)))isNatIListKind#(V2)active#(isNat(length(V1)))isNatIListKind#(V1)
active#(U21(X1, X2))U21#(active(X1), X2)U51#(mark(X1), X2, X3)U51#(X1, X2, X3)
proper#(isNat(X))proper#(X)proper#(U12(X))proper#(X)
active#(length(cons(N, L)))and#(isNatList(L), isNatIListKind(L))proper#(U22(X))U22#(proper(X))
proper#(U42(X1, X2))U42#(proper(X1), proper(X2))active#(U11(X1, X2))U11#(active(X1), X2)
active#(s(X))s#(active(X))s#(ok(X))s#(X)
proper#(length(X))proper#(X)active#(isNat(s(V1)))U21#(isNatKind(V1), V1)
active#(U51(X1, X2, X3))U51#(active(X1), X2, X3)proper#(s(X))s#(proper(X))
active#(zeros)cons#(0, zeros)proper#(U31(X1, X2))U31#(proper(X1), proper(X2))
proper#(U21(X1, X2))proper#(X1)U31#(ok(X1), ok(X2))U31#(X1, X2)
active#(U11(tt, V1))isNatList#(V1)U52#(mark(X1), X2)U52#(X1, X2)
top#(ok(X))top#(active(X))proper#(U42(X1, X2))proper#(X2)
active#(U51(tt, V1, V2))isNat#(V1)proper#(U31(X1, X2))proper#(X1)
U32#(ok(X))U32#(X)U11#(ok(X1), ok(X2))U11#(X1, X2)
isNatIListKind#(ok(X))isNatIListKind#(X)cons#(ok(X1), ok(X2))cons#(X1, X2)
proper#(isNatIList(X))isNatIList#(proper(X))active#(U42(tt, V2))isNatIList#(V2)
proper#(U11(X1, X2))U11#(proper(X1), proper(X2))proper#(U52(X1, X2))U52#(proper(X1), proper(X2))
proper#(and(X1, X2))and#(proper(X1), proper(X2))U12#(mark(X))U12#(X)
active#(cons(X1, X2))cons#(active(X1), X2)active#(U42(tt, V2))U43#(isNatIList(V2))
active#(U61(X1, X2))U61#(active(X1), X2)proper#(and(X1, X2))proper#(X2)
proper#(U61(X1, X2))proper#(X2)U61#(mark(X1), X2)U61#(X1, X2)
active#(U11(tt, V1))U12#(isNatList(V1))U22#(mark(X))U22#(X)
length#(ok(X))length#(X)active#(U61(tt, L))s#(length(L))
active#(U11(X1, X2))active#(X1)proper#(U41(X1, X2, X3))U41#(proper(X1), proper(X2), proper(X3))
proper#(U43(X))proper#(X)U61#(ok(X1), ok(X2))U61#(X1, X2)
active#(U51(X1, X2, X3))active#(X1)top#(mark(X))top#(proper(X))
proper#(cons(X1, X2))proper#(X2)proper#(isNatIList(X))proper#(X)
active#(isNatIListKind(cons(V1, V2)))isNatIListKind#(V2)active#(length(cons(N, L)))and#(isNat(N), isNatKind(N))
U22#(ok(X))U22#(X)active#(isNatIList(cons(V1, V2)))and#(isNatKind(V1), isNatIListKind(V2))
isNatList#(ok(X))isNatList#(X)active#(U21(tt, V1))U22#(isNat(V1))
active#(U31(tt, V))isNatList#(V)proper#(s(X))proper#(X)
active#(length(cons(N, L)))isNatIListKind#(L)proper#(isNatList(X))isNatList#(proper(X))
active#(isNat(length(V1)))U11#(isNatIListKind(V1), V1)proper#(U43(X))U43#(proper(X))
proper#(U51(X1, X2, X3))U51#(proper(X1), proper(X2), proper(X3))proper#(U61(X1, X2))U61#(proper(X1), proper(X2))
active#(cons(X1, X2))active#(X1)proper#(U53(X))U53#(proper(X))
active#(length(cons(N, L)))isNatKind#(N)proper#(U41(X1, X2, X3))proper#(X3)
active#(U42(X1, X2))active#(X1)proper#(U31(X1, X2))proper#(X2)
and#(ok(X1), ok(X2))and#(X1, X2)active#(U43(X))active#(X)
proper#(and(X1, X2))proper#(X1)active#(length(cons(N, L)))and#(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N)))
U53#(ok(X))U53#(X)active#(length(cons(N, L)))isNatList#(L)
active#(U41(tt, V1, V2))isNat#(V1)proper#(U21(X1, X2))proper#(X2)
proper#(U32(X))proper#(X)active#(U31(X1, X2))U31#(active(X1), X2)
active#(U12(X))U12#(active(X))active#(length(cons(N, L)))isNat#(N)
U41#(mark(X1), X2, X3)U41#(X1, X2, X3)active#(U22(X))U22#(active(X))
proper#(isNatIListKind(X))isNatIListKind#(proper(X))proper#(U51(X1, X2, X3))proper#(X3)
active#(isNatKind(s(V1)))isNatKind#(V1)proper#(U21(X1, X2))U21#(proper(X1), proper(X2))
proper#(U53(X))proper#(X)U43#(mark(X))U43#(X)
active#(length(X))length#(active(X))active#(U32(X))U32#(active(X))
U42#(ok(X1), ok(X2))U42#(X1, X2)active#(isNatIList(cons(V1, V2)))isNatKind#(V1)
U31#(mark(X1), X2)U31#(X1, X2)proper#(U61(X1, X2))proper#(X1)
s#(mark(X))s#(X)proper#(U52(X1, X2))proper#(X2)
active#(U21(X1, X2))active#(X1)active#(isNatIList(cons(V1, V2)))U41#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
proper#(cons(X1, X2))cons#(proper(X1), proper(X2))active#(U22(X))active#(X)
U12#(ok(X))U12#(X)U21#(mark(X1), X2)U21#(X1, X2)
active#(s(X))active#(X)active#(isNatList(cons(V1, V2)))isNatKind#(V1)
active#(and(X1, X2))active#(X1)active#(isNatIList(V))U31#(isNatIListKind(V), V)
U21#(ok(X1), ok(X2))U21#(X1, X2)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


The following SCCs where found

active#(U52(tt, V2)) → isNatList#(V2)active#(isNatIList(V)) → isNatIListKind#(V)
active#(U12(X)) → active#(X)active#(U61(X1, X2)) → U61#(active(X1), X2)
active#(isNatIListKind(cons(V1, V2))) → isNatKind#(V1)active#(U11(tt, V1)) → U12#(isNatList(V1))
active#(U11(X1, X2)) → active#(X1)active#(U61(tt, L)) → s#(length(L))
active#(U51(X1, X2, X3)) → active#(X1)active#(U51(tt, V1, V2)) → U52#(isNat(V1), V2)
active#(U32(X)) → active#(X)active#(U61(X1, X2)) → active#(X1)
active#(length(cons(N, L))) → and#(isNat(N), isNatKind(N))active#(length(X)) → active#(X)
active#(U52(tt, V2)) → U53#(isNatList(V2))active#(U21(tt, V1)) → isNat#(V1)
active#(U41(X1, X2, X3)) → active#(X1)active#(U31(tt, V)) → isNatList#(V)
active#(isNatList(cons(V1, V2))) → isNatIListKind#(V2)active#(length(cons(N, L))) → isNatIListKind#(L)
active#(isNat(length(V1))) → U11#(isNatIListKind(V1), V1)active#(U31(tt, V)) → U32#(isNatList(V))
active#(isNatList(cons(V1, V2))) → U51#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)active#(cons(X1, X2)) → active#(X1)
active#(length(cons(N, L))) → isNatKind#(N)active#(U42(X1, X2)) → active#(X1)
active#(U52(X1, X2)) → U52#(active(X1), X2)active#(U41(X1, X2, X3)) → U41#(active(X1), X2, X3)
active#(U43(X)) → active#(X)active#(isNatList(cons(V1, V2))) → and#(isNatKind(V1), isNatIListKind(V2))
active#(U52(X1, X2)) → active#(X1)active#(U41(tt, V1, V2)) → isNat#(V1)
active#(U53(X)) → active#(X)active#(and(X1, X2)) → and#(active(X1), X2)
active#(U12(X)) → U12#(active(X))active#(U31(X1, X2)) → U31#(active(X1), X2)
active#(length(cons(N, L))) → isNat#(N)active#(length(cons(N, L))) → U61#(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
active#(U31(X1, X2)) → active#(X1)active#(length(X)) → length#(active(X))
active#(U32(X)) → U32#(active(X))active#(length(cons(N, L))) → and#(isNatList(L), isNatIListKind(L))
active#(isNatIList(cons(V1, V2))) → isNatKind#(V1)active#(U11(X1, X2)) → U11#(active(X1), X2)
active#(isNatIList(cons(V1, V2))) → U41#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)active#(U21(X1, X2)) → active#(X1)
active#(U22(X)) → active#(X)active#(U51(X1, X2, X3)) → U51#(active(X1), X2, X3)
active#(isNat(s(V1))) → U21#(isNatKind(V1), V1)active#(s(X)) → active#(X)
active#(zeros) → cons#(0, zeros)active#(isNatList(cons(V1, V2))) → isNatKind#(V1)
active#(isNatIList(V)) → U31#(isNatIListKind(V), V)active#(and(X1, X2)) → active#(X1)

isNatIListKind#(ok(X)) → isNatIListKind#(X)

U32#(ok(X)) → U32#(X)U32#(mark(X)) → U32#(X)

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

active#(U51(X1, X2, X3)) → active#(X1)active#(U32(X)) → active#(X)
active#(U42(X1, X2)) → active#(X1)active#(U12(X)) → active#(X)
active#(U61(X1, X2)) → active#(X1)active#(length(X)) → active#(X)
active#(U43(X)) → active#(X)active#(U52(X1, X2)) → active#(X1)
active#(U41(X1, X2, X3)) → active#(X1)active#(U53(X)) → active#(X)
active#(U21(X1, X2)) → active#(X1)active#(U22(X)) → active#(X)
active#(s(X)) → active#(X)active#(U31(X1, X2)) → active#(X1)
active#(and(X1, X2)) → active#(X1)active#(U11(X1, X2)) → active#(X1)
active#(cons(X1, X2)) → active#(X1)

proper#(U52(X1, X2)) → proper#(X1)proper#(U51(X1, X2, X3)) → proper#(X2)
proper#(cons(X1, X2)) → proper#(X1)proper#(U11(X1, X2)) → proper#(X1)
proper#(isNatIListKind(X)) → proper#(X)proper#(U42(X1, X2)) → proper#(X2)
proper#(U41(X1, X2, X3)) → proper#(X3)proper#(U31(X1, X2)) → proper#(X1)
proper#(U31(X1, X2)) → proper#(X2)proper#(and(X1, X2)) → proper#(X1)
proper#(U41(X1, X2, X3)) → proper#(X2)proper#(U42(X1, X2)) → proper#(X1)
proper#(U21(X1, X2)) → proper#(X2)proper#(U32(X)) → proper#(X)
proper#(isNatKind(X)) → proper#(X)proper#(U11(X1, X2)) → proper#(X2)
proper#(and(X1, X2)) → proper#(X2)proper#(U61(X1, X2)) → proper#(X2)
proper#(U41(X1, X2, X3)) → proper#(X1)proper#(isNatList(X)) → proper#(X)
proper#(U51(X1, X2, X3)) → proper#(X3)proper#(U53(X)) → proper#(X)
proper#(U43(X)) → proper#(X)proper#(isNat(X)) → proper#(X)
proper#(cons(X1, X2)) → proper#(X2)proper#(U12(X)) → proper#(X)
proper#(isNatIList(X)) → proper#(X)proper#(U61(X1, X2)) → proper#(X1)
proper#(U52(X1, X2)) → proper#(X2)proper#(length(X)) → proper#(X)
proper#(s(X)) → proper#(X)proper#(U51(X1, X2, X3)) → proper#(X1)
proper#(U21(X1, X2)) → proper#(X1)proper#(U22(X)) → proper#(X)

U43#(mark(X)) → U43#(X)U43#(ok(X)) → U43#(X)

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

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

active#(U52(tt, V2)) → isNatList#(V2)active#(isNatIList(V)) → isNatIListKind#(V)
active#(U12(X)) → active#(X)active#(cons(X1, X2)) → cons#(active(X1), X2)
active#(U61(X1, X2)) → U61#(active(X1), X2)active#(isNatIListKind(cons(V1, V2))) → isNatKind#(V1)
active#(U11(tt, V1)) → U12#(isNatList(V1))active#(U11(X1, X2)) → active#(X1)
active#(U61(tt, L)) → s#(length(L))active#(U51(X1, X2, X3)) → active#(X1)
active#(U51(tt, V1, V2)) → U52#(isNat(V1), V2)active#(U32(X)) → active#(X)
active#(U61(X1, X2)) → active#(X1)active#(length(cons(N, L))) → and#(isNat(N), isNatKind(N))
active#(length(X)) → active#(X)active#(U52(tt, V2)) → U53#(isNatList(V2))
active#(U21(tt, V1)) → isNat#(V1)active#(U41(X1, X2, X3)) → active#(X1)
active#(U31(tt, V)) → isNatList#(V)active#(isNatList(cons(V1, V2))) → isNatIListKind#(V2)
active#(length(cons(N, L))) → isNatIListKind#(L)active#(isNat(length(V1))) → U11#(isNatIListKind(V1), V1)
active#(U31(tt, V)) → U32#(isNatList(V))active#(isNatList(cons(V1, V2))) → U51#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
active#(cons(X1, X2)) → active#(X1)active#(length(cons(N, L))) → isNatKind#(N)
active#(U42(X1, X2)) → active#(X1)active#(U52(X1, X2)) → U52#(active(X1), X2)
active#(U41(X1, X2, X3)) → U41#(active(X1), X2, X3)active#(U43(X)) → active#(X)
active#(isNatList(cons(V1, V2))) → and#(isNatKind(V1), isNatIListKind(V2))active#(U52(X1, X2)) → active#(X1)
active#(U41(tt, V1, V2)) → isNat#(V1)active#(U53(X)) → active#(X)
active#(and(X1, X2)) → and#(active(X1), X2)active#(U12(X)) → U12#(active(X))
active#(U31(X1, X2)) → U31#(active(X1), X2)active#(length(cons(N, L))) → isNat#(N)
active#(length(cons(N, L))) → U61#(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)active#(U31(X1, X2)) → active#(X1)
active#(length(X)) → length#(active(X))active#(U32(X)) → U32#(active(X))
active#(length(cons(N, L))) → and#(isNatList(L), isNatIListKind(L))active#(isNatIList(cons(V1, V2))) → isNatKind#(V1)
active#(U11(X1, X2)) → U11#(active(X1), X2)active#(isNatIList(cons(V1, V2))) → U41#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
active#(U21(X1, X2)) → active#(X1)active#(U22(X)) → active#(X)
active#(U51(X1, X2, X3)) → U51#(active(X1), X2, X3)active#(isNat(s(V1))) → U21#(isNatKind(V1), V1)
active#(s(X)) → active#(X)active#(zeros) → cons#(0, zeros)
active#(isNatList(cons(V1, V2))) → isNatKind#(V1)active#(isNatIList(V)) → U31#(isNatIListKind(V), V)
active#(and(X1, X2)) → active#(X1)

U22#(ok(X)) → U22#(X)U22#(mark(X)) → U22#(X)

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

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

isNatKind#(ok(X)) → isNatKind#(X)

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)

U12#(ok(X)) → U12#(X)U12#(mark(X)) → U12#(X)

U53#(mark(X)) → U53#(X)U53#(ok(X)) → U53#(X)

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

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

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

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

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

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

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 4: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U43#(mark(X))U43#(X)U43#(ok(X))U43#(X)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U43#(mark(X))U43#(X)U43#(ok(X))U43#(X)

Problem 5: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U32#(ok(X))U32#(X)U32#(mark(X))U32#(X)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U32#(ok(X))U32#(X)U32#(mark(X))U32#(X)

Problem 6: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 7: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 8: DependencyGraph



Dependency Pair Problem

Dependency Pairs

active#(isNatIList(V))isNatIListKind#(V)active#(U52(tt, V2))isNatList#(V2)
active#(U12(X))active#(X)active#(U61(X1, X2))U61#(active(X1), X2)
active#(isNatIListKind(cons(V1, V2)))isNatKind#(V1)active#(U11(tt, V1))U12#(isNatList(V1))
active#(U61(tt, L))s#(length(L))active#(U11(X1, X2))active#(X1)
active#(U51(X1, X2, X3))active#(X1)active#(U51(tt, V1, V2))U52#(isNat(V1), V2)
active#(U32(X))active#(X)active#(U61(X1, X2))active#(X1)
active#(length(cons(N, L)))and#(isNat(N), isNatKind(N))active#(length(X))active#(X)
active#(U52(tt, V2))U53#(isNatList(V2))active#(U21(tt, V1))isNat#(V1)
active#(U41(X1, X2, X3))active#(X1)active#(U31(tt, V))isNatList#(V)
active#(isNatList(cons(V1, V2)))isNatIListKind#(V2)active#(length(cons(N, L)))isNatIListKind#(L)
active#(isNat(length(V1)))U11#(isNatIListKind(V1), V1)active#(U31(tt, V))U32#(isNatList(V))
active#(isNatList(cons(V1, V2)))U51#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)active#(cons(X1, X2))active#(X1)
active#(length(cons(N, L)))isNatKind#(N)active#(U42(X1, X2))active#(X1)
active#(U41(X1, X2, X3))U41#(active(X1), X2, X3)active#(U52(X1, X2))U52#(active(X1), X2)
active#(U43(X))active#(X)active#(U52(X1, X2))active#(X1)
active#(isNatList(cons(V1, V2)))and#(isNatKind(V1), isNatIListKind(V2))active#(U41(tt, V1, V2))isNat#(V1)
active#(and(X1, X2))and#(active(X1), X2)active#(U53(X))active#(X)
active#(U31(X1, X2))U31#(active(X1), X2)active#(U12(X))U12#(active(X))
active#(length(cons(N, L)))isNat#(N)active#(length(cons(N, L)))U61#(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)
active#(U31(X1, X2))active#(X1)active#(length(X))length#(active(X))
active#(U32(X))U32#(active(X))active#(length(cons(N, L)))and#(isNatList(L), isNatIListKind(L))
active#(isNatIList(cons(V1, V2)))isNatKind#(V1)active#(U11(X1, X2))U11#(active(X1), X2)
active#(U21(X1, X2))active#(X1)active#(isNatIList(cons(V1, V2)))U41#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
active#(isNat(s(V1)))U21#(isNatKind(V1), V1)active#(U51(X1, X2, X3))U51#(active(X1), X2, X3)
active#(U22(X))active#(X)active#(s(X))active#(X)
active#(zeros)cons#(0, zeros)active#(isNatList(cons(V1, V2)))isNatKind#(V1)
active#(isNatIList(V))U31#(isNatIListKind(V), V)active#(and(X1, X2))active#(X1)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


The following SCCs where found

active#(U51(X1, X2, X3)) → active#(X1)active#(U32(X)) → active#(X)
active#(U12(X)) → active#(X)active#(U42(X1, X2)) → active#(X1)
active#(U61(X1, X2)) → active#(X1)active#(length(X)) → active#(X)
active#(U43(X)) → active#(X)active#(U52(X1, X2)) → active#(X1)
active#(U41(X1, X2, X3)) → active#(X1)active#(U53(X)) → active#(X)
active#(U21(X1, X2)) → active#(X1)active#(U22(X)) → active#(X)
active#(s(X)) → active#(X)active#(U31(X1, X2)) → active#(X1)
active#(and(X1, X2)) → active#(X1)active#(U11(X1, X2)) → active#(X1)
active#(cons(X1, X2)) → active#(X1)

Problem 9: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U53#(mark(X))U53#(X)U53#(ok(X))U53#(X)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U53#(mark(X))U53#(X)U53#(ok(X))U53#(X)

Problem 10: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U12#(ok(X))U12#(X)U12#(mark(X))U12#(X)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U12#(ok(X))U12#(X)U12#(mark(X))U12#(X)

Problem 11: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

isNatIListKind#(ok(X))isNatIListKind#(X)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNatIListKind#(ok(X))isNatIListKind#(X)

Problem 12: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

isNatKind#(ok(X))isNatKind#(X)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

isNatKind#(ok(X))isNatKind#(X)

Problem 13: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 15: 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, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, 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 16: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 17: 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, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, 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 18: DependencyGraph



Dependency Pair Problem

Dependency Pairs

active#(isNatIList(V))isNatIListKind#(V)active#(U52(tt, V2))isNatList#(V2)
active#(U12(X))active#(X)active#(cons(X1, X2))cons#(active(X1), X2)
active#(U61(X1, X2))U61#(active(X1), X2)active#(isNatIListKind(cons(V1, V2)))isNatKind#(V1)
active#(U11(tt, V1))U12#(isNatList(V1))active#(U61(tt, L))s#(length(L))
active#(U11(X1, X2))active#(X1)active#(U51(X1, X2, X3))active#(X1)
active#(U51(tt, V1, V2))U52#(isNat(V1), V2)active#(U32(X))active#(X)
active#(U61(X1, X2))active#(X1)active#(length(cons(N, L)))and#(isNat(N), isNatKind(N))
active#(length(X))active#(X)active#(U52(tt, V2))U53#(isNatList(V2))
active#(U21(tt, V1))isNat#(V1)active#(U41(X1, X2, X3))active#(X1)
active#(U31(tt, V))isNatList#(V)active#(isNatList(cons(V1, V2)))isNatIListKind#(V2)
active#(length(cons(N, L)))isNatIListKind#(L)active#(isNat(length(V1)))U11#(isNatIListKind(V1), V1)
active#(U31(tt, V))U32#(isNatList(V))active#(isNatList(cons(V1, V2)))U51#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)
active#(cons(X1, X2))active#(X1)active#(length(cons(N, L)))isNatKind#(N)
active#(U42(X1, X2))active#(X1)active#(U41(X1, X2, X3))U41#(active(X1), X2, X3)
active#(U52(X1, X2))U52#(active(X1), X2)active#(U43(X))active#(X)
active#(U52(X1, X2))active#(X1)active#(isNatList(cons(V1, V2)))and#(isNatKind(V1), isNatIListKind(V2))
active#(U41(tt, V1, V2))isNat#(V1)active#(and(X1, X2))and#(active(X1), X2)
active#(U53(X))active#(X)active#(U31(X1, X2))U31#(active(X1), X2)
active#(U12(X))U12#(active(X))active#(length(cons(N, L)))isNat#(N)
active#(length(cons(N, L)))U61#(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L)active#(U31(X1, X2))active#(X1)
active#(length(X))length#(active(X))active#(U32(X))U32#(active(X))
active#(length(cons(N, L)))and#(isNatList(L), isNatIListKind(L))active#(isNatIList(cons(V1, V2)))isNatKind#(V1)
active#(U11(X1, X2))U11#(active(X1), X2)active#(U21(X1, X2))active#(X1)
active#(isNatIList(cons(V1, V2)))U41#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)active#(U22(X))active#(X)
active#(isNat(s(V1)))U21#(isNatKind(V1), V1)active#(U51(X1, X2, X3))U51#(active(X1), X2, X3)
active#(s(X))active#(X)active#(zeros)cons#(0, zeros)
active#(isNatList(cons(V1, V2)))isNatKind#(V1)active#(isNatIList(V))U31#(isNatIListKind(V), V)
active#(and(X1, X2))active#(X1)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


The following SCCs where found

active#(U51(X1, X2, X3)) → active#(X1)active#(U32(X)) → active#(X)
active#(U12(X)) → active#(X)active#(U42(X1, X2)) → active#(X1)
active#(U61(X1, X2)) → active#(X1)active#(length(X)) → active#(X)
active#(U43(X)) → active#(X)active#(U52(X1, X2)) → active#(X1)
active#(U41(X1, X2, X3)) → active#(X1)active#(U53(X)) → active#(X)
active#(U21(X1, X2)) → active#(X1)active#(U22(X)) → active#(X)
active#(s(X)) → active#(X)active#(U31(X1, X2)) → active#(X1)
active#(and(X1, X2)) → active#(X1)active#(U11(X1, X2)) → active#(X1)
active#(cons(X1, X2)) → active#(X1)

Problem 29: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

active#(U51(X1, X2, X3))active#(X1)active#(U32(X))active#(X)
active#(U61(X1, X2))active#(X1)active#(U42(X1, X2))active#(X1)
active#(U12(X))active#(X)active#(length(X))active#(X)
active#(U43(X))active#(X)active#(U52(X1, X2))active#(X1)
active#(U41(X1, X2, X3))active#(X1)active#(U21(X1, X2))active#(X1)
active#(U53(X))active#(X)active#(U22(X))active#(X)
active#(s(X))active#(X)active#(U31(X1, X2))active#(X1)
active#(and(X1, X2))active#(X1)active#(U11(X1, X2))active#(X1)
active#(cons(X1, X2))active#(X1)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Polynomial Interpretation

There are no usable rules

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

active#(U31(X1, X2))active#(X1)

Problem 19: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 20: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 21: 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, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, 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 22: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

active#(U51(X1, X2, X3))active#(X1)active#(U32(X))active#(X)
active#(U61(X1, X2))active#(X1)active#(U12(X))active#(X)
active#(U42(X1, X2))active#(X1)active#(length(X))active#(X)
active#(U43(X))active#(X)active#(U52(X1, X2))active#(X1)
active#(U41(X1, X2, X3))active#(X1)active#(U21(X1, X2))active#(X1)
active#(U53(X))active#(X)active#(U22(X))active#(X)
active#(s(X))active#(X)active#(U31(X1, X2))active#(X1)
active#(and(X1, X2))active#(X1)active#(U11(X1, X2))active#(X1)
active#(cons(X1, X2))active#(X1)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

active#(U51(X1, X2, X3))active#(X1)active#(U32(X))active#(X)
active#(U61(X1, X2))active#(X1)active#(U12(X))active#(X)
active#(U42(X1, X2))active#(X1)active#(length(X))active#(X)
active#(U43(X))active#(X)active#(U52(X1, X2))active#(X1)
active#(U41(X1, X2, X3))active#(X1)active#(U21(X1, X2))active#(X1)
active#(U53(X))active#(X)active#(U22(X))active#(X)
active#(s(X))active#(X)active#(U31(X1, X2))active#(X1)
active#(and(X1, X2))active#(X1)active#(U11(X1, X2))active#(X1)
active#(cons(X1, X2))active#(X1)

Problem 23: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 24: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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

Problem 25: 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, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, 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 26: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

U22#(ok(X))U22#(X)U22#(mark(X))U22#(X)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

U22#(ok(X))U22#(X)U22#(mark(X))U22#(X)

Problem 27: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

proper#(U52(X1, X2))proper#(X1)proper#(U51(X1, X2, X3))proper#(X2)
proper#(cons(X1, X2))proper#(X1)proper#(U11(X1, X2))proper#(X1)
proper#(isNatIListKind(X))proper#(X)proper#(U42(X1, X2))proper#(X2)
proper#(U41(X1, X2, X3))proper#(X3)proper#(U31(X1, X2))proper#(X1)
proper#(U31(X1, X2))proper#(X2)proper#(and(X1, X2))proper#(X1)
proper#(U41(X1, X2, X3))proper#(X2)proper#(U42(X1, X2))proper#(X1)
proper#(U32(X))proper#(X)proper#(U21(X1, X2))proper#(X2)
proper#(isNatKind(X))proper#(X)proper#(U11(X1, X2))proper#(X2)
proper#(and(X1, X2))proper#(X2)proper#(U61(X1, X2))proper#(X2)
proper#(U41(X1, X2, X3))proper#(X1)proper#(U51(X1, X2, X3))proper#(X3)
proper#(isNatList(X))proper#(X)proper#(U53(X))proper#(X)
proper#(U43(X))proper#(X)proper#(isNat(X))proper#(X)
proper#(cons(X1, X2))proper#(X2)proper#(U12(X))proper#(X)
proper#(isNatIList(X))proper#(X)proper#(U61(X1, X2))proper#(X1)
proper#(U52(X1, X2))proper#(X2)proper#(length(X))proper#(X)
proper#(s(X))proper#(X)proper#(U51(X1, X2, X3))proper#(X1)
proper#(U21(X1, X2))proper#(X1)proper#(U22(X))proper#(X)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

proper#(U51(X1, X2, X3))proper#(X2)proper#(U52(X1, X2))proper#(X1)
proper#(cons(X1, X2))proper#(X1)proper#(U11(X1, X2))proper#(X1)
proper#(isNatIListKind(X))proper#(X)proper#(U42(X1, X2))proper#(X2)
proper#(U31(X1, X2))proper#(X1)proper#(U41(X1, X2, X3))proper#(X3)
proper#(U31(X1, X2))proper#(X2)proper#(and(X1, X2))proper#(X1)
proper#(U41(X1, X2, X3))proper#(X2)proper#(U42(X1, X2))proper#(X1)
proper#(U32(X))proper#(X)proper#(U21(X1, X2))proper#(X2)
proper#(isNatKind(X))proper#(X)proper#(U11(X1, X2))proper#(X2)
proper#(and(X1, X2))proper#(X2)proper#(U61(X1, X2))proper#(X2)
proper#(U41(X1, X2, X3))proper#(X1)proper#(U51(X1, X2, X3))proper#(X3)
proper#(isNatList(X))proper#(X)proper#(U53(X))proper#(X)
proper#(U43(X))proper#(X)proper#(isNat(X))proper#(X)
proper#(cons(X1, X2))proper#(X2)proper#(U12(X))proper#(X)
proper#(isNatIList(X))proper#(X)proper#(U61(X1, X2))proper#(X1)
proper#(U52(X1, X2))proper#(X2)proper#(s(X))proper#(X)
proper#(length(X))proper#(X)proper#(U51(X1, X2, X3))proper#(X1)
proper#(U21(X1, X2))proper#(X1)proper#(U22(X))proper#(X)

Problem 28: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

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

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatList(V1)))
active(U12(tt))mark(tt)active(U21(tt, V1))mark(U22(isNat(V1)))
active(U22(tt))mark(tt)active(U31(tt, V))mark(U32(isNatList(V)))
active(U32(tt))mark(tt)active(U41(tt, V1, V2))mark(U42(isNat(V1), V2))
active(U42(tt, V2))mark(U43(isNatIList(V2)))active(U43(tt))mark(tt)
active(U51(tt, V1, V2))mark(U52(isNat(V1), V2))active(U52(tt, V2))mark(U53(isNatList(V2)))
active(U53(tt))mark(tt)active(U61(tt, L))mark(s(length(L)))
active(and(tt, X))mark(X)active(isNat(0))mark(tt)
active(isNat(length(V1)))mark(U11(isNatIListKind(V1), V1))active(isNat(s(V1)))mark(U21(isNatKind(V1), V1))
active(isNatIList(V))mark(U31(isNatIListKind(V), V))active(isNatIList(zeros))mark(tt)
active(isNatIList(cons(V1, V2)))mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(isNatIListKind(nil))mark(tt)
active(isNatIListKind(zeros))mark(tt)active(isNatIListKind(cons(V1, V2)))mark(and(isNatKind(V1), isNatIListKind(V2)))
active(isNatKind(0))mark(tt)active(isNatKind(length(V1)))mark(isNatIListKind(V1))
active(isNatKind(s(V1)))mark(isNatKind(V1))active(isNatList(nil))mark(tt)
active(isNatList(cons(V1, V2)))mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2))active(length(nil))mark(0)
active(length(cons(N, L)))mark(U61(and(and(isNatList(L), isNatIListKind(L)), and(isNat(N), isNatKind(N))), L))active(cons(X1, X2))cons(active(X1), X2)
active(U11(X1, X2))U11(active(X1), X2)active(U12(X))U12(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X))U22(active(X))
active(U31(X1, X2))U31(active(X1), X2)active(U32(X))U32(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2))U42(active(X1), X2)
active(U43(X))U43(active(X))active(U51(X1, X2, X3))U51(active(X1), X2, X3)
active(U52(X1, X2))U52(active(X1), X2)active(U53(X))U53(active(X))
active(U61(X1, X2))U61(active(X1), X2)active(s(X))s(active(X))
active(length(X))length(active(X))active(and(X1, X2))and(active(X1), X2)
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X))mark(U12(X))U21(mark(X1), X2)mark(U21(X1, X2))
U22(mark(X))mark(U22(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X))mark(U32(X))U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))
U42(mark(X1), X2)mark(U42(X1, X2))U43(mark(X))mark(U43(X))
U51(mark(X1), X2, X3)mark(U51(X1, X2, X3))U52(mark(X1), X2)mark(U52(X1, X2))
U53(mark(X))mark(U53(X))U61(mark(X1), X2)mark(U61(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
and(mark(X1), X2)mark(and(X1, X2))proper(zeros)ok(zeros)
proper(cons(X1, X2))cons(proper(X1), proper(X2))proper(0)ok(0)
proper(U11(X1, X2))U11(proper(X1), proper(X2))proper(tt)ok(tt)
proper(U12(X))U12(proper(X))proper(isNatList(X))isNatList(proper(X))
proper(U21(X1, X2))U21(proper(X1), proper(X2))proper(U22(X))U22(proper(X))
proper(isNat(X))isNat(proper(X))proper(U31(X1, X2))U31(proper(X1), proper(X2))
proper(U32(X))U32(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2))U42(proper(X1), proper(X2))proper(U43(X))U43(proper(X))
proper(isNatIList(X))isNatIList(proper(X))proper(U51(X1, X2, X3))U51(proper(X1), proper(X2), proper(X3))
proper(U52(X1, X2))U52(proper(X1), proper(X2))proper(U53(X))U53(proper(X))
proper(U61(X1, X2))U61(proper(X1), proper(X2))proper(s(X))s(proper(X))
proper(length(X))length(proper(X))proper(and(X1, X2))and(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(isNatKind(X))isNatKind(proper(X))
proper(nil)ok(nil)cons(ok(X1), ok(X2))ok(cons(X1, X2))
U11(ok(X1), ok(X2))ok(U11(X1, X2))U12(ok(X))ok(U12(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X))ok(U22(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X))ok(U32(X))
U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))U42(ok(X1), ok(X2))ok(U42(X1, X2))
U43(ok(X))ok(U43(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2), ok(X3))ok(U51(X1, X2, X3))U52(ok(X1), ok(X2))ok(U52(X1, X2))
U53(ok(X))ok(U53(X))U61(ok(X1), ok(X2))ok(U61(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(X))
and(ok(X1), ok(X2))ok(and(X1, X2))isNatIListKind(ok(X))ok(isNatIListKind(X))
isNatKind(ok(X))ok(isNatKind(X))top(mark(X))top(proper(X))
top(ok(X))top(active(X))

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, isNat, U61, U43, U42, U41, length, ok, proper, U21, cons, U22, top, isNatIList, isNatKind, mark, and, 0, isNatList, U51, s, tt, zeros, U53, U52, active, U11, U12, U31, U32, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

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