X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?a=blobdiff_plain;f=trav-proofs.tex;h=06a54cfb0521161bd329823d9d685a877c52e30b;hb=ad178f973fea2cc5483a55f6dc84599277cbf39b;hp=b4b483cca9e01bd3627b11862cf5228f6c29d1be;hpb=bad4f62b80ab375d478d5ad59908dfb194b944e7;p=topbloke-formulae.git

diff --git a/trav-proofs.tex b/trav-proofs.tex
index b4b483c..06a54cf 100644
--- a/trav-proofs.tex
+++ b/trav-proofs.tex
@@ -45,6 +45,16 @@ $L \nothaspatch \pc$. I.e. $L \nothaspatch \pq$. OK.
 
 That's everything for Create Base.  $\qed$
 
+\subsection{Recreate Base Final Declaration}
+
+\subsubsection{Base Only} $\patchof{W} = \patchof{L} = \pn$.  OK.
+
+\subsubsection{Unique Tips}
+
+Want to prove that for any $\p \isin C$, $\tipdy$ is a suitable $T$.
+
+WIP
+
 \subsection{Tip Base Merge}
 
 $L = W$, $R = \tipcn$.