(VAR IL L M N )
(RULES 
        U72(tt) -> s(length(L))
        U93(tt) -> cons(N)
        zeros -> cons(0)
        U11(tt) -> tt
        U21(tt) -> tt
        U31(tt) -> tt
        U41(tt) -> U42(isNatIList)
        U42(tt) -> tt
        U51(tt) -> U52(isNatList)
        U52(tt) -> tt
        U61(tt) -> U62(isNatIList)
        U62(tt) -> tt
        U71(tt) -> U72(isNat)
        U81(tt) -> nil
        U91(tt) -> U92(isNat)
        U92(tt) -> U93(isNat)
        isNat -> tt
        isNat -> U11(isNatList)
        isNat -> U21(isNat)
        isNatIList -> U31(isNatList)
        isNatIList -> tt
        isNatIList -> U41(isNat)
        isNatList -> tt
        isNatList -> U51(isNat)
        isNatList -> U61(isNat)
        length(nil) -> 0
        length(cons(N)) -> U71(isNatList)
        take(0, IL) -> U81(isNatIList)
        take(s(M), cons(N)) -> U91(isNatIList)
        
)