		Search-engine friendly clone of the ACL2 documentation.

Node

Co-node->fanin

Access the fanin literal from a combinational output node, i.e., from a primary output or a next-state (register input) node.

Signature
(co-node->fanin node) → lit
Arguments: node — Guard (node-p node).
Returns: lit — Type (litp lit).

Definitions and Theorems

Function: co-node->fanin

(defun co-node->fanin (node)
  (declare (xargs :guard (node-p node)))
  (declare (xargs :guard (equal (node->type node) (out-type))))
  (let ((__function__ 'co-node->fanin))
    (declare (ignorable __function__))
    (lit-fix (if (equal (node->regp node) 1)
                 (nxst-node->fanin node)
               (po-node->fanin node)))))

Theorem: litp-of-co-node->fanin

(defthm litp-of-co-node->fanin
  (b* ((lit (co-node->fanin node)))
    (litp lit))
  :rule-classes :type-prescription)

Theorem: co-node->fanin-of-po-node

(defthm co-node->fanin-of-po-node
  (equal (co-node->fanin (po-node f))
         (lit-fix f)))

Theorem: co-node->fanin-of-nxst-node

(defthm co-node->fanin-of-nxst-node
  (equal (co-node->fanin (nxst-node f n))
         (lit-fix f)))

Theorem: co-node->fanin-of-node-fix-node

(defthm co-node->fanin-of-node-fix-node
  (equal (co-node->fanin (node-fix node))
         (co-node->fanin node)))

Theorem: co-node->fanin-node-equiv-congruence-on-node

(defthm co-node->fanin-node-equiv-congruence-on-node
  (implies (node-equiv node node-equiv)
           (equal (co-node->fanin node)
                  (co-node->fanin node-equiv)))
  :rule-classes :congruence)