3 Programs for Mechanical Program Verification D. C. Cooper

If the original formula included this function, we must also allow for its negation. This can either be eliminated or the following formula complicated to allow for this situation. However, in our examples this negation cannot appear and so we do not include it.