\newcommand{\To}{\Rightarrow}
\newcommand{\inl}{\mathsf{inl}}
\newcommand{\inr}{\mathsf{inr}}
\newcommand{\alt}{\mathrel{\bf \,\mid\,}}

\newcommand{\ob}{\text{Ob}}


\newcommand{\extlc}{\text{Ext-}\lambda}
\newcommand{\extlcm}{\text{Ext-}\lambda^{-\text{trans}}}
\newcommand{\extlcmm}{\text{Ext-}\lambda^{-\text{trans}-\text{cast}}}
\newcommand{\extlcprime}{\text{Ext-}\lambda'}
\newcommand{\intlc}{\text{Int-}\lambda}
\newcommand{\intlcbisim}{\text{Int$_\approx$-}\lambda}
\newcommand{\erase}[1]{\lfloor {#1} \rfloor}


\newcommand{\uarrowl}{\mathrel{\rotatebox[origin=c]{-30}{$\leftarrowtail$}}}
\newcommand{\uarrowr}{\mathrel{\rotatebox[origin=c]{60}{$\leftarrowtail$}}}
\newcommand{\darrowl}{\mathrel{\rotatebox[origin=c]{30}{$\twoheadleftarrow$}}}
\newcommand{\darrowr}{\mathrel{\rotatebox[origin=c]{120}{$\twoheadleftarrow$}}}
\newcommand{\vuarrow}{\mathrel{\rotatebox[origin=c]{-90}{$\leftarrowtail$}}}
\newcommand{\vdarrow}{\mathrel{\rotatebox[origin=c]{90}{$\twoheadleftarrow$}}}

% Types, terms, and precision 

\newcommand{\dyn}{?}
\newcommand{\nat}{\text{Nat}}
\newcommand{\bool}{\text{Bool}}
\newcommand{\ra}{\rightharpoonup}
\newcommand{\Ret}[1]{\mathsf{Ret\,}{#1}}
\newcommand{\hole}[1]{\bullet \colon {#1}}
\newcommand{\dyntodyn}{\dyn \ra\, \dyn}


\newcommand{\up}[2]{\langle{#2}\uarrowl{#1}\rangle}
\newcommand{\dn}[2]{\langle{#1}\darrowl{#2}\rangle}

\newcommand{\upc}[2]{\text{up}\,{#1}\,{#2}}
\newcommand{\dnc}[2]{\text{dn}\,{#1}\,{#2}}


% \newcommand{\ret}{\mathsf{ret}}
\newcommand{\err}{\mho}
\newcommand{\zro}{\textsf{zro}}
\newcommand{\suc}{\textsf{suc}}
\newcommand{\lda}[2]{\lambda {#1} . {#2}}
\newcommand{\injarr}[1]{\textsf{Inj}_\ra ({#1})}
\newcommand{\injnat}[1]{\textsf{Inj}_\text{nat} ({#1})}
\newcommand{\casenat}[4]{\text{Case}_\text{nat} ({#1}) \{ \text{no} \to {#2} \alt \text{nat}({#3}) \to {#4} \}}
\newcommand{\casearr}[4]{\text{Case}_\ra ({#1}) \{ \text{no} \to {#2} \alt \text{fun}({#3}) \to {#4} \}}
\newcommand{\casedyn}[5]{\text{Case}_\Dyn ({#1}) \{ \text{nat}({#2}) \to {#3} \alt \text{fun}({#4}) \to {#5} \}}
%\newcommand{\bind}[3]{\text{var } {#1} = {#2} \text{ in } {#3}}
\newcommand{\matchnat}[4]{\text{match } {#1} \text{ with } \{ \textsf {zero} \Rightarrow {#2} \alt \textsf{ suc } {#3} \Rightarrow {#4} \}}

\newcommand{\refl}{\text{refl}}

\newcommand{\Lift}{\text{Lift}}

%\newcommand{\rel}{\circ\hspace{-4px}-\hspace{-4px}\bullet}
\newcommand{\rel}{\mathrel{\circ\mkern-6mu-\mkern-6mu\bullet}}
% \newcommand{\wand}{\mathrel{-\mkern-6mu*}}
\newcommand{\wand}{\mathrel{\multimap}}
\newcommand{\ltdyn}{\sqsubseteq}
\newcommand{\gtdyn}{\sqsupseteq}
\newcommand{\equidyn}{\mathrel{\gtdyn\ltdyn}}
\newcommand{\gamlt}{\Gamma^\ltdyn}
\newcommand{\deltalt}{\Delta^\ltdyn}
\newcommand{\relcomp}{\odot}

\newcommand{\hasty}[3]{{#1} \vdash {#2} \colon {#3}}
\newcommand{\vhasty}[3]{{#1} \vdash^v {#2} \colon {#3}}
\newcommand{\phasty}[3]{{#1} \vdash^c {#2} \colon {#3}}
\newcommand{\etmprec}[4]{{#1} \vdash {#2} \ltdyn_e {#3} \colon {#4}}
\newcommand{\itmprec}[4]{{#1} \vdash {#2} \ltdyn_i {#3} \colon {#4}}
\newcommand{\etmequidyn}[4]{{#1} \vdash {#2} \equidyn_e {#3} \colon {#4}}
\newcommand{\itmequidyn}[4]{{#1} \vdash {#2} \equidyn_i {#3} \colon {#4}}
\newcommand{\synbisim}{\approx_{\text{syn}}}

\newcommand{\Dwn}{\Downarrow}
\newcommand{\qte}[1]{\text{quote}({#1})}

\newcommand{\elab}[1]{\text{Elab}({#1})}

% Perturbations
\newcommand{\pertp}{\text{Pert}^\text{P}}
\newcommand{\perte}{\text{Pert}^\text{E}}
\newcommand{\pertdyn}[2]{\text{pert-dyn}({#1}, {#2})}
\newcommand{\delaypert}[1]{\text{delay-pert}({#1})}

\newcommand{\pertc}{\text{Pert}_{\text{C}}}
\newcommand{\pertv}{\text{Pert}_{\text{V}}}


% SGDT and Intensional Stuff

\newcommand{\later}{\vartriangleright}
\newcommand{\type}{\texttt{Type}}
\newcommand{\lob}{\text{L\"{o}b}}
\newcommand{\tick}{\mathsf{tick}}
\newcommand{\nxt}{\mathsf{next}}
\newcommand{\fix}{\mathsf{fix}}
\newcommand{\kpa}{\kappa}

% Model-related stuff
\newcommand{\calV}{\mathcal{V}}
\newcommand{\calE}{\mathcal{E}}
\newcommand{\calVk}{\mathcal{V}_k}
\newcommand{\calEk}{\mathcal{E}_k}
\newcommand{\tok}{\mathrel{\mathop{\to}\limits^{\textrm{\footnotesize k}}}}
\newcommand{\timesk}{\mathrel{\mathop{\times}\limits^{\textrm{k}}}}
\newcommand{\Fk}{\mathrel{\mathop{F}\limits^{\textrm{k}}}}
\newcommand{\Uk}{\mathrel{\mathop{U}\limits^{\textrm{k}}}}

\newcommand{\op}[1]{{#1}^{\textrm{op}}}
\newcommand{\calC}{\mathcal{C}}
\newcommand{\Set}{\mathsf{Set}}
\newcommand{\Yo}{\mathsf{Yo}}
\newcommand{\Hom}{\mathsf{Hom}}
\newcommand{\calS}{\mathcal{S}}
\newcommand{\gfix}{\texttt{gfix}}
\newcommand{\calU}{\mathcal{U}}
\newcommand{\laterhat}{\widehat{\later}}
\newcommand{\El}{\mathsf{El}}
\newcommand{\Clock}{\mathsf{Clock}}

\newcommand{\Machine}[1]{\mathsf{Machine}\, {#1}}


% Predomains and EP pairs
\newcommand{\Nat}{\mathsf{Nat}}
\newcommand{\Dyn}{\mathsf{Dyn}}
\newcommand{\ty}[1]{\langle {#1} \rangle}
\newcommand{\li}{L_\mho}
\newcommand{\liclk}[1]{L_\mho [{#1}]}

\newcommand{\ext}[2]{\text{ext}\,{#1}\,{#2}}
\newcommand{\map}[2]{\text{map}\,{#1}\,{#2}}

\newcommand{\ltls}{\lesssim}
\newcommand{\bisim}{\approx}
\newcommand{\semlt}{\le}
\newcommand{\semltbad}{\lesssim}

%\newcommand{\injarr}{\textsf{Inj}_\to}
%\newcommand{\injnat}{\textsf{Inj}_\mathbb{N}}

\newcommand{\id}{\mathsf{id}}
\newcommand{\ep}{\leadsto}

\newcommand{\emb}[2]{\mathsf{emb}_{#1}({#2})}
\newcommand{\proj}[2]{\mathsf{proj}_{#1}({#2})}

\newcommand{\monto}{\to_m}


% Notation for wait functions
\newcommand{\wre}{w_r^e}
\newcommand{\wle}{w_l^e}
\newcommand{\wrp}{w_r^p}
\newcommand{\wlp}{w_l^p}

\newcommand{\sem}[1]{\llbracket {#1} \rrbracket}
\newcommand{\semgl}[1]{{\sem{#1}}^\text{gl}}


% Denotational model
\newcommand{\ptb}{\text{ptb}}
\newcommand{\push}{\text{push}}
\newcommand{\pull}{\text{pull}}

\newcommand{\pv}{P^{\mathcal{V}}}
\newcommand{\pe}{P^{\mathcal{E}}}
\newcommand{\ptbv}{\text{ptb}^\mathcal{V}}
\newcommand{\ptbe}{\text{ptb}^\mathcal{E}}

\newcommand{\Ppure}{P}
\newcommand{\Pk}{P^K}
\newcommand{\ptbk}{\text{ptb}^K}


\newcommand{\upf}{\text{up}}
\newcommand{\dnf}{\text{dn}
}
\newcommand{\arr}{\to}
\newcommand{\comp}{\bullet}

\newcommand{\vf}{\mathcal{V}_f}
\newcommand{\vsq}{\mathcal{V}_{sq}}
\newcommand{\ef}{\mathcal{E}_f}
\newcommand{\esq}{\mathcal{E}_{sq}}

\newcommand{\sv}{s_{\mathcal{V}}}
\newcommand{\tv}{t_{\mathcal{V}}}
\newcommand{\rv}{r_{\mathcal{V}}}
\newcommand{\se}{s_{\mathcal{E}}}
\newcommand{\te}{t_{\mathcal{E}}}
\newcommand{\re}{r_{\mathcal{E}}}

\newcommand{\Ff}{F_f}
\newcommand{\Fsq}{F_{sq}}
\newcommand{\Uf}{U_f}
\newcommand{\Usq}{U_{sq}}
\newcommand{\arrf}{\arr_f}
\newcommand{\arrsq}{\arr_{sq}}

\newcommand{\vsim}{\mathcal{V}_{\bisim}}
\newcommand{\esim}{\mathcal{E}_{\bisim}}
\newcommand{\svsim}{s_{\mathcal{V}}^\bisim}
\newcommand{\tvsim}{t_{\mathcal{V}}^\bisim}
\newcommand{\rvsim}{r_{\mathcal{V}}^\bisim}
\newcommand{\sesim}{s_{\mathcal{E}}^\bisim}
\newcommand{\tesim}{t_{\mathcal{E}}^\bisim}
\newcommand{\resim}{r_{\mathcal{E}}^\bisim}



\newcommand{\ve}{\mathcal{V}_e}
\newcommand{\ee}{\mathcal{E}_e}

\newcommand{\relatedin}[3]{{#1}\, {#3}\, {#2}}
\newcommand{\binrel}[1]{\mathbin{#1}}


\newcommand{\da}{\downarrow}

\newcommand{\ret}{\text{ret}}
\newcommand{\bind}[3]{{#1} <- {#2}\, ; \, {#3}}

\newcommand{\piv}{\Pi^\mathcal{V}}
\newcommand{\pie}{\Pi^\mathcal{E}}