		Search-engine friendly clone of the ACL2 documentation.

Proof-support

Constraint-satp-to-definition-satp

Proof rule to turn relation constraint satisfaction to definition satisfaction.

This is useful for compostional reasoning, as mentioned in proof-support.

Definitions and Theorems

Theorem: constraint-satp-to-definition-satp

(defthm constraint-satp-to-definition-satp
 (implies
  (and
     (primep p)
     (assignmentp asg)
     (assignment-wfp asg p)
     (constraint-case constr :relation)
     (no-duplicatesp-equal
          (definition->para
               (lookup-definition (constraint-relation->name constr)
                                  defs))))
  (b* ((vals (eval-expr-list (constraint-relation->args constr)
                             asg p)))
    (implies
         (not (reserrp vals))
         (equal (constraint-satp constr defs asg p)
                (definition-satp (constraint-relation->name constr)
                                 defs vals p))))))