		Search-engine friendly clone of the ACL2 documentation.

Proof-support

Constraint-satp-of-equal

Proof rule for equality constraints.

This says that the satisfaction of an equality constraint reduces to the two expressions being equal and non-erroneous.

This rule lets us dispense with the existentially quantified proof tree for the case of equality constraints.

Definitions and Theorems

Theorem: constraint-satp-of-equal

(defthm constraint-satp-of-equal
 (implies
      (and (assignment-wfp asg p)
           (constraint-case constr :equal))
      (equal (constraint-satp constr defs asg p)
             (constraint-equal-satp (constraint-equal->left constr)
                                    (constraint-equal->right constr)
                                    asg p))))