		Search-engine friendly clone of the ACL2 documentation.

Best-aig

Aig-list-label-nodes

Extends aig-label-nodes to an AIG list.

Signature
(aig-list-label-nodes x free map) → (mv free map)
Arguments: x — AIG list to traverse.; free — Guard (natp free).
Returns: free — Type (natp free).

Definitions and Theorems

Function: aig-list-label-nodes

(defun aig-list-label-nodes (x free map)
  (declare (xargs :guard (natp free)))
  (let ((__function__ 'aig-list-label-nodes))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (mv (nfix free) map))
         ((mv free map)
          (aig-label-nodes (car x) free map)))
      (aig-list-label-nodes (cdr x)
                            free map))))

Theorem: natp-of-aig-list-label-nodes.free

(defthm natp-of-aig-list-label-nodes.free
  (b* (((mv ?free common-lisp::?map)
        (aig-list-label-nodes x free map)))
    (natp free))
  :rule-classes :type-prescription)