\RequirePackage{amssymb}

% General
\def\isdef{\stackrel{\text{def}}{=}}
\def\axjustifies{\thickness0em\justifies}

% Parsing
\def\parsepgmop{\mathit{Parse}}
\def\parsepgm#1{\parsepgmop\left(#1\right)}
\def\parsestrop{\mathit{ParseStr}}
\def\parsestr#1{\parsestrop\left(#1\right)}
\def\unescapeop{\mathit{unescape}}
\def\unescape#1{\unescapeop\left(#1\right)}
\def\escapeop{\mathit{escape}}
\def\escape#1{\escapeop\left(#1\right)}

% Types
\def\Pgm{\mathit{Pgm}}
\def\Stm{\mathit{Stm}}
\def\Input{\mathit{Input}}
\def\Output{\mathit{Output}}
\def\State{\mathit{State}}
\def\String{\mathit{String}}
\def\Char{\mathit{Char}}

% Stack
\def\Stack#1{\mathbf{Stack}\left[\mathit{#1}\right]}
\def\Nil{\texttt{Nil}}
\def\pushop{\mathit{push}}
\def\popop{\mathit{pop}}
\def\push#1#2{\pushop\left(#1, #2\right)}
\def\pop#1{\popop\left(#1\right)}

% Store
\def\putop{\mathit{put}}
\def\put#1#2#3{\putop\left(#1, #2, #3\right)}
\def\emptystore{\varnothing}

% Syntax
\def\SynPgm{\langle\Pgm\rangle}
\def\SynStm{\langle\Stm\rangle}
\def\SynString{\langle\String\rangle}
\def\SynChar{\langle\Char\rangle}

% Statements
\let\statement\texttt
\def\StmPush{\statement{Push}}
\def\StmCat{\statement{Cat}}
\def\StmHead{\statement{Head}}
\def\StmTail{\statement{Tail}}
\def\StmQuotify{\statement{Quotify}}
\def\StmPut{\statement{Put}}
\def\StmGet{\statement{Get}}
\def\StmInput{\statement{Input}}
\def\StmOutput{\statement{Output}}
\def\StmExec{\statement{Exec}}

% Transitions
\def\trans#1#2#3#4#5#6{\left\langle#1,#2,#3\right\rangle\to\left(#4,#5,#6\right)}

\def\sostrans#1#2#3#4#5#6#7#8{\left\langle#1,#2,#3,#4\right\rangle\Rightarrow\left(#5,#6,#7,#8\right)}
\def\sostranseind#1#2#3#4#5#6#7{\left\langle#1,#2,#3,#4\right\rangle\Rightarrow\left(#5,#6,#7\right)}
\def\sostransgamma#1#2#3#4#5{\left\langle#1,#2,#3,#4\right\rangle\Rightarrow#5}

% Rules
\def\rule#1#2{[\mbox{#1}_{\mbox{\footnotesize{#2}}}]}
\def\rlambdans{\rule{$\lambda$}{ns}}
\def\rpushns{\rule{push}{ns}}
\def\rheadns{\rule{head}{ns}}
\def\rtailns{\rule{tail}{ns}}
\def\rquotifyns{\rule{quotify}{ns}}
\def\rcatns{\rule{cat}{ns}}
\def\rgetns{\rule{get}{ns}}
\def\rputns{\rule{put}{ns}}
\def\rinputns{\rule{input}{ns}}
\def\routputns{\rule{output}{ns}}
\def\rexecns{\rule{exec}{ns}}

\def\rtailsos{\rule{tail}{sos}}
\def\rcompeensos{\rule{comp}{sos}}
\def\rexecsos{\rule{exec}{sos}}

% Common names
\def\stk{\mathit{stk}}
\def\str{\mathit{str}}
\def\ip{\mathit{i}}
\def\op{\mathit{o}}
\def\pgm{\mathit{pgm}}
\def\stm{\mathit{stm}}
\def\st{\mathit{st}}
\def\var{\mathit{var}}
\def\val{\mathit{val}}

% Programs
\newenvironment{smurf}{\tt\begin{center}}{\end{center}}
\let\smurfinline\texttt