strategy: reachable is going well

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

diff --git a/trav-proofs.tex b/trav-proofs.tex
index b4b483cca9e01bd3627b11862cf5228f6c29d1be..421bb61c296fb8979b9d0744f067921eed0c0e0d 100644 (file)
--- a/trav-proofs.tex
+++ b/trav-proofs.tex
@@ -3,11 +3,34 @@
 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{Reachability and coverage}
+
+We ensure Tip Covers Reachable as follows:
+
+\begin{itemize}
+\item  We do not generate any commits $\in \py$ other than
+       during $\alg{Merge-Tip}(\py)$;
+\item  So at the start of $\alg{Merge-Tip}(\py)$,
+       $ \pendsof{\allreach}{\py} = \pendsof{\allsrcs}{\py} $
+\item  $\alg{Merge-tip}$ arranges that when it is done
+       $\tippy \ge \pendsof{\allreach}{\py}$ --- see below.
+\end{itemize}
+
+A corrolary is as follows:
+\statement{Tip Covers Superior Reachable} {
+  \bigforall_{\pd \isdep \pc}
+    \tipdy \ge \pendsof{\allreachof{\pcy}}{\pdy}
+}
+\proof{
+  No commits $\in \pdy$ are created other than during
+  $\alg{Merge-Tip}(\pd)$, which runs (and has thus completed)
+  before $\alg{Merge-Tip}(\pcy)$
+  So $\pendsof{\allreachof{\pcy}}{\pdy} =
+      \pendsof{\allreachof{\pdy}}{\pdy}$.
+}
 
 \subsection{Traversal Lemmas}
 
-Firstly, some lemmas.
 \statement{Tip Correct Contents}{
   \tipcy \haspatch \pa E
     \equiv
@@ -45,6 +68,16 @@ $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$.