TIMEOUT

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

The following DP Processors were used


Problem 1 remains open; application of the following processors failed [DependencyGraph (timeout)].

The following open problems remain:



Open Dependency Pair Problem 1

Dependency Pairs

proper#(cons(X1, X2))proper#(X1)U85#(ok(X1), ok(X2))U85#(X1, X2)
proper#(length(X))length#(proper(X))active#(U51(X1, X2))active#(X1)
active#(U94(X1, X2))active#(X1)active#(U93(X1, X2, X3))active#(X1)
U11#(mark(X1), X2)U11#(X1, X2)active#(isNatIListKind(cons(V1, V2)))U51#(isNatKind(V1), V2)
proper#(U92(X1, X2, X3))proper#(X1)active#(isNatList(cons(V1, V2)))U81#(isNatKind(V1), V1, V2)
U51#(mark(X1), X2)U51#(X1, X2)U91#(mark(X1), X2, X3)U91#(X1, X2, X3)
active#(isNatIListKind(cons(V1, V2)))isNatKind#(V1)active#(isNatIList(cons(V1, V2)))U41#(isNatKind(V1), V1, V2)
top#(mark(X))proper#(X)length#(mark(X))length#(X)
isNatKind#(ok(X))isNatKind#(X)U43#(mark(X1), X2, X3)U43#(X1, X2, X3)
U86#(mark(X))U86#(X)active#(U81(X1, X2, X3))active#(X1)
active#(U41(tt, V1, V2))isNatKind#(V1)active#(U82(tt, V1, V2))U83#(isNatIListKind(V2), V1, V2)
active#(length(X))active#(X)proper#(U43(X1, X2, X3))proper#(X3)
active#(U21(tt, V1))isNatKind#(V1)proper#(U42(X1, X2, X3))U42#(proper(X1), proper(X2), proper(X3))
active#(U86(X))U86#(active(X))active#(U85(tt, V2))isNatList#(V2)
proper#(U23(X))U23#(proper(X))U43#(ok(X1), ok(X2), ok(X3))U43#(X1, X2, X3)
proper#(U82(X1, X2, X3))proper#(X1)active#(U32(tt, V))U33#(isNatList(V))
proper#(U43(X1, X2, X3))proper#(X1)proper#(isNatKind(X))isNatKind#(proper(X))
active#(U33(X))active#(X)active#(U43(tt, V1, V2))U44#(isNatIListKind(V2), V1, V2)
U45#(ok(X1), ok(X2))U45#(X1, X2)proper#(U44(X1, X2, X3))U44#(proper(X1), proper(X2), proper(X3))
active#(U41(X1, X2, X3))U41#(active(X1), X2, X3)active#(U44(tt, V1, V2))U45#(isNat(V1), V2)
proper#(U45(X1, X2))U45#(proper(X1), proper(X2))active#(U91(tt, L, N))isNatIListKind#(L)
active#(U84(tt, V1, V2))U85#(isNat(V1), V2)active#(U45(tt, V2))U46#(isNatIList(V2))
active#(U44(X1, X2, X3))active#(X1)proper#(U41(X1, X2, X3))proper#(X1)
U93#(ok(X1), ok(X2), ok(X3))U93#(X1, X2, X3)active#(U52(X))active#(X)
active#(U31(X1, X2))active#(X1)active#(U22(X1, X2))active#(X1)
active#(isNatKind(s(V1)))U71#(isNatKind(V1))active#(U81(tt, V1, V2))U82#(isNatKind(V1), V1, V2)
proper#(isNatList(X))proper#(X)active#(U13(X))active#(X)
proper#(U51(X1, X2))proper#(X2)active#(U93(tt, L, N))isNatKind#(N)
proper#(U91(X1, X2, X3))proper#(X3)proper#(U71(X))U71#(proper(X))
active#(U83(X1, X2, X3))U83#(active(X1), X2, X3)proper#(U22(X1, X2))U22#(proper(X1), proper(X2))
U41#(ok(X1), ok(X2), ok(X3))U41#(X1, X2, X3)active#(U21(X1, X2))U21#(active(X1), X2)
active#(U52(X))U52#(active(X))active#(U12(tt, V1))isNatList#(V1)
proper#(isNat(X))proper#(X)proper#(U91(X1, X2, X3))U91#(proper(X1), proper(X2), proper(X3))
active#(U94(tt, L))s#(length(L))U33#(mark(X))U33#(X)
active#(U11(X1, X2))U11#(active(X1), X2)proper#(U92(X1, X2, X3))proper#(X3)
active#(U83(X1, X2, X3))active#(X1)active#(U92(tt, L, N))isNat#(N)
U22#(ok(X1), ok(X2))U22#(X1, X2)active#(isNat(s(V1)))U21#(isNatKind(V1), V1)
U91#(ok(X1), ok(X2), ok(X3))U91#(X1, X2, X3)active#(U51(tt, V2))isNatIListKind#(V2)
proper#(U31(X1, X2))U31#(proper(X1), proper(X2))proper#(U21(X1, X2))proper#(X1)
active#(U41(tt, V1, V2))U42#(isNatKind(V1), V1, V2)U31#(ok(X1), ok(X2))U31#(X1, X2)
active#(U31(tt, V))U32#(isNatIListKind(V), V)proper#(U81(X1, X2, X3))U81#(proper(X1), proper(X2), proper(X3))
active#(U22(X1, X2))U22#(active(X1), X2)U12#(ok(X1), ok(X2))U12#(X1, X2)
isNatIListKind#(ok(X))isNatIListKind#(X)cons#(ok(X1), ok(X2))cons#(X1, X2)
proper#(U12(X1, X2))proper#(X2)active#(U42(X1, X2, X3))active#(X1)
proper#(U11(X1, X2))U11#(proper(X1), proper(X2))active#(U21(tt, V1))U22#(isNatKind(V1), V1)
proper#(U51(X1, X2))U51#(proper(X1), proper(X2))U85#(mark(X1), X2)U85#(X1, X2)
proper#(U94(X1, X2))proper#(X2)active#(U51(X1, X2))U51#(active(X1), X2)
length#(ok(X))length#(X)U12#(mark(X1), X2)U12#(X1, X2)
proper#(U81(X1, X2, X3))proper#(X2)active#(U85(tt, V2))U86#(isNatList(V2))
proper#(U32(X1, X2))proper#(X1)proper#(U41(X1, X2, X3))U41#(proper(X1), proper(X2), proper(X3))
active#(U85(X1, X2))U85#(active(X1), X2)U71#(mark(X))U71#(X)
active#(U11(tt, V1))isNatIListKind#(V1)active#(U61(X))U61#(active(X))
active#(U92(X1, X2, X3))active#(X1)U52#(ok(X))U52#(X)
active#(U22(tt, V1))U23#(isNat(V1))active#(U93(X1, X2, X3))U93#(active(X1), X2, X3)
proper#(s(X))proper#(X)U32#(ok(X1), ok(X2))U32#(X1, X2)
active#(U51(tt, V2))U52#(isNatIListKind(V2))active#(U13(X))U13#(active(X))
proper#(isNatList(X))isNatList#(proper(X))proper#(U45(X1, X2))proper#(X2)
active#(isNat(length(V1)))U11#(isNatIListKind(V1), V1)active#(U33(X))U33#(active(X))
proper#(U85(X1, X2))proper#(X2)proper#(U32(X1, X2))U32#(proper(X1), proper(X2))
U84#(ok(X1), ok(X2), ok(X3))U84#(X1, X2, X3)U33#(ok(X))U33#(X)
active#(cons(X1, X2))active#(X1)proper#(U81(X1, X2, X3))proper#(X3)
active#(U43(tt, V1, V2))isNatIListKind#(V2)active#(U82(X1, X2, X3))active#(X1)
U44#(ok(X1), ok(X2), ok(X3))U44#(X1, X2, X3)active#(U86(X))active#(X)
proper#(U31(X1, X2))proper#(X2)proper#(U92(X1, X2, X3))U92#(proper(X1), proper(X2), proper(X3))
proper#(U61(X))U61#(proper(X))proper#(U51(X1, X2))proper#(X1)
active#(length(cons(N, L)))isNatList#(L)proper#(U43(X1, X2, X3))proper#(X2)
active#(U83(tt, V1, V2))U84#(isNatIListKind(V2), V1, V2)proper#(U85(X1, X2))U85#(proper(X1), proper(X2))
active#(U11(tt, V1))U12#(isNatIListKind(V1), V1)proper#(U81(X1, X2, X3))proper#(X1)
active#(U44(X1, X2, X3))U44#(active(X1), X2, X3)proper#(U42(X1, X2, X3))proper#(X2)
active#(length(cons(N, L)))U91#(isNatList(L), L, N)U94#(mark(X1), X2)U94#(X1, X2)
proper#(U12(X1, X2))proper#(X1)proper#(U61(X))proper#(X)
active#(isNatKind(length(V1)))U61#(isNatIListKind(V1))proper#(U84(X1, X2, X3))proper#(X3)
proper#(U84(X1, X2, X3))proper#(X1)proper#(U33(X))U33#(proper(X))
s#(mark(X))s#(X)proper#(U84(X1, X2, X3))proper#(X2)
active#(U31(tt, V))isNatIListKind#(V)proper#(U86(X))proper#(X)
active#(U45(X1, X2))U45#(active(X1), X2)active#(s(X))active#(X)
proper#(U46(X))proper#(X)U83#(mark(X1), X2, X3)U83#(X1, X2, X3)
U52#(mark(X))U52#(X)U92#(ok(X1), ok(X2), ok(X3))U92#(X1, X2, X3)
active#(U61(X))active#(X)active#(isNatIList(V))U31#(isNatIListKind(V), V)
U21#(ok(X1), ok(X2))U21#(X1, X2)active#(U82(X1, X2, X3))U82#(active(X1), X2, X3)
U42#(ok(X1), ok(X2), ok(X3))U42#(X1, X2, X3)proper#(U44(X1, X2, X3))proper#(X2)
proper#(U33(X))proper#(X)proper#(U11(X1, X2))proper#(X1)
proper#(U71(X))proper#(X)active#(isNatIList(V))isNatIListKind#(V)
proper#(U91(X1, X2, X3))proper#(X2)proper#(U52(X))U52#(proper(X))
active#(U42(X1, X2, X3))U42#(active(X1), X2, X3)active#(U32(tt, V))isNatList#(V)
proper#(U91(X1, X2, X3))proper#(X1)proper#(U41(X1, X2, X3))proper#(X2)
proper#(U32(X1, X2))proper#(X2)proper#(isNatKind(X))proper#(X)
proper#(U94(X1, X2))proper#(X1)proper#(U11(X1, X2))proper#(X2)
active#(U42(tt, V1, V2))isNatIListKind#(V2)active#(U83(tt, V1, V2))isNatIListKind#(V2)
proper#(U23(X))proper#(X)active#(U22(tt, V1))isNat#(V1)
U44#(mark(X1), X2, X3)U44#(X1, X2, X3)active#(U42(tt, V1, V2))U43#(isNatIListKind(V2), V1, V2)
active#(U46(X))active#(X)isNat#(ok(X))isNat#(X)
proper#(U46(X))U46#(proper(X))proper#(U94(X1, X2))U94#(proper(X1), proper(X2))
isNatIList#(ok(X))isNatIList#(X)active#(U41(X1, X2, X3))active#(X1)
active#(U12(X1, X2))U12#(active(X1), X2)active#(isNatKind(length(V1)))isNatIListKind#(V1)
active#(isNat(s(V1)))isNatKind#(V1)proper#(U13(X))U13#(proper(X))
proper#(U42(X1, X2, X3))proper#(X3)active#(U91(tt, L, N))U92#(isNatIListKind(L), L, N)
proper#(U93(X1, X2, X3))proper#(X1)active#(U93(tt, L, N))U94#(isNatKind(N), L)
proper#(isNatIListKind(X))proper#(X)U22#(mark(X1), X2)U22#(X1, X2)
cons#(mark(X1), X2)cons#(X1, X2)proper#(U44(X1, X2, X3))proper#(X1)
active#(U43(X1, X2, X3))active#(X1)top#(ok(X))active#(X)
active#(U91(X1, X2, X3))U91#(active(X1), X2, X3)U82#(mark(X1), X2, X3)U82#(X1, X2, X3)
proper#(U93(X1, X2, X3))proper#(X3)proper#(U93(X1, X2, X3))U93#(proper(X1), proper(X2), proper(X3))
U45#(mark(X1), X2)U45#(X1, X2)U83#(ok(X1), ok(X2), ok(X3))U83#(X1, X2, X3)
U94#(ok(X1), ok(X2))U94#(X1, X2)U13#(mark(X))U13#(X)
active#(U94(tt, L))length#(L)proper#(isNat(X))isNat#(proper(X))
active#(isNat(length(V1)))isNatIListKind#(V1)U51#(ok(X1), ok(X2))U51#(X1, X2)
proper#(U45(X1, X2))proper#(X1)U61#(mark(X))U61#(X)
active#(U12(X1, X2))active#(X1)proper#(U42(X1, X2, X3))proper#(X1)
active#(s(X))s#(active(X))s#(ok(X))s#(X)
U81#(ok(X1), ok(X2), ok(X3))U81#(X1, X2, X3)proper#(length(X))proper#(X)
active#(U32(X1, X2))active#(X1)active#(U32(X1, X2))U32#(active(X1), X2)
proper#(s(X))s#(proper(X))active#(U23(X))active#(X)
active#(zeros)cons#(0, zeros)active#(U46(X))U46#(active(X))
top#(ok(X))top#(active(X))U61#(ok(X))U61#(X)
proper#(U31(X1, X2))proper#(X1)U71#(ok(X))U71#(X)
U92#(mark(X1), X2, X3)U92#(X1, X2, X3)U11#(ok(X1), ok(X2))U11#(X1, X2)
U23#(mark(X))U23#(X)proper#(isNatIList(X))isNatIList#(proper(X))
proper#(U83(X1, X2, X3))proper#(X1)active#(cons(X1, X2))cons#(active(X1), X2)
active#(U45(tt, V2))isNatIList#(V2)U82#(ok(X1), ok(X2), ok(X3))U82#(X1, X2, X3)
active#(U81(tt, V1, V2))isNatKind#(V1)proper#(U83(X1, X2, X3))proper#(X2)
U93#(mark(X1), X2, X3)U93#(X1, X2, X3)active#(U91(X1, X2, X3))active#(X1)
active#(U11(X1, X2))active#(X1)active#(U23(X))U23#(active(X))
U81#(mark(X1), X2, X3)U81#(X1, X2, X3)U84#(mark(X1), X2, X3)U84#(X1, X2, X3)
active#(U82(tt, V1, V2))isNatIListKind#(V2)top#(mark(X))top#(proper(X))
U42#(mark(X1), X2, X3)U42#(X1, X2, X3)proper#(cons(X1, X2))proper#(X2)
proper#(isNatIList(X))proper#(X)U13#(ok(X))U13#(X)
active#(U84(X1, X2, X3))active#(X1)active#(U43(X1, X2, X3))U43#(active(X1), X2, X3)
active#(U45(X1, X2))active#(X1)proper#(U22(X1, X2))proper#(X2)
isNatList#(ok(X))isNatList#(X)proper#(U84(X1, X2, X3))U84#(proper(X1), proper(X2), proper(X3))
active#(U84(tt, V1, V2))isNat#(V1)active#(U92(X1, X2, X3))U92#(active(X1), X2, X3)
proper#(U82(X1, X2, X3))U82#(proper(X1), proper(X2), proper(X3))active#(U71(X))U71#(active(X))
active#(U81(X1, X2, X3))U81#(active(X1), X2, X3)proper#(U82(X1, X2, X3))proper#(X3)
active#(U84(X1, X2, X3))U84#(active(X1), X2, X3)proper#(U12(X1, X2))U12#(proper(X1), proper(X2))
proper#(U83(X1, X2, X3))U83#(proper(X1), proper(X2), proper(X3))proper#(U41(X1, X2, X3))proper#(X3)
proper#(U85(X1, X2))proper#(X1)U86#(ok(X))U86#(X)
proper#(U13(X))proper#(X)active#(U85(X1, X2))active#(X1)
proper#(U21(X1, X2))proper#(X2)proper#(U22(X1, X2))proper#(X1)
active#(U31(X1, X2))U31#(active(X1), X2)U41#(mark(X1), X2, X3)U41#(X1, X2, X3)
proper#(isNatIListKind(X))isNatIListKind#(proper(X))U23#(ok(X))U23#(X)
proper#(U86(X))U86#(proper(X))active#(U44(tt, V1, V2))isNat#(V1)
active#(isNatKind(s(V1)))isNatKind#(V1)active#(U94(X1, X2))U94#(active(X1), X2)
proper#(U21(X1, X2))U21#(proper(X1), proper(X2))active#(length(X))length#(active(X))
proper#(U43(X1, X2, X3))U43#(proper(X1), proper(X2), proper(X3))active#(U92(tt, L, N))U93#(isNat(N), L, N)
active#(isNatIList(cons(V1, V2)))isNatKind#(V1)U46#(mark(X))U46#(X)
U31#(mark(X1), X2)U31#(X1, X2)proper#(U92(X1, X2, X3))proper#(X2)
proper#(U44(X1, X2, X3))proper#(X3)active#(U21(X1, X2))active#(X1)
proper#(cons(X1, X2))cons#(proper(X1), proper(X2))proper#(U93(X1, X2, X3))proper#(X2)
active#(U12(tt, V1))U13#(isNatList(V1))proper#(U82(X1, X2, X3))proper#(X2)
U21#(mark(X1), X2)U21#(X1, X2)U32#(mark(X1), X2)U32#(X1, X2)
active#(isNatList(cons(V1, V2)))isNatKind#(V1)U46#(ok(X))U46#(X)
active#(U71(X))active#(X)proper#(U52(X))proper#(X)
proper#(U83(X1, X2, X3))proper#(X3)

Rewrite Rules

active(zeros)mark(cons(0, zeros))active(U11(tt, V1))mark(U12(isNatIListKind(V1), V1))
active(U12(tt, V1))mark(U13(isNatList(V1)))active(U13(tt))mark(tt)
active(U21(tt, V1))mark(U22(isNatKind(V1), V1))active(U22(tt, V1))mark(U23(isNat(V1)))
active(U23(tt))mark(tt)active(U31(tt, V))mark(U32(isNatIListKind(V), V))
active(U32(tt, V))mark(U33(isNatList(V)))active(U33(tt))mark(tt)
active(U41(tt, V1, V2))mark(U42(isNatKind(V1), V1, V2))active(U42(tt, V1, V2))mark(U43(isNatIListKind(V2), V1, V2))
active(U43(tt, V1, V2))mark(U44(isNatIListKind(V2), V1, V2))active(U44(tt, V1, V2))mark(U45(isNat(V1), V2))
active(U45(tt, V2))mark(U46(isNatIList(V2)))active(U46(tt))mark(tt)
active(U51(tt, V2))mark(U52(isNatIListKind(V2)))active(U52(tt))mark(tt)
active(U61(tt))mark(tt)active(U71(tt))mark(tt)
active(U81(tt, V1, V2))mark(U82(isNatKind(V1), V1, V2))active(U82(tt, V1, V2))mark(U83(isNatIListKind(V2), V1, V2))
active(U83(tt, V1, V2))mark(U84(isNatIListKind(V2), V1, V2))active(U84(tt, V1, V2))mark(U85(isNat(V1), V2))
active(U85(tt, V2))mark(U86(isNatList(V2)))active(U86(tt))mark(tt)
active(U91(tt, L, N))mark(U92(isNatIListKind(L), L, N))active(U92(tt, L, N))mark(U93(isNat(N), L, N))
active(U93(tt, L, N))mark(U94(isNatKind(N), L))active(U94(tt, L))mark(s(length(L)))
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(isNatKind(V1), V1, V2))
active(isNatIListKind(nil))mark(tt)active(isNatIListKind(zeros))mark(tt)
active(isNatIListKind(cons(V1, V2)))mark(U51(isNatKind(V1), V2))active(isNatKind(0))mark(tt)
active(isNatKind(length(V1)))mark(U61(isNatIListKind(V1)))active(isNatKind(s(V1)))mark(U71(isNatKind(V1)))
active(isNatList(nil))mark(tt)active(isNatList(cons(V1, V2)))mark(U81(isNatKind(V1), V1, V2))
active(length(nil))mark(0)active(length(cons(N, L)))mark(U91(isNatList(L), L, N))
active(cons(X1, X2))cons(active(X1), X2)active(U11(X1, X2))U11(active(X1), X2)
active(U12(X1, X2))U12(active(X1), X2)active(U13(X))U13(active(X))
active(U21(X1, X2))U21(active(X1), X2)active(U22(X1, X2))U22(active(X1), X2)
active(U23(X))U23(active(X))active(U31(X1, X2))U31(active(X1), X2)
active(U32(X1, X2))U32(active(X1), X2)active(U33(X))U33(active(X))
active(U41(X1, X2, X3))U41(active(X1), X2, X3)active(U42(X1, X2, X3))U42(active(X1), X2, X3)
active(U43(X1, X2, X3))U43(active(X1), X2, X3)active(U44(X1, X2, X3))U44(active(X1), X2, X3)
active(U45(X1, X2))U45(active(X1), X2)active(U46(X))U46(active(X))
active(U51(X1, X2))U51(active(X1), X2)active(U52(X))U52(active(X))
active(U61(X))U61(active(X))active(U71(X))U71(active(X))
active(U81(X1, X2, X3))U81(active(X1), X2, X3)active(U82(X1, X2, X3))U82(active(X1), X2, X3)
active(U83(X1, X2, X3))U83(active(X1), X2, X3)active(U84(X1, X2, X3))U84(active(X1), X2, X3)
active(U85(X1, X2))U85(active(X1), X2)active(U86(X))U86(active(X))
active(U91(X1, X2, X3))U91(active(X1), X2, X3)active(U92(X1, X2, X3))U92(active(X1), X2, X3)
active(U93(X1, X2, X3))U93(active(X1), X2, X3)active(U94(X1, X2))U94(active(X1), X2)
active(s(X))s(active(X))active(length(X))length(active(X))
cons(mark(X1), X2)mark(cons(X1, X2))U11(mark(X1), X2)mark(U11(X1, X2))
U12(mark(X1), X2)mark(U12(X1, X2))U13(mark(X))mark(U13(X))
U21(mark(X1), X2)mark(U21(X1, X2))U22(mark(X1), X2)mark(U22(X1, X2))
U23(mark(X))mark(U23(X))U31(mark(X1), X2)mark(U31(X1, X2))
U32(mark(X1), X2)mark(U32(X1, X2))U33(mark(X))mark(U33(X))
U41(mark(X1), X2, X3)mark(U41(X1, X2, X3))U42(mark(X1), X2, X3)mark(U42(X1, X2, X3))
U43(mark(X1), X2, X3)mark(U43(X1, X2, X3))U44(mark(X1), X2, X3)mark(U44(X1, X2, X3))
U45(mark(X1), X2)mark(U45(X1, X2))U46(mark(X))mark(U46(X))
U51(mark(X1), X2)mark(U51(X1, X2))U52(mark(X))mark(U52(X))
U61(mark(X))mark(U61(X))U71(mark(X))mark(U71(X))
U81(mark(X1), X2, X3)mark(U81(X1, X2, X3))U82(mark(X1), X2, X3)mark(U82(X1, X2, X3))
U83(mark(X1), X2, X3)mark(U83(X1, X2, X3))U84(mark(X1), X2, X3)mark(U84(X1, X2, X3))
U85(mark(X1), X2)mark(U85(X1, X2))U86(mark(X))mark(U86(X))
U91(mark(X1), X2, X3)mark(U91(X1, X2, X3))U92(mark(X1), X2, X3)mark(U92(X1, X2, X3))
U93(mark(X1), X2, X3)mark(U93(X1, X2, X3))U94(mark(X1), X2)mark(U94(X1, X2))
s(mark(X))mark(s(X))length(mark(X))mark(length(X))
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(X1, X2))U12(proper(X1), proper(X2))
proper(isNatIListKind(X))isNatIListKind(proper(X))proper(U13(X))U13(proper(X))
proper(isNatList(X))isNatList(proper(X))proper(U21(X1, X2))U21(proper(X1), proper(X2))
proper(U22(X1, X2))U22(proper(X1), proper(X2))proper(isNatKind(X))isNatKind(proper(X))
proper(U23(X))U23(proper(X))proper(isNat(X))isNat(proper(X))
proper(U31(X1, X2))U31(proper(X1), proper(X2))proper(U32(X1, X2))U32(proper(X1), proper(X2))
proper(U33(X))U33(proper(X))proper(U41(X1, X2, X3))U41(proper(X1), proper(X2), proper(X3))
proper(U42(X1, X2, X3))U42(proper(X1), proper(X2), proper(X3))proper(U43(X1, X2, X3))U43(proper(X1), proper(X2), proper(X3))
proper(U44(X1, X2, X3))U44(proper(X1), proper(X2), proper(X3))proper(U45(X1, X2))U45(proper(X1), proper(X2))
proper(U46(X))U46(proper(X))proper(isNatIList(X))isNatIList(proper(X))
proper(U51(X1, X2))U51(proper(X1), proper(X2))proper(U52(X))U52(proper(X))
proper(U61(X))U61(proper(X))proper(U71(X))U71(proper(X))
proper(U81(X1, X2, X3))U81(proper(X1), proper(X2), proper(X3))proper(U82(X1, X2, X3))U82(proper(X1), proper(X2), proper(X3))
proper(U83(X1, X2, X3))U83(proper(X1), proper(X2), proper(X3))proper(U84(X1, X2, X3))U84(proper(X1), proper(X2), proper(X3))
proper(U85(X1, X2))U85(proper(X1), proper(X2))proper(U86(X))U86(proper(X))
proper(U91(X1, X2, X3))U91(proper(X1), proper(X2), proper(X3))proper(U92(X1, X2, X3))U92(proper(X1), proper(X2), proper(X3))
proper(U93(X1, X2, X3))U93(proper(X1), proper(X2), proper(X3))proper(U94(X1, X2))U94(proper(X1), proper(X2))
proper(s(X))s(proper(X))proper(length(X))length(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(X1), ok(X2))ok(U12(X1, X2))
isNatIListKind(ok(X))ok(isNatIListKind(X))U13(ok(X))ok(U13(X))
isNatList(ok(X))ok(isNatList(X))U21(ok(X1), ok(X2))ok(U21(X1, X2))
U22(ok(X1), ok(X2))ok(U22(X1, X2))isNatKind(ok(X))ok(isNatKind(X))
U23(ok(X))ok(U23(X))isNat(ok(X))ok(isNat(X))
U31(ok(X1), ok(X2))ok(U31(X1, X2))U32(ok(X1), ok(X2))ok(U32(X1, X2))
U33(ok(X))ok(U33(X))U41(ok(X1), ok(X2), ok(X3))ok(U41(X1, X2, X3))
U42(ok(X1), ok(X2), ok(X3))ok(U42(X1, X2, X3))U43(ok(X1), ok(X2), ok(X3))ok(U43(X1, X2, X3))
U44(ok(X1), ok(X2), ok(X3))ok(U44(X1, X2, X3))U45(ok(X1), ok(X2))ok(U45(X1, X2))
U46(ok(X))ok(U46(X))isNatIList(ok(X))ok(isNatIList(X))
U51(ok(X1), ok(X2))ok(U51(X1, X2))U52(ok(X))ok(U52(X))
U61(ok(X))ok(U61(X))U71(ok(X))ok(U71(X))
U81(ok(X1), ok(X2), ok(X3))ok(U81(X1, X2, X3))U82(ok(X1), ok(X2), ok(X3))ok(U82(X1, X2, X3))
U83(ok(X1), ok(X2), ok(X3))ok(U83(X1, X2, X3))U84(ok(X1), ok(X2), ok(X3))ok(U84(X1, X2, X3))
U85(ok(X1), ok(X2))ok(U85(X1, X2))U86(ok(X))ok(U86(X))
U91(ok(X1), ok(X2), ok(X3))ok(U91(X1, X2, X3))U92(ok(X1), ok(X2), ok(X3))ok(U92(X1, X2, X3))
U93(ok(X1), ok(X2), ok(X3))ok(U93(X1, X2, X3))U94(ok(X1), ok(X2))ok(U94(X1, X2))
s(ok(X))ok(s(X))length(ok(X))ok(length(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, U94, isNat, U46, U45, U44, U61, U43, U93, U42, U92, U41, U91, length, ok, proper, U23, U21, top, cons, U22, isNatIList, isNatKind, U83, U84, U85, mark, U86, U71, 0, s, U51, isNatList, tt, zeros, U82, U81, U52, U11, active, U12, U13, U31, U32, U33, nil