From: Ian Jackson Date: Sat, 7 Jul 2012 22:26:16 +0000 (+0100) Subject: traversal: wip prove Recreate Base Beginning OK, currently need to prove Tip Correct... X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=commitdiff_plain;h=d29c556b0ebedf4081684216f426b83ee9f04573 traversal: wip prove Recreate Base Beginning OK, currently need to prove Tip Correct Contents --- diff --git a/trav-alg.tex b/trav-alg.tex index abe2441..8a9a68a 100644 --- a/trav-alg.tex +++ b/trav-alg.tex @@ -29,6 +29,11 @@ such that: \statement{Correct Base}{ \baseof{\tipcy} = \tipcn } +\statement{Base Correct Contents}{ + \tipcn \haspatch \pd + \equiv + \pc \hasdep \pd +} \statement{Tip Exceeds Inputs}{ \tipcy \ge \pendsof{\allsrcs}{\pcy} } @@ -97,7 +102,7 @@ Choose a $\hasdep$-maximal direct dependency $\pd$ of $\pc$. \item -Use $\alg{Create Base}$ with $L$ = $\pdy,\; \pq = \pc$ to generate $C$ +Use $\alg{Create Base}$ with $L$ = $\tipdy,\; \pq = \pc$ to generate $C$ and set $W \iassign C$. (Recreate Base Beginning.) \item diff --git a/trav-proofs.tex b/trav-proofs.tex index 981483e..3c2a175 100644 --- a/trav-proofs.tex +++ b/trav-proofs.tex @@ -5,6 +5,19 @@ that the commit generation preconditions are met. 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 +} +\proof{ + WIP +} + \subsection{Base Dependency Merge, Base Sibling Merge} We do not prove that the preconditions are met. Instead, we check @@ -17,8 +30,9 @@ WIP WHAT ABOUT PROVING ALL THE TRAVERSAL RESULTS \subsection{Recreate Base Beginning} -WHAT IF $\pendsof{L}{\pqy} \neq \{\}$ ? -FIX BY CHANGE PRECOND OF CREATE BASE +\subsubsection{Create Acyclic} + +$L = \tipdy$ so \subsection{Tip Base Merge}