		Search-engine friendly clone of the ACL2 documentation.

Proof-support

Constraint-equal-satp

Satisfaction of an equality constraint, expressed without proof trees.

Signature
(constraint-equal-satp left right asg p) → yes/no
Arguments: left — Guard (expressionp left).; right — Guard (expressionp right).; asg — Guard (assignmentp asg).; p — Guard (primep p).
Returns: yes/no — Type (booleanp yes/no).

This is an alternative definition of constraint-satp for the case in which the constrains is an equality. We prove in constraint-satp-of-equal its equivalence to constraint-satp.

This is a simpler definition, because it does not directly involve the execution of proof trees. It says that the equality is satisfied exactly when the two expressions are equal and non-erroneous.

Definitions and Theorems

Function: constraint-equal-satp

(defun constraint-equal-satp (left right asg p)
  (declare (xargs :guard (and (expressionp left)
                              (expressionp right)
                              (assignmentp asg)
                              (primep p))))
  (declare (xargs :guard (assignment-wfp asg p)))
  (let ((__function__ 'constraint-equal-satp))
    (declare (ignorable __function__))
    (and (natp (eval-expr left asg p))
         (equal (eval-expr left asg p)
                (eval-expr right asg p)))))

Theorem: booleanp-of-constraint-equal-satp

(defthm booleanp-of-constraint-equal-satp
  (b* ((yes/no (constraint-equal-satp left right asg p)))
    (booleanp yes/no))
  :rule-classes :rewrite)