		Search-engine friendly clone of the ACL2 documentation.

Well-formedness

System-wfp

Check if a system is well-formed.

Signature
(system-wfp sys) → yes/no
Arguments: sys — Guard (systemp sys).
Returns: yes/no — Type (booleanp yes/no).

The list of definitions must be well-formed, and the list of constraints must be well-formed with respect to the list of definitions.

Definitions and Theorems

Function: system-wfp

(defun system-wfp (sys)
  (declare (xargs :guard (systemp sys)))
  (let ((__function__ 'system-wfp))
    (declare (ignorable __function__))
    (b* (((system sys) sys))
      (and (definition-list-wfp sys.definitions)
           (constraint-list-wfp sys.constraints sys.definitions)))))

Theorem: booleanp-of-system-wfp

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

Theorem: system-wfp-of-system-fix-sys

(defthm system-wfp-of-system-fix-sys
  (equal (system-wfp (system-fix sys))
         (system-wfp sys)))

Theorem: system-wfp-system-equiv-congruence-on-sys

(defthm system-wfp-system-equiv-congruence-on-sys
  (implies (system-equiv sys sys-equiv)
           (equal (system-wfp sys)
                  (system-wfp sys-equiv)))
  :rule-classes :congruence)