		Search-engine friendly clone of the ACL2 documentation.

Hons-sublis

Hons-sublis-aux

Memoized core of hons-sublis.

Definitions and Theorems

Function: hons-sublis-aux

(defun hons-sublis-aux (fal x)
  (declare (xargs :guard t))
  (if (atom x)
      (let ((pair (hons-get x fal)))
        (if pair (cdr pair) x))
    (cons (hons-sublis-aux fal (car x))
          (hons-sublis-aux fal (cdr x)))))

Theorem: hons-sublis-aux-removal

(defthm hons-sublis-aux-removal
  (implies (alistp fal)
           (equal (hons-sublis-aux fal x)
                  (sublis fal x))))

Function: hons-sublis-aux-memoize-condition

(defun hons-sublis-aux-memoize-condition (fal x)
  (declare (ignorable fal x)
           (xargs :guard 't))
  (consp x))