(VAR L N) (RULES zeros -> cons(0) U11(tt) -> U12(tt) U12(tt) -> s(length(L)) length(nil) -> 0 length(cons(N)) -> U11(tt) )