Check if incremental rules appear after non-incremental rules with the same names.
An incremental rule may appear only if there is a preceding rule with the same name. A non-incremental rule may appear only if there is no preceding rule with the same name.
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)
Function:
(defun rulelist-incremental-ok-p (rules) (declare (xargs :guard (rulelistp rules))) (rulelist-incremental-ok-p-aux nil rules))
Theorem:
(defthm booleanp-of-rulelist-incremental-ok-p (b* ((yes/no (rulelist-incremental-ok-p rules))) (booleanp yes/no)) :rule-classes :rewrite)