(VAR V2 L N V1 V)
(STRATEGY CONTEXTSENSITIVE 
  (zeros)
  (cons 1)
  (0)
  (U11 1)
  (tt)
  (U21 1)
  (U31 1)
  (U41 1)
  (U42 1)
  (isNatIList)
  (U51 1)
  (U52 1)
  (isNatList)
  (U61 1)
  (U62 1)
  (isNat)
  (s 1)
  (length 1)
  (nil)
)
(RULES 
zeros -> cons(0,zeros)
U11(tt) -> tt
U21(tt) -> tt
U31(tt) -> tt
U41(tt,V2) -> U42(isNatIList(V2))
U42(tt) -> tt
U51(tt,V2) -> U52(isNatList(V2))
U52(tt) -> tt
U61(tt,L,N) -> U62(isNat(N),L)
U62(tt,L) -> s(length(L))
isNat(0) -> tt
isNat(length(V1)) -> U11(isNatList(V1))
isNat(s(V1)) -> U21(isNat(V1))
isNatIList(V) -> U31(isNatList(V))
isNatIList(zeros) -> tt
isNatIList(cons(V1,V2)) -> U41(isNat(V1),V2)
isNatList(nil) -> tt
isNatList(cons(V1,V2)) -> U51(isNat(V1),V2)
length(nil) -> 0
length(cons(N,L)) -> U61(isNatList(L),L,N)
)

Proving termination of context-sensitive rewriting for LengthOfFiniteLists_nokinds_noand:

-> Dependency pairs:
nF_U41(tt,V2) -> nF_U42(isNatIList(V2))
nF_U41(tt,V2) -> nF_isNatIList(V2)
nF_U51(tt,V2) -> nF_U52(isNatList(V2))
nF_U51(tt,V2) -> nF_isNatList(V2)
nF_U61(tt,L,N) -> nF_U62(isNat(N),L)
nF_U61(tt,L,N) -> nF_isNat(N)
nF_U62(tt,L) -> nF_length(L)
nF_U62(tt,L) -> L
nF_isNat(length(V1)) -> nF_U11(isNatList(V1))
nF_isNat(length(V1)) -> nF_isNatList(V1)
nF_isNat(s(V1)) -> nF_U21(isNat(V1))
nF_isNat(s(V1)) -> nF_isNat(V1)
nF_isNatIList(V) -> nF_U31(isNatList(V))
nF_isNatIList(V) -> nF_isNatList(V)
nF_isNatIList(cons(V1,V2)) -> nF_U41(isNat(V1),V2)
nF_isNatIList(cons(V1,V2)) -> nF_isNat(V1)
nF_isNatList(cons(V1,V2)) -> nF_U51(isNat(V1),V2)
nF_isNatList(cons(V1,V2)) -> nF_isNat(V1)
nF_length(cons(N,L)) -> nF_U61(isNatList(L),L,N)
nF_length(cons(N,L)) -> nF_isNatList(L)

-> Proof of termination for LengthOfFiniteLists_nokinds_noand_1_1:
-> -> Dependency pairs in cycle:
nF_U61(tt,L,N) -> nF_U62(isNat(N),L)
nF_length(cons(N,L)) -> nF_U61(isNatList(L),L,N)
nF_U62(tt,L) -> nF_length(L)

Usable Rules:
zeros -> cons(0,zeros)
U11(tt) -> tt
U21(tt) -> tt
U51(tt,V2) -> U52(isNatList(V2))
U52(tt) -> tt
U61(tt,L,N) -> U62(isNat(N),L)
U62(tt,L) -> s(length(L))
isNat(0) -> tt
isNat(length(V1)) -> U11(isNatList(V1))
isNat(s(V1)) -> U21(isNat(V1))
isNatList(nil) -> tt
isNatList(cons(V1,V2)) -> U51(isNat(V1),V2)
length(nil) -> 0
length(cons(N,L)) -> U61(isNatList(L),L,N)

Polynomial Interpretation:

[zeros] = 0
[cons](X1,X2) = X1.X2 + X2
[0] = 1
[U11](X) = 1
[tt] = 1
[U21](X) = X.X
[U31](X) = 0
[U41](X1,X2) = 0
[U42](X) = 0
[isNatIList](X) = 0
[U51](X1,X2) = X2
[U52](X) = X
[isNatList](X) = X
[U61](X1,X2,X3) = 1
[U62](X1,X2) = 1
[isNat](X) = X
[s](X) = X.X
[length](X) = 1
[nil] = 1
[nF_U61](X1,X2,X3) = X2.X3 + X1
[nF_length](X) = X
[nF_U62](X1,X2) = X1.X2 + 1

TIME: 0.18188


-> Proof of termination for LengthOfFiniteLists_nokinds_noand_1_2:
-> -> Dependency pairs in cycle:
nF_U41(tt,V2) -> nF_isNatIList(V2)
nF_isNatIList(cons(V1,V2)) -> nF_U41(isNat(V1),V2)


Polynomial Interpretation:

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

TIME: 7.4074e-2

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

-> Proof of termination for LengthOfFiniteLists_nokinds_noand_1_3:
-> -> Dependency pairs in cycle:
nF_isNat(s(V1)) -> nF_isNat(V1)
nF_isNatList(cons(V1,V2)) -> nF_isNat(V1)
nF_isNat(length(V1)) -> nF_isNatList(V1)
nF_U51(tt,V2) -> nF_isNatList(V2)
nF_isNatList(cons(V1,V2)) -> nF_U51(isNat(V1),V2)


Polynomial Interpretation:

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

TIME: 1.5492e-2

Termination proved: There exists a projection such that there are no minimal mu-rewrite sequences in cycle.
-> -> Dependency pairs in cycle:
nF_isNat(s(V1)) -> nF_isNat(V1)
nF_isNatList(cons(V1,V2)) -> nF_isNat(V1)
nF_isNat(length(V1)) -> nF_isNatList(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.