		Search-engine friendly clone of the ACL2 documentation.

Network

Fanin-count

Number of fanin nodes in the list of nodes

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

This gives the ID of the last fanin node in the list.

Definitions and Theorems

Function: fanin-count

(defun fanin-count (x)
  (declare (xargs :guard (node-listp x)))
  (let ((__function__ 'fanin-count))
    (declare (ignorable __function__))
    (if (atom x)
        0
      (+ (if (fanin-node-p (car x)) 1 0)
         (fanin-count (cdr x))))))

Theorem: fanin-count-of-cons

(defthm fanin-count-of-cons
  (equal (fanin-count (cons a x))
         (+ (if (fanin-node-p a) 1 0)
            (fanin-count x))))

Theorem: fanin-count-of-atom

(defthm fanin-count-of-atom
  (implies (not (consp x))
           (equal (fanin-count x) 0))
  :rule-classes ((:rewrite :backchain-limit-lst 1)))

Theorem: fanin-count-of-cdr-strong

(defthm fanin-count-of-cdr-strong
  (implies (and (consp x) (fanin-node-p (car x)))
           (equal (fanin-count (cdr x))
                  (+ -1 (fanin-count x)))))

Theorem: fanin-count-of-cdr-weak

(defthm fanin-count-of-cdr-weak
  (<= (fanin-count (cdr x))
      (fanin-count x))
  :rule-classes :linear)

Theorem: fanin-count-of-node-list-fix-x

(defthm fanin-count-of-node-list-fix-x
  (equal (fanin-count (node-list-fix x))
         (fanin-count x)))

Theorem: fanin-count-node-list-equiv-congruence-on-x

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