%----*- coding: utf-8 -*-

\newcommand\semof[1]{\mbox{\textbf{#1}}}
\newcommand\sel{\mbox{\texttt{sel}}}
\newcommand\nil{\mbox{\texttt{nil}}}

\newcommand\EMPTY{\textsf{\footnotesize{empty}}}
\newcommand\TRIVIAL{\mathbb{T}}

\newcommand\CONJ{\textsf{Conj}}

\newcommand\wrong{\#}

\newcommand\exref[1]{(\ref{#1})}



\newcommand {\lsembrac}		{\mbox{[ \kern -0.5 em [}}
\newcommand {\rsembrac}		{\mbox{] \kern -0.5 em ]}}
\newcommand {\sem} [1]		{{\lsembrac #1 \rsembrac}}
%\newcommand {\Rightarrow} 		{-\!\!\!-\!\!\circ}
% Used as in, e.g., \sem{\phi}^{\rm DPL}_{M,w,t}

% \csmodels is for putting in inference patterns, and \csmodel is for
% running text
\newcommand {\csmodels} 	{\hspace*{0.5em}\mbox{$\mid$ \kern -0.5 em
$\approx$}\hspace*{0.5em}}
\newcommand {\csmodel} 	{\mbox{$\mid$ \kern -0.5 em $\approx$}}

\newtheorem{definition}{Definition}
\newtheorem{translation}{Translation}
\newtheorem{mytheorem}{Theorem}
\newtheorem{mylemma}{Lemma}
\newtheorem{mycorollary}{Corollary}
\newtheorem{myfact} {Fact}

\newenvironment{defn}{
\begin{definition}\begin{quote}\em}
        {\end{quote}\end{definition}}

\newcommand {\notcsmodels} {\hspace*{0.5em}\mbox{$\mid$ \kern -0.5 em $\approx$
\kern -1 em $/$}\hspace*{0.5em}}

\newcommand {\believes} {{\cal B}}

\newcommand {\happyface} {\mbox{\Large
$\bigcirc$\small\raisebox{-0.02in}{\hspace*{-0.17in}$\smile$}
\raisebox{0.06in}{\hspace*{-0.17in}.\hspace*{0.03in}.}}\normalsize
\hspace{0.05in}}


\newcommand\comment[1]{\marginpar{\footnotesize #1}}
\newcommand{\hidden}[1]{\comment{#1}}

% New DAG macro:

\newcommand{\dgw}[1]{{\setlength{\arraycolsep}{0mm}
                     \renewcommand{\arraystretch}{1.1}
                       \left[
                         \begin{array}{l}
                           \\[-0.1in] #1 \\[-0.1in]
                         \end{array}
                       \right]
                    }}




\newcommand{\dg}[2]{{\setlength{\arraycolsep}{0mm}
                     \renewcommand{\arraystretch}{1.1}
                       \left[
                         \begin{array}{l}
				#1\\
                           	#2 \\
                         \end{array}
                       \right]
                    }}
\newcommand{\di}[2]{ #1: #2 \\}

\newcommand{\ind}[1]{{\setlength{\fboxsep}{0.5mm} \: \fbox{{\tiny #1}} \:}}

 \def\drs#1#2{\begin{tabular}{|l|}\hline #1 \\ \hline \\
		[-8pt] #2\\[-8pt] \\ \hline \end{tabular} }

 \def\ddrs#1{\begin{tabular}{||c||}\hline \\
		[-8pt] #1\\[-8pt] \\ \hline \end{tabular} }

 \def\topdrs#1#2{\begin{tabular}{|l|}\hline #1 \\ \hline \\
		[-8pt] #2 \\[-8pt] \\ \hline \end{tabular} }

 \def\proof#1#2#3#4{\drs{#1}{#2} \ $\vdash$ \ \drs{#3}{#4}}
 \def\modimp#1#2#3#4{\mbox{\drs{#1}{#2} \ $\Box$ \ \drs{#3}{#4}}}
% \def\imp#1#2#3#4{\drs{#1}{#2} \ $\Rightarrow$ \ \drs{#3}{#4}}
 \def\dis#1#2#3#4{\mbox{\drs{#1}{#2} \ $\vee$ \ \drs{#3}{#4}}}
 \def\pos#1#2{\mbox{$\Diamond$ \ \drs{#1}{#2}}}
%\def\intend#1#2{\mbox{$\intend$ \ \drs{#1}{#2}}}
 \def\nec#1#2{\mbox{$\Box$ \ \drs{#1}{#2}}}
 \def\nega#1#2{\mbox{$\neg$ \ \drs{#1}{#2}}}
 \def\pred#1#2#3{\mbox{#1\ :\drs{#2}{#3}}}

 \def\raute#1#2{\setlength{\unitlength}{2 em}
	\begin{picture}(2,2)(0,0)
	\put (1,1){\line(1,-1){1}}
	\put (1,1){\line(-1,-1){1}}
	\put (0,0){\line(1,-1){1}}
	\put (1,-1){\line(1,1){1}}
	\put (1,0.15){\makebox(0,0)[b]{#1}}
	\put (1,-0.5){\makebox(0,0)[b]{#2}}
	\end{picture}}

 \def\dup#1#2#3#4#5#6{\mbox{\begin{tabular}{c}
			\drs{#1}{#2} \hspace{-1.3 em}
				\raute{\scriptsize #4}{#3}
			\hspace{-0.6 em}
			\drs{#5}{#6} \\
		     \end{tabular}}}

 \def\xdup#1#2#3#4#5#6{\begin{tabular}{c}
			\drs{#1}{#2}\hspace*{-1mm}\raute{#4}{#3}
			\hspace{-0.6 em}
			\drs{#5}{#6} \\
		     \end{tabular}}


\newcommand{\ben}{\begin{enumerate}}
\newcommand{\een}{\end{enumerate}}
\newcommand{\spc}{\bigskip}
\newcommand{\bqt}{\begin{quote}}
\newcommand{\eqt}{\end{quote}}
\newcommand{\bit}{\begin{itemize}}
\newcommand{\eit}{\end{itemize}}
\newcommand{\var}[1]{\mbox{\em #1}}
\newcommand{\linfon}{\langle \! \langle}
\newcommand{\rinfon}{\rangle \! \rangle}
\newcommand{\infon}[3]{\mbox{$\langle \! \langle  {#1},{#2};{#3}\rangle \!\rangle$}}
\newcommand{\prop}[3]{\mbox{$[{#1}\,|\,{#2 }\models {#3}]$}}
\newcommand{\satisfies}{\| \! $-$}
\newcommand{\use}{\underline}
\newcommand{\linterp}{[ \! [}
\newcommand{\rinterp}{] \! ]}
\newcommand{\interp}[3] {_{#1} \linterp {#2} \rinterp _{#3}}


\renewcommand\refname{}

\newcommand\imp{\rightarrow}
\newcommand\betareduce{\rightarrow_\beta}

\newcommand\syntactictype[1]{\mbox{\textit{#1}}}
\newcommand{\SC}{\syntactictype{s}}
\newcommand{\NP}{\syntactictype{np}}
\newcommand{\N}{\syntactictype{n}}
\newcommand\inter[1]{\llbracket#1\rrbracket}

\newcommand\ent{e}
\newcommand\Prop{t}

\newcommand\defin{\stackrel{\Delta}{=}} 

\newcommand\abs{\lambda}

\newcommand\field[1]{\textsf{{\scriptsize #1}}}
\newcommand\referents{\field{m\_ref}}
\newcommand\factreferents{\field{f\_ref}}
\newcommand\base{\field{base}}
\newcommand\modalbase[2]{\{\referents=#1;\base=#2\}}

\newcommand\modal{\field{m}}
\newcommand\factual{\field{f}}

\newcommand\theory{\field{theory}}
\newcommand\PROP{\textsf{prop}}
\newcommand\THEORY{\field{\textsc{Theory}}}
\newcommand\TEST{\texttt{\footnotesize{TEST}}}
\newcommand\HALT{\texttt{Halt}}
\newcommand\EVAL{\texttt{EVAL}}

\newcommand\modalbasetype[2]{\left\{\begin{array}{rl}\referents & :#1;\\\base& :#2
    \end{array}
  \right\}}

\newcommand\modalbasevector[2]{\left\{\begin{array}{rl}\referents & =#1\\\base& =#2
    \end{array}
  \right\}}

\newcommand\modfactvector[3]{\left\{\begin{array}{rl}\referents & =#1\\\base& =#2\\ \factreferents & =#3
    \end{array}
  \right\}}

\newcommand\modfact[3]{\{\referents =#1;\base =#2; \factreferents
  =#3\}}

\newcommand\modfacttype[3]{\{\referents :#1;\base :#2; \factreferents
  :#3\}}


\newcommand\modfactvectortype[3]{\left\{\begin{array}{rl}\referents & :#1\\\base& :#2\\ \factreferents & :#3
    \end{array}
  \right\}}

\newcommand\const[1]{c_{\mbox{\scriptsize{\textit{#1}}}}}

\newcommand\outputrecord[2]{\left\{\begin{array}{rl}\modal & = #1\\ \factual & =#2
    \end{array}
  \right\}}