Whether $\baseof{C}$ is required, and if so what the value is, is
stated in the proof of Unique Base for each kind of commit.
Whether $\baseof{C}$ is required, and if so what the value is, is
stated in the proof of Unique Base for each kind of commit.
-$C \haspatch \pa{Q}$ or $\nothaspatch \pa{Q}$ is represented as the
-set $\{ \pa{Q} | C \haspatch \pa{Q} \}$. Whether $C \haspatch \pa{Q}$
+$C \haspatch \pq$ or $\nothaspatch \pq$ is represented as the
+set $\{ \pq | C \haspatch \pq \}$. Whether $C \haspatch \pq$
for the ingredients $I$),
in the proof of Coherence for each kind of commit.
for the ingredients $I$),
in the proof of Coherence for each kind of commit.
using the lemma Calculation of Ends, above.
We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
make it wrong to make plain commits with git because the recorded $\pends$
using the lemma Calculation of Ends, above.
We do not annotate $\pendsof{C}{\py}$ for $C \in \py$. Doing so would
make it wrong to make plain commits with git because the recorded $\pends$
\subsection{Tip Contents}
Consider some arbitrary commit $D$. If $D = C$, trivially satisfied.
If $D \neq C$, $D \isin C \equiv D \isin B$.
\subsection{Tip Contents}
Consider some arbitrary commit $D$. If $D = C$, trivially satisfied.
If $D \neq C$, $D \isin C \equiv D \isin B$.