		Search-engine friendly clone of the ACL2 documentation.

Proof-support

Constraint-relation-nofreevars-satp

Satisfaction of a relation constraint without free variables, expressed without proof trees.

Signature
(constraint-relation-nofreevars-satp name args defs asg p) → yes/no
Arguments: name — Guard (namep name).; args — Guard (expression-listp args).; defs — Guard (definition-listp defs).; asg — Guard (assignmentp asg).; p — Guard (primep p).
Returns: yes/no — Type (booleanp yes/no).

This is a specialized version of constraint-relation-satp, applicable when the definition of the relation has no free variables. In this case, we can avoid the existential quantification.

Definitions and Theorems

Function: constraint-relation-nofreevars-satp

(defun constraint-relation-nofreevars-satp (name args defs asg p)
 (declare (xargs :guard (and (namep name)
                             (expression-listp args)
                             (definition-listp defs)
                             (assignmentp asg)
                             (primep p))))
 (declare (xargs :guard (assignment-wfp asg p)))
 (let ((__function__ 'constraint-relation-nofreevars-satp))
  (declare (ignorable __function__))
  (b* ((def (lookup-definition name defs)))
   (and
    def (emptyp (definition-free-vars def))
    (b* (((definition def) def))
     (and
       (equal (len args) (len def.para))
       (b* ((vals (eval-expr-list args asg p)))
         (and (nat-listp vals)
              (b* ((asg-para-vals (omap::from-lists def.para vals)))
                (constraint-list-satp
                     def.body defs asg-para-vals p))))))))))

Theorem: booleanp-of-constraint-relation-nofreevars-satp

(defthm booleanp-of-constraint-relation-nofreevars-satp
 (b*
  ((yes/no
        (constraint-relation-nofreevars-satp name args defs asg p)))
  (booleanp yes/no))
 :rule-classes :rewrite)