\newcommand\ch{\check{$\Leftarrow$}}
\newcommand\f{\varphi}
\renewcommand\v{\mathrel\vdash}
\newcommand\p{\mathrel\otimes}
\newcommand\s{\mathrel\oplus}
\renewcommand\u{\mathbf{1}}
\newcommand\z{\mathbf{0}}
\newcommand\ar{\rightarrow}
\newcommand{\atoms}[1]{\AA_{#1}}
\newcommand{\first}[1]{\mbox{\bf first}(#1)}
\newcommand{\last}[1]{\mbox{\bf last}(#1)}
\newcommand{\lastinv}[1]{\mbox{\bf last}^{-1}(#1)}
\newcommand{\st}[2]{\bbx{#2}_{\!#1}}
\newcommand{\sr}[2]{\bx{#2}_{\!#1}}
%\newcommand\ends{\mathit{r}}
\newcommand\bigs{\bigsqcup}
\newcommand\Progs{{\sf P}}
\newcommand\HL{{\sf HL}}
%\newcommand\S{{\sf S}}
\newcommand\RegPB{\ensuremath{\mathsf{Reg}_{\Progs,\Bool}}}
\newcommand\GddStr{\ensuremath{\Sigma_{\Progs,\Bool}}}

\def\xinfer[#1]#2#3{\infer[\mbox{\scriptsize{#1}}]{#2}{#3}}
\def\xinfers[#1]#2#3{\infer*[\mbox{\scriptsize{#1}}]{#2}{#3}}
%\newcommand\comp#1#2{{#1}\mathrel{;}{#2}}
\newcommand\judge[2]{{#1}\mathrel\vdash{#2}}
\newcommand\njudge[2]{{#1}\mathrel\nvdash{#2}}
\newcommand\frat[2]{\displaystyle\frac{#1}{#2}}
\newcommand\lleq{\sqsubseteq}
%\newcommand\union{\mathrel\cup}
%\newcommand\intersect{\mathrel\cap}
\newcommand\eqv[1]{#1/\mbox{$\equiv$}}
\renewcommand\plus{^+}

\newcommand\definerule[1]{\mbox{\textbf{(#1)}}}

\newcommand\Rimp{\definerule{R\:$\imp$}}
%\newcommand\Limp{\definerule{L\:$\imp$}}
\newcommand\Limp{\definerule{I\:$\imp$}}
\newcommand\Iimp{\definerule{I\:$\imp$}}
\newcommand\Ip{\definerule{I\:$\p$}}
\newcommand\Is{\definerule{I\:$\s$}}
\newcommand\Istar{\definerule{I\:$\star$}}
\newcommand\Ibot{\definerule{I\:$\z$}}
\newcommand\Ep{\definerule{E\:$\p$}}
\newcommand\ELs{\definerule{E1\:$\s$}}
\newcommand\ERs{\definerule{E2\:$\s$}}
\newcommand\ELstar{\definerule{E1\:$\star$}}
\newcommand\ERstar{\definerule{E2\:$\star$}}
\newcommand\Eone{\definerule{E\:$\u$}}
%\newcommand\Eimp{\definerule{E\:$\imp$}}
%\newcommand\Eimp{\definerule{MP}}
\newcommand\Eimp{\definerule{ER\:$\imp$}}
%\newcommand\MP{\definerule{MP}}
\newcommand\Wpsi{\definerule{W\:$\psi$}}
\newcommand\Wp{\definerule{W\:$p$}}
\newcommand\Wstar{\definerule{W\:$\star$}}
%\newcommand\Wbot{\definerule{W\:$\z$}}
\newcommand\Cut{\definerule{cut}}
\newcommand\IH{\definerule{IH}}
\newcommand\LH{\definerule{LH}}
\newcommand\Iplus{\definerule{I\:$\plus$}}
\newcommand\Eplus{\definerule{E\:$\plus$}}
\newcommand\Wplus{\definerule{CC\:$\plus$}}
\newcommand\Curry{\definerule{curry}}
\newcommand\Uncurry{\definerule{uncurry}}
\newcommand\Iter{\definerule{iter}}
\newcommand\Ident{\definerule{ident}}
\newcommand\Mono{\definerule{mono}}
\newcommand\TCut{\definerule{test-cut}}


\newcommand\mgname[1]{{\mathfrak m}_{#1}} 
\renewcommand\mg[2]{\mgname{#1}(#2)} 
\newcommand\gsname{\mathrm{gs}}
\newcommand\gs[1]{\gsname(#1)}
\newcommand\trace[3]{#1_0#2_0#1_1\cdots #1_{#3-1}#2_{#3-1}#1_#3}
\newcommand\inftrace[2]{{#1}_0{#2}_0{#1}_1{#2}_1\cdots}
%\newcommand\GSname{\mathit{GS}}
%\newcommand\GS[1]{\GSname(#1)}
\newcommand\Rname{\mathit{R}}
\renewcommand\R[1]{\Rname(#1)}
\newcommand\Hname{\mathit{H}}
\renewcommand\H[1]{\Hname(#1)}
\newcommand\Gname{\mathit{G}}
\renewcommand\G[1]{\Gname(#1)}

\newcommand\trans[4]{{#2}\goesto{#3}{#1}{#4}}
\newcommand\tx[3]{{#1}\goesto{#2}{}{#3}}
\renewcommand\lbl[1]{\mathbf{label}(#1)}
\newcommand\smallfirst[1]{{\scriptstyle\mathbf{first}}(#1)}
\newcommand\smalllast[1]{{\scriptstyle\mathbf{last}}(#1)}
\newcommand\FreeB{\FF_\Bool}
\renewcommand\aa{{\bf a}}
\renewcommand\tt{{\bf t}}

\newcommand\level[1]{\mathbf{level}(#1)}
\renewcommand\true{\mathbf{true}}
\renewcommand\false{\mathbf{false}}
\renewcommand\c{\mathrel{\triangleleft}}
%\newcommand\GddStr{\ensuremath{\mathit{GS}_{\Progs,\Bool}}}
%\newcommand\PGddStr{\ensuremath{\mathit{PGS}_{\Progs,\Bool}}}
\renewcommand\GddStr{\ensuremath{\mathbf{GS}}}
\newcommand\PGddStr{\ensuremath{\mathbf{PGS}}}
\newcommand\DAGS{DAGS}
\newcommand\AGS{AGS}
\newcommand\PGSname{\mathit{PGS}}
\newcommand\PGS[1]{\PGSname(#1)}

\newcommand\sig[3]{\sigma_{#1}({#2},{#3})}
\newcommand\sigb[3]{\sig{#1}{\bx{#2}}{#3}}
\newcommand\lcpName{\operatornamewithlimits{\mathbf{lcp}}}
\newcommand\lcp[2]{\lcpName_{#1}\:{#2}}

\renewcommand\S{\ensuremath{\mathsf{S}}}

\renewcommand\bbx[1]{\bx{\hbox{\kern-4pt$\bx{#1}$\kern-4pt}}}


