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