%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% WARNING: I changed these commands
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\renewcommand{\u}{\underline}
\renewcommand{\sup}[2]{\srho{\upcast{#1}{#2}}}

%% This is a proof that only appears in the long version, and is
%% otherwise completely omitted
\NewEnviron{longproof}{%
  \iflong\begin{proof}\BODY \end{proof}\fi%
}
\NewEnviron{shortproof}{%
  \ifshort\begin{proof}\BODY \end{proof}\fi%
}
\NewEnviron{longfigure}{%
  \iflong\begin{figure}\BODY \end{figure}\fi%
}
\NewEnviron{longonly}{%
  \iflong\BODY \fi%
}
\NewEnviron{shortonly}{%
  \ifshort\BODY \fi%
}

%% \newtheorem*{nonnum-theorem}{Theorem}

\newcommand{\num}{\texttt{Num}}
\newcommand{\String}{\texttt{String}}

\newcommand{\cbpv}{CBPV}
\newcommand{\cbpvstar}{CBPV*}
\newcommand{\cbpvtxt}{\cbpv}
\newcommand{\sem}[1]{\llbracket{#1}\rrbracket}
\newcommand{\sdncast}[2]{\sem{\dncast{#1}{#2}}}
\newcommand{\supcast}[2]{\sem{\upcast{#1}{#2}}}
\newcommand{\srho}[1]{\sem{#1}_\rho}
\newcommand{\sdn}[2]{\srho{\dncast{#1}{#2}}}
\newcommand{\hetplug}[1]{\langle#1\rangle}
\newcommand{\nats}{\mathbb{N}}
\newtheorem{principle}{Principle}
\newcommand{\vtype}{\,\,\text{val type}}
\newcommand{\ctype}{\,\,\text{comp type}}
\newcommand{\ctx}{\,\,\text{ctx}}
\newcommand{\stoup}{\,\,\text{stoup}}
\newcommand{\pipe}{\,\,|\,\,}
\newcommand{\hole}{\bullet}
\newcommand{\floor}[1]{\lfloor#1\rfloor}
\newcommand{\ltdyn}{\sqsubseteq}
\newcommand{\gtdyn}{\sqsupseteq}

\newcommand{\precltdyn}{\mathrel{\preceq\ltdyn}}
\newcommand{\precgtdyn}{\mathrel{\preceq\gtdyn}}
\newcommand{\ltdynsucc}{\mathrel{\ltdyn\succeq}}
\newcommand{\equidyn}{\mathrel{\gtdyn\ltdyn}}
\newcommand{\ltdynv}{\mathrel{\sqsubseteq_V}}
\newcommand{\ltdynt}{\mathrel{\sqsubseteq_T}}
\newcommand{\ltlogty}[2]{\mathrel{\ltdyn^{#1}_{#2}}}
\newcommand{\ltlogc}[1]{\mathrel{\ltdyn^{#1}_{\vdash}}}
\newcommand{\ltctx}{\mathrel{\ltdyn^{ctx}}}
\newcommand{\ltciu}{\mathrel{\ltdyn^{ciu}}}
\newcommand{\ltlog}{\mathrel{\ltdyn^{log}}}

\newcommand{\apreorder}{\trianglelefteq}
\newcommand{\ctxpreorder}{\mathrel{\apreorder^{\text{ctx}}}}
\newcommand{\ctxize}[1]{\mathrel{{#1}^{\text{ctx}}}}
\newcommand{\ix}[2]{\mathrel{#1^{#2}}}
\newcommand{\simsub}[1]{\mathrel{\sim_{#1}}}

\newcommand{\itylrof}[3]{\ilrof{#1}{#3,#2}}
\newcommand{\ilrof}[2]{\mathrel{{#1}^{\text{log}}_{#2}}}
\newcommand{\itylr}[2]{\itylrof{\apreorder}{#1}{#2}}
\newcommand{\ilr}[1]{\ilrof{\apreorder}{#1}}

\newcommand{\simp}[1]{{#1}^{\dag}}
\newcommand{\simpp}[1]{\simp{({#1})}}

%% Operational steps
\newcommand{\step}{\mapsto}
\newcommand{\stepsin}[1]{\mathrel{\mapsto^{#1}}}
\newcommand{\stepzero}{\stepsin 0}
\newcommand{\stepone}{\stepsin 1}
\newcommand{\stepstar}{\stepsin{*}}
\newcommand{\bigstepsin}[1]{\mathrel{\Mapsto^{#1}}}
\newcommand{\bigstepzero}{\bigstepsin{0}}
\newcommand{\bigstepany}{\bigstepsin{}}

\newcommand{\pair}[2]{\{ \pi \mapsto {#1} \pipe \pi' \mapsto {#2}\}}
\newcommand{\pairone}[1]{\{ \pi \mapsto {#1}}
\newcommand{\pairtwo}[1]{\pipe \pi' \mapsto {#1}\}}
\newcommand{\emptypair}[0]{\{\}}
\newcommand{\pairWtoXYtoZ}[4]{\{ #1 \mapsto {#2} \pipe #3 \mapsto {#4}\}}
\newcommand{\tru}{\texttt{true}}
\newcommand{\fls}{\texttt{false}}
\newcommand{\ifXthenYelseZ}[3]{\kw{if}#1\,\kw{then}#2\,\kw{else}#3}
\newcommand{\bool}{\mathbb{B}}
\newcommand{\inl}{\kw{inl}}
\newcommand{\inr}{\kw{inr}}
\newcommand{\intag}[1]{\texttt{in}_{#1}}
\newcommand{\els}{\kw {else}}
\newcommand{\seq}{\texttt{seq}}

\newcommand{\dyn}{{?}}
\newcommand{\dynv}{{?}}
\newcommand{\dync}{\u {\text{?`}}}
\newcommand{\uarrow}{\mathrel{\rotatebox[origin=c]{-30}{$\leftarrowtail$}}}
\newcommand{\darrow}{\mathrel{\rotatebox[origin=c]{30}{$\twoheadleftarrow$}}}
\newcommand{\upcast}[2]{\langle{#2}\uarrow{#1}\rangle}
\newcommand{\dncast}[2]{\langle{#1}\darrow{#2}\rangle}
\newcommand{\obcast}[2]{\langle{#1}\Leftarrow{#2}\rangle}
\newcommand{\err}{\mho}
\newcommand{\diverge}{\Omega}
\newcommand{\print}{\kw{print}}
\newcommand{\roll}{\kw{roll}}
\newcommand{\rollty}[1]{\texttt{roll}_{#1}\,\,}
\newcommand{\unroll}{\kw{unroll}}
\newcommand{\unrollty}[1]{\texttt{unroll}_{#1}\,\,}
\newcommand{\defupcast}[2]{\langle\kern-1ex~\langle{#2}\uarrow{#1}\rangle\kern-1ex~\rangle}
\newcommand{\defdncast}[2]{\langle\kern-1ex~\langle{#1}\darrow{#2}\rangle\kern-1ex~\rangle}

\newcommand{\result}{\text{result}}
\newcommand{\Set}{\text{Set}}
\newcommand{\relto}{\to}
\newcommand{\M}{\mathcal{M}}
\newcommand{\sq}{\square}
\newcommand{\lett}{\kw{let}}
\newcommand{\letXbeYinZ}[2]{\lett#2 = #1;}
\newcommand{\bindXtoYinZ}[2]{\kw{bind}#2 \leftarrow #1;}
\newcommand{\too}{\kw{to}}
\newcommand{\case}{\kw{case}}
\newcommand{\kw}[1]{\texttt{#1}\,\,}
\newcommand{\absurd}{\kw{absurd}}
\newcommand{\caseofXthenYelseZ}[3]{\case #1 \{ #2 \pipe #3 \}}
\newcommand{\caseofX}[1]{\case #1}
\newcommand{\thenY}{\{}
\newcommand{\elseZ}[1]{\pipe #1 \}}
\newcommand{\pmpairWtoXYinZ}[4]{\kw{split} #1\,\kw{to} (#2,#3). #4}
\newcommand{\pmpairWtoinZ}[2]{\kw{split} #1\,\kw{to} (). #2}
\newcommand{\pmmuXtoYinZ}[3]{\kw{unroll} #1 \,\kw{to} \roll #2. #3}
\newcommand{\ret}{\kw{ret}}
\newcommand{\thunk}{\kw{thunk}}
\newcommand{\force}{\kw{force}}
\newcommand{\abort}{\kw {abort}}
\newcommand{\with}{\mathbin{\&}}
\DeclareMathOperator*{\With}{\&}

\newcommand{\dyncaseofX}{\kw{tycase}}
\newcommand{\elseZandmore}{\pipe\,}
\newcommand{\dyncaseofXthenOnePairSumU}[5]{\kw{tycase} #1\,\{ #2 \pipe #3 \pipe #4 \pipe #5 \}}
\newcommand{\dyncaseofXthenYelseZ}[3]{\kw{tycase} #1\,\{ #2 \pipe #3 \}}
\newcommand{\dyncocaseWithFunF}[3]{\{\with \mapsto #1 \pipe (\to) \mapsto #2 \pipe \u F \mapsto #3 \}}
\newcommand{\dyncaseofXthenBoolUPair}[4]{\kw{tycase} #1\,\{ #2 \pipe #3 \pipe #4 \}}
\newcommand{\dyncocaseFunF}[2]{\{(\to) \mapsto #1 \pipe \u F \mapsto #2 \}}

\newcommand{\bnfalt}{\mathrel{\bf \,\mid\,}}
\newcommand{\alt}{\bnfalt}
\newcommand{\bnfdef}{\mathrel{\bf ::=}}
\newcommand{\bnfadd}{\mathrel{\bf +::=}}
\newcommand{\bnfsub}{\mathrel{\bf -::=}}

\newcommand\dynvctx[0]{\mathsf{dyn\mathord{-}vctx}}
\newcommand\dyncctx[0]{\mathsf{dyn\mathord{-}cctx}}

\newcommand\leastdynv[0]{\bot_{\mathsf{v}}}
\newcommand\leastdync[0]{\bot_{\mathsf{c}}}

\newcommand\errordivergeleft[0]{\preceq\ltdyn}
\newcommand\errordivergeright[0]{\ltdyn\succeq}
\newcommand\errordivergerightop[0]{\preceq\gtdyn}

\newcommand\cbvtocbpvcomp[1]{#1^{c}}
\newcommand\cbvtocbpvval[1]{#1^{v}}
\newcommand\cbvtocbpvstk[1]{#1^{s}}
\newcommand\cbvtocbpvty[1]{#1^{ty}}
\newcommand\purely{\downarrow}

% Stack formatting
\newenvironment{stackAux}[2]{%
\setlength{\arraycolsep}{0pt}
\begin{array}[#1]{#2}}{
\end{array}\ignorespacesafterend}
\newenvironment{stackCC}{
\begin{stackAux}{c}{c}}{\end{stackAux}\ignorespacesafterend}
\newenvironment{stackCL}{
\begin{stackAux}{c}{l}}{\end{stackAux}\ignorespacesafterend}
\newenvironment{stackTL}{
\begin{stackAux}{t}{l}}{\end{stackAux}\ignorespacesafterend}
\newenvironment{stackTR}{
\begin{stackAux}{t}{r}}{\end{stackAux}\ignorespacesafterend}
\newenvironment{stackBC}{
\begin{stackAux}{b}{c}}{\end{stackAux}\ignorespacesafterend}
\newenvironment{stackBL}{
\begin{stackAux}{b}{l}}{\end{stackAux}\ignorespacesafterend}

%% Local Variables:
%% compile-command: "./latexrun jfp-gtt.tex"
%% End: