		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)