		Search-engine friendly clone of the ACL2 documentation.

Create-count-alist

Count-alistp

Recognizer for a count alist (see create-count-alist)

Signature
(count-alistp l) → *

Definitions and Theorems

Function: count-alistp

(defun count-alistp (l)
  (declare (xargs :guard t))
  (let ((__function__ 'count-alistp))
    (declare (ignorable __function__))
    (cond ((atom l) (eq l nil))
          (t (and (consp (car l))
                  (natp (caar l))
                  (natp (cdar l))
                  (count-alistp (cdr l)))))))

Theorem: count-alistp-implies-alistp

(defthm count-alistp-implies-alistp
  (implies (count-alistp l) (alistp l)))

Theorem: nat-listp-of-strip-cars-of-count-alistp

(defthm nat-listp-of-strip-cars-of-count-alistp
  (implies (count-alistp alst)
           (nat-listp (strip-cars alst))))

Theorem: nat-listp-of-strip-cdrs-of-count-alistp

(defthm nat-listp-of-strip-cdrs-of-count-alistp
  (implies (count-alistp alst)
           (nat-listp (strip-cdrs alst))))

Theorem: natp-of-key-of-first-pair-of-count-alistp

(defthm natp-of-key-of-first-pair-of-count-alistp
  (implies (and (count-alistp alst) (consp alst))
           (natp (caar alst))))