Recognizer for alists whose every value is an ordered set.
(alist-values-are-sets-p x) → *
Function:
(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:
(defthm alist-values-are-sets-p-when-atom (implies (not (consp x)) (equal (alist-values-are-sets-p x) t)))
Theorem:
(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:
(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:
(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:
(defthm alist-values-are-sets-p-of-mergesort-alist-values (alist-values-are-sets-p (mergesort-alist-values x)))
Theorem:
(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))