(VAR L N X )
(RULES 
        and(tt) -> X
        length(cons(N)) -> s(length(L))
        zeros -> cons(0)
        length(nil) -> 0
        
)