		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)