		Search-engine friendly clone of the ACL2 documentation.

Calist

Calistp

Recognizer for calist.

Signature
(calistp x) → *

Definitions and Theorems

Function: calistp

(defun calistp (x)
  (declare (xargs :guard t))
  (let ((__function__ 'calistp))
    (declare (ignorable __function__))
    (if (atom x)
        (eq x nil)
      (and (consp (car x))
           (not (hons-assoc-equal (caar x) (cdr x)))
           (bitp (cdar x))
           (calistp (cdr x))))))

Theorem: calistp-of-cdr

(defthm calistp-of-cdr
  (implies (calistp x) (calistp (cdr x))))

Theorem: bitp-of-cdar-when-calistp

(defthm bitp-of-cdar-when-calistp
  (implies (and (calistp x) (consp x))
           (bitp (cdar x))))

Theorem: calistp-of-cons

(defthm calistp-of-cons
  (equal (calistp (cons a x))
         (and (and (consp a)
                   (bitp (cdr a))
                   (not (hons-assoc-equal (car a) x)))
              (calistp x))))