%\newtheorem{theorem}{Theorem}[section]
%\newtheorem{definition}{Definition}[section]
%\newtheorem{notation}[theorem]{Notation}
%\newtheorem{lemma}[theorem]{Lemma}
%\newtheorem{problem}[theorem]{Problem}
%\newtheorem{fact}[theorem]{Fact}
\newtheorem{rem}[theorem]{}
%\newtheorem{claim}[theorem]{Claim}
%\newtheorem{proposition}[theorem]{Proposition}
%\newtheorem{criterion}[theorem]{Criterion}
%\newtheorem{exercise}[theorem]{Exercise}
%\newtheorem{remark}[theorem]{Remark}
%\newtheorem{corollary}[theorem]{Corollary}
%\newtheorem{example}[theorem]{Example}
%\newenvironment{proof}{\begin{trivlist}\item[]\hspace{\parindent}{\em Proof.}}
%                      {\hfill \rule{.2em}{.2em}\end{trivlist}}

                    

\newcommand{\at}[3]{{\tt at } \; #1 \; {\tt use }\;  #2 \; {\tt else }\; #3}
\newcommand{\bat}[2]{{\tt at } \; #1 \; {\tt use }\;  #2}
\newcommand{\nat}[4]{{\tt at } \; #1:(#2) \; {\tt use }\;  #3 \; {\tt else }\; #4}
\newcommand{\match}[2]{{\sf match}(#1,#2)}
\newcommand{\MATCH}[2]{{\sf MATCH}(#1,#2)}
\renewcommand\MATCH[3]{{\sf MATCH}(#1,#2,#3)}
\newcommand{\rew}{\rightarrow}
\newcommand{\Rew}{\Rightarrow}
\newcommand{\none}{{\tt fail}}
\newcommand{\ematch}[3]{@(#1,#2,#3)}
\newcommand{\id}{{\tt id}}
\renewcommand{\l}{\lambda}
\newcommand{\sub}[2]{#1\{#2\}}
\newcommand{\isub}[2]{\{\vec{#1}/\vec{#2}\}}
\newcommand{\imut}[2]{[\vec{#1}/\vec{#2}]}
\newcommand{\simut}[2]{[\l #1/\l #2]}
\newcommand{\sisub}[2]{\{#1/#2\}}
\newcommand{\repl}[2]{[\bind{#1} / \bind{#2}]}
\newcommand{\psub}[2]{#1/#2}
\newcommand{\bnf}{\;|\;}
%\newcommand{\wf}[1]{WF(#1)}
\newcommand{\bv}[1]{{\sf bv}(#1)}
\newcommand{\mv}[1]{{\sf mv}(#1)}
\newcommand{\fv}[1]{{\sf fv}(#1)}
\newcommand{\ov}[1]{ov(#1)}
\newcommand{\bal}[1]{bal(#1)}
\newcommand{\var}[1]{{\sf var}(#1)}
\newcommand{\lfv}[1]{lfv(#1)}
\newcommand{\lbv}[1]{lbv(#1)}
\newcommand{\bind}[1]{\lambda  #1}
\newcommand{\set}[1]{\{ #1 \}}
\newcommand{\unionsub}{\sqcup}
\newcommand{\app}[2]{#1 \; #2}
\newcommand{\ds}[2]{\cdot \; #1 \; #2}
\newcommand{\tds}[3]{\cdot^{#1} \; #2 \; #3}
\newcommand{\subterm}{\triangleleft}
\newcommand{\pr}{\gg}
\newcommand{\R}{{\cal R}}
\newcommand{\blinear}{blinear}
\newcommand{\flinear}{flinear}
\newcommand{\linearfv}{linearfv}
\newcommand{\eqalpha}{=_{\alpha}}
\newcommand{\pgg}{\gg\!\!\gg}
\newcommand{\dom}[1]{{\sf dom}(#1)}
\newcommand{\binddom}{binddom}
\newcommand{\im}{im}
\newcommand{\Gam}{\Gamma}
\newcommand{\Del}{\Delta}
\newcommand{\wf}{{\bf wf}}
\newcommand{\ws}{{\bf ws}}
\newcommand{\sep}{\hspace{.5cm}}
\newcommand{\ctxt}[1]{ctxt(#1)}
\newcommand{\weak}[2]{{\sf wk}(#1,#2)}
\long\def\ignore#1{\relax}
\newcommand{\sm}{\setminus}
\newcommand{\ems}{ \{ \} }
\newcommand{\avoid}[2]{{\sf avoid}(#1,#2)}
\newcommand{\daniele}[1]{$[$ {\large \bf Change daniele:} $]$ #1}
\newcommand{\changed}[2]{\daniele{{\bf #2}}}
%\newcommand{\changed}[2]{#1}
\newcommand{\commentd}[1]{$[${\bf Comment daniele: #1}$]$}
%\newcommand{\commentd}[1]{}
\newcommand{\barry}[1]{$[$ {\large \bf Change barry:} $]$ #1}
\newcommand{\changeb}[2]{\barry{{\bf #2}}}
%\newcommand{\changeb}[2]{#2}
\newcommand{\commentb}[1]{$[${\bf Comment barry: #1}$]$}
%\newcommand{\commentb}[1]{}
\newcommand{\ms}[2]{#1[#2]}
\newcommand{\default}{\mbox{{\tt def}}}
\newcommand{\tra}[1]{{\tt T}(#1)}
\newcommand{\traw}[1]{{\tt W}(#1)}
\def\UpdateSalary{\mbox{{\sf update-salary}}}

\def\CEqual{\mbox{{\sf c-equal}}}
\def\elimc{\mbox{{\sf elim-c}}}
\def\gelim{\mbox{{\sf elim}}}
%%%%%%%%%%%%%%%%%%%%\renewcommand{\to}{\Rightarrow}
\def\Charac{\mbox{{\sf charact}}}
\def\emptyqueue{\mbox{\sf empQ}}
\def\cqueue{\mbox{\sf consQ}}
%\def\insert{\mbox{\sf insert}}
\def\lastqueue{\mbox{\sf lastQ}}
\def\winner{\mbox{{\sf Winner}}}
\def\loser{\mbox{{\sf Loser}}}
\def\game{\mbox{{\sf game}}}
\def\factorial{\mbox{{\sf fact}}}
\def\timest{\mbox{{\sf times2}}}
\newcommand{\eqdef}{\ensuremath{\stackrel{\rm def}{=}}}

\def\FindFred{{\sf findFred}} % functions  with Lower case letters
\def\Person{{\sf Person}} % constants with Upper case letters
\def\Salary{{\sf Salary}} % constants with Upper case letters

\def\phiwhnf{$\Phi$-weak head normal form}

\renewcommand\at[3]{#2 \to_{#1} #3}
%\newcommand\vmatch[2]{\{\!\!\{#1/ #2\}\!\!\}}
\newcommand\vmatch[2]{\{#1/ #2\}}
\newcommand\vvmatch[2]{\{#1/\!\!/ #2\}}
\renewcommand\match[3]{\vmatch{#1}{#2}_{#3}}
\renewcommand\none{{\sf none}}
\newcommand\es{\phi}
\newcommand\restrict[2]{#1_{#2}}
%\renewcommand\MATCH[3]{\restrict{\match {#1} {#2} \es} {#3}}
%\renewcommand\match[3]{{\sf match}(#1,#2,#3)}
\newcommand\pmatch[2]{{\sf pmatch}(#1,#2)}
\renewcommand{\rew}{\longrightarrow}
\newcommand\Equal{{\sf equal}}
\newcommand\True{{\sf true}}
\newcommand\False{{\sf alse}}
\newcommand\Nil{{\sf nil}}
\newcommand\Cons{{\sf cons}}
\newcommand\Singleton{{\sf singleton}}
\newcommand\Update{{\sf update}}
\def\wild{\bullet}
\def\LessThanOrEqual{{\sf lessOrEqual}}


\def\bind{\theta}
\def\constructors{\gamma}

\def\Department{{\sf Department}}

\newcommand{\nil}{[ \; ]}

%\renewcommand{\paragraph}[1]{\subsection{#1}}
\renewcommand{\example}[1]{{\vspace{6pt}\noindent \bf #1}}

\def\Undefined{{\rm undefined}}

\def\If{{\sf if}}


%%%%%%%% MACRO DAN %%%%%%%%%%%

\renewcommand{\paragraph}[1]{\bigskip \noindent{\bf #1}}
\newcommand{\pic}{$\pi$-calculus}
\newcommand{\hopi}{HO$\pi$}
\newcommand{\mmrec}{\mbox{\bf rec\,}}
\newcommand{\iap}[2]{#1(#2)}
\newcommand{\oap}[2]{\overline{#1} \langle #2 \rangle}
\newcommand{\encode}[1]{[\![\,#1\,]\!]}
\newcommand{\stoppr}{{\bf 0}}
\newcommand{\barb}[1]{\downarrow_{#1}}
\newcommand{\diverge}{\Uparrow}
\newcommand{\bbis}{\stackrel {\mbox{\tiny $ _\bullet$}} \cong}
\newcommand{\beq}{\cong}
\newcommand{\res}[1]{(\nu #1)}
\newcommand{\bang}{{\it bang}}
\newcommand{\chan}{{\it chan}}

\newcommand{\EndProofBox}{\null\hfill$\Box$}
\global\let\EndProof\EndProofBox
\newcommand{\boxHere}{\global\let\EndProof\empty\EndProofBox}
\renewenvironment{proof}{\trivlist\item[]{\bf Proof:}\rm}{\EndProof
    \global\let\EndProof\EndProofBox \endtrivlist}

%%%margin notes
\marginparsep 5pt
\marginparwidth 40pt
 \newcommand{\olds}[1]{\oldstylenums{#1}}
 \newcommand{\oldsb}[1]{{\bfseries\olds{#1}}}
 \newcommand{\mnote}[1]{\stepcounter{ncomm}%
 \vbox to0pt{\vss\llap{\tiny\oldsb{\arabic{ncomm}}}\vskip6pt}%
 \marginpar{\tiny\bf\raggedright%
 {\oldsb{\arabic{ncomm}}}.\hskip0.5em#1}}
 \newcounter{ncomm}
%%%


\newenvironment{eqn}{\begin{eqnarray*}}{\end{eqnarray*}}
\newenvironment{program}{\[\begin{array}{l}}{\end{array}\]}

\def\Pair{{\sf Pair}}

\newcommand{\Rule}[4]{
\makebox{  %%%{\rm (#1)}                                
$\displaystyle
\frac{\begin{array}{l}#2\\\end{array}}
{\begin{array}{l}#3\\\end{array}}$
 #4}}

\newcommand{\vsp}{$ \hspace*{\fill} \\[4mm] \hspace*{\fill} $}
\newcommand{\hsp}{$\hspace*{\fill}$}

\def\Confirm{{\sf confirm}}
\def\Flight{{\sf flight}}
\def\Treq{{\sf t\_req}}
\def\Choose{{\sf Choose}}
\def\Where{{\sf where}}
\def\CHOICE{{\sf CHOICE}}
\def\Yes{{\sf yes}}
\def\No{{\sf no}}
\def\Maybe{{\sf maybe}}
\def\STORE{{\sf STORE}}
\def\Match{{\sf match}}
\def\With{{\sf with}}
\def\Areq{{\sf a\_req}}
\def\Let{{\sf let}}
\def\In{{\sf in}}
\def\Offer{{\sf Offer}}
\def\Select{{\sf select}}
\def\BOOK{{\sf BOOK}}
\def\ch{{\,\&\,}}
\def\Then{{\sf then}}
\def\Else{{\sf else}}
\newcommand{\Linda}{{\sc Linda}}
\newcommand{\pc}{{\sc Pc}}
\newcommand{\cpc}{{\sc Cpc}}
\def\CreditCard{{\sf crcard}}
\def\Seat{{\sf seat}}
\newcommand{\wt}[1]{\widetilde{#1}}
\newcommand{\ex}[1]{\mbox{$\ulcorner\! #1 \!\urcorner$}}
\newcommand{\substit}[3]{ #1 \{\raisebox{.5ex}{\small$#2$}\! / \!\mbox{\small $#3$}\}}
\newcommand{\fix}[1]{{\it fix}_{#1}}

\newcommand{\A}{{\sf A}}
\newcommand{\B}{{\sf B}}
\newcommand{\Tr}{{\sf Tr}}
\newcommand{\Ag}{{\sf Ag}}
\newcommand{\Air}{{\sf Air}}


\newcommand{\lpar}{\mbox{\tt \&}}
\newcommand{\lsum}{\mbox{\tt |}}
\newcommand{\lstar}{\mbox{\tt *}}
\newcommand{\lproc}{\mbox{\tt P}}
\newcommand{\lzero}{\mbox{\tt 0}}
\newcommand{\lact}{\mbox{\tt a}}
\newcommand{\lvar}{\mbox{\tt var\,}}
\newcommand{\lt}{\mbox{\tt t}}
\newcommand{\lT}{\mbox{\tt T}}
\newcommand{\lout}[1]{\mbox{\tt out(#1)}}
\newcommand{\lin}[1]{\mbox{\tt in(#1)}}
\newcommand{\lrd}[1]{\mbox{\tt read(#1)}}
\newcommand{\config}[2]{[#1 \parallel #2]}
\newcommand{\TS}{TS}
\newcommand{\tuple}[1]{\langle #1 \rangle}
\def\Out{{\sf Out}}
\def\ttuple{{\tt t}}
\def\NEW{{\sf new}}
\def\SUCC{{\sf succ}}
\newcommand{\define}{\stackrel {\rm def} =}

\def\Ra{\Rightarrow}

\def\RECORD{{\sf RECORD}}
\def\Ag{{\sf Agent}}
\def\Areq{{\sf agent\_request}}
\def\CONFIRM{{\sf CONFIRM}}
\def\SELECT{{\sf SELECT}}
\def\Treq{{\sf traveller\_request}}
\def\Tr{{\sf Traveller}}

\def\Fix{{\sf fix}}
\def\Copy{{\sf Splitcopy}}
\def\bang{{\sf Bang}}


\newcommand\ssmatch[5]{\{#1\,[#2|\!\!|#3]\,#4\}_{#5}}
\newcommand\smatch[5]{\{#1\,[#2|#3]\,#4\}_{#5}}

\usepackage{color}
\definecolor{mygrey}{gray}{0.8}

\def\Done{{\sf done}}


%%%%% MACROS - TGW %%%%%
\def\pmatch{|\!|}
\def\zero{{\bf 0}}
\def\pre{\to}
\def\buy{{\sf Buy}}
\def\sel{{\sf Sell}}
\def\reg{{\sf Reg}}
\def\prom{{\sf Prom}}
\def\nav{{\sf Nave}}
\def\sname{{\sf ABC}}
\def\snum{{\sf 100}}
\def\sprice{{\sf \$0.38}}
\def\banam{{\sf accountnumber}}
\def\banum{{\sf accountname}}
\newcommand{\pro}[1]{\ulcorner\! #1\!\urcorner}
