\section{Roadmap of the appendix}\label{app:roadmap}

The appendix contains the full proofs of all results of the main text, in the order of the sections, and
ends with a table of notation. \Cref{fig:dependency} shows how the results depend on each other.

\begin{figure}[h]
\centering
\IfFileExists{figs/fig_dependency.pdf}{\includegraphics[width=\linewidth]{figs/fig_dependency.pdf}}{\fbox{dependency graph}}
\caption{Dependencies between the results. An arrow from $X$ to $Y$ means that the proof of $Y$ cites $X$,
after transitive reduction. Dashed frames mark imported theorems, thick frames mark the main theorems,
and hypotheses are not drawn. \Cref{thm:accbarrier,prop:fas} use no other result.}
\label{fig:dependency}
\end{figure}

\paragraph{How to read the proofs.}
We write the proofs in the structured style of Lamport~\cite{Lam95,Lam12}. A proof is a list of numbered
steps, and $\pflab{k}{j}$ is the $j$-th step at level $k$. Each step states a claim, and a proof of the
claim follows it. This proof is a short paragraph or a list of steps at the next level. The last step of
each list, \textsc{q.e.d.}, proves the goal of the list from the earlier steps. \textsc{Assume} and
\textsc{Prove} state the hypothesis and the goal of a step, \textsc{Let} introduces a symbol, and
\textsc{Case} marks one case of a case split. A reader who wants only the main idea can read the level-1
steps and skip their proofs. Each restated result keeps its number from the main text.