The Equivalent and Implies commands test the Boolean expressions a and b for logical equivalence or logical implication respectively.

The Equivalent(a, b) calling sequence returns true in the event that the two expressions are logically equivalent, and false if they are not.  Similarly, Implies(a, b) returns true if a implies b (that is, if for every valuation for which a is true, then b is also true) and false otherwise.

If the parameter p is supplied and the test returns false, then a valuation is assigned to p which demonstrates a negative result.  Otherwise, p is assigned NULL.

Note: The test may be significantly faster if p is not given.