  We present a unified rule format for structural operational semantics with
terms as labels that guarantees that the associated labelled transition system
has some bounded-nondeterminism property. The properties we consider include
finite branching, initials finiteness and image finiteness.
