		Search-engine friendly clone of the ACL2 documentation.

Proof-support

Exec-proof-tree-when-constraint-equal

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.

Definitions and Theorems

Theorem: exec-proof-tree-when-constraint-equal

(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))))))))