3 Given $L$ and some other commits $\set R$, generate a
4 `fake merge': i.e., a commit which is a descendant of $L$ and $\set R$
5 but whose contents are exactly those of $L$.
8 C \hasparents \{ L \} \cup \set R
10 \patchof{C} = \patchof{L}
12 D \isin C \equiv D \isin L \lor D = C
15 \subsection{Conditions}
21 \[ \eqn{ Ingredients }{
22 \bigforall_{R \in \set R}
30 \[ \eqn{ Unique Tips }{
31 C \haspatch \p \implies
33 \pendsof{C}{\py} = \{ T \}
36 \[ \eqn{ Foreign Unaffected }{
37 \pendsof{C}{\foreign} = \pendsof{L}{\foreign}
40 \subsection{Lemma: Foreign Identical}
42 $\isforeign{D} \implies \big[ D \le C \equiv D \le L \big]$.
45 Trivial by Foreign Unaffected and the definition of $\pends$
48 It might seem that bare git commits might also be psuedo-merges ---
49 e.g., merges made directly with {\tt git merge -s ours}. However, by
50 our definition of $\has$, these are considered simply as normal merges
51 (\autoref{commit-merge}).
53 \subsection{No Replay}
55 Ingredients Prevent Replay applies:
56 $A = L$ always satisfies the $\exists$. $\qed$
58 \subsection{Unique Base}
60 Not applicable, by Base Only.
62 \subsection{Tip Contents}
64 Not applicable, by Base Only.
66 \subsection{Base Acyclic}
68 Relevant only if $L \in \pn$. For $D = C$, $D \in \pn$; OK.
69 For $D \neq C$, OK by Base Acyclic for $L$. $\qed$
71 \subsection{Coherence and Patch Inclusion}
75 L \haspatch \p : & C \haspatch \p \\
76 L \nothaspatch \p : & C \nothaspatch \p
81 Consider some $D \in \py$. $D \neq C$ by Base Only.
82 So $C \has \p \equiv L \has \p$.
85 \subsection{Unique Tips}
87 Explicitly dealt with by our Unique Tips condition.
89 \subsection{Foreign Inclusion}
91 We need to consider $D \in \foreign$.
93 For $D = C$: $D \has C$, $D \le C$; OK.
95 For $D \neq C$: $D \has C \equiv D \has L$ by construction.
96 $D \has L \equiv D \le L$ by Foreign Inclusion of $L$.
97 $D \neq C$ so this $D \le L \equiv D \le C$.
101 \subsection{Foreign Ancestry}
105 \subsection{Bases' Children}
107 We need to consider this for $D=L$ and also for $D=R$ ($R \in \set
110 For $D=L$: $L \in \pn$ so $\pd = \p$. And $C \in \pn = \pdn$. Bases'
111 Children applies and is satisfied.
113 For $D = R \in \set R, R \in \pn$: $D \in \pn, \pd = \p, C \in \pn$ as
116 For $D = R \in \set R, R \in \foreign$, or $R \in \pqy$: $D \not\in
117 \pdn$ so Bases' Children does not apply.
119 Other possibilities for $D \in \set R$ are excluded by Ingredients.