sort-symbols

(local (defthm len-strict-merge-symbol<
    (<= (len (strict-merge-symbol< l1 l2 acc))
      (+ (len l1) (len l2) (len acc)))
    :rule-classes :linear))

(local (defthm len-evens
    (equal (len l) (+ (len (evens l)) (len (odds l))))
    :rule-classes :linear))

(local (defthm symbol-listp-evens
    (implies (symbol-listp x) (symbol-listp (evens x)))
    :hints (("Goal" :induct (evens x)))))

(local (defthm symbol-listp-odds
    (implies (symbol-listp x) (symbol-listp (odds x)))))

(local (defthm symbol-listp-strict-merge-symbol<
    (implies (and (symbol-listp l1) (symbol-listp l2) (symbol-listp acc))
      (symbol-listp (strict-merge-symbol< l1 l2 acc)))))

(local (defthm symbol-listp-strict-merge-sort-symbol<
    (implies (symbol-listp x)
      (symbol-listp (strict-merge-sort-symbol< x)))))

(local (defthm member-eq-revappend-lemma
    (implies (member-eq a y) (member-eq a (revappend x y)))))

(local (defthm member-eq-revappend
    (iff (member-eq a (revappend x y))
      (or (member-eq a x) (member-eq a y)))))

(local (defthm member-eq-strict-merge-symbol<
    (iff (member-eq a (strict-merge-symbol< x y z))
      (or (member-eq a x) (member-eq a y) (member-eq a z)))))

(local (defthm member-eq-evens
    (implies (syntaxp (symbolp x))
      (iff (member-eq a x)
        (or (member-eq a (evens x)) (member-eq a (evens (cdr x))))))))

(local (defun strict-symbol->-sortedp
    (x)
    (declare (xargs :guard (symbol-listp x)))
    (cond ((or (endp x) (null (cdr x))) t)
      (t (and (symbol< (cadr x) (car x))
          (strict-symbol->-sortedp (cdr x)))))))

(local (defun sorted-lists-symbol->
    (x y)
    (or (atom x) (atom y) (symbol< (car y) (car x)))))

(local (defthm strict-symbol<-revappend
    (implies (and (symbol-listp x)
        (strict-symbol->-sortedp x)
        (symbol-listp y)
        (strict-symbol<-sortedp y)
        (sorted-lists-symbol-> y x))
      (strict-symbol<-sortedp (revappend x y)))))

(local (defthm strict-symbol<-sortedp-strict-merge-symbol<
    (implies (and (symbol-listp x)
        (symbol-listp y)
        (symbol-listp acc)
        (strict-symbol<-sortedp x)
        (strict-symbol<-sortedp y)
        (strict-symbol->-sortedp acc)
        (sorted-lists-symbol-> x acc)
        (sorted-lists-symbol-> y acc))
      (strict-symbol<-sortedp (strict-merge-symbol< x y acc)))))