other
(in-package "ACL2")
other
(verify-termination merge-symbol<)
acl2-count-evenstheorem
(defthm acl2-count-evens (implies (consp (cdr x)) (< (acl2-count (evens x)) (acl2-count x))) :rule-classes :linear)
other
(verify-termination merge-sort-symbol< (declare (xargs :verify-guards nil)))
symbol-listp-evenstheorem
(defthm symbol-listp-evens (implies (symbol-listp x) (symbol-listp (evens x))) :hints (("Goal" :induct (evens x))))
symbol-listp-merge-symbol<theorem
(defthm symbol-listp-merge-symbol< (implies (and (symbol-listp l1) (symbol-listp l2) (symbol-listp acc)) (symbol-listp (merge-symbol< l1 l2 acc))))
symbol-listp-merge-sort-symbol<theorem
(defthm symbol-listp-merge-sort-symbol< (implies (symbol-listp x) (symbol-listp (merge-sort-symbol< x))))
other
(verify-guards merge-sort-symbol<)