wip traversal

diff --git a/trav-alg.tex b/trav-alg.tex
index 8cbaa9a2cfae6a5f56c4489ac4ff35b27cd01eae..9e5197e1a65378f672d83efd2e6a7b0f52bcec7f 100644 (file)
--- a/trav-alg.tex
+++ b/trav-alg.tex
@@ -69,7 +69,7 @@ In some order, perhaps interleaving the two kinds of merge:
 \item For each $\hasdep$-maximal $\pd \isdirdep \pc$, find a merge base
 $M \le W,\; \le \tipdy$ and merge $\tipdy$ into $W$.
 That is, use $\alg{Merge}$ with $L = W,\; R = \tipdy$.
 \item For each $\hasdep$-maximal $\pd \isdirdep \pc$, find a merge base
 $M \le W,\; \le \tipdy$ and merge $\tipdy$ into $W$.
 That is, use $\alg{Merge}$ with $L = W,\; R = \tipdy$.

-(Dependency Merge.)
+(Base Dependency Merge.)

 
 \item For each $S \in S^{\pcn}_i$, merge it into $W$.
 That is, use $\alg{Merge}$ with $L = W,\; R = S,\; M = M^{\pcn}_i$.
 
 \item For each $S \in S^{\pcn}_i$, merge it into $W$.
 That is, use $\alg{Merge}$ with $L = W,\; R = S,\; M = M^{\pcn}_i$.


@@ -81,6 +81,9 @@ That is, use $\alg{Merge}$ with $L = W,\; R = S,\; M = M^{\pcn}_i$.
 
 Execute $\alg{Fixup-Base}(W,\pc)$.
 
 
 Execute $\alg{Fixup-Base}(W,\pc)$.
 

+\subsubsection{Result}
+
+If all of that was successful, let $\tipcn = W$.

 
 \subsection{$\alg{Recreate-Base}(\pc)$}
 
 
 \subsection{$\alg{Recreate-Base}(\pc)$}
 

diff --git a/trav-proofs.tex b/trav-proofs.tex
index 67e1b113b696e79de2680381c0df917654b7488a..415c939b0b03c9675a7dcfa9bfde517fee3de6ab 100644 (file)
--- a/trav-proofs.tex
+++ b/trav-proofs.tex
@@ -3,6 +3,14 @@
 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.
 

+\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}.
+
+WIP WHAT ABOUT PROVING ALL THE TRAVERSAL RESULTS
+

 \subsection{Tip Base Merge}
 
 $L = W$, $R = \tipcn$.
 \subsection{Tip Base Merge}
 
 $L = W$, $R = \tipcn$.