From ad178f973fea2cc5483a55f6dc84599277cbf39b Mon Sep 17 00:00:00 2001
From: Ian Jackson <ijackson@chiark.greenend.org.uk>
Date: Sun, 8 Jul 2012 00:40:14 +0100
Subject: [PATCH] traversal: wip Recreate Base Final Declaration

---
 trav-proofs.tex | 10 ++++++++++
 1 file changed, 10 insertions(+)

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