Function:
(defun acl2::<-ordered-p (x) (declare (xargs :guard (and t (nat-listp x)) :stobjs nil)) (cond ((atom x) t) ((atom (cdr x)) t) ((< (first x) (second x)) (acl2::<-ordered-p (cdr x))) (t (and (not (< (second x) (first x))) (acl2::<-ordered-p (cdr x))))))
Function:
(defun acl2::<-merge (x y) (declare (xargs :stobjs nil :guard (and t (nat-listp x) (nat-listp y)))) (cond ((atom x) y) ((atom y) x) ((< (car y) (car x)) (cons (car y) (acl2::<-merge x (cdr y)))) (t (cons (car x) (acl2::<-merge (cdr x) y)))))
Function:
(defun acl2::<-merge-tr (x y acl2::acc) (declare (xargs :stobjs nil :guard (and t (nat-listp x) (nat-listp y)))) (cond ((atom x) (acl2::revappend-without-guard acl2::acc y)) ((atom y) (acl2::revappend-without-guard acl2::acc x)) ((< (car y) (car x)) (acl2::<-merge-tr x (cdr y) (cons (car y) acl2::acc))) (t (acl2::<-merge-tr (cdr x) y (cons (car x) acl2::acc)))))
Function:
(defun acl2::<-mergesort-fixnum (x len) (declare (xargs :stobjs nil :guard (and t (nat-listp x) (natp len) (<= len (len x)))) (type (signed-byte 30) len)) (cond ((mbe :logic (zp len) :exec (eql (the (signed-byte 30) len) 0)) nil) ((eql (the (signed-byte 30) len) 1) (list (car x))) (t (let* ((acl2::len1 (the (signed-byte 30) (ash (the (signed-byte 30) len) -1))) (acl2::len2 (the (signed-byte 30) (- (the (signed-byte 30) len) (the (signed-byte 30) acl2::len1)))) (acl2::part1 (acl2::<-mergesort-fixnum x acl2::len1)) (acl2::part2 (acl2::<-mergesort-fixnum (acl2::rest-n acl2::len1 x) acl2::len2))) (acl2::<-merge-tr acl2::part1 acl2::part2 nil)))))
Function:
(defun acl2::<-mergesort-integers (x len) (declare (xargs :stobjs nil :guard (and t (nat-listp x) (natp len) (<= len (len x)))) (type integer len)) (cond ((mbe :logic (zp len) :exec (eql (the integer len) 0)) nil) ((eql (the integer len) 1) (list (car x))) (t (let* ((acl2::len1 (the integer (ash (the integer len) -1))) (acl2::len2 (the integer (- (the integer len) (the integer acl2::len1)))) (acl2::part1 (if (< (the integer acl2::len1) (acl2::mergesort-fixnum-threshold)) (acl2::<-mergesort-fixnum x acl2::len1) (acl2::<-mergesort-integers x acl2::len1))) (acl2::part2 (if (< (the integer acl2::len2) (acl2::mergesort-fixnum-threshold)) (acl2::<-mergesort-fixnum (acl2::rest-n acl2::len1 x) acl2::len2) (acl2::<-mergesort-integers (acl2::rest-n acl2::len1 x) acl2::len2)))) (acl2::<-merge-tr acl2::part1 acl2::part2 nil)))))
Function:
(defun acl2::<-sort (x) (declare (xargs :guard (and t (nat-listp x)) :stobjs nil)) (mbe :logic (cond ((atom x) nil) ((atom (cdr x)) (list (car x))) (t (let ((acl2::half (floor (len x) 2))) (acl2::<-merge (acl2::<-sort (take acl2::half x)) (acl2::<-sort (nthcdr acl2::half x)))))) :exec (let ((len (len x))) (if (< len (acl2::mergesort-fixnum-threshold)) (acl2::<-mergesort-fixnum x len) (acl2::<-mergesort-integers x len)))))
Theorem:
(defthm acl2::<-sort-preserves-duplicity (equal (acl2::duplicity a (acl2::<-sort x)) (acl2::duplicity a x)))
Theorem:
(defthm acl2::<-sort-creates-comparable-listp (implies (nat-listp x) (nat-listp (acl2::<-sort x))))
Theorem:
(defthm acl2::<-sort-sorts (acl2::<-ordered-p (acl2::<-sort x)))
Theorem:
(defthm acl2::<-sort-no-duplicatesp-equal (equal (no-duplicatesp-equal (acl2::<-sort x)) (no-duplicatesp-equal x)))
Theorem:
(defthm acl2::<-sort-true-listp (true-listp (acl2::<-sort x)) :rule-classes :type-prescription)
Theorem:
(defthm acl2::<-sort-len (equal (len (acl2::<-sort x)) (len x)))
Theorem:
(defthm acl2::<-sort-consp (equal (consp (acl2::<-sort x)) (consp x)))
Theorem:
(defthm acl2::<-sort-is-identity-under-set-equiv (acl2::set-equiv (acl2::<-sort x) x))
Function:
(defun acl2::<-insert (elt x) (declare (xargs :guard (and t (natp elt) (nat-listp x)) :stobjs nil)) (if (atom x) (list elt) (if (< (car x) elt) (cons (car x) (acl2::<-insert elt (cdr x))) (cons elt x))))
Function:
(defun acl2::<-insertsort (x) (declare (xargs :guard (and t (nat-listp x)) :stobjs nil)) (if (atom x) nil (acl2::<-insert (car x) (acl2::<-insertsort (cdr x)))))
Theorem:
(defthm acl2::<-mergesort-equals-insertsort (equal (acl2::<-sort x) (acl2::<-insertsort x)))
Theorem:
(defthm acl2::<-insertsort-preserves-duplicity (equal (acl2::duplicity a (acl2::<-insertsort x)) (acl2::duplicity a x)))
Theorem:
(defthm acl2::<-insertsort-creates-comparable-listp (implies (nat-listp x) (nat-listp (acl2::<-insertsort x))))
Theorem:
(defthm acl2::<-insertsort-sorts (acl2::<-ordered-p (acl2::<-insertsort x)))
Theorem:
(defthm acl2::<-insertsort-no-duplicatesp-equal (equal (no-duplicatesp-equal (acl2::<-insertsort x)) (no-duplicatesp-equal x)))
Theorem:
(defthm acl2::<-insertsort-true-listp (true-listp (acl2::<-insertsort x)) :rule-classes :type-prescription)
Theorem:
(defthm acl2::<-insertsort-len (equal (len (acl2::<-insertsort x)) (len x)))
Theorem:
(defthm acl2::<-insertsort-consp (equal (consp (acl2::<-insertsort x)) (consp x)))
Theorem:
(defthm subsetp-cdr-and-<-insertsort (subsetp-equal (acl2::<-insertsort (cdr a)) (acl2::<-insertsort a)))
Theorem:
(defthm a-is-a-subset-of-<-insertsort-a (subsetp-equal a (acl2::<-insertsort a)))
Theorem:
(defthm <-insertsort-a-is-a-subset-of-a (subsetp-equal (acl2::<-insertsort a) a))
Theorem:
(defthm <-insertsort-equal-under-set-equiv (acl2::set-equiv (acl2::<-insertsort a) a))