chiark
/
gitweb
/
~ian
/
topbloke-formulae.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
| inline |
side by side
(parent:
bad4f62
)
traversal: wip Recreate Base Final Declaration
author
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Sat, 7 Jul 2012 23:40:14 +0000
(
00:40
+0100)
committer
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Sat, 7 Jul 2012 23:40:14 +0000
(
00:40
+0100)
trav-proofs.tex
patch
|
blob
|
history
diff --git
a/trav-proofs.tex
b/trav-proofs.tex
index b4b483cca9e01bd3627b11862cf5228f6c29d1be..06a54cfb0521161bd329823d9d685a877c52e30b 100644
(file)
--- 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$.