% (setq tex-open-quote "\"" tex-close-quote "\"")
% (find-fline "~/ZHTML/escripts/tex.e")
%
% «.twocol»  (to "twocol")

%\documentclass{book}
\documentclass[oneside]{book}
\usepackage[cp850]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{mathrsfs}
\usepackage{stmaryrd}

% (find-es "tex" "bussproofs")
\usepackage{bussproofs}
\def\ScoreOverhang{0pt}

% Old way:
% Tive que hardcodear esse valor, nÆo sei qual o jeito standard de
% encontr�-lo...
% (find-fline "/etc/texmf/language.dat" "portu")
%
%\language3
%\usepackage{portuges}
%
% New way (from babel's user.dvi):
%\usepackage[portuges,english]{babel}
\usepackage[brazilian,english]{babel}

%\usepackage{bbold}
% (find-fline "/usr/lib/texmf/tex/latex/misc/bbold.sty")
% (find-fline "/usr/lib/texmf/source/latex/amsfonts/amsfonts.dtx" "mathbb")
% (find-fline "/usr/lib/texmf/source/latex/psnfss/mathtime.dtx" "Bbb")
%\newcommand{\bblowfamily}{\fontencoding{U}\fontfamily{bbold}\selectfont}
%\newcommand{\textbblow}[1]{{\bbfamily#1}}
%\DeclareMathAlphabet{\mathbblow}{U}{bbold}{m}{n}
%
% (find-fline "/usr/lib/texmf/tex/latex/bbm/bbm.sty")
\DeclareMathAlphabet{\mathbblow}{U}{bbm}{m}{n}
\SetMathAlphabet\mathbblow{bold}{U}{bbm}{bx}{n}

% (find-es "tex" "rsfs")
\usepackage{mathrsfs}

\usepackage{graphicx}
\def\epsscale{0.8}
%\def\eps#1{\includegraphics[scale=0.8]{#1.eps}}
\def\eps#1{\includegraphics[scale=\epsscale]{eps/#1.eps}}
\def\epsn#1{
  \begin{array}[b]{c}
    \eps{#1} \\
    \text{#1} \\
  \end{array}
}
%\usepackage[arrow,curve]{xy}
%\usepackage[ps,xdvi,arrow,matrix,curve]{xy}
%\usepackage{vgatim}
\usepackage{proof.edrx}
%
% (find-ptfile "proofs/boxproof.tex")
% (find-fline "/usr/lib/texmf/source/amstex/doc/amsguide.tex" "loadeurm")
%
% A quick hack to write the filename, date and time at the footer.
%
% p.11=22 (find-lsrcfile "lshort/src/things.tex" "pagestyle")
% source2e p.328=337 (find-lsrcfile "base/ltpage.dtx" "pagestyle")
% classes p.19=19 (find-lsrcfile "base/classes.dtx" "The page style")
% (find-lsrcfile "base/classes.dtx" "<!book>\\pagestyle{plain}")
% (find-lsrcfile "base/classes.dtx" "\\def\\ps@headings")
% (find-lsrcfile "base/book.cls" "if@twoside")
% (find-lsrcfile "base/nfssfont.tex" "time")
%
\makeatletter
\newcount\m \newcount\n
\def\twodigits#1{\ifnum #1<10 0\fi \number#1}
\def\hours{\n=\time \divide\n 60
  \m=-\n \multiply\m 60 \advance\m \time
  \twodigits\n:\twodigits\m}
%
\def\draftfooter{\jobname{} \today{} \hours}
\def\footertext{\draftfooter}
\def\ps@headings{%
  \def\@oddfoot{\hfil \footertext \hfil}
  \let\@evenfoot\@oddfoot
  \def\@oddhead{{\slshape\rightmark}\hfil\thepage}%
  \let\@mkboth\markboth
  \def\chaptermark##1{%
    \markright {\MakeUppercase{%
      \ifnum \c@secnumdepth >\m@ne
        \if@mainmatter
          \@chapapp\ \thechapter. \ %
        \fi
      \fi
      ##1}}}}
\ps@headings
\makeatother
%
\def\shorttoday{%
  \number\year%
  \ifcase\month\or jan\or feb\or mar\or apr\or may\or
     jun\or jul\or aug\or sep\or oct\or nov\or dec\fi
  \twodigits\day}
\def\edrxnotesfooter#1{{\tiny #1 (typeset \shorttoday{} \hours)
  {\tt edrx@mat.puc-rio.br}}}
\def\edrxnotes#1{\gdef\footertext{\edrxnotesfooter{#1}}}
%
% (find-es "tex" "edrxnotes")
% (find-lsrcfile "../generic/babel/portuges.dtx" "dateportuges")




% Setas,
%
\newcommand\ito{\hookrightarrow}
\newcommand\isoto{\underset{iso}{\to}}
\newcommand\epito{{\twoheadrightarrow}}
\newcommand\bij{\leftrightarrow}
\newcommand\toto{\rightrightarrows}
\newcommand\functo{\Rightarrow}
\newcommand\ton[1]{\overset{#1}{\to}}
\newcommand\xton[1]{\xrightarrow{#1}}
\newcommand\iton[1]{\overset{#1}{\ito}}
\newcommand\TNto{\overset{.}{\to}}
\newcommand\idto{\overset{id}{\to}}
\newcommand\vaipra{\quad\Longrightarrow\quad}
\newcommand\funto{\Rightarrow}
\newcommand\funton[1]{\overset{#1}\Rightarrow}
\newcommand\tnto{\ton{\bullet}}
%\newcommand\iff{\Leftrightarrow}
\newcommand\Bij{\Leftrightarrow}
\newcommand\funot{\Leftarrow}
\newcommand\dnto{\downarrow}
\newcommand\upto{\uparrow}
\newcommand\dnfunto{\Downarrow}
\newcommand\upfunto{\Uparrow}
\newcommand\monicto{\rightarrowtail}
%
% (find-lsrcfile "base/fontdef.dtx" "rightarrow")

\newcommand\Set{\mathbf{Set}}
\newcommand\Sets{\mathbf{Sets}}
\newcommand\E{\mathbf{E}}
\newcommand\T{\mathbf{T}}
\newcommand\N{\mathbb{N}}
\newcommand\R{\mathbb{R}}
\newcommand\Z{\mathbb{Z}}

\renewcommand\O{\mathbf{O}}
\renewcommand\o{\mathbf{o}}
\renewcommand\t{\tau}
\newcommand\typ{\mathbf{t}}
%

% Quantificadores,
%
\newcommand\Exob[1]{\mathop{\exists\;{#1}}}
\newcommand\Exbangob[1]{\mathop{\exists!\;{#1}}}
\newcommand\Faob[1]{\mathop{\forall\;{#1}}}
\newcommand\Ex{\exists}
\newcommand\Exbang{\exists!}
\newcommand\Fa{\forall}

\newcommand\virg{{,\,\,}}
%

% NSA e SSA,
%
%\newcommand{\ii}{\iota}
\newcommand{\ii}{\mathbblow{i}}
\newcommand{\I}{\mathbb{I}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\cofiN}{\mathcal{N}}
\newcommand{\U}{\mathcal{U}}
\newcommand{\OO}{\mathcal{O}}
\newcommand{\jj}{\mathbblow{j}}

\def\littlo{o}
\def\bigO{O}


\newcommand{\void}{\varnothing}
\newcommand\id{\mathrm{id}}
\newcommand\ev{\mathrm{ev}}
\newcommand\cur{\mathrm{cur}}
\newcommand\dom{\mathrm{dom}}
\newcommand\cod{\mathrm{cod}}
%
\newcommand\bsl{\backslash}
\def\phi{\varphi}
\def\False{\Finv}

% (find-knuthfile "tex/texbook.tex" "Active")
\catcode`°=13 \def°{\mathstrut}
\catcode`ª=13 \defª{\neg}
\catcode`�=13 \def�{\times}
% \catcode`�=13 \def�{${}^\underline{\mathrm{o}}$}
\def�{\square}
\defè{\lozenge}
\defì{\Fa}
\defí{\Ex}
\defõ{\top}
\def�{\bot}
\defú{\cdot}
\def×{\in}
\def�{\lambda}
\def�{\circ}
\defÏ{\otimes}
\def�{\oplus}
%\catcode`�=13
\def�{\multimap}
\def�{\bullet}

\def\aa{\alpha}
\def\bb{\beta}
\def\cc{\gamma}
\def\dd{\delta}
\def\ee{\epsilon}
\def\kk{\kappa}
\def\ww{\omega}
\def\Om{\Omega}

\def\ot{\leftarrow}

% (find-fline "~/MTA/vtutil" "setglyphs")
% (setglyphs ?\^R nil 18 ?\^E nil 5 ?\^T nil 20 ?\^D nil 4)
\catcode`=13 \def{\delta}
\catcode`=13 \def{\epsilon}
\catcode`=13 \def{\rho}
\catcode`=13 \def{\theta}
\catcode`=13 \def{\to}
\catcode`=13 \def{\ot}
\catcode`=13 \def{\land}
\catcode`∨=13 \def∨{\lor}
\catcode`=13 \def{\amalg}
%
\catcode`�=13 \def�{\partial}
\catcode`�=13 \def�{\nabla}
%\catcode`�=13 \def�{\}
\catcode`�=13 \def�{\Omega}
\catcode`ê=13 \defê{\nu}
\catcode`�=13 \def�{\sqcap}
\catcode`Ó=13 \defÓ{\sqcup}

\catcode`�=13 \def�{\int}
\catcode`ü=13 \defü{^{-1}}
\catcode`�=13 \def�{\cap}
\catcode`ç=13 \defç{\cup}

\catcode`=13 \def{\mathbf}
\catcode`ò=13 \defò{\infty}
\catcode`�=13\def�{\ulcorner}
\catcode`�=13\def�{\urcorner}
\catcode`�=13 \def�{\mathrm}
\def\sto{\Rrightarrow}          % syntactic "to"



% �rvores,
%
% (find-knuthfile "tex/texbook.tex" "csname")
% (find-knuthfile "tex/texbook.tex" "*|\\csname|")
\def\ded#1{\csname ded-#1\endcsname}
\def\defded#1#2{\expandafter\def\csname ded-#1\endcsname{#2}}

% (find-knuthfile "tex/texbook.tex" "|\\ifundefined#1|")
% (find-knuthfile "tex/texbook.tex" "test if tokens agree")
%
\def\ifdedundefined#1{\expandafter\ifx\csname ded-#1\endcsname\relax}
\def\ded#1{\ifdedundefined{#1}
    \errmessage{UNDEFINED DEDUCTION: #1}
  \else
    \csname ded-#1\endcsname
  \fi
}

% Set_A,
%
\newcommand\A{\mathcal{A}}
\def\Aregras{\A^{\to,\land,\lor,�}}
\newcommand\SetA{{\bf Set_{\mathcal A}}}

\def\Aplus{{\A^\ast}}
\def\LA{\Lambda_\A}



\def\lbe{{\lambda\beta\eta}}
%\def\lbeto{\underset{\lbe}{\epito}}
\def\lbeto{\epito}
\def\lbeot{{\twoheadleftarrow}}


\def\lbes{{\lambda\beta\eta^\ast}}
%\def\lbeto{{\epito^\ast}}



%\newcommand\n{\mathcal{n}}
%\newcommand\r{\mathcal{r}}
%\newcommand\Set{{\bf Set}}
%\newcommand\SetU{{\bf Set^{\mathcal U}}}
%\newcommand\SetF{{\bf Set^{\mathcal F}}}
\newcommand\SetI{{\Set^{\mathbb{I}}}}
\newcommand\SetF{{\Set^{\mathcal{F}}}}
\newcommand\SetU{{\Set^{\mathcal{U}}}}
\newcommand\SetP{{\Set^{\mathbf{P}}}}
\newcommand\SetM{{\Set^{\mathbf{M}}}}
\newcommand\SetC{{\Set^{\bf C}}}
\newcommand\Top{{\bf Top}}
\newcommand\PTop{{\bf PTop}}
\newcommand\Vect{{\bf Vect}}
\newcommand\Grp{{\bf Grp}}
\newcommand\Mon{{\bf Mon}}
%\newcommand\catC{\mathcal{C}}
%\newcommand\catD{\mathcal{D}}
%\newcommand\catE{\mathcal{E}}
\newcommand\catC{\mathbf{C}}
\newcommand\catD{\mathbf{D}}
\newcommand\catE{\mathbf{E}}
\newcommand\catP{\mathbf{P}}
\newcommand\catA{\mathbf{A}}
\newcommand\catB{\mathbf{B}}
\newcommand\OX{{\mathcal{O}_X}}

\newcommand\calC{\mathcal{C}}
\newcommand\calD{\mathcal{D}}
\newcommand\calE{\mathcal{E}}
\newcommand\calA{\mathcal{A}}
\newcommand\calB{\mathcal{B}}

% Coisas para o cap�tulo sobre an�lise nÆo-standard
%
% (find-lsrcfile "amslatex/math/amsmath.dtx" "sideset#1")
\makeatletter
\def\sidesetscript#1#2#3{%
  \@mathmeasure\z@\scriptstyle{#3}%
  \global\setbox\@ne\vbox to\ht\z@{}\dp\@ne\dp\z@
  \setbox\tw@\box\@ne
  \@mathmeasure4\scriptstyle{\copy\tw@#1}%
  \@mathmeasure6\scriptstyle{#3\nolimits#2}%
  \dimen@-\wd6 \advance\dimen@\wd4 \advance\dimen@\wd\z@
  \hbox to\dimen@{}\mathop{\kern-\dimen@\box4\box6}%
}
\makeatother
%
\newcommand\B{\mathcal{B}}
\newcommand\interfin{\bigcap_{\rm fin}}
\newcommand\ns[1]{\sideset{^*}{}{\mathop{#1}}}
\newcommand\nss[1]{\sidesetscript{^*}{}{\mathop{#1}}}
\newcommand\raiseset{\mathord{\uparrow}}
\newcommand\Pts{\mathcal{P}}


% Combinadores,
%
\def\cbS{\mathbf{S}}
\def\cbK{\mathbf{K}}
\def\cbI{\mathbf{I}}
\def\cbP{\mathbf{P}}
\def\cbD{\mathbf{D}}
\def\cbV{\mathbf{V}}
\def\cbT{\mathbf{T}}
\def\cbF{\mathbf{F}}
\def\SKI{\mathbf{SKI}}
\def\app{\operatorname{app}}


% Conectivos,
%
% (find-fline "/usr/lib/texmf/tex/latex/misc/program.sty" "poor man's bold")
% (find-fline "/usr/lib/texmf/tex/latex/amslatex/amsbsy.sty" "pmb")
% (find-fline "/usr/lib/texmf/tex/latex/amslatex/amstex.sty" "pmb")
% (find-fline "/usr/lib/texmf/tex/latex/tools/bm.sty" "pmb")
%\def\pmb{\protect\ppmb}
%\def\ppmb#1{\setbox0=\hbox{\bf #1}
%            \kern-.025em\copy0\kern-\wd0
%           \kern.05em\copy0\kern-\wd0
%           \kern-.025em\raise.0433em\box0 }}
\def\LAND{\pmb{\land}}
\def\LOR{\pmb{\lor}}
\def\TO{\pmb{\to}}
\def\TO{\funto}



% Regras de dedu�Æo,
%
\def\dedrulename#1#2{#1{\rm #2}}
\def\andI{{\dedrulename\land{I}}}
\def\andE#1{{\dedrulename\land{E_#1}}}
\def\orI#1{{\dedrulename\lor{I_#1}}}
\def\orE{{\dedrulename\lor{E}}}
\def\toI{{\dedrulename{\to\!\!}{I}}}
\def\toE{{\dedrulename{\to\!\!}{E}}}
\def\topI{{\dedrulename\top{I}}}
\def\botE{{\dedrulename\bot{E}}}
\def\FaI{{\dedrulename\Fa{I}}}
\def\FaE{{\dedrulename\Fa{E}}}
\def\ExI{{\dedrulename\Ex{I}}}
\def\ExE{{\dedrulename\Ex{E}}}

\def\ruleF#1{{\mathrm{F}_{#1}}}

\def\ruleT#1#2{{\mathrm{T}_{#1}^{#2}}}          % \ruleT\DN\treeA
\def\ruleTe#1{{\mathrm{T\!e}_{#1}}}             % \ruleTe\DN
\def\ruleTDN{{\ruleT\DN{}}}
\def\ruleTCCC{{\ruleT\CCC{}}}

\def\DNT{{\DN\mathord+\ruleTDN}}
\def\CCCT{{\DN\mathord+\ruleTCCC}}
\def\DNminustoI{{\DN'\mathord-\setof{\toI}}}

\def\DN{{\rm DN}}
\def\SD{{\rm SD}}
\def\CCC{{\rm CCC}}
\def\treeA{{\mathsf{A}}}
\def\treeB{{\mathsf{B}}}
\def\diagD{{\mathsf{D}}}
\def\diagE{{\mathsf{E}}}

\def\TFI{{\rm TFI}}
\def\TFImp{{\rm TFImp}}

%\def\smallded#1#2{{{#1} \above 1.5pt {#2}}}
\def\smallded#1#2{\genfrac{}{}{1.5pt}{}{#1}{#2}}



% {array}s,
%
\def\hli{\mathstrut \\ \hline \mathstrut \\}
%
% (find-fline "/usr/lib/texmf/source/latex/base/lttab.dtx" "l,r,c")
% (find-fline "/usr/lib/texmf/source/latex/tools/array.dtx")

\def\alob{\allowbreak}


% Tipos,
%
\def\nn{\mathbblow{n}}
\def\r{\mathbblow{r}}
\def\z{\mathbblow{z}}
\def\lefto{\mathcal{L}}
\def\righto{\mathcal{R}}

\def\compr{\operatorname{compr}}
\def\Int{\operatorname{Int}}

\def\mon{{\mathop{[\;]}}}

\newcommand\setof[1]{\{\,#1\,\}}
%\newcommand\setofst[2]{\,\setof{{#1}\;|\;{#2}}\,}
\newcommand\setofst[2]{\{\,#1\;|\;#2\,\}}

\def\adj{\operatorname{adj}}

\def\conetr#1#2#3{(\O_{#3},\, #3 \to #1,\, #3 \to #2)}
\def\coneab#1{\conetr{a}{b}{#1}}


%%%
%
% 6: A �lgebra dos valores de verdade
%
%%%

\def\Props{\mathbb{P}}
\def\Patom{\Props_{\rm atom}}
\def\brkt{{[ú]}}
\def\Pbrkt{\Props_{\!/ \brkt}}
\def\Pbrktplic{\Props_{\!/ \brkt'}}
\def\Pbij{\Props_{\!/ \bij}}
\def\conseq{\operatorname{conseq}}
\def\Omantes#1{\Om_{\to #1}}
\def\Omdepois#1{\Om_{#1 \to}}

% Conjuntos parcialmente ordenados
%
% (find-fline "kripkealg.tex")
\def\cpoQuatro#1#2#3#4{{\unitlength=.1ex
\begin{picture}(15,34)
\put(0,0){\scriptsize #1}
\put(0,12){\scriptsize #2}
\put(6,24){\scriptsize #3}
\put(12,12){\scriptsize #4}
\end{picture}
}}
\def\cpoV#1#2#3{{\unitlength=.1ex
\begin{picture}(15,22)
\put(0,0){\scriptsize #1}
\put(6,12){\scriptsize #2}
\put(12,0){\scriptsize #3}
\end{picture}
}}
\def\cpoDois#1#2{{\genfrac{}{}{0pt}{}{#1}{#2}}}


%%%
%
% 7: An�lise nÆo-standard
%
%%%

\def\Eiplic{\E_{\ii'}}
\def\Explic{\E_{x'}}
\def\Eyplic{\E_{y'}}

\def\ddx{\frac{d}{dx}}


%%%
%
% 9: Onde gostar�amos de chegar
%
%%%

\def\dim{\operatorname{dim}}
\def\dimE#1{\dim \E_{#1}}




% Extras:

%\input oldgerm
\usepackage{oldgerm}

%\newcommand\gothfamily{\usefont{U}{ygoth}{m}{n}}
%\DeclareTextFontCommand{\textgoth}{\gothfamily}
%\newcommand\swabfamily{\usefont{U}{yswab}{m}{n}}
%\DeclareTextFontCommand{\textswab}{\swabfamily}
%\newcommand\frakfamily{\usefont{U}{yfrak}{m}{n}}
%\DeclareTextFontCommand{\textfrak}{\frakfamily}

\def\newpage{\vfill\break}

\newcommand\tnton[1]{\underset{#1}{\overset{\bullet}{\to}}}
%\newcommand\tnton[1]{\underset{#1}{\to}}



%%%%%
%
% 2001
%
%%%%%

\def\hom{\operatorname{hom}}
\def\Hom{\operatorname{Hom}}
\def\op{{\operatorname{op}}}
\def\und#1{{\underline{#1}}}
\def\Cat{\mathbf{Cat}}
\def\colim{{\operatorname{colim}}}
\def\Colim{{\operatorname{Colim}}}
\def\Lim{{\operatorname{Lim}}}




%%%%%
%
% two-column modes, for personal math notes
% 2000oct31
%
%%%%%

% «twocol»  (to ".twocol")
% (find-es "tex" "twocolumn")
% See also Kopka/Daly pp.196-- for info on defining environments.

\newenvironment{twocol}{}{}
\def\edrxtwocol{
  \renewenvironment{twocol}{
    \begin{multicols}{2}
    \setlength\columnseprule{.2pt}
  }{\end{multicols}
  }
}
\def\edrxscriptsize{\edrxtwocol \def\epsscale{0.6} \scriptsize}
\def\edrxtiny{\edrxtwocol \def\epsscale{0.4} \tiny}

% Now the commands "\edrxtiny" and "\edrxscriptsize" will set two very
% condensed two-column modes; you may need to add a "\usepackage{multicol}"
% command just after the "\begin{document}", though.




\endinput








% (find-lsrcfile "base/ltmiscen.dtx" "\\def\\begin")
% (find-lsrcfile "base/ltdefns.dtx" 509)
% (find-elnode "Narrowing" "(save-restriction")

% (progn (fundamental-mode) (setq fill-prefix "% "))
% (normal-mode)
% (cs 0)
% (cs 1)

% We have to tell Emacs to edit this file using the latin1 charset,
% even though all my TeXeable notes are in 850math; this is just
% because at this moment I am only supporting htmlization of latin1
% files, and I want the links to work in the html files... Of course,
% many chars here will look really weird after htmlization.


% Local Variables:
% coding:               no-conversion
% ee-delimiter-hash:    "\n#*\n"
% ee-delimiter-percent: "\n%*\n"
% ee-anchor-format:     "«%s»"
% ee-charset-indicator: "Ñ"
% End: