		Search-engine friendly clone of the ACL2 documentation.

Depgraph

Alist-values-are-sets-p

Recognizer for alists whose every value is an ordered set.

Signature
(alist-values-are-sets-p x) → *

Definitions and Theorems

Function: alist-values-are-sets-p

(defun alist-values-are-sets-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'alist-values-are-sets-p))
    (declare (ignorable __function__))
    (b* (((when (atom x)) t)
         ((when (atom (car x)))
          (alist-values-are-sets-p (cdr x))))
      (and (setp (cdar x))
           (alist-values-are-sets-p (cdr x))))))

Theorem: alist-values-are-sets-p-when-atom

(defthm alist-values-are-sets-p-when-atom
  (implies (not (consp x))
           (equal (alist-values-are-sets-p x) t)))

Theorem: alist-values-are-sets-p-of-cons

(defthm alist-values-are-sets-p-of-cons
  (equal (alist-values-are-sets-p (cons a x))
         (and (setp (cdr a))
              (alist-values-are-sets-p x))))

Theorem: setp-of-lookup-when-alist-values-are-sets-p

(defthm setp-of-lookup-when-alist-values-are-sets-p
  (implies (alist-values-are-sets-p x)
           (setp (cdr (hons-assoc-equal a x)))))

Theorem: alist-values-are-sets-p-of-hons-shrink-alist

(defthm alist-values-are-sets-p-of-hons-shrink-alist
  (implies (and (alist-values-are-sets-p x)
                (alist-values-are-sets-p ans))
           (alist-values-are-sets-p (hons-shrink-alist x ans))))

Theorem: alist-values-are-sets-p-of-mergesort-alist-values

(defthm alist-values-are-sets-p-of-mergesort-alist-values
  (alist-values-are-sets-p (mergesort-alist-values x)))

Theorem: list-equiv-implies-equal-alist-values-are-sets-p-1

(defthm list-equiv-implies-equal-alist-values-are-sets-p-1
  (implies (acl2::list-equiv x x-equiv)
           (equal (alist-values-are-sets-p x)
                  (alist-values-are-sets-p x-equiv)))
  :rule-classes (:congruence))