		Search-engine friendly clone of the ACL2 documentation.

Semantics-deeply-embedded

System-satp

Check if an assignment satisfies a system.

Signature
(system-satp sys asg p) → yes/no
Arguments: sys — Guard (systemp sys).; asg — Guard (assignmentp asg).; p — Guard (primep p).
Returns: yes/no — Type (booleanp yes/no).

All the constraints in the system must be satisfied, in the context of the definitions in the system.

Definitions and Theorems

Function: system-satp

(defun system-satp (sys asg p)
  (declare (xargs :guard (and (systemp sys)
                              (assignmentp asg)
                              (primep p))))
  (declare (xargs :guard (assignment-wfp asg p)))
  (let ((__function__ 'system-satp))
    (declare (ignorable __function__))
    (constraint-list-satp (system->constraints sys)
                          (system->definitions sys)
                          asg p)))

Theorem: booleanp-of-system-satp

(defthm booleanp-of-system-satp
  (b* ((yes/no (system-satp sys asg p)))
    (booleanp yes/no))
  :rule-classes :rewrite)