Synthesis of list algorithms by mechanical proving

When the knowledge base does not contain the auxiliary functions needed for the respective version of the algorithm, then the proof fails and from this failure a new proof goal is created, which is the synthesis statement for the missing auxiliary functions (“cascading”).