Set of numeric ranges in a rule list.
(rulelist-num-ranges rules) → ranges
This is the union of the sets of numeric ranges from all the rules that form the list.
Function:
(defun rulelist-num-ranges (rules) (declare (xargs :guard (rulelistp rules))) (let ((__function__ 'rulelist-num-ranges)) (declare (ignorable __function__)) (cond ((endp rules) nil) (t (union (rule-num-ranges (car rules)) (rulelist-num-ranges (cdr rules)))))))
Theorem:
(defthm num-range-setp-of-rulelist-num-ranges (b* ((ranges (rulelist-num-ranges rules))) (num-range-setp ranges)) :rule-classes :rewrite)
Theorem:
(defthm rulelist-num-ranges-of-rulelist-fix-rules (equal (rulelist-num-ranges (rulelist-fix rules)) (rulelist-num-ranges rules)))
Theorem:
(defthm rulelist-num-ranges-rulelist-equiv-congruence-on-rules (implies (rulelist-equiv rules rules-equiv) (equal (rulelist-num-ranges rules) (rulelist-num-ranges rules-equiv))) :rule-classes :congruence)