From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Sat, 7 Jul 2012 23:40:14 +0000 (+0100)
Subject: traversal: wip Recreate Base Final Declaration
X-Git-Url: https://www.chiark.greenend.org.uk/ucgi/~ian/git?a=commitdiff_plain;h=ad178f973fea2cc5483a55f6dc84599277cbf39b;p=topbloke-formulae.git

traversal: wip Recreate Base Final Declaration
---

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$.