• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
    • Apt
    • Zfc
    • Acre
    • Milawa
    • Smtlink
    • Abnf
    • Vwsim
    • Isar
    • Wp-gen
    • Dimacs-reader
    • Pfcs
    • Legacy-defrstobj
    • C
    • Proof-checker-array
    • Soft
    • Farray
    • Rp-rewriter
    • Instant-runoff-voting
      • Fairness-criteria
      • Candidate-with-least-nth-place-votes
      • Eliminate-candidate
      • First-choice-of-majority-p
      • Candidate-ids
        • Sorting-candidate-ids
      • Irv
      • Create-nth-choice-count-alist
      • Irv-alt
      • Irv-ballot-p
      • Majority
      • Number-of-candidates
      • List-elements-equal
      • Number-of-voters
    • Imp-language
    • Sidekick
    • Ethereum
    • Leftist-trees
    • Java
    • Riscv
    • Taspi
    • Bitcoin
    • Zcash
    • Des
    • X86isa
    • Sha-2
    • Yul
    • Proof-checker-itp13
    • Regex
    • ACL2-programming-language
    • Json
    • Jfkr
    • Equational
    • Cryptography
    • Axe
    • Poseidon
    • Where-do-i-place-my-book
    • Aleo
    • Bigmems
    • Builtins
    • Execloader
    • Solidity
    • Paco
    • Concurrent-programs
    • Bls12-377-curves
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Candidate-ids

Sorting-candidate-ids

Definitions and Theorems

Function: <-ordered-p

(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: <-merge

(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: <-merge-tr

(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: <-mergesort-fixnum

(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: <-mergesort-integers

(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: <-sort

(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: <-sort-preserves-duplicity

(defthm acl2::<-sort-preserves-duplicity
  (equal (acl2::duplicity a (acl2::<-sort x))
         (acl2::duplicity a x)))

Theorem: <-sort-creates-comparable-listp

(defthm acl2::<-sort-creates-comparable-listp
  (implies (nat-listp x)
           (nat-listp (acl2::<-sort x))))

Theorem: <-sort-sorts

(defthm acl2::<-sort-sorts
  (acl2::<-ordered-p (acl2::<-sort x)))

Theorem: <-sort-no-duplicatesp-equal

(defthm acl2::<-sort-no-duplicatesp-equal
  (equal (no-duplicatesp-equal (acl2::<-sort x))
         (no-duplicatesp-equal x)))

Theorem: <-sort-true-listp

(defthm acl2::<-sort-true-listp
  (true-listp (acl2::<-sort x))
  :rule-classes :type-prescription)

Theorem: <-sort-len

(defthm acl2::<-sort-len
  (equal (len (acl2::<-sort x)) (len x)))

Theorem: <-sort-consp

(defthm acl2::<-sort-consp
  (equal (consp (acl2::<-sort x))
         (consp x)))

Theorem: <-sort-is-identity-under-set-equiv

(defthm acl2::<-sort-is-identity-under-set-equiv
  (acl2::set-equiv (acl2::<-sort x) x))

Function: <-insert

(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: <-insertsort

(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: <-mergesort-equals-insertsort

(defthm acl2::<-mergesort-equals-insertsort
  (equal (acl2::<-sort x)
         (acl2::<-insertsort x)))

Theorem: <-insertsort-preserves-duplicity

(defthm acl2::<-insertsort-preserves-duplicity
  (equal (acl2::duplicity a (acl2::<-insertsort x))
         (acl2::duplicity a x)))

Theorem: <-insertsort-creates-comparable-listp

(defthm acl2::<-insertsort-creates-comparable-listp
  (implies (nat-listp x)
           (nat-listp (acl2::<-insertsort x))))

Theorem: <-insertsort-sorts

(defthm acl2::<-insertsort-sorts
  (acl2::<-ordered-p (acl2::<-insertsort x)))

Theorem: <-insertsort-no-duplicatesp-equal

(defthm acl2::<-insertsort-no-duplicatesp-equal
  (equal (no-duplicatesp-equal (acl2::<-insertsort x))
         (no-duplicatesp-equal x)))

Theorem: <-insertsort-true-listp

(defthm acl2::<-insertsort-true-listp
  (true-listp (acl2::<-insertsort x))
  :rule-classes :type-prescription)

Theorem: <-insertsort-len

(defthm acl2::<-insertsort-len
  (equal (len (acl2::<-insertsort x))
         (len x)))

Theorem: <-insertsort-consp

(defthm acl2::<-insertsort-consp
  (equal (consp (acl2::<-insertsort x))
         (consp x)))

Theorem: subsetp-cdr-and-<-insertsort

(defthm subsetp-cdr-and-<-insertsort
  (subsetp-equal (acl2::<-insertsort (cdr a))
                 (acl2::<-insertsort a)))

Theorem: a-is-a-subset-of-<-insertsort-a

(defthm a-is-a-subset-of-<-insertsort-a
  (subsetp-equal a (acl2::<-insertsort a)))

Theorem: <-insertsort-a-is-a-subset-of-a

(defthm <-insertsort-a-is-a-subset-of-a
  (subsetp-equal (acl2::<-insertsort a)
                 a))

Theorem: <-insertsort-equal-under-set-equiv

(defthm <-insertsort-equal-under-set-equiv
  (acl2::set-equiv (acl2::<-insertsort a)
                   a))