|
|
|---|
|
|
|
|---|
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.
Theorem:
(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))))