X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?a=blobdiff_plain;f=anticommit.tex;h=49931279917b36872d16a2f179788458ee4a7d17;hb=d29c556b0ebedf4081684216f426b83ee9f04573;hp=39d13e5500c4d268375480aa92a623615c8a0a71;hpb=28bb86cd8218c491ad4fe845c4547af57b1aecb4;p=topbloke-formulae.git diff --git a/anticommit.tex b/anticommit.tex index 39d13e5..4993127 100644 --- a/anticommit.tex +++ b/anticommit.tex @@ -8,7 +8,7 @@ Used for removing a branch dependency. \gathnext \patchof{C} = \patchof{L} \gathnext - \mergeof{C}{L}{R^+}{R^-} + \commitmergeof{C}{L}{R^+}{R^-} \end{gather} \subsection{Conditions} @@ -37,7 +37,7 @@ is a descendant, not an ancestor, of the 2nd parent.) \subsection{No Replay} -By $\merge$, +By \commitmergename, $D \isin C \implies D \isin L \lor D \isin R^- \lor D = C$. So, by Ordering of Ingredients, Ingredients Prevent Replay applies. $\qed$ @@ -67,13 +67,13 @@ So $D \isin R^+$. By Base Acyclic for $R^-$, $D \not\isin R^-$. -Apply $\merge$: $D \not\isin C$. OK. +Apply \commitmergename: $D \not\isin C$. OK. \subsubsection{For $D \neq C, D \le L, D \notin \pry$:} By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$. -Apply $\merge$: $D \isin C \equiv D \isin L$. OK. +Apply \commitmergename: $D \isin C \equiv D \isin L$. OK. $\qed$ @@ -131,7 +131,7 @@ Single Parent Unique Tips applies. $\qed$ \subsection{Foreign Inclusion} -Consider some $D$ s.t. $\isforeign{D}$. $D \neq C$. +Consider some $D \in \foreign$. $D \neq C$. So by Desired Contents $D \isin C \equiv D \isin L$. By Foreign Inclusion of $D$ in $L$, $D \isin L \equiv D \le L$.