		Search-engine friendly clone of the ACL2 documentation.

Node

Gate-node->fanin1

Access the fanin 1 literal from a gate node, whether an AND or an XOR.

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

Definitions and Theorems

Function: gate-node->fanin1

(defun
     gate-node->fanin1 (node)
     (declare (xargs :guard (node-p node)))
     (declare (xargs :guard (equal (node->type node) (gate-type))))
     (let ((__function__ 'gate-node->fanin1))
          (declare (ignorable __function__))
          (lit-fix (if (equal (node->regp node) 1)
                       (xor-node->fanin1 node)
                       (and-node->fanin1 node)))))

Theorem: litp-of-gate-node->fanin1

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

Theorem: gate-node->fanin1-of-and-node

(defthm gate-node->fanin1-of-and-node
        (equal (gate-node->fanin1 (and-node f0 f1))
               (lit-fix f1)))

Theorem: gate-node->fanin1-of-xor-node

(defthm gate-node->fanin1-of-xor-node
        (equal (gate-node->fanin1 (xor-node f0 f1))
               (lit-fix f1)))

Theorem: gate-node->fanin1-of-node-fix-node

(defthm gate-node->fanin1-of-node-fix-node
        (equal (gate-node->fanin1 (node-fix node))
               (gate-node->fanin1 node)))

Theorem: gate-node->fanin1-node-equiv-congruence-on-node

(defthm gate-node->fanin1-node-equiv-congruence-on-node
        (implies (node-equiv node node-equiv)
                 (equal (gate-node->fanin1 node)
                        (gate-node->fanin1 node-equiv)))
        :rule-classes :congruence)