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.Function:
(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:
(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:
(defthm 4v-sexpr-compose-nofal-is-4v-sexpr-compose (equal (4v-sexpr-compose-nofal x al) (4v-sexpr-compose x al)))
Theorem:
(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)))