\def\Pl{\hbox to12pt{\hfil$+$\hfil}}
\def\Ti{\hbox to12pt{\hfil$\.$\hfil}}
\def\Ex{\hbox to12pt{\hfil$\uparrow$\hfil}}
\def\Se{\hbox to12pt{\hfil$\Uparrow$\hfil}}

%PDF
% http://insti.physics.sunysb.edu/~siegel/tex.shmtl

\def\yy{\catcode`~=12\catcode`\#=12\relax}
\def\zz{\catcode`~=13\catcode`\#=6\relax}
\def\rgboo#1{\pdfliteral{#1 rg #1 RG}}
\def\rgbo#1#2{\rgboo{#1}#2\rgboo{0 0 0}}

\newif\ifonline
\def\pdfklink#1#2{\ifonline%
	\pdfliteral{0 0 1 rg}
	\noindent\pdfstartlink user
		{/Subtype /Link
		/Border [ 0 0 0 ]
		/A << /S /URI /URI (#2) >>}{\rgbo{.3 .3 1}{$\underline{\hbox{\ninett#1}}$}}%
	\pdfendlink
\else
	\noindent\pdfstartlink user
		{/Subtype /Link
		/Border [ 0 0 0 ]
		/A << /S /URI /URI (#2) >>}{{\ninett#1}}%
	\pdfendlink
\fi}

\def\pdfKlink#1#2{\ifonline%
	\pdfliteral{0 0 1 rg}
	\noindent\pdfstartlink user
		{/Subtype /Link
		/Border [ 0 0 0 ]
		/A << /S /URI /URI (#2) >>}{\rgbo{0 0 1}{$\!\!\underline{\hbox{#1}}$}}%
	\pdfendlink
\else
	\noindent\pdfstartlink user
		{/Subtype /Link
		/Border [ 0 0 0 ]
		/A << /S /URI /URI (#2) >>}{#1}%
	\pdfendlink
\fi}
\def\pdflink#1{\pdfklink{#1}{#1}}

\def\image#1{\immediate\pdfximage{#1}
	\centerline{\hbox{\pdfrefximage \pdflastximage}}}

\def\pa#1{\immediate\pdfximage page #1 {/u/nelson/public_html/books/pa.pdf}\hbox{\pdfrefximage \pdflastximage}}

% FONTS
\font\bigrm=cmr7 scaled \magstep4
\font\bbbold=msbm10
\def\bbb#1{\hbox{\bbbold#1}}
\font\ninerm=cmr9
\font\ninebf=cmbx9
\font\nineit=cmti9
\font\ninett=cmtt9
\font\ninei=cmmi9
\font\eighti=cmmi8
\font\eightrm=cmr8
\font\eightbf=cmbx8
\font\eightit=cmti8
\font\eightsl=cmsl8
\font\eighttt=cmtt8
\font\eightsy=cmsy8
\font\tenss=cmss10
\font\ninesy=cmsy9
\font\eightsy=cmsy8
\font\nineit=cmti9
\font\eightit=cmti8
\font\sixrm=cmr6
\font\sixbf=cmbx6
\font\sixi=cmmi6
\font\sixsy=cmsy6
\font\sans=cmss10
\font\ninesans=cmss9
\font\eightsans=cmss8
\font\sansit=cmssi10
\font\tenmsa=msam10
\def\ninepoint{\def\rm{\fam0\ninerm}%
   \textfont0=\ninerm \scriptfont0=\sixrm \scriptscriptfont0=\fiverm
   \textfont1=\ninei \scriptfont1=\sixi \scriptscriptfont1=\fivei
   \textfont2=\ninesy \scriptfont2=\sixsy \scriptscriptfont2=\fivesy
   \textfont3=\tenex \scriptfont3=\tenex \scriptscriptfont3=\tenex
   \textfont\itfam=\nineit \def\it{\fam\itfam\nineit}%
   \textfont\bffam=\ninebf \scriptfont\bffam=\sixbf
    \scriptscriptfont\bffam=\fivebf \def\bf{\fam\bffam\ninebf}%
   \normalbaselineskip=11pt
   \setbox\strutbox=\hbox{\vrule height8pt depth 3pt width0pt}%
   \let\big=\ninebig \normalbaselines\rm}
\def\eightpoint{\def\rm{\fam0\eightrm}%
   \textfont0=\eightrm \scriptfont0=\sixrm \scriptscriptfont0=\fiverm
   \textfont1=\eighti \scriptfont1=\sixi \scriptscriptfont1=\fivei
   \textfont2=\eightsy \scriptfont2=\sixsy \scriptscriptfont2=\fivesy
   \textfont3=\tenex \scriptfont3=\tenex \scriptscriptfont3=\tenex
   \textfont\itfam=\eightit \def\it{\fam\itfam\eightit}%
   \textfont\bffam=\eightbf \scriptfont\bffam=\sixbf
    \scriptscriptfont\bffam=\fivebf \def\bf{\fam\bffam\eightbf}%
   \normalbaselineskip=11pt
   \setbox\strutbox=\hbox{\vrule height8pt depth 3pt width0pt}%
   \let\big=\eightbig \normalbaselines\rm}
\catcode`@=11
\def\ninebig#1{{\hbox{$\textfont0=\tenrm\textfont2=\tensy
  \left#1\vbox to7.25pt{}\right.\n@space$}}}
\catcode`@=12
\let\Smallskip=\smallskip
\def\SMALL{\ninepoint\def\medskip{}\def\Bigbreak{\Smallskip}\def\smallskip{}}

% MAGNIFICATION
\magnification=\magstep1

% QED MACROS
\def\umlaut#1{\accent "7F #1}
\let\doublequote="
%\catcode`"=13
%\def"{}
\def\a#1.#2"{\Medbreak\par\noindent{\it Ax}\ $#1$:\quad$#2 $.\medskip\par}
\def\anull{}
\def\tnull{}
\def\dnull{}
\def\aaa#1.#2"{$#1$:\quad$#2 $}
\def\t#1.#2"{\Medbreak\par\noindent{\it Th}\ $#1$:\quad$#2 $.\medskip\par}
\def\tw#1.#2"{\Bigbreak\par\noindent{\it Th}\ $#1$:\quad$#2 $, where:\medskip\par}
\def\d#1.#2"{\Bigbreak\par\noindent{\it Df\/}\ $#1$:\quad$#2 $.\medskip\par}
\def\dw#1.#2"{\Bigbreak\par\noindent{\it Df\/}\ $#1$:\quad$#2 $, where:\medskip\par}
\def\ddd#1.#2"{{\it Df\/}\ $#1$:\quad$#2 $}
\def\l#1.#2"{(.$#1$)~$#2 $}
\def\ll#1.{(.#1)}
\def\L#1.#2"{.$#1$)~$#2 $}
\def\abb#1?{\br Let\ .0)\er\ #1.\ \br Then{\colon}\er\hfil\break\indent}
\newif\ifproof
\let\lbracket=[
\catcode`[=\active
\def[{\ifproof\{\else\lbracket\fi}
\let\rbracket=]
\catcode`]=\active
\def]{\ifproof\}\else\rbracket\fi}
\def\p#1.#2"{\ifdim\lastskip<\medskipamount\removelastskip\penalty3000\smallskip\fi\begingroup\prooftrue\binoppenalty=1000\baselineskip=11pt\scriptfont0=\ninerm\scriptfont1=\ninei\scriptfont2=\ninesy\scriptscriptfont0=\sixrm\scriptscriptfont1=\sixi\scriptscriptfont2=\sixsy\ninerm\par$\scriptstyle #2\!\!\!.$\par\endgroup\prooffalse}
\def\pf#1.#2"{\ifdim\lastskip<\bigskipamount\removelastskip\penalty3000\smallskip\fi\begingroup\prooftrue\binoppenalty=1000\baselineskip=11pt\scriptfont0=\ninerm\scriptfont1=\ninei\scriptfont2=\ninesy\scriptscriptfont0=\sixrm\scriptscriptfont1=\sixi\scriptscriptfont2=\sixsy\ninerm\par$\scriptstyle #2$\par\endgroup\prooffalse}
\def\\{\allowbreak\mskip 8mu plus 16mu minus 4mu}
\let\semicolon=;
\catcode`;=\active
\def;{\ifmmode\semicolon\penalty1000\mskip.1mu\penalty1000\relax\else\semicolon\fi}
\let\colon=:
%%%%%%%%%%%%%%%%%%%%%%%\catcode`:=\active
%%%%%%%%%%%%%%%%%%%%%%%\def:{{\colon}}
\let\comma=,
\catcode`,=\active
\def,{\ifmmode\comma\penalty8000\relax\else\comma\fi}
\let\slash=/
\def\sslash{$\scriptstyle\slash$}
\def\tild{$\scriptstyle\sim$}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\catcode`/=\active
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%\def/{}
\let\acute=\'
%\def\'#1'{{}$#1${}}
\def\thm{\hbox{\it thm}}
\def\(#1,{_{#1}(}
\let\dollar=\$
\def\$#1:{}
\let\lowbar=\_
%\def\_{\lowbar\hskip1pt\discretionary{}{}{}}
\def\_{\allowbreak\ }
\def\upto{\allowbreak\hbox{--}\allowbreak}
\def\iff{\allowbreak\hskip8pt plus2pt minus3pt\mathrel{\hbox{$\leftrightarrow$}}\hskip8pt plus2pt minus3pt}
\def\iffF{\allowbreak\leftrightarrow}
\def\imp{\allowbreak\hskip8pt plus2pt minus3pt\mathrel{\hbox{$\rightarrow$}}\hskip8pt plus2pt minus3pt}
\def\impP{\allowbreak\rightarrow}
\def\andD{\allowbreak\mathrel{\hskip1pt\&\hskip1pt}}
\def\and{\allowbreak\hskip7pt plus2pt minus3pt\mathrel{\&}\hskip7pt plus2pt minus3pt}
\def\orR{\allowbreak\kern1pt\lor\kern1.25pt}
\def\or{\allowbreak\hskip7pt plus2pt minus3pt\mathrel{\hbox{$\vee$}}\hskip7pt plus2pt minus3pt}
\def\leE{{\scriptstyle\le}}
\def\ltT{{\scriptstyle<}}
\def\inN{{\scriptstyle\in}}
\def\EC{{\rm EC}}
\def\UC{{\rm UC}}
\let\graveaccent=\`
%\def\`#1{(.#1)}
\let\dotaccent=\.
\def\.{\cdot}
\def\:#1:#2:#3:#4:#5:#6:#7:{#1\{\,#4#5#6\allowbreak\,\colon\allowbreak\,#7\,\}}
\def\?#1;#2;#3;#4;#5;#6;#7;{\{\,\langle#3,#4\rangle\,\colon\,#3\in#5\and#6\and#7\,\}}
\def\@#1;#2;#3;#4;#5;{\{\,\langle#3,#4\rangle\allowbreak\,\colon\,#3\in#5\,\}}

% REGISTERS
\newcount\firstpage
\newcount\footno
\newcount\secno
\newtoks\chaptername
\newtoks\sectionname
\newwrite\raw
\newwrite\tabcon
\newif\ifindexmode

% FORMATING
\predisplaypenalty=0
\def\foot#1{\global\advance\footno by 1
  {\baselineskip=9pt 
	\frenchspacing
    \setbox\strutbox=\hbox{\vrule height7pt depth2pt width0pt}%
	\def\textindent##1{\indent\llap{##1}}%
	\def\sl{\eightsl}\def\bf{\eightbf}\def\rm{\eightrm}%
	\def\it{\eightit}\def\tt{\eighttt}%
	\eightrm\footnote{$^{\hbox{{\eightrm\the\footno}}}$}{#1}}}
\def\footnoterule{\kern-3pt \hrule width 2truein height 0pt}
\hsize=11cm
\vsize=17.5cm 
%\voffset=2\baselineskip
\hoffset=1.7truecm
%\headline={\Headline}
%\footline={\Footline}
%\def\Headline{\ifnum\firstpage=\pageno \hfil \else\ifodd\pageno%
   %\righthead\else\lefthead\fi\fi}
%\def\Footline{\ifnum\firstpage=\pageno \hss\tenrm\folio\hss \else{}\fi}
%\newif\ifrighthead
%\def\lefthead{\tenrm\folio\hfil{\eightrm CHAPTER \chapno.\ \ \uppercase\expandafter{\the\chaptername}}\hfil}
%\def\righthead{\ifrighthead\hfil{\eightrm{\chapno.\botmark}}%
   %\hfil\tenrm\folio\else\lefthead\fi}
%\let\chapno=0
%\def\chap#1.#2{\chaptername={#2} \firstpage=\pageno 
    %\footno=0 \def\chapno{#1}
   %\hrule width0pt depth1.5cm
   %\centerline{\tenrm CHAPTER\ #1}\vskip .45cm
   %\centerline{\bigrm #2}\vskip 1cm \ifindexmode\write\tabcon%
   %{#1\  #2 \the\count0}\fi}
%\def\section#1{\rightheadtrue\forwardtrue\def\sectionname{\eightrm\uppercase{#1}}\global\advance\secno by 1\bigbreak\noindent{\bf\the\secno.\  #1}\mark{\the\secno\ \ \sectionname}\medskip%
   %\ifindexmode\write\tabcon{#1 \the\count0}\fi\nobreak}
%\def\footnoterule{}
%\skip\footins=\medskipamount
\def\poetry{\smallbreak\parindent=40pt \baselineskip=11pt
  \setbox\strutbox=\hbox{\vrule height8pt depth3pt width 0pt}%
   \obeylines\ninerm}% LEAVE BLANK LINE AND TYPE {\poetry <poem>
%                                                                 }
%\def\endchap{\ifodd\pageno\vfill\supereject\headline={\hfil}\eject\line{}\vfil\eject\else\vfill\supereject\fi\headline={\Headline}\rightheadfalse\secno=0\footno=0}

% VERBATIM
\def\uncatcodespecials{\def\do##1{\catcode`##1=12 }\dospecials}
\def\setupverbatim{\eighttt\hyphenpenalty=10000\def\par{\leavevmode\endgraf}\obeylines\uncatcodespecials\catcode`"=12\catcode`/=12\def~{\hbox{\eighttt\char'176}}\def/{\hbox{\eighttt\char'057}}\obeyspaces}
{\obeyspaces\global\let =\ }
\def\|{\begingroup\setupverbatim\doverbatim}
\def\doverbatim#1#2{\def\next##1#1#2{##1\endgroup}\next}

% INDEXING
\def\ind#1{\ifindexmode\write\raw{#1, \the\count0 }#1\else#1\fi}
\def\sind#1{\ifindexmode\write\raw{#1, \the\count0 }\fi}
\def\ii#1.{\ifindexmode\write\raw{#1, \the\count0 }{\it#1}%
   \else{\it#1}\fi}
\def\b[#1]{\sind{#1]}[#1]}

% TEXT MACROS
\def\Lseq#1.#2{$\rm#1_1$,~\dots,~$\rm#1_#2$}
\def\secsign{\mathhexbox 278}
\def\pmb#1{\setbox0=\hbox{#1}\kern-.025em\copy0\kern-\wd0 \kern.05em\copy0\kern-\wd0 \kern-.025em\raise.0433em\box0 }
\def\SMASH{{\pmb{$\;\Smash$}}}
\def\smasH{{$\scriptstyle\Smash$}}
\newif\ifforward
\def\Medbreak{\forwardtrue\medbreak}
\def\Bigbreak{\ifforward\medbreak\else\bigbreak\fi\forwardfalse}
\long\def\Omit#1{}

% TEXT OR MATH MACROS
\def\nn{\hbox{{\sans N}}}
\def\qq{\hbox{{\sans Q}}}
\def\ll{\hbox{{\sans L}}}
\def\ss{\hbox{{\sans S}}}
\def\smallss{\hbox{{\eightsans S}}}
\def\smallssz{\hbox{{\eightsans S}}^0}
\def\vdss{\vdash_{\smallss}}
\def\vT{\vdash_{\ro T}}
\def\vdsss{\vdash_{\smallss^*}}
\def\vdssz{\vdash_{\smallss^0}}
\def\ssb{\hbox{$\overline{\ss}$}}
\def\ssbz{\hbox{$\overline{\ss}\,^0$}}
\def\sss{\hbox{$\ss^*$}}
\def\ssz{\hbox{$\ss^0$}}
\def\qo{$\hbox{\sans Q}_0$}
\def\qob{$\overline{\hbox{\sans Q}}_0$}
\def\so{$\hbox{\sans S}_0$}
\def\sh#1{[Sh,~\S#1]}
\def\ul{\hbox{\tenmsa\char"70}}
\def\ur{\hbox{\tenmsa\char"71}}
\def\phiI{\phi^{\phantom\prime}_{\ro I}}
\def\down{^{\phantom\prime}}
\def\phip{\phi^+}
\def\phit{\phi^{\scriptscriptstyle\,\bullet\,}}
\def\phiE{\phi^{\scriptscriptstyle\uparrow}}
\def\cite#1{[{\ninerm PA~Ch.~#1}]}
\let\phi=\varphi
\def\N{\hbox{\bbb N}}
\let\hyphen=\-
\def\-{\relax\hyphen}
\def\cseq#1#2#3{#1_1#2\cdots#2#1_#3}
\def\lseq#1#2#3{#1_1#2\ldots#2#1_#3}
%\def\bull{\vrule height .9ex width .8ex depth -.1ex }
%\def\bul{\vrule height .7ex width .6ex depth -.1ex }
\def\ro#1{{\rm #1}}
\def\T{\hbox{\sans t}}
\def\f{\hbox{\sans f}}
\def\UU{\hbox{$\rm U_I$}}
\def\I{{\rm I}}
\def\PP{{\tenss P}}
\def\EBA{{\tenss EBA}}
\def\QQ{\hbox{$\rm\bar Q$}}

\def\ti{\hbox{$\rm T\hskip1pt^\omega$}}
\def\len#1{|#1|}
\def\vti{\vdash_{\ro T^\omega}}
\def\bul{\hfill\hbox{\tenmsa\char3}}
\def\tl{\hbox{$\rm T^\lambda$}}
\def\tlm{\hbox{$\rm T^{\lambda-1}$}}
\def\vtl{\vdash_{\ro T^\lambda}}
\def\vtz{\vdash_{\ro T^0}}
\def\vtlp{\vdash_{\ro T^{\lambda+1}}}
\def\Theorem{T{\eightrm HEOREM~}}
\def\ds{\displaystyle}
\def\ax{{\it Ax. \quad }}
\def\df#1 {\medskip\par\noindent #1 {\it Def.\quad}}
\def\th#1 {\medskip\par\noindent #1 {\it Thm.\quad}}
\def\ax#1 {\medskip\par\noindent #1 {\it Ax.\quad}}
\def\dff{{\it Def}.\ }
\def\pf{\medskip\par{\it Proof. }}
\def\pff{\medskip\par{\it Proof scheme. }}
\def\noin{\noindent}
\def\noi{\medskip\par\noindent}
\def\qd{\medskip\par\qquad}
\def\op{\oplus}
\def\ep{\epsilon}
\def\od{\odot}
\def\pr{\preceq}
\def\heq{\mathrel{\hat=}}
\def\hpp{{\hat{\scriptstyle\preceq}}}
\def\hpr{\mathrel{\hat\preceq}}
\def\hP{\hbox{\rm\^P}}
\def\hop{\mathbin{\hat\oplus}}
\def\hod{\mathbin{\hat\odot}}
\def\hep{\hat\ep}
\def\hz{\hat{\0}}
\def\ho{\hat{\1}}
\def\hor{\hat\vee}
\def\hneg{\hat\neg}
\def\phic{\ro C}
\def\phio{\ro C^1}
\def\phiw{\ro C^2}
\def\phie{\ro C^3}
\def\0{\hbox{o}}
\def\1{\hbox{\hskip1pt\i\hskip1.5pt}}
\def\pp{{\scriptstyle\preceq}}
\def\tr{^{{\rm tr}}}
\def\arith#1.{\ul{\rm#1}\ur}
\def\vdashh{\vdash^\star}
\def\uu{^\#}
\def\true{\hbox{true}}

\def\evft{encodes a variable-free term}
\def\ecf{encodes a closed formula}
\def\eti{encodes a true inequality}
\def\ete{encodes a true equality}
\def\etaf{encodes a true atomic formula}
\def\etvff{encodes a true variable-free formula}
\def\easo{encodes an atomic subformula of }
\def\evff{encodes a variable-free formula}
\def\etof{encodes a true open formula}
\def\evff{encodes a variable-free formula}

\def\tg{$\Theta_\gamma$}
\def\tgo{$\Theta_{\gamma+1}$}
\def\tgobb{$\Theta_{\gamma+1}(b)$}
\def\tgb{$\rm\Theta_\gamma(b)$}
\def\tgbb{$\Theta_\gamma(b)$}
\def\sg{$\Sigma_\gamma$}
\def\sgo{$\Sigma_{\gamma+1}$}
\def\sgobb{$\Sigma_{\gamma+1}(b)$}
\def\sgb{$\rm\Sigma_\gamma(b)$}
\def\sgbb{$\Sigma_\gamma(b)$}

\def\si{\hbox{\it string-ind }}
\def\ffor{\hbox{\quad for \quad}}
\def\GG{$\rm\ul G\ur$}
\long\def\omit#1{}
%REFERENCING

\def\R#1.{\medskip\par\noindent(#1)\qquad}
\def\r#1.{(#1)}

