		Search-engine friendly clone of the ACL2 documentation.

Well-formedness

Num-val-wfp

A direct numeric value notation is well-formed iff it consists of at least one number; a range numeric value notation is well-formed iff the minimum does not exceed the maximum.

Signature
(num-val-wfp num-val) → yes/no
Arguments: num-val — Guard (num-val-p num-val).
Returns: yes/no — Type (booleanp yes/no).

The condition on direct numeric value notations is required by the rules bin-val, dec-val, and hex-val in [RFC:4]. The condition on range numeric value notations is reasonably justifiable because no number exists in a range whose minimum exceeds the maximum; formally, no tree matches a malformed range numeric value notation.

Definitions and Theorems

Function: num-val-wfp

(defun num-val-wfp (num-val)
  (declare (xargs :guard (num-val-p num-val)))
  (num-val-case num-val
                :direct (consp num-val.get)
                :range (<= num-val.min num-val.max)))

Theorem: booleanp-of-num-val-wfp

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

Theorem: justification-for-num-val-range-wfp

(defthm justification-for-num-val-range-wfp
  (implies (and (num-val-case num-val :range)
                (> (num-val-range->min num-val)
                   (num-val-range->max num-val)))
           (not (tree-match-num-val-p tree num-val))))