(VAR L N V V1 V2 X )
(STRATEGY CONTEXTSENSITIVE
        (zeros ) 
        (cons 1) 
        (0 ) 
        (U11 1) 
        (tt ) 
        (s 1) 
        (length 1) 
        (and 1) 
        (isNat ) 
        (isNatList ) 
        (isNatIList ) 
        (nil ) 
)
(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)
        
)