		Search-engine friendly clone of the ACL2 documentation.

Network

Fanin-node-p

Signature
(fanin-node-p x) → *
Arguments: x — Guard (node-p x).

Definitions and Theorems

Function: fanin-node-p

(defun fanin-node-p (x)
  (declare (xargs :guard (node-p x)))
  (let ((__function__ 'fanin-node-p))
    (declare (ignorable __function__))
    (not (equal (ctype (stype x)) (out-ctype)))))

Theorem: fanin-node-p-implies-not-output

(defthm fanin-node-p-implies-not-output
  (implies (fanin-node-p x)
           (and (not (equal (ctype (stype x)) (out-ctype)))
                (not (equal (stype x) :po))
                (not (equal (stype x) :nxst))))
  :rule-classes :forward-chaining)

Theorem: fanin-node-p-by-ctype

(defthm fanin-node-p-by-ctype
  (implies (and (equal ctype (ctype (stype x)))
                (syntaxp (quotep ctype)))
           (equal (fanin-node-p x)
                  (not (equal ctype (out-ctype))))))

Theorem: fanin-node-p-of-node-fix-x

(defthm fanin-node-p-of-node-fix-x
  (equal (fanin-node-p (node-fix x))
         (fanin-node-p x)))

Theorem: fanin-node-p-node-equiv-congruence-on-x

(defthm fanin-node-p-node-equiv-congruence-on-x
  (implies (node-equiv x x-equiv)
           (equal (fanin-node-p x)
                  (fanin-node-p x-equiv)))
  :rule-classes :congruence)