\def\vd{\null\mathrel{\vdash}} %Frank's
\def\nprv{\null\mathrel{\not\vdash}} %Frank's
\def\nvd{\null\mathrel{\not\vdash}} %Frank's
\newcommand{\df}{\mathit{def}}
\newcommand{\mnot}{{\rm Not}}
\newcommand{\ex}{\exists}
\newcommand{\atm}{\mbox{\textrm{At}}}
\renewcommand{\ll}{\overline{l}}
\newcommand{\xn}{\overline{x_n}}
\newcommand{\xk}{\overline{x_k}}
\newcommand{\xnk}{\overline{x_{n^k}}}
\newcommand{\ym}{\overline{y_m}}
\newcommand{\yn}{\overline{y_n}}
\newcommand{\Xn}{\overline{X_n}}
\newcommand{\Yn}{\overline{Y_n}}
\newcommand{\Zn}{\overline{Z_n}}
\newcommand{\Ym}{\overline{Y_m}}
\renewcommand{\wr}{\overline{w_r}}
\newcommand{\Wr}{\overline{W_r}}
\newcommand{\zp}{\overline{z_p}}
\newcommand{\zm}{\overline{z_m}}
\newcommand{\Zp}{\overline{Z_p}}
\newcommand{\tn}{\overline{t_n}}
\newcommand{\tm}{\overline{t_m}}
\newcommand{\sm}{\overline{s_m}}
\newcommand{\un}{\overline{u_n}}
\newcommand{\sN}{\overline{s_n}}
\newcommand{\Am}{\overline{A_m}}
\newcommand{\An}{\overline{A_n}}
\newcommand{\Bn}{\overline{B_n}}
\newcommand{\Ep}{\overline{E_q}}
\newcommand{\Hk}{\overline{H_k}}
\newcommand{\Mm}{\overline{M_m}}
 \newcommand{\Mn}{\ol{M_{n}}}
\newcommand{\Nn}{\overline{N_n}}
\newcommand{\vx}{\vec{x}}
\newcommand{\vy}{\vec{y}}
\newcommand{\vz}{\vec{z}}
\newcommand{\vw}{\vec{w}}
\newcommand{\vX}{\vec{X}}
\newcommand{\vY}{\vec{Y}}
\newcommand{\vZ}{\vec{Z}}
\newcommand{\vW}{\vec{W}}
\newcommand{\vt}{\vec{t}}
\newcommand{\vs}{\vec{s}}

\newcommand{\sqless}{\sqsubseteq}
\newcommand{\mdots}{, \dots ,}
\newcommand{\suchthat}{\mid}
\newcommand{\prv}{\vd}
\newcommand{\nq}{\neq}
\newcommand{\nebe}{\not =_{\beta\eta}}  % do not need argument
\newcommand{\ebe}{=_{\beta\eta}}
\renewcommand{\l}{\lambda}
\newcommand{\lll}{{$L_{\l}$}}
\newcommand{\skl}{\mbox{}\\}
\newcommand{\vsk}{\\[2ex]}
\newcommand{\s}{\sigma}
\newcommand{\q}{\theta}
\newcommand{\fo}{first-order }
\newcommand{\ho}{higher-order }
\newcommand{\eg}{e.g.~}
\newcommand{\ie}{{i.e.~}}
\newcommand{\wrt}{{w.r.t.~}}
\newcommand{\lp}{logic programming\/ }
\newcommand{\cN}{{\cal N}}
\newcommand{\cC}{{\cal C}}
\newcommand{\cD}{{\cal D}}
\newcommand{\cE}{{\cal E}}
\newcommand{\cB}{{\cal B}}
\newcommand{\cQ}{{\cal Q}}
\newcommand{\cP}{{\cal P}}
\newcommand{\GG}{\Gamma}
%\newcommand{\ap}{\mathrm{ca}}
%\newcommand{\ci}{\mathrm{ci}}
%\newcommand{\sk}{\mathit{sk}}
\newcommand{\SLD}{{\em SLD\/}}
\newcommand{\SLDNF}{{\em SLDNF\/}}
\newcommand{\NF}{{\em NF }}
\newcommand{\nf}{{\em NF }}
\newcommand{\ul}{\underline}
\newcommand{\ol}{\overline}
\newcommand{\Or}{\vee}
\newcommand{\BOr}{\bigvee}
\newcommand{\And}{\wedge}
\newcommand{\ANd}{\bigwedge}
\newcommand{\BAnd}{\bigwedge}
\newcommand{\Not}{\neg}
\newcommand{\Imp}{\rightarrow}
\newcommand{\LImp}{\longrightarrow}
\newcommand{\Lmap}{\longmapsto}
\newcommand{\lead}{\leadsto}
\newcommand{\If}{\leftarrow}
\newcommand{\Ift}{:-}
\newcommand{\Bimp}{\leftrightarrow}
\newcommand{\leavebigvspace}{\par \addvspace{\bigskipamount}}
\newcommand{\la}{\langle}
\newcommand{\ra}{\rangle}
\newcommand{\eneq}{\end{eqnarray*}}
\newcommand{\beq}{\begin{eqnarray*}}
\newcommand{\bca}{\[\begin{array}{c}}
\newcommand{\eca}{\end{array}\]}
\newcommand{\bit}{\begin{itemize}}
\newcommand{\enit}{\end{itemize}}
\newcommand{\ben}{\begin{enumerate}}
\newcommand{\enen}{\end{enumerate}}
\newcommand{\bedef}{\begin{Def}}
\newcommand{\enef}{\end{Def}}



% \newtheorem{Theorem}{Theorem}
% 
% \newtheorem{Lemma}[Theorem]{Lemma}
% \newtheorem{Corollary}[Theorem]{Corollary}
% \newtheorem{Definition}[Theorem]{Definition}


% \newtheorem{Theorem}{Theorem} [chapter]  %-cd
% \newtheorem{Definition}{Definition}[theorem]
% \newtheorem{Lemma}{Lemma}[theorem]
% \newtheorem{Corollary}{Corollary}[theorem]
% \newtheorem{Fact}{Fact}[theorem]
%        \newtheorem{Notation}{Notation}[theorem]
%        \newtheorem{Observation}{Observation}[theorem]
%        \newtheorem{Proposal}{Proposal}[theorem]
%        \newtheorem{Remark}{Remark}[theorem]
%        \newtheorem{Result}{Result}[theorem]
%        \newtheorem{Conjecture}{Conjecture}[theorem]
%        \newtheorem{Claim}{Claim}[theorem]
%        \newtheorem{Example}{Example}[theorem]
%        \newtheorem{example}{example}[theorem]

%\newtheorem{Theorem}{Theorem}[theorem]

\newenvironment{Examplen}
{\begin{Example}\def\p@example{\theexample} \em}
{{$\phantom{a}$\hfill$\Diamond$}\end{Example}}
\newcommand{\bdef}[1]
{{\small{\bf Definition \ref{#1}}}}
\def\thedefinition{\thesection.\arabic{definition}}

\newenvironment{Def}
{\begin{Definition}%  
\def\p@definition{\thedefinition} \em}%
{\end{Definition}}
\def\theproperty{\thesection.\arabic{property}}
%\newtheorem{Property}{Property}[theorem]
\newenvironment{Pty}
{\begin{Property}%  
\def\p@property{\theproperty} \em}%
{\end{Property}}
\newcommand{\bpty}[1]
{{\small{\bf Property \ref{#1}}}}
\def\theproperty{\thesection.\arabic{property}}
%\newtheorem{Proposition}{Proposition}[theorem]
\newenvironment{Ppn}
{\begin{Proposition}%  
\def\p@proposition{\theproposition} \em}%
{\end{Proposition}}
\newcommand{\bppn}[1]
{{\small{\bf Proposition \ref{#1}}}}

\newcommand{\RImp}{\stackrel{\mbox{\tiny  $1$}}{\Imp}}
% \newcommand{\rapp}{^{\verb+^+}}
\newcommand{\rapp}{^{\ \#}}
\newcommand{\zapp}{\circ}
 \newcommand{\TImp}{\stackrel{\mbox{\tiny  u}}{\Imp}}
 \newcommand{\KImp}{\stackrel{\mbox{\tiny  k}}{\Imp}}
%\newcommand{\TImp}{\Imp}
\newcommand{\ZImp}{\stackrel{\mbox{\tiny  $0$}}{\Imp}}
% \newcommand{\red}{\stackrel{\mbox{\tiny whr}}{\longrightarrow}}
\newcommand{\GImp}[1]{\stackrel{\mbox{\tiny  ${#1}$}}{\Imp}}
\renewcommand{\LImp}{\stackrel{\mbox{\tiny  $l$}}{\Imp}}
\newcommand{\prvs}{\prv_{\Sigma}}
\newcommand{\nprvs}{\nprv_{\Sigma}}
% \newcommand{\lom}{\lambda^{\omega}}
\newcommand{\lom}{\lambda}
% \newcommand{\lR}{\lambda^{\rm {small R}}}
\newcommand{\lr}{\lambda^{\mbox{\tiny   1}}}
\newcommand{\lt}{\lambda^{\mbox{\tiny   0}}}
\newcommand{\lu}{\lambda^{\mbox{\tiny   u}}}
\newcommand{\lx}{\lambda x \, . \, }
\newcommand{\ly}{\lambda y \, . \, }
\newcommand{\PI}[2]{\Pi {#1}\!:\!{#2}.\,}
\renewcommand{\ex}[2]{\exists {#1}\!:\!{#2}.\,}
\newcommand{\all}[2]{\forall {#1}\!:\!{#2}.\,}
 \newcommand{\lamb}[2]{\lambda {#1}\!:\!{#2}.\,}
\newcommand{\of}[2]{{#1}\!:\!{#2}}

\newcommand{\lxa}{\lambda x\!:\! A.\,}
% \newcommand{\lc}{\lambda{{\stackrel{l}{\Imp}}}}
 \newcommand{\lc}{\lambda^{\LImp}}
\newcommand{\eset}{\emptyset}
\def\squareforqed{\hbox{\rlap{$\sqcap$}$\sqcup$}}
\def\qed{\ifmmode\squareforqed\else{\unskip\nobreak\hfil
\penalty50\hskip1em\null\nobreak\hfil\squareforqed
\parfillskip=0pt\finalhyphendemerits=0\endgraf}\fi}
\def\be{\beta\eta}
% \newenvironment{proof}{\noindent
% {\bf Proof.} $\;$}{$\phantom{a}$\hfill$\Box$\leavebigvspace}


\newcommand{\prop}{\mbox{\textbf{o}}}
\newcommand{\xoa}{x\oftp A}

\newcommand{\vN}{\vec{N}}
\newcommand{\vM}{\vec{M}}
\newcommand{\itc}{\item[\textbf{Case:}]}
\newcommand{\bmeta}{\begin{metanote}}
\newcommand{\emeta}{\end{metanote}}
\newcommand{\btab}{\begin{tabbing}}
\newcommand{\etab}{\end{tabbing}}
\newcommand{\bv}{\` By inversion\\}
\newcommand{\bd}{\` By definition\\}
\newcommand{\bs}{\` Subderivation\\}
\newcommand{\bi}{\` By IH }
\newcommand{\bh}{\` Hypothesis\\}
\newcommand{\ba}{\` Assumption\\}
\newcommand{\bsu}{\` By subst.}
\newcommand{\br}{\` By rule }
\newcommand{\bl}[1]{\` By Lemma \ref{#1} \\}
\newcommand{\bru}[1]{\` By Lemma $#1$ \\}
\newcommand{\hence}{hence the claim.}


\newcommand{\eqdef}{\stackrel{\mbox{\tiny  \textrm{def}}}{=}}
\newcommand{\mmnot}{\neg}
\newcommand{\rep}[1]{\ulcorner #1\urcorner}  % amsfonts.sty
\newcommand{\arv}[2]{\begin{array}{c} #1\\#2\end{array}}
\newcommand{\UImp}{\GImp{u}}
\newcommand{\god}{\Gamma; \Omega;\Delta}
\newcommand{\godp}{\Gamma'; \Omega';\Delta'}
\newcommand{\godemp}{(\GG,\O,D)\emp}
\newcommand{\betared}{\stackrel{\beta}{\longrightarrow}}
\newcommand{\etaexp}{\stackrel{\bar\eta}{\longrightarrow}}
\newcommand{\lxua}{\lambda x^{u}\!:\!  A.\, }
\newcommand{\D}{\Delta}
\renewcommand{\O}{\Omega}
\newcommand{\dmn}{(\D_{M},\D_{N})}
\newcommand{\Mns}{\overline{M_n^1}}
\newcommand{\Nns}{\overline{N_n^1}}
\newcommand{\emp}{;\cdot;\cdot}
\newcommand{\cF}{{\cal F}}
\newcommand{\xnl}{\overline{x_{n}^{k}}}
\newcommand{\cM}{{\cal M}}
\newcommand{\mbc}{\bigcap} %overloaded notation: may be changed
\newcommand{\mna}{\mmnot} %overloaded notation: may be changed
\newcommand{\mcap}{\cap}
\newcommand{\mbigcap}{\cap} %overloaded
\newcommand{\da}{\downarrow}
\newcommand{\bua}{\Uparrow}
\newcommand{\buda}{\Uparrow\!\downarrow}
\newcommand{\blip}{\Rightarrow}
\newcommand{\xoc}{x\oftp C}


%%%%%%%%%%% from cconew


\newcommand{\defp}{\mbox{\textrm{def}}}
\newcommand{\xrq}{x R^i q}
\renewcommand{\bar}{\|}
\newcommand{\ecs}{\circ}
\newcommand{\cS}{{\cal S}}
\newcommand{\ins}{<}
\newcommand{\block}[1]{\lceil #1\rceil}
\newcommand{\some}[1]{\mbox{\textrm{SOME}} \ {#1} \,. }
\newcommand{\sla}{\setminus}
\newcommand{\gap}{\GG';\cD'}
\newcommand{\inss}{\ins\cS}
\newcommand{\dsats}{\models_{\!\cS\bar\cS'}}
\newcommand{\dsato}{\models_{\!\cS_1}}
\newcommand{\dsat}{\models_{\!\cS}}
\newcommand{\dsatt}{\models_{\!\cS_2}}
\newcommand{\insss}{\ins\cS\bar\cS'}
\newcommand{\eq}{\eqd}  
\newcommand{\yield}{\Rightarrow}
\renewcommand{\neq}{\not\eqd}
\newcommand{\alg}{aug_{\mbox{\tiny \textrm{G}}}}
\newcommand{\ald}{aug_{\mbox{\tiny \textrm{D}}}}
\newcommand{\gfald}{\ga\vd_{\!\Phi}\ald} %changed
\newcommand{\gfalg}{\Gamma;\cD\prv_{\!\Phi}\alg}
\newcommand{\mnota}{{\rm Not}_{\mbox{$\alpha$} }}
\newcommand{\mnotd}{{\rm Not}_{\rm D}  }
\newcommand{\mnotg}{{\rm Not}_{\rm G}  }
 \newcommand{\mnotxi}{\mnot^i_x}
\renewcommand{\sp}{\vd_{\!\cP}}
\newcommand{\PP}{\cP}
\newcommand{\PM}{\cP}
\newcommand{\spp}{\vd_{\!\PP}}
\newcommand{\snp}{\vd_{\!\PM}\mnotg}
\newcommand{\sn}{\vd_{\!\PM}}
\newcommand{\PIXA}{\Pi x\!:\!A.\,}
\newcommand{\exa}{\exists x\!:\!A.\,}
\newcommand{\fpp}{\nvd_{\!\PP}}
\newcommand{\fnp}{\nvd_{\!\PM}\mnotg }
\newcommand{\fn}{\nvd_{\!\PM}}
\newcommand{\fp}{\nvd_{\!\cP}}
\newcommand{\cA}{{\cal A}}
\newcommand{\cT}{{\cal T}}
\newcommand{\cJ}{{\cal J}}
\newcommand{\tensor}{\oplus}
\newcommand{\ga}{\Gamma;\cD }
\newcommand{\gna}{ \Gamma;\cD }
\newcommand{\vS}{\vec{S}}
\newcommand{\PA}{\mid \cP\mid}
\newcommand{\eqd}{\stackrel{\cdot}{=}}
\newcommand{\neqd}{\not\stackrel{\cdot}{=}}
\newcommand{\imm}{\mbox{$>\!\!>$}}
\newcommand{\notimm}{\mbox{$\not >\!\!>$}}
\newcommand{\nimm}{\imm}
\newcommand{\IP}{{\cal I}^{+}}
\newcommand{\IM}{{\cal I}^{-}}
\newcommand{\SP}{{\cal S}^{+}}
\newcommand{\SM}{{\cal S}^{-}}
%\newcommand{\gf}{\Gamma;\cD\vd_{\!\Phi}^{\! Q}} CHANGE (Input
%variables \Phi
\newcommand{\gf}{\Gamma\vd}
%\newcommand{\gf}{\Gamma\vd^{\! Q}}
\newcommand{\gfq}{}
%\newcommand{\gfq}{q\oftp \An\Imp\prop\vd}
% \newcommand{\vdf}{\vd_{\!\Phi}} input variables
\newcommand{\vdf}{\vd_{\!\cP}}
\newcommand{\foq}{\mbox{\textrm{for all }$ \q$  }}
\newcommand{\dom}{\mbox{\textrm{dom}}}
\renewcommand{\emp}{\cdot;\top}
\newcommand{\csa}{\cS^a}
\newcommand{\yd}{\stackrel{\mbox{\tiny{$D$}}}{\Longrightarrow}}
\newcommand{\yg}{\stackrel{\mbox{\tiny{$G$}}}{\Longrightarrow}}
\newcommand{\less}{\prec} 
\newcommand{\boxarray}[1]{\[\fbox{$\begin{array}
      {c}\mbox{}\vsk #1\mbox{}\vsk\end{array}$}\]}
% call with the context of the array
\renewcommand{\Pi}{\forall}  %%% all for pi


%%%%%%%%%%% Start cdsty
\setlength{\textwidth}{12.9cm}
\setlength{\textheight}{19.3cm}
%%% A modification of fpstd.sty appropriate for this book.
%%% Modifications are noted with %-cd
%%% Modifications for article 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Environment and Miscellaneous
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\let\um=\"

\newcommand{\horizline}{{\rule{\textwidth}{0.4pt}}}
\newenvironment{dfigure*}{\begin{figure*}[tb]\horizline}{\par\vskip-\parskip
 \horizline\end{figure*}}
\newenvironment{symbolfootnotes}{\def\thefootnote{\fnsymbol{footnote}}}{}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Typesetting Deductions
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newbox\tempa
\newbox\tempb
\newdimen\tempc
\newbox\tempd

\def\mud#1{\hfil $\displaystyle{#1}$\hfil}
\def\rig#1{\hfil $\displaystyle{#1}$}

\def\inruleanhelp#1#2#3{\setbox\tempa=\hbox{$\displaystyle{\mathstrut #2}$}%
                        \setbox\tempd=\hbox{$\; #3$}%
                        \setbox\tempb=\vbox{\halign{##\cr
        \mud{#1}\cr
        \noalign{\vskip\the\lineskip}%
        \noalign{\hrule height 0pt}%
        \rig{\vbox to 0pt{\vss\hbox to 0pt{\copy\tempd \hss}\vss}}\cr
        \noalign{\hrule}%
        \noalign{\vskip\the\lineskip}%
        \mud{\copy\tempa}\cr}}%
                      \tempc=\wd\tempb
                      \advance\tempc by \wd\tempa
                      \divide\tempc by 2 }

\def\inrulean#1#2#3{{\inruleanhelp{#1}{#2}{#3}%
                     \hbox to \wd\tempa{\hss \box\tempb \hss}}}
\def\inrulebn#1#2#3#4{\inrulean{#1\quad\qquad #2}{#3}{#4}}

\def\ian#1#2#3{{\lineskip 4pt\inrulean{#1}{#2}{#3}}}
\def\ibn#1#2#3#4{{\lineskip 4pt\inrulebn{#1}{#2}{#3}{#4}}}

\def\lowerhalf#1{\hbox{\raise -0.8\baselineskip\hbox{#1}}}

\def\ianc#1#2#3{{\lineskip 4pt\lowerhalf{\inruleanhelp{#1}{#2}{#3}%
                   \box\tempb\hskip\wd\tempd}}}
\def\ibnc#1#2#3#4{{\lineskip 4pt\ianc{#1\quad\qquad #2}{#3}{#4}}}

\def\rulespacing{\renewcommand{\arraystretch}{3} \arraycolsep 5em}
\def\rulestretch{\renewcommand{\arraystretch}{3}}

\def\above#1#2{\begin{array}[b]{c}\relax #1\\ \relax #2\end{array}}
\def\abovec#1#2{\begin{array}{c}\relax #1\\ \relax #2\end{array}}

\def\cian#1#2#3{\ctr{\ianc{#1}{#2}{#3}}}
\def\cibn#1#2#3#4{\ctr{\ibnc{#1}{#2}{#3}{#4}}}

\def\hypo#1#2{\begin{array}[b]{c}\relax #1\\ \vdots \\ \relax #2\end{array}}
\def\hypoc#1#2{\begin{array}{c}\relax #1\\ \vdots \\ \relax #2\end{array}}
\def\hypol#1#2#3{\begin{array}[b]{c}\relax #1\\ #2 \\ \relax #3\end{array}}
\def\hypolc#1#2#3{\begin{array}{c}\relax #1\\ #2 \\ \relax #3\end{array}}

\def\ctr#1{\begin{array}{c} #1\end{array}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Common abbreviations
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\bnfas{\mathrel{::=}}
\def\bnfalt{\mid}

\def\lam{\lambda}
\def\Lam{\Lambda}
\def\oftp{\mathord{:}}
\def\hastype{\mathrel{:}}

\def\ldot{\mathord{.}\;}
\def\ldott{\mathrel{.}}
\def\oftpp{\mathrel{:}}
\def\dot{\cdot}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Judgments
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\vd{\null\mathrel{\vdash}}
%\def\gvd{\Gamma \vd}

\def\th{\null\mathrel{\vdash\!\!\!\vdash}}
\def\gth{\Gamma \th}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Code
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\def\ttuscore{{\tt\char`\_}}
\def\ttlbrace{{\tt\char`\{}}
\def\ttrbrace{{\tt\char`\}}}

%%%%%%%%%
 \def\zzctdrawdotedge{\drawdotedge{4pt}0}
 \def\ctabutborderlr{1em}
 \def\ctabutbordertb{1ex}



\renewcommand{\sp}{\vd_{\!\cP}}
\newcommand{\lf}{logical framework}
\renewcommand{\tensor}{\Or}
\renewcommand{\Pi}{\forall}  %%% all for pi
\renewcommand{\vM}{\Mn}
\renewcommand{\vN}{\Nn}
\renewcommand{\bar}{\|}
\renewcommand{\csa}{\cS}
\renewcommand{\ex}{e_x}