Ultrafilters on words for a fragment of logic

We give a method for specifying ultrafilter equations and identify their projections on the set of profinite words. Let BB be the set of languages captured by first-order sentences using unary predicates for each letter, arbitrary uniform unary numerical predicates and a predicate for the length of a word. We illustrate our methods by giving ultrafilter equations characterising BB and then projecting these to obtain profinite equations characterising B∩RegB∩Reg. This suffices to establish the decidability of the membership problem for B∩RegB∩Reg.