Revert all "wip dependency insertion"

This is actually a subcase of Merge.

Revert "wip dependency insertion"

This reverts commit 12818e0da31738adbaecf129c1e697633d371cf8.

Revert "wip dependency insertion"

This reverts commit c39f3f1f5a5df2a4d628f335f7aaad44c0f68913.

Revert "wip dependency insertion"

This reverts commit e41fe6dd695b0354aa46929828f0d4ffd604f643.

Revert "wip dependency insertion"

This reverts commit 2e2c0cd70b9a6819e2289a7b07addb6e19f5012c.

Revert "wip dependency insertion"

This reverts commit d357159ce17651ed7deba459e32400636973b827.

Revert "wip dependency insertion"

This reverts commit c759fdf5965e18b0fc6f713b22526ec9464ed7f7.

Revert "wip dependency insertion"

This reverts commit de686ee8ee88dade41eb58f604a89f901b3a13a1.

Revert "wip dependency insertion"

This reverts commit fc96ba0c73d771839a025fc5cb771554cf178eaa.

diff --git a/article.tex b/article.tex
index 0ed90a67314921007898565e28874630769e8908..e1d47123d04fc3a9bfb2d37437e12e1bf132f171 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -789,125 +789,6 @@ $\qed$
 
 Not applicable.
 
 
 Not applicable.
 

-\section{Dependency Insertion}
-
-Given $L$ construct $C$ which additionally
-contains $\pr$ as represented by $R^+$ and $R^-$.
-This may even be used for reintroducing a previous-removed branch
-dependency.
-\gathbegin
- C \hasparents \{ L, R^+ \}
-\gathnext
- \patchof{C} = \patchof{L}
-\gathnext
- \mergeof{C}{L}{R^-}{R^+}
-\end{gather}
-
-\subsection{Conditions}
-
-\[ \eqn{ Ingredients }{
- R^- = \baseof{R^+}
-}\]
-\[ \eqn{ Into Base }{
- L \in \pqn
-}\]
-\[ \eqn{ Currently Excluded }{
- L \nothaspatch \pr
-}\]
-\[ \eqn{ Inserted's Ends }{
- E \in \pendsof{L}{\pry} \implies E \le R^+
-}\]
-\[ \eqn{ Others' Ends }{
- \bigforall_{\p \patchisin \L}
- E \in \pendsof{R^+}{\py} \implies E \le L
-}\]
-\[ \eqn{ Insertion Acyclic }{
- R^+ \nothaspatch \pq
-}\]
-
-\subsection{No Replay}
-
-By $\merge$,
-$D \isin C \implies D \isin L \lor D \isin R^+ \lor D = C$.
-So Ingredients Prevent Replay applies. $\qed$
-
-\subsection{Unique Base}
-
-Not applicable.
-
-\subsection{Tip Contents}
-
-Not applicable.
-
-\subsection{Base Acyclic}
-
-Consider some $D \isin C$.  We will show that $D \not\in \pqy$.
-By $\merge$, $D \isin L \lor D \isin R^+ \lor D = C$.
-
-For $D \isin L$, Base Acyclic for L suffices.  For $D \isin R^+$,
-Insertion Acyclic suffices.  For $D = C$, trivial.  $\qed$.
-
-\subsection{Coherence and Patch Inclusion}
-
-$$
-\begin{cases}
-  \p = \pr    \lor L \haspatch \p : & C \haspatch \p \\
-  \p \neq \pr \land L \nothaspatch \p : & C \nothaspatch \p
-\end{cases}
-$$
-\proofstarts
-~ Consider some $D \in \py$.
-$D \neq C$ so $D \le C \equiv D \le L \lor D \le R^+$.
-
-\subsubsection{For $\p = \pr$:}
-
-$D \not\isin L$ by Currently Excluded.
-$D \not\isin R^-$ by Base Acyclic.
-So by $\merge$, $D \isin C \equiv D \isin R^+$,
-which by Tip Self Inpatch of $R^+$, $\equiv D \le R^+$.
-
-And by definition of $\pancs$,
-$D \le L \equiv D \in \pancsof{L}{R^+}$.
-Applying Transitive Ancestors to Inserted's Ends gives
-$A \in \pancsof{L}{R^+} \implies A \le R^+$.
-So $D \le L \implies D \le R^+$.
-Thus $D \le C \equiv D \le R^+$.
-
-So $D \isin C \equiv D \le C$, i.e. $C \haspatch \pr$.
-OK.
-
-\subsubsection{For $\p \neq \pr$:}
-
-By Exclusive Tip Contents for $R^+$ ($D \not\in \pry$ case)
-$D \isin R^+ \equiv D \isin R^-$.
-So by $\merge$, $D \isin C \equiv D \isin L$.
-
-If $L \nothaspatch \p$, $D \not\isin L$ so $C \nothaspatch \p$.  OK.
-
-If $L \haspatch \p$, Others' Ends applies; by Transitive
-Ancestors, $A \in \pancsof{R^+}{\py} \implies A \le L$.
-So $D \le R^+ \implies D \le L$,
-since $D \le R^+ \equiv D \in \pancsof{R^+}{\py}$.
-Thus $D \le C \equiv D \le L$.
-And by $\haspatch$, $D \le L \equiv D \isin L$ so
-$D \isin C \equiv D \le C$.  Thus $C \haspatch \p$.
-OK.
-
-$\qed$
-
-\subsection{Foreign Inclusion}
-
-Consider some $D$ s.t. $\patchof{D} = \bot$.
-
-By Tip Contents for $R^+$, $D \isin R^+ \equiv D \isin R^-$.
-So by $\merge$, $D \isin C \equiv D \isin L$.
-
-xxx up to here, need new condition
-
-$D \neq C$.
-
-
-

 \section{Merge}
 
 Merge commits $L$ and $R$ using merge base $M$:
 \section{Merge}
 
 Merge commits $L$ and $R$ using merge base $M$: