(COMMENT generated from Maude module 'LengthOfFiniteLists' by 'nokinds-noand' transformation) (VAR L N V1 V2 V Z Y X) (STRATEGY CONTEXTSENSITIVE (U11 1) (U21 1) (U31 1) (U41 1) (U42 1) (U51 1) (U52 1) (U61 1) (U62 1) (cons 1) (isNat ) (isNatIList ) (isNatList ) ) (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) )