chiark
/
gitweb
/
~ian
/
topbloke-formulae.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
traversal: wip prove Recreate Base Beginning OK, currently need to prove Tip Correct...
[topbloke-formulae.git]
/
trav-proofs.tex
diff --git
a/trav-proofs.tex
b/trav-proofs.tex
index a9ed5cd30a428f45ec78706534ce86b77ceeb425..3c2a1754cd8991bcc8cd1c4877812297cc9cdbd4 100644
(file)
--- 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
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
\subsection{Base Dependency Merge, Base Sibling Merge}
We do not prove that the preconditions are met. Instead, we check
@@
-17,7
+30,9
@@
WIP WHAT ABOUT PROVING ALL THE TRAVERSAL RESULTS
\subsection{Recreate Base Beginning}
\subsection{Recreate Base Beginning}
+\subsubsection{Create Acyclic}
+$L = \tipdy$ so
\subsection{Tip Base Merge}
\subsection{Tip Base Merge}