		Search-engine friendly clone of the ACL2 documentation.

Numeric-range-retrieval

Rule-num-ranges

Set of numeric ranges in a rule.

Signature
(rule-num-ranges rule) → ranges
Arguments: rule — Guard (rulep rule).
Returns: ranges — Type (num-range-setp ranges).

This is the set of numeric ranges in the alternation that defines the rules.

Definitions and Theorems

Function: rule-num-ranges

(defun rule-num-ranges (rule)
  (declare (xargs :guard (rulep rule)))
  (let ((__function__ 'rule-num-ranges))
    (declare (ignorable __function__))
    (alternation-num-ranges (rule->definiens rule))))

Theorem: num-range-setp-of-rule-num-ranges

(defthm num-range-setp-of-rule-num-ranges
  (b* ((ranges (rule-num-ranges rule)))
    (num-range-setp ranges))
  :rule-classes :rewrite)

Theorem: rule-num-ranges-of-rule-fix-rule

(defthm rule-num-ranges-of-rule-fix-rule
  (equal (rule-num-ranges (rule-fix rule))
         (rule-num-ranges rule)))

Theorem: rule-num-ranges-rule-equiv-congruence-on-rule

(defthm rule-num-ranges-rule-equiv-congruence-on-rule
  (implies (rule-equiv rule rule-equiv)
           (equal (rule-num-ranges rule)
                  (rule-num-ranges rule-equiv)))
  :rule-classes :congruence)