merge-sort-term-order

Included Books

other

(in-package "ACL2")

include-book

(include-book "perm")

include-book

(include-book "term-ordered-perms")

include-book

(include-book "convert-perm-to-how-many")

local

(local (defthm term-order-total
    (implies (not (term-order x y)) (term-order y x))))

term-orderedp-merge-sort-term-ordertheorem

(defthm term-orderedp-merge-sort-term-order
  (term-orderedp (merge-sort-term-order x))
  :hints (("Goal" :in-theory (e/d nil (term-order)))))

true-listp-merge-sort-term-ordertheorem

(defthm true-listp-merge-sort-term-order
  (implies (true-listp x)
    (true-listp (merge-sort-term-order x))))

how-many-merge-term-ordertheorem

(defthm how-many-merge-term-order
  (equal (how-many e (merge-term-order x y))
    (+ (how-many e x) (how-many e y))))

how-many-evens-and-oddstheorem

(defthm how-many-evens-and-odds
  (implies (consp x)
    (equal (+ (how-many e (evens x)) (how-many e (evens (cdr x))))
      (how-many e x))))

how-many-merge-sort-term-ordertheorem

(defthm how-many-merge-sort-term-order
  (equal (how-many e (merge-sort-term-order x))
    (how-many e x)))