		Search-engine friendly clone of the ACL2 documentation.

Well-formedness

Rulelist-wfp

A rule list is well-formed iff all its rules are well-formed, there are no duplicate rules, and incremental rules follow non-incremental rules.

Signature
(rulelist-wfp rules) → yes/no
Arguments: rules — Guard (rulelistp rules).
Returns: yes/no — Type (booleanp yes/no).

The first condition is structural. The second condition is justifiable because duplicate rules are redundant. The third condition is reasonably implied by [RFC:3.3].

Non-emptiness is not required by the rule rulelist in [RFC:4], which allows just (*c-wsp c-nl) groups without rules.

Definitions and Theorems

Function: rulelist-wfp

(defun rulelist-wfp (rules)
  (declare (xargs :guard (rulelistp rules)))
  (and (rule-list-wfp rules)
       (no-duplicatesp-equal rules)
       (rulelist-incremental-ok-p rules)))

Theorem: booleanp-of-rulelist-wfp

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