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:
63b8fab
)
traversal: Prove Recreate Base Beginning - done
author
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Sat, 7 Jul 2012 23:28:40 +0000
(
00:28
+0100)
committer
Ian Jackson
<ijackson@chiark.greenend.org.uk>
Sat, 7 Jul 2012 23:28:40 +0000
(
00:28
+0100)
trav-proofs.tex
patch
|
blob
|
history
diff --git
a/trav-proofs.tex
b/trav-proofs.tex
index 0a2d49127eb06a1d7c46e3ae8ad028955d27dd29..b4b483cca9e01bd3627b11862cf5228f6c29d1be 100644
(file)
--- a/
trav-proofs.tex
+++ b/
trav-proofs.tex
@@
-41,7
+41,9
@@
By Tip Correct Contents of $L$,
$L \haspatch \pa E \equiv \pa E = \pd \lor \pa E \isdep \pd$.
Now $\pd \isdirdep \pc$,
so by Coherence, and setting $\pa E = \pc$,
$L \haspatch \pa E \equiv \pa E = \pd \lor \pa E \isdep \pd$.
Now $\pd \isdirdep \pc$,
so by Coherence, and setting $\pa E = \pc$,
-$L \nothaspatch \pc$. I.e. $L \nothaspatch \pq$. $\qed$
+$L \nothaspatch \pc$. I.e. $L \nothaspatch \pq$. OK.
+
+That's everything for Create Base. $\qed$
\subsection{Tip Base Merge}
\subsection{Tip Base Merge}