strategy: wip reachable etc.

[topbloke-formulae.git] / trav-proofs.tex

diff --git a/trav-proofs.tex b/trav-proofs.tex
index 67e1b113b696e79de2680381c0df917654b7488a..06a54cfb0521161bd329823d9d685a877c52e30b 100644 (file)
--- a/trav-proofs.tex
+++ b/trav-proofs.tex
@@ -3,6 +3,58 @@
 For each operation called for by the traversal algorithms, we prove
 that the commit generation preconditions are met.
 
 For each operation called for by the traversal algorithms, we prove
 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 \pa E
+    \equiv
+  \pa E = \pc \lor \pa E \isdep \pc
+}
+\proof{
+  For $\pc = \pa E$, Tip Own Contents suffices.
+  For $\pc \neq \pa E$, 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}
+
+We do not prove that the preconditions are met.  Instead, we check
+them at runtime.  If they turn out not to be met, we abandon
+\alg{Merge-Base} and resort to \alg{Recreate-Base}.
+
+TODO COMPLETE MERGE-BASE STUFF
+
+WIP WHAT ABOUT PROVING ALL THE TRAVERSAL RESULTS
+
+\subsection{Recreate Base Beginning}
+
+To recap we are executing Create Base with
+$L = \tipdy$ and $\pq = \pc$.
+
+\subsubsection{Create Acyclic}
+
+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 \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$.
 \subsection{Tip Base Merge}
 
 $L = W$, $R = \tipcn$.