		Search-engine friendly clone of the ACL2 documentation.

Insertion-sort-of-integers-from-to

Applying insertion sort to an ordered list of integers in a range yields the same list.

This should be moved to a more general library.

Definitions and Theorems

Theorem: insertion-sort-of-integers-from-to

(defthm insertion-sort-of-integers-from-to
  (implies (and (integerp min) (integerp max))
           (equal (insertion-sort (integers-from-to min max))
                  (integers-from-to min max))))