%= %------ Environments -----------------------------------------%
%= 
%= \def\prooflabel{Demonstra\c c\~ao}
%= %newenvironment{proof}{\begin{small}\noindent{\bf\prooflabel:}}{$\Box$\end{small}}
%= 
%= \newenvironment{barra}
%=       {\hrule}
%=       {\hrule}
%= 
%= \newenvironment{aspasquote}{%
%= \setlength{\parindent}{0pt}
%= \setlength{\parskip}{\baselineskip}
%= \begin{quote}\begin{small} ``}%    por \em antes de ``?
%= {'' \end{small}\end{quote}}
%= 
%= \newenvironment{codigo}[1]{\refstepcounter{codigo}
%= \setlength{\parindent}{0pt}
%= \setlength{\parskip}{\baselineskip}
%= \bigskip\hrule\medskip\noindent
%= 	{\bf Exemplo}~\arabic{codigo} (#1)}%
%= {\medskip\hrule\bigskip}
%= 
%= %------ Figuras      -----------------------------------------%
%= 
%= \def\foto#1#2#3#4{%
%= \begin{photo}
%=         \centering
%=         \fbox{\rule{0cm}{#4cm}
%=               \rule{#3cm}{0cm}
%=               \hspace{-3cm} #3 cm x #4 cm}
%=         \caption{#2\label{fot:#1}}
%= \end{photo}
%= }
%= 
%= \def\figuraX#1#2#3{
%=     \begin{figure}
%= 	\centering
%= 	\unitlength=#3
%=         \getPic{#1}
%= 	\caption{#2\label{fig:#1}}
%=     \end{figure}
%= }
%= 
%= \def\figura#1#2 {
%=     \begin{figure}
%= 	\centering
%= 	\getPic{#1}
%= 	\caption{#2\label{fig:#1}}
%=     \end{figure}
%= }
%= 
%= \def\figuraEPS#1#2{
%=     \begin{figure}
%= 	\centering
%= \fbox{\mypsfig{#1}{.75\textwidth}}
%= 	\caption{#2\label{fig:#1}}
%= 	\end{figure}
%= }
%= 
%= \def\especie#1#2{\put(  #1   ){\makebox(0,0){{\bf #2 }}}
%=                \put(  #1   ){\oval(60,40)}}
%= %------              -----------------------------------------%
%= \def\esp{~\\}
%= \def\espaco{~\\~\\}
%= \def\Espaco{{~\\ ~ \\ ~ \\}}
%= \def\screen#1{%\medskip
%=   \begin{center}
%=   \fbox{\begin{minipage}{0.99\textwidth}\small #1 \end{minipage}}
%=   \end{center}\medskip}
%= \def\defbox#1{\medskip
%=   \begin{center}
%=   \fbox{\begin{minipage}{0.9\textwidth}\em\protect{#1}\end{minipage}}
%=   \end{center}}
%= \def\bloco#1
%=     { ~ \\ ~ \\ \ $\Box$ \ \parbox[t]{5in} { {\Huge #1} } \\ ~ \\ }
%= \def\caixa#1{\begin{center}
%= 		      \fbox{~ #1 ~}
%=              \end{center}}
%= \def\boxsep{~\\$\Box$\\~\\}
%= \def\nota#1
%=     { ~ \\ ~ \\ \ {\bf Nota:~} \ \parbox[t]{5in} { #1 } \\ ~ \\ }
%= \def\quoit#1{\begin{quote}
%= 		      {\em #1}
%=              \end{quote}}
%= \def\aspas#1{``#1''}
%= \def\naspas#1{{\footnotesize $\ll$}#1{\footnotesize $\gg$}}
%= 
%= \def\super#1{\mbox{{\scriptsize #1}}}
%= \def\esimo#1{#1${.\kern-.1em}^{\super{o}}$}
%= \def\esimas#1{#1${.\kern-.1em}^{\super{as}}$}
%= \def\esima#1{#1${.\kern-.1em}^{\super{a}}$}
%= \def\abrev#1{${}^{\super{#1}}$}
%= \def\verso{\esimo{v}}
%= \def\no#1{\mbox{n.$\!{}^{\super{o}}$ #1}}
%= \def\nos#1{\mbox{n.$\!{}^{\super{os}}$ #1}}
%= \let\nr=\no
%= 
%= \def\chaveta#1#2#3{\mbox{#1}
%=                    \left\{\begin{array}{l}\mbox{#2}\\ \mbox{#3}
%= 				          \end{array} \right.}
%= \def\first{$1^{st}$}
%= \def\sec#1{s\'ec.\ {\sc #1}}
%= \def\secs#1{s\'ecs.\ {\sc #1}}
%= %\def\second{$2^{nd}$}
%= %\def\third{$3^{rd}$}
%= \def\nth#1{%
%= %                Calculo do resto da dvisao de #1 por 10
%= %                (deve existir este operador no TeX...)
%= %                D := #1; d := 10; x := D;
%= %                x := x / d;
%= %                x := x * d;
%= %                D := D - x;
%= %                id D=1 then D st (first)
%= %                       else if D=2 then D nd (second)
%= %                                   else if D=3 then D rd (third)
%= %                                               else D th
%= \newcount\D\D=#1\newcount\d\d=10\newcount\x\x=\D
%= \divide\x by\d
%= \multiply\x by\d
%= \advance\D by-\x
%= \def\exp{\ifnum\D=1 st
%= \else\ifnum\D=2 nd
%= \else\ifnum\D=3 rd \else th\fi\fi\fi}$#1^{\exp}$}
%= \def\versus{{\em versus\/}}
%= \def\uk#1{`#1'}
%= \def\latim#1{`#1'}
%= \def\abrev#1{${}^{\hbox{\footnotesize #1}}$}
%= \def\no#1{n${.}^{\b{o}}$ #1}
%= \def\nos#1{n${.}^{\b{o}}$s #1}
%= \newcommand{\Nos}{N.\abrev{os}}
%= \newcommand{\No}{N.\abrev{o}}
%= 
%= %------ Matematica   -----------------------------------------%
%= \def\lcb{\left\{}
\def\leftfunc#1#2{%
   \lefteqn{#1} \nonumber && \\ \lefteqn{#2\deff} \nonumber \\ && }
%= \def\botFun{\overline\bot} % bottom
%= \def\bnft#1{~\mattt{#1}~}
%= \def\bnfnt#1{\mathopen{\langle}\matem{#1}\mathclose{\rangle}}
%= \def\bnf#1#2{\bnfnt{#1} & ::= & \begin{array}[t]{ll} #2 \end{array}}
%= \def\bnfor{\asor}
%= \def\const#1{\mathopen{[}#1\mathclose{]}}
%= \def\alt#1#2{#1\mathbin{|}#2}                    % f | g
%= 
%= \def\caso#1#2#3#4{\left\{
%=     \begin{array}{lcl}#1&\Rightarrow&#2\\#3&\Rightarrow&#4\end{array}\right.}
%= \def\nJoin{\Join_{\!\!\!\!n}}
%= \def\coJoin{\stackrel{+}{\Join}}
%= \def\rest#1#2{#1|#2}
%= %------ Matematica -> Basicas --------------------------------%
%= \def\mean#1{\mathopen{[\![}#1\mathclose{]\!]}}
%= \def\comp{\mathbin{\circ}}
%= \def\sat{\mathbin{\mbox{\underline{sat}}}}
%= \def\tuple#1{\mathopen{\langle}#1\mathclose{\rangle}} % <a,b,...z>
%= \def\pexp#1#2{\left\{\begin{array}{lcl} #1 &\Rightarrow& #2 \end{array} \right.}
%= \def\matsc#1{\mbox{\sc #1}}
%= \def\matbf#1{\mbox{\bf #1}}
\def\mattt#1{\mbox{\tt #1}}
%= \def\matem#1{\mbox{{\em #1}}}
%= \def\nrelem#1{{|#1|}}
%= \def\implies{\mathbin\Rightarrow}
%= \def\and{\mathbin\wedge}
%= \def\andif{\mathbin{\wedge \!\!\!.\,}}
%= \def\Z{\mbox{Z$\!\!$Z}}
%= \def\CC{\mbox{C$\!\!\!$C}}
%= \def\R{\mbox{I$\!$R}}
%= \def\N{\mbox{I$\!$N}}
%= %\def\NN{I\! N}                            % Nat numbers
%= %\def\NNZ{I\! N_{0}}                       % Nat0 numbers
\def\deff{\stackrel{\rm def}{=}}          % function definition symbol 
%= \def\func#1{\mbox{\sf #1}}
%= \def\arrow#1{\stackrel{#1}{\rightarrow}} % category theoretic
%=                                          % arrow
%= \def\universal#1#2{\forall #1: #2}
%= \def\existential#1#2{\exists #1: #2}
%= %------ Matematica -> Provas etc -----------------------------%
%= 
%= \def\eqbyx{% NB: devia ser simplesmente eqby{} !!!
%= \\&\updownarrow& \\}
%= 
%= \def\Eq#1{\begin{array}[t]{c}=\\\makebox[0em][c]{{\footnotesize #1}}\end{array}}
%= \def\Eqby#1{\\&\updownarrow&\mbox{{\footnotesize #1}}\\}
%= \def\By#1{\\&&\mbox{{\footnotesize #1}}\\}
%= 
%= \def\eqby#1{%
%= \gdef\@y{#1}\gdef\nada{}
%= \gdef\@x{\ifx\@y\nada\ \else(\ref{#1})\fi}
%= \\&\updownarrow&\mbox{\@x}\\}
%= 
%= \newenvironment{induction}[1]{%
%= \def\base{\item {\em Caso de Base}:~}
%= \def\istep{\item {\em Salto indutivo}:~}
%= \def\step{\item {\em Passo}:~}
%= \def\hyp{\begin{enumerate}\item {\em Hip\'otese de indu\cao}:~}
%= \noindent Prova por indu\cao\ sobre $#1$:
%= \begin{enumerate}}%
%= {\end{enumerate}\end{enumerate}}
%= 
%= %------ Matematica -> Conjuntos ------------------------------%
%= \def\inseg#1{\overline{#1}}
%= \def\pow#1{{\cal P}({#1})}               % P(X)
%= \def\settag#1{{#1}\hbox{-set}}           % #1-set
%= \def\bagtag#1{{#1}\hbox{-bag}}           % #-1bag
%= \def\ZF{| \; }                            % ZF bar 
%= \def\setdef#1#2{\{#1 \asor \;#2\}}             % { f(x) | p(x) }
%= \def\enset#1{\mathopen{ \{ }#1\mathclose{ \} }} % {a,b,...z}
%= \def\st{. \, }                           % "such that"
\def\card#1{{\sf card} \, {#1}}         % card s
%= %------ Matematica -> Listas ---------------------------------%
%= \def\set#1{2^{#1}}                       % 2^X
%= \def\seq#1{{#1}^{\star}}                 % X*
%= \def\listtag#1{{#1}\hbox{-list}}         % #1-list
\def\listdef#1#2{\enlist{ #1 \asor #2}} % < f(x) | x <- l>
%= \let\seqdef=\listdef
%= \def\from{\mathbin{\leftarrow}}
%= \def\len#1{{\sf len} \, {#1}}            % len x
%= \def\len#1{\unary{length}{#1}}
%= \def\head#1{\unary{head}{#1}}
%= \def\tail#1{\unary{tail}{#1}}
%= \let\hd\head
%= \let\tl\tail
%= \def\elems#1{\unary{elems}{#1}}
%= \def\length#1{\unary{length}{#1}}      % elems l
\def\conc{\mathbin{\frown}}
\def\enlist#1{\mathopen{<}#1\mathclose{>}} % <a,b,...z>
\def\seqen#1{\mathopen{<}#1\mathclose{>}}
\def\emptylist{\enlist{}}
%= %------ Matematica -> Funcoes --------------------------------%
%= \def\absf#1{f_{(\ref{#1})}}
%= \def\absi#1{\phi_{(\ref{#1})}}
%= \def\unary#1#2{\def\arg{#2}\def\omisso{}
%=                #1\ifx\arg\omisso\relax\else(#2)\fi}
%= \def\enapp#1#2{\left(\begin{array}{ccccccccc}#1\\#2\end{array} \right)}
\def\plus{\mathbin{\dagger}}
\def\tfunc#1{\longrightarrow {#1}}       % total   funct.
\def\pfunc#1{\hookrightarrow {#1}}        % partial funct.
%= \def\rng#1{\unary{rng}{#1}}               % rng x
%= \def\dom#1{\unary{dom}{#1}}               % dom x
%= \def\mapdef#1#2{\{ #1|\;#2 \}}              % [ x -> f(x) | p(x) ]
%= \def\enmap#1{\mathopen{\{}#1\mathclose{\}}} % [a,b,...z]
%= \def\emptymap{\enmap{~}}
\def\mapdr{\mathbin{|}}
\def\mapds{\mathbin{\setminus}}
%= \def\famdef#1#2{(#1)_{#2}}                  % (f(x))x in S
%= %------ Matematica -> VDMAS ----------------------------------%
%= \def\mk#1{\hbox{mk-}{#1}}                % mk-#1
\def\is#1{\hbox{is-}{#1}}                % is-#1
%= \def\vdmas{sintaxe abstracta em \vdm}
%= \def\asalt#1{\mathopen{[}#1\mathclose{]}} % [ A ]
\def\asor{\mathbin{|}}                    % A | B
%= \def\ascom#1{~~\mbox{/*\matem{#1} */}}
%= \def\Ascom#1#2
%=          {~~\mbox{\begin{minipage}[t]{#1cm}\em/* #2 */\end{minipage}}}
%= \def\pair#1{\tuple{#1}}
%= %------ Matematica -> SETS -----------------------------------%
%= \def\mcup{\mathbin{\oplus}}           % bag union 
%= \def\mcap{\mathbin{\mbox{%
%= \unitlength=.5ex
%= \special{em:linewidth 0.4pt}
%= \linethickness{0.4pt}
%= \begin{picture}(2.00,2.00)
%= \put(0.00,0.00){\makebox(0,0)[cc]{$\cap$}}
%= \put(0.00,0.00){\circle{4.00}}
%= \end{picture}
%= }}}
%= 
%= \let\Mcup\bigoplus                    % bag Union 
%= \let\mminus\ominus                    % bag difference
%= \let\msubseteq\subseteq               % bag inclusion
%= \def\model#1{{\cal {#1}} : \Sigma \rightarrow Sets}
%= \def\assina#1{\Sigma_{#1}}
%= \def\Assina#1{\Sigma_{#1}:\Omega_{#1}\rightarrow S^{\star}_{#1}\times S_{#1}}
%= \def\lred#1#2{\unlhd_{#1}^{#2}}
%= %------ Matematica -> Outras ---------------------------------%
%= \def\traco{\esp\mbox{}\hrulefill\mbox{} \\*}
%= \def\mapp#1{\stackrel{m}\rightarrow {#1}}  % -m->
%= \def\brel#1{\stackrel{m}\leftrightarrow {#1}}  % <-m->
%= \def\orif{\mathbin{\dot{\vee}}}
%= \def\post#1{\hbox{post-}{#1}}              % post-#1
%= \def\pre#1{\hbox{pre-}{#1}}                % pre-#1
%= \def\inv#1{\hbox{inv-}{#1}}                % inv-#1
%= %------ CCS          -----------------------------------------%
%= \def\paralel#1#2{\prod_{#1}#2}                  %  | i=1,n
%= \def\succ#1{\stackrel{\rm #1}{\rightarrow}}  % - a - > 
%= \def\atimes{\mathbin{\parallel}}             % a . P
%= \def\athen{\mathbin{.}}                      % a . P
%= \def\then{\mathbin{:}}                       % a : P
%= \def\restr{\mathbin{\uparrow}}               % P | A
%= \def\obs{\mathbin{\sim}}                     % P ~ Q
%= \def\aobs{\mathbin{\approx}}                 % P ~ Q
%= \def\ainv#1{\overline{#1}}                   % ~ a 
%= \def\fix#1{\underline{fix}~#1}               % fix X
%= %------ Matematica -> Diagramas --------------------------------%
%= \def\diag#1#2#3#4#5#6#7#8
%=     {\begin{picture}(200,95)(0,0)
%=      \def\fAbst{#8}\def\fConc{#6}\def\omissa{}
%=      \put(55,80){\makebox(0,0)[r]{$#1$}}
%=      \put(55,20){\makebox(0,0)[rt]{$#2$}}
%=      \put(125,20){\makebox(0,0)[lt]{$#3$}}
%=      \put(125,80){\makebox(0,0)[l]{$#4$}}
%= % seta horizontal inferior
%=      \ifx\fConc\omissa\relax
%=      \else\put(65,15){\vector(1,0){50}}\put(90,10){\makebox(0,0){$#6$}}\fi
%= % seta horizontal superior
%=      \ifx\fAbst\omissa\relax
%=      \else\put(65,80){\vector(1,0){50}}\put(90,87){\makebox(0,0){$#8$}}\fi
%= %
%=      \put(50,26){\vector(0,1){48}}
%=      \put(45,50){\makebox(0,0)[r]{$#5$}}
%= %
%=      \put(130,26){\vector(0,1){48}}
%=      \put(135,50){\makebox(0,0)[l]{$#7$}}
%=      \end{picture}}
%= 
%= % refdiag usa global vars a e b
%= \newcount\xa\xa=87
%= \newcount\xb\xb=167
%= \def\refdiag#1#2#3#4#5#6#7#8{%
%= \def\nil{}\def\um{#1}
%=     \begin{picture}(200,70)(0,0)
%= \ifx\um\nil\relax\else
%=     \put(\xa,5){\makebox(0,0){$#6$}}
%=     \put(\xa,65){\makebox(0,0){$#1$}}
%=     \put(\xa,12){\vector(0,1){47}}
%= \advance \xa by -5
%=      \put(\xa,35){\makebox(0,0)[r]{$#4$}}
%= \fi
%=      \put(\xb,5){\makebox(0,0){$#8$}}
%=      \put(\xb,65){\makebox(0,0){$#3$}}
%=      \put(\xb,12){\vector(0,1){47}}
%= \advance \xb by 5
%=      \put(\xb,35){\makebox(0,0)[l]{$#5$}}
%= %
%=      \put(105,5){\vector(1,0){50}}
%=      \put(130,0){\makebox(0,0){$#7$}}
%=      \put(105,65){\vector(1,0){50}}
%=      \put(130,70){\makebox(0,0){$#2$}}
%=      \end{picture}
%= }
%= 
%= 
%= % epp!
%= %           \def\enapp#1#2{\left(\begin{array}{c}#1\\#2\end{array} \right)}
%=             \def\dbuf{\setlength{\unitlength}{.5\unitlength} 
%=                       \begin{picture}(40,40)(0,0)
%=                       \put(20, 0){\line(0,1){10}}
%=                       \put(20,30){\line(0,1){10}}
%=                       \put(40,20){\line(-1,0){15}}
%=                       \put(10,30){\line( 1,0){20}}
%=                       \put(10,30){\line(1,-2){10}}
%=                       \put(20,10){\line(1, 2){10}}
%=                       \end{picture}}
%=             \def\rbuf{\setlength{\unitlength}{.5\unitlength} 
%=                       \begin{picture}(40,40)(0,0)
%=                       \put(0,20){\line(1,0){10}}
%=                       \put(30,20){\line(1,0){10}}
%=                       \put(20,0){\line(0,1){15}}
%=                       \put(10,10){\line(0,1){20}}
%=                       \put(10,10){\line(2,1){20}}
%=                       \put(10,30){\line( 2,-1){20}}
%=                       \end{picture}}
%=            \def\ne#1#2{\begin{picture}(10,30)(0,0)
%=                       \put( 0,#2){\line(1,0){#1}}
%=                       \put(#1, 0){\line(0,1){#2}}
%=                     % \put(10, 0){\circle*{2.5}}
%=                       \end{picture}}
%=            \def\no#1#2{\begin{picture}(#1,#2)(0,0)
%=                       \put( 0, 0){\line(0,1){#2}}
%=                       \put( 0,#2){\line(1,0){#1}}
%=                     % \put( 0, 0){\circle{2.5}}
%=                       \end{picture}}
%=           \def\se#1#2{\begin{picture}(10,30)(0,0)
%=                       \put( 0, 0){\line(1,0){#1}}
%=                       \put(#1, 0){\line(0,1){#2}}
%=                     % \put( 0,30){\circle*{2.5}}
%=                       \end{picture}}
%=           \def\so#1#2{\begin{picture}(10,30)(0,0)
%=                       \put( 0, 0){\line(0,1){#2}}
%=                       \put( 0, 0){\line(1,0){#1}}
%=                     % \put( 0,30){\circle*{2.5}}
%=                       \end{picture}}
%=           \def\lpin#1{\begin{picture}(50,17)(0,0)
%=                       \put(50,0){\vector(-1,0){50}}
%=                       \put(5, 7){\makebox(0,0)[l]{\footnotesize $#1$}}
%=                       \end{picture}}
%=          \def\lpout#1{\begin{picture}(50,17)(0,0)
%=                       \put(50,0){\vector(-1,0){50}}
%=                       \put(45, 7){\makebox(0,0)[r]{\footnotesize $#1$}}
%=                       \end{picture}}
%=           \def\rpout#1{\begin{picture}(50,17)(0,0)
%=                       \put(0,0){\vector(1,0){50}}
%=                       \put(5, 7){\makebox(0,0)[l]{{\footnotesize $#1$}}}
%=                       \end{picture}}
%=           \def\rpin#1{\begin{picture}(50,17)(0,0)
%=                       \put(0,0){\vector(1,0){50}}
%=                       \put(45, 7){\makebox(0,0)[r]{{\footnotesize $#1$}}}
%=                       \end{picture}}
%=           \def\int#1{\begin{picture}(50,80)(0,0)
%=                      \put(25,40){\makebox(0,0){\footnotesize #1}}
%=                      \put(0,0){\line(1,0){50}}
%=                      \put(0,80){\line(1,0){50}}
%=                      \put(50,0){\line(0,1){80}}
%=                      \put(0,0){\line(0,1){80}}
%=                      \end{picture}}
%= \def\icu#1#2#3#4#5#6#7{\begin{picture}(150,80)(0,0)
%=                      \put(50,0){\int{$#1$}}
%=                      \put(0,70){\rpin{#2}}
%=                      \put(0,40){\rpin{#3}}
%=                      \put(0,10){\rpin{#4}}
%=                      \put(100,70){\lpin{#5}}
%=                      \put(100,40){\lpin{#6}}
%=                      \put(100,10){\rpout{#7}}
%=                      \end{picture}}
%= \def\icd#1#2#3#4#5#6#7#8{\begin{picture}(150,80)(0,0)
%=                      \put(50,0){\int{$#1$}}
%=                      \put(0,70){\rpin{#2}}
%=                      \put(0,50){\rpin{#3}}
%=                      \put(0,30){\rpin{#4}}
%=                      \put(0,10){\rpin{#5}}
%=                      \put(100,70){\rpin{#6}}
%=                      \put(100,40){\rpin{#7}}
%=                      \put(100,10){\lpin{#8}}
%=                      \end{picture}}
%= \def\isd#1#2#3#4#5#6#7#8#9{\begin{picture}(150,80)(0,0)
%=                      \put(50,0){\int{$#1$}}
%=                      \put(0,70){\rpin{#2}}
%=                      \put(0,50){\rpin{#3}}
%=                      \put(0,30){\rpin{#4}}
%=                      \put(0,10){\rpin{#5}}
%=                      \put(100,70){\lpin{#6}}
%=                      \put(100,50){\lpin{#7}}
%=                      \put(100,30){\rpout{#8}}
%=                      \put(100,10){\rpout{#9}}
%=                      \end{picture}}
%=     \def\idu#1#2#3#4{\begin{picture}(150,80)(0,0)
%=                      \put(50,0){\int{$#1$}}
%=                      \put(0,70){\rpin{#2}}
%=                      \put(0,10){\rpin{#3}}
%=                      \put(100,40){\rpin{#4}}
%=                      \end{picture}}
%=   \def\idd#1#2#3#4#5{\begin{picture}(150,80)(0,0)
%=                      \put(50,0){\int{$#1$}}
%=                      \put(0,70){\rpin{#2}}
%=                      \put(0,10){\rpin{#3}}
%=                      \put(100,70){\rpout{#4}}
%=                      \put(100,10){\rpout{#5}}
%=                      \end{picture}}
%= \def\idt#1#2#3#4#5#6{\begin{picture}(150,80)(0,0)
%=                      \put(50,0){\int{$#1$}}
%=                      \put(0,70){\rpin{#2}}
%=                      \put(0,10){\rpin{#3}}
%=                      \put(100,70){\rpout{#4}}
%=                      \put(100,40){\rpout{#5}}
%=                      \put(100,10){\rpout{#6}}
%=                      \end{picture}}
%= \def\iqd#1#2#3#4#5#6#7{\begin{picture}(150,80)(0,0)
%=                      \put(50,0){\int{$#1$}}
%=                      \put(0,70){\rpin{#2}}
%=                      \put(0,40){\rpin{#3}}
%=                      \put(0,10){\rpin{#4}}
%=                      \put(100,70){\rpout{#5}}
%=                      \put(100,40){\rpout{#6}}
%=                      \put(100,10){\lpin{#7}}
%=                      \end{picture}}
%= \def\iqt#1#2#3#4#5#6#7#8{\begin{picture}(150,80)(0,0)
%=                      \put(50,0){\int{$#1$}}
%=                      \put(0,70){\rpin{#2}}
%=                      \put(0,50){\rpin{#3}}
%=                      \put(0,30){\rpin{#4}}
%=                      \put(0,10){\rpin{#5}}
%=                      \put(100,70){\rpout{#6}}
%=                      \put(100,40){\rpout{#7}}
%=                      \put(100,10){\rpout{#8}}
%=                      \end{picture}}
%= \def\iqq#1#2#3#4#5#6#7#8#9{\begin{picture}(150,80)(0,0)
%=                      \put(50,0){\int{$#1$}}
%=                      \put(0,70){\rpin{#2}}
%=                      \put(0,50){\rpin{#3}}
%=                      \put(0,30){\rpin{#4}}
%=                      \put(0,10){\rpin{#5}}
%=                      \put(100,70){\rpout{#6}}
%=                      \put(100,50){\rpout{#7}}
%=                      \put(100,30){\rpout{#8}}
%=                      \put(100,10){\rpout{#9}}
%=                      \end{picture}}
%=   \def\itu#1#2#3#4#5{\begin{picture}(150,80)(0,0)
%=                      \put(50,0){\int{$#1$}}
%=                      \put(0,70){\rpin{#2}}
%=                      \put(0,40){\rpin{#3}}
%=                      \put(0,10){\rpin{#4}}
%=                      \put(100,40){\rpout{#5}}
%=                      \end{picture}}
%=   \def\itd#1#2#3#4#5#6{\begin{picture}(150,80)(0,0)
%=                      \put(50,0){\int{$#1$}}
%=                      \put(0,70){\rpin{#2}}
%=                      \put(0,40){\rpin{#3}}
%=                      \put(100,10){\lpin{#4}}
%=                      \put(100,70){\rpout{#5}}
%=                      \put(  0,10){\lpout{#6}}
%=                      \end{picture}}
%=   \def\itt#1#2#3#4#5#6#7{\begin{picture}(150,80)(0,0)
%=                      \put(50,0){\int{$#1$}}
%=                      \put(0,70){\rpin{#2}}
%=                      \put(100,40){\lpin{#3}}
%=                      \put(0,40){\rpin{#4}}
%=                      \put(100,70){\rpout{#5}}
%=                      \put(100,10){\rpout{#6}}
%=                      \put(0,10){\lpout{#7}}
%=                      \end{picture}}
%=   \def\iud#1#2#3#4{\begin{picture}(150,80)(0,0)
%=                      \put(50,0){\int{$#1$}}
%=                      \put(0,40){\rpin{#2}}
%=                      \put(100,70){\rpout{#3}}
%=                      \put(100,10){\rpout{#4}}
%=                      \end{picture}}
%= 
%= %
%= % Pretty-Print macros and definitions
%= %

%\def\KEY#1{\underline{#1}}
\def\KEY#1{\mathbf{#1}}
\def\LET{\begin{array}[t]{l@{}l}\KEY{let}&\begin{array}[t]{l}}
\def\IN{\end{array}\\\KEY{in}&\begin{array}[t]{l}}
\def\TEL{\end{array}\end{array}}

%\def\POST{\begin{array}[t]{ll}p\underline{ost}&\begin{array}[t]{l}}
\def\POST{\begin{array}[t]{ll}\KEY{post}&\begin{array}[t]{l}}
\let\TSOP=\TEL

%\def\PRE{\begin{array}[t]{ll}p\underline{re}&\begin{array}[t]{l}}
\def\PRE{\begin{array}[t]{ll}\KEY{pre}&\begin{array}[t]{l}}
\let\ERP=\TEL

\def\OTHERWISE{\KEY{else}}
\def\CASE{\left\{\begin{array}{rcl}}
\def\VALUE{&\Rightarrow&}
\def\ESAC{\end{array}\right.}

\def\PROD{\begin{array}[t]{rclc}}
\def\TYPE{&:&}
\def\NEXT{&\times \\}
\def\DORP{\end{array}}

\def\B#1#2#3{\begin{array}[t]{@{~}l}\hspace{-1mm}\KEY{#1}~#2\\\Ab{#3}\end{array}}

\def\Aif#1{\begin{array}[t]{@{}l@{~}l}\KEY{if}&\left\{\begin{array}{@{}r@{~\Rightarrow~}l}#1\end{array}\right.\end{array}} %% JJ not tested
\def\Afor#1#2{\B{foreach}{#1}{#2}}
\def\Awhile#1#2{\B{while}{#1}{#2}}
\def\Afun#1#2{\B{Fun}{#1}{#2}}
\def\Ab#1{\left\{\begin{array}{@{}l}#1\end{array}\right.}
\def\Av{&\Rightarrow&}
\def\Aret#1{\KEY{ret:}~#1}
\def\Aat#1#2{#1\leftarrow#2}
\def\Acom#1{[\mbox{#1}]}
\def\Asig#1#2{\left(\begin{array}{r@{~:~}l}#1 \end{array}\right):#2}
\def\Apar#1#2{#1 & #2\\}
\def\Alet#1#2{\LET #1 \IN #2 \TEL}

\long\def\COND#1#2#3{
\left\{\begin{array}{rcl}#1~&\Rightarrow&#2\\\neg(#1)&\Rightarrow&#3\end{array}
\right.}

%= \def\CONDX#1#2#3#4{
%= \lcb\begin{array}{rcl}#1~&\Rightarrow&#2\\#3&\Rightarrow&#4\end{array}
%= \right.}

%= \def\IF{\begin{array}[t]{l}if~~}
%= \def\If{~if~}

%= \def\THEN{\\ then~~}
%= \def\ThEN{~then~}

%= \def\ELSE{\\ else~~}
%= \def\ElSE{~else~}

%= \def\FI{\end{array}}
%= \def\Fi{}
%= 
%= \def\true{V}
%= \def\false{F}
%= 
%= \def\ORS{\begin{array}[t]{ll}}
%= \def\OR{&\vee\\}
%= \def\SRO{\end{array}}
%= 
%= \def\IFP{\begin{array}[t]{l}(if~~}
%= \def\FIP{)\end{array}}
%= 
%= \def\WHILE{\begin{array}[t]{l}while~~}
%= 
%= \def\WHILEP{\begin{array}[t]{l}(while~~}
%= \def\ODP{)\end{array}}
%= 
%= \def\DO{\\ do~~}
%= 
%= \def\OD{\end{array}}
%= 
%= \def\NEW{new~~}
%= 
\def\COMP#1#2{#1 \circ #2}
%= 
%= \def\ID#1{1_{#1}}
%= 
%= \def\CST#1{\overline{#1}}

\def\INV#1{inv-(#1)}

\def\LAMBDA#1{\lambda(#1)}

%= \def\MODEL#1{\noindent\mbox{\Large Model #1}\\\\}
%= 
%= \def\STATE#1#2{\noindent\mbox{\Large State} $#1:#2$\vskip 2em}
%= 
%= \def\INCLUDE#1{\noindent\mbox{\large include #1}\\\\}

\def\TRUE{true}
\def\FALSE{false}

%= %input{psfig}
%= 
%= \def\epsBox#1#2{ \[ \fbox{\mypsfig{#2}{#1}} \] }
%= \def\picBox#1#2{{\unitlength=#1 \[ \mbox{\getPic{#2}} \] }}
%= 
%= %newcount\ll \ll=0 % listlevel em lista
%= %renewenvironment{itemize}{%
%= %global\advance\ll by 1
%= %typeout{;; baselineskip=\number\baselineskip}
%= %typeout{;; listlevel=\number\ll}
%= %begin{list}{$\bullet$}{\leftmargin 1em
%= %                \labelwidth .5em
%= %                \labelsep .5em
%= %                \rightmargin 0em
%= %                \parsep .4ex
%= %                \itemsep\z@
%= %                \listparindent 0em}}{\end{list}\global\advance\ll by -1
%= %typeout{;; listlevel=\number\ll}}
%= 
%= \newenvironment{solucao}[1]{%
%= \espaco \begin{small}{\bf Resolu\c c\~ao \ref{ex:#1}}:~}%
%= {$\Box$\end{small}}
%= 
%= 
%= %\def\SORTS{\traco{\noindent\rule[-.4em]{0mm}{2.1em}}{\Large\sc Sorts}\traco\\[1em]}
%= %\def\OPERS{\traco{\noindent\rule[-.4em]{0mm}{2.1em}}{\Large\sc Operations}\traco\\[1em]}
%= \def\SORTS{{\noindent\rule[-.4em]{0mm}{2.1em}}{\Large\sc Sorts}\traco}
%= \def\OPERS{\vskip 2em {\noindent\rule[-.4em]{0mm}{2.1em}}{\Large\sc Operations}\traco}
%= 
%= \def\n#1{$\backslash$n#1}

\def\jjff#1#2{#1 \rightharpoonup #2}
\def\jjset#1{ set(#1) }
\def\jjseq#1{ #1^* }
\def\jjprod#1#2{#1 \times #2}
\def\jjalt#1#2{#1 + #2}
\def\jjfunc#1#2{#1 \rightarrow #2}
%\def\jjany{any}
%\def\jjnil{\perp}
\def\jjnil{\mbox{\textbf{1}}}
\def\jjany{\mbox{\textbf{any}}}

\def\traco{\addvspace{3mm}}
\def\SORTS{}
\def\INV#1{inv (#1)}
\def\OPERS{\addvspace{1mm}}
\def\cong{=}
%\def\SORTS{\esp\mbox{}\hrulefill\mbox{} \\*}
%\def\OPERS{\esp\mbox{}\hrulefill\mbox{} \\*}
\def\set#1{set(#1)}
\def\STATE#1#2{
 \addvspace{1mm}
 \mbox{\textbf{State} } $#1:#2$

}

