---

1.3.1 The balancing algorithm

The balancing algorithm given in Boehm et al (1995) is described as follows. We have an infinite sequence of bins, each labeled with Fibonacci number corresponding to its index. We process the leaves of the rope from left-to-right: A leaf of length ℓ is placed into the bin with index d such that Fib(d) ≤ ℓ < Fib(d+1) if the bin is empty, and if not, all the contents of the bin and the bins with smaller indices are concatenated into a single rope, that is then concatenated with the leaf; finally the resulting rope has a new length ℓ', and the process repeats with this new rope: find the corresponding bin indexed by d' for which Fib(d') ≤ ℓ' < Fib(d' + 1) and so on. At some point this process will stop, and we can move on to the next leaf of the rope. In the end, we concatenate all contents of the bins into a single rope, which will be balanced!

To understand why that is true, we present a few invariant properties that hold in between each iteration of the algorithm described above.

1. Each bin is empty or has one element.
2. The length of that element is less than the label of the next bin, but larger or equal to the label of its host bin.
3. The ropes (and strings) are in decreasing order, meaing that the contents of the higher-indexed bins are coming before (in order of appearance in the represented total string) those of lower-indexed bins.
4. The ropes inside the bins are balanced.
5. The feeding process modifies the bins and places a rope in the bins that respects all of the above.

Critically, in order to prove the second point, we need the Fibonacci function to be involved!