Satisfaction of a relation constraint without free variables, expressed without proof trees.
(constraint-relation-nofreevars-satp name args defs asg p) → 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.
Function:
(defun constraint-relation-nofreevars-satp (name args defs asg p) (declare (xargs :guard (and (stringp 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:
(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)