This section gives details of the internal workings of the graph rewriting formula processor. It covers the definition of bounding regions, the input to the formula parser, then how the formula parser builds a graph that represents the formula and parses it.