		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)