From 547f81711b274591ce075b8df2c3e41c6394eb93 Mon Sep 17 00:00:00 2001 From: Ian Jackson Date: Sat, 7 Jul 2012 17:53:27 +0100 Subject: [PATCH] internal notation: invent \commitmergename and use it everywhere perl -i~ -pe 's/\$\\commitmerge\b\$/\\commitmergename/' *.tex plus the actual definition --- anticommit.tex | 6 +++--- article.tex | 1 + merge.tex | 30 +++++++++++++++--------------- 3 files changed, 19 insertions(+), 18 deletions(-) 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$ diff --git a/article.tex b/article.tex index 7bff692..2253d43 100644 --- a/article.tex +++ b/article.tex @@ -87,6 +87,7 @@ \newcommand{\commitmerge}{{\mathcal M}} \newcommand{\commitmergeof}[4]{\commitmerge(#1,#2,#3,#4)} %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}} +\newcommand{\commitmergename}{${\mathcal M}$} \newcommand{\patch}{{\mathcal P}} \newcommand{\base}{{\mathcal B}} diff --git a/merge.tex b/merge.tex index 9022249..9daaa00 100644 --- a/merge.tex +++ b/merge.tex @@ -79,7 +79,7 @@ is therefore consistent with our model. \subsection{No Replay} -By definition of $\commitmerge$, +By definition of \commitmergename, $D \isin C \implies D \isin L \lor D \isin R \lor D = C$. So, by Ingredients, Ingredients Prevent Replay applies. $\qed$ @@ -135,7 +135,7 @@ $$ $D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L \in \py$ ie $L \haspatch \p$ by Tip Own Contents for $L$). So $D \neq C$. -Applying $\commitmerge$ gives $D \not\isin C$ i.e. $C \nothaspatch \p$. +Applying \commitmergename gives $D \not\isin C$ i.e. $C \nothaspatch \p$. OK. \subsubsection{For $L \haspatch \p, R \haspatch \p$:} @@ -149,17 +149,17 @@ For $D \neq C$: $D \le C \equiv D \le L \lor D \le R (Likewise $D \le C \equiv D \le X \lor D \le Y$.) Consider $D \neq C, D \isin X \land D \isin Y$: -By $\commitmerge$, $D \isin C$. Also $D \le X$ +By \commitmergename, $D \isin C$. Also $D \le X$ so $D \le C$. OK for $C \zhaspatch \p$. Consider $D \neq C, D \not\isin X \land D \not\isin Y$: -By $\commitmerge$, $D \not\isin C$. +By \commitmergename, $D \not\isin C$. And $D \not\le X \land D \not\le Y$ so $D \not\le C$. OK for $C \zhaspatch \p$. Remaining case, wlog, is $D \not\isin X \land D \isin Y$. $D \not\le X$ so $D \not\le M$ so $D \not\isin M$. -Thus by $\commitmerge$, $D \isin C$. And $D \le Y$ so $D \le C$. +Thus by \commitmergename, $D \isin C$. And $D \le Y$ so $D \le C$. OK for $C \zhaspatch \p$. So, in all cases, $C \zhaspatch \p$. @@ -183,26 +183,26 @@ By Tip Own Contents, $L \haspatch \p$ so $L \neq X$, therefore we must have $L=Y$, $R=X$. Conversely $R \not\in \py$ so by Tip Merge $M = \baseof{L}$. Thus $M \in \pn$ so -by Base Acyclic $M \nothaspatch \p$. By $\commitmerge$, $D \isin C$, +by Base Acyclic $M \nothaspatch \p$. By \commitmergename, $D \isin C$, and $D \le C$. OK. Consider $D \neq C, M \nothaspatch \p, D \isin Y$: $D \le Y$ so $D \le C$. -$D \not\isin M$ so by $\commitmerge$, $D \isin C$. OK. +$D \not\isin M$ so by \commitmergename, $D \isin C$. OK. Consider $D \neq C, M \nothaspatch \p, D \not\isin Y$: $D \not\le Y$. If $D \le X$ then $D \in \pancsof{X}{\py}$, so by Addition Merge Ends and Transitive Ancestors $D \le Y$ --- a contradiction, so $D \not\le X$. -Thus $D \not\le C$. By $\commitmerge$, $D \not\isin C$. OK. +Thus $D \not\le C$. By \commitmergename, $D \not\isin C$. OK. Consider $D \neq C, M \haspatch \p, D \isin Y$: $D \le Y$ so $D \in \pancsof{Y}{\py}$ so by Removal Merge Ends and Transitive Ancestors $D \in \pancsof{M}{\py}$ so $D \le M$. -Thus $D \isin M$. By $\commitmerge$, $D \not\isin C$. OK. +Thus $D \isin M$. By \commitmergename, $D \not\isin C$. OK. Consider $D \neq C, M \haspatch \p, D \not\isin Y$: -By $\commitmerge$, $D \not\isin C$. OK. +By \commitmergename, $D \not\isin C$. OK. $\qed$ @@ -242,7 +242,7 @@ $C \haspatch \p$ so by definition of $\haspatch$, $D \isin C \equiv D $D \neq C$. By Tip Contents of $L$, $D \isin L \equiv D \isin \baseof{L}$, so by Tip Merge condition, -$D \isin L \equiv D \isin M$. So by $\commitmerge$, $D \isin +$D \isin L \equiv D \isin M$. So by \commitmergename, $D \isin C \equiv D \isin R$. And $R = \baseof{C}$ by Unique Base of $C$. Thus $D \isin C \equiv D \isin \baseof{C}$. OK. @@ -260,7 +260,7 @@ Whereas if $\baseof{L} = \baseof{M}$, by definition of $\base$, $\patchof{M} = \patchof{L} = \py$, so by Tip Contents of $M$, $D \isin M \equiv D \isin \baseof{M} \equiv D \isin \baseof{L}$. -So $D \isin M \equiv D \isin L$ so by $\commitmerge$, +So $D \isin M \equiv D \isin L$ so by \commitmergename, $D \isin C \equiv D \isin R$. But from Unique Base, $\baseof{C} = \baseof{R}$. Therefore $D \isin C \equiv D \isin \baseof{C}$. OK. @@ -293,17 +293,17 @@ $D \isin C$ and $D \le C$. OK. \subsubsection{For $D \neq C, D \isin M$:} Thus $D \le M$ so $D \le L$ and $D \le R$ so $D \isin L$ and $D \isin -R$. So by $\commitmerge$, $D \isin C$. And $D \le C$. OK. +R$. So by \commitmergename, $D \isin C$. And $D \le C$. OK. \subsubsection{For $D \neq C, D \not\isin M, D \isin X$:} -By $\commitmerge$, $D \isin C$. +By \commitmergename, $D \isin C$. And $D \isin X$ means $D \le X$ so $D \le C$. OK. \subsubsection{For $D \neq C, D \not\isin M, D \not\isin L, D \not\isin R$:} -By $\commitmerge$, $D \not\isin C$. +By \commitmergename, $D \not\isin C$. And $D \not\le L, D \not\le R$ so $D \not\le C$. OK -- 2.30.2