%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% general commands
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% TEXT ORGANIZATION
%
\newcommand{\commen}[1]{}
\newcommand{\comment}[1]{}
\newcommand{\comentari}[1]{}
\newcommand{\tutorial}[1]{}
%
% hyperTEXT ORGANIZATION
%
\newcommand{\refin}[2]{#1 #2} % APUNTS: 1er nivell de refinament
\newcommand{\refindos}[1]{#1} % APUNTS: 2on nivell de refinament
\newcommand{\refintres}[1]{#1} % APUNTS: 3er nivell de refinament
\newcommand{\profe}[1]{#1} % APUNTS: notes al profe
%
% FIGURES
%
\newcommand{\extfigure}[3] % posa un dibuix com a figura
  {\begin{figure}[htbp]
    \centerline{#3}
    \caption{#2}
    \label{#1}
    \end{figure}}
%
\newcommand{\dibuix}[3] % crea una dibuix a partir d'un dibuix extern
{\vbox to #2
  {\hrule width #1 height 0pt depth 0pt
   \vfill
   \special{picture #3}}}
%
\newcommand{\cdibuix}[3] % crea una dibuix centrat a partir d'un dibuix extern
{\vfill\centerline{\dibuix{#1}{#2}{#3}}\vfill}
%
\newcommand{\cfigu}[3]{\begin{center}\mbox{\psfig{figure=#1,height=#2,rheight=#3}}\end{center}}
%
\newcommand{\tapproach}[5]
{\begin{tabular}{c}
\hline\\
#1\\
\hline\hline
\begin{tabular}{|l|l|}
\hline
Temporal Entity         & #2 \\
Basic relations         & #3 \\
Relations set           & #4 \\
Tasks/results           & #5 \\
\hline
\end{tabular}
\end{tabular}
}
%
\newcommand{\ra}[3]{\stackrel{#1}{\rule[#2]{#3}{1mm}}}
%
% TRANSPAS
%
\newcommand{\subtitol}[1]{\centerline{\large\bf #1}}
\newcommand{\subsubtitol}[1]{\centerline{\fbox{\bf #1}}}
\newcommand{\paratitol}[1]{\fbox{\bf #1}}
%
%%% SYNTAX
%
%\newcommand{\cod}[1]
%{\begin{center}\framebox{\vbox{
%\begin{tabbing}
%\hspace{.5cm}\=\hspace{.5cm}\=\hspace{.5cm}\=\hspace{.5cm}\=\hspace{.5cm}\=
%\hspace{-2.5cm}#1
%\end{tabbing}}}
%\end{center}}
%
\newcommand{\cod}[1]
{\begin{tabbing}
\hspace{.5cm}\=\hspace{.5cm}\=\hspace{.5cm}\=\hspace{.5cm}\=\hspace{.5cm}\=
\hspace{.5cm}\=\hspace{.5cm}\=\hspace{.5cm}\=\hspace{.5cm}\=\hspace{.5cm}\=
\hspace{.5cm}\=\hspace{.5cm}\=\hspace{.5cm}\=\hspace{.5cm}\kill
#1
\end{tabbing}}
%
\newcommand{\codflex}[1]
{\begin{tabbing}
\hspace{.5cm}\=\hspace{.5cm}\=\hspace{.5cm}\=\hspace{.5cm}\=\hspace{.5cm}\=
\hspace{.5cm}\=\hspace{.5cm}\=\hspace{.5cm}\=\hspace{.5cm}\=\hspace{.5cm}\=
\hspace{.5cm}\=\hspace{.5cm}\=\hspace{.5cm}\=\hspace{.5cm}\kill
#1
\end{tabbing}
}
%
\newcommand{\algorisme}[1] % per escriure pseudo-codi
{\centerline{\vbox{\begin{tabbing}
xxxx\=xxxx\=xxxx\=xxxx\=xxxx\=xxxx\= \kill #1 \end{tabbing}}}}
%
\newcommand{\indexat}[2]{\settowidth{\unitlength}{$#1$}
       #1\kern-\unitlength\raise -.6em\hbox to \unitlength{\hss$\scriptscriptstyle #2$\hss}\kern.3em}
%
% Latex legal reasoning rule syntax
% #1 body of the rule
% #2 head of the rule
%
\newcommand{\rul}[2]{\mbox{\ }\\{\tt
\begin{tabular}{ll}
If& 
\begin{tabular}[t]{l}
#1
\end{tabular} \\
then & 
\begin{tabular}[t]{l}
#2\\
\mbox{\ }\\
\end{tabular}
\end{tabular}
}}
%
\newcommand{\facts}[1]{\mbox{\ }\\{\tt
\mbox{}\noindent\begin{tabular}[t]{l}
#1\\
\mbox{}\\
\end{tabular}
}}
%
\newcommand{\syndef}[1]{\mbox{\ }\\{\it
\mbox{}\noindent\begin{tabular}[t]{lrl}
#1\\\
\mbox{}
\end{tabular}
}}
%
\newcommand{\signature}[1]{\mbox{\ }\\{\it
\mbox{}\noindent\begin{tabular}[t]{lll}
#1\\
\end{tabular}\\
}}
%
%%% SEMANTICS
%
\newcommand{\lmark}{{[}{[}}
\newcommand{\rmark}{{]}{]}}
\newcommand{\lsem}{[\kern -.13 em [}
\newcommand{\rsem}{]\kern -.13 em ]}
\newcommand{\sem}[1]{\lsem #1 \rsem}
\newcommand{\pmodels}{\vert\hspace{-.17cm}\approx}
%
%%% LEXIC
%
% general
%
\newcommand{\ratn}{{\mathbb{Q}}}
%\newcommand{\ratn}{{\cal{Q}}}
%
\newcommand{\conn}[1]{\mbox\bf {#1}}
\newcommand{\pred}[1]{\mbox\sc {#1}}
\newcommand{\dpred}[1]{\mbox\em {#1}}
\newcommand{\ub}[1]{{\bf #1}}
\newcommand{\ul}[1]{\underline{#1}}
\newcommand{\uub}[1]{{\bf \underline{#1}}}
\newcommand{\ubpo}{{\bf (}}
\newcommand{\ubpc}{{\bf )}}
\newcommand{\eqd}{\stackrel{def}{=}}
%
% abbreviations for BNF specifications
%
\newcommand{\tvert}{{$\vert$\ }}
%
% abbreviations for MILORD
%
\newcommand{\mi}{{\em Mi\-lord}}  %Milord
\newcommand{\mill}{{\em Mi\-lord~II}} %Milord II
\newcommand{\tmill}{{\em Time\-lord}}  % temporal Milord II
%
% abbreviations for temporal constraint models
%
\newcommand{\timestruc}{{\em time-structure}}
\newcommand{\btr}{{\mbox{\bf BTR}}}
\newcommand{\BTR}{{\mbox{\bf BTR}}}
%\newcommand{\tpm}{TCSP({\bf M})}
%\newcommand{\tpq}{$TCSP_{\bf PA}$}
%\newcommand{\tiq}{{\em TCSP$(I_{\cal Q})$}}
%\newcommand{\tpmiq}{{\em TCSP$(p_{\cal M},I_{\cal Q})$}}
%\newcommand{\tpmdm}{{\em TCSP$(p_{\cal M},D_{\cal M})$}}
\newcommand{\tpm}{{\em TCSP$(p_{\cal M})$}}
\newcommand{\tpq}{{\em TCSP$(p_{\cal Q})$}}
\newcommand{\tiq}{{\em TCSP$(I_{\cal Q})$}}
\newcommand{\tpmiq}{{\em TCSP$(p_{\cal M},I_{\cal Q})$}}
\newcommand{\tpmdm}{{\em TCSP$(p_{\cal M},D_{\cal M})$}}
\newcommand{\bpa}{{\bf BPA}}
\newcommand{\cpa}{{\bf CPA}}
\newcommand{\pa}{{\bf PA}}
\newcommand{\bia}{{\bf BIA}}
\newcommand{\ipa}{{\bf IPA}}
\newcommand{\pia}{{\bf PIA}}
\newcommand{\ia}{{\bf IA}}
\newcommand{\BPA}{{\bf BPA}}
\newcommand{\CPA}{{\bf CPA}}
\newcommand{\PA}{{\bf PA}}
\newcommand{\BIA}{{\bf BIA}}
\newcommand{\IPA}{{\bf IPA}}
\newcommand{\PIA}{{\bf PIA}}
\newcommand{\IA}{{\bf IA}}
\newcommand{\ixtet}{{\em IxTeT}}
\newcommand{\timegraph}{{\em TimeGraph}}
\newcommand{\timegraphii}{{\em TimeGraph II}}
%
% abbreviations for temporal languages
%
\newcommand{\sttc}{{\em Simple TTC}}
\newcommand{\ttc}{{\em TTC}}
\newcommand{\datalog}{$Datalog$}
\newcommand{\datalogns}{$Datalog_{ns}$}
\newcommand{\datalogs}{$Datalog_{1s}$}
\newcommand{\mds}{$Monadic\ Datalog_{1s}$}
\newcommand{\templog}{{\em Templog}}
\newcommand{\clp}{{\em CLP}}
\newcommand{\CLP}{{\em CLP}}
% \newcommand{\tclp}{{\em CLP}$({\cal T})$}
\newcommand{\tclp}{{\em TCLP}}
\newcommand{\clpl}{{\em Constraint Logic Programming}}
\newcommand{\tclpl}{{\em Temporal Constraint Logic Programming}}
\newcommand{\dt}{${\cal D_{\cal TIME}}$}
\newcommand{\ddt}{${D_{\cal TIME}}$}
\newcommand{\iit}{${\cal I_{\cal TIME}}$}
\newcommand{\lt}{${\cal L_{\cal TIME}}$}
\renewcommand{\time}{{\cal TIME}}
\newcommand{\ERIR}{\mbox{\em ERIR}}
\newcommand{\PCIR}{\mbox{\em PCIR}}
\newcommand{\JIR}{\mbox{\em JIR}}
\newcommand{\DJIR}{\mbox{\em DJIR}}
\newcommand{\LTR}{{\rm LTR}}
\newcommand{\ltr}{{\bf LTR}}
%
% tclp elements
%
\newcommand{\mr}{{\em mr}}
%\newcommand{\index}{\mbox{\em index}}
\newcommand{\path}{\mbox{\em path}}
\newcommand{\pathij}{{\em path_{ij}}}
%
% names of theories
%
%\renewcommand{\ar}{${\bf AR}$}
\newcommand{\allen}{${\cal A}$}
\newcommand{\allenbis}{${\cal A'}$}
\newcommand{\ah}{${\cal AH}$}
\newcommand{\galton}{${\cal G}$}
\newcommand{\g}{${\cal G}$}
\newcommand{\e}{${\cal E}$}
\newcommand{\ip}{${\cal IP}$}
\newcommand{\ipd}{${\cal IP_{\mbox{\small\it dense}}}$}
\newcommand{\cd}{${\cal CD}$}
\newcommand{\cdm}{${\cal CD_{\mbox{\small\it max}}}$}
%
% formal elements
%
\newtheorem{theorem}{Theorem}
\newtheorem{teorema}{Teorema}
\newtheorem{proposition}{Proposition}
\newtheorem{definition}{Definition}
\newtheorem{definicio}{Definici\'o}
\newtheorem{lemma}{Lemma}
\newtheorem{cor}{Corollary}
\newtheorem{corollary}{Corollary}
\newtheorem{example}{Example}
\newtheorem{ejemplo}{Ejemplo}
\newtheorem{exemple}{Exemple}
%\newtheorem{ex}{Example}
\newenvironment{proof}{\trivlist\item[\hskip\labelsep{\it Proof:\/}]\ignorespaces}{\hfill$\Box$\endtrivlist}
\newenvironment{sketch}{\trivlist\item[\hskip\labelsep{\it Sketch:\/}]\ignorespaces}{\hfill$\Box$\endtrivlist}
\newtheorem{remark}{Remark}
\newtheorem{claim}{Claim}
\newtheorem{conjecture}{Conjecture}
\newtheorem{obs}{Observation}
\newtheorem{fact}{Fact}
\newtheorem{exercici}{Exercici}
\newtheorem{exerciciresolt}{Exercici Resolt}
%\newtheorem{solucio}{Soluci\'o}

\newcommand{\recordatori}[1]
   {\begin{center}
{\footnotesize\fbox{
\begin{minipage}[t]{0.9\textwidth}{\bf{Recordatori de Teoria}: } 
#1
\end{minipage}}}\end{center}
\vspace{0.1in}}

\newenvironment{solucio}
   {\ \newline\ {\bf Soluci\'o}.}%
   {{\bf Fi soluci\'o.}}
%{\mbox{\ }\\}
%\noindent\rule{\textwidth}{0.01in}\vspace{0.01cm}}

%\newenvironment{recordatori}
%   {\vspace{0.1in}{\bf Recorda que ... }\newline\vspace{-0.1in}
%\begin{center}\begin{minipage}[t]{0.9\textwidth}\rule{\textwidth}{0.01in}\\ 
%\footnotesize}%
%{\vspace{0.1in}\mbox{}\newline\rule{\textwidth}{0.01in}\end{minipage}
%\end{center}}
%
% logical connectives
%
\newcommand{\ssi}{\mbox{\bf\ iff\ }}
\newcommand{\aand}{\mbox{\bf\ and\ }}
\newcommand{\oor}{\mbox{\bf\ or\ }}
\newcommand{\conj}{\: \wedge \:}
\newcommand{\disj}{\: \vee \:}
%\newcommand{\implies}{\: \rightarrow \:}
\newcommand{\iiff}{\: \leftrightarrow \:}
%\newcommand{\iff}{\: \leftrightarrow \:}
%\newcommand{\iff}{\: \leftrightarrow \:}
\newcommand{\existsn}{\tilde{\exists}}
\newcommand{\foralln}{\tilde{\forall}}
%
% logical meta-language
%
\newcommand{\mapeig}{\: \mapsto \:}
%
% Qualitative Temporal relations
%
\newcommand{\ibegin}{begin}
\newcommand{\iend}{end}
\newcommand{\meetpoint}{\mbox{\tt meetpoint}}
%
% TEMPORAL FUNCTIONS
%
\newcommand{\concat}{\mbox{\tt concat}}
\newcommand{\tjoin}{\mbox{\tt join}}
\newcommand{\join}{\mbox{\tt join}}
\newcommand{\mymin}{\mbox{\tt min}}
\newcommand{\mymax}{\mbox{\tt max}}
%
% QUALITATIVE TEMPORAL RELATIONS
%
% instant
%
\newcommand{\moment}{\mbox{\sc Moment}}
%\renewcommand{\next}{\mbox{\tt Next}}
\newcommand{\Next}{\mbox{\tt Next}}
%

% instant-period
%
\newcommand{\within}{\mbox{\tt Within}}
\newcommand{\WITHIN}{\mbox{\tt Within}}
\newcommand{\mylimits}{\mbox{\tt Limits}}
\newcommand{\MYLIMITS}{\mbox{\tt Limits}}
\newcommand{\LIMITS}{\mbox{\tt Limits}}
\newcommand{\previous}{\mbox{\tt Previous}}

\newcommand{\myimmediate}{\mbox{\tt Immediate}}
\newcommand{\later}{\mbox{\tt Later}}
%
\newcommand{\ipprecedes}{\mbox{\tt .precedes.}}
\newcommand{\ipstarts}{\mbox{\tt .starts.}}
\newcommand{\ipduring}{\mbox{\tt .during.}}
\newcommand{\ipfinishes}{\mbox{\tt .finishes.}}
\newcommand{\ipafter}{\mbox{\tt .after.}}
%
% period
%
\newcommand{\IN}{\mbox{\tt In}}
\newcommand{\myin}{\mbox{\tt In}}
\newcommand{\disjoint}{\mbox{\tt Disjoint}}
\newcommand{\disjointd}{\mbox{\tt Disjoint$^{\neg\hspace{-0.6mm}\_}_{on}$}}
\newcommand{\disjointc}{\mbox{\tt Disjoint$^{^\sim}_{on}$}}
\newcommand{\before}{\mbox{\tt Before}}
\newcommand{\after}{\mbox{\tt After}}
\newcommand{\meets}{\mbox{\tt Meets}}
\newcommand{\MEETS}{\mbox{\tt Meets}}
\newcommand{\metby}{\mbox{\tt Met\_by}}
\newcommand{\overlaps}{\mbox{\tt Overlaps}}
\newcommand{\overlappedby}{\mbox{\tt Overlapped\_by}}
\newcommand{\starts}{\mbox{\tt Starts}}
\newcommand{\start}{\mbox{\tt Start}}
\newcommand{\startedby}{\mbox{\tt Started\_by}}
\newcommand{\during}{\mbox{\tt During}}
\newcommand{\contains}{\mbox{\tt Contains}}
\newcommand{\finishes}{\mbox{\tt Finishes}}
\newcommand{\finishedby}{\mbox{\tt Finished\_by}}
\newcommand{\iequal}{\mbox{\tt Equal}}
\newcommand{\equal}{\mbox{\tt Equal}}
\newcommand{\touch}{\mbox{\tt Touch}}
\newcommand{\share}{\mbox{\tt Share}}
%
% METRIC TEMPORAL RELATIONS
%
\newcommand{\du}{${\cal DU}$}
\newcommand{\fdu}{${\cal FDU}$}
\newcommand{\lfdu}{${\cal L}_{\cal FDU}$}
\newcommand{\DU}{${\cal DU}$}
\newcommand{\FDU}{${\cal FDU}$}
\newcommand{\LFDU}{${\cal L}_{\cal FDU}$}
\newcommand{\dist}{\mbox{\tt dist}}
\newcommand{\fdist}{\mbox{\tt F\_dist}}
\newcommand{\fudist}{\mbox{\tt fuzzdist}}
\newcommand{\ftimes}{\mbox{\tt F\_times}}
\newcommand{\distance}{\mbox{\tt distance}}
\newcommand{\dura}{\mbox{\tt dura}}
\newcommand{\duration}{\mbox{\tt duration}}
\newcommand{\ptl}{${\cal PTL}$}
\newcommand{\tl}{${\cal TL}$}
\newcommand{\PTL}{${\cal PTL}$}
%
% TOKEN-TO-TIME PREDICATES AND FUNCTIONS
%
\newcommand{\now}{\mbox{\tt now}}
\newcommand{\BEGIN}{\mbox{\tt begin}}
\newcommand{\bbegin}{\mbox{\tt begin}}
\newcommand{\Bbegin}{\mbox{\tt Begin}}
\newcommand{\BBEGIN}{\mbox{\tt begin}}
\newcommand{\END}{\mbox{\tt end}}
\newcommand{\eend}{\mbox{\tt end}}
\newcommand{\Eend}{\mbox{\tt End}}
\newcommand{\EEND}{\mbox{\tt end}}
\newcommand{\ttime}{\mbox{\tt time}}
\newcommand{\inst}{\mbox{\tt instant}}
\newcommand{\instant}{\mbox{\tt instant}}
\newcommand{\period}{\mbox{\tt period}}
\newcommand{\interval}{\mbox{\tt interval}}
\newcommand{\pairs}{\mbox{\tt pairs}}
\newcommand{\partsof}{\mbox{\tt parts\_of}}
\newcommand{\makepair}{\mbox{\tt makepair}}
\newcommand{\first}{\mbox{\tt first}}
\newcommand{\second}{\mbox{\tt second}}
%
% TEMPORAL CONSTRAINTS
%
%\newcommand{\var}{\mbox{\em var}}
\newcommand{\val}{\mbox{\em val}}
\newcommand{\rel}{\mbox{\em rel}}
\newcommand{\dom}{\mbox{\em domain}}
%
% TOKEN-TO-SOMETHING PREDICATES AND FUNCTIONS
%
\newcommand{\relation}{\mbox{\em relation}}
\newcommand{\member}{\mbox{\em member}}
\newcommand{\attribute}{\mbox{\em attribute}}
\newcommand{\timetoken}{\mbox{\tt Time\_Token}}
\newcommand{\type}{\mbox{{\sc Type}}}
\newcommand{\TYPE}{\mbox{{\sc Type}}}
\newcommand{\ttype}{\mbox{\sc Ttype}}
%
% TEMPORAL modal operators
%
\newcommand{\since}{\ \mbox{\em\sc Since}\ }
\newcommand{\until}{\ \mbox{\em\sc Until}\ }
\newcommand{\AT}{\ \mbox{\em\sc AT}}
\newcommand{\ON}{\ \mbox{\em\sc ON}}
%
% TEMPORAL OCCURRENCE PREDICATES
%


% \renewcommand{\sc }{}
\newcommand{\on}{\mbox{\sc On}}
\newcommand{\at}{\mbox{\sc At}}
\newcommand{\false}{\mbox{\sc False}}
\newcommand{\true}{\mbox{\sc True}}
\newcommand{\TRUE}{\mbox{\sc True}}
\newcommand{\ttrue}{\mbox{\sc Temp\_True}}
\newcommand{\TTRUE}{\mbox{\sc Temp\_True}}
\newcommand{\holds}{\mbox{\sc Holds}}
\newcommand{\HOLDS}{\mbox{\sc Holds}}
\newcommand{\holdson}{\mbox{{\sc Holds}$_{on}$}}
\newcommand{\HOLDSON}{\mbox{{\sc Holds}$_{on}$}}
\newcommand{\holdsat}{\mbox{{\sc Holds}$_{at}$}}
\newcommand{\HOLDSAT}{\mbox{{\sc Holds}$_{at}$}}
\newcommand{\holdsin}{\mbox{{\sc Holds}$_{in}$}}
\newcommand{\HOLDSIN}{\mbox{{\sc Holds}$_{in}$}}
\newcommand{\occur}{\mbox{\sc Occurs}}
\newcommand{\OCCUR}{\mbox{\sc Occurs}}
\newcommand{\occurs}{\mbox{\sc Occurs}}
\newcommand{\OCCURS}{\mbox{\sc Occurs}}
\newcommand{\occursat}{\mbox{{\sc Occurs}$_{at}$}}
\newcommand{\OCCURSAT}{\mbox{{\sc Occurs}$_{at}$}}
\newcommand{\occurson}{\mbox{{\sc Occurs}$_{on}$}}
\newcommand{\OCCURSON}{\mbox{{\sc Occurs}$_{on}$}}
\newcommand{\occursin}{\mbox{{\sc Occurs}$_{in}$}}
\newcommand{\OCCURSIN}{\mbox{{\sc Occurs}$_{in}$}}
\newcommand{\occurring}{\mbox{\sc Occurring}}
\newcommand{\holdsonc}{\mbox{{\sc Holds}$^{^\sim}_{on}$}}
\newcommand{\holdsond}{\mbox{{\sc Holds}$^{\neg\hspace{-0.6mm}\_}_{on}$}}
\newcommand{\holdsatc}{\mbox{{\sc Holds}$^{^\sim}_{at}$}}       
\newcommand{\holdsatd}{\mbox{{\sc Holds}$^{\neg\hspace{-0.6mm}\_}_{at}$}}
\newcommand{\occursonc}{\mbox{{\sc Occurs}$^{^\sim}_{on}$}}
\newcommand{\occursond}{\mbox{{\sc Occurs}$^{\neg\hspace{-0.6mm}\_}_{on}$}}
\newcommand{\occursatc}{\mbox{{\sc Occurs}$^{^\sim}_{at}$}}     
\newcommand{\occursatd}{\mbox{{\sc Occurs}$^{\neg\hspace{-0.6mm}\_}_{at}$}}
%
% Temporal Millord II code of Temporal Occurrence Predicates
%
\newcommand{\cholds}{\mbox{\bf Holds}}
\newcommand{\choldson}{\mbox{\bf Holds\_on}}
\newcommand{\choldsat}{\mbox{\bf Holds\_at}}
\newcommand{\coccurson}{\mbox{\bf Occurs\_on}}
\newcommand{\coccursat}{\mbox{\bf Occurs\_at}}
\newcommand{\ctrueon}{\mbox{\bf True\_on}}
\newcommand{\ctrueat}{\mbox{\bf True\_at}}
\newcommand{\cposson}{\mbox{\bf Poss\_on}}
\newcommand{\cpossat}{\mbox{\bf Poss\_at}}
%
% tclp code
%
\newcommand{\logcode}[1]{{\small\tt\begin{tabular}{ll}#1\end{tabular}}}
\newcommand{\purecode}[1]{}
\newcommand{\logsep}{\mbox{}\indent}
%
% FLUENTS
%
\newcommand{\prog}{\mbox{\sc Prog}}
%\newcommand{\fc}{f^c}
%\newcommand{\Fc}{F^c}
%%%\newcommand{\fc}{$f^{^\sim}$}
%\newcommand{\fd}{f^d}
%\newcommand{\Fd}{F^d}
\newcommand{\fd}{$f^{\neg\hspace{-0.6mm}\_}$}
%\newcommand{\ii}{\lbrack\!\lbrack\ \rbrack\!\rbrack}
%\newcommand{\ii}[1]{\lbrack\!\lbrack #1 \rbrack\!\rbrack}
%
% meta- or token to token predicates
%
\newcommand{\cause}{\mbox{\sc Cause}}
\newcommand{\CAUSE}{\mbox{\sc Cause}}
\newcommand{\ecause}{\mbox{\sc Ecause}}
\newcommand{\ECAUSE}{\mbox{\sc Ecause}}
\newcommand{\effect}{\mbox{\sc Effect}}
\newcommand{\initiates}{\mbox{\sc Initiates}}
\newcommand{\terminates}{\mbox{\sc Terminates}}
\newcommand{\generates}{\mbox{\sc Generates}}
\newcommand{\causes}{\mbox{\sc Causes}}
\newcommand{\contradictory}{\mbox{\sc Contradictory}}
\newcommand{\exclusive}{\mbox{\sc Exclusive}}
\newcommand{\assume}{\mbox{\sc Assume}}
\newcommand{\incompatible}{\mbox{\tt Incompatible}}
%
% legal and trading domain predicates
                                % fluents
\newcommand{\contract}{\mbox{\em contract}}
\newcommand{\escrow}{\mbox{\em escrow}}
\newcommand{\sale}{\mbox{\em sale}}
\newcommand{\salecontract}{\mbox{\em sale\_contract}}
\newcommand{\offer}{\mbox{\em offer}}
\newcommand{\revocation}{\mbox{\em revocation}}
\newcommand{\acceptance}{\mbox{\em acceptance}}
\newcommand{\rejection}{\mbox{\em rejection}}
\newcommand{\confirmation}{\mbox{\em confirmation}}
\newcommand{\conf}{\mbox{\em conf}}
                                % legal and traiding fluents or domain attributes (roles)
\newcommand{\who}{\mbox{\em who}}
\newcommand{\fromwhom}{\mbox{\em from\_whom}}
\newcommand{\towhom}{\mbox{\em to\_whom}}
\newcommand{\bywhom}{\mbox{\em by\_whom}}
\newcommand{\what}{\mbox{\em what}}
\newcommand{\when}{\mbox{\em when}}
\newcommand{\contracttype}{\mbox{\em contract\_type}}
\newcommand{\contractstatus}{\mbox{\em contract\_status}}
\newcommand{\status}{\mbox{\em status}}
\newcommand{\offerer}{\mbox{\em offerer}}
\newcommand{\offeror}{\mbox{\em offeror}}
\newcommand{\offered}{\mbox{\em ffered}}
\newcommand{\offeree}{\mbox{\em offeree}}
                                % legal and trading domain values
\newcommand{\defined}{\mbox{\em Defined}}
\newcommand{\accepted}{\mbox{\em Accepted}}
\newcommand{\concluded}{\mbox{\em concluded}}
\newcommand{\revoked}{\mbox{\em Revoked}}
\newcommand{\effective}{\mbox{\em Effective}}
\newcommand{\expired}{\mbox{\em Expired}}
\newcommand{\sent}{\mbox{\em Sent}}
\newcommand{\committed}{\mbox{\em Committed}}
\newcommand{\obliged}{\mbox{\em Obliged}}
% \newcommand{\received}{\mbox{\em received}}
\newcommand{\dispatched}{\mbox{\em dispatched}}
\newcommand{\valid}{\mbox{\em valid}}
\newcommand{\obligation}{\mbox{\em obligation}}
\newcommand{\correctform}{\mbox{\em Correct\_form}}
                                % legal and trading individuals 
\newcommand{\smallco}{\mbox{\em sco}}
\newcommand{\bigco}{\mbox{\em bco}}
\newcommand{\smallCo}{\mbox{\em sco}}
\newcommand{\bigCo}{\mbox{\em bco}}
%
                                % legal and trading events 
\newcommand{\leave}{{\mbox{\em Leave}}}
\newcommand{\hire}{{\mbox{\em Hire}}}
\newcommand{\promote}{{\mbox{\em Promote}}}
\newcommand{\wwrite}{\mbox{\em Write}}
\newcommand{\writeoffer}{\mbox{\em Write}}
\newcommand{\reach}{\mbox{\em Reach}}
\newcommand{\send}{\mbox{\em Send}}
\newcommand{\senddocument}{\mbox{\em SendDoc}}
\newcommand{\sendgood}{\mbox{\em SendGoods}}
\newcommand{\receive}{\mbox{\em Receive}}
\newcommand{\receivedocument}{\mbox{\em RecDoc}}
\newcommand{\accept}{\mbox{\em Accept}}
\newcommand{\pay}{\mbox{\em Pay}}
\newcommand{\deliver}{\mbox{\em Deliver}}
\newcommand{\dispatch}{\mbox{\em Dispatch}}
\newcommand{\expire}{\mbox{\em Expire}}
%
                                % tenis domain predicates
\newcommand{\act}{{\em \mbox{act}}}
\newcommand{\actor}{{\em \mbox{actor}}}
\newcommand{\partner}{{\em \mbox{partner}}}
\newcommand{\place}{{\em \mbox{place}}}
\newcommand{\Blanes}{{\em \mbox{Blanes}}} 
\newcommand{\Barcelona}{{\em \mbox{Barcelona}}}
\newcommand{\playtennis}{{\em \mbox{play\_tennis}}}
\newcommand{\tennis}{{\em \mbox{tennis}}}
\newcommand{\play}{{\em \mbox{play}}}
\newcommand{\kiss}{{\em \mbox{kiss}}}
\newcommand{\rain}{\mbox{\em rain}}
\newcommand{\landslide}{\mbox{\em landslide}}
\newcommand{\dance}{\mbox{\em dance}}
\newcommand{\dances}{\mbox{\em dance}}
\newcommand{\decidedance}{\mbox{{\em decides\_to\_dance}}}
\newcommand{\decidedances}{\mbox{{\em decides\_to\_dance}}}
\newcommand{\destination}{{\em \mbox{destination}}}
\newcommand{\happy}{\mbox{\em happy}}
                                % tenis domain functions
\newcommand{\manager}{\mbox{\em manager}}
                                % tenis domain constants
\newcommand{\jordi}{\mbox{\em jordi}}
\newcommand{\Jordi}{\mbox{\em jordi}}
\newcommand{\felip}{{\em \mbox{felip}}}
\newcommand{\Felip}{{\em \mbox{felip}}}
\newcommand{\peter}{\mbox{\em peter}}
\newcommand{\Peter}{\mbox{\em peter}}
\newcommand{\John}{{\mbox{\em john}}}
\newcommand{\iolanda}{\mbox{\em iolanda}}
\newcommand{\yolanda}{\mbox{\em yolanda}}
\newcommand{\Iolanda}{\mbox{\em iolanda}}
\newcommand{\Yolanda}{\mbox{\em yolanda}}
\newcommand{\lecturer}{{\em \mbox{lecturer}}}
\newcommand{\mary}{\mbox{\em mary}}
\newcommand{\Mary}{\mbox{\em mary}}
\newcommand{\jane}{\mbox{\em jane}}
\newcommand{\Jane}{\mbox{\em jane}}
%\newcommand{\object}{{\em \mbox{object}}}
\newcommand{\pedro}{\mbox{{\em Pedro}}}
\newcommand{\professor}{\mbox{\em professor}}

\newcommand{\rank}{{\em \mbox{rank}}}
\newcommand{\rankvalue}{{\em \mbox{rankvalue}}}
\newcommand{\source}{{\em \mbox{source}}}
\newcommand{\salaryincrement}{\mbox{\em Salary\_increment}}
\newcommand{\stopdancing}{{\em \mbox{stopdancing}}}
\newcommand{\startcar}{\mbox{{\em start\_car}}}
\newcommand{\startdancing}{{\em \mbox{startdancing}}}
\newcommand{\subclass}{\mbox{{\em subclass}}}
\newcommand{\tired}{\mbox{{\em tired}}}
\newcommand{\wet}{\mbox{{\em wet}}}
\newcommand{\eddi}{\mbox{{\em Eddi}}}
\newcommand{\tami}{\mbox{{\em Tami}}}
\newcommand{\escrew}{\mbox{{\em escrew}}}
\newcommand{\seller}{\mbox{{\em seller}}}
\newcommand{\buyer}{\mbox{{\em buyer}}}
\newcommand{\disease}{\mbox{{\em disease}}}
%
                                % Electrical events
\newcommand{\turnon}{\mbox{{\em turn\_on}}}
\newcommand{\turnoff}{\mbox{{\em turn\_off}}}
\newcommand{\lighton}{\mbox{{\em light\_on}}}
\newcommand{\lightoff}{\mbox{{\em light\_off}}}
\newcommand{\signal}{\mbox{{\em signal}}}
\newcommand{\high}{\mbox{{\em high}}}
\newcommand{\low}{\mbox{{\em low}}}
\newcommand{\relay}{\mbox{{\em relay}}}
\newcommand{\open}{\mbox{{\em open}}}
\newcommand{\close}{\mbox{{\em close}}}
\newcommand{\closed}{\mbox{{\em closed}}}
%
% spanish
%
\newcommand{\causa}{\mbox{\sc Causa}}
\newcommand{\exclusivo}{\mbox{\sc Exclusivo}}
%\newcommand{\incompatible}{\mbox{\sc Incompatible}}
\newcommand{\inicia}{\mbox{\sc Inicia}}
\newcommand{\finaliza}{\mbox{\sc Finaliza}}
\newcommand{\inicio}{\mbox{\sc Inicio}}
\newcommand{\Fin}{\mbox{\sc Fin}}
\newcommand{\tiempo}{\mbox{\sc Tiempo}}
\newcommand{\rango}{{\em \mbox{rango}}}
\newcommand{\accion}{{\em \mbox{accion}}}
\newcommand{\fuente}{{\em \mbox{fuente}}}
\newcommand{\destino}{{\em \mbox{destino}}}
\newcommand{\pasara}{{\em \mbox{pasar\_a\_ser}}}
\newcommand{\dejarde}{{\em \mbox{dejar\_de\_ser}}}
\newcommand{\promocionar}{{\em \mbox{promocionar}}}
\newcommand{\titular}{{\em \mbox{titular}}}
\newcommand{\catedratico}{{\em \mbox{catedratico}}}
\newcommand{\Maria}{{\em \mbox{Maria}}}
%
% programming variables
%
\newcommand{\fifo}{\mbox{\tt FIFO}}
%
%%% functions del TTC
%
\newcommand{\rfnt}{{\em Retrieve\_facts}_{NT}}
\newcommand{\rft}{{\em Retrieve\_facts}_T}
\newcommand{\aft}{{\em Add\_facts}_T}
\newcommand{\afnt}{{\em Add\_facts}_{NT}}
\newcommand{\FB}{{\cal FB}}
\newcommand{\RB}{{\cal RB}}
\newcommand{\KB}{{\cal KB}}
\newcommand{\kb}{{\cal KB}}
\newcommand{\ikb}{{\cal I}_\infty({\cal KB})}
\newcommand{\ikbl}{{\cal I}^-_\infty({\cal KB})}
\newcommand{\ikbp}{{\cal I}^+_\infty({\cal KB})}
\newcommand{\skb}{{\cal S}({\cal KB})}
%\newcommand{\gkb}{{\em Gd}({\cal KB})}
%
% BIBLIOGRAPHY
%
%\renewcommand{\cite}[1]{[#1]}
%
% MISCELANIA
%
% \def\-{\_}
\def\ii{\'{\i}}
\def\nn{\~n}
\newcommand{\rar}{$\Rightarrow$}
\newcommand{\nosep}{\vspace{-\parskip}}
\newcommand{\sep}{\mbox{}\\\noindent}
\newcommand{\eqb}{\begin{eqnarray*}}
\newcommand{\eqe}{\end{eqnarray*}}
\newcommand{\Pf}{\em Proof:\rm}
\newcommand{\floor}[1]{\left\lfloor #1 \right\rfloor}
\newcommand{\abar}{\bar{a}}
\newcommand{\eps}{\varepsilon}
\newcommand{\half}{\frac{1}{2}}
%%%\newcommand{\union}{mbox{}
\newcommand{\UNION}{\bigcup}
\newcommand{\bigand}{\bigwedge}
\newcommand{\bin}[2]{(\!\!\!\begin{array}{c} {\scriptstyle #1}\\[-0.2 cm] {\scriptstyle #2 }\end{array}\!\!\!)}
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%
% logic new commands
%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\denota}{\mbox{\ \underline{denota}\ }}

\newcommand{\cert}{\mbox{\tt cert}}
\newcommand{\fals}{\mbox{\tt fals}}

%\newcommand{\land}{\mbox{$\wedge$}}
%\newcommand{\lor}{\mbox{$\vee$}}
\newcommand{\lexor}{\mbox{$\otimes$}}
\newcommand{\limplies}{\mbox{\ $\rightarrow$\ }}
\newcommand{\liff}{\mbox{\ $\leftrightarrow$\ }}
%\newcommand{\lnot}{\mbox{$\neg$}}
\newcommand{\ltrue}{\mbox{\tt 1}}
\newcommand{\lfalse}{\mbox{\tt 0}}

\newcommand{\li}{\mbox{$\wedge$}}
\newcommand{\lo}{\mbox{$\vee$}}
\newcommand{\loex}{\mbox{$\otimes$}}
\newcommand{\limplica}{\mbox{\ $\rightarrow$\ }}
\newcommand{\lno}{\mbox{$\neg$}}
\newcommand{\lcert}{\mbox{\tt 1}}
\newcommand{\lfals}{\mbox{\tt 0}}

\newcommand{\contradiccio}{\mbox{$\square$}}
\newcommand{\tautologia}{\mbox{$\blacksquare$}}

\newcommand{\satisfies}{\mbox{$\|\!-$}}
\newcommand{\entails}{\mbox{$\models$}}

% --- --- --- ---  newcommand algoritmes


% definició de Kw de funcions
\SetKwFunction{pdr}{Deduccio\_via\_Resolucio}
\SetKwFunction{pasaclausal}{Pas\_a\_Clausal}
\SetKwFunction{simplificar}{Simplificar}
\SetKwFunction{rlcs}{Resolucio\_Lineal\_Ordenada\_amb\_Conjunt\_Suport}
\SetKwFunction{selecinicial}{Seleccionar\_Claúsula\_Inicial}
\SetKwFunction{unifica}{Unifica}

\SetKwFunction{seleclateralordenadament}{Seleccionar\_Claúsula\_Lateral\_Ordenadament}
\SetKwFunction{backtracking}{Backtracking}
\SetKwFunction{resolvent}{Resolvent}
\SetKwFunction{selectroncal}{Seleccionar\_Claúsula\_Troncal}

% definició de Kw de dades
\SetKwData{conjuntdeclausules}{Conjunt\_de(Claúsula)}
\SetKwData{llistadeclausules}{Llista\_de(Claúsula)}
\SetKwData{clausula}{Claúsula}
\SetKwData{literal}{Literal}
\SetKwData{boolea}{booleà}
\SetKwData{candidateslateral}{Candidates\_Lateral}
\SetKwData{liniatroncal}{Linia\_Troncal}
\SetKwData{unificador}{unificador}
\SetKwData{fracas}{fracàs}

% --- --- --- ---

% \newcommand{\subs}[1]{\mbox{$_\mbox{#1}$}}
\newcommand{\subs}[1]{\mbox{$_{\mbox{\footnotesize #1}}$}}
% \newcommand{\sups}[1]{\mbox{$^\mbox{#1}$}}
\newcommand{\sups}[1]{#1}
% \newcommand{\gap}[1]{{\it e}\subs{{\it #1}}}
\newcommand{\gap}[1]{{\it e}$_#1$}
\newcommand{\englex}[1]{{\it #1}}
\newcommand{\englexcat}[2]{{\it #1}$_\mbox{#2}$}
\newcommand{\foreignlang}[1]{{\it #1}}
\newcommand{\gloss}[1]{{`#1'}}
\newcommand{\techterm}[1]{{\it #1}}
\newcommand{\verbquote}[1]{``#1''}
\newcommand{\scare}[1]{``#1''}
\newcommand{\attention}[1]{\mbox{\bf #1}}
\newcommand{\symbquote}[1]{`#1'}
\newcommand{\filler}[2]{#1$_#2$}
\newcommand{\bfiller}[2]{[#1]$_#2$}
% \newcommand{\filler}[2]{{\attention{#1}\subs{{\it #2}}}}
% \newcommand{\bfiller}[2]{{[\attention{#1}]\subs{{\it #2}}}}
% Reference the previous example
\newcommand{\prevex}{\arabic{equation}}
% Reference the next example
\newcommand{\nextex}{\addtocounter{equation}{1}\arabic{equation}\addtocounter{equation}{-1}}
\newcommand{\unacc}{{\begin{picture}(0,0)\put(-5,-2){*}\end{picture}}}
\newcommand{\semiacc}{{\begin{picture}(0,0)\put(-5,-2){?}\end{picture}}}
\newcommand{\lexass}{\mbox{:=}}
\newcommand{\rewrite}[3]{#1 $\rightarrow$ #2 #3}
\newcommand{\unaryrewrite}[2]{#1 $\rightarrow$ #2}
\newcommand{\tertiaryrewrite}[4]{#1 $\rightarrow$ #2 #3 #4}
\newcommand{\metarewrite}{$\downarrow$}
\newcommand{\labmetarewrite}[1]{$\downarrow$\subs{#1}}
\newcommand{\unaryrule}[2]{#1 $\Rightarrow$ #2}
\newcommand{\binaryrule}[3]{#1 + #2 $\Rightarrow$ #3}
\newcommand{\tertiaryrule}[4]{#1 + #2 + #3 $\Rightarrow$ #4}
\newcommand{\unarymetarule}[4]{\unaryrule{#1}{#2}$\Longrightarrow$\unaryrule{#3}{#4}}
%\newcommand{\var}[1]{{\it #1}}
\newcommand{\trans}{$\Rightarrow$}
\newcommand{\const}[1]{\mbox{#1$^\prime$}}
\newcommand{\constn}[2]{{#1$_\mbox{#2}^\prime$}}
\newcommand{\landpsection}[1]{\vspace{0.25in}\begin{center}\sc #1\end{center}
        \vspace{0.25in}}
% L&P main section: initial letter capital only
\newcommand{\landpsubsection}[1]{\vspace{0.15in}{\it #1}\vspace{0.15in}}
% L&P subsection: initial letters of all content words capital
\newcommand{\rmsubsubsection}[1]{\subssubsection*{{\rm #1}}}
\newcommand{\lamx}{$\lambda$\var{x}}
\newcommand{\lamy}{$\lambda$\var{y}}
\newcommand{\lamz}{$\lambda$\var{z}}
\newcommand{\lamxy}{$\lambda$\var{x}$\lambda$\var{y}}
\newcommand{\lamxyz}{$\lambda$\var{x}$\lambda$\var{y}$\lambda$\var{z}}
\newcommand{\I}{{\bf I}}
\newcommand{\B}{{\bf B}}
\newcommand{\C}{{\bf C}}
\newcommand{\W}{{\bf W}}
%\newcommand{\SS}{{\bf S}}
\newcommand{\K}{{\bf K}}
\newcommand{\T}{{\bf T}}
\newcommand{\PHI}{${\bf \Phi}$}
\newcommand{\fa}{\mbox{$>$}}
\newcommand{\ba}{\mbox{$<$}}
\newcommand{\fB}{\fa\B}
\newcommand{\bxB}{\B\sups{x}\ba}
\newcommand{\bB}{\B\ba}
\newcommand{\Bbx}{{\bf B\subs{b}\sups{x}}}
\newcommand{\Bfn}{\Bf\sups{n}}
\newcommand{\Bbxn}{\Bbx\sups{n}}
\newcommand{\fT}{\fa\T}
\newcommand{\bT}{\T\ba}
\newcommand{\Tfx}{{\bf T\subs{f}\sups{x}}}
\newcommand{\Tbx}{{\bf T\subs{b}\sups{x}}}
\newcommand{\pn}{{\bf p\subs{n}}}
\newcommand{\ro}{{\bf r\subs{o}}}
\newcommand{\Sf}{{\bf S\subs{f}}}
%\newcommand{\Sb}{{\bf S\subs{b}}}
\newcommand{\SK}{{\bf S$_K$}}
\newcommand{\V}{{\bf V}}
\newcommand{\A}{{\bf A}}
\newcommand{\N}{{\bf N}}
\newcommand{\D}{{\bf D}}
\newcommand{\intens}{\^{}}
\newcommand{\extens}{$^v$}
\newcommand{\vsl}{\mbox{\mbox{$|$}}}
\newcommand{\bsl }{\mbox{\mbox{$\backslash$}}}
%\newcommand{\up }{\mbox{\mbox{\^{}}}}
\newcommand{\dn }{\mbox{\mbox{\v{}}}}
\newcommand{\Id}{\mbox{\bf I\sups{\extens}\subs{T}}}
\newcommand{\Iu}{\mbox{\bf I\sups{\intens}\subs{4}}}
\newcommand{\Iun}{\mbox{\bf I\sups{\intens}\subs{4}\sups{$n$}}}
\newcommand{\scott}[1]{[[\mbox{#1}]]}
\newcommand{\Scott}[2]{[[#1]]#2}

\newcommand{\oscott}{[\hspace*{-0.025in}[}
\newcommand{\cscott}{]\hspace*{-0.025in}]}

\newcommand{\gka}{\mbox{$\alpha$}}
\newcommand{\gkb}{\mbox{$\beta$}}
%\newcommand{\tab}{\mbox{\hspace*{0.35in}}}
\newcommand{\tb}{\mbox{\hspace*{0.25in}}}
\newcommand{\link}{\mbox{$\ -\ $}}

%\newcommand{\And}{\mbox{$\wedge$}}
\newcommand{\Or}{\mbox{$\vee$}}
%\newcommand{\implies}{\mbox{\ $\rightarrow$\ }}
\newcommand{\Implies}{\mbox{\ $\rightarrow$\ }}
\newcommand{\Not}{\mbox{$\neg$}}

%\newcommand{\nao}{{\begin{picture}(0,0)\put(0,0){$/$}
%\put(0,0){0}\end{picture}}\ }
%\newcommand{\nao}{{}\circ\hspace*{-0.108in}/{}}
%\newcommand{\snao}{{}\circ\hspace*{-0.06in}/{}}
%\newcommand{\nau}{{}\circ\hspace*{-0.108in}\backslash{}}
%\newcommand{\snau}{{}\circ\hspace*{-0.06in}\backslash{}}

% \newcommand{\nao}{{\mbox{$\rangle$}}}
% \newcommand{\nau}{{\mbox{$\langle$}}}

\newcommand{\snao}{\makebox[0in][l]{{\footnotesize $\circ$}}{\footnotesize /}}
\newcommand{\snau}{\makebox[0in][l]{{\footnotesize $\circ$}}{\footnotesize \bsl}}

\newcommand{\unao}{{}\hspace*{-0.06in}\circ\hspace*{-0.108in}/{}}
\newcommand{\unau}{{}\circ\hspace*{-0.108in}\backslash{}\hspace*{-0.02in}}
\newcommand{\usu}{\backslash\hspace*{-0.015in}}
\newcommand{\uso}{\hspace*{-0.015in}/}
\newcommand{\uu}{\backslash\hspace*{-0.022in}}
\newcommand{\uo}{\hspace*{-0.02in}/}
% \newcommand{\nau}{{\begin{picture}(0,0)\put(0,0){$\backslash$}
% \put(0,0){0}\end{picture}}\ }

\newcommand{\nassp}{{\begin{picture}(0,0)\put(0,0){$\cdot$}
\put(0,0){0}\end{picture}}\ }
\newcommand{\afb}[3]{#1$\backslash$#2$/$#3}
\newcommand{\nfb}[3]{#1\nau #2\nao #3}

% --- --- --- --- glyn example macros

\newenvironment{topex}
   {\hspace{0.0001in}\vspace{0.1in}\newline\hspace*{0in}\begin{minipage}[t]{5.4in}\rule{5.4in}{0.01in}\newline\footnotesize\ \\{\bf Exercici}.}%
   {\end{minipage}}

\newenvironment{topprob}
   {\hspace{0.0001in}\vspace{0.1in}\newline\hspace*{0in}\begin{minipage}[t]{5.4in}\rule{5.4in}{0.01in}\newline\footnotesize\ \\{\bf Problema}.}%
   {\end{minipage}}

\newenvironment{bott}
   {\hspace{0.0001in}\vspace*{-0.125in}\newline\hspace*{0in}\begin{minipage}[t]{5.4in}\footnotesize\ \\{\bf Solució}.}%
   {\vspace{0.1in}\mbox{\ }\newline\rule{5.4in}{0.01in}\end{minipage}\vspace{0.1in}\newline}

\newenvironment{twobott}
   {\hspace{0.0001in}\vspace*{-0.125in}\newline\hspace*{0in}\begin{minipage}[t]{5.4in}\footnotesize\ \\}%
   {\vspace{0.1in}\newline\rule{5.4in}{0.01in}\end{minipage}\vspace{0.1in}\newline}

\newcounter{fnum}


\newcommand{\ftext}[1]{\addtocounter{fnum}{1}
\begin{center}
Figura
\thefnum. #1
\end{center}}

\newcommand{\prevf}{\thefnum}
% Reference the next figure

\newcommand{\nextf}{\addtocounter{fnum}{1}\thefnum\addtocounter{fnum}{-1}}
% Numbered display macro 

\newenvironment{disp}
   {\hspace*{-1.5in}\begin{equation}\begin{minipage}[t]{5in}}%
   {\end{minipage}\end{equation}\vspace{0in}}
% vspace 0.15in for double-spaced

\newenvironment{plaindisp}
   {\hspace{0.0001in}\vspace{0.1in}\newline\hspace*{0in}\begin{minipage}[t]{5.25in}}%
   {\end{minipage}\vspace{0.1in}\newline}

\newenvironment{dispfns}
   {\begin{footnotesize}\begin{equation}\begin{minipage}[t]{3.75in}}%
   {\end{minipage}\end{equation}\vspace{0in}\end{footnotesize}}

\setlength{\itemsep}{0in}

\newcommand{\boolpicklen}[4]% #1=lencommand, #2=bool, #3= len1, #4= len2
   {\setlength{#1}{#4}
    \setlength{#1}{-1#1}
    \addtolength{#1}{#3}
    \setlength{#1}{#2#1}
    \addtolength{#1}{#4}}

\newcounter{nolabelbool}
\newcommand{\nolabels}{\setcounter{nolabelbool}{1}}
\newcommand{\nol}{\nolabels}
\newlength{\exwidth}

\newcommand{\ulitem}[1]{
    \item
    \hspace*{-2em}
    \parbox[t]{\exwidth}{#1}}

\newcommand{\exonecolumn}%
   {\setlength{\exwidth}{\textwidth}
    \addtolength{\exwidth}{-0.5in}}

\newcommand{\extwocolumn}%
   {\setlength{\exwidth}{0.5\textwidth}
    \addtolength{\exwidth}{-0.5\columnsep}
    \addtolength{\exwidth}{-0.4in}}

\exonecolumn

\newenvironment{ex}
   {\begin{equation}
    \begin{minipage}[t]{\exwidth}
    \begin{list}{}{
      \settowidth{\labelsep}{\theequation}
      \boolpicklen{\leftmargin}{\value{nolabelbool}}{-.5em}{.8em}
      \addtolength{\leftmargin}{\labelsep}
      \addtolength{\exwidth}{-.5em}
      \setlength{\itemsep}{0.5\itemsep}
      \setlength{\labelwidth}{2.3em}
      \setlength{\labelsep}{1.2em}}}%
   {\end{list}
    \end{minipage}
    \end{equation}
    \setcounter{nolabelbool}{0}}

\newenvironment{nonumex}
   {\ \vspace*{.15in}\\
    \hspace*{2.5em}
    \begin{minipage}[t]{\exwidth}
    \begin{list}{}{
      \settowidth{\labelsep}{\theequation}
      \boolpicklen{\leftmargin}{\value{nolabelbool}}{-.5em}{.8em}
      \addtolength{\leftmargin}{\labelsep}
      \addtolength{\exwidth}{-.5em}
      \setlength{\itemsep}{0.5\itemsep}
      \setlength{\labelwidth}{2.3em}
      \setlength{\labelsep}{1.2em}}}%
   {\end{list}
    \end{minipage}
    \setcounter{nolabelbool}{0}
    \vspace*{.18in}\\}

\newenvironment{exfns}
   {\begin{equation}
    \begin{minipage}[t]{\exwidth}
    \begin{footnotesize}
    \begin{list}{}{
      \settowidth{\labelsep}{\theequation}
      \boolpicklen{\leftmargin}{\value{nolabelbool}}{-.5em}{.8em}
      \addtolength{\leftmargin}{\labelsep}
      \addtolength{\exwidth}{-.5em}
      \setlength{\labelwidth}{2.3em}
      \setlength{\labelsep}{1.2em}}}%
   {\end{list}
    \end{footnotesize}
    \end{minipage}
    \end{equation}
    \setcounter{nolabelbool}{0}}

% refer to some footnote
\newcommand{\somefootnote}[1]{\addtocounter{footnote}{#1}
                     (\arabic{footnote})
                     \addtocounter{footnote}{-#1}}

%%***************** end of my example macro

\newcommand{\upsl}{\mbox{$\uparrow$}}
\newcommand{\dupsl}{\mbox{$\Uparrow$}}
\newcommand{\dbsl}{\mbox{$\backslash\backslash$}}
\newcommand{\pfsl}{\mbox{$\nearrow$}}
\newcommand{\pbsl}{\mbox{$\nwarrow$}}
\newcommand{\perm}{\mbox{$\triangle$}}
\newcommand{\union}{\mbox{$\cup$}}
\newcommand{\insect}{\mbox{$\cap$}}

\newcommand{\hdsl}{\mbox{$\ll$}}
\newcommand{\hdcat}[2]{#1\hdsl #2}

\renewcommand{\pfsl}{\mbox{\zlbox{$\circ$}/}}
\renewcommand{\pbsl}{\mbox{\zlbox{$\circ$}\bsl}}

\newcommand{\refop}{\mbox{$\ominus$}}
\newcommand{\refopa}{\mbox{$\otimes$}}

\newcommand{\refsl}{/\refop}
\newcommand{\refbsl}{\bsl\refop}

\newcommand{\for}{\mbox{\verb+>+}}     %\newcommand{\for}{\mbox{$>$}}
\newcommand{\bac}{\mbox{\verb+<+}}     %\newcommand{\bac}{\mbox{$<$}}
\newcommand{\forb}{\for\bx}
\newcommand{\bacb}{\bac\bx}
\newcommand{\fort}{\for\tx}
\newcommand{\bact}{\bac\tx}

%\newcommand{\fc}{$\gg$}
%\newcommand{\bc}{$\ll$}

\newcommand{\fx}{{\bf f}}
\newcommand{\bx}{{\bf B}}
\newcommand{\cx}{{\bf C}}
\newcommand{\dx}{{\bf D}}
\newcommand{\vx}{{\bf V}}
\newcommand{\ax}{{\bf A}}
\newcommand{\hx}{{\bf H}}
\newcommand{\tx}{{\bf T}}
\newcommand{\bn}[1]{\bx$^{#1}$}
\newcommand{\rx}{{\bf R}}
\newcommand{\sx}{{\bf S}}
\newcommand{\kx}{{\bf K}}
\newcommand{\nx}{{\bf N}}
\newcommand{\ix}{{\bf I}}
\newcommand{\rn}[1]{\rx$^{#1}$}

\newlength{\lenabc}
\newcommand{\textspace}[1]{\settowidth{\lenabc}{#1}\hspace*{\lenabc}}
\newcommand{\ungr}{\makebox[0in][r]{*}}
\newcommand{\judg}[1]{\makebox[0in][r]{#1}}
\newcommand{\sub}[1]{\mbox{$_{\mbox{\scriptsize#1}}$}}
\newcommand{\super}[1]{{$^{\mbox{\scriptsize#1}}$}}
\newcommand{\zsuper}[1]{{\makebox[0pt][l]{$^{\mbox{\scriptsize\,#1}}$}}}
\newcommand{\prim}{\mbox{$^\prime$}}
\newcommand{\imp}{\mbox{$\rightarrow$}}
\newcommand{\lam}{\mbox{$\lambda$}}
\newcommand{\norm}[1]{{\normalsize #1}}
\newcommand{\zlbox}[1]{\makebox[0pt][l]{#1}}
\newcommand{\zrbox}[1]{\makebox[0in][r]{#1}} 
\newcommand{\zbox}[1]{\makebox[0in]{#1}} 
\newcommand{\ptbox}[1]{\makebox(0,0){#1}}

\newcommand{\thirdin}{\hspace*{.33in}}

\newcommand{\lingform}[1]{`#1'}

\newcommand{\senteg}[1]{
    \ \vspace*{-0.12in}\\
    \begin{minipage}[t]{\textwidth}
    \begin{tabular}{lllllllllllllll}
    #1
    \end{tabular}
    \end{minipage}}

\newcommand{\glossbox}[1]{\zlbox{`#1'}}

\newcommand{\subsetof}[2]{#1 $\subseteq$ #2}
\newcommand{\myphi}{\mbox{\large $\phi$}}
\newcommand{\mypsi}{\mbox{\large $\psi$}}
\newcommand{\mypi}{\mbox{\large $\pi$}}
\newcommand{\myphin}[1]{\mbox{\large $\phi^{#1}$}}
\newcommand{\halfbreakin}{\vspace*{.05in} \\ \thirdin}

\newcommand{\halfbreak}{\vspace*{.05in} \\ }

\newcommand{\fc}{\for\bn{n}}
\newcommand{\bc}{\bac\bn{n}}
\newcommand{\app}{\mbox{\ }}
\newcommand{\pair}{\mbox{,\ }}
\newcommand{\inl}{\mbox{$i\ $}}
\newcommand{\inr}{\mbox{$j\ $}}

\newcommand{\munion}{\mbox{$\cup_m$}}
\newcommand{\cmunion}{\mbox{$\}_m$}}

%\newcommand{\first}{\mbox{$\pi_1$}}
%\newcommand{\second}{\mbox{$\pi_2$}}

%***************************************************************************
%          DERIVATION DRAWER
%***************************************************************************

% Some length commands needed by the derivation drawer
%
\newlength{\dtopskip}
\newlength{\dbottomskip}
\newlength{\dheight}
\newlength{\lena}
\newlength{\lenb}
\newlength{\lenc}
\newlength{\firstlen}
\newlength{\secondlen}
\newlength{\dmargin}
\newlength{\dmarginbasic}
\newlength{\wordgap}
\newlength{\spacing}
\newlength{\dlineskip}
\newlength{\textlen}
\newlength{\vertpos}
\newlength{\centrept}
\newlength{\dlinelen}
\newlength{\catlen}
\newlength{\dlineraise}
\newlength{\dlinethickness}
\newlength{\lone}
\newlength{\ltwo}
\newlength{\lthree}
\newlength{\rone}
\newlength{\rtwo}
\newlength{\rthree}
\newlength{\lfour}
\newlength{\rfour}
\newlength{\lfive}
\newlength{\rfive}
\newlength{\lsix}
\newlength{\rsix}
\newlength{\lseven}
\newlength{\rseven}
\newlength{\leight}
\newlength{\reight}
\newlength{\lnine}
\newlength{\rnine}
\newlength{\lten}
\newlength{\rten}


% sets length command given as first argument to take value of 
% second or third argument - whichever is the larger
%
\newcommand{\settolargerlength}[3]{
   \setlength{\firstlen}{#2}
   \addtolength{\firstlen}{-1#3}
   \setlength{\secondlen}{#3}
   \addtolength{\secondlen}{-1#2}
   \settowidth{\firstlen}{\framebox[\firstlen]{}\framebox[\secondlen]{}}
   \addtolength{\firstlen}{#2}
   \addtolength{\firstlen}{#3}
   \setlength{#1}{0.5\firstlen}}

% sets length command given as first argument to take value of 
% second or third argument - whichever is the smaller
%
\newcommand{\settosmallerlength}[3]{
   \setlength{\firstlen}{#2}
   \addtolength{\firstlen}{-1#3}
   \setlength{\secondlen}{#3}
   \addtolength{\secondlen}{-1#2}
   \settowidth{\firstlen}{\framebox[\firstlen]{}\framebox[\secondlen]{}}
   \setlength{\firstlen}{-1\firstlen}
   \addtolength{\firstlen}{#2}
   \addtolength{\firstlen}{#3}
   \setlength{#1}{0.5\firstlen}}

% Put Derivational Object:      < linenum, vert-dist, horiz-dist, text >
%                                   #1         #2        #3        #4
% puts text specified as #4 at position in derivation given by other
% parameters - vertical coordinate distance will be #1 times
% \dlineskip PLUS #2, horizontal coordinate distance #3
%
%
\newcommand{\putdobj}[4]{
    \setlength{\vertpos}{\dtopskip}
    \addtolength{\vertpos}{#1\dlineskip}
    \addtolength{\vertpos}{#2}
    \put(0,0){\raisebox{\vertpos}{\rule{#3}{0in}{#4}}}}

% Put Derivational Object centred: < linenum, vert-dist, horiz-dist, text >
%                                      #1         #2        #3        #4
% puts text specified as #4 CENTRED at position in derivation given by 
% other parameters - vertical coordinate distance will be #1 times
% \dlineskip PLUS #2, horizontal coordinate distance #3
%
%
\newcommand{\putdobjcentred}[4]{
   \putdobj{#1}{#2}{#3}{\makebox[0in]{#4}}}

% Put Derivational Parbox:< linenum, vert-dist, horiz-dist, box-len, text >
%                              #1         #2        #3        #4      #5
% puts a parbox of len #4 containing text specified as #5 at position 
% in derivation given by other parameters - vertical coordinate distance 
% will be #1 times \dlineskip PLUS #2, horizontal coordinate distance #3
%
%
\newcommand{\putdparbox}[5]{
   \putdobj{#1}{#2}{#3}{\parbox[t]{#4}{#5}}}


% Derivation Line command: < line-length >
%
% draws a sl.raised rule of the length given
%
\newcommand{\derivline}[1]{\rule[\dlineraise]{#1}{\dlinethickness}}

\newenvironment{deriv}[1]%
  {\noindent
   \begin{minipage}[t]{1in}
   \setlength{\wordgap}{1.5em}%   
   \setlength{\dlineraise}{0.265em}
   \setlength{\dlineskip}{-0.9em}   
   \setlength{\dtopskip}{\dlineskip}
   \setlength{\dbottomskip}{0\dlineskip}
   \setlength{\dlinethickness}{0.01in}
   \setlength{\dmarginbasic}{0in}
   \resetdmargin
   \setlength{\dheight}{-#1\dlineskip}
   \begin{picture}(0,0)}%
  {\end{picture}
   \newline
   \addtolength{\dheight}{-\dtopskip}
   \addtolength{\dheight}{-\dbottomskip}
   \rule{0in}{\dheight}
   \newline
   \end{minipage}
   \newline}
   
\newenvironment{derivfns}[1]%
  {\begin{footnotesize}
   \begin{deriv}{#1}}%
  {\end{deriv}
   \end{footnotesize}}


\newcommand{\shiftdtopskip}[1]{\addtolength{\dtopskip}{#1\dlineskip}}

\newcommand{\shiftdmargin}[1]{
   \setlength{\lena}{#1}
   \addtolength{\dmargin}{\lena}}

\newcommand{\resetdmargin}{\setlength{\dmargin}{\dmarginbasic}}


% PREWORD command:< TEXT >
%                    #1   
% places text #1 on line 0 at position given by \dmargin - then moves
% \dmargin along by length of text plus \wordgap
%
\newcommand{\preword}[1]{
  \putdobj{0}{0in}{\dmargin}{#1}
  \settowidth{\textlen}{#1}
  \shiftdmargin{\textlen}
  \shiftdmargin{\wordgap}}

% same as preword 
\newcommand{\derivitem}[1]{\preword{#1}}
 
% WORD command: < left, right, word, category, spacing >
%                  #1    #2     #3      #4       #5
% puts word, derivline and category on lines 0, 1, 2 respectively at
% position calculated from \dmargin and width of items (ie, with of #3,
% #4 or #5 - whichever is the wider), then moves \dmargin along by
% larger item width plus \wordgap. Sets #1 and #2 length commands to
% distances in to left and right edges of the category text.
%
\newcommand{\word}[5]{                    
  \settowidth{\textlen}{#3}
  \settowidth{\catlen}{#4}
  \settowidth{\spacing}{#5}
  \settolargerlength{\dlinelen}{\textlen}{\catlen}
  \settolargerlength{\spacing}{\spacing}{\dlinelen}
  \setlength{\centrept}{\dmargin}
  \addtolength{\centrept}{0.5\spacing}
  \putdobjcentred{0}{0in}{\centrept}{#3}
  \putdobjcentred{1}{0in}{\centrept}{\derivline{\dlinelen}}
  \putdobjcentred{2}{0in}{\centrept}{#4}
  \setlength{#1}{\centrept}
  \addtolength{#1}{-0.5\catlen}
  \setlength{#2}{\centrept}
  \addtolength{#2}{0.5\catlen}
  \shiftdmargin{\spacing}
  \shiftdmargin{\wordgap}}

% WORD"num" commands < word, category, spacing-text >
% set of commands which call upon the WORD macro and instanciating its
% first and second arguments as the length commands \l"num" and \r"num"
%
\newcommand{\wordone}[3]{\word{\lone}{\rone}{#1}{#2}{#3}}
\newcommand{\wordtwo}[3]{\word{\ltwo}{\rtwo}{#1}{#2}{#3}}
\newcommand{\wordthree}[3]{\word{\lthree}{\rthree}{#1}{#2}{#3}}
\newcommand{\wordfour}[3]{\word{\lfour}{\rfour}{#1}{#2}{#3}}
\newcommand{\wordfive}[3]{\word{\lfive}{\rfive}{#1}{#2}{#3}}
\newcommand{\wordsix}[3]{\word{\lsix}{\rsix}{#1}{#2}{#3}}
\newcommand{\wordseven}[3]{\word{\lseven}{\rseven}{#1}{#2}{#3}}
\newcommand{\wordeight}[3]{\word{\leight}{\reight}{#1}{#2}{#3}}
\newcommand{\wordnine}[3]{\word{\lnine}{\rnine}{#1}{#2}{#3}}
\newcommand{\wordten}[3]{\word{\lten}{\rten}{#1}{#2}{#3}}



% CAT SPACE command: < left, right, category, space-text>
%                        #1    #2      #3      #4
% puts category on line 0 at 
% position calculated from \dmargin and width of items (ie, with of #3,
% #4 - whichever is the wider), then moves \dmargin along by
% larger item width plus \wordgap. Sets #1 and #2 length commands to
% distances in to left and right edges of the category text.
%
\newcommand{\cat}[4]{
  \settowidth{\catlen}{#3}
  \settowidth{\spacing}{#4}
  \settolargerlength{\spacing}{\spacing}{\catlen}
  \setlength{\centrept}{\dmargin}
  \addtolength{\centrept}{0.5\spacing}
  \putdobjcentred{0}{0in}{\centrept}{#3}
  \setlength{#1}{\centrept}
  \addtolength{#1}{-0.5\catlen}
  \setlength{#2}{\centrept}
  \addtolength{#2}{0.5\catlen}
  \shiftdmargin{\spacing}
  \shiftdmargin{\wordgap}}


% CAT"num" macro < category, spacing >
% set of macros calling on the CAT macro - instanciating its first and
% second arguments as the length commands \l"num" and \r"num" 
\newcommand{\catone}[2]{\cat{\lone}{\rone}{#1}{#2}}
\newcommand{\cattwo}[2]{\cat{\ltwo}{\rtwo}{#1}{#2}}
\newcommand{\catthree}[2]{\cat{\lthree}{\rthree}{#1}{#2}}
\newcommand{\catfour}[2]{\cat{\lfour}{\rfour}{#1}{#2}}
\newcommand{\catfive}[2]{\cat{\lfive}{\rfive}{#1}{#2}}
\newcommand{\catsix}[2]{\cat{\lsix}{\rsix}{#1}{#2}}
\newcommand{\catseven}[2]{\cat{\lseven}{\rseven}{#1}{#2}}
\newcommand{\cateight}[2]{\cat{\leight}{\reight}{#1}{#2}}
\newcommand{\catnine}[2]{\cat{\lnine}{\rnine}{#1}{#2}}
\newcommand{\catten}[2]{\cat{\lten}{\rten}{#1}{#2}}



% REDUCE command : < line, left, right, label, category >
%                     #1    #2    #3     #4       #5
% puts a deriv-line on line #1 running between horizontal positions specified
% as #2 and #3. Puts labeling text #4 at the end of this line, and
% puts category #5 centred on the line below the deriv-line. Sets #2 and #3
% to distances in to left and right edges of the category.
%
\newcommand{\reduce}[5]{
  \setlength{\dlinelen}{#3}
  \addtolength{\dlinelen}{-1#2}
  \settowidth{\catlen}{#5}
      %
  \settolargerlength{\dlinelen}{\dlinelen}{\catlen} 
      % this line of code sets length of line to be length of category text
      % if this is larger than distance between left and right coordinates.
      %
  \setlength{\centrept}{0.5#2}
  \addtolength{\centrept}{0.5#3}
  \putdobjcentred{#1}{0in}{\centrept}{\derivline{\dlinelen}\makebox[0in][l]{#4}}
  \putdobjcentred{#1}{\dlineskip}{\centrept}{#5}
  \setlength{#2}{\centrept}
  \addtolength{#2}{-0.5\catlen}
  \setlength{#3}{\centrept}
  \addtolength{#3}{0.5\catlen}}


% MAKELABEL < key > 
% associates key #1 with next number in the "equation" sequence, without
% causing LaTeX to write an instance of the number on the page
%
\newcommand{\mymakelabel}[1]%
    {\makebox[0in]{\begin{picture}(0,0)%
                   \put(700,0){\parbox{1in}{\begin{equation}
                                            \label{#1}
                                            \end{equation}}}%
                   \end{picture}}}



% PUTDERIVNUMKEY < lineno, horiz-dist, key > 
% associates key #1 with next number in the "equation" sequence, and puts
% a reference to this number at stated position
%
\newcommand{\putderivnumkey}[3]%
    {\putdparbox{#1}{0in}{#2}{.5in}%
                {\begin{equation}
                 \label{#3}
                 \end{equation}}}

% PUTDERIVNUM < lineno, horiz-dist >
% puts reference to next number in the ``equation'' sequence at stated
% position
%
\newcommand{\putderivnum}[2]%
    {\putdparbox{#1}{0in}{#2}{.5in}%
                {\begin{equation}
                 \end{equation}}}


% DERIVNUMKEY < key > 
% associates key #1 with next number in the "equation" sequence, and puts
% a reference to this number at start of line 0 in derivation.
%
\newcommand{\derivnumkey}[1]{\putderivnumkey{0}{0in}{#1}}


% DERIVNUM
% puts reference to next number in the ``equation'' sequence at start
% of line 0 in the derivation
%
\newcommand{\derivnum}{\putderivnum{0}{0in}}


\newcommand{\axiom}[5]{
  \settowidth{\catlen}{#3}
  \settowidth{\spacing}{#4}
  \settolargerlength{\spacing}{\spacing}{\catlen}
  \setlength{\centrept}{\dmargin}
  \addtolength{\centrept}{0.5\spacing}
  \putdobjcentred{#5}{0in}{\centrept}{#3}
  \setlength{#1}{\centrept}
  \addtolength{#1}{-0.5\catlen}
  \setlength{#2}{\centrept}
  \addtolength{#2}{0.5\catlen}
  \shiftdmargin{\spacing}
  \shiftdmargin{\wordgap}}

% AXIOM'N' < LINENO > < SEQUENT > < SPACING-TEXT >

\newcommand{\axiomone}[3]{\axiom{\lone}{\rone}{#2}{#3}{#1}}
\newcommand{\axiomtwo}[3]{\axiom{\ltwo}{\rtwo}{#2}{#3}{#1}}
\newcommand{\axiomthree}[3]{\axiom{\lthree}{\rthree}{#2}{#3}{#1}}
\newcommand{\axiomfour}[3]{\axiom{\lfour}{\rfour}{#2}{#3}{#1}}
\newcommand{\axiomfive}[3]{\axiom{\lfive}{\rfive}{#2}{#3}{#1}}
\newcommand{\axiomsix}[3]{\axiom{\lsix}{\rsix}{#2}{#3}{#1}}
\newcommand{\axiomseven}[3]{\axiom{\lseven}{\rseven}{#2}{#3}{#1}}
\newcommand{\axiomeight}[3]{\axiom{\leight}{\reight}{#2}{#3}{#1}}
\newcommand{\axiomnine}[3]{\axiom{\lnine}{\rnine}{#2}{#3}{#1}}
\newcommand{\axiomten}[3]{\axiom{\lten}{\rten}{#2}{#3}{#1}}
%*************************************************************************
%    (end of derivation drawer)
%*************************************************************************

%*************************************************************************
%    RESOLUTION TREE DRAWER
%*************************************************************************
\newcommand{\resol}[3]{
        \begin{picture}(100,60)
        \put(0,60){\makebox(0,0){$#1$}}
        \put(80,60){\makebox{$#2$}}
        \put(60,30){\makebox{$#3$}}
        \put(0,50){\line(0,-1){40}}
        \put(0,10){\line(2,1){80}}
        \end{picture}\\
}
\newcommand{\resolsuccess}{
        \begin{picture}(100,0)
        \put(0,10){\makebox(0,0){$\square$}}
        \end{picture}
}
\newcommand{\resolfailure}{
        \begin{picture}(100,0)
        \put(0,10){\makebox(0,0){$--$}}
        \end{picture}
}
\newcommand{\resolres}[1]{
        \begin{picture}(100,0)
        \put(0,10){\makebox(0,0){$#1$}}
        \end{picture}
}
\newenvironment{resolutiontree}
   {\hspace{0.0001in}\begin{center}\begin{tabular}[t]{l}}%
   {\end{tabular}\end{center}}

%*************************************************************************
%    (end of derivation drawer)
%*************************************************************************


% \newcommand{\axiom}[5]{
%  \settowidth{\catlen}{#3}
%  \settowidth{\spacing}{#4}
%  \settolargerlength{\spacing}{\spacing}{\catlen}
%  \setlength{\centrept}{\dmargin}
%  \addtolength{\centrept}{0.5\spacing}
%  \putdobjcentred{#5}{0in}{\centrept}{#3}
%  \setlength{#1}{\centrept}
%  \addtolength{#1}{-0.5\catlen}
%  \setlength{#2}{\centrept}
%  \addtolength{#2}{0.5\catlen}
%  \shiftdmargin{\spacing}
%  \shiftdmargin{\wordgap}}

% AXIOM'N' < LINENO > < SEQUENT > < SPACING-TEXT >

%\newcommand{\axiomone}[3]{\axiom{\lone}{\rone}{#2}{#3}{#1}}
%\newcommand{\axiomtwo}[3]{\axiom{\ltwo}{\rtwo}{#2}{#3}{#1}}
%\newcommand{\axiomthree}[3]{\axiom{\lthree}{\rthree}{#2}{#3}{#1}}
%\newcommand{\axiomfour}[3]{\axiom{\lfour}{\rfour}{#2}{#3}{#1}}
%\newcommand{\axiomfive}[3]{\axiom{\lfive}{\rfive}{#2}{#3}{#1}}
%\newcommand{\axiomsix}[3]{\axiom{\lsix}{\rsix}{#2}{#3}{#1}}
%\newcommand{\axiomseven}[3]{\axiom{\lseven}{\rseven}{#2}{#3}{#1}}
%\newcommand{\axiomeight}[3]{\axiom{\leight}{\reight}{#2}{#3}{#1}}
%\newcommand{\axiomnine}[3]{\axiom{\lnine}{\rnine}{#2}{#3}{#1}}
%\newcommand{\axiomten}[3]{\axiom{\lten}{\rten}{#2}{#3}{#1}}

\newcommand{\seq}[2]{\mbox{#1 $\Rightarrow$ #2}}
\newcommand{\axx}[1]{#1 $\Rightarrow$ #1}

\newcommand{\gleft}[1]{\,[#1L]}
\newcommand{\gright}[1]{\,[#1R]}
\newcommand{\elim}[1]{{\scriptsize#1E}}
\newcommand{\intro}[2]{{\scriptsize#1I\super{\,#2}}}
\newcommand{\cut}{\,[cut]}
\newcommand{\rp}{\mbox{$>$}}

\newcommand{\Gam}{\mbox{$\Gamma$}}
\newcommand{\Om}{\mbox{$\Omega$}}
\newcommand{\Del}{\mbox{$\Delta$}}
\newcommand{\Lam}{\mbox{$\Lambda$}}

%% \newcommand{\xmod}[1]%
%%      {\mbox{${\setlength{\fboxsep}{0.5mm} \: 
%%       \fbox{{\tiny #1}\rule[.1ex]{0ex}{0.8ex}} \:}$}}

\newcommand{\xmod}[1]%
     {\mbox{${\setlength{\fboxsep}{0.5mm} \: 
      \fbox{{\tiny \raisebox{.2em}{#1}}\rule[.23ex]{0ex}{0.8ex}} \:}$}}

%\newcommand{\mod}{\xmod{\hspace*{0.4em}}}
% \newcommand{\smod}{\xmod{a}}

%  \newcommand{\mod}{\mbox{$\Box$}}
%  \newcommand{\xmod}[1]%
%     {\zlbox{\hspace*{.3em}\raisebox{.06em}{{\scriptsize #1}}}\mod}


%  < vlevel, hdist, text >

\newcommand{\lta}[3]{
   \setlength{\lena}{-0.5in}
   \addtolength{\lena}{#1\lena}
   \addtolength{\lena}{.4in}
   \putdobjcentred{0}{\lena}{#2}{#3}
   \putdobj{.5}{\lena}{#2}{\line(5,-3){36}}
   \putdobj{.5}{\lena}{#2}{\line(-5,-3){36}}
   \setlength{\lone}{#2}
   \addtolength{\lone}{-0.5in}
   \setlength{\rone}{\lone}
   \addtolength{\rone}{1in}}


%  < vlevel, hdist, text >

\newcommand{\ltb}[3]{
   \setlength{\lena}{-0.5in}
   \addtolength{\lena}{#1\lena}
   \addtolength{\lena}{.4in}
   \putdobjcentred{0}{\lena}{#2}{#3}
   \putdobj{.5}{\lena}{#2}{\line(3,-1){65}}
   \putdobj{.5}{\lena}{#2}{\line(-5,-3){36}}
   \setlength{\lone}{#2}
   \addtolength{\lone}{-0.5in}
   \setlength{\rone}{\lone}
   \addtolength{\rone}{1.43in}}


%  < vlevel, hdist, text >

\newcommand{\ltc}[3]{
   \setlength{\lena}{-0.5in}
   \addtolength{\lena}{#1\lena}
   \addtolength{\lena}{.4in}
   \putdobjcentred{0}{\lena}{#2}{#3}
   \putdobj{.5}{\lena}{#2}{\line(1,-1){22}}
   \putdobj{.5}{\lena}{#2}{\line(-1,-1){22}}
   \setlength{\lone}{#2}
   \addtolength{\lone}{-0.35in}
   \setlength{\rone}{\lone}
   \addtolength{\rone}{.7in}}

%  < vlevel, hdist, text >

\newcommand{\putnode}[3]{
   \setlength{\lena}{-0.5in}
   \addtolength{\lena}{#1\lena}
   \addtolength{\lena}{.4in}
   \putdobjcentred{0}{\lena}{#2}{#3}}

% < vlevel, hdist, text-node, text-lex >

\newcommand{\ltlex}[4]{
   \setlength{\lena}{-0.5in}
   \addtolength{\lena}{#1\lena}
   \addtolength{\lena}{.4in}
   \putdobjcentred{0}{\lena}{#2}{#3}
   \putdobj{.5}{\lena}{#2}{\line(0,-1){22}}
   \addtolength{\lena}{-.5in}
   \putdobjcentred{0}{\lena}{#2}{#4}
   \setlength{\lone}{#2}}
   


\newcommand{\proofdots}[2]{
    \settowidth{\lena}{#1}
    \hspace*{-0.4\lena}
    \makebox[\lena]{\makebox[0in][l]{#1}
                    \hspace*{0.5\lena}
                    \hspace*{-0.05in}
                    \raisebox{.14in}{\makebox[0in]{$\vdots$}}
                    \hspace*{-0.04in}
                    \raisebox{.35in}{\makebox[0in]{#2}}}
    \hspace*{.2\lena}}

\newcommand{\noi}{\noindent}

\newcommand{\lang}[1]{\mbox{${\cal L}_{{\rm #1}}$}}

\newcommand{\langsubsets}[2]{\mbox{$\lang{#1} \subseteq \lang{#2}$}}


\newcommand{\interp}[1]{%
    \makebox[.6em][l]{\begin{picture}(0,0)(0,2.5)
          \put(0,0){\line(0,1){12}}
          \put(2.5,0){\line(0,1){12}}
          \put(0,12){\line(1,0){4}}
          \put(0,0){\line(1,0){4}}
          \end{picture}}#1\makebox[.7em][l]{\,\begin{picture}(0,0)(0,2.5)
                                            \put(4,0){\line(0,1){12}}
                                            \put(1.5,0){\line(0,1){12}}
                                            \put(0,12){\line(1,0){4}}
                                            \put(0,0){\line(1,0){4}}
                                            \end{picture}}}


\newcommand{\permreduce}[8]{
    \reduce{#1}{#2}{#3}{#6}{\makebox[\dlinelen]{#7\hfill #8}}
    \settowidth{#4}{#7}
    \addtolength{#4}{#2}
    \settowidth{#5}{#8}
    \setlength{#5}{-1#5}
    \addtolength{#5}{#3}}


\newcommand{\nolinereduce}[4]{
  \settowidth{\catlen}{#4}
  \setlength{\centrept}{0.5#2}
  \addtolength{\centrept}{0.5#3}
  \putdobjcentred{#1}{0in}{\centrept}{#4}
  \setlength{#2}{\centrept}
  \addtolength{#2}{-0.5\catlen}
  \setlength{#3}{\centrept}
  \addtolength{#3}{0.5\catlen}}


\newcommand{\wordgapstretch}[1]{
    \setlength{\wordgap}{#1\wordgap}}

\newcommand{\derives}{\mbox{$\ \Rightarrow\ $}}
\newcommand{\substin}{\mbox{$\leftarrow$}}

\newcommand{\yields}{\mbox{$\ \vdash\ $}}
\newcommand{\equivd}{\mbox{$\ \dashv\vdash\ $}}
%\newcommand{\yields}{\mbox{$\ \Rightarrow\ $}}
\newcommand{\ta}[3]{#1-#2:#3}
\newcommand{\lingobj}[1]{`#1'}
\newcommand{\contracts}{\rhd}
\newcommand{\reduces}{\leadsto}
\newcommand{\mrs}[1]{_{\mbox{\scriptsize #1}}}
\newcommand{\repl}[2]{[#1\leftarrow#2]}

\newcommand{\forlang}[1]{{\it #1}}
\newcommand{\lnk}{\mbox{\ --\ }}
\newcommand{\ass}{\mbox{:\ }}
\newcommand{\llnk}{\mbox{-}}
\newcommand{\lass}{\mbox{:}}

\newcommand{\blmod}{\mbox{$\blacksquare$}}

\newcommand{\tup}{\mbox{$\uparrow$}}
\newcommand{\tdn}{\mbox{$\downarrow$}}

\newcommand{\bnd}{\mbox{$\Uparrow$}}

%%%\newcommand{\conj}{\mbox{$\wedge$}}
\newcommand{\iconj}{\mbox{$\sqcap$}}

%%%\newcommand{\disj}{\mbox{$\vee$}}
\newcommand{\idisj}{\mbox{$\sqcup$}}

\newcommand{\uniq}{\mbox{$\bigwedge$}}
\newcommand{\iuniq}{\mbox{$\bigsqcap$}}

\newcommand{\exiq}{\mbox{$\bigvee$}}
\newcommand{\iexiq}{\mbox{$\bigsqcup$}}
\newcommand{\product}{\mbox{$\bullet$}}

% \newcommand{\perm}{\mbox{$\bigtriangleup$}}

\newcommand{\linimp}{\mbox{$-\!\circ$}}

\newcommand{\ext}{\mbox{$\uparrow$}}
\newcommand{\amod}{\begin{picture}(0,0)\put(0,2){\small$\bigcirc$}\end{picture}\hspace{0.13in}}

\newcommand{\nao}{\mbox{$<$}}
\newcommand{\nau}{\mbox{$>$}}

\newcommand{\naprod}{\mbox{$\stackrel{\diamond}{}$}}

\newcommand{\extract}{\mbox{$\uparrow$}}
\newcommand{\infix}{\mbox{$\downarrow$}}
\newcommand{\dprod}{\mbox{$\odot$}}
\newcommand{\inc}{\mbox{$\circ$}}

\newcommand{\fst}{\mbox{fst}}
\newcommand{\snd}{\mbox{snd}}
\newcommand{\trd}{\mbox{trd}}

%\newcommand{\mybrack}{\mbox{[$\,$]}}
%\newcommand{\antibrack}{\mbox{[\hspace*{0.05in}]$^{-1}$}}
\newcommand{\mybrack}[1]{\mbox{[$\,$#1$\,$]}}
\newcommand{\antibrack}[1]{\mbox{[$\,$#1$\,$]$^{-1}$}}
\newcommand{\contantibrack}[1]{\mbox{[#1]$^{-1}$}}

\newcommand{\nmodels}{\begin{picture}(0,0)\put(0,0){\mbox{$\models$}}\put(2,0){\mbox{/}}\end{picture}\hspace{0.2in}}

\newcommand{\nil}{\mbox{$\epsilon$}}
\newcommand{\exsep}{\vspace{-0.125in}}
\newcommand{\bngen}{\mbox{\ ::=\ }}
\newcommand{\fmodels}{\mbox{$|\!\!\!=$}}
\newcommand{\bmodels}{\mbox{$=\!\!\!|$}}
\newcommand{\add}{\mbox{\small $+$}}
\newcommand{\mconj}{\mbox{$\,\otimes\,$}}
\newcommand{\mdisj}{\mbox{$\,$+$\,$}}
\newcommand{\adisj}{\mbox{$\,\oplus\,$}}
\newcommand{\linneg}{\mbox{$^\bot$}}
%\newcommand{\ng}{\mbox{$^-$}}
\newcommand{\ps}{\mbox{$^+$}}
\newcommand{\comp}{\mbox{$-$}}
\newcommand{\meet}{\mbox{$\sqcap$}}
%\newcommand{\join}{\mbox{$\sqcup$}}
\newcommand{\bottom}{\mbox{$\perp$}}
\newcommand{\mytop}{\mbox{$\top$}}
\newcommand{\gives}{\mbox{$\ \Rightarrow\ $}}
\newcommand{\ent}[1]{\hspace*{0.25in}\begin{minipage}{5.15in}
\hspace*{-0.25in}#1\end{minipage}}
\newcommand{\sect}[1]{{\large\bf #1\ \\}}
\newenvironment{pdisp}
   {\hspace{0.001in}\newline\hspace*{0.33in}\vspace{0in}\begin{minipage}[t]{5.25in}}%
   {\end{minipage}\vspace{0in}\newline}
\newcommand{\ol}{\mbox{/$_l$}}
%%%\newcommand{\ul}{\mbox{\bsl$_l$}}
\newcommand{\orr}{\mbox{/$_r$}}
\newcommand{\ur}{\mbox{\bsl$_r$}}
\newcommand{\addl}{\mbox{$+_l$}}
\newcommand{\addr}{\mbox{$+_r$}}
\newcommand{\addh}{\mbox{$+_h$}}
\newcommand{\lingate}{\mbox{$\,\circ\!-\,$}}
\newcommand{\pcnst}[1]{\mbox{{\bf #1}}}
\newcommand{\scnst}[1]{\mbox{{\bf #1}}}
\newcommand{\pconst}[1]{\mbox{{\bf #1}}}
\newcommand{\lnksm}{\mbox{-}}
\newcommand{\AL}{\mbox{\bf L}}
\newcommand{\LP}{\mbox{\bf LP}}
\newcommand{\NL}{\mbox{\bf NL}}
\newcommand{\gate}{\mbox{\ $\leftarrow$\  }}
\newcommand{\cnj}{\mbox{\ $\wedge$\  }}
\newcommand{\linid}{\mbox{\bf 1}}
\newcommand{\id}{\mbox{$\top$}}
\newcommand{\degree}{\mbox{$^{\mbox{\scriptsize o}}$}}
\newcommand{\ffbox}[1]{\fbox{\vspace*{0.4in}#1}}
%\newcommand{\split}{\mbox{\$}}
\newcommand{\bridge}{\mbox{$^\wedge$}}
\newcommand{\rest}{\mbox{$\uparrow$}}

\newcommand{\demzero}[3]{#1 &
\rule{0cm}{0.5cm}#2
 & #3\\}
\newcommand{\demone}[3]{#1 &
\ \ \begin{tabular}[t]{|l}
\rule{0cm}{0.5cm}#2
\end{tabular}
 & #3\\}
\newcommand{\demoneh}[3]{#1\rule{0cm}{0.5cm} &
\ \ \begin{tabular}{|l}
#2
\\\hline
\end{tabular}
 & #3\\}
\newcommand{\demtwo}[3]{#1 &
\ \ \begin{tabular}[t]{|l}
\ \ 
\begin{tabular}[t]{|l}
\rule{0cm}{0.5cm}#2\\
\end{tabular}
\end{tabular} & #3\\}
\newcommand{\demtwoh}[3]{#1 &
\ \ \begin{tabular}[t]{|l}
\ \rule{0cm}{0.5cm}\ 
\begin{tabular}{|l}
#2\\\hline
\end{tabular}
\end{tabular} & #3\\}
\newcommand{\demthree}[3]{#1 &
\ \ \begin{tabular}[t]{|l}
\ \ \begin{tabular}[t]{|l}
\ \ 
\begin{tabular}[t]{|l}
\rule{0cm}{0.5cm}#2\\
\end{tabular}
\end{tabular}
\end{tabular} & #3\\}
\newcommand{\demthreeh}[3]{#1 &
\ \ \begin{tabular}[t]{|l}
\ \ \begin{tabular}[t]{|l}
\ \rule{0cm}{0.5cm}\ 
\begin{tabular}{|l}
#2\\\hline
\end{tabular}
\end{tabular}
\end{tabular} & #3\\}
