%%% 
%%% SIMBOLI E MACRO
%%% 

\newcommand*{\A}	{\mathbb{A}}
\newcommand*{\C}	{\mathbb{C}}
\newcommand*{\E}	{\mathbb{E}}
\newcommand*{\Ia}	{\mathbb{I}_{\A}}
\newcommand*{\Ic}	{\mathbb{I}_{\C}}
\newcommand*{\IdC}	{\mathit{Id}_{\C}}
\newcommand*{\IdIc}	{\mathit{Id}_{\mathbb{I}}}
\newcommand*{\PA}	{\mathbb{PA}}
\newcommand*{\PC}	{\mathbb{PC}}
\newcommand*{\atoms}	{\mathit{Atoms}}
\newcommand*{\clauseif}	{\ensuremath{\mathord{\leftarrow}}}
\newcommand*{\emptygoal}	{\boxempty}
\newcommand*{\emptyprog}	{\emptyset}
\newcommand*{\emptysub}	{\varepsilon}
\newcommand*{\equivC}	{\mathrel{\equiv_{\C}}}
\newcommand*{\goals}	{\mathit{Goals}}
\newcommand*{\tT}{\mathit{true}}	
\newcommand*{\vT}{\_}	
\newcommand*{\wfs}	{\mathit{WFS}}

\newcommand*{\I}[1][\alpha]	{\mathcal{I}_{#1}}
\newcommand*{\J}[1][\alpha]	{\mathcal{K}_{#1}}
\newcommand*{\Pu}[1][\alpha]	{\mathoper{pu}_{#1}}
\newcommand*{\Su}[1][\alpha]	{\mathoper{su}_{#1}}
\newcommand*{\Trans}[1][\alpha]	{\mathrel{\mathop{\longmapsto}\limits_{P}^{#1}}}
\newcommand*{\Tsym}[1][\alpha]	{\mathscr{T}_{#1}}
\newcommand*{\Unf}[1][P]	{\mathoper{unf}_{#1, \alpha}}
\newcommand*{\equivA}[1][]	{\mathrel{\equiv_{\A#1}}}

\newcommand*{\Atom}[2][\alpha]	{\mathop{\mathscr{A}_{#1}}\llbracket#2\rrbracket}
\newcommand*{\Beha}[2][\alpha]	{\mathop{\mathscr{B}_{#1}}\llbracket#2\rrbracket}
\newcommand*{\ClauseT}[1]	{\widetilde{\mathscr{C}}\llbracket#1\rrbracket}
\newcommand*{\Clause}[2][\alpha]	{\mathop{\mathscr{C}_{#1}}\llbracket#2\rrbracket}
\newcommand*{\Eqns}[1]	{\mathoper{eqn}(#1)}%\mathop{\mathscr{E}}
\newcommand*{\FIv}[2][\alpha]	{\mathop{\mathscr{F}_{#1}^{\I}}\llbracket#2\rrbracket}
\newcommand*{\F}[2][\alpha]	{\mathop{\mathscr{F}_{#1} \llbracket#2\rrbracket}}
\newcommand*{\Goal}[2][\alpha]	{\mathop{\mathscr{G}_{#1}}\llbracket#2\rrbracket}
\newcommand*{\Op}[2][\alpha]	{\mathop{\mathscr{O}_{#1}}\llbracket#2\rrbracket}
\newcommand*{\Orac}[2][\alpha]	{\mathop{\mathscr{OS}_{#1}}\llbracket#2\rrbracket}
\newcommand*{\ProgIv}[2][\alpha]	{\mathop{\mathscr{P}}\nolimits_{#1}^{\I}\llbracket#2\rrbracket}
\newcommand*{\Prog}[2][\alpha]	{\mathop{\mathscr{P}_{#1}}\llbracket#2\rrbracket}
\newcommand*{\Query}[2][\alpha]	{\mathop{\mathscr{Q}_{#1}}\llbracket#2\rrbracket}
\newcommand*{\Sem}[2][\alpha]	{\mathop{\mathscr{S}_{#1}}\llbracket#2\rrbracket}
\newcommand*{\assoc}[2]	{{\left[\left.{}^{#2}\!\right/\mbox{}\!\!{}_{#1}\right]}}
\newcommand*{\bra}[1]	{\llbracket#1\rrbracket}
\newcommand*{\clause}[2]	{#1\mathbin{\clauseif}#2}%\allowbreak
\newcommand*{\close}[2][\alpha]	{[{#2}]^{*}_{#1}}
\newcommand*{\cpo}[2]	{{(#1, \, \mathord{#2})}}
\newcommand*{\derivEQ}[2][\alpha-]	{\xrightarrow[{#2}]{#1\mathrm{eq}}}
\newcommand*{\derivSLD}[2]	{\xrightarrow[{#2}]{#1}}
\newcommand*{\eT}[3]	{\langle#2\rangle^{#1}_{#3}}
\newcommand*{\equivVar}[1]	{\mathrel{\equiv_{#1}}}%\E,
\newcommand*{\initcoll}[1]	{\phi_{#1}} %{\mathoper{\mathit{coll}}(#1)}
\newcommand*{\ordinal}[2]	{\mathop{{#1} \mathord{\uparrow}{\scriptstyle #2}}} 
\newcommand*{\pT}[2]	{#1 \mathop{\vdash} #2}	
\newcommand*{\pair}[2]	{{\langle #1, \, #2\rangle}}
\newcommand*{\quer}[2]	{#1 \mathbin{\mathit{in}} #2}
\newcommand*{\resultant}[2]	{{#1\mathbin{\clauseif}#2}}%\allowbreak
\newcommand*{\seq}[2][n]	{{#2_{1}, \allowbreak \ldots, \allowbreak #2_{#1}}}
\newcommand*{\single}[2]	{#1 \mapsto #2}

\newcommand*{\eg}	{e.g.,}
\newcommand*{\etc}	{\emph{etc}}
\newcommand*{\ie}	{i.e.,}
\newcommand*{\st}	{s.t.}
\newcommand*{\wrt}	{w.r.t.}

\newenvironment{bycases}{\left\{\def\arraystretch{1.2}\array{@{}l@{\,}l@{}}}{\endarray\right.}
\renewcommand*{\Join}	{\triangleright}%\rightslice
\renewcommand*{\wr}	{\lightning}%\mathord{}
