\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)} % 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)} % Rules \def\rule#1#2{[\mbox{#1}_{\mbox{\footnotesize{#2}}}]} \def\rlambdans{\rule{$\lambda$}{ns}} \def\rheadns{\rule{head}{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}} % 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}}