strategy: move traversal proofs inline

[topbloke-formulae.git] / article.tex

diff --git a/article.tex b/article.tex
index 7bff6920bd91db6129b61de48da10bb779183756..6bbe082c65b2a73eb682c81ce1e2296535501fb4 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -84,15 +84,18 @@
 \newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
 \newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
 
-\newcommand{\commitmerge}{{\mathcal M}}
-\newcommand{\commitmergeof}[4]{\commitmerge(#1,#2,#3,#4)}
+%\newcommand{\commitmerge}{\text{\commitmergename}}
+\newcommand{\commitmergeof}[4]{#1 \approx \stmtmergeof{#2}{#3}{#4}}
 %\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
+\newcommand{\commitmergename}{Git Merge}
 
 \newcommand{\patch}{{\mathcal P}}
 \newcommand{\base}{{\mathcal B}}
 \newcommand{\depsreq}{{\mathcal G}}
 
 \newcommand{\allsrcs}{\set U}
+\newcommand{\allreach}{\set O}
+\newcommand{\allreachof}[1]{\set O^{#1}}
 
 \newcommand{\patchof}[1]{\patch ( #1 ) }
 \newcommand{\baseof}[1]{\base ( #1 ) }
@@ -109,9 +112,9 @@
 \newcommand{\mergeof}[3]{\left\langle #1 \;\middle\langle #2 \middle\rangle\; #3 \right\rangle}
 
 \newcommand{\alg}[1]{\text{\bf #1}}
-\newcommand{\setmerge}{\alg{merge}}
-\newcommand{\setmergeof}[3]{\setmerge\mergeof{#1}{#2}{#3}}
-\newcommand{\stmtmergeof}[3]{\setmerge\mergeof{#1}{#2}{#3}}
+\newcommand{\setmerge}{\mergeof{}{}{}}
+\newcommand{\setmergeof}[3]{\mergeof{#1}{#2}{#3}}
+\newcommand{\stmtmergeof}[3]{\mergeof{#1}{#2}{#3}}
 
 %\newcommand{\setmergeof}[3]{\setmerge\left\lgroup #1 \;\middle\lmoustache\; #2 \;\middle\rmoustache\; #3 \right\rgroup}
 %\newcommand{\setmergeof}[3]{\setmerge\left\rmoustache #1 \middle\rmoustache #2 \middle\lmoustache #3 \right\lmoustache}
@@ -132,6 +135,8 @@
 \newcommand{\tipdn}{ \tipa \pdn }
 \newcommand{\tipdy}{ \tipa \pdy }
 
+\newcommand{\tippy}{ \tipa \py }
+
 %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
 \newcommand{\bigforall}{%
   \mathop{\mathchoice%
@@ -154,6 +159,8 @@
 \newcommand{\qed}{\square}
 \newcommand{\proofstarts}{{\it Proof:}}
 \newcommand{\proof}[1]{\proofstarts #1 $\qed$}
+\newcommand{\commitproof}[1]{{\it Proof of commit generation conditions:}
+ #1 $\qed$}
 
 \newcommand{\statement}[2]{\[\eqn{ #1 }{ #2 }\]}