		Search-engine friendly clone of the ACL2 documentation.

Semantics-deeply-embedded

Constraint-list-satp

Semantic function saying if an assignment satisfies a list of constraints, given a list of definitions and a prime field.

This is similar to constraint-satp, but for lists of constraints.

Definitions and Theorems

Theorem: constraint-list-satp-suff

(defthm constraint-list-satp-suff
 (implies
    (and (proof-tree-listp ptrees)
         (equal (exec-proof-tree-list ptrees defs p)
                (proof-list-outcome-assertions
                     (assertion-list-from (repeat (len constrs) asg)
                                          constrs))))
    (constraint-list-satp constrs defs asg p)))

Theorem: booleanp-of-constraint-list-satp

(defthm booleanp-of-constraint-list-satp
  (b* ((yes/no (constraint-list-satp constrs defs asg p)))
    (booleanp yes/no))
  :rule-classes :rewrite)