%------------------------ jno.mac -----------------------------------------
%\input{jno-dmac.sty}
\def\D{\jnowarning{DVI}}
\long\def\resolucao#1{%
\espaco\footnoterule\noindent{\sc Resolu\cao}: #1 $\Box$}
%------ Controlo de textualidade -------------------------------%
\def\jnowarning#1{\typeout{JNO Warning: #1 - document page [\thepage]}}
\def\F{%.......................... falta ......................................
.\dotfill .\\ .\dotfill .\\ .\dotfill .\\ .\dotfill .\\ .\dotfill .\\ }
\def\anterior{anterior\typeout{Warning:jno:anterior!}}
%------ Dados pessoais -----------------------------------------%
\def\email{email: jno@di.uminho.pt}
\def\mywww{URL: http://www.di.uminho.pt/\~{ }jno/}
\def\fax{Fax: +351~53~612954}
\def\edi{Dept.\ de Inform\'atica\\
Universidade do Minho,\\
Estrada de Gualtar \\
4700 Braga}
\def\ediinesc{DI/INESC\\
Universidade do Minho,\\
Gualtar,\\
4700 Braga}
\def\ecces{C.C.E.S.\\
Universidade do Minho,\\
Estrada de Gualtar \\
4700 Braga}
%------ Abreviaturas -------------------------------------------%
\def\tad#1{{\sf TAD#1}}
\def\sw{software}
\def\Sw{Software}
\def\hw{hardware}
\def\Hw{Hardware}
\def\pdecl{programa\c{c}\~{a}o decla\-rativa}
\def\ef{especifica\c{c}\~{a}o formal}
\def\pestr{Programa\c{c}\~{a}o Estruturada}
\def\pFunc{Programa\c{c}\~{a}o Funcional}
\def\Cc{Ci\^{e}ncias da Computa\c{c}\~{a}o}
\def\etal{{\em et al}}
%------ Linguagens ---------------------------------------------%
\def\sets{{\sc Sets}}
\def\case{{\sc Case}}
\def\sour{{\sc Sour}}
\def\C{{\sc C}}
\def\clear{{\sc Clear}}
\def\camila{{\sc Camila}}
\def\setcalc{{\sc Sets}}
\def\eril{{\sc Eril}}
\def\foops{{\sc Foops}}
\def\lisp{{\sc Lisp}}
\def\xlisp{{\sc Xlisp}}
\def\msdos{{\sc Ms/dos}}
\def\obj{{\sc Obj}}
\def\pebble{{\sc Pebble}}
\def\oblog{{\sc Oblog}}
\def\pascal{{\sc Pascal}}
\def\plone{{\sc Pl/1}}
\def\fortran{{\sc Fortran}}
\def\prolog{{\sc Prolog}}
\def\sml{{\sf Standard ML}}
\def\sperry{{\sf UNISYS}}
\def\hitex{{\sc Hitex}}
\def\smalltalk{{\sc Smalltalk}}
\def\mac{{\sc Macintosh}}
\def\unix{{\sc Unix}}
\def\csp{{\sc Csp}}
\def\ccs{{\sc Ccs}}
\def\vdm{{\sc Vdm}}
\def\meta{{\sc Meta-iv}}
\def\z{{\sc Z}}
\def\metoo{{\sc Me-too}}
\def\xmetoo{{\sc Xmetoo}}
\def\yarpt{{\sc Yarpt}}
%------ Revistas ---------------------------------------------%
\def\journal#1#2{%
\def\omissa{}\def\ref{#2}\underline{#1}\ifx\ref\omissa{}\relax\else~#2:\fi}
\def\acm{\journal{ACM}{}}
\def\cacm#1{\journal{CACM}{#1}}
\def\jacm#1{\journal{JACM}{#1}}
\def\jcss#1{\journal{JCSS}{#1}}
\def\lncs#1{\journal{LNCS}{#1}}
\def\tcs#1{\journal{TCS}{#1}}
%------ Instituicoes -----------------------------------------%
\def\aic{{\sf AIC}}
\def\adb{{\sc Adb/Um}}
\def\cpce{{\sf CPCE}}
\newcommand{\nig}{{\sf NIG}}
\newcommand{\cium}{{\sf CIUM}}
\def\um{{\sc U.Minho}}
\def\inic{{\sf INIC}}
\def\inesc{{\sc Inesc}}
%\def\fundetec{{\sc \fundetec}}
\def\jnict{{\sc Jnict}}
\def\pmct{{\sc Pmct}}
\def\gdcc{{\sc Gdcc}}
\def\cces{{\sf CCES}}
\def\lig{{\sc LIG}}
\def\leei{{\sc Leei}}
\def\lesi{{\sc Lesi}}
\def\lmcc{{\sc Lmcc}}
\def\Lesi{Licenciatura em Engenharia de Sistemas e Inform\'atica}
\def\Lmcc{Licenciatura em Ma\-te\-m\'a\-ti\-ca e Ci\^encias da Computa\c c\~ao}
\def\ibM{{\sf IBM}} % a eliminar
\def\ibm{{\sc Ibm}}
\def\eid{{\sf EID}}
\def\tm#1{{\sc #1}\abrev{{\scriptsize TM}}}
%------ 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\cao{\c{c}\~ao}
\def\coes{\c{c}\~oes}
\def\ii{\'{\i}}
\def\feira#1{\ifnum #1=7 S\'abado\else\ifnum #1=1 Domingo\else\esima{#1}~feira\fi\fi}
\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\\#3&\Rightarrow\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}} %
\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{>}} %
% \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\LET{\begin{array}[t]{ll}\underline{let}&\begin{array}[t]{l}}
\def\IN{\end{array}\\\underline{in}&\begin{array}[t]{l}}
\def\TEL{\end{array}\end{array}}
\def\POST{\begin{array}[t]{ll}p\underline{ost}&\begin{array}[t]{l}}
\let\TSOP=\TEL
\def\PRE{\begin{array}[t]{ll}p\underline{re}&\begin{array}[t]{l}}
\let\ERP=\TEL
\def\OTHERWISE{\underline{otherwise}}
\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}}
\long\def\COND#1#2#3{
\left\{\begin{array}{rcl}#1~&\Rightarrow\\\neg(#1)&\Rightarrow\end{array}
\right.}
\def\CONDX#1#2#3#4{
\lcb\begin{array}{rcl}#1~&\Rightarrow\\#3&\Rightarrow\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}\\\\}
%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}