		Search-engine friendly clone of the ACL2 documentation.

Svex-focused-equivalence-checking

Hons-aig-accumulate-nodes

Signature
(hons-aig-accumulate-nodes x acc) → nodes
Returns: nodes — Type (alistp nodes), given (alistp acc).

Definitions and Theorems

Function: hons-aig-accumulate-nodes

(defun hons-aig-accumulate-nodes (x acc)
  (declare (xargs :guard t))
  (let ((__function__ 'hons-aig-accumulate-nodes))
    (declare (ignorable __function__))
    (b* (((when (atom x))
          (if (or (booleanp x) (hons-get x acc))
              acc
            (hons-acons x t acc)))
         ((when (eq (cdr x) nil))
          (hons-aig-accumulate-nodes (car x) acc))
         ((when (hons-get x acc)) acc)
         (acc (hons-acons x t acc))
         (acc (hons-aig-accumulate-nodes (car x)
                                         acc)))
      (hons-aig-accumulate-nodes (cdr x)
                                 acc))))

Theorem: alistp-of-hons-aig-accumulate-nodes

(defthm alistp-of-hons-aig-accumulate-nodes
  (implies (alistp acc)
           (b* ((nodes (hons-aig-accumulate-nodes x acc)))
             (alistp nodes)))
  :rule-classes :rewrite)