
\newcommand{\mi}[1]{\mathit{#1}}

% defs.tex ---
% for WADT99
% copied from Tarlecki's definitions for frocos'98
% modified from moving defs.tex

\newcommand{\ASP}{\mathit{ASP}}
\newcommand{\SP}{\mathit{SP}}
\newcommand{\UDD}{\mathit{UDD}}
\newcommand{\UT}{\mathit{T}}
\newcommand{\UN}{\mathit{U}}
\newcommand{\UDecl}{\mathit{Dcl}}
\newcommand{\UDefn}{\mathit{Dfn}}

\newcommand{\parspec}[3]{#1{\stackrel{#2}{\longrightarrow}}#3}

\newcommand{\archspec}[2]{\textbf{arch spec }#1\textbf{ result }#2}
\newcommand{\decl}[2]{#1\colon#2}
\newcommand{\dfn}[2]{#1=#2}
\newcommand{\amlg}[4]{#1\textbf{ with }#2\textbf{ and }#3\textbf{ with }#4}
\newcommand{\appl}[3]{#1\lbrack#2\textbf{ fit }#3\rbrack}
\newcommand{\gris}{\mathrel{::=}}


\newcommand{\Mset}{\mathcal{M}}
\newcommand{\Fset}{\mathcal{F}}

\newcommand{\Dgm}{\mathit{Diag}}
\newcommand{\Shape}[1]{\mathit{Shape}(#1)}
\newcommand{\Nodes}[1]{\mathit{Nodes}(#1)}
\newcommand{\Edges}[1]{\mathit{Edges}(#1)}
%\newcommand{\restrict}[2]{\reduct{#1}{#2}}

\newcommand{\fm}[2]{\langle#1\rangle_{#2}}

\newcommand{\incl}[2]{\iota_{{#1}\subseteq{#2}}}

\newcommand{\st}{\mathit{st}}
\newcommand{\stC}{\mathit{C}_{\st}}
\newcommand{\stB}{\mathit{B}_{\st}}
\newcommand{\stP}{\mathit{P}_{\st}}
\newcommand{\emptystC}{\stC^\emptyset}
\newcommand{\emptyUC}{\UC^\emptyset}
\newcommand{\UC}{\mathcal{C}}
\newcommand{\UEv}{\mathit{UEv}}
\newcommand{\Uset}{\mathcal{V}}
\newcommand{\UU}{\mathit{V}}

\newcommand{\EstC}{\mathcal{C}_{\st}}
\newcommand{\emptyEstC}{\EstC^\emptyset}
\newcommand{\EstB}{\mathcal{B}_{\st}}
\newcommand{\SD}{D}

\newcommand{\CstC}{\mathfrak{C}_{\st}}

\newcommand{\getstctx}{\mathit{ctx}}

\newcommand{\env}{\mathit{E}}

\newcommand{\lambdaexp}[2]{\lambda#1\cdot#2}
\newcommand{\reduct}[2]{#1|_{#2}}

\newlength{\croutw}
\newlength{\crouth}
\newcommand{\crossout}[1]%
        {\settowidth{\croutw}{$#1$}\settoheight{\crouth}{$#1$}#1%
        \hspace{-1.0\croutw}\raisebox{0.3\crouth}{\rule{\croutw}{0.1ex}}}

\newcommand{\commentout}[1]{\ignorespaces}
\newcommand{\underscore}{\rule{3mm}{0.005in}}

\newcommand{\extaticsem}[3]{#1 \vdash #2 \extsmb #3}
\newcommand{\extsmb}{\mathrel{\rhd\hspace{-0.5em}\rhd}}

\newcommand{\rulesection}[1]{\[\fbox{$#1$}\]}
\newcommand{\infrule}[2]{\frac{#1}{#2}}
\newcommand{\staticsem}[3]{#1 \vdash #2 \rhd #3}
\newcommand{\modelsem}[3]{#1 \vdash #2 \Rightarrow #3}
\newcommand{\staticsembreak}[3]{\begin{array}{r}#1 \vdash #2 \qquad\\ 
                                                \rhd #3 \end{array}}
\newcommand{\modelsembreak}[3]{\begin{array}{r}#1 \vdash #2 \qquad\\
                                                 \Rightarrow #3 \end{array}}



% Defs from Till 


%\newenvironment{proof}{\begin{trivlist}\item[\textbf{Proof. 
%}]}{\end{trivlist}}

%\newcommand{\qed} {\hfill{$\Box$}}

\newcommand{\ttsize}{\footnotesize }
\newcommand{\NT}[1]{{\ttsize\texttt{#1}}}

%\newcommand{\gram}[1]{{\texttt{#1}}}
%\newenvironment{grammar}
% {\texonly{\footnotesize}
%  \begin{example}}{\end{example}\normalsize}
%\newenvironment{slgrammar}
% {\texonly{\footnotesize}
%  \begin{example}\texorhtml{\slshape}{\it}}{\end{example}\normalsize}


\newcommand{\cofidirectory}{}


%symbols etc
\newcommand{\parrightarrow}{\p\rightarrow}
\newcommand{\p}[1]{\mathrel{\ooalign{\hfil$\mapstochar\mkern 
5mu$\hfil\cr$#1$}}}
%\newsavebox{\pararrbox}
%\savebox{\pararrbox}{$\ \rightarrow\!\!\!\!\!\!{\raisebox{.15cm}{\tiny
%p}}\ \ $}
%\newcommand{\classicalpararrow}{{\usebox{\pararrbox}}}
\newcommand{\totrightarrow}{\rightarrow}


\newcommand{\X}{CASL}
%\newcommand{\congr}{\equiv}
%\newcommand{\TSX}{{T_{\Sigma}(X)}}
\newcommand{\LSX}{{W_{\Sigma}(X)}}

\newcommand{\Powfin}{\mathcal{P}_\omega}
\newcommand{\gen}[1]{\mid_{#1}}
\newcommand{\cogen}[1]{\mid^{#1}}
\newcommand{\induce}[2]{\mid^{#1}_{#2}}
\newcommand{\inducefrom}[1]{\!\mid_{#1}}
\newcommand{\induceto}[1]{\mid^{#1}}

%\makeindex

%\newcommand{\Mod}{\mathbf{Mod}}
\newcommand{\sen}{\mathbf{Sen}}

%\newcommand{\Sen}{\mathbf{Sen}}

%\newcommand{\Sign}{\mathbf{Sign}}
%\newcommand{\Set}{\mathbf{Set}}
%\newcommand{\ttsize}{\footnotesize }
%\newcommand{\NT}[1]{{\ttsize\texttt{#1}}}
\newcommand{\PF}{\mathit{PF}}
\newcommand{\TF}{\mathit{TF}}

\newcommand{\SY}{\mathit SY}
\newcommand{\SYs}{\mathit SYs}
\newcommand{\RSY}{\mathit RSY}
\newcommand{\RSYs}{\mathit RSYs}
\newcommand{\Sym}{\mathit{Sym}}
\newcommand{\RawSym}{\mathit{RawSym}}
\newcommand{\RawSymMap}{\mathit{RawSymMap}}
\newcommand{\IDAsRawSym}{\mathit{IDAsRawSym}}
\newcommand{\SymAsRawSym}{\mathit{SymAsRawSym}}

%\newcommand{\dom}{\mathit{dom}}
%\newcommand{\graph}{\mathit{graph}}
%% incompatible with xypic -- dirk


%\newenvironment{grammar}
% {\ttsize\begin{alltt}}{\end{alltt}}



\newcommand{\TSX}{{T_{\Sigma^\#}(X)}}

\newcommand{\bit}{\begin{itemize}}
\newcommand{\eit}{\end{itemize}}
\newcommand{\Equivalent}{\Leftrightarrow}
%\newcommand{\Implies}{\Rightarrow}
\newcommand{\logand}{\wedge}
\newcommand{\logor}{\vee}
%\newcommand{\union}{\cup}
\newcommand{\intersection}{\cap}
\newcommand{\comp}{\circ}
\newcommand{\suchthat}{\mid}
\newcommand{\congr}{\equiv}
\newcommand{\disjoint}{\uplus}
\newcommand{\buildset}[1]{\{#1\}}
\newcommand{\Si}{\Sigma}
\newcommand{\al}{\alpha}
\newcommand{\pp}[2]{#1_1\commadots #1_{#2}}
%\newcommand{\map}[2]{\colon#1\!\longrightarrow\!#2}
\newcommand{\mmap}[2]{#1\!\longrightarrow\!#2}
\newcommand{\anddots}{\logand\,\cdots\,\logand}
\newcommand{\lldots}{\,\ldots\,}
\newcommand{\ccdots}{\,\cdots\,}
\newcommand{\commadots}{,\lldots,}
\newcommand{\sigspec}[1]{\langle #1 \rangle}
\newcommand{\eq}{\stackrel{\mbox{\scriptsize e}}{=}}
\newcommand{\weq}{\stackrel{\mbox{\scriptsize w}}{=}}

\newcommand{\mBox}[1]{\, \mbox{#1} \,}

\newcommand{\engtwocase}[3]{
\left\{
\begin{array}{ll}
  #1,&\mBox{if }#2\\
  #3,&\mBox{otherwise}
\end{array}\right.}

\newcommand{\threecase}[5]{
\left\{
\begin{array}{ll}
  #1,&\mbox{if }#2\\
  #3,&\mbox{if }#4\\
  #5,&\mbox{otherwise}
\end{array}\right.}

\newcommand{\threefullcase}[6]{
\left\{
\begin{array}{ll}
  #1,&\mbox{if }#2\\
  #3,&\mbox{if }#4\\
  #5,&\mbox{if }#6
\end{array}\right.}

\newcommand{\delete}[1]{$\overline{\mbox{#1}}$}
\newcommand{\new}[1]{{\it\tiny #1}}

\newcommand{\mbs}[1]{\mbox{$#1$}}




\newcommand{\ASL}[1]{[\![#1]\!]}

\newcommand{\sym}{\mathit{sym}}
\newcommand{\totqual}{\mathsf{t}}
\newcommand{\parqual}{\mathsf{p}}
\newcommand{\ws}{\mathit{ws}}
\newcommand{\FinSet}[1]{\mathit{FinSet}(#1)}
\newcommand{\RawSymOf}{\mathit{RawSymOf}}
\newcommand{\Gram}[1]{{\textup{\texttt{#1}}}}

\newcommand{\implicitqualkind}{\mathit{implicit}}
\newcommand{\sortqualkind}{\mathit{sort}}
\newcommand{\funqualkind}{\mathit{fun}}
\newcommand{\predqualkind}{\mathit{pred}}
\newcommand{\SymKind}{\mathit{SymKind}}

%\newcommand{\Sort}{\mathit{Sort}}
\newcommand{\QualFunName}{\mathit{QualFunName}}
\newcommand{\QualPredName}{\mathit{QualPredName}}



% Lutz's definitions


\hfuzz1pc
\sloppy
%\frenchspacing


%\spnewtheorem{thm}{Theorem}[section]{\bfseries}{\itshape}
%\spnewtheorem{cor}[theorem]{Corollary}{\bfseries}{\itshape}
%\spnewtheorem{lem}[theorem]{Lemma}{\bfseries}{\itshape}
%\spnewtheorem{prop}[theorem]{Proposition}{\bfseries}{\itshape}
%\spnewtheorem{defn}[theorem]{Definition}{\bfseries}{\upshape}
%\spnewtheorem{rem}[theorem]{Remark}{\bfseries}{\upshape}
%\spnewtheorem{expl}[theorem]{Example}{\bfseries}{\upshape}
%\spnewtheorem{thmdefn}[theorem]{Theorem and Definition}{\bfseries}{\itshape}
%\spnewtheorem{propdefn}[theorem]{Proposition and Definition}{\bfseries}{\itshape}
%\spnewtheorem{assumption}[theorem]{Assumption}{\bfseries}{\upshape}
%\spnewtheorem{algorithm}[theorem]{Algorithm}{\bfseries}{\upshape}

%% Other environments
%\newenvironment{mycd}
%       {\begin{displaymath}\renewcommand{\arraystretch}{0.5}\begin{CD}}
%       {\end{CD}\end{displaymath}}
\newenvironment{rmenumerate}%
        {\begin{enumerate}\renewcommand{\labelenumi}{(\roman{enumi})}}%
        {\end{enumerate}}
\newenvironment{alenumerate}%
        {\begin{enumerate}\renewcommand{\labelenumi}{(\alph{enumi})}}%
        {\end{enumerate}}
\newenvironment{Alenumerate}%
        {\begin{enumerate}\renewcommand{\labelenumi}{\Alph{enumi})}}%
        {\end{enumerate}}
\newenvironment{numenumerate}%
        {\begin{enumerate}\renewcommand{\labelenumi}{\arabic{enumi})}}%
        {\end{enumerate}}
%\newenvironment{defn}%
%       {\begin{definition}\em}%
%       {\end{definition}}
%\newenvironment{rem}%
%       {\begin{remark}\em}%
%       {\end{remark}}
%\renewenvironment{example}%
%       {\begin{expl}\em}%
%       {\end{expl}}
%\newenvironment{texteqnarray}%
%       {\setlength{\itemsep}{0pt}%
%       \setlength{\topsep}{0pt}%
%       \begin{trivlist}\item[]\begin{displaymath}%
%       \renewcommand{\arraystretch}{1.2}\begin{array}{rcll}}%
%       {\end{array}\end{displaymath}\end{trivlist}}
%\newenvironment{acknowledge}%
%       {\begin{list}{}{\setlength{\leftmargin}{0pt}%
%                       \setlength{\topsep}{1cm}}% 
%       \item{\bf Acknowledgements:}}%
%       {\end{list}}

%\newcommand{\qed}{\hfill\openbox}
%\newenvironment{proof}
%       {\begin{trivlist}\item{\sc Proof: }}
%       {\qed\end{trivlist}}



%% Math definitions
\newcommand{\Cat}{\mathbf}
\newcommand{\Cls}{\mathcal}
\newcommand{\Opname}{\mathrm}

\newcommand{\Ob}{{\Opname{Ob}\,}}
\newcommand{\Mor}{{\Opname{Mor}\,}}
\newcommand{\Epi}{{\Opname{Epi}\,}}
\newcommand{\Mono}{{\Opname{Mono}\,}}
\newcommand{\Iso}{{\Opname{Iso}\,}}
\newcommand{\Ident}{{\Opname{Ident}\,}}
\newcommand{\Op}{{op}}
\newcommand{\colim}{{\Opname{colim}\,}}

\newcommand{\lrule}[3]{(#1)\;\;\infrule{#2}{#3}}
\newcommand{\lrrule}[3]{(#1)\;\;\infrule{\underline{#2}}{#3}}
\newcommand{\laxiom}[2]{(#1)\;\;#2}

\newcommand{\BA}{{\Cat A}}
%\newcommand{\BB}{{\Cat B}}
\newcommand{\BC}{{\Cat C}}
\newcommand{\BD}{{\Cat D}}
\newcommand{\BI}{{\Cat I}}
\newcommand{\BK}{{\Cat K}}
\newcommand{\BL}{{\Cat L}}
\newcommand{\BM}{{\Cat M}}
\newcommand{\BN}{{\Cat N}}
\newcommand{\BS}{{\Cat S}}
\newcommand{\BW}{{\Cat W}}
\newcommand{\Btwo}{{\Cat 2}}

\newcommand{\CC}{{\Cls C}}
\newcommand{\CE}{{\Cls E}}
%\newcommand{\CK}{{\Cls K}}
% \newcommand{\CL}{{\Cls L}}
\newcommand{\CM}{{\Cls M}}
\newcommand{\CO}{{\Cls O}}
\newcommand{\CP}{{\Cls P}}
\newcommand{\CS}{{\Cls S}}
\newcommand{\CT}{{\Cls T}}
\newcommand{\eps}{\varepsilon}

\newcommand{\integers}{{\mathbb Z}}
\newcommand{\tensor}{\otimes}

%\newcommand{\openbox}{\leavevmode
%  \hbox to.77778em{%
%  \hfil\vrule
%  \vbox to.675em{\hrule width.6em\vfil\hrule}%
%  \vrule\hfil}}
\newcommand{\mystrut}[1]{\rule[#1]{0cm}{0.1cm}}



%\newcommand{\red}{\vdash}
\newcommand{\idred}{\red}
\newcommand{\step}{\red_c}
% \newcommand{\stepeq}{\succeq}
\newcommand{\downto}{\succeq}
\newcommand{\upto}{\preceq}
\newcommand{\moremonicthan}{\Rightarrow}
\newcommand{\into}{\hookrightarrow}
\newcommand{\impl}{\Rightarrow}
\newcommand{\id}{{id}}
\newcommand{\ev}{{ev}}
\newcommand{\Hom}{{hom}}
\newcommand{\Dom}{{dom\, }}
\newcommand{\Cod}{{cod}}
\newcommand{\adj}{\dashv}
\newcommand{\powerset}{{\mathcal P}}
\newcommand{\finpowerset}{{\powerset_\omega}}
\newcommand{\kVec}{\mbox{$k$-$\Cat{Vec}$}}
\newcommand{\termObj}{1}

\newcommand{\map}[2]{:#1\to #2}
\newcommand{\restr}[2]{{#1}|_{#2}}
\newcommand{\wordbrace}[1]{\underbrace{\hspace{1.5cm}}_{\displaystyle{#1}}}
\newcommand{\forget}[1]{|_{#1}}
\newcommand{\argument}{\_\!\_}%{\underline{\;\;}}
%\newcommand{\substack}[2]{{{#1} \atop {#2}}}

%% Category Names
\newcommand{\CASLsign}{\Cat{CASLsign}}
\newcommand{\enrCASLsign}{\Cat{enrCASLsign}}
\newcommand{\refCASLsign}{\Cat{refCASLsign}}
%\newcommand{\Mod}{\Cat{Mod}\,}
% the \, caused bad effect when copmbined with indices etc.
\newcommand{\EnrMod}{\Cat{Mod}_e}
\newcommand{\CAT}{\Cat{CAT}}
\newcommand{\Sen}{\Cat{Sen}}
\newcommand{\Sign}{\Cat{Sign}}
\newcommand{\SignVar}{\Cat{Var}}
\newcommand{\EnrSign}{\Cat{EnrSign}}
%\newcommand{\Set}{\Cat{Set}}
\newcommand{\CLS}{\Cat{CLS}}

\newcommand{\SmallSpecName}[1]{\textsc{\small #1}}
%% Institution Names
\newcommand{\EnrInst}{EnrPCFOL}
\newcommand{\CASLInst}{SubPCFOL}
\newcommand{\PCFOLInst}{PCFOL}

%% Words
\newcommand{\Word}{\mathbf}
\newcommand{\Ba}{{\Word{a}}}
\newcommand{\Bb}{{\Word{b}}}
\newcommand{\Bc}{{\Word{c}}}
\newcommand{\Bf}{{\Word{f}}}
\newcommand{\Bg}{{\Word{g}}}
\newcommand{\Bh}{{\Word{h}}}
\newcommand{\Bl}{{\Word{l}}}
\newcommand{\Br}{{\Word{r}}}



%% For HasCASL:

\newcommand{\HasCASL}{{\sc HasCasl}\xspace}
\newcommand{\ML}{{\textsf{ML}}\xspace}
\newcommand{\BaseTypes}{B}
\newcommand{\SimpleTypes}{T}
\newcommand{\TotalFunType}[2]{#1\to #2}
\newcommand{\sbullet}{\mbox{ $\scriptstyle\bullet$ }}
\newcommand{\lambdaTotal}[2]{\lambda\, #1\sbullet\!\! !\, #2}
\newcommand{\PartialFunType}[2]{#1\to ?#2}
\newcommand{\lambdaPartial}[2]{\lambda\, #1\sbullet #2}
\newcommand{\lambdaType}[2]{\lambda\, #1\sbullet #2}
\newcommand{\NonStrictFunType}[2]{\PartialFunType{\Maybe{#1}}{#2}}
\newcommand{\lambdaNonStrict}[2]{\lambda\, #1\sbullet #2}
\newcommand{\substTerm}[3]{{#1[#3/#2]}}
\newcommand{\PredType}[1]{{\textsf{pred}(#1)}}
\newcommand{\ProdType}[2]{#1 * #2}
\newcommand{\pMonType}[2]{#1 -\!\!\mu\!\!\to\hspace{-1pt}? #2}
\newcommand{\tMonType}[2]{#1 -\!\!\mu\!\!\to #2}
\newcommand{\pContType}{Pcont}
\newcommand{\tContType}{Tcont}
\newcommand{\projOp}[1]{{pr_#1}}
\newcommand{\fst}{{\textsf{fst}}}
\newcommand{\snd}{{\textsf{snd}}}
\newcommand{\UnitType}{{\textsf{unit}}}
\newcommand{\UnitOp}{{()}}
\newcommand{\Maybe}[1]{?#1}
\newcommand{\TypeSchemes}{{TS}}
\newcommand{\TypeContext}{\mathcal{C}}
\newcommand{\UniversalType}[2]{{\forall #1\sbullet #2}}
\newcommand{\applyPoly}[2]{{#1[#2]}}
%\newcommand{\lambdaPoly}[2]{\Lambda #1:\TypeKind.\, #2}
\newcommand{\ConstrainedType}[2]{{#1 \Rightarrow #2}}
\newcommand{\Constraint}{C}
\newcommand{\TypeKind}{\textsf{type}}
\newcommand{\TypeVars}{{TV}}
\newcommand{\TypeOps}{{TO}}
\newcommand{\PseudoTypes}{{PT}}
\newcommand{\SubstType}[3]{{#1[#3/#2]}}
\newcommand{\varco}[1]{{v^+(#1)}}
\newcommand{\varcontra}[1]{{v^-(#1)}}
\newcommand{\Covar}{\textsf{covariant}}
\newcommand{\Contravar}{\textsf{contravariant}}
\newcommand{\sigSorts}{S}
\newcommand{\sigClasses}{C}
\newcommand{\sigConstrs}{T}
\newcommand{\sigAlias}{{A}}
\newcommand{\sigExpand}{{\varepsilon}}
\newcommand{\unalias}{{\bar\sigExpand}}
\newcommand{\sigSub}{\leq}
\newcommand{\extSub}{\leq_*}
\newcommand{\elPred}[2]{{#1\in #2}}
\newcommand{\downCast}[2]{{#1\textsf{ as }#2}}
\newcommand{\upCast}[2]{{#1:#2}}
\newcommand{\sigOps}{O}
\newcommand{\IndVars}{V}
\newcommand{\ifthenelse}[3]{{\textsf{if }#1\textsf{ then }#2
                        \textsf{  else }#3}}
\newcommand{\BT}{B}
\newcommand{\emb}{{emb}}

\newcommand{\Context}{\Gamma}
\newcommand{\ContextTerm}[3]{{#1 \rhd #2: #3}}
\newcommand{\ContextEq}[2]{{#1 \rhd #2}}
\newcommand{\ContextEntails}[3]{{#2 \entails_{#1} #3}}
\newcommand{\ContextImpl}[3]{{#2 \impl_{#1} #3}}
\newcommand{\exeq}{\stackrel{e}{=}}
\newcommand{\IsDef}{\operatorname{def}}

\newcommand{\isFormula}[1]{{#1\in\textsf{Prop}}}

\newcommand{\Model}{M}
\newcommand{\Sem}[1]{{[\![#1]\!]}}
\newcommand{\extendsTo}{\preceq}
\newcommand{\True}{\top}
\newcommand{\False}{\bot}
\newcommand{\uexists}{\exists !}
\newcommand{\iotaTerm}[2]{\iota #1\sbullet #2}
%\newcommand{\conj}{\wedge}
\newcommand{\disj}{\vee}
\newcommand{\modimpl}{\to}
\newcommand{\modiff}{\leftrightarrow}
\newcommand{\intEq}{eq}
\newcommand{\dOrder}[3]{#2 \le\![#1]\,#3}
\newcommand{\resTerm}[2]{#1\ res\ #2}
\newcommand{\mono}[2]{\operatorname{mono}_{#1}#2}
%\newcommand{\entails}{\vdash}

%% CASL constructs

%% HasCASL constructs
\newcommand{\Class}{\textbf{class}}
\newcommand{\Instance}{\textbf{instance}}
\newcommand{\Program}{\textbf{program}}
\newcommand{\Internal}{\textbf{internal}}
\providecommand{\pfun}{\mathrel{\rightarrow?}}
\newcommand{\iimpl}{\Rightarrow}
\newcommand{\iconj}{\wedge}

%% For Monads:
\newcommand{\BBT}{\mathbb{T}}
\newcommand{\DO}{\operatorname{do}}
\newcommand{\Let}{\operatorname{let}}
\newcommand{\retOp}{\operatorname{ret}}
\newcommand{\retOpHC}{\mathit{ret}}
\newcommand{\ret}[1]{\retOp #1}
\newcommand{\letTerm}[2]{\DO\, #1; \ #2}
\newcommand{\leteq}{\leftarrow}
\newcommand{\se}[2]{\mathsf{se}(#1,#2)}
\newcommand{\Pfin}{\mathcal P_{\mathit{fin}}}

%% Program logic
\newcommand{\nec}{\square\,}
\newcommand{\gbox}{\square\hspace{-6.5pt}\raisebox{2pt}{\tiny{G}}\;}
\newcommand{\pbox}[1]{[#1]\,}
\newcommand{\pdiamond}[1]{<\hspace{-3pt}#1\hspace{-3pt}>\!}
%\newcommand{\lbox}{\square\,}
\newcommand{\lbox}{\Box}
\newcommand{\ldiamond}{\Diamond}
\newcommand{\pmodal}[2]{[#1]_G\,#2}
\newcommand{\Timpl}{\Rightarrow_T}
\newcommand{\Tconj}{\wedge}
\newcommand{\HTriple}[3]{\{#1\}~#2~\{#3\}}
\newcommand{\ContextHTriple}[4]{#1\rhd\HTriple{#2}{#3}{#4}}
\newcommand{\DummyCHT}[4]{\HTriple{#2}{#3}{#4}}
\newcommand{\sef}{\mathit{sef}}
\newcommand{\dsef}{\mathit{dsef}}

%% For polymorphism
\newcommand{\extInst}[1]{\mathrm{Ext}(#1)}
%\newcommand{\gextInst}[1]{\mathrm{gExt}(#1)}
\newcommand{\Poly}[1]{\mathrm{Poly}(#1)}
%% For institutions


\newcommand{\ModFunctor}{\Cat{Mod}\,}


\newcommand{\la}{\langle}
\newcommand{\ra}{\rangle}


\newcommand{\si}{\sigma}

\newcommand{\ISig}{\mathit{Sig}}
\newcommand{\IMod}{\mathit{Mod}}
\newcommand{\IAx}{\mathit{Ax}}

\newcounter{blubber}

\newenvironment{algenumerate}
{\begin{list}
  {\arabic{blubber}.}
  {\usecounter{blubber}
   \setlength{\leftmargin}{3ex}
    \setlength{\parsep}{0pt}
    \setlength{\itemindent}{1ex}
    \setlength{\itemsep}{2pt}   
    \setlength{\listparindent}{0ex}
  }
}
{\end{list}}

\newenvironment{specsem}%
        {\smallskip\par\noindent\qquad$\begin{array}{@{}l@{{}={}}l}}%
        {\end{array}$\par\noindent}


%% Width of parboxes for figures
\newlength{\myboxwidth}
\setlength{\myboxwidth}{\textwidth}
\addtolength{\myboxwidth}{-20pt}
\newenvironment{myfigure}{\begin{figure}\begin{center}
	\setlength{\fboxsep}{10pt}}% 
	{\end{center}\end{figure}}

%% Coalgebraic Modal Logic
\newcommand{\Lang}{\mathcal{L}}	
\newcommand{\FLang}{\mathcal{F}}	
\newcommand{\pls}{\Lambda}
\newcommand{\pl}[3]{#1\in #2(#3)}
\newcommand{\polypl}[3]{#1\in #2 #3}
\newcommand{\negpl}[3]{#1\notin #2(#3)}
\newcommand{\plbox}[1]{[#1]}
%\newcommand{\pldiamond}[1]{<\hspace{-3pt}#1\hspace{-3pt}>\!}
\newcommand{\pldiamond}[1]{\langle#1\rangle}
\newcommand{\gldiamond}[1]{\Diamond_{#1}}
\newcommand{\glbox}[1]{\square_{#1}}

\newcommand{\HMLBox}[1]{\square\hspace{-5.5pt}\raisebox{2pt}{$\scriptscriptstyle{#1}$}\;}
\newcommand{\HMLDiamondb}[1]{\Diamond\hspace{-5pt}\raisebox{1.5pt}{$\scriptscriptstyle{#1}$}\;}
\newcommand{\HMLDiamonda}[1]{\Diamond\hspace{-5.3pt}\raisebox{1.9pt}{$\scriptscriptstyle{#1}$}\;}
\newcommand{\pldbox}[2]{[#1]_{#2}}
\newcommand{\plempty}{\plbox{\emptyset}}
\newcommand{\plcan}{\square}
\newcommand{\FC}{{\mathfrak C}}
\newcommand{\negcl}[1]{\mathit{cl}(#1)}
\newcommand{\Nat}{{\mathbb{N}}}
\newcommand{\Int}{{\mathbb{Z}}}
\newcommand{\Rat}{{\mathbb{Q}}}
\newcommand{\Real}{{\mathbb{R}}}
\newcommand{\List}{\mathsf{list}}
\newcommand{\PDist}{D_\omega}%% Provisionary!!
%\newcommand{\Id}{\mathit{Id}}
\newcommand{\SFun}{\mathcal{SP}}
\newcommand{\plcomp}{\circledast}
\newcommand{\contrapower}{2^{\argument}}
\newcommand{\trans}[1]{#1^\flat}
\newcommand{\boolcl}[2]{\mathrm{bcl}_{#1}(#2)}
\newcommand{\Bag}{\mathcal{B}}
\newcommand{\Baginfty}{\mathcal{B}_\infty}
%\newcommand{\Ab}{\mathcal{B}_{\mathbb{Z}}}
\newcommand{\Prop}{\mathsf{Prop}}
\newcommand{\Up}{\mathsf{Up}}
\newcommand{\Lit}{\mathsf{Lit}}
\newcommand{\nneg}{\sim}
\newcommand{\satisfies}{\vDash}
\newcommand{\gsatisfies}{\satisfies_g}
\newcommand{\nsatisfies}{\nvDash}
\newcommand{\PSPACE}{\mathit{PSPACE}}
\newcommand{\Rules}{\mathcal{R}}
\newcommand{\RulesC}{\Rules_C}
\newcommand{\Frame}[1]{2^{2^{#1}}}
\newcommand{\UpP}{\mathsf{Up}\mathcal{P}}
\newcommand{\one}{\mathbb{1}}
%\newcommand{\smaller}[2]{#1_{<#2}}
\newcommand{\total}{\nu}
\newcommand{\sgn}{\mathit{sgn}}
%\newcommand{\RedClause}{\Clause^r}
\newcommand{\size}{\mathit{size}}
\newcommand{\arity}{\mathit{ar}}

\newcommand{\Sorts}{\mathcal{S}}
\newcommand{\MSorts}{\Sorts_0}
\newcommand{\ModOp}{L}
\newcommand{\contrapow}{\mathcal{Q}}
\newcommand{\profto}{\stackrel{\bullet}{\to}}
\newcommand{\Struct}{\mathcal{M}}
\newcommand{\Id}{\mathit{Id}}
\newcommand{\Det}{\mathsf{Det}}
\newcommand{\hDet}{\mathsf{hDet}}
\newcommand{\FF}{\mathfrak{F}}
\newcommand{\idOp}{\plbox{\iota}}
\newcommand{\Sig}{\mathit{Sig}}

\newcommand{\NEXP}{\mi{NEXPTIME}}
\newcommand{\EXP}{\mi{EXPTIME}}
\newcommand{\NP}{\mi{NP}}
\newcommand{\at}{\mi{at}}
\newcommand{\Max}{\mi{max}}
\newcommand{\muprod}{\textstyle\prod^\mu}
\newcommand{\tsum}{\textstyle\sum}
\DeclareMathOperator{\mge}{\ge}
\DeclareMathOperator{\meq}{=}
\DeclareMathOperator{\mle}{\le}
\DeclareMathOperator{\fixarrow}{\uparrow}
\newcommand{\Stable}{S}
\newcommand{\Zero}{Z}
\newcommand{\Regular}{U}
\newcommand{\last}{\lambda}
\newcommand{\fix}[2]{#1\!\fixarrow #2}
\newcommand{\msf}{\mathsf}

\newcommand{\CKCMi}{\CK\!+\!\CMi\xspace}
\newcommand{\CK}{\mathit{CK}}
\newcommand{\CMi}{\mathit{CMi}}
\newcommand{\Ax}{\mathcal{A}}

%\newcommand{\PLentails}{\entails_{\mi{PL}}}
%\newcommand{\ModSig}{\Lambda}

\newcommand{\modelsCA}{\models}
\newcommand{\Th}{\mathsf{Th}}
\newcommand{\rank}{\operatorname{rank}}
\newcommand{\Space}{\mathcal{S}}
\newcommand{\osder}[2]{\entails_{#1}^{#2}}
\newcommand{\gentails}[1]{\entails^{#1}_g}
