		Search-engine friendly clone of the ACL2 documentation.

Depgraph

Mergesort-alist-values

Sort all of the values bound in an alist.

Signature
(mergesort-alist-values x) → *

Definitions and Theorems

Function: mergesort-alist-values

(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: mergesort-alist-values-when-atom

(defthm mergesort-alist-values-when-atom
  (implies (atom x)
           (equal (mergesort-alist-values x) nil)))

Theorem: mergesort-alist-values-of-cons

(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: alistp-of-mergesort-alist-values

(defthm alistp-of-mergesort-alist-values
  (alistp (mergesort-alist-values x)))

Theorem: hons-assoc-equal-of-mergesort-alist-values

(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: alist-keys-of-mergesort-alist-values

(defthm alist-keys-of-mergesort-alist-values
  (equal (alist-keys (mergesort-alist-values x))
         (alist-keys x)))

Theorem: list-equiv-implies-equal-mergesort-alist-values-1

(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: alist-equiv-implies-alist-equiv-mergesort-alist-values-1

(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))