chiark
/
gitweb
/
~ian
/
topbloke-formulae.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
a1bcf34
)
move merge X and Y def up
author
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Tue, 6 Mar 2012 17:29:22 +0000
(17:29 +0000)
committer
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Tue, 6 Mar 2012 17:29:22 +0000
(17:29 +0000)
article.tex
patch
|
blob
|
history
diff --git
a/article.tex
b/article.tex
index 3db83bfeec3b23a2adf57dfe5548411873f4051b..a0adacbdee9b8d02bb1f2421f8158b1a43b505b2 100644
(file)
--- a/
article.tex
+++ b/
article.tex
@@
-474,6
+474,7
@@
Merge commits $L$ and $R$ using merge base $M$ ($M < L, M < R$):
\gathnext
\mergeof{C}{L}{M}{R}
\end{gather}
\gathnext
\mergeof{C}{L}{M}{R}
\end{gather}
+We will occasionally use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
\subsection{Conditions}
\subsection{Conditions}
@@
-531,8
+532,6
@@
$\qed$
Need to determine $C \haspatch P$ based on $L,M,R \haspatch P$.
This involves considering $D \in \py$.
Need to determine $C \haspatch P$ based on $L,M,R \haspatch P$.
This involves considering $D \in \py$.
-We will use $X,Y$ s.t. $\{X,Y\} = \{L,R\}$.
-
\subsubsection{For $L \nothaspatch P, R \nothaspatch P$:}
$D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
\in \py$ ie $L \haspatch P$ by Tip Self Inpatch). So $D \neq C$.
\subsubsection{For $L \nothaspatch P, R \nothaspatch P$:}
$D \not\isin L \land D \not\isin R$. $C \not\in \py$ (otherwise $L
\in \py$ ie $L \haspatch P$ by Tip Self Inpatch). So $D \neq C$.