use new extended Self Tip Inpatch

[topbloke-formulae.git] / article.tex

diff --git a/article.tex b/article.tex
index 714fbd167e00d67c850ccf69d0942e9a8b3b116a..d5e73b1a7e19da4ee9041dcb04a1bebcf5a7b4d4 100644 (file)
--- a/article.tex
+++ b/article.tex
@@ -1,21 +1,118 @@
-\documentclass[a4paper]{article}
-\usepackage{MnSymbol}
-\usepackage{stmaryrd}
-\usepackage{slashed}
+\documentclass[a4paper,leqno]{strayman}
+\errorcontextlines=50
+\let\numberwithin=\notdef
+\usepackage{amsmath}
+\usepackage{mathabx}
+\usepackage{txfonts}
+\usepackage{amsfonts}
+\usepackage{mdwlist}
+%\usepackage{accents}
+
+\usepackage{fancyhdr}
+\pagestyle{fancy}
+\lhead[\rightmark]{}
+
+\let\stdsection\section
+\renewcommand\section{\newpage\stdsection}
+
+\renewcommand{\ge}{\geqslant}
+\renewcommand{\le}{\leqslant}
+\newcommand{\nge}{\ngeqslant}
+\newcommand{\nle}{\nleqslant}
+
+\newcommand{\has}{\sqsupseteq}
+\newcommand{\isin}{\sqsubseteq}
+
+\newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}}
+\newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}}
+\newcommand{\haspatch}{\sqSupset}
+\newcommand{\patchisin}{\sqSubset}
+
+        \newif\ifhidehack\hidehackfalse
+        \DeclareRobustCommand\hidefromedef[2]{%
+          \hidehacktrue\ifhidehack#1\else#2\fi\hidehackfalse}
+        \newcommand{\pa}[1]{\hidefromedef{\varmathbb{#1}}{#1}}
+
+\newcommand{\set}[1]{\mathbb{#1}}
+\newcommand{\pay}[1]{\pa{#1}^+}
+\newcommand{\pan}[1]{\pa{#1}^-}
+
+\newcommand{\p}{\pa{P}}
+\newcommand{\py}{\pay{P}}
+\newcommand{\pn}{\pan{P}}
+
+\newcommand{\pq}{\pa{Q}}
+\newcommand{\pqy}{\pay{Q}}
+\newcommand{\pqn}{\pan{Q}}
+
+\newcommand{\pr}{\pa{R}}
+\newcommand{\pry}{\pay{R}}
+\newcommand{\prn}{\pan{R}}
+
+%\newcommand{\hasparents}{\underaccent{1}{>}}
+%\newcommand{\hasparents}{{%
+%  \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}}
+\newcommand{\hasparents}{>_{\mkern-7.0mu _1}}
+\newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}}
+
+\renewcommand{\implies}{\Rightarrow}
+\renewcommand{\equiv}{\Leftrightarrow}
+\renewcommand{\nequiv}{\nLeftrightarrow}
+\renewcommand{\land}{\wedge}
+\renewcommand{\lor}{\vee}
+
+\newcommand{\pancs}{{\mathcal A}}
+\newcommand{\pends}{{\mathcal E}}
+
+\newcommand{\pancsof}[2]{\pancs ( #1 , #2 ) }
+\newcommand{\pendsof}[2]{\pends ( #1 , #2 ) }
+
+\newcommand{\merge}{{\mathcal M}}
+\newcommand{\mergeof}[4]{\merge(#1,#2,#3,#4)}
+%\newcommand{\merge}[4]{{#2 {{\frac{ #1 }{ #3 } #4}}}}
+
+\newcommand{\patch}{{\mathcal P}}
+\newcommand{\base}{{\mathcal B}}
+
+\newcommand{\patchof}[1]{\patch ( #1 ) }
+\newcommand{\baseof}[1]{\base ( #1 ) }
+
+\newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} }
+\newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} }
+
+%\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}}
+\newcommand{\bigforall}{%
+  \mathop{\mathchoice%
+    {\hbox{\huge$\forall$}}%
+    {\hbox{\Large$\forall$}}%
+    {\hbox{\normalsize$\forall$}}%
+    {\hbox{\scriptsize$\forall$}}}%
+}
+
+\newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}}
+\newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}}
+
+\newcommand{\qed}{\square}
+\newcommand{\proofstarts}{{\it Proof:}}
+\newcommand{\proof}[1]{\proofstarts #1 $\qed$}
+
+\newcommand{\gathbegin}{\begin{gather} \tag*{}}
+\newcommand{\gathnext}{\\ \tag*{}}
+
+\newcommand{\true}{t}
+\newcommand{\false}{f}
+
 \begin{document}
-\def\iwjtest{{/\mkern-9mu\Sqsupset}}
-\newcommand{\iwjtestx}{\mathrel{\ooalign{$\Sqsubset$ $\sslash$}}}
-\newcommand{\iwjtesty}{{%
-  \declareslashed{}{\sslash}{-0.04}{0}{\Sqsubset}\slashed{\Sqsubset}}}
-sponge
-$ A \sqsubseteq B $
-$ A \not \sqsubseteq B $
-$ A \nsqsubseteq B $
-$ A \Sqsubset B $
-$ A \Sqsupset B $
-$ \sslash $
-$ \iwjtest $
-$ \iwjtestx $
-$ \iwjtesty $
-$ A \iwjtesty B $
+
+\input{notation.tex}
+\input{invariants.tex}
+\input{lemmas.tex}
+\input{annotations.tex}
+
+\input{simple.tex}
+\input{create-base.tex}
+\input{create-tip.tex}
+\input{anticommit.tex}
+\input{merge.tex}
+
 \end{document}