		Search-engine friendly clone of the ACL2 documentation.

Sexpr-rewriting-internals

4v-sexpr-compose-nofal

Identical to 4v-sexpr-compose, but not memoized and does not use fast alist lookups.

Used for rewriting because the terms and alists involved are small. This is called on the RHS of a rewrite rule, which is a small term in common usage; with an alist that may have large terms in its range, but only has a few variables bound. Therefore, it is appropriate to forego memoization and fast alist lookups, since the overhead will outweigh the benefit.

Definitions and Theorems

Function: 4v-sexpr-compose-nofal

(defun 4v-sexpr-compose-nofal (x al)
  (declare (xargs :guard t))
  (if (atom x)
      (and x
           (let ((look (hons-assoc-equal x al)))
             (and look (cdr look))))
    (hons (car x)
          (4v-sexpr-compose-nofal-list (cdr x)
                                       al))))

Function: 4v-sexpr-compose-nofal-list

(defun 4v-sexpr-compose-nofal-list (x al)
  (declare (xargs :guard t))
  (if (atom x)
      x
    (hons (4v-sexpr-compose-nofal (car x) al)
          (4v-sexpr-compose-nofal-list (cdr x)
                                       al))))

Theorem: 4v-sexpr-compose-nofal-is-4v-sexpr-compose

(defthm 4v-sexpr-compose-nofal-is-4v-sexpr-compose
  (equal (4v-sexpr-compose-nofal x al)
         (4v-sexpr-compose x al)))

Theorem: 4v-sexpr-compose-nofal-list-is-4v-sexpr-compose-list

(defthm 4v-sexpr-compose-nofal-list-is-4v-sexpr-compose-list
  (equal (4v-sexpr-compose-nofal-list x al)
         (4v-sexpr-compose-list x al)))