\def\subjnum{6.044J/18.423J}

\def\subjname{Computability, Programming, and Logic}

%% Let's just keep this simple for now.
%% dmj, 14 September 1995

\RequirePackage{amssymb}

\RequirePackage{stmaryrd}

%%  %
%%  % We'll want amssymb (or amssymbl or amssymbols) and stmaryrd, if
%%  % they're available.  If not, we'll work around them when we need to.
%%  % \if@haveamssymb, \if@haveamssymbl, \if@haveamssymbols and
%%  % \if@havestmaryrd will indicate for us if these are available.
%%  %
%%  % Because amssymb should make amssymbols obsolete and amssymbl
%%  % unneccessary, only one of the relevant tests should be true.
%%  %
%%  
%%  \newif\if@haveamssymb
%%  \openin1 amssymb.sty \ifeof1 \@haveamssymbfalse
%%      \else \closein1 \relax\input amssymb.sty \@haveamssymbtrue \fi
%%  
%%  \newif\if@haveamssymbl
%%  \if@haveamssymb \@haveamssymblfalse \else
%%  \openin1 amssymbl.sty \ifeof1 \@haveamssymblfalse
%%      \else \closein1 \relax\input amssymbl.sty \@haveamssymbltrue \fi\fi
%%  
%%  \newif\if@haveamssymbols
%%  \if@haveamssymb \@haveamssymbolsfalse \else
%%  \if@haveamssymbl \@haveamssymbolsfalse \else
%%  \openin1 amssymbols.sty \ifeof1 \@haveamssymbolsfalse
%%      \else \closein1 \relax\input amssymbols.sty \@haveamssymbolstrue \fi\fi\fi
%%  
%%  \newif\if@havestmaryrd
%%  \openin1 stmaryrd.sty \ifeof1 \@havestmaryrdfalse
%%      \else \closein1 \relax\input stmaryrd.sty \@havestmaryrdtrue \fi
%%  
%%  \newif\if@haveBbb
%%  \if@haveamssymb\@haveBbbtrue\fi
%%  \if@haveamssymbl\@haveBbbtrue\fi
%%  \if@haveamssymbols\@haveBbbtrue\fi

% hack to get (over) on the bottom of all following odd pages
% must be placed by hand in source text

\outer\def\OVER{\def\@oddfoot{\message{OVER}\rm\hfil(over)}}


% QED slug, with built in preceeding quad (i.e., do not insert
% preceding spaces by hand)

%%from 6001 by ARM 9/95
\newenvironment{lisp}{%
    \def\verbatim@font{\normalfont\ttfamily
                   \let\do\do@noligs
                   \verbatim@nolig@list
                   \advance\leftskip1.5em}%
\verbatim}{\endverbatim}


\newcommand{\QED}%
       {\penalty 1000\ \raise 1pt\hbox{\vrule height6pt width6pt depth0pt}}


% theorems, lemmas, and such, NOT in italic, and with PERIODS.

\def\@begintheorem#1#2{\trivlist \item[\hskip \labelsep{\bf #1\ #2.}]}
\def\@opargbegintheorem#1#2#3{\trivlist
      \item[\hskip \labelsep{\bf #1\ #2\ (#3).}]}
\def\@endtheorem{\endtrivlist}

\newtheorem{lemma}{Lemma}
\newtheorem{claim}{Claim}
\newtheorem{proposition}{Proposition}
\newtheorem{theorem}{Theorem}
\newtheorem{corollary}{Corollary}
\newtheorem{definition}{Definition}
\newtheorem{exercise}{Exercise}
\newtheorem{axiom}{Axiom}
\newtheorem{expression}{Expression}
\newtheorem{newexamp}{Example}
\newtheorem{newnot}{Notation}
\newtheorem{newrem}{Remark}
\newtheorem{fact}{Fact}

% things that are like theorems but without numbers

\newenvironment{remark}{\trivlist\item[]{\bf Remark.}\ }{\endtrivlist}
\newenvironment{solution}{\trivlist\item[]{\it Solution.}\ }{\endtrivlist}
\newenvironment{instruct}{\trivlist\item[]{\bf Instructions.}\ }{\endtrivlist}
\newenvironment{proof}{\trivlist\item[]{\it Proof:}\ }{\QED\endtrivlist}
\newenvironment{proofsketch}{\trivlist\item[]{\it Proof Sketch:}\ }%
                            {\QED\endtrivlist}
\newenvironment{proofx}[1]{\trivlist\item[]{\it Proof \rm #1.}\ }%
                            {\QED\endtrivlist}
\newenvironment{example}{\trivlist\item[]{\bf Example.}\ }{\endtrivlist}
\newenvironment{examples}{\trivlist\item[]{\bf Examples.}\ }{\endtrivlist}
\newenvironment{lemma*}{\trivlist\item[]{\bf Lemma.}\ }{\endtrivlist}
\newenvironment{theorem*}{\trivlist\item[]{\bf Theorem.}\ }{\endtrivlist}
\newenvironment{definition*}{\trivlist\item[]{\bf Definition.}\ }{\endtrivlist}
%%%
%%% Cases environment and pmod redefinition taken from amstex.sty
%%%

\def\cases{\left\{\def\arraystretch{1.2}\hskip-\arraycolsep
  \array{l@{\quad}l}}
\def\endcases{\endarray\hskip-\arraycolsep\right.}

\def\pmod#1{\allowbreak\ifinner\mkern8mu\else\mkern18mu\fi
  ({\rm mod}\,\,#1)}


%
% \problem[number](points) and \subproblem[number](points)
%
% If [number] is omitted (along with its braces), problems are
% numbered automatically.  If (points) is omitted (along with its
% parentheses), no point value is given.  Either may be present or
% omitted.
%

\newcounter{problem}
\newcounter{subproblem}[problem]

\renewcommand{\theproblem}{\arabic{problem}}
\renewcommand{\thesubproblem}{\theproblem(\alph{subproblem})}

\newcommand{\problem}%
    {\@ifnextchar[{\@problem}{\refstepcounter{problem}\@problem[\theproblem]}}
\newcommand{\subproblem}%
    {\@ifnextchar[{\@subproblem}%
                  {\refstepcounter{subproblem}\@subproblem[\thesubproblem]}}

\def\@problem[#1]{\@ifnextchar({\@@problem[#1]}{\paragraph{Problem #1.}}}
\def\@subproblem[#1]{\@ifnextchar({\@@subproblem[#1]}{\paragraph{#1}}}

\def\@@problem[#1](#2){\paragraph{Problem #1~\rm[#2 points].}}
\def\@@subproblem[#1](#2){\paragraph{#1~\rm[#2 points].}}


\def\readingproblem {\paragraph{Reading for the Problem Set.}}
\def\readinglecture {\paragraph{Reading for Lectures.}}
\def\reading {\paragraph{Reading assignment.}}

\newcommand{\due}{\paragraph{Due:}}
\newcommand{\reminder}{\paragraph{Reminder:}}

% subproblems as lists (alternative to \subproblem paragraphs)

\dimen0\labelsep
\setbox0\hbox{\bf(m)}
\edef\subproblabelwidth{\the\wd0\relax}
\advance\dimen0 by\wd0
\edef\subprobleftmargin{\the\dimen0\relax}

\newenvironment{subproblems}{\list{\bf(\alph{subproblem})}%
        {\usecounter{subproblem}%
         \leftmargin\subprobleftmargin
         \labelwidth\subproblabelwidth}}%
        {\endlist}

\newenvironment{moresubproblems}{\list{\bf(\alph{subproblem})}%
        {\count9=\value{subproblem}%
         \usecounter{subproblem}%
         \setcounter{subproblem}{\count9}%
         \leftmargin\subprobleftmargin
         \labelwidth\subproblabelwidth}}%
        {\endlist}

% for putting point values on subproblems

\newcommand{\itemp}[1]{\item{[#1 points]}}

% various enumeration methods which don't interfere with problems
% and subproblems.
% enumerate environment produces lowercase roman labels in parentheses

\newcounter{ctr}

\newenvironment{newenum}{%
\begin{list}{(\arabic{ctr})}{\usecounter{ctr} \labelwidth=30pt%
\labelsep=10pt \leftmargin=40pt 
\topsep=3pt% \listparindent=22pt
 \itemsep=0pt }}{\end{list}}

\newenvironment{rmenum}{% enumerate using small roman numerals
\begin{list}{(\roman{ctr})}{\usecounter{ctr} \labelwidth=30pt%
\labelsep=10pt \leftmargin=40pt 
\topsep=3pt% \listparindent=22pt
 \itemsep=0pt }}{\end{list}}

\newenvironment{newitemize}{%
\begin{list}{$\bullet$}{\labelwidth=30pt
\labelsep=10pt %\leftmargin=40pt
 \topsep=3pt %\listparindent=18pt
 \itemsep=0pt }}{\end{list}}


% abbreviations

\newcommand{\ie}{{\em i.e.}}
\newcommand{\etc}{{\em etc.}}
\newcommand{\eg}{{\em e.g.}}
\newcommand{\Wlog}{{\em w.l.o.g.}}
\newcommand{\cf}{{\em cf.}}
\newcommand{\viz}{{\em viz.}}
\newcommand{\hint}{{\em Hint}\/:\ }             % for in-line hints
\newcommand{\note}{{\em Note}\/:\ }             % for in-line notes

\newcommand{\eqdef}{\stackrel{\rm def}{=}}        % ``equals by definition''

% notation

%
% \fortext and \formath create macros that will work, more or less, in
% both horizontal and math modes.  \fortext expects a math expression,
% and \formath expects a horizontal-mode expression.
%
% \kw (for ``keyword'') is similar to \formath, except its argument is
% set as a mathop, and in boldface.
%

\newcommand{\fortext}[1]{\relax\ifmmode{#1}\else\mbox{$#1$}\fi}
\newcommand{\mathify}{\fortext}
\newcommand{\formath}{\relax\ifmmode\noexpand\hbox\fi}
\newcommand{\kw}[1]{\relax\ifmmode\noexpand\mathop\fi{\bf #1}}
\@ifundefined{operatorname}%
   {\newcommand{\operatorname}[1]{\mathop{\rm #1}\nolimits}}{}
\newcommand{\Wins}{Winskel}

\newcommand{\Cal}[1]{\fortext{{\cal #1}}}
\newcommand{\pow}[1]{\fortext{\hbox{\Cal Pow}(#1)}}
\newcommand{\powf}[1]{\fortext{\hbox{\Cal Pow}_{f}(#1)}}
\newcommand{\ceil}[1]{\fortext{\left\lceil#1\right\rceil}}
\newcommand{\floor}[1]{\fortext{\left\lfloor#1\right\rfloor}}
\newcommand{\set}[1]{\fortext{\left\{#1\right\}}}
%%  \if@havestmaryrd
   \newcommand{\mean}[1]{\fortext{\left\llbracket#1\right\rrbracket}}
%%  \else
%%     \newcommand{\mean}[1]{\fortext{\left[\!\left[#1\right]\!\right]}}
%%     \newcommand{\llbracket}{\[\!\[}
%%     \newcommand{\rrbracket}{\]\!\]}
%%  \fi
\newcommand{\Amean}[1]{\fortext{\Cal A\mean{#1}}}
\newcommand{\Bmean}[1]{\fortext{\Cal B\mean{#1}}}
\newcommand{\Cmean}[1]{\fortext{\Cal C\mean{#1}}}
\newcommand{\Armean}[1]{\fortext{\Cal A_r\mean{#1}}}
\newcommand{\Brmean}[1]{\fortext{\Cal B_r\mean{#1}}}
\newcommand{\Crmean}[1]{\fortext{\Cal C_r\mean{#1}}}
\newcommand{\Avmean}[1]{\fortext{\Cal Av\mean{#1}}}

\newcommand{\Int}{{\bf N}}

%\if@haveBbb
             \newcommand{\Real}{\fortext{\Bbb R}}    % reals
%\else                   \newcommand{\Real}{{\kw R}} \fi


%\newcommand{\fix}{\operatorname{fix}}
\newcommand{\fix}{\fortext{\hbox{\rm fix}}}
%\newcommand{\fix}[1]{\fortext{\hbox{\it fix}(#1)}}
\newcommand{\Eval}[1]{\fortext{\hbox{Eval}(#1)}}
\newcommand{\valof}[1]{\fortext{\hbox{\rm ev-val}(#1)}}
\newcommand{\compose}{\circ}

\newcommand{\emptystring}{\fortext{e}}          % empty string
\@ifundefined{nRightarrow}{\def\nRightarrow{\not\Rightarrow}}{}
\renewcommand{\to}{\mathop{\rightarrow}}        % function space
\newcommand{\pto}{\mathop{\rightharpoonup}}     % partial function space
\newcommand{\rw}{\rightarrow}                   % rewrites relation
\newcommand{\rwone}{\fortext{\mathop{\rw_{1}}}}
\newcommand{\rwr}{\fortext{\mathop{\rw_{r}}}}
\newcommand{\rwrone}{\fortext{\mathop{\rw_{r,1}}}}
\newcommand{\rwtwo}{\mathrel{\mathop{\kern0pt\rw}%
                        \limits^{\vbox to 0pt{\vss\hbox{$\scriptstyle2$}}}}}
                                        % two-way rewrites relation
                        % (This convoluted definition will make ^*
                        %  appear in the right spot in $\rwtwo^*$.)

\@ifundefined{nleq}{\def\nleq{\not\le}}{}
\newcommand{\lub}{\sqcup}
\newcommand{\Lub}{\bigsqcup}
\newcommand{\glb}{\sqcap}
%\if@havestmaryrd
   \newcommand{\Glb}{\bigsqcap}
%\else
%   \newcommand{\Glb}{\sqcap}
%\fi
%\newcommand{\psubset}{\sqsubset}
\newcommand{\intersect}{\cap}                   % set intersection
\newcommand{\Intersect}{\bigcap}                % big set intersection
\newcommand{\union}{\cup}                       % set union
\newcommand{\Union}{\bigcup}                    % big set union

\newcommand{\cross}{\times}                     % cross product
\@ifundefined{npreceq}{\def\npreceq{\not\preceq}}{}
\mathchardef\subset="3212                       % subset
\mathchardef\psubset="321A                      % proper subset
\newcommand{\Land}{\bigwedge}                   % big logical And
\newcommand{\Lor}{\bigvee}                      % big logical Or
\renewcommand{\land}{\wedge}                    % logical and
\renewcommand{\lor}{\vee}                       % logical or
\newcommand{\conj}{\mathrel{\&}}
\newcommand{\disj}{\vee}


\@ifundefined{Vdash}{\def\Vdash{\mathrel{|\vdash}}}{}
\newcommand{\derives}{\Vdash}                   % derivation (a la Winskel)
\newcommand{\<}{\langle}                        % angle brackets
\renewcommand{\>}{\rangle}

\newcommand{\alt}{\mathrel{|}}          % | as a relation for BNF alternatives

\newcommand{\pair}{\fortext{\operatorname{pair}}} % pairing
\newcommand{\frst}{\fortext{\operatorname{first}}}
\newcommand{\scnd}{\fortext{\operatorname{second}}}
\newcommand{\mkpair}{\operatorname{mkpair}} % pairing
\newcommand{\pleft}{\operatorname{left}}
\newcommand{\pright}{\operatorname{right}}
\newcommand{\inl}{\operatorname{in}_{\ell}}
\newcommand{\inr}{\operatorname{in}_r}
\newcommand{\dom}{\operatorname{domain}}
\newcommand{\ran}{\operatorname{range}}
\newcommand{\loc}{\operatorname{loc}}
\newcommand{\num}{\operatorname{num}}
\newcommand{\FV}{\operatorname{FV}}
\newcommand{\charf}[1]{\mathord{\rm char}_{#1}} %characteristic function

\def\bot{{\mathord{\perp}}}

\newcommand{\bits}{\set{{\tt 0},{\tt 1}}}       % for binary words (\bits^*)

%%% For common uses of text in math displays:

%\newcommand{\implies}{\formath{ implies }}  % logical implication
%\newcommand{\implies}{\Rightarrow}  % logical implication
\renewcommand{\iff}{\mbox{ iff }} 
\newcommand{\cmt}{\qquad\formath}                       % comment about a line
\newcommand{\arity}{\operatorname{arity}}


%%% Program keywords:

\newcommand{\If}{\kw{if}}
\newcommand{\Then}{\kw{then}}
\newcommand{\Else}{\kw{else}}
\newcommand{\While}{\kw{while}}
\newcommand{\Do}{\kw{do}}
\newcommand{\Skip}{\kw{skip}}
\newcommand{\Goto}{\kw{goto}}
\newcommand{\Diverge}{\kw{diverge}}
\newcommand{\Resultis}{\kw{resultis}}
\newcommand{\valis}{\kw{valis}}
\newcommand{\Valis}[2]{\fortext{{#1}\valis{#2}}}
\newcommand{\Cond}[3]{\fortext{\If #1 \Then #2 \Else #3}}
\newcommand{\Whileloop}[2]{\fortext{\While #1 \Do #2}}
\newcommand{\True}{\kw{true}}
\newcommand{\False}{\kw{false}}

\def\Truth{\kw{Truth}}
\def\Provable{\kw{Provable}}

\newcommand{\IMP}{\kw{IMP}}
\newcommand{\IMPres}{\fortext{\IMP_r}}
\newcommand{\IMPval}{\fortext{\IMP_{\rm val}}}
\newcommand{\IMPpar}{\fortext{\IMP_{\rm par}}}
\newcommand{\Loc}{\kw{Loc}}
\newcommand{\Num}{\formath{\bf N}}
\newcommand{\Bool}{\formath{\bf T}}
\newcommand{\TF}{\fortext{\set{\True,\False}}}
\newcommand{\Aexp}{\kw{Aexp}}
\newcommand{\Aexpr}{\fortext{\Aexp_r}}
\newcommand{\Aexpv}{\kw{Aexpv}}
\newcommand{\Assn}{\kw{Assn}}
\newcommand{\Intvar}{\kw{Intvar}}
\newcommand{\DynAssn}{\kw{DynAssn}}
\newcommand{\Bexp}{\kw{Bexp}}
\newcommand{\Bexpr}{\fortext{\Bexp_r}}
\newcommand{\Com}{\kw{Com}}
\newcommand{\Comr}{\fortext{\Com_r}}
\newcommand{\Hoare}{{\fortext{\vdash_{\hbox{\tiny Hoare}}}}}



%% \def\Code#1{\hbox{\tt#1}}

\newcommand{\pca}[3]{\fortext{\set{#1}#2\set{#3}}}

\newcommand{\conf}[2]{\fortext{\left\< #1,#2\right\>}}

\@namedef{rw1}{\rwone}
\@namedef{rw1*}{\mathrel{\rw_1^*}}
\@namedef{rwr1}{\rwrone}
\@namedef{rwr1*}{\mathrel{\rw_{r,1}^*}}

\newcommand{\evals}{\@ifnextchar[{\@evals}{\@evals[]}}
\newcommand{\evalsto}{\@evals[]}
\def\@evals[#1]#2#3#4{\fortext{\conf{#2}{#3}\@nameuse{rw#1}#4}}

% The following definitions are buggy
%\def\rew1#1#2#3{\fortext{\conf{#1}{#2}\rw_1 #3}}
%try this anyway:
\def\rew1*#1#2#3{\fortext{\conf{#1}{#2}\rw_1^* #3}}

\newcommand{\rewritesto}{\underset{\rm rew}{\rulesto}}
\newcommand{\fe}{\underset{\rm func}{=}}

\newcommand{\hole}{\Code{[ ]}}
%\newcommand{\hole}{\fortext{[\: ]}}

%%% Additional hyphenation patterns:

\hyphenation{manu-script ne-gate ne-gat-ed}


%
% \answerbox[width,height]
%
% Place a box for answers to be filled in, with baseline slightly
% below the text baseline.  The default size for the box is
% .6in x .15in.  An optional [width,height] argument will override the
% defaults.  The optional argument, if present can omit either or both
% of width and height, leaving the default in effect.  If the optional
% argument is present, however, the comma is required.
%

\newdimen\@answerboxheight \newdimen\@answerboxwidth
\newcommand{\answerbox}{\@ifnextchar[{\@answerbox}{\@answerbox[,]}}
\def\@answerbox[#1,#2]%
      {\@answerboxwidth=.6in\if!#1!\else\@answerboxwidth=#1\fi
       \@answerboxheight=.15in\if!#2!\else\@answerboxheight=#2\fi
       \framebox[\@answerboxwidth]{\rule[-.05in]{0in}{\@answerboxheight}}}
\newcommand{\answer}{\@ifnextchar[{\@answer}{\@answer[,]}}
\def\@answer[#1,#2]#3%
      {\@answerboxwidth=.6in\if!#1!\else\@answerboxwidth=#1\fi
       \@answerboxheight=.15in\if!#2!\else\@answerboxheight=#2\fi
       \framebox[\@answerboxwidth]{\rule[-.05in]{0in}{\@answerboxheight}%
                                   \em\hfil #3\hfil}}


%%% From Jon Riecke's thesis:

\newcommand{\Rule}[2]{          % Unnumbered rule
  \begin{array}{c}
  #1 \\\hline
  #2
  \end{array}}

\newcommand{\RuleName}[3]{
\noindent
\[ \begin{array}{cr}
\Rule{#1}{#2} & \cmt{(#3)}
\end{array} \]
}

\newcommand{\AxiomName}[2]{
\noindent
\[ \begin{array}{cr}
{#1} & \cmt{(#2)}
\end{array} \]
}


%% Stuff imported from 6001.sty September 14, 1995, by dmj.  Let's see
%% how well this works.

\RequirePackage{bnf}
\RequirePackage{eqnarray}
\RequirePackage{verbatim}

\newcommand\RFS{Revised$^4$ Scheme}

%%  Modifications to bnf.sty

% \newcommand{\pto}{\mathop{\rightharpoonup}}     % partial function space

\def\bnf{%
   \mathcode`"=\mathactive
%   \mathcode`[=\mathactive \mathcode`\]=\mathactive
   \mathcode`(=\mathactive \mathcode`\)=\mathactive
   \mathcode`|=\mathactive \mathcode`-=\mathactive
   \mathcode`<=\mathactive \mathcode`\>=\mathactive
   \mathcode`@=\mathactive \mathcode`==\mathactive
   \mathcode96 \mathactive
}

\def\endbnf{\global\@ignoretrue}

\begingroup
  \catcode`\~=\active
  \lccode`\~=`\^^M
  \lowercase{\endgroup
    \gdef\Terminal{\relax\PreTerminal
      \ifmmode \hbox \else \leavevmode\null \fi
      \bgroup
      \TerminalFont
      \catcode`~\active
      \def~{\egroup\@latexerr{Terminal string ended by
                              end of line.}\@ehc}%
    \let\do\@makeother \dospecials \@vobeyspaces \frenchspacing
    \@sTerminal}}

\begingroup
    \catcode`@\active

    \gdef@{% either an escape char or a star group
        \ifnonterminal
            \expandafter\NotInNonTerminal
        \fi
    }%

\endgroup

%%  End of modifications to bnf.sty

\newtoks\old@everyhbox

\def\Code{%
    \leavevmode
    \old@everyhbox=\expandafter{\the\everyhbox}%
    \everyhbox=\expandafter{%
        \the\everyhbox
        \tt\frenchspacing
        \catcode`\#=12
        \global\everyhbox=\expandafter{\the\old@everyhbox}%
    }%
    \hbox
}

\let\rulesto\longrightarrow

\newcommand{\patch}[3]{#1[#2 \leftarrow #3]}
\newcommand{\byrule}[1]{\mathbin{\mathop{\rulesto}\limits_{\rm #1}}}
\def\eval1{\fortext{\byrule{eval}}}
\def\evalss{\fortext{{\byrule{eval}}^{*}}}

\newcommand{\subst}[3]{\ensuremath{#1[#2 := #3]}}

\newcommand{\provable}{\ensuremath{\vdash\,}}

\newcommand{\proves}[1][]{% provability (cf. \models)
    \if!#1!
        \ensuremath{\vdash\,}
    \else
        \ensuremath{\mathrel{\mathop{\vdash}\limits_{#1}}}%
    \fi
}

%\newcommand{\ple}{\proves{\leq}}
\newcommand{\cle}{\ensuremath{\mathbin{\Code{<=}}}}

\newcommand{\integers}{\ensuremath{\mathbb{Z}}}
\newcommand{\reals}{\ensuremath{\mathbb{R}}}
\newcommand{\nnintegers}{\ensuremath{\mathbb{N}}}

\endinput
