Another simple example is the construction of a Quicksort program sort(L), which sorts the elements of a list L **according to a given order** relation "x < y" (x is less than y) between any elements x and y of L**. The**
core of such a program can be represented by the functional pseudocode

$$\begin{array}{c}{{a p p e n d(s o r t(x\in L:x<f i r s t(L)),}}\\ {{f i r s t(L),}}\\ {{s o r t(x\in L:f i r s t(L)<x))),}}\end{array}$$
$$\left(1\right)$$

where the append function appends lists and first(L**) is the first element of**
a list L. In order to sort a list L**, the program (1) sorts the elements** x ∈ L
that are less than its first element first(L) and the elements x ∈ L **that are** greater than first(L**). The recursive application of this "divide-and-conquer"**
strategy yields smaller and smaller partial lists or empty lists which need not be sorted. Finally, the program (1) generates a sorted list containing all elements of L **by successively appending all partial lists previously sorted.**
The Quicksort program (1) can also be constructed on the basis of **elementary knowledge about the functions it contains. Roughly speaking, this**
knowledge need merely give the domains and ranges of the functions, that is, the sets on which the functions are defined and the sets of values the functions may take on. For example, the proposition x < first(L**) in (1)** can be constructed on the basis of the knowledge that first(L**) is an element**
of L and x < y is a proposition for any elements x ∈ L and y ∈ L**. An**
efficient selection of the functions used in the Quicksort program (1) seems feasible because they are very elementary such as the append **function or even**
explicitly contained in the programming task such as the order relation "<".

For example, the SHUNYATA program generated theorem-proving **programs by analyzing proofs of simple theorems on the basis of elementary**
knowledge about the functions the programs are composed of [1]. The development of these programs illustrates very simple aspects of the **principles**
given above, for example, the unification of analytical spaces and the generation of economical variations. The theorem-proving programs **developed**
by SHUNYATA generated proofs of further theorems, in particular, a proof of SAM's Lemma which is simpler than any proof known before. The complexity of SAM's Lemma more or less represented the state of the art in automated theorem proving [1, p. 561].

G¨odel's incompleteness theorem says that every formal number theory contains an undecidable formula, that is, neither the formula nor its **negation**