		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.