		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 common case of equality constraints.

Definitions and Theorems

Theorem: constraint-satp-of-equal

(defthm constraint-satp-of-equal
        (implies (and (assignment-for-prime-p asg p)
                      (constraint-case constr :equal))
                 (b* ((left (constraint-equal->left constr))
                      (right (constraint-equal->right constr)))
                     (iff (constraint-satp asg constr defs p)
                          (and (equal (eval-expr asg left p)
                                      (eval-expr asg right p))
                               (eval-expr asg left p))))))