Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
% (find-angg "LATEX/2009projections.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009projections.tex && latex    2009projections.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2009projections.tex && pdflatex 2009projections.tex"))
% (eev "cd ~/LATEX/ && Scp 2009projections.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (find-dvipage "~/LATEX/2009projections.dvi")
% (find-pspage  "~/LATEX/2009projections.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2009projections.ps 2009projections.dvi")
% (find-pspage  "~/LATEX/2009projections.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage  "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2009projections.pdf" (ee-twupfile "LATEX/2009projections.pdf") 'over)
% (ee-cp "~/LATEX/2009projections.pdf" (ee-twusfile "LATEX/2009projections.pdf") 'over)

\documentclass[oneside]{book}
\usepackage[latin1]{inputenc}
\usepackage{edrx08}       % (find-dn4ex "edrx08.sty")
%L process "edrx08.sty"  -- (find-dn4ex "edrx08.sty")
\input edrxheadfoot.tex   % (find-dn4ex "edrxheadfoot.tex")
\begin{document}

\input 2009projections.dnt

%*
% (eedn4-51-bounded)

Index of the slides:
\msk
% To update the list of slides uncomment this line:
%\makelos{tmp.los}
% then rerun LaTeX on this file, and insert the contents of "tmp.los"
% below, by hand (i.e., with "insert-file"):
% (find-fline "tmp.los")
% (insert-file "tmp.los")

%D diagram ??
%D 2Dx       100  +20    +20     +20  +20
%D 2D  100          a杗,b步|-c每
%D 2D
%D 2D  +30 a,b|-c        c每       A,B|-C
%D 2D
%D 2D  +20        c              C
%D 2D
%D ((      a杗,b步|-c每	     #   0
%D    a,b|-c   c每   A,B|-C  # 1 2 3
%D           c     C         #  4 5
%D    @ 0 @ 1 => .plabel= l _:'
%D    @ 0 @ 2 => .plabel= l _\vdash'
%D    @ 0 @ 3 => .plabel= r _:
%D    @ 1 @ 4 => .plabel= b _\vdash'
%D    @ 2 @ 4 => .plabel= b _:
%D    @ 2 @ 5 => .plabel= b _:'
%D    @ 3 @ 5 => .plabel= b _\vdash'
%D ))
%D enddiagram
%D
$$\diag{??}$$

Other projections:

$_{ζ}$ - erase the vector sign from contexts

$_{T_d}$ - erase the lists of dependencies from type names

$_{t_d}$ - erase the lists of dependencies from term names

$_=$ - compress a whole tree into a double-bar derivation

$_{砸sw}}$ - project on the syntactical world

$_{砸mc}}$ - drop some weakenings to force minimal contexts

$_{砸var}}$ - erase the subtrees that are above `var' rules

$_{砸pres}}$ - pretend that the hyp.\ preservation isos and cleavage isos are equalities

\def\piveca{_{ζ}}
\def\piTd{_{T_d}}
\def\pitd{_{t_d}}
\def\pidbar{_=}
\def\pisw{_{砸sw}}}
\def\pimc{_{砸mc}}}
\def\pivar{_{砸var}}}
\def\pipres{_{砸pres}}}

\msk

Notes:

$\piveca$ simplifies the rules and make them look more restricted

$\piTd$ simplifies the rules and make them look more restricted

$\piTd$ and $\pitd$ make more sense when we allow impurities

$\pisw$ requires defining protothings

$\pimc$ may strengthen (slightly) a conclsuion

$\pivar$ may hide hypotheses (solution: split trees)

\msk

Translations:

Use long names for variables

Use long names for terms

Expand the long names in terms

Replace the long names for variables by standard names

Erase the primes in long names (this is bad, it collapses things!)

Convert logic to $$-calculus

Convert $$-calculus to logic



%*

\end{document}

% Local Variables:
% coding:           raw-text-unix
% ee-anchor-format: "«%s»"
% End: