\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