Auxiliary function to define rulelist-incremental-ok-p.
The rules in
Function:
(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:
(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)