%------              -----------------------------------------%
\def\esp{~\\}
%------ 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 -> 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\pfunc#1{\rightharpoonup {#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
%
% Pretty-Print macros and definitions
%
\def\LET{\hspace{-2mm}\begin{array}[t]{ll}\underline{let}&\hspace{-2mm}\begin{array}[t]{l}}
\def\IN{\end{array}\\\underline{in}&\hspace{-2mm}\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&#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{\underline{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}

\def\epsBox#1#2{ \[ \fbox{\mypsfig{#2}{#1}} \] }
\def\picBox#1#2{{\unitlength=#1 \[ \mbox{\getPic{#2}} \] }}

\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}