  We present a first-order theorem proving framework for establishing the
correctness of functional programs implementing sorting algorithms with
recursive data structures.
  We formalize the semantics of recursive programs in many-sorted first-order
logic and integrate sortedness/permutation properties within our first-order
formalization. Rather than focusing on sorting lists of elements of specific
first-order theories, such as integer arithmetic, our list formalization relies
on a sort parameter abstracting (arithmetic) theories and hence concrete sorts.
We formalize the permutation property of lists in first-order logic so that we
automatically prove verification conditions of such algorithms purely by
superpositon-based first-order reasoning. Doing so, we adjust recent efforts
for automating inducion in saturation. We advocate a compositional approach for
automating proofs by induction required to verify functional programs
implementing and preserving sorting and permutation properties over
parameterized list structures. Our work turns saturation-based first-order
theorem proving into an automated verification engine by (i) guiding automated
inductive reasoning with manual proof splits and (ii) fully automating
inductive reasoning in saturation. We showcase the applicability of our
framework over recursive sorting algorithms, including Mergesort and Quicksort.
