Synthesis of Merging algorithms on binary trees using multisets in Theorema

We present the principles and the experiments of deduction based synthesis of merging algorithms for binary trees. Merging is an auxiliary function used in certain algorithms for sorting of binary trees, however we also address concatenation of unsorted trees (the result will also be in general not sorted) as well as merging of sorted trees (both inputs as well as the output are sorted). We follow...