		Search-engine friendly clone of the ACL2 documentation.

Aig-substitution

Aig-restrict-alist

(aig-restrict-alist x sigma) substitutes into an AIG Alist (an alist binding keys to AIGs).

Signature
(aig-restrict-alist x sigma) → aig-alist
Arguments: x — Alist binding names to AIGs. This doesn't need to be a fast alist.; sigma — Fast alist binding variables to replacement AIGs, as in aig-restrict.
Returns: aig-alist — Ordinary (slow) alist with the same keys as x, and values formed by restricting each aig with aig-restrict.

Definitions and Theorems

Function: aig-restrict-alist

(defun aig-restrict-alist (x sigma)
       (declare (xargs :guard t))
       (let ((__function__ 'aig-restrict-alist))
            (declare (ignorable __function__))
            (cond ((atom x) nil)
                  ((atom (car x))
                   (aig-restrict-alist (cdr x) sigma))
                  (t (cons (cons (caar x)
                                 (aig-restrict (cdar x) sigma))
                           (aig-restrict-alist (cdr x) sigma))))))

Theorem: alistp-of-aig-restrict-alist

(defthm alistp-of-aig-restrict-alist
        (alistp (aig-restrict-alist x sigma)))

Subtopics

Aig-restrict-alist-thms: Basic theorems about aig-restrict-alist.