chiark
/
gitweb
/
~ian
/
topbloke-formulae.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
traversal: Base/Tip Correct Contents chane notation
[topbloke-formulae.git]
/
trav-proofs.tex
diff --git
a/trav-proofs.tex
b/trav-proofs.tex
index 876525dd7253d56f8963a23d41f6d71f02a1a52e..f1993d31191fa6ec9798dc9a00bca0903540cc98 100644
(file)
--- a/
trav-proofs.tex
+++ b/
trav-proofs.tex
@@
-9,13
+9,13
@@
WIP WHAT ABOUT PROVING ALL THE TRAVERSAL RESULTS
Firstly, some lemmas.
\statement{Tip Correct Contents}{
Firstly, some lemmas.
\statement{Tip Correct Contents}{
- \tipcy \haspatch \p
d
+ \tipcy \haspatch \p
a E
\equiv
\equiv
- \p
d = \pc \lor \pd
\isdep \pc
+ \p
a E = \pc \lor \pa E
\isdep \pc
}
\proof{
}
\proof{
- For $\pc = \p
d
$, Tip Own Contents suffices.
- For $\pc \neq \p
d
$, Exclusive Tip Contents
+ For $\pc = \p
a E
$, Tip Own Contents suffices.
+ For $\pc \neq \p
a E
$, Exclusive Tip Contents
gives $D \isin \tipcy \equiv D \isin \baseof{\tipcy}$
which by Correct Base $\equiv D \isin \tipcn$.
}
gives $D \isin \tipcy \equiv D \isin \baseof{\tipcy}$
which by Correct Base $\equiv D \isin \tipcn$.
}