Literature.
[1] J. Komara. Specification and Verification of Programs. Online.
[2] Ján Kľuka. Úvod do deklaratívneho programovania. Online.
[3] Ján Komara. Recursive Functions. Online.
Insertion sort. Implement insertion sort; that is, define the function such that
with the help of the insertion function .
[CL] Remark. Below we will use the discrimination on whether or not . As we have
we may suppose that the test takes constant time.