(include-book "quicksort")

(defun hm (e x)
  (if (endp x)
      0
      (if (equal e (car x))
          (+ 1 (hm e (cdr x)))
          (hm e (cdr x)))))

(defthm hm-append
  (equal (hm e (append a b))
         (+ (hm e a)
            (hm e b))))

(include-book "arithmetic-5/top" :dir :system)

(defthm hm-removes
  (EQUAL (+ (HM E (REMOVE-GT D A))
            (HM E (REMOVE-LTE D A)))
         (HM E A)))


(defthm main-lemma
  (equal (hm e (quicksort x))
         (hm e x)))

(defthm hm-rm
  (equal (hm e (rm d a))
         (if (memb d a)
             (if (equal e d)
                 (- (hm e a) 1)
                 (hm e a))
             (hm e a))))

(defthm perm-hm-left-to-right
  (implies (perm a b)
           (equal (hm e a) (hm e b))))

(thm (implies (equal (hm e a) (hm e b))
              (perm a b)))

(let ((a '(1 2 2 2 3))
      (b '(1 2 2 2 3 4))
      (e 2))
  (implies (equal (hm e a) (hm e b))
           (perm a b)))

(defstub bad (x y) t)

(defaxiom bad-axiom
  (iff (perm x y)
       (equal (hm (bad x y) x)
              (hm (bad x y) y))))

(defthm main
  (perm (quicksort x) x))