From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Sun, 11 Mar 2012 12:07:19 +0000 (+0000)
Subject: anticommit base acyclic
X-Git-Tag: f0.2~100
X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?a=commitdiff_plain;h=f2495efb49a64ea535aab56e9070c06fd9f4dc58;p=topbloke-formulae.git

anticommit base acyclic
---

diff --git a/article.tex b/article.tex
index 0688c7a..33a0846 100644
--- a/article.tex
+++ b/article.tex
@@ -488,9 +488,13 @@ applicable. $\qed$
 
 Again, not applicable. $\qed$
 
-xxx tbd
+\subsection{Base Acyclic}
 
-xxx need to finish anticommit
+By Base Acyclic for $L$, $D \isin L \implies D \not\in \py$.
+And by From Base $C \not\in \py$.
+Now from Desired Contents, above, $D \isin C
+\implies D \isin L \lor D = C$, which thus
+$\implies D \not\in \py$.  $\qed$.
 
 \section{Merge}