(VAR L N X IL M)
(RULES 
zeros -> cons(0)
U11(tt) -> s(length(L))
U21(tt) -> nil
U31(tt) -> cons(N)
and(tt) -> X
isNat -> tt
isNat -> isNatList
isNat -> isNat
isNatIList -> isNatList
isNatIList -> tt
isNatIList -> and(isNat)
isNatList -> tt
isNatList -> and(isNat)
isNatList -> and(isNat)
length(nil) -> 0
length(cons(N)) -> U11(and(isNatList))
take(0,IL) -> U21(isNatIList)
take(s(M),cons(N)) -> U31(and(isNatIList))
)