TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (7997ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (21ms), PolynomialLinearRange4iUR (5000ms), DependencyGraph (22ms), PolynomialLinearRange8NegiUR (15000ms), DependencyGraph (22ms), ReductionPairSAT (timeout)].
 | – Problem 3 remains open; application of the following processors failed [SubtermCriterion (2ms), DependencyGraph (2270ms), PolynomialLinearRange4iUR (29ms), DependencyGraph (2222ms), PolynomialLinearRange8NegiUR (20ms), DependencyGraph (2304ms)].

The following open problems remain:



Open Dependency Pair Problem 2

Dependency Pairs

U45#(tt, V2)isNatIList#(activate(V2))U44#(tt, V1, V2)U45#(isNat(activate(V1)), activate(V2))
U42#(tt, V1, V2)U43#(isNatIListKind(activate(V2)), activate(V1), activate(V2))isNatIList#(n__cons(V1, V2))U41#(isNatKind(activate(V1)), activate(V1), activate(V2))
U43#(tt, V1, V2)U44#(isNatIListKind(activate(V2)), activate(V1), activate(V2))U41#(tt, V1, V2)U42#(isNatKind(activate(V1)), activate(V1), activate(V2))

Rewrite Rules

zeroscons(0, n__zeros)U11(tt, V1)U12(isNatIListKind(activate(V1)), activate(V1))
U12(tt, V1)U13(isNatList(activate(V1)))U13(tt)tt
U21(tt, V1)U22(isNatKind(activate(V1)), activate(V1))U22(tt, V1)U23(isNat(activate(V1)))
U23(tt)ttU31(tt, V)U32(isNatIListKind(activate(V)), activate(V))
U32(tt, V)U33(isNatList(activate(V)))U33(tt)tt
U41(tt, V1, V2)U42(isNatKind(activate(V1)), activate(V1), activate(V2))U42(tt, V1, V2)U43(isNatIListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2)U44(isNatIListKind(activate(V2)), activate(V1), activate(V2))U44(tt, V1, V2)U45(isNat(activate(V1)), activate(V2))
U45(tt, V2)U46(isNatIList(activate(V2)))U46(tt)tt
U51(tt, V2)U52(isNatIListKind(activate(V2)))U52(tt)tt
U61(tt)ttU71(tt)tt
U81(tt, V1, V2)U82(isNatKind(activate(V1)), activate(V1), activate(V2))U82(tt, V1, V2)U83(isNatIListKind(activate(V2)), activate(V1), activate(V2))
U83(tt, V1, V2)U84(isNatIListKind(activate(V2)), activate(V1), activate(V2))U84(tt, V1, V2)U85(isNat(activate(V1)), activate(V2))
U85(tt, V2)U86(isNatList(activate(V2)))U86(tt)tt
U91(tt, L, N)U92(isNatIListKind(activate(L)), activate(L), activate(N))U92(tt, L, N)U93(isNat(activate(N)), activate(L), activate(N))
U93(tt, L, N)U94(isNatKind(activate(N)), activate(L))U94(tt, L)s(length(activate(L)))
isNat(n__0)ttisNat(n__length(V1))U11(isNatIListKind(activate(V1)), activate(V1))
isNat(n__s(V1))U21(isNatKind(activate(V1)), activate(V1))isNatIList(V)U31(isNatIListKind(activate(V)), activate(V))
isNatIList(n__zeros)ttisNatIList(n__cons(V1, V2))U41(isNatKind(activate(V1)), activate(V1), activate(V2))
isNatIListKind(n__nil)ttisNatIListKind(n__zeros)tt
isNatIListKind(n__cons(V1, V2))U51(isNatKind(activate(V1)), activate(V2))isNatKind(n__0)tt
isNatKind(n__length(V1))U61(isNatIListKind(activate(V1)))isNatKind(n__s(V1))U71(isNatKind(activate(V1)))
isNatList(n__nil)ttisNatList(n__cons(V1, V2))U81(isNatKind(activate(V1)), activate(V1), activate(V2))
length(nil)0length(cons(N, L))U91(isNatList(activate(L)), activate(L), N)
zerosn__zeros0n__0
length(X)n__length(X)s(X)n__s(X)
cons(X1, X2)n__cons(X1, X2)niln__nil
activate(n__zeros)zerosactivate(n__0)0
activate(n__length(X))length(X)activate(n__s(X))s(X)
activate(n__cons(X1, X2))cons(X1, X2)activate(n__nil)nil
activate(X)X

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, U94, n__s, activate, isNat, U46, U45, U44, n__0, U61, U43, U93, U42, U92, U41, U91, length, n__nil, U23, n__zeros, U21, cons, U22, isNatIList, n__length, isNatKind, U83, U84, U85, U86, U71, n__cons, 0, s, U51, isNatList, tt, zeros, U82, U81, U52, U11, U12, U13, U31, U32, U33, nil




Open Dependency Pair Problem 3

Dependency Pairs

U91#(tt, L, N)activate#(L)U12#(tt, V1)activate#(V1)
U81#(tt, V1, V2)isNatKind#(activate(V1))U83#(tt, V1, V2)activate#(V2)
U83#(tt, V1, V2)activate#(V1)U92#(tt, L, N)U93#(isNat(activate(N)), activate(L), activate(N))
U21#(tt, V1)isNatKind#(activate(V1))U11#(tt, V1)U12#(isNatIListKind(activate(V1)), activate(V1))
U51#(tt, V2)activate#(V2)isNat#(n__length(V1))activate#(V1)
isNat#(n__s(V1))activate#(V1)U94#(tt, L)activate#(L)
U91#(tt, L, N)activate#(N)U91#(tt, L, N)isNatIListKind#(activate(L))
isNatIListKind#(n__cons(V1, V2))activate#(V2)isNatList#(n__cons(V1, V2))activate#(V2)
isNatKind#(n__length(V1))isNatIListKind#(activate(V1))isNatIListKind#(n__cons(V1, V2))isNatKind#(activate(V1))
U84#(tt, V1, V2)activate#(V2)U83#(tt, V1, V2)U84#(isNatIListKind(activate(V2)), activate(V1), activate(V2))
U92#(tt, L, N)activate#(L)U82#(tt, V1, V2)activate#(V1)
length#(cons(N, L))isNatList#(activate(L))U22#(tt, V1)activate#(V1)
U12#(tt, V1)isNatList#(activate(V1))U94#(tt, L)length#(activate(L))
U83#(tt, V1, V2)isNatIListKind#(activate(V2))isNatIListKind#(n__cons(V1, V2))activate#(V1)
isNatKind#(n__s(V1))isNatKind#(activate(V1))U82#(tt, V1, V2)U83#(isNatIListKind(activate(V2)), activate(V1), activate(V2))
isNat#(n__s(V1))U21#(isNatKind(activate(V1)), activate(V1))isNat#(n__s(V1))isNatKind#(activate(V1))
isNatIListKind#(n__cons(V1, V2))U51#(isNatKind(activate(V1)), activate(V2))U82#(tt, V1, V2)isNatIListKind#(activate(V2))
U22#(tt, V1)isNat#(activate(V1))U92#(tt, L, N)activate#(N)
U93#(tt, L, N)activate#(N)isNatKind#(n__length(V1))activate#(V1)
isNatKind#(n__s(V1))activate#(V1)U51#(tt, V2)isNatIListKind#(activate(V2))
isNatList#(n__cons(V1, V2))isNatKind#(activate(V1))U85#(tt, V2)isNatList#(activate(V2))
U81#(tt, V1, V2)U82#(isNatKind(activate(V1)), activate(V1), activate(V2))isNatList#(n__cons(V1, V2))U81#(isNatKind(activate(V1)), activate(V1), activate(V2))
U84#(tt, V1, V2)isNat#(activate(V1))U84#(tt, V1, V2)activate#(V1)
U81#(tt, V1, V2)activate#(V2)U21#(tt, V1)activate#(V1)
U85#(tt, V2)activate#(V2)isNat#(n__length(V1))U11#(isNatIListKind(activate(V1)), activate(V1))
U11#(tt, V1)activate#(V1)U11#(tt, V1)isNatIListKind#(activate(V1))
U84#(tt, V1, V2)U85#(isNat(activate(V1)), activate(V2))activate#(n__length(X))length#(X)
U92#(tt, L, N)isNat#(activate(N))U93#(tt, L, N)isNatKind#(activate(N))
U91#(tt, L, N)U92#(isNatIListKind(activate(L)), activate(L), activate(N))length#(cons(N, L))U91#(isNatList(activate(L)), activate(L), N)
U21#(tt, V1)U22#(isNatKind(activate(V1)), activate(V1))U82#(tt, V1, V2)activate#(V2)
isNatList#(n__cons(V1, V2))activate#(V1)U93#(tt, L, N)activate#(L)
U81#(tt, V1, V2)activate#(V1)isNat#(n__length(V1))isNatIListKind#(activate(V1))
U93#(tt, L, N)U94#(isNatKind(activate(N)), activate(L))length#(cons(N, L))activate#(L)

Rewrite Rules

zeroscons(0, n__zeros)U11(tt, V1)U12(isNatIListKind(activate(V1)), activate(V1))
U12(tt, V1)U13(isNatList(activate(V1)))U13(tt)tt
U21(tt, V1)U22(isNatKind(activate(V1)), activate(V1))U22(tt, V1)U23(isNat(activate(V1)))
U23(tt)ttU31(tt, V)U32(isNatIListKind(activate(V)), activate(V))
U32(tt, V)U33(isNatList(activate(V)))U33(tt)tt
U41(tt, V1, V2)U42(isNatKind(activate(V1)), activate(V1), activate(V2))U42(tt, V1, V2)U43(isNatIListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2)U44(isNatIListKind(activate(V2)), activate(V1), activate(V2))U44(tt, V1, V2)U45(isNat(activate(V1)), activate(V2))
U45(tt, V2)U46(isNatIList(activate(V2)))U46(tt)tt
U51(tt, V2)U52(isNatIListKind(activate(V2)))U52(tt)tt
U61(tt)ttU71(tt)tt
U81(tt, V1, V2)U82(isNatKind(activate(V1)), activate(V1), activate(V2))U82(tt, V1, V2)U83(isNatIListKind(activate(V2)), activate(V1), activate(V2))
U83(tt, V1, V2)U84(isNatIListKind(activate(V2)), activate(V1), activate(V2))U84(tt, V1, V2)U85(isNat(activate(V1)), activate(V2))
U85(tt, V2)U86(isNatList(activate(V2)))U86(tt)tt
U91(tt, L, N)U92(isNatIListKind(activate(L)), activate(L), activate(N))U92(tt, L, N)U93(isNat(activate(N)), activate(L), activate(N))
U93(tt, L, N)U94(isNatKind(activate(N)), activate(L))U94(tt, L)s(length(activate(L)))
isNat(n__0)ttisNat(n__length(V1))U11(isNatIListKind(activate(V1)), activate(V1))
isNat(n__s(V1))U21(isNatKind(activate(V1)), activate(V1))isNatIList(V)U31(isNatIListKind(activate(V)), activate(V))
isNatIList(n__zeros)ttisNatIList(n__cons(V1, V2))U41(isNatKind(activate(V1)), activate(V1), activate(V2))
isNatIListKind(n__nil)ttisNatIListKind(n__zeros)tt
isNatIListKind(n__cons(V1, V2))U51(isNatKind(activate(V1)), activate(V2))isNatKind(n__0)tt
isNatKind(n__length(V1))U61(isNatIListKind(activate(V1)))isNatKind(n__s(V1))U71(isNatKind(activate(V1)))
isNatList(n__nil)ttisNatList(n__cons(V1, V2))U81(isNatKind(activate(V1)), activate(V1), activate(V2))
length(nil)0length(cons(N, L))U91(isNatList(activate(L)), activate(L), N)
zerosn__zeros0n__0
length(X)n__length(X)s(X)n__s(X)
cons(X1, X2)n__cons(X1, X2)niln__nil
activate(n__zeros)zerosactivate(n__0)0
activate(n__length(X))length(X)activate(n__s(X))s(X)
activate(n__cons(X1, X2))cons(X1, X2)activate(n__nil)nil
activate(X)X

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, U94, n__s, activate, isNat, U46, U45, U44, n__0, U61, U43, U93, U42, U92, U41, U91, length, n__nil, U23, n__zeros, U21, cons, U22, isNatIList, n__length, isNatKind, U83, U84, U85, U86, U71, n__cons, 0, s, U51, isNatList, tt, zeros, U82, U81, U52, U11, U12, U13, U31, U32, U33, nil


Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

U91#(tt, L, N)activate#(L)U81#(tt, V1, V2)isNatKind#(activate(V1))
isNatIList#(V)U31#(isNatIListKind(activate(V)), activate(V))U12#(tt, V1)U13#(isNatList(activate(V1)))
U51#(tt, V2)U52#(isNatIListKind(activate(V2)))U83#(tt, V1, V2)activate#(V1)
U92#(tt, L, N)U93#(isNat(activate(N)), activate(L), activate(N))U94#(tt, L)s#(length(activate(L)))
U31#(tt, V)isNatIListKind#(activate(V))U51#(tt, V2)activate#(V2)
isNat#(n__length(V1))activate#(V1)U94#(tt, L)activate#(L)
U91#(tt, L, N)isNatIListKind#(activate(L))isNatIListKind#(n__cons(V1, V2))activate#(V2)
length#(nil)0#U44#(tt, V1, V2)isNat#(activate(V1))
isNatIList#(n__cons(V1, V2))isNatKind#(activate(V1))U92#(tt, L, N)activate#(L)
length#(cons(N, L))isNatList#(activate(L))U82#(tt, V1, V2)activate#(V1)
isNatIList#(n__cons(V1, V2))U41#(isNatKind(activate(V1)), activate(V1), activate(V2))isNatKind#(n__s(V1))isNatKind#(activate(V1))
isNatIListKind#(n__cons(V1, V2))activate#(V1)isNat#(n__s(V1))isNatKind#(activate(V1))
isNatIList#(n__cons(V1, V2))activate#(V2)U82#(tt, V1, V2)isNatIListKind#(activate(V2))
activate#(n__zeros)zeros#U92#(tt, L, N)activate#(N)
isNatKind#(n__length(V1))activate#(V1)U32#(tt, V)isNatList#(activate(V))
isNatKind#(n__s(V1))activate#(V1)isNatList#(n__cons(V1, V2))isNatKind#(activate(V1))
U85#(tt, V2)isNatList#(activate(V2))U31#(tt, V)activate#(V)
U31#(tt, V)U32#(isNatIListKind(activate(V)), activate(V))U32#(tt, V)U33#(isNatList(activate(V)))
zeros#cons#(0, n__zeros)isNatKind#(n__s(V1))U71#(isNatKind(activate(V1)))
U21#(tt, V1)activate#(V1)U81#(tt, V1, V2)activate#(V2)
U32#(tt, V)activate#(V)U11#(tt, V1)activate#(V1)
U41#(tt, V1, V2)activate#(V2)U11#(tt, V1)isNatIListKind#(activate(V1))
U43#(tt, V1, V2)activate#(V2)U93#(tt, L, N)isNatKind#(activate(N))
length#(cons(N, L))U91#(isNatList(activate(L)), activate(L), N)U21#(tt, V1)U22#(isNatKind(activate(V1)), activate(V1))
U44#(tt, V1, V2)activate#(V2)isNatList#(n__cons(V1, V2))activate#(V1)
U82#(tt, V1, V2)activate#(V2)U81#(tt, V1, V2)activate#(V1)
isNat#(n__length(V1))isNatIListKind#(activate(V1))U43#(tt, V1, V2)U44#(isNatIListKind(activate(V2)), activate(V1), activate(V2))
U42#(tt, V1, V2)isNatIListKind#(activate(V2))U12#(tt, V1)activate#(V1)
U83#(tt, V1, V2)activate#(V2)zeros#0#
U21#(tt, V1)isNatKind#(activate(V1))U45#(tt, V2)activate#(V2)
U45#(tt, V2)isNatIList#(activate(V2))U11#(tt, V1)U12#(isNatIListKind(activate(V1)), activate(V1))
U44#(tt, V1, V2)U45#(isNat(activate(V1)), activate(V2))U44#(tt, V1, V2)activate#(V1)
U41#(tt, V1, V2)isNatKind#(activate(V1))U91#(tt, L, N)activate#(N)
isNat#(n__s(V1))activate#(V1)isNatList#(n__cons(V1, V2))activate#(V2)
isNatIList#(V)isNatIListKind#(activate(V))isNatKind#(n__length(V1))isNatIListKind#(activate(V1))
isNatIListKind#(n__cons(V1, V2))isNatKind#(activate(V1))U42#(tt, V1, V2)activate#(V1)
U84#(tt, V1, V2)activate#(V2)U83#(tt, V1, V2)U84#(isNatIListKind(activate(V2)), activate(V1), activate(V2))
U42#(tt, V1, V2)U43#(isNatIListKind(activate(V2)), activate(V1), activate(V2))U41#(tt, V1, V2)activate#(V1)
isNatKind#(n__length(V1))U61#(isNatIListKind(activate(V1)))U42#(tt, V1, V2)activate#(V2)
U85#(tt, V2)U86#(isNatList(activate(V2)))activate#(n__0)0#
U22#(tt, V1)activate#(V1)U12#(tt, V1)isNatList#(activate(V1))
U83#(tt, V1, V2)isNatIListKind#(activate(V2))U94#(tt, L)length#(activate(L))
U82#(tt, V1, V2)U83#(isNatIListKind(activate(V2)), activate(V1), activate(V2))isNat#(n__s(V1))U21#(isNatKind(activate(V1)), activate(V1))
U22#(tt, V1)U23#(isNat(activate(V1)))isNatIListKind#(n__cons(V1, V2))U51#(isNatKind(activate(V1)), activate(V2))
U22#(tt, V1)isNat#(activate(V1))U45#(tt, V2)U46#(isNatIList(activate(V2)))
U93#(tt, L, N)activate#(N)U51#(tt, V2)isNatIListKind#(activate(V2))
isNatList#(n__cons(V1, V2))U81#(isNatKind(activate(V1)), activate(V1), activate(V2))U81#(tt, V1, V2)U82#(isNatKind(activate(V1)), activate(V1), activate(V2))
U84#(tt, V1, V2)isNat#(activate(V1))isNatIList#(V)activate#(V)
U84#(tt, V1, V2)activate#(V1)activate#(n__cons(X1, X2))cons#(X1, X2)
U41#(tt, V1, V2)U42#(isNatKind(activate(V1)), activate(V1), activate(V2))U85#(tt, V2)activate#(V2)
isNat#(n__length(V1))U11#(isNatIListKind(activate(V1)), activate(V1))U43#(tt, V1, V2)activate#(V1)
activate#(n__s(X))s#(X)U84#(tt, V1, V2)U85#(isNat(activate(V1)), activate(V2))
activate#(n__length(X))length#(X)activate#(n__nil)nil#
U92#(tt, L, N)isNat#(activate(N))U43#(tt, V1, V2)isNatIListKind#(activate(V2))
U91#(tt, L, N)U92#(isNatIListKind(activate(L)), activate(L), activate(N))U93#(tt, L, N)activate#(L)
U93#(tt, L, N)U94#(isNatKind(activate(N)), activate(L))isNatIList#(n__cons(V1, V2))activate#(V1)
length#(cons(N, L))activate#(L)

Rewrite Rules

zeroscons(0, n__zeros)U11(tt, V1)U12(isNatIListKind(activate(V1)), activate(V1))
U12(tt, V1)U13(isNatList(activate(V1)))U13(tt)tt
U21(tt, V1)U22(isNatKind(activate(V1)), activate(V1))U22(tt, V1)U23(isNat(activate(V1)))
U23(tt)ttU31(tt, V)U32(isNatIListKind(activate(V)), activate(V))
U32(tt, V)U33(isNatList(activate(V)))U33(tt)tt
U41(tt, V1, V2)U42(isNatKind(activate(V1)), activate(V1), activate(V2))U42(tt, V1, V2)U43(isNatIListKind(activate(V2)), activate(V1), activate(V2))
U43(tt, V1, V2)U44(isNatIListKind(activate(V2)), activate(V1), activate(V2))U44(tt, V1, V2)U45(isNat(activate(V1)), activate(V2))
U45(tt, V2)U46(isNatIList(activate(V2)))U46(tt)tt
U51(tt, V2)U52(isNatIListKind(activate(V2)))U52(tt)tt
U61(tt)ttU71(tt)tt
U81(tt, V1, V2)U82(isNatKind(activate(V1)), activate(V1), activate(V2))U82(tt, V1, V2)U83(isNatIListKind(activate(V2)), activate(V1), activate(V2))
U83(tt, V1, V2)U84(isNatIListKind(activate(V2)), activate(V1), activate(V2))U84(tt, V1, V2)U85(isNat(activate(V1)), activate(V2))
U85(tt, V2)U86(isNatList(activate(V2)))U86(tt)tt
U91(tt, L, N)U92(isNatIListKind(activate(L)), activate(L), activate(N))U92(tt, L, N)U93(isNat(activate(N)), activate(L), activate(N))
U93(tt, L, N)U94(isNatKind(activate(N)), activate(L))U94(tt, L)s(length(activate(L)))
isNat(n__0)ttisNat(n__length(V1))U11(isNatIListKind(activate(V1)), activate(V1))
isNat(n__s(V1))U21(isNatKind(activate(V1)), activate(V1))isNatIList(V)U31(isNatIListKind(activate(V)), activate(V))
isNatIList(n__zeros)ttisNatIList(n__cons(V1, V2))U41(isNatKind(activate(V1)), activate(V1), activate(V2))
isNatIListKind(n__nil)ttisNatIListKind(n__zeros)tt
isNatIListKind(n__cons(V1, V2))U51(isNatKind(activate(V1)), activate(V2))isNatKind(n__0)tt
isNatKind(n__length(V1))U61(isNatIListKind(activate(V1)))isNatKind(n__s(V1))U71(isNatKind(activate(V1)))
isNatList(n__nil)ttisNatList(n__cons(V1, V2))U81(isNatKind(activate(V1)), activate(V1), activate(V2))
length(nil)0length(cons(N, L))U91(isNatList(activate(L)), activate(L), N)
zerosn__zeros0n__0
length(X)n__length(X)s(X)n__s(X)
cons(X1, X2)n__cons(X1, X2)niln__nil
activate(n__zeros)zerosactivate(n__0)0
activate(n__length(X))length(X)activate(n__s(X))s(X)
activate(n__cons(X1, X2))cons(X1, X2)activate(n__nil)nil
activate(X)X

Original Signature

Termination of terms over the following signature is verified: isNatIListKind, U94, U46, isNat, activate, n__s, U45, U44, U43, U61, n__0, U42, U93, U92, U41, U91, length, n__nil, U23, n__zeros, U21, cons, U22, isNatIList, n__length, isNatKind, U83, U84, U85, U86, U71, n__cons, 0, isNatList, U51, s, zeros, tt, U82, U52, U81, U11, U12, U31, U13, U32, U33, nil

Strategy


The following SCCs where found

U45#(tt, V2) → isNatIList#(activate(V2))U44#(tt, V1, V2) → U45#(isNat(activate(V1)), activate(V2))
U42#(tt, V1, V2) → U43#(isNatIListKind(activate(V2)), activate(V1), activate(V2))isNatIList#(n__cons(V1, V2)) → U41#(isNatKind(activate(V1)), activate(V1), activate(V2))
U43#(tt, V1, V2) → U44#(isNatIListKind(activate(V2)), activate(V1), activate(V2))U41#(tt, V1, V2) → U42#(isNatKind(activate(V1)), activate(V1), activate(V2))

U91#(tt, L, N) → activate#(L)U81#(tt, V1, V2) → isNatKind#(activate(V1))
U12#(tt, V1) → activate#(V1)U83#(tt, V1, V2) → activate#(V2)
U83#(tt, V1, V2) → activate#(V1)U92#(tt, L, N) → U93#(isNat(activate(N)), activate(L), activate(N))
U21#(tt, V1) → isNatKind#(activate(V1))U11#(tt, V1) → U12#(isNatIListKind(activate(V1)), activate(V1))
U51#(tt, V2) → activate#(V2)U91#(tt, L, N) → isNatIListKind#(activate(L))
U91#(tt, L, N) → activate#(N)U94#(tt, L) → activate#(L)
isNat#(n__s(V1)) → activate#(V1)isNat#(n__length(V1)) → activate#(V1)
isNatIListKind#(n__cons(V1, V2)) → activate#(V2)isNatKind#(n__length(V1)) → isNatIListKind#(activate(V1))
isNatList#(n__cons(V1, V2)) → activate#(V2)isNatIListKind#(n__cons(V1, V2)) → isNatKind#(activate(V1))
U84#(tt, V1, V2) → activate#(V2)U83#(tt, V1, V2) → U84#(isNatIListKind(activate(V2)), activate(V1), activate(V2))
U92#(tt, L, N) → activate#(L)length#(cons(N, L)) → isNatList#(activate(L))
U82#(tt, V1, V2) → activate#(V1)U22#(tt, V1) → activate#(V1)
U12#(tt, V1) → isNatList#(activate(V1))U83#(tt, V1, V2) → isNatIListKind#(activate(V2))
U94#(tt, L) → length#(activate(L))isNatKind#(n__s(V1)) → isNatKind#(activate(V1))
isNatIListKind#(n__cons(V1, V2)) → activate#(V1)isNat#(n__s(V1)) → U21#(isNatKind(activate(V1)), activate(V1))
U82#(tt, V1, V2) → U83#(isNatIListKind(activate(V2)), activate(V1), activate(V2))isNat#(n__s(V1)) → isNatKind#(activate(V1))
isNatIListKind#(n__cons(V1, V2)) → U51#(isNatKind(activate(V1)), activate(V2))U82#(tt, V1, V2) → isNatIListKind#(activate(V2))
U22#(tt, V1) → isNat#(activate(V1))U92#(tt, L, N) → activate#(N)
isNatKind#(n__length(V1)) → activate#(V1)U93#(tt, L, N) → activate#(N)
isNatKind#(n__s(V1)) → activate#(V1)U51#(tt, V2) → isNatIListKind#(activate(V2))
isNatList#(n__cons(V1, V2)) → isNatKind#(activate(V1))U85#(tt, V2) → isNatList#(activate(V2))
isNatList#(n__cons(V1, V2)) → U81#(isNatKind(activate(V1)), activate(V1), activate(V2))U81#(tt, V1, V2) → U82#(isNatKind(activate(V1)), activate(V1), activate(V2))
U84#(tt, V1, V2) → isNat#(activate(V1))U84#(tt, V1, V2) → activate#(V1)
U21#(tt, V1) → activate#(V1)U81#(tt, V1, V2) → activate#(V2)
U85#(tt, V2) → activate#(V2)U11#(tt, V1) → activate#(V1)
isNat#(n__length(V1)) → U11#(isNatIListKind(activate(V1)), activate(V1))U11#(tt, V1) → isNatIListKind#(activate(V1))
activate#(n__length(X)) → length#(X)U84#(tt, V1, V2) → U85#(isNat(activate(V1)), activate(V2))
U92#(tt, L, N) → isNat#(activate(N))U93#(tt, L, N) → isNatKind#(activate(N))
length#(cons(N, L)) → U91#(isNatList(activate(L)), activate(L), N)U91#(tt, L, N) → U92#(isNatIListKind(activate(L)), activate(L), activate(N))
U21#(tt, V1) → U22#(isNatKind(activate(V1)), activate(V1))isNatList#(n__cons(V1, V2)) → activate#(V1)
U82#(tt, V1, V2) → activate#(V2)U81#(tt, V1, V2) → activate#(V1)
U93#(tt, L, N) → activate#(L)isNat#(n__length(V1)) → isNatIListKind#(activate(V1))
U93#(tt, L, N) → U94#(isNatKind(activate(N)), activate(L))length#(cons(N, L)) → activate#(L)