...
The final phase converts an expression in (not necessarily reduced or normalized) If form to an equivalent expression constructed from variables and { true, false, And, Or, Not, Implies, If. This process eliminates every expression of the form
...