Sort all of the values bound in an alist.
(mergesort-alist-values x) → *
Function:
(defun mergesort-alist-values (x) (declare (xargs :guard t)) (let ((__function__ 'mergesort-alist-values)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) ((when (atom (car x))) (mergesort-alist-values (cdr x)))) (cons (cons (caar x) (mergesort (cdar x))) (mergesort-alist-values (cdr x))))))
Theorem:
(defthm mergesort-alist-values-when-atom (implies (atom x) (equal (mergesort-alist-values x) nil)))
Theorem:
(defthm mergesort-alist-values-of-cons (equal (mergesort-alist-values (cons a x)) (if (atom a) (mergesort-alist-values x) (cons (cons (car a) (mergesort (cdr a))) (mergesort-alist-values x)))))
Theorem:
(defthm alistp-of-mergesort-alist-values (alistp (mergesort-alist-values x)))
Theorem:
(defthm hons-assoc-equal-of-mergesort-alist-values (equal (hons-assoc-equal key (mergesort-alist-values x)) (let ((look (hons-assoc-equal key x))) (and look (cons (car look) (mergesort (cdr look)))))))
Theorem:
(defthm alist-keys-of-mergesort-alist-values (equal (alist-keys (mergesort-alist-values x)) (alist-keys x)))
Theorem:
(defthm list-equiv-implies-equal-mergesort-alist-values-1 (implies (acl2::list-equiv x x-equiv) (equal (mergesort-alist-values x) (mergesort-alist-values x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm alist-equiv-implies-alist-equiv-mergesort-alist-values-1 (implies (acl2::alist-equiv x x-equiv) (acl2::alist-equiv (mergesort-alist-values x) (mergesort-alist-values x-equiv))) :rule-classes (:congruence))