next up previous
Next: Implication [GS] Up: No Title Previous: No Title

One Point Rule

The One Point Rule is useful for dealing with existential quantifiers. It says that if you have an existentially quantified statement and part of it pins down an exact value for the quantified variable, then you can remove the quantification and replace the variable by the value whereever that variable appears in the rest of the statement.


Note the side condition that you must check before applying this rule: The variable, x, must not be free in the term, t, that you are using in the substitution.

For example, tex2html_wrap_inline557 is equivalent to tex2html_wrap_inline559 . The first conjunct checks that the term is member of the right set; it is usually easy to discharge that check. Then, you are left with just the part of the predicate in which the substitution has been made, e.g., tex2html_wrap_inline561 .

Norman Papernick
Thu Mar 21 14:07:58 EST 1996