Characterization of a proof tree for an equality constraint.
If running a proof tree is successful and returns an assertion for an equality constraint, then the proof tree must be one for an equality, and its components (assignment and expressions) must coincide with the ones from the assertion.
This is used to prove constraint-satp-of-equal.
Theorem:
(defthm exec-proof-tree-when-constraint-equal (b* ((outcome (exec-proof-tree ptree defs p))) (implies (proof-outcome-case outcome :assertion) (b* ((asser (proof-outcome-assertion->get outcome)) (asg (assertion->asg asser)) (constr (assertion->constr asser))) (implies (constraint-case constr :equal) (and (proof-tree-case ptree :equal) (equal (proof-tree-equal->asg ptree) asg) (equal (proof-tree-equal->left ptree) (constraint-equal->left constr)) (equal (proof-tree-equal->right ptree) (constraint-equal->right constr)) (equal (eval-expr (constraint-equal->left constr) asg p) (eval-expr (constraint-equal->right constr) asg p)) (natp (eval-expr (constraint-equal->left constr) asg p))))))))