source: LTS/DICE2014/unimacro.tex @ 3498

\def\Env{\mathbb Env}

\newcommand{\derl}{\vdash^{\ell}_{\nabla}}
\newcommand{\ders}{\vdash^{*}_{\nabla}}
\newcommand{\piv}{\nu_{_{\!\nabla}}}
\newcommand\COMMENT[1]{}
\newcommand{\der}{\vdash_{\nabla}}
\newcommand{\SE}{\mathcal{S}}


\def\eqclass#1{{\pmb [} #1 {\pmb ]}_{^{\stackrel{\nabla}{\simeq}}}}
\def\tuple#1{\langle #1 \rangle}
%\def\cl#1{\mbox{cl}(#1)}
%\def\clf#1{\mbox{cl}_{fin}(#1)}
%\def\eval{\mbox{eval}}
\def\C{\mathbb{C}}
\def\lift{\jmath}


\def\Coh{\mathcal{C}oh}
%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\x}{{\tt x}}
\newcommand{\y}{{\tt y}}
\newcommand{\z}{{\tt z}}
\newcommand{\M}{{\tt M}}
\newcommand{\N}{{\tt N}}
\newcommand{\toc}{{\tt p}}
\newcommand{\compatto}{{\tt d}}
\def\rank{\mbox{\sc rank}}
%Simboli per spazi coerenti
%\def\frownsmile{%
%\mathrel{\vbox{\hbox{${\frown}$}\vspace{-2ex}\hbox{${\smile}$}\vspace{-.3ex}}}}
%\def\smilefrown{%
%\mathrel{\vbox{\hbox{${\smile}$}\vspace{-2ex}\hbox{${\frown}$}\vspace{-.5ex}}}}
%\def\smilefrown{\asymp}
\newcommand{\Pbot}{{\pmb{\pmb \perp}}}
\newcommand{\Ptop}{{\pmb{\pmb \top}}}
\newcommand{\coer}{ \frownsmile}
%\newcommand{\clique}{\sqsubseteq}
\newcommand{\Cl}{\mathcal{C}l}
\newcommand{\tr}{\hbox{$\mathcal{T}$\hspace{-1mm}\hbox{$r$}}}
\newcommand{\stapprox}{\sqsubseteq_{S}}
\newcommand{\extapprox}{\sqsubseteq_{E}}
\def\subfin{\subseteq_{fin}}
\newcommand \bibar[1]{\lceil{#1}\rfloor}
\newcommand \Bibar[1]{\left\lceil{#1}\right\rfloor}
\newcommand{\fix}{{\tt fix}}

%---------------------------------------------------------
%      ENVIRONMENTS
%---------------------------------------------------------
 \newtheorem{notation}{Notation}[section]
%\newtheorem{example}[notation]{Example}
% \newtheorem{remark}[notation]{Remark}
%   \newtheorem{theorem}[notation]{Theorem}
%    \newtheorem{corollary}[notation]{Corollary}
%     \newtheorem{proposition}[notation]{Proposition}
%      \newtheorem{lemma}[notation]{Lemma}
%       \newtheorem{definition}[notation]{Definition}
%       \newtheorem{property}[notation]{Property}
%          \newtheorem{exercise}[notation]{Exercise}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%5
\def\Vin{{ \Delta}}
\def \Gomega {{\pmb\surd\Omega}}
\def \Gxp {{\pmb\surd}}

\def \Lomega {{\pmb\angle\Omega}}
\def \Lxp {{\pmb\angle}}

\def \LVcbn {\rightarrow_{\Lambda\ell}}
\def \LVcbns {\rightarrow^*_{\Lambda\ell}}
\def \LVcbv {\rightarrow_{\Gamma\ell}}
\def \LVcbvs {\rightarrow^*_{\Gamma\ell}}

\def \can {\rightarrow_{\Xi\ell}}
\def \cans {\rightarrow^*_{\Xi\ell}}
\def \Xell {\Xi\ell}

\newcommand\kcan[1]{\stackrel{\hspace{-3mm}#1}{\can}}

\def\evr{\mathcal{E}}
\def\Uio{{\mathcal{U}^\Vin_\Vout}}

\def\UHio{{\mathcal{U}^\Lambda_{\Lambda\mbox{\tiny-HNF}}}}


\def\LLb{L_0}
\def\LLe{L_1}
\def\VVb{V_0}
\def\VVe{V_1}

%\newcommand{\restri}[1]{\hspace{-1,3mm}\upharpoonright_{\rm\!#1}\!}

%%%%%%%%%%%    SISTEMI NUMERICI
\newcommand{\Zero}{\mbox{\sffamily Zero}}
\newcommand{\Succ}{\mbox{\sffamily Succ}}
\newcommand{\Test}{\mbox{\sffamily Test}}
\newcommand{\Pred}{\mbox{\sffamily Pred}}
\newcommand{\T}{\mbox{\sffamily T}}
\newcommand{\F}{\mbox{\sffamily F}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% Ex LUMACRO.tex Precede
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\FV{\mathrm{FV}}
\def\nfset{\mbox{-NF}}
\def\Var{\mathrm{Var}}

\newcommand \dstrategy[1]{\,
            \makebox[0mm]{\raisebox{2,83mm}{$\hspace{5mm}_{#1}$}}
                          \raisebox{-0.39mm}{$\hookrightarrow$}}
\newcommand \ndstrategy[1]{\,
            \makebox[0mm]{\raisebox{2,5mm}{$\hspace{3mm}_{#1}$}}
                          \raisebox{-0.35mm}{$\Rightarrow$}}

\def\Bnf{\mathsf{nf_{\!\Lambda}}}
\def\BOnf{\mathsf{nf_{\!\Lambda \Omega}}}
\def\args{\mathsf{args}}


%\renewcommand\vec[1]{\overrightarrow{#1}}
%\renewcommand\vec[1]{\overrightarrow{#1\;}}
\newcommand\repre[1]{\ulcorner #1 \urcorner}
\def \Vred {\rightarrow_{\Vin}}
\def \Vequ {=_{\Vin}}
\def \Vpar {\Rightarrow_{\Vin}}
\def \Wred {\leadsto_{\Vin}}
\def \Wequ {=_{\Vin}}
\def \Vdst {\hookrightarrow_{\Vin}}
%\def \can {\rightarrow_{\Xi}}
%\def \cans {\rightarrow^*_{\Xi}}
\def  \canequ {=_\Xi}
\def \Vsolv {\searrow}
\def \V {{\bf V}}
\def \NF {{\bf N }}
\def \L {{\bf L}}
\def \O {{\bf O}}
\def \H {{\bf H}}
\def \e {{\O\eta}}
\def\erre{{\scriptsize\textcircled{r}}}
\def\pipi{{\scriptsize\textcircled{\tiny P}}}

%Warning: gli spazi sono sgnificativi nelle definizioni seguenti
\def\SubTerm{\mbox{\sffamily SubTerm}}
%\def\len{\mathsf len}
\def\Val{\mathsf{Val} }
\def\Vin{{ \Delta}}
\def\Win{{\widetilde{{\mathsf V}}}}
\def\Vout{{\Theta}}
\def\lambdastar{\lambda^{\!\star}\!}

\def \Vcbn {\rightarrow_{\Lambda}}
\def \Vcbns {\rightarrow^*_{\Lambda}}
\def \Vcbv {\rightarrow_{\Gamma}}
\def \Vcbvs {\rightarrow^*_{\Gamma}}
\def\exe{\rightarrow^p_\Vin}
\def\con{\Downarrow_{\Vin, \Vout}}
\def \lom {\rightarrow_{\Lambda\Omega}}
\def \leta {\rightarrow_{\eta\Omega}}
\def \reta {\rightarrow_{\eta}}


% Semantica operazionale
\newcommand{\op}{\Downarrow_{{\bf O}}}
\newcommand{\h}{\Downarrow_{{\bf H}}}
\newcommand{\nf}{\Downarrow_{{\bf N}}}
\newcommand{\opi}{\Downarrow_{{\bf I}}}
\newcommand{\lazy}{\Downarrow_{{\bf L}}}
\newcommand{\secd}{\Downarrow_{{\bf V}}}
\newcommand{\inner}{\Downarrow_I}
\newcommand{\ahead}{\Downarrow_A}
\newcommand{\vu}{\rightarrow_v}
\newcommand{\vv}{\rightarrow^*_v}
\newcommand{\vstar}{\rightarrow_v^*}
\newcommand{\vleft}{\rightarrow_l}
\newcommand{\vbp}{\Rightarrow_v}

% Sistemi numerici
%\newcommand{\Zero}{{\bf Zero}}
%\newcommand{\Succ}{{\bf Succ}}
%\newcommand{\Test}{{\bf Test}}
%\newcommand{\Pred}{{\bf Pred}}
%\newcommand{\T}{{\bf T}}
%\newcommand{\F}{{\bf F}}


% 'Settaggi' globali

% proof  e' un ambiente per dimostrazioni. Fa si' che il testo di
%        una dimostrazione sia preceduto dalla parola "Proof.",
%        scritta in corsivo, e che sia seguito dal quadratino di
%        fine dimostrazione, allineato a destra.
%        Va tenuto presente che il quadratino di fine dimostrazione
%        potrebbe comparire, da solo, nella pagina che segue la
%        dimostrazione, oppure allineato a sinistra, a seconda se,
%        rispettivamente, la dimostrazione termini a fine pagina o
%        con una riga larga come tutta la pagina.

%\renewenvironment{proof}{\begin{proof}}{\hfill $\box$ \end{proof}}
%\renewenvironment{proof}{{\it Proof.} }{\hspace*{\fill}$\Box$\medskip}
%\renewenvironment{proof}{{\it Proof.} }{\hfill $\Box$\vspace{\baselineskip}}
%\newenvironment{proof}{\noindent {\em Proof.} }{\hfill $\Box$
%\vspace{\baselineskip}}
\def\proof{\par\addvspace{5pt}\trivlist\item[\hskip\labelsep{\it Proof.}]}
%\def\endproof{\unskip\nobreak\hspace*{\fill}$\Box$\endtrivlist}
\def\endproof{{%        set up{
    \parfillskip=0pt
    \widowpenalty=10000     % so we dont break the page before \square
   \displaywidowpenalty=10000  % ditto
   \finalhyphendemerits=0  % TeXbook exercise 14.32
  %
  %                 horizontal
   \leavevmode             % \nobreak means lines not pages
   \unskip\nobreak                 % remove previous space or glue
   \hspace*{\fill}
   $\Box$%              % the end-of-proof mark
  %                   vertical \looseness=-1
  }\endtrivlist}

%\newenvironment{prova}[2]{\vspace{\baselineskip}\noindent {\bf\em #1} ({\it #2})\\ }{\hspace*{\fill}$\blacktriangle$\medskip}
\newenvironment{subProof}[2]
{\vspace{\baselineskip}\noindent $\blacktriangledown\vspace{1mm}$ {\bf #1} ({#2}).\par\noindent}
{\hspace*{\fill}$\blacksquare$\medskip}




%denotational sematics
%
\newcommand{\dpap}{\llbracket}%{[\![}
\newcommand{\dpch}{\rrbracket}%{]\!]}

%den e' la funzione di interpretazione semantica
\newcommand{\den}[1]{\dpap {#1} \dpch}

%dene e' la funzione di interpretazione semantica in un environment
\newcommand{\dene}[2]{\dpap {#1} \dpch _{#2}}

%denm e' la funzione di interpretazione semantica
% in un modello
\newcommand{\denm}[2]{\dpap {#1} \dpch^{\cal {#2}}}

%denem e' la funzione di interpretazione semantica
% in un modello e un environment
\newcommand{\denem}[3]{\dpap {#1} \dpch^{\cal {#2}}_{#3}}

%dm e' l'uguaglianza denotazionale in un dato modello
\newcommand{\dm}[1]{\sim_{\cal {#1}}}

\def \dom {{\mathbb D}}
\def \dvin {{\mathbb I}}

%relazione d'ordine per il modello LL
\newcommand{\sLL}{\trianglelefteq}
\newcommand{\eqsLL}{\triangleq}

\newcommand{\cl}[1]{\sqsubseteq_{\mathbb {#1}}}

%costruttore di domini
\def \con {{\bold c}}

% uno e' il termine \lambda x y.x y.
%\newcommand{\uno}{\mbox{$1\!\!\!$}\raisebox{.28ex}{$1$}}
\newcommand{\uno}{\mbox{$1\!\!1$}}
% metalambda, eset e linimpl sono rispett. il metalambda,l'insieme
%vuoto e l'implicazione lineare.
%
%\newcommand{\metalambda}{\mbox{$\lambda\!\!\!$}\raisebox{.28ex}{$\lambda$}}
\newcommand{\metalambda}{\mbox{$\lambda\hspace{-1,58mm}\lambda$}}
%\newcommand{\metalambda}{\mathbb{\bblambda}}
\newcommand{\metax}[2]{\metalambda {#1}\!:\! {#2} \pmb.\,}
\newcommand{\eset}{\emptyset}
\newcommand{\linimpl}{\mathrel{-\!\circ}}

\newcommand{\seq}[3]{#1_{#2} , \!\ldots\! , #1_{#3}}

% seqT serve per scrivere sequenze di variabili tipate indicizzate.
%        E' come 'seq', ma ha quattro parametri dei quali il secondo
%        denota il tipo (che variera' sugli stessi indici).
%
\newcommand{\seqT}[4]{#1_{#3}\!:\!#2_{#3},\!\ldots\!,#1_{#4}\!:\!#2_{#4}}

% seqL e seqTL sono come 'seq' e 'seqT', ma senza le virgole. Sono utili
%        per le lambda-astrazioni.
%
\newcommand{\seqL}[3]{#1_{#2}\!\ldots\!#1_{#3}}
\newcommand{\seqTL}[4]{#1_{#3}\!:\!#2_{#3}\!\ldots\!#1_{#4}\!:\!#2_{#4}}

% Di seguito sono definiti vari tipi di spazi. Quelli orizzontali sono
%        utili in modalita' matematica per distanziare una formula
%        dall'altra (ad es. una premessa dall'altra in una regola).
%        Quelli verticali distanziano una riga dalla successiva. Sono
%        utili ad esempio per separare una regola dalla successiva.
%
\newcommand{\xspace}{ \makebox[1em]{} }
\newcommand{\xspaceD}{ \makebox[2em]{} }
\newcommand{\xspaceT}{ \makebox[3em]{} }
\newcommand{\xspaceQ}{ \makebox[4em]{} }
\newcommand{\xspaceC}{ \makebox[5em]{} }
\newcommand{\xspaceMezzo}{ \makebox[0.5em]{} }



\def\leqmodel{\setbox0=\hbox{$\sqsubset$}%\,\hbox
{\raise.2em\copy0\kern-\wd0\kern0.05em\raise-0.3em\hbox
{{\small$\sim$}}}\,}

%-------------------------------------------------------------------
% MACROS FOR MAKE RULES OF SYSTEM
%-------------------------------------------------------------------
%\newcommand \UN[3] {\prooftree #3 \justifies #2 \using \scriptstyle #1 \endprooftree}
%\infer[\scriptsize\mbox{\bf (z)}]{\tt \Gamma \vdash {\bf 0}
%  \triangle \_}{}
%\newcommand\cal[1]{\mathcal{#1}}

\newcommand \UN[3]{\infer[\scriptsize #1]{#2}{#3}}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "LogicalModel"
%%% End: