		Search-engine friendly clone of the ACL2 documentation.

Faig

Faig-compose

(faig-compose x sigma) performs variable substitution throughout the FAIG x, unconditionally replacing every variable in x with its binding in sigma.

Signature
(faig-compose x sigma) → *

See aig-compose; the sigma should be a fast alist and you will want to clear the memoize table for aig-compose when you are done using the env.

Definitions and Theorems

Function: faig-compose

(defun faig-compose (x sigma)
  (declare (xargs :guard t))
  (let ((__function__ 'faig-compose))
    (declare (ignorable __function__))
    (if (atom x)
        '(t . t)
      (cons (aig-compose (car x) sigma)
            (aig-compose (cdr x) sigma)))))

Subtopics

Faig-compose-thms: Basic theorems about faig-compose.