From: Ian Jackson Date: Sat, 7 Jul 2012 23:05:10 +0000 (+0100) Subject: traversal: proof of Tip Correct Contents X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=commitdiff_plain;h=d5836b17ce78e4f79f38325cdb1ce20f29c881ca traversal: proof of Tip Correct Contents --- diff --git a/trav-alg.tex b/trav-alg.tex index 8a9a68a..210b20b 100644 --- a/trav-alg.tex +++ b/trav-alg.tex @@ -32,7 +32,7 @@ such that: \statement{Base Correct Contents}{ \tipcn \haspatch \pd \equiv - \pc \hasdep \pd + \pd \isdep \pc } \statement{Tip Exceeds Inputs}{ \tipcy \ge \pendsof{\allsrcs}{\pcy} diff --git a/trav-proofs.tex b/trav-proofs.tex index 3c2a175..876525d 100644 --- a/trav-proofs.tex +++ b/trav-proofs.tex @@ -8,14 +8,16 @@ WIP WHAT ABOUT PROVING ALL THE TRAVERSAL RESULTS \subsection{Traversal Lemmas} Firstly, some lemmas. - \statement{Tip Correct Contents}{ \tipcy \haspatch \pd \equiv - \pc = \pd \lor \pc \hasdep \pd + \pd = \pc \lor \pd \isdep \pc } \proof{ - WIP + For $\pc = \pd$, Tip Own Contents suffices. + For $\pc \neq \pd$, Exclusive Tip Contents + gives $D \isin \tipcy \equiv D \isin \baseof{\tipcy}$ + which by Correct Base $\equiv D \isin \tipcn$. } \subsection{Base Dependency Merge, Base Sibling Merge}