		Search-engine friendly clone of the ACL2 documentation.

Network

Stype-count

(stype-count type x) counts the number of nodes whose sequential-type is type in the node list x.

Signature
(stype-count type x) → count
Arguments: type — Guard (stypep type).; x — Guard (node-listp x).
Returns: count — Type (natp count).

This is a key function in the logical story of Aignet input, output, and register numbering. See representation for more details.

Definitions and Theorems

Function: stype-count

(defun stype-count (type x)
       (declare (xargs :guard (and (stypep type) (node-listp x))))
       (let ((__function__ 'stype-count))
            (declare (ignorable __function__))
            (cond ((atom x) 0)
                  ((equal (stype-fix type) (stype (car x)))
                   (+ 1 (stype-count type (cdr x))))
                  (t (stype-count type (cdr x))))))

Theorem: natp-of-stype-count

(defthm natp-of-stype-count
        (b* ((count (stype-count type x)))
            (natp count))
        :rule-classes :type-prescription)

Theorem: stype-count-of-cons

(defthm stype-count-of-cons
        (equal (stype-count type (cons a b))
               (if (equal (stype-fix type) (stype a))
                   (+ 1 (stype-count type b))
                   (stype-count type b))))

Theorem: stype-count-of-atom

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

Theorem: positive-stype-count-implies-consp

(defthm positive-stype-count-implies-consp
        (implies (< 0 (stype-count stype x))
                 (consp x))
        :rule-classes :forward-chaining)

Theorem: stype-count-of-stype-fix-type

(defthm stype-count-of-stype-fix-type
        (equal (stype-count (stype-fix type) x)
               (stype-count type x)))

Theorem: stype-count-stype-equiv-congruence-on-type

(defthm stype-count-stype-equiv-congruence-on-type
        (implies (stype-equiv type type-equiv)
                 (equal (stype-count type x)
                        (stype-count type-equiv x)))
        :rule-classes :congruence)

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

(defthm stype-count-of-node-list-fix-x
        (equal (stype-count type (node-list-fix x))
               (stype-count type x)))

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

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