\text{ either } C \haspatch \p \text{ or } C \nothaspatch \p
\gathnext
\bigforall_{\py \not\ni C} \pendsof{C}{\py}
+\gathnext
+ \pendsof{C}{\foreign}
\end{gather}
$\patchof{C}$, for each kind of Topbloke-generated commit, is stated
for the ingredients $I$)
in the proof of Coherence for each kind of commit.
-$\pendsof{C}{\py}$ is computed, for all Topbloke-generated commits,
+$\pendsof{C}{\py}$ and $\pendsof{C}{\foreign}$
+are computed, for all Topbloke-generated commits,
using the lemma Calculation of Ends, above.
-We do not annotate $\pendsof{C}{\pay{C}}$ for $C \in \pay{C}$. Doing so would
+We do not annotate $\pendsof{C}{\set S}$ for $C \in \set S$. Doing so would
make it wrong to make plain commits with git because the recorded $\pends$
would have to be updated. The annotation is not needed in that case
-because $\forall_{\pay{C} \ni C} \; \pendsof{C}{\pay{C}} = \{C\}$.
+because $\forall_{\set S \ni C} \; \pendsof{C}{\set S} = \{C\}$.