(COMMENT generated from Maude module 'LengthOfFiniteLists' by 'nokinds' transformation) (VAR L N V1 V2 V X Z Y) (STRATEGY CONTEXTSENSITIVE (U11 1) (and 1) (cons 1) (isNat ) (isNatIList ) (isNatList ) ) (RULES zeros -> cons(0,zeros) U11(tt,L) -> s(length(L)) and(tt,X) -> X isNat(0) -> tt isNat(length(V1)) -> isNatList(V1) isNat(s(V1)) -> isNat(V1) isNatIList(V) -> isNatList(V) isNatIList(zeros) -> tt isNatIList(cons(V1,V2)) -> and(isNat(V1),isNatIList(V2)) isNatList(nil) -> tt isNatList(cons(V1,V2)) -> and(isNat(V1),isNatList(V2)) length(nil) -> 0 length(cons(N,L)) -> U11(and(isNatList(L),isNat(N)),L) )