		Search-engine friendly clone of the ACL2 documentation.

Aig-semantics

Aig-eval-list

(aig-eval-list x env) evaluates a list of AIGs.

Signature
(aig-eval-list x env) → vals
Arguments: x — The AIG list to evaluate.; env — The environment to use; see aig-eval.
Returns: vals — A list of Boolean values; the evaluations of each AIG under this environment.

Definitions and Theorems

Function: aig-eval-list

(defun aig-eval-list (x env)
       (declare (xargs :guard t))
       (let ((__function__ 'aig-eval-list))
            (declare (ignorable __function__))
            (if (atom x)
                nil
                (cons (aig-eval (car x) env)
                      (aig-eval-list (cdr x) env)))))

Theorem: consp-of-aig-eval-list

(defthm consp-of-aig-eval-list
        (equal (consp (aig-eval-list x env))
               (consp x)))

Theorem: len-of-aig-eval-list

(defthm len-of-aig-eval-list
        (equal (len (aig-eval-list x env))
               (len x)))

Theorem: aig-eval-list-of-append

(defthm aig-eval-list-of-append
        (equal (aig-eval-list (append x y) env)
               (append (aig-eval-list x env)
                       (aig-eval-list y env))))