1This document occasionally uses the notation F∕N when referring to predicates and functions. When this notation is used, it refers to the predicate or function that is called F , which has N arguments.