Every call of the \<Refill> procedure spends time $\O(1)$ amortized.
\proof
-Every call of \<Refill> can be split to the bottom part (rank~$r$ and below) and the
-upper part. Whenever we recurse on the bottom part when processing the upper one,
-we spend at most~$\O(r)$ time there. We will show that
-
-We will prove that all refills together take time $\O(nr)$, which will be charged on the
+When \<Refill> is called from the \<DeleteMin> operation, it recurses on a~subtree of the
+queue. This subtree can be split to the ``lossless'' lower part (rank~$r$ and below)
+and the upper part where list concatenation and thus also corruption takes place. Whenever
+we visit the lower part during the recursion, we spend at worst $\O(r)$ time there.
+We will prove that the total time spent in the upper parts during the whole life of the
+data structure is $\O(n)$. Since each upper vertex can perform at most two calls to the lower
+part, the total time spent in the lower parts is $\O(rn)$. All this can be pre-paid by the
inserts.
+Let us focus on the upper part. There are three possibilities of what can happen
+when we visit a~vertex:
+
+\itemize\ibull
+
+\:We delete it: Every vertex deleted has to have been created at some time in the past.
+New vertices are created only during inserts and melds (when joining two trees) and
+we have already shown that these operations have constant amortized complexity. So the
+same must hold for deletions.
+
+\:We recurse twice and concatenate the lists: The lists are disassembled only when
+they reach the root of the tree, otherwise they are only concatenated. We can easily
+model the situation by a~binary tree forest similar to the meld forest. There are~$n$
+leaves and every internal vertex has outdegree two, so the total number of concatenations
+is at most~$n$. Each of them can be performed in constant time as the list is doubly linked.
+
+\:We recurse only once: This occurs only if the rank is even and the gap between the
+rank of this vertex and its sons is small. It therefore cannot happen twice in a~row,
+so it is clearly dominated by the other possibilities.
+
+\endlist
+\>The total cost of all operations on the upper part is therefore $\O(n)$.
+\qed
+
+It remains to analyse the rest of the \<DeleteMin> operation.
+
+\lemma
+Every \<DeleteMin> takes $\O(1)$ time amortized.
+
+\proof
\qed
\endpart