		Search-engine friendly clone of the ACL2 documentation.

Aig-substitution

Aig-restrict-list

(aig-restrict-list x sigma) substitutes into a list of AIGs.

Signature
(aig-restrict-list x sigma) → aig-list
Arguments: x — List of AIGs.; sigma — Fast alist binding variables to replacement AIGs, as in aig-restrict.

Definitions and Theorems

Function: aig-restrict-list

(defun aig-restrict-list (x sigma)
  (declare (xargs :guard t))
  (let ((__function__ 'aig-restrict-list))
    (declare (ignorable __function__))
    (mbe :logic
         (if (atom x)
             nil
           (cons (aig-restrict (car x) sigma)
                 (aig-restrict-list (cdr x) sigma)))
         :exec (aig-restrict-list-acc x sigma nil))))