		Search-engine friendly clone of the ACL2 documentation.

Well-formedness

Repeat-range-wfp

A repetition range is well-formed iff the minimum does not exceed the maximum.

Signature
(repeat-range-wfp range) → yes/no
Arguments: range — Guard (repeat-rangep range).
Returns: yes/no — Type (booleanp yes/no).

This condition is reasonably justifiable because no number of repetitions exists in a range whose minimum exceeds the maximum.

Definitions and Theorems

Function: repeat-range-wfp

(defun repeat-range-wfp (range)
  (declare (xargs :guard (repeat-rangep range)))
  (b* ((min (repeat-range->min range))
       (max (repeat-range->max range)))
    (or (nati-case max :infinity)
        (<= min (nati-finite->get max)))))

Theorem: booleanp-of-repeat-range-wfp

(defthm booleanp-of-repeat-range-wfp
  (b* ((yes/no (repeat-range-wfp range)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: justification-for-repeat-range-wfp

(defthm justification-for-repeat-range-wfp
  (implies (and (nati-case (repeat-range->max range)
                           :finite)
                (> (repeat-range->min range)
                   (nati-finite->get (repeat-range->max range))))
           (not (numrep-match-repeat-range-p numrep range))))