		Search-engine friendly clone of the ACL2 documentation.

Best-aig

Aig-count-labels

Signature
(aig-count-labels x map) → count
Arguments: x — A single AIG.; map — Mapping of AIG nodes to labels.
Returns: count — Type (natp count).

Definitions and Theorems

Function: aig-count-labels

(defun aig-count-labels (x map)
  (declare (xargs :guard t))
  (let ((__function__ 'aig-count-labels))
    (declare (ignorable __function__))
    (set::cardinality (aig-collect-labels x map))))

Theorem: natp-of-aig-count-labels

(defthm natp-of-aig-count-labels
  (b* ((count (aig-count-labels x map)))
    (natp count))
  :rule-classes :type-prescription)