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.
 
 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}
 
 
 \subsection{Traversal Lemmas}
 

-Firstly, some lemmas.

 \statement{Tip Correct Contents}{
   \tipcy \haspatch \pa E
     \equiv
 \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$
 
 
 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$.