X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=create-base.tex;h=cc99af8e489d3e65db8264d5f55e01026684c668;hp=800fcd7faf08042c7bbb7406d5155fb9bef79bb4;hb=294a235fb0c1167d1101866cb35f41ddfabc287b;hpb=815e77b8814aa78d2af65676cc7e87449e1b6e7f diff --git a/create-base.tex b/create-base.tex index 800fcd7..cc99af8 100644 --- a/create-base.tex +++ b/create-base.tex @@ -13,7 +13,10 @@ create a Topbloke base branch initial commit $B$. \subsection{Conditions} \[ \eqn{ Create Acyclic }{ - \pendsof{L}{\pqy} = \{ \} + L \nothaspatch \pq +}\] +\[ \eqn{ Ingredients }{ + \patchof L = \foreign \lor \patchof L = \py }\] \subsection{No Replay} @@ -31,8 +34,7 @@ Not applicable. \subsection{Base Acyclic} Consider some $D \isin B$. If $D = B$, $D \in \pqn$. -If $D \neq B$, $D \isin L$, so by No Replay $D \le L$ -and by Create Acyclic +If $D \neq B$, $D \isin L$, so by Create Acyclic $D \not\in \pqy$. $\qed$ \subsection{Coherence and Patch Inclusion} @@ -54,7 +56,11 @@ Single Parent Unique Tips applies. $\qed$ Simple Foreign Inclusion applies. $\qed$ -\subsection{Foreign Contents} +\subsection{Foreign Ancestry} Not applicable. +\subsection{Bases' Children} + +Not applicable, by Ingredients. +