Rabin conditions are a general class of properties of infinite sequences that encompass most known automata-theoretic acceptance conditions and notions of fairness. In this paper, we introduce a concept, called a Rabin measure, which in a precise sense expresses progress for each transition toward satisfaction of the Rabin condition.

We show that these measures of progress are linked to the Kleene-Brouwer ordering of recursion theory. This property is used in [Kla94a(JPL)] to establish an exponential upper bound for the complementation of automata on infinite trees.

When applied to termination problems under fairness constraints, Rabin measures eliminate the need for syntax-dependent, recursive applications of proof rules.