		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))))