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