		Search-engine friendly clone of the ACL2 documentation.

Skip-detection

Sd-patalist-p

(sd-patalist-p x) recognizes alists that bind strings to sd-keylist-ps.

Definitions and Theorems

Function: sd-patalist-p

(defun sd-patalist-p (x)
  (declare (xargs :guard t))
  (if (atom x)
      t
    (and (consp (car x))
         (stringp (caar x))
         (sd-keylist-p (cdar x))
         (sd-patalist-p (cdr x)))))

Theorem: sd-patalist-p-when-not-consp

(defthm sd-patalist-p-when-not-consp
  (implies (not (consp x))
           (equal (sd-patalist-p x) t)))

Theorem: sd-patalist-p-of-cons

(defthm sd-patalist-p-of-cons
  (equal (sd-patalist-p (cons a x))
         (and (consp a)
              (stringp (car a))
              (sd-keylist-p (cdr a))
              (sd-patalist-p x))))

Theorem: sd-keylist-p-of-cdr-of-hons-assoc-equal-when-sd-patalist-p

(defthm sd-keylist-p-of-cdr-of-hons-assoc-equal-when-sd-patalist-p
  (implies (force (sd-patalist-p x))
           (sd-keylist-p (cdr (hons-assoc-equal a x)))))

Theorem: sd-patalist-p-of-hons-shrink-alist

(defthm sd-patalist-p-of-hons-shrink-alist
  (implies (and (sd-patalist-p x)
                (sd-patalist-p y))
           (sd-patalist-p (hons-shrink-alist x y))))