(VAR V1 V V2 L N)
(STRATEGY CONTEXTSENSITIVE 
  (zeros)
  (cons 1)
  (0)
  (U11 1)
  (tt)
  (U12 1)
  (isNatIListKind)
  (U13 1)
  (isNatList)
  (U21 1)
  (U22 1)
  (isNatKind)
  (U23 1)
  (isNat)
  (U31 1)
  (U32 1)
  (U33 1)
  (U41 1)
  (U42 1)
  (U43 1)
  (U44 1)
  (U45 1)
  (U46 1)
  (isNatIList)
  (U51 1)
  (U52 1)
  (U61 1)
  (U71 1)
  (U81 1)
  (U82 1)
  (U83 1)
  (U84 1)
  (U85 1)
  (U86 1)
  (U91 1)
  (U92 1)
  (U93 1)
  (U94 1)
  (s 1)
  (length 1)
  (nil)
)
(RULES 
zeros -> cons(0,zeros)
U11(tt,V1) -> U12(isNatIListKind(V1),V1)
U12(tt,V1) -> U13(isNatList(V1))
U13(tt) -> tt
U21(tt,V1) -> U22(isNatKind(V1),V1)
U22(tt,V1) -> U23(isNat(V1))
U23(tt) -> tt
U31(tt,V) -> U32(isNatIListKind(V),V)
U32(tt,V) -> U33(isNatList(V))
U33(tt) -> tt
U41(tt,V1,V2) -> U42(isNatKind(V1),V1,V2)
U42(tt,V1,V2) -> U43(isNatIListKind(V2),V1,V2)
U43(tt,V1,V2) -> U44(isNatIListKind(V2),V1,V2)
U44(tt,V1,V2) -> U45(isNat(V1),V2)
U45(tt,V2) -> U46(isNatIList(V2))
U46(tt) -> tt
U51(tt,V2) -> U52(isNatIListKind(V2))
U52(tt) -> tt
U61(tt) -> tt
U71(tt) -> tt
U81(tt,V1,V2) -> U82(isNatKind(V1),V1,V2)
U82(tt,V1,V2) -> U83(isNatIListKind(V2),V1,V2)
U83(tt,V1,V2) -> U84(isNatIListKind(V2),V1,V2)
U84(tt,V1,V2) -> U85(isNat(V1),V2)
U85(tt,V2) -> U86(isNatList(V2))
U86(tt) -> tt
U91(tt,L,N) -> U92(isNatIListKind(L),L,N)
U92(tt,L,N) -> U93(isNat(N),L,N)
U93(tt,L,N) -> U94(isNatKind(N),L)
U94(tt,L) -> s(length(L))
isNat(0) -> tt
isNat(length(V1)) -> U11(isNatIListKind(V1),V1)
isNat(s(V1)) -> U21(isNatKind(V1),V1)
isNatIList(V) -> U31(isNatIListKind(V),V)
isNatIList(zeros) -> tt
isNatIList(cons(V1,V2)) -> U41(isNatKind(V1),V1,V2)
isNatIListKind(nil) -> tt
isNatIListKind(zeros) -> tt
isNatIListKind(cons(V1,V2)) -> U51(isNatKind(V1),V2)
isNatKind(0) -> tt
isNatKind(length(V1)) -> U61(isNatIListKind(V1))
isNatKind(s(V1)) -> U71(isNatKind(V1))
isNatList(nil) -> tt
isNatList(cons(V1,V2)) -> U81(isNatKind(V1),V1,V2)
length(nil) -> 0
length(cons(N,L)) -> U91(isNatList(L),L,N)
)

Proving termination of context-sensitive rewriting for LengthOfFiniteLists_complete_noand:

-> Dependency pairs:
nF_U11(tt,V1) -> nF_U12(isNatIListKind(V1),V1)
nF_U11(tt,V1) -> nF_isNatIListKind(V1)
nF_U12(tt,V1) -> nF_U13(isNatList(V1))
nF_U12(tt,V1) -> nF_isNatList(V1)
nF_U21(tt,V1) -> nF_U22(isNatKind(V1),V1)
nF_U21(tt,V1) -> nF_isNatKind(V1)
nF_U22(tt,V1) -> nF_U23(isNat(V1))
nF_U22(tt,V1) -> nF_isNat(V1)
nF_U31(tt,V) -> nF_U32(isNatIListKind(V),V)
nF_U31(tt,V) -> nF_isNatIListKind(V)
nF_U32(tt,V) -> nF_U33(isNatList(V))
nF_U32(tt,V) -> nF_isNatList(V)
nF_U41(tt,V1,V2) -> nF_U42(isNatKind(V1),V1,V2)
nF_U41(tt,V1,V2) -> nF_isNatKind(V1)
nF_U42(tt,V1,V2) -> nF_U43(isNatIListKind(V2),V1,V2)
nF_U42(tt,V1,V2) -> nF_isNatIListKind(V2)
nF_U43(tt,V1,V2) -> nF_U44(isNatIListKind(V2),V1,V2)
nF_U43(tt,V1,V2) -> nF_isNatIListKind(V2)
nF_U44(tt,V1,V2) -> nF_U45(isNat(V1),V2)
nF_U44(tt,V1,V2) -> nF_isNat(V1)
nF_U45(tt,V2) -> nF_U46(isNatIList(V2))
nF_U45(tt,V2) -> nF_isNatIList(V2)
nF_U51(tt,V2) -> nF_U52(isNatIListKind(V2))
nF_U51(tt,V2) -> nF_isNatIListKind(V2)
nF_U81(tt,V1,V2) -> nF_U82(isNatKind(V1),V1,V2)
nF_U81(tt,V1,V2) -> nF_isNatKind(V1)
nF_U82(tt,V1,V2) -> nF_U83(isNatIListKind(V2),V1,V2)
nF_U82(tt,V1,V2) -> nF_isNatIListKind(V2)
nF_U83(tt,V1,V2) -> nF_U84(isNatIListKind(V2),V1,V2)
nF_U83(tt,V1,V2) -> nF_isNatIListKind(V2)
nF_U84(tt,V1,V2) -> nF_U85(isNat(V1),V2)
nF_U84(tt,V1,V2) -> nF_isNat(V1)
nF_U85(tt,V2) -> nF_U86(isNatList(V2))
nF_U85(tt,V2) -> nF_isNatList(V2)
nF_U91(tt,L,N) -> nF_U92(isNatIListKind(L),L,N)
nF_U91(tt,L,N) -> nF_isNatIListKind(L)
nF_U92(tt,L,N) -> nF_U93(isNat(N),L,N)
nF_U92(tt,L,N) -> nF_isNat(N)
nF_U93(tt,L,N) -> nF_U94(isNatKind(N),L)
nF_U93(tt,L,N) -> nF_isNatKind(N)
nF_U94(tt,L) -> nF_length(L)
nF_U94(tt,L) -> L
nF_isNat(length(V1)) -> nF_U11(isNatIListKind(V1),V1)
nF_isNat(length(V1)) -> nF_isNatIListKind(V1)
nF_isNat(s(V1)) -> nF_U21(isNatKind(V1),V1)
nF_isNat(s(V1)) -> nF_isNatKind(V1)
nF_isNatIList(V) -> nF_U31(isNatIListKind(V),V)
nF_isNatIList(V) -> nF_isNatIListKind(V)
nF_isNatIList(cons(V1,V2)) -> nF_U41(isNatKind(V1),V1,V2)
nF_isNatIList(cons(V1,V2)) -> nF_isNatKind(V1)
nF_isNatIListKind(cons(V1,V2)) -> nF_U51(isNatKind(V1),V2)
nF_isNatIListKind(cons(V1,V2)) -> nF_isNatKind(V1)
nF_isNatKind(length(V1)) -> nF_U61(isNatIListKind(V1))
nF_isNatKind(length(V1)) -> nF_isNatIListKind(V1)
nF_isNatKind(s(V1)) -> nF_U71(isNatKind(V1))
nF_isNatKind(s(V1)) -> nF_isNatKind(V1)
nF_isNatList(cons(V1,V2)) -> nF_U81(isNatKind(V1),V1,V2)
nF_isNatList(cons(V1,V2)) -> nF_isNatKind(V1)
nF_length(cons(N,L)) -> nF_U91(isNatList(L),L,N)
nF_length(cons(N,L)) -> nF_isNatList(L)

-> Proof of termination for LengthOfFiniteLists_complete_noand_1_1:
-> -> Dependency pairs in cycle:
nF_U91(tt,L,N) -> nF_U92(isNatIListKind(L),L,N)
nF_length(cons(N,L)) -> nF_U91(isNatList(L),L,N)
nF_U94(tt,L) -> nF_length(L)
nF_U93(tt,L,N) -> nF_U94(isNatKind(N),L)
nF_U92(tt,L,N) -> nF_U93(isNat(N),L,N)

Usable Rules:
zeros -> cons(0,zeros)
U11(tt,V1) -> U12(isNatIListKind(V1),V1)
U12(tt,V1) -> U13(isNatList(V1))
U13(tt) -> tt
U21(tt,V1) -> U22(isNatKind(V1),V1)
U22(tt,V1) -> U23(isNat(V1))
U23(tt) -> tt
U51(tt,V2) -> U52(isNatIListKind(V2))
U52(tt) -> tt
U61(tt) -> tt
U71(tt) -> tt
U81(tt,V1,V2) -> U82(isNatKind(V1),V1,V2)
U82(tt,V1,V2) -> U83(isNatIListKind(V2),V1,V2)
U83(tt,V1,V2) -> U84(isNatIListKind(V2),V1,V2)
U84(tt,V1,V2) -> U85(isNat(V1),V2)
U85(tt,V2) -> U86(isNatList(V2))
U86(tt) -> tt
U91(tt,L,N) -> U92(isNatIListKind(L),L,N)
U92(tt,L,N) -> U93(isNat(N),L,N)
U93(tt,L,N) -> U94(isNatKind(N),L)
U94(tt,L) -> s(length(L))
isNat(0) -> tt
isNat(length(V1)) -> U11(isNatIListKind(V1),V1)
isNat(s(V1)) -> U21(isNatKind(V1),V1)
isNatIListKind(nil) -> tt
isNatIListKind(zeros) -> tt
isNatIListKind(cons(V1,V2)) -> U51(isNatKind(V1),V2)
isNatKind(0) -> tt
isNatKind(length(V1)) -> U61(isNatIListKind(V1))
isNatKind(s(V1)) -> U71(isNatKind(V1))
isNatList(nil) -> tt
isNatList(cons(V1,V2)) -> U81(isNatKind(V1),V1,V2)
length(nil) -> 0
length(cons(N,L)) -> U91(isNatList(L),L,N)

Polynomial Interpretation:

[zeros] = 0
[cons](X1,X2) = X1.X2 + X2
[0] = 1
[U11](X1,X2) = X2
[tt] = 1
[U12](X1,X2) = X1.X2
[isNatIListKind](X) = 1
[U13](X) = X
[isNatList](X) = X
[U21](X1,X2) = 1
[U22](X1,X2) = 1
[isNatKind](X) = X.X
[U23](X) = 1
[isNat](X) = X
[U31](X1,X2) = 0
[U32](X1,X2) = 0
[U33](X) = 0
[U41](X1,X2,X3) = 0
[U42](X1,X2,X3) = 0
[U43](X1,X2,X3) = 0
[U44](X1,X2,X3) = 0
[U45](X1,X2) = 0
[U46](X) = 0
[isNatIList](X) = 0
[U51](X1,X2) = 1
[U52](X) = 1
[U61](X) = X.X
[U71](X) = 1
[U81](X1,X2,X3) = X2.X3
[U82](X1,X2,X3) = X2.X3
[U83](X1,X2,X3) = X1.X2.X3
[U84](X1,X2,X3) = X1.X2.X3
[U85](X1,X2) = X1.X2
[U86](X) = X
[U91](X1,X2,X3) = X1.X2.X3 + X1.X2 + X1.X3 + 1
[U92](X1,X2,X3) = X1.X2.X3 + X1 + X3
[U93](X1,X2,X3) = X1.X2 + X1
[U94](X1,X2) = 1
[s](X) = 1
[length](X) = X.X + X + 1
[nil] = 1
[nF_U91](X1,X2,X3) = X2.X3 + X1
[nF_length](X) = X
[nF_U94](X1,X2) = X2
[nF_U93](X1,X2,X3) = X1.X2
[nF_U92](X1,X2,X3) = X1.X2.X3 + 1

TIME: 0.176771


-> Proof of termination for LengthOfFiniteLists_complete_noand_1_2:
-> -> Dependency pairs in cycle:
nF_U41(tt,V1,V2) -> nF_U42(isNatKind(V1),V1,V2)
nF_isNatIList(cons(V1,V2)) -> nF_U41(isNatKind(V1),V1,V2)
nF_U45(tt,V2) -> nF_isNatIList(V2)
nF_U44(tt,V1,V2) -> nF_U45(isNat(V1),V2)
nF_U43(tt,V1,V2) -> nF_U44(isNatIListKind(V2),V1,V2)
nF_U42(tt,V1,V2) -> nF_U43(isNatIListKind(V2),V1,V2)


Polynomial Interpretation:

[cons](X1,X2) = X2 + 1

TIME: 1.4442e-2

Termination proved: There exists a projection such that there are no minimal mu-rewrite sequences in cycle.

-> Proof of termination for LengthOfFiniteLists_complete_noand_1_3:
-> -> Dependency pairs in cycle:
nF_U11(tt,V1) -> nF_U12(isNatIListKind(V1),V1)
nF_isNat(length(V1)) -> nF_U11(isNatIListKind(V1),V1)
nF_U84(tt,V1,V2) -> nF_isNat(V1)
nF_U83(tt,V1,V2) -> nF_U84(isNatIListKind(V2),V1,V2)
nF_U82(tt,V1,V2) -> nF_U83(isNatIListKind(V2),V1,V2)
nF_U81(tt,V1,V2) -> nF_U82(isNatKind(V1),V1,V2)
nF_isNatList(cons(V1,V2)) -> nF_U81(isNatKind(V1),V1,V2)
nF_U85(tt,V2) -> nF_isNatList(V2)
nF_U84(tt,V1,V2) -> nF_U85(isNat(V1),V2)
nF_U12(tt,V1) -> nF_isNatList(V1)
nF_U22(tt,V1) -> nF_isNat(V1)
nF_U21(tt,V1) -> nF_U22(isNatKind(V1),V1)
nF_isNat(s(V1)) -> nF_U21(isNatKind(V1),V1)

Usable Rules:
U11(tt,V1) -> U12(isNatIListKind(V1),V1)
U12(tt,V1) -> U13(isNatList(V1))
U13(tt) -> tt
U21(tt,V1) -> U22(isNatKind(V1),V1)
U22(tt,V1) -> U23(isNat(V1))
U23(tt) -> tt
U51(tt,V2) -> U52(isNatIListKind(V2))
U52(tt) -> tt
U61(tt) -> tt
U71(tt) -> tt
U81(tt,V1,V2) -> U82(isNatKind(V1),V1,V2)
U82(tt,V1,V2) -> U83(isNatIListKind(V2),V1,V2)
U83(tt,V1,V2) -> U84(isNatIListKind(V2),V1,V2)
U84(tt,V1,V2) -> U85(isNat(V1),V2)
U85(tt,V2) -> U86(isNatList(V2))
U86(tt) -> tt
isNat(0) -> tt
isNat(length(V1)) -> U11(isNatIListKind(V1),V1)
isNat(s(V1)) -> U21(isNatKind(V1),V1)
isNatIListKind(nil) -> tt
isNatIListKind(zeros) -> tt
isNatIListKind(cons(V1,V2)) -> U51(isNatKind(V1),V2)
isNatKind(0) -> tt
isNatKind(length(V1)) -> U61(isNatIListKind(V1))
isNatKind(s(V1)) -> U71(isNatKind(V1))
isNatList(nil) -> tt
isNatList(cons(V1,V2)) -> U81(isNatKind(V1),V1,V2)

Polynomial Interpretation:

[zeros] = 1
[cons](X1,X2) = X1.X2 + X2 + 1
[0] = 1
[U11](X1,X2) = 1
[tt] = 1
[U12](X1,X2) = 1
[isNatIListKind](X) = X
[U13](X) = 1
[isNatList](X) = X.X
[U21](X1,X2) = X2
[U22](X1,X2) = X2
[isNatKind](X) = X.X
[U23](X) = X
[isNat](X) = X
[U31](X1,X2) = 0
[U32](X1,X2) = 0
[U33](X) = 0
[U41](X1,X2,X3) = 0
[U42](X1,X2,X3) = 0
[U43](X1,X2,X3) = 0
[U44](X1,X2,X3) = 0
[U45](X1,X2) = 0
[U46](X) = 0
[isNatIList](X) = 0
[U51](X1,X2) = X2
[U52](X) = X
[U61](X) = 1
[U71](X) = X
[U81](X1,X2,X3) = X2.X3 + X3
[U82](X1,X2,X3) = X2.X3 + X3
[U83](X1,X2,X3) = X2.X3 + X3
[U84](X1,X2,X3) = X1.X2 + X1
[U85](X1,X2) = X1
[U86](X) = 1
[U91](X1,X2,X3) = 0
[U92](X1,X2,X3) = 0
[U93](X1,X2,X3) = 0
[U94](X1,X2) = 0
[s](X) = X + 1
[length](X) = X.X + 1
[nil] = 1
[nF_U11](X1,X2) = X1.X2
[nF_isNat](X) = X
[nF_U84](X1,X2,X3) = X2 + X3
[nF_U83](X1,X2,X3) = X1.X2 + X3
[nF_U82](X1,X2,X3) = X2.X3 + X3
[nF_U81](X1,X2,X3) = X2.X3 + X3
[nF_isNatList](X) = X
[nF_U85](X1,X2) = X2
[nF_U12](X1,X2) = X2
[nF_U22](X1,X2) = X2
[nF_U21](X1,X2) = X2

TIME: 0.13818299999999994

-> -> Dependency pairs in cycle:
nF_U11(tt,V1) -> nF_U12(isNatIListKind(V1),V1)
nF_isNat(length(V1)) -> nF_U11(isNatIListKind(V1),V1)
nF_U84(tt,V1,V2) -> nF_isNat(V1)
nF_U83(tt,V1,V2) -> nF_U84(isNatIListKind(V2),V1,V2)
nF_U82(tt,V1,V2) -> nF_U83(isNatIListKind(V2),V1,V2)
nF_U81(tt,V1,V2) -> nF_U82(isNatKind(V1),V1,V2)
nF_isNatList(cons(V1,V2)) -> nF_U81(isNatKind(V1),V1,V2)
nF_U12(tt,V1) -> nF_isNatList(V1)
nF_U85(tt,V2) -> nF_isNatList(V2)
nF_U84(tt,V1,V2) -> nF_U85(isNat(V1),V2)

Usable Rules:
U11(tt,V1) -> U12(isNatIListKind(V1),V1)
U12(tt,V1) -> U13(isNatList(V1))
U13(tt) -> tt
U21(tt,V1) -> U22(isNatKind(V1),V1)
U22(tt,V1) -> U23(isNat(V1))
U23(tt) -> tt
U51(tt,V2) -> U52(isNatIListKind(V2))
U52(tt) -> tt
U61(tt) -> tt
U71(tt) -> tt
U81(tt,V1,V2) -> U82(isNatKind(V1),V1,V2)
U82(tt,V1,V2) -> U83(isNatIListKind(V2),V1,V2)
U83(tt,V1,V2) -> U84(isNatIListKind(V2),V1,V2)
U84(tt,V1,V2) -> U85(isNat(V1),V2)
U85(tt,V2) -> U86(isNatList(V2))
U86(tt) -> tt
isNat(0) -> tt
isNat(length(V1)) -> U11(isNatIListKind(V1),V1)
isNat(s(V1)) -> U21(isNatKind(V1),V1)
isNatIListKind(nil) -> tt
isNatIListKind(zeros) -> tt
isNatIListKind(cons(V1,V2)) -> U51(isNatKind(V1),V2)
isNatKind(0) -> tt
isNatKind(length(V1)) -> U61(isNatIListKind(V1))
isNatKind(s(V1)) -> U71(isNatKind(V1))
isNatList(nil) -> tt
isNatList(cons(V1,V2)) -> U81(isNatKind(V1),V1,V2)

Polynomial Interpretation:

[zeros] = 1
[cons](X1,X2) = X1.X2 + X1 + X2 + 1
[0] = 1
[U11](X1,X2) = X1.X2 + X1
[tt] = 1
[U12](X1,X2) = 1
[isNatIListKind](X) = X.X
[U13](X) = 1
[isNatList](X) = X.X
[U21](X1,X2) = X1.X2 + X1
[U22](X1,X2) = 1
[isNatKind](X) = X.X
[U23](X) = 1
[isNat](X) = X.X
[U31](X1,X2) = 0
[U32](X1,X2) = 0
[U33](X) = 0
[U41](X1,X2,X3) = 0
[U42](X1,X2,X3) = 0
[U43](X1,X2,X3) = 0
[U44](X1,X2,X3) = 0
[U45](X1,X2) = 0
[U46](X) = 0
[isNatIList](X) = 0
[U51](X1,X2) = X1
[U52](X) = 1
[U61](X) = X.X
[U71](X) = X.X
[U81](X1,X2,X3) = X1.X3 + X1
[U82](X1,X2,X3) = 1
[U83](X1,X2,X3) = 1
[U84](X1,X2,X3) = 1
[U85](X1,X2) = 1
[U86](X) = 1
[U91](X1,X2,X3) = 0
[U92](X1,X2,X3) = 0
[U93](X1,X2,X3) = 0
[U94](X1,X2) = 0
[s](X) = X.X + X + 1
[length](X) = X.X + X + 1
[nil] = 1
[nF_U11](X1,X2) = X1 + X2
[nF_isNat](X) = X
[nF_U84](X1,X2,X3) = X2 + X3 + 1
[nF_U83](X1,X2,X3) = X2 + X3 + 1
[nF_U82](X1,X2,X3) = X2 + X3 + 1
[nF_U81](X1,X2,X3) = X2 + X3 + 1
[nF_isNatList](X) = X
[nF_U12](X1,X2) = X2
[nF_U85](X1,X2) = X2

TIME: 0.142676

-> -> Dependency pairs in cycle:
nF_U11(tt,V1) -> nF_U12(isNatIListKind(V1),V1)
nF_isNat(length(V1)) -> nF_U11(isNatIListKind(V1),V1)
nF_U84(tt,V1,V2) -> nF_isNat(V1)
nF_U83(tt,V1,V2) -> nF_U84(isNatIListKind(V2),V1,V2)
nF_U82(tt,V1,V2) -> nF_U83(isNatIListKind(V2),V1,V2)
nF_U81(tt,V1,V2) -> nF_U82(isNatKind(V1),V1,V2)
nF_isNatList(cons(V1,V2)) -> nF_U81(isNatKind(V1),V1,V2)
nF_U12(tt,V1) -> nF_isNatList(V1)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for LengthOfFiniteLists_complete_noand_1_4:
-> -> Dependency pairs in cycle:
nF_isNatKind(s(V1)) -> nF_isNatKind(V1)
nF_isNatIListKind(cons(V1,V2)) -> nF_isNatKind(V1)
nF_isNatKind(length(V1)) -> nF_isNatIListKind(V1)
nF_U51(tt,V2) -> nF_isNatIListKind(V2)
nF_isNatIListKind(cons(V1,V2)) -> nF_U51(isNatKind(V1),V2)


Polynomial Interpretation:

[s](X) = X
[cons](X1,X2) = X1 + X2 + 1
[length](X) = X

TIME: 1.4135e-2

Termination proved: There exists a projection such that there are no minimal mu-rewrite sequences in cycle.
-> -> Dependency pairs in cycle:
nF_isNatKind(s(V1)) -> nF_isNatKind(V1)
nF_isNatIListKind(cons(V1,V2)) -> nF_isNatKind(V1)
nF_isNatKind(length(V1)) -> nF_isNatIListKind(V1)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in CSDG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Simple mixed
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.