\subsection{Tip Self Inpatch}
Given Exclusive Tip Contents and Base Acyclic for $C$,
$$
- \bigforall_{C \in \py} C \haspatch \p
+ \bigforall_{C \in \py} C \haspatch \p \land \neg[ C \nothaspatch \p ]
$$
Ie, tip commits contain their own patch.
\proof{
Apply Exclusive Tip Contents to some $D \in \py$:
$ \bigforall_{C \in \py}\bigforall_{D \in \py}
- D \isin C \equiv D \le C $
+ D \isin C \equiv D \le C $.
+Thus $C \haspatch \p$.
+And, since $C \le C$, $C \isin C$. Therefore $\neg[ C \nothaspatch \p ]$
}
\subsection{Exact Ancestors}