(COMMENT generated from Maude module 'LengthOfFiniteLists' by 'complete-noand' transformation)
(VAR L N V1 V2 V Z Y X)
(STRATEGY CONTEXTSENSITIVE

(U11 1)
(U12 1)
(U13 1)
(U21 1)
(U22 1)
(U23 1)
(U31 1)
(U32 1)
(U33 1)
(U41 1)
(U42 1)
(U43 1)
(U44 1)
(U45 1)
(U46 1)
(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)
(cons 1)
(isNat )
(isNatIList )
(isNatIListKind )
(isNatKind )
(isNatList )




)
(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)
)