latex_header.tex

\usepackage{comment} 

\usepackage{etoolbox} % fixes fatal error caused by combining bm, stackengine, hyperref (seriously?)
% http://tex.stackexchange.com/questions/22995/package-incompatibilites-etoolbox-hyperref-and-bm-standalone

\usepackage{etex} % else error on too many packages

% includes
\usepackage{algorithm}
%\usepackage{algorithmic} % conflicts with algpseudocode
\usepackage{algpseudocode}
%\newcommand*\Let[2]{\State #1 $\gets$ #2}
\algrenewcommand\alglinenumber[1]{
{\scriptsize #1}}
\algrenewcommand{\algorithmicrequire}{\textbf{Input:}}
\algrenewcommand{\algorithmicensure}{\textbf{Output:}}


%\usepackage[multiple]{footmisc} % footnotes at the same character separated by ','

\usepackage{multicol}

\usepackage{afterpage}

\usepackage{changepage} % for adjustwidth

\usepackage{tikz}
\usetikzlibrary{shapes,arrows,backgrounds,graphs,%
matrix,patterns,arrows,decorations.pathmorphing,decorations.pathreplacing,%
positioning,fit,calc,decorations.text,shadows,decorations.markings%
}

\usepackage{bussproofs}
\EnableBpAbbreviations


\usepackage{amsmath}
\usepackage{amsthm}
%\usepackage{amssymb} % the reals
\usepackage{mathtools} % smashoperator

\usepackage{thm-restate} % restatable env

% needs extra work and fails on some label here
%\usepackage{cleveref} % cref, apparently better than autoref of hyperref 

\usepackage{nicefrac} % nicefrac

\usepackage{mathrsfs} % mathscr

\usepackage{pst-node} % http://tex.stackexchange.com/questions/35717/how-to-draw-arrows-between-parts-of-an-equation-to-show-the-math-distributive-pr

\usepackage{stackengine}

\usepackage{thmtools} % advanced thm commands (declaretheorem)


\usepackage{nameref} % reference name of thm instead of counter

\usepackage{todonotes}

% conflict with beamer
%\usepackage{paralist} % compactenum

\usepackage{hyperref}
%\hypersetup{hidelinks}  % don't give options to usepackage, it doesn't work with beamer
%\hypersetup{colorlinks=false}  % don't give options to usepackage, it doesn't work with beamer


% \usepackage{enumitem} % labels for enumerate % breaks beamer and memoir itemize


\usepackage{url} 

%\usepackage[format=hang,justification=raggedright]{caption}% or e.g. [format=hang]
% for \ContinuedFloat % this can cause problems with memoir

\usepackage{cancel} % \cancel

\usepackage{lineno}


% commands

% logic etcs
%\newcommand{\ex}[2]{\bigskip\section*{Exercise #1: \begin{minipage}[t]{.80\linewidth} \small \textnormal{\it #2} \end{minipage} } }

\newcommand{\ex}[2]{\bigskip \noindent\textbf{Exercise #1.} \textit{#2} \smallskip}

\newcommand{\comm}[1]{{\color{gray} // #1 }}


\newcommand{\true}[0]{\textbf{1}}
\newcommand{\false}[0]{\textbf{0}}
\newcommand{\tr}{\true}
\newcommand{\fa}{\false}

\newcommand{\ra}{\rightarrow}
\newcommand{\Ra}{\Rightarrow}
\newcommand{\la}{\leftarrow}
\newcommand{\La}{\Leftarrow}

\newcommand{\lra}{\leftrightarrow}
\newcommand{\Lra}{\Leftrightarrow}

\newcommand{\NKZ}{\textbf{NK2}}

%\DeclareMathOperator{\syneq}{\equiv} %spacing seems wrong, therefore defined as newcommand below
\DeclareMathOperator{\limpl}{\supset}
\DeclareMathOperator{\liff}{\lra}
\DeclareMathOperator{\semiff}{\Lra}
\newcommand{\syneq}{\equiv}
\newcommand{\union}{\cup}
\newcommand{\bigunion}{\bigcup}
\newcommand{\intersection}{\cap}
\newcommand{\bigintersection}{\bigcap}
\newcommand{\intersect}{\intersection}
\newcommand{\bigintersect}{\bigintersection}

\newcommand{\powerset}{\mathcal{P}}

\newcommand{\entails}{\vDash}
\newcommand{\notentails}{\nvDash}
\newcommand{\proves}{\vdash}

\newcommand{\vm}{\ensuremath{\vv_\mathcal{M}}}
\newcommand{\Dia}{\ensuremath{\lozenge}}

\newcommand{\spaced}[1]{\ \ #1 \ \ }
\newcommand{\spa}[1]{\spaced{#1}}
\newcommand{\spas}[1]{\;{#1}\;}
\newcommand{\spam}[1]{\;\,{#1}\;\,}
\newcommand{\spal}[1]{\spa{#1}}

% functions
\DeclareMathOperator{\sk}{sk}
\DeclareMathOperator{\mgu}{mgu}
\DeclareMathOperator{\dom}{dom}
\DeclareMathOperator{\ran}{ran}

\DeclareMathOperator{\id}{id}
\DeclareMathOperator{\Fun}{FS}
\DeclareMathOperator{\Pred}{PS}
\DeclareMathOperator{\LV}{LV}
\newcommand{\LiftingVars}{\LV}
\DeclareMathOperator{\FV}{FV}
\newcommand{\Vars}{\FV}
\DeclareMathOperator{\Lang}{L}
\DeclareMathOperator{\ar}{ar}
\DeclareMathOperator{\PI}{PI}
\DeclareMathOperator{\LI}{LI}
\DeclareMathOperator{\Congr}{Congr}
\DeclareMathOperator{\Refl}{Refl}
\DeclareMathOperator{\aiu}{au}
\DeclareMathOperator{\expa}{unfold-lift}

\newcommand{\PIinc}{\LI}
\newcommand{\PIincde}{\LIde}

\newcommand{\LIde}{\ensuremath{\LI^\Delta}}

\newcommand{\LIcl}{\ensuremath{\LI_{\operatorname{cl}}}}
\newcommand{\LIclde}{\ensuremath{\LI_{\operatorname{cl}}^\Delta}}

\newcommand{\LIpre}{\LI^\bullet}

\newcommand{\PIstep}{\PI_{\mathrm{step}}}
\newcommand{\PIinit}{\PI_{\mathrm{init}}}

%\newcommand{\nosigmasym}{\circ}
%\newcommand{\nosigma}{^\nosigmasym}

%$\newcommand{\Wtilde}[1]{\stackrel{\sim}{\smash{#1}\rule{0pt}{1.1ex}}}
%\newcommand{\Wtilde}[1]{\stackrel{\sim}{#1}}
\newcommand{\Wtilde}[1]{\bm\tilde{#1}}


\newcommand{\nosigma}[1]{\Wtilde{#1}}
\newcommand{\PInosigma}{\Wtilde{\PI}}

%\newcommand{\PIstepnosigma}{\PInosigma_{\mathrm{step}}}
\newcommand{\PIstepstarnosigma}{\PInosigma^{*}_{\mathrm{step}}}

%\newcommand{\PIstarnosigma}{\bm\tilde\PI^{*\nosigmasym}}
\newcommand{\PIstarnosigma}{\PInosigma^{*}}

%\newcommand{\star}{^*}

\newcommand{\cll}{\ensuremath{_{\operatorname{LIcl}}}}
\newcommand{\cllde}{\ensuremath{_{\operatorname{LIcl}^\Delta}}}

%\newcommand{\lifi}{\mathop{\ell\text{}i}}
\newcommand{\lifiboth}[1]{\ensuremath{\LIcl(#1)}}
\newcommand{\lifidelta}[1]{\ensuremath{\LIclde(#1)}}

\newcommand{\domainofmodel}[1]{\ensuremath{D_{#1}}}
\newcommand{\interpretation}[1]{\ensuremath{\calI_{#1}}}


%\DeclareMathOperator{\abstraction}{abstraction}

%\newcommand{\sk}{\ensuremath{\mathrm{sk}}}
%\newcommand{\mgu}{\ensuremath{\mathrm{mgu}}}
%\newcommand{\Fun}{\ensuremath{\mathrm{FS}}}
%\newcommand{\Pred}{\ensuremath{\mathrm{PS}}}
%\newcommand{\PI}{\ensuremath{\mathrm{PI}}}
%\newcommand{\Lang}{\ensuremath{\mathrm{L}}}
%\newcommand{\ar}{\ensuremath{\mathrm{ar}}}

\DeclareMathOperator{\AI}{AI}
\newcommand{\AIde}{\ensuremath{\AI^\Delta}}
\newcommand{\AImatrix}{\ensuremath{\AI_\mathrm{mat}}}
\newcommand{\AImatrixde}{\ensuremath{\AI_\mathrm{mat}^\Delta}}
\newcommand{\AImat}{\AImatrix}
\newcommand{\AImatde}{\AImatrixde}
\newcommand{\AIclause}{\ensuremath{\AI_\mathrm{cl}}}
\newcommand{\AIcl}{\AIclause}
\newcommand{\AIclde}{\AIclausede}
\newcommand{\AIclausede}{\ensuremath{\AIclause^\Delta}}
\newcommand{\fromclause}{\ensuremath{_{\operatorname{AIcl}}}}
\newcommand{\fromclausede}{\ensuremath{_{\operatorname{AIcl}^\Delta}}}
\newcommand{\cl}{\fromclause}
\newcommand{\clde}{\fromclausede}

\newcommand{\Q}{\ensuremath{Q}}

\newcommand{\AIcol}{\ensuremath{\AI_\mathrm{col}}}
\newcommand{\AIcolde}{\AIcol^\Delta}

\newcommand{\AIany}{\ensuremath{\AI_\mathrm{*}}}
\newcommand{\AIanyde}{\AIany^\Delta}

\newcommand{\AIclpre}{\AIclause^\bullet}
\newcommand{\AImatpre}{\AImatrix^\bullet}

\newcommand{\PS}{\Pred}
\newcommand{\FS}{\Fun}

\DeclareMathOperator{\LangSym}{\mathcal{L}}

%\newcommand{\mguarr}{\sim_\ra}
\newcommand{\mguarr}{\mapsto_{\mgu}}


%\newcommand{\Trans}{\ensuremath{\mathrm{T}}}
%\newcommand{\Trans}{\ensuremath{\mathrm{T}}}
\DeclareMathOperator{\Trans}{T}
\DeclareMathOperator{\TransInv}{T^{-1}}

\DeclareMathOperator{\FAX}{F_{Ax}}
\DeclareMathOperator{\EAX}{E_{Ax}}
%\newcommand{\FAX}{\ensuremath{\mathrm{F_{Ax}}}}
%\newcommand{\EAX}{\ensuremath{\mathrm{E_{Ax}}}}

%\newcommand{\TransAll}{\ensuremath{\Trans_{\mathrm{Ax}}}}
\DeclareMathOperator{\TransAll}{\Trans_{Ax}}
%\newcommand{\FAX}{\ensuremath{\mathrm{F_{Ax}}}}

\DeclareMathOperator{\defeq}{\,\stackrel{\mathclap{\mathrm{def}}}{=}\,}
\DeclareMathOperator{\defeqBeamer}{\,\stackrel{\mathclap{\mathsf{def}}}{=}\,}

\newcommand{\subst}[1]{[#1]}
%\newcommand{\abstractionOp}[1]{\{#1\}}

\newcommand{\subformdefinitional}[1]{\ensuremath{D_{\Sigma(#1)}}}

\newcommand{\lits}{\Lambda}


%\newcommand{\lift}[3]{\operatorname{Lift}_{#1}(#2; #3)}
%\newcommand{\lift}[3]{\operatorname{Lift}_{#1,#3}(#2)}
%\newcommand{\lift}[3]{\operatorname{Lift}_{#1,#3}[#2]}
%\newcommand{\lift}[3]{\overline{#2}_{#1,#3}}
\newcommand{\lifsym}{\ell}
%\newcommand{\lift}[3]{\lifsym_{#1,#3}[#2]}
\newcommand{\lift}[3]{\lifsym_{#1}^{#3}[#2]}
\newcommand{\liftnovar}[2]{\lifsym_{#1}[#2]}

\newcommand{\lifpart}{\lifsym_\mathrm{part}}

%\newcommand{\lft}[3]{\lifsym_{#1,#2}[#3]}
\newcommand{\lft}[3]{\lift{#1}{#3}{#2}}
\newcommand{\lifboth}[1]{\lifsym[#1]}

%\newcommand{\lifi}{\mathop{\ell\text{}i}}
%\newcommand{\lifiboth}[1]{\lifi[#1]}
%\newcommand{\lifidelta}[1]{\lifi_\Delta^x[#1]}
%\newcommand{\lifideltanovar}[1]{\lifi_\Delta[#1]}

\newcommand{\lifdelta}[1]{\lift{\Delta}{#1}{x}}
\newcommand{\lifdeltanovar}[1]{\liftnovar{\Delta}{#1}}
\newcommand{\lifgamma}[1]{\lift{\Gamma}{#1}{y}}
\newcommand{\lifgammanovar}[1]{\liftnovar{\Gamma}{#1}}
\newcommand{\lifphinovar}[1]{\liftnovar{\Phi}{#1}}
\newcommand{\lifphi}[1]{\lift{\Phi}{#1}{z}}

\newcommand{\lifgammadelta}[1]{\lift{\Gamma\cup\Delta}{#1}{z}}

\newcommand{\tauell}{\tau^\lifsym}
\newcommand{\tauellphi}{\tau^{\lifsym_\Phi}}
\newcommand{\tauelldelta}{\tau^{\lifsym_\Delta}}

\DeclareMathOperator{\arr}{\mathcal{A}}
%\DeclareMathOperator{\arrFinal}{{\mathcal{A}^{\bm*}}}
\DeclareMathOperator{\arrFinal}{{\mathcal{\bm{\hat}A}}}
\DeclareMathOperator{\warr}{\marr}
\DeclareMathOperator{\marr}{\mathcal{M}}

\DeclareMathOperator{\apath}{\leadsto}
\DeclareMathOperator{\mpath}{\leadsto_=}
\DeclareMathOperator{\notapath}{\not\leadsto}
\DeclareMathOperator{\notmpath}{\not\leadsto_=}

\newcommand{\ltArrC}{<_{\arrFinal(C)}}
\newcommand{\ltAC}{<_{\arr(C)}}
\newcommand{\ltArrCOne}{<_{\arrFinal(C_1)}}
\newcommand{\ltArrCTwo}{<_{\arrFinal(C_2)}}
%\newcommand{\ltArrC}{<_{\scalebox{0.6}{$\arrFinal(C)$}}}
\newcommand{\ltArr}{<_{\scalebox{0.6}{$\arrFinal$}}}

\newcommand{\bhat}{\bm\hat}
\newcommand{\bbar}{\bm\bar}
\newcommand{\bdot}{\bm\dot}

%\usepackage{yfonts}
\usepackage{upgreek}
\DeclareMathAlphabet{\mathpzc}{OT1}{pzc}{m}{it}
%\DeclareMathOperator{\pos}{\mathscr{P}}
%\DeclareMathOperator{\pos}{\mathpzc{p}}
%\DeclareMathOperator{\pos}{{\rho}}
\DeclareMathOperator{\pos}{{\operatorname P}}
%\DeclareMathOperator{\pos}{P}
\DeclareMathOperator{\poslit}{\pos_\mathrm{lit}}
\DeclareMathOperator{\posterm}{\pos_\mathrm{term}}
%\newcommand{\poslit}[1]{\ensuremath{p_\text{lit}(#1)}}
%\newcommand{\posterm}[1]{\ensuremath{p_\text{term}(#1)}}
\newcommand{\at}[1]{|_{#1}}
\newcommand{\atp}{\at{p}}
\newcommand{\atq}{\at{q}}

\newcommand{\UICm}[1]{\UnaryInfCm{#1}}
\newcommand{\UnaryInfCm}[1]{\UnaryInfC{$#1$}}
\newcommand{\BICm}[1]{\BinaryInfCm{#1}}
\newcommand{\BinaryInfCm}[1]{\BinaryInfC{$#1$}}
\newcommand{\RightLabelm}[1]{\RightLabel{$#1$}}
\newcommand{\LeftLabelm}[1]{\LeftLabel{$#1$}}
\newcommand{\AXCm}[1]{\AxiomCm{#1}}
\newcommand{\AxiomCm}[1]{\AxiomC{$#1$}}
\newcommand{\mt}[1]{\textnormal{#1}}

\newcommand{\UnaryInfm}[1]{\UnaryInf$#1$}
\newcommand{\BinaryInfm}[1]{\BinaryInf$#1$}
\newcommand{\Axiomm}[1]{\Axiom$#1$}

\newcommand{\quantifierdots}{\dots} % dots for $\forall x_1 \quantifierdots \forall x_n$
% cdots are somewhat nicer, but look inconsistent with other dots at the bottom of the line 
%\newcommand{\quantifierdots}{\cdots} % dots for $\forall x_1 \quantifierdots \forall x_n$



% math
\newcommand{\calI}{\ensuremath{\mathcal{I}}}

\newcommand{\tupleShort}[2]{\ensuremath{(#1_1,\dotsc,#1_{#2})}}
\newcommand{\tuple}[2]{\ensuremath{(#1_1,\:#1_2\:,\dotsc,\:#1_{#2})}}
\newcommand{\setelements}[2]{\ensuremath{\{#1_1,\:#1_2\:,\dotsc,\:#1_{#2}\}}}
\newcommand{\pathelements}[2]{\ensuremath{ (#1_1,\:#1_2\:,\dotsc,\:#1_{#2}) }}

\newcommand{\elems}[1]{\ensuremath{#1_1,\dotsc, #1_{n}) }}

\newcommand{\defiemph}[1]{\emph{#1}}

\newcommand{\setofbases}{\ensuremath{\mathcal{B}}}
\newcommand{\setofcircuits}{\ensuremath{\mathcal{C}}}

\newcommand{\reals}{\ensuremath{\mathbb{R}}}
\newcommand{\integers}{\ensuremath{\mathbb{Z}}} 
\newcommand{\naturalnumbers}{\ensuremath{\mathbb{N}}}

% general
\newcommand{\zit}[3]{#1\ \cite{#2}, #3}
\newcommand{\zitx}[2]{#1\ \cite{#2}}
\newcommand{\footzit}[3]{\footnote{\zit{#1}{#2}{#3}}}
\newcommand{\footzitx}[2]{\footnote{\zitx{#1}{#2}}}

\newcommand{\ite}{\begin{itemize}}
\newcommand{\ete}{\end{itemize}}

\newcommand{\bfr}{\begin{frame}}
\newcommand{\efr}{\end{frame}}

\newcommand{\ilc}[1]{\texttt{#1}}


% misc

% multiframe
\usepackage{xifthen}% provides \isempty test
% new counter to now which frame it is within the sequence
\newcounter{multiframecounter}
% initialize buffer for previously used frame title
\gdef\lastframetitle{\textit{undefined}}
% new environment for a multi-frame
\newenvironment{multiframe}[1][]{%
\ifthenelse{\isempty{#1}}{%
% if no frame title was set via optional parameter,
% only increase sequence counter by 1
\addtocounter{multiframecounter}{1}%
}{%
% new frame title has been provided, thus
% reset sequence counter to 1 and buffer frame title for later use
\setcounter{multiframecounter}{1}%
\gdef\lastframetitle{#1}%
}%
% start conventional frame environment and
% automatically set frame title followed by sequence counter
\begin{frame}%
\frametitle{\lastframetitle~{\normalfont \Roman{multiframecounter}}}%
}{%
\end{frame}%
}




% http://texfragen.de/hurenkinder_und_schusterjungen
\usepackage[all]{nowidow}



% force no overlong lines:
%\tolerance=1 % tolerance for how badly spaced lines are allowed, less means "better" lines
\tolerance=500 %  need more tolerance for equations
%\tolerance=9999 %  really much tolerance, 10k is max
%\emergencystretch=\maxdimen % this creates really ugly lines
%\emergencystretch=200pt
%\setlength{\emergencystretch}{3em}
%\hyphenpenalty=10000 % forces no hyphenation
%\hbadness=10000


% http://tex.stackexchange.com/questions/35717/how-to-draw-arrows-between-parts-of-an-equation-to-show-the-math-distributive-pr
\tikzset{square arrow/.style={to path={ -- ++(.0,-.15)  -| (\tikztotarget)}}}
\tikzset{square arrow2/.style={to path={ -- ++(.0,-.25)  -| (\tikztotarget)}}}
%\tikzset{square arrow/.style={to path={ -- ++(00,-.01) -- ++(0.5,-0.1) -- ++(0.5,-0.1) -| (\tikztotarget)},color=red}}


% have arrows from a to b and from c to d here
% just use: texttext\arrowA texttest \arrowB texttext
\newcommand{\arrowA}{\tikz[overlay,remember picture] \node (a) {};}
\newcommand{\arrowB}{\tikz[overlay,remember picture] \node (b) {};}
\newcommand{\drawAB}{
	\tikz[overlay,remember picture]
	{\draw[->,bend left=5,color=red] (a.south) to (b.south);}
	%{\draw[->,square arrow,color=red] (a.south) to (b.south);}
}
\newcommand{\arrowAP}{\tikz[overlay,remember picture] \node (ap) {};}
\newcommand{\arrowBP}{\tikz[overlay,remember picture] \node (bp) {};}
\newcommand{\drawABP}{
	\tikz[overlay,remember picture]
	{\draw[->,bend right=5,color=red] (ap.south) to (bp.south);}
	%{\draw[->,square arrow,color=red] (a.south) to (b.south);}
}

\newcommand{\arrowAB}{\tikz[overlay,remember picture] \node (ab) {};}
\newcommand{\arrowBA}{\tikz[overlay,remember picture] \node (ba) {};}
\newcommand{\drawAABB}{
	\tikz[overlay,remember picture]
	%{\draw[->,bend left=80] (a.north) to (b.north);}
	{\draw[->,square arrow,color=brown] (ab.south) to (ba.south);
	\draw[->,square arrow,color=brown] (ba.south) to (ab.south);}
}


\newcommand{\arrowCD}{\tikz[overlay,remember picture] \node (cd) {};}
\newcommand{\arrowDC}{\tikz[overlay,remember picture] \node (dc) {};}
\newcommand{\drawCCDD}{
	\tikz[overlay,remember picture]
	%{\draw[->,bend left=80] (a.north) to (b.north);}
	{\draw[<->,dashed,square arrow,color=green] (cd.south) to (dc.south); }
}



\newcommand{\arrowC}{\tikz[overlay,remember picture] \node (c) {};}
\newcommand{\arrowD}{\tikz[overlay,remember picture] \node (d) {};}
\newcommand{\drawCD}{
	\tikz[overlay,remember picture]
	{\draw[->,square arrow,color=blue] (c.south) to (d.south);}
}

\newcommand{\arrowE}{\tikz[overlay,remember picture] \node (e) {};}
\newcommand{\arrowF}{\tikz[overlay,remember picture] \node (f) {};}
\newcommand{\drawEF}{
	\tikz[overlay,remember picture]
	{\draw[->,square arrow2,color=orange] (e.south) to (f.south);}
}


\newcommand{\arrAP}{\arrowAP}
\newcommand{\arrBP}{\arrowBP}
\newcommand{\arrA}{\arrowA}
\newcommand{\arrB}{\arrowB}
\newcommand{\arrC}{\arrowC}
\newcommand{\arrD}{\arrowD}
\newcommand{\arrE}{\arrowE}
\newcommand{\arrF}{\arrowF}


\DeclareMathOperator{\simgeq}{\scalebox{0.92}{$\gtrsim$}}

\newcommand{\refsub}[2]{\hyperref[#2]{\ref*{#1}.\ref*{#2}}}

%\newcommand{\sigmarange}[2]{\sigma_{#1}^{#2} }
\newcommand{\sigmarange}[2]{\sigma_{(#1,\,#2)} }
\newcommand{\sigmaz}[1]{\sigmarange{0}{#1} }
\newcommand{\sigmazi}[0]{\sigmaz{i} }
\newcommand{\sigmazmi}[0]{\sigmaz{i-1} }

\DeclareMathOperator{\lit}{lit}

%\def\fCenter{\ \proves\ }
\def\fCenter{\proves}

\newcommand{\prflbl}[2]{\RightLabel{\footnotesize $#1, #2$} }
%\newcommand{\prflblid}[1]{\RightLabel{$#1, \id$} }
\newcommand{\prflblid}[1]{\RightLabel{\footnotesize $#1$} }

\DeclareMathOperator{\resruleres}{res}
\DeclareMathOperator{\resrulefac}{fac}
\DeclareMathOperator{\resrulepar}{par}
\newcommand{\lkrule}[2]{\ensuremath{\operatorname{#1}:#2}} % operatorname fixes spacing issues for =
\newcommand{\resrule}[2]{\ensuremath{\underset{#2}{{#1}}}} 
\newcommand{\resruleremark}[3]{\ensuremath{\underset{#2}{{#1}} #3}}
%\newcommand{\lkrule}[2]{\ensuremath{\stackrel{\operatorname{#1}}{#2}}} % operatorname fixes spacing issues for =

\newcommand{\parti}[4]{\ensuremath{ \langle (#1; #2),\allowbreak (#3; #4)\rangle  }}

\newcommand{\partisym}{\ensuremath{\chi}}

\newcommand{\occur}[1]{\ensuremath{[#1]}}
\newcommand{\occ}[1]{\occur{#1}}

\newcommand{\occurat}[2]{\ensuremath{{\occur{#1}_{#2}}}}
\newcommand{\occuratp}[1]{\occurat{#1}{p}}
\newcommand{\occat}[2]{\occurat{#1}{#2}}
\newcommand{\occatp}[1]{\occurat{#1}{p}}
\newcommand{\occatq}[1]{\occurat{#1}{q}}




% fix restateable spacing 
%http://tex.stackexchange.com/questions/111639/extra-spacing-around-restatable-theorems

\makeatletter

\def\thmt@rst@storecounters#1{%
%THIS IS THE LINE I ADDED:
\vspace{-1.9ex}%
  \bgroup
        % ugly hack: save chapter,..subsection numbers
        % for equation numbers.
  %\refstepcounter{thmt@dummyctr}% why is this here?
  %% temporarily disabled, broke autorefname.
  \def\@currentlabel{}%
  \@for\thmt@ctr:=\thmt@innercounters\do{%
    \thmt@sanitizethe{\thmt@ctr}%
    \protected@edef\@currentlabel{%
      \@currentlabel
      \protect\def\@xa\protect\csname the\thmt@ctr\endcsname{%
        \csname the\thmt@ctr\endcsname}%
      \ifcsname theH\thmt@ctr\endcsname
        \protect\def\@xa\protect\csname theH\thmt@ctr\endcsname{%
          (restate \protect\theHthmt@dummyctr)\csname theH\thmt@ctr\endcsname}%
      \fi
      \protect\setcounter{\thmt@ctr}{\number\csname c@\thmt@ctr\endcsname}%
    }%
  }%
  \label{thmt@@#1@data}%
  \egroup
}%

\makeatother




\newcommand{\mymark}[1]{\ensuremath{(#1)}}
\newcommand{\markA}{\mymark \circ}
\newcommand{\markB}{\mymark *}
\newcommand{\markC}{\mymark \divideontimes}

\newcommand{\wrong}[1]{{\LARGE \color{red}WRONG: #1\par}}
\newcommand{\NB}[1]{{\color{blue}NB: #1}}
\newcommand{\hl}[1]{{\color{orange} #1}}
\newcommand{\mytodo}[1]{{\color{red}TODO: #1}}
\newcommand{\largered}[1]{{

		\LARGE\bfseries\boldmath{\color{red}
		#1

}}}
\newcommand{\largeblue}[1]{{

	  \large\bfseries\color{blue}
		#1

}}




\usepackage{ulem} %  \dotuline{dotty} \dashuline{dashing} \sout{strikethrough}
\normalem

\usepackage{tabu} % tabular also in math mode (and much more)

\usepackage[color]{changebar} %  \cbstart, \cbend
\cbcolor{red}



% http://tex.stackexchange.com/questions/7032/good-way-to-make-textcircled-numbers
\newcommand*\circled[1]{\tikz[baseline=(char.base)]{
\node[shape=circle,draw,inner sep=2pt] (char) {#1};}}



% http://tex.stackexchange.com/questions/43346/how-do-i-get-sub-numbering-for-theorems-theorem-1-a-theorem-1-b-theorem-2

\makeatletter
\newenvironment{subtheorem}[1]{%
  \def\subtheoremcounter{#1}%
  \refstepcounter{#1}%
  \protected@edef\theparentnumber{\csname the#1\endcsname}%
  \setcounter{parentnumber}{\value{#1}}%
  \setcounter{#1}{0}%
  \expandafter\def\csname the#1\endcsname{\theparentnumber.\Alph{#1}}%
  \ignorespaces
}{%
  \setcounter{\subtheoremcounter}{\value{parentnumber}}%
  \ignorespacesafterend
}
\makeatother
\newcounter{parentnumber}


\usepackage{tabularx}% http://ctan.org/pkg/tabularx
\newcolumntype{Y}{>{\centering\arraybackslash}X}

\newcommand{\mycols}[2][3]{
	\noindent\begin{tabularx}{\textwidth}{*{#1}{Y}}
		#2
	\end{tabularx}%
}


\newcommand{\definethms}{

	%\declaretheorem[title=Theorem,qed=$\triangle$,parent=chapter]{thm}
	\newcommand{\thmqed}{$\square$} % for thms without proof
	\newcommand{\propqed}{$\square$} % for props without proof
	\newcommand{\lemmaqed}{$\blacksquare$} % for lemmas without proof
	\declaretheorem[title=Theorem]{thm}
	\declaretheorem[title=Proposition,sibling=thm]{prop}
	\declaretheorem[title=Conjectured Proposition,sibling=thm]{cprop}

	%\declaretheorem[title=Lemma,parent=chapter]{lemma}
	\declaretheorem[sibling=thm]{lemma}
	\declaretheorem[sibling=thm,title=Conjectured Lemma]{clemma}
	\declaretheorem[sibling=thm,title=Refutated Lemma {\color{red} {(this is wrong)}}]{rlemma}
	\declaretheorem[title=Corollary,sibling=thm]{corr}
	\declaretheorem[sibling=thm,title=Definition,style=definition,qed=$\triangle$]{defi}
	%\declaretheorem[title=Definition,qed=$\triangle$,parent=chapter]{defi}
	\declaretheorem[title=Example,style=definition,qed=$\triangle$,sibling=thm]{exa}

	\declaretheorem[sibling=thm,title=Conjecture]{conj}

	\declaretheorem[title=Remark,style=remark,numbered=no,qed=$\triangle$]{remark}


}

\usepackage[matha]{mathabx} % the locial operators here have more space around them and [ and ] are thicker, also langle and rangle are a bit nicer; subseteq looks a bit weird

%\usepackage{MnSymbol} % again other symbols


\newcommand{\inference}{\ensuremath{\iota}}
\DeclareMathOperator{\ca}{col-alt}
\DeclareMathOperator{\qa}{quant-alt}

\usepackage{cases} % numcases


% this should be loaded last: http://tex.stackexchange.com/questions/86343/no-room-for-a-new-mathgroup
\usepackage{bm} % bm, bold math symbols


\newcommand{\allbold}[1]{\textbf{\boldmath{#1}}}

\usepackage{pdflscape} % like lscape but rotates pdf-page automatically

\newenvironment{indproof}{ \begin{itemize} }{ \end{itemize} } \newcommand{\indproofitem}[1]{\item[#1.]}
%\newenvironment{indproof}{ \begin{description} }{ \end{description} } \newcommand{\indproofitem}[1]{\item{}#1.}

\usepackage{microtype}