		Search-engine friendly clone of the ACL2 documentation.

Rulelist-incremental-ok-p

Rulelist-incremental-ok-p-aux

Auxiliary function to define rulelist-incremental-ok-p.

Signature
(rulelist-incremental-ok-p-aux previous-rules next-rules) → yes/no
Arguments: previous-rules — Guard (rulelistp previous-rules).; next-rules — Guard (rulelistp next-rules).
Returns: yes/no — Type (booleanp yes/no).

The rules in next-rules are examined one after the other, and checked against the rules already examined, which are accumulated in previous-rules.

Definitions and Theorems

Function: rulelist-incremental-ok-p-aux

(defun rulelist-incremental-ok-p-aux (previous-rules next-rules)
  (declare (xargs :guard (and (rulelistp previous-rules)
                              (rulelistp next-rules))))
  (or (endp next-rules)
      (and (iff (rule->incremental (car next-rules))
                (lookup-rulename (rule->name (car next-rules))
                                 previous-rules))
           (rulelist-incremental-ok-p-aux
                (append previous-rules (list (car next-rules)))
                (cdr next-rules)))))

Theorem: booleanp-of-rulelist-incremental-ok-p-aux

(defthm booleanp-of-rulelist-incremental-ok-p-aux
  (b*
   ((yes/no
         (rulelist-incremental-ok-p-aux previous-rules next-rules)))
   (booleanp yes/no))
  :rule-classes :rewrite)