X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=anticommit.tex;h=49931279917b36872d16a2f179788458ee4a7d17;hp=ee23c7f40b141f6a655aca1be2882c291ddea522;hb=504314d4eb8beba3ea97850f02e89500bfd9b2bf;hpb=e938c1413dba5cf8dc107871664216d269950b69 diff --git a/anticommit.tex b/anticommit.tex index ee23c7f..4993127 100644 --- a/anticommit.tex +++ b/anticommit.tex @@ -37,7 +37,7 @@ is a descendant, not an ancestor, of the 2nd parent.) \subsection{No Replay} -By $\commitmerge$, +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 $\commitmerge$: $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 $\commitmerge$: $D \isin C \equiv D \isin L$. OK. +Apply \commitmergename: $D \isin C \equiv D \isin L$. OK. $\qed$