(defun emptyp (x)
  (atom x))

(defun val (x)
  (car x))

(defun left (x)
  (cadr x))

(defun right (x)
  (caddr x))

(defun tree-count (x)
  (if (emptyp x)
      0
      (+ 1 (+ (tree-count (left x))
              (tree-count (right x))))))

(defthm natp-tree-count
  (natp (tree-count x)))

(defthm count-tree-count
  (if (emptyp x)
      (equal (tree-count x) 0)
      (equal (tree-count x)
             (+ 1
                (tree-count (left x))
                (tree-count (right x))))))

(defthm tree-count-<
  (implies (not (emptyp x))
           (and (< (tree-count (right x)) (tree-count x))
                (< (tree-count (left x)) (tree-count x)))))

(defun lessp (x e)
  (if (emptyp x)
      t
      (and (lessp (left x) e)
           (< (val x) e)
           (lessp (right x) e))))

(defun overp (x e)
  (if (emptyp x)
      t
      (and (overp (left x) e)
           (< e (val x))
           (overp (right x) e))))

(defun treep (x)
  (if (emptyp x)
      (null x)
      (and (consp x)
           (rationalp (car x))
           (consp (cdr x))
           (treep (cadr x))
           (consp (cddr x))
           (treep (caddr x))
           (lessp (left x) (val x))
           (overp (right x) (val x))
           (null (cdddr x)))))

(defun tree (x l r)
  (list x l r))

(defthm tree-elim
  (implies (and (treep x)
                (not (emptyp x)))
           (equal (tree (val x) (left x) (right x))
                  x))
  :rule-classes :elim)

(defthm tree-left
  (implies (and (treep x)
                (not (emptyp x)))
           (treep (left x))))

(defthm tree-right
  (implies (and (treep x)
                (not (emptyp x)))
           (treep (right x))))

(defthm rationalp-val
  (implies (and (treep x)
                (not (emptyp x)))
           (rationalp (val x))))

(defthm lessp-left
  (implies (and (treep x)
                (not (emptyp x)))
           (lessp (left x) (val x))))

(defthm overp-right
  (implies (and (treep x)
                (not (emptyp x)))
           (overp (right x) (val x))))

(defthm treep-tree
  (implies (and (rationalp x)
                (treep l)
                (treep r)
                (lessp l x)
                (overp r x))
           (treep (tree x l r)))
  :rule-classes (:rewrite))

(in-theory (disable emptyp treep val tree left right tree-count))

(defun tree-memberp (e x)
  (declare (xargs :measure (tree-count x)))
  (if (emptyp x)
      nil
      (if (= (val x) e)
          t
          (if (< e (val x))
              (tree-memberp e (left x))
              (tree-memberp e (right x))))))

(defthm lessp-not-member
  (implies (and (treep x)
                (lessp x e))
           (not (tree-memberp e x)))
  :hints (("Goal" :induct (lessp x e))))

(defthm overp-not-member
  (implies (and (treep x)
                (overp x e))
           (not (tree-memberp e x)))
  :hints (("Goal" :induct (overp x e))))

(defthm not-tree-memberp-lemma-lessp2
  (implies (and (treep x)
                (<= e1 e2)
                (lessp x e1))
           (lessp x e2))
  :rule-classes ((:rewrite :match-free :all)))

(defthm not-tree-memberp-lemma-overp2
  (implies (and (treep x)
                (< e1 e2)
                (overp x e2))
           (overp x e1))
  :rule-classes ((:rewrite :match-free :all)))

(defthm not-tree-memberp
  (implies (and (treep x)
                (not (emptyp x)))
           (if (= e (val x))
               t
               (if (< e (val x))
                   (not (tree-memberp e (right x)))
                   (not (tree-memberp e (left x))))))
  :hints (("Goal" :induct (tree-memberp e x))))

(defun tree-to-list (x)
  (declare (xargs :measure (tree-count x)))
  (if (emptyp x)
      nil
      (append (tree-to-list (left x))
              (list (val x))
              (tree-to-list (right x)))))

(defthm member-append
  (iff (member e (append x y))
       (or (member e x)
           (member e y))))

(defthm tree-memberp-member-tree-to-list
  (implies (treep x)
           (iff (tree-memberp e x)
                (member e (tree-to-list x))))
  :rule-classes nil)

(defthm member-tree-to-list-tree-memberp
  (implies (treep x)
           (iff (member e (tree-to-list x))
                (tree-memberp e x)))
  :hints (("Goal" :use (tree-memberp-member-tree-to-list)))
  :rule-classes nil)