From: Ian Jackson Date: Sun, 4 Aug 2013 18:19:24 +0000 (+0100) Subject: merge: prove bases' children X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=commitdiff_plain;h=f58dec73ac7e656f88ff6e23f3e635c96286ae77 merge: prove bases' children --- diff --git a/merge.tex b/merge.tex index 9daaa00..5bb0db2 100644 --- a/merge.tex +++ b/merge.tex @@ -27,6 +27,16 @@ satisfied; in particular, provided that $L \ge \baseof{R}$. \text{otherwise} : & \false \end{cases} }\] +$\eqn{ Base Merge }{ + L \in \pn \implies + \big[ + R \in \pn + \lor + R \in \foreign + \lor + R \in \pqy + \big] +}$ \[ \eqn{ Merge Acyclic }{ L \in \pn \implies @@ -314,3 +324,24 @@ $\qed$ Only relevant if $\isforeign{L}$, in which case $\isforeign{C}$ and by Foreign Merges $\isforeign{R}$, so Totally Foreign Contents applies. $\qed$ + +\subsection{Bases' Children} + +If $L \in \py, R \in \py$: not applicable for either $D=L$ or $D=R$. + +If $L \in \py, R \in \pn$: not applicable for $L$, OK for $R$. + +Other possibilities for $L \in \py$ are excluded by Tip Merge. + +If $L \in \pn, R \in \pn$: satisfied for both $L$ and $R$. + +If $L \in \pn, R \in \foreign$: satisfied for $L$, not applicable for +$R$. + +If $L \in \pn, R \in \pqy$: satisfied for $L$, not applicable for +$R$. + +Other possibilities for $L \in \pn$ are excluded by Base Merge. + +If $L \in \foreign$: not applicable for $L$; nor for $R$, by Foreign Merges. +