		Search-engine friendly clone of the ACL2 documentation.

Semantics

Tree-match-num-val-p

Semantics of numeric value notations.

Signature
(tree-match-num-val-p tree num-val) → yes/no
Arguments: tree — Guard (treep tree).; num-val — Guard (num-val-p num-val).
Returns: yes/no — Type (booleanp yes/no).

A tree matches a numeric value notation iff one of the following conditions holds:

The numeric value notation is a list of natural numbers, and the tree is a leaf consisting of exactly that list of natural numbers.
The numeric value notation is a range of natural numbers, and the tree is a leaf consisting of one natural number in that range. (Note that no tree matches a range whose minimum exceeds the maximum.)

Definitions and Theorems

Function: tree-match-num-val-p

(defun tree-match-num-val-p (tree num-val)
  (declare (xargs :guard (and (treep tree) (num-val-p num-val))))
  (and (tree-case tree :leafterm)
       (let ((nats (tree-leafterm->get tree)))
         (num-val-case num-val
                       :direct (equal nats num-val.get)
                       :range (and (= (len nats) 1)
                                   (<= num-val.min (car nats))
                                   (<= (car nats) num-val.max))))))

Theorem: booleanp-of-tree-match-num-val-p

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

Theorem: tree-match-num-val-p-of-tree-fix-tree

(defthm tree-match-num-val-p-of-tree-fix-tree
  (equal (tree-match-num-val-p (tree-fix tree)
                               num-val)
         (tree-match-num-val-p tree num-val)))

Theorem: tree-match-num-val-p-tree-equiv-congruence-on-tree

(defthm tree-match-num-val-p-tree-equiv-congruence-on-tree
  (implies (tree-equiv tree tree-equiv)
           (equal (tree-match-num-val-p tree num-val)
                  (tree-match-num-val-p tree-equiv num-val)))
  :rule-classes :congruence)

Theorem: tree-match-num-val-p-of-num-val-fix-num-val

(defthm tree-match-num-val-p-of-num-val-fix-num-val
  (equal (tree-match-num-val-p tree (num-val-fix num-val))
         (tree-match-num-val-p tree num-val)))

Theorem: tree-match-num-val-p-num-val-equiv-congruence-on-num-val

(defthm tree-match-num-val-p-num-val-equiv-congruence-on-num-val
  (implies (num-val-equiv num-val num-val-equiv)
           (equal (tree-match-num-val-p tree num-val)
                  (tree-match-num-val-p tree num-val-equiv)))
  :rule-classes :congruence)