\item For each $i \ldots 1..n$, update our putative direct
dependencies:
$$
-\Gamma \assign \alg{set-merge}\left[\Gamma,
- \left( \begin{cases}
- M_i \in \pcn : & \depsreqof{M_i} \\
- M_i \not\in \pcn : & \{ \}
- \end{cases} \right),
- \depsreqof{S_i}
- \right]
+\Gamma \assign \setmergeof{
+ \Gamma
+ }{
+ \begin{cases}
+ M_i \in \pcn : & \depsreqof{M_i} \\
+ M_i \not\in \pcn : & \{ \}
+ \end{cases}
+ }{
+ \depsreqof{S_i}
+ }
$$
-TODO define $\alg{set-merge}$
+TODO define $\setmerge$
\item Finalise our putative direct dependencies
$
as necessary).
If this results in a cycle, abort entirely (as the function $g$ is
inappropriate; a different $g$ could work).
-\end{enumerate}
\item Run $\alg{Rank-Recurse}(\pd)$.
+\end{enumerate}
\end{enumerate}
\end{itemize}
+\subsection{Proof of termination}
+
+$\alg{Rank-Recurse}(\pc)$ recurses but only downwards through the
+finite graph $\hasdirdep$, so it must terminate.
+
+The whole ranking algorithm iterates but each iteration involves
+adding one or more patches to $\allpatches$. Since there are
+finitely many patches and we never remove anything from $\allpatches$
+this must complete eventually.
+
+$\qed$
+
\section{Traversal phase}
For each patch $C \in \allpatches$ in topological order by $\hasdep$,