Unless stated otherwise or obvious, throughout the paper newly introduced variables and functions are assumed to cover the range implicit in the context. denotes the binary alphabet , the set of possible bitstrings over , denotes the number of bits in a bitstring ; the -th bit of ; the empty string (where ); if and otherwise (where ). Occasionally it may be convenient to consult Figure 1 below.