% (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¨A,b¨B|-c¨C
%D 2D
%D 2D  +30 a,b|-c        c¨C       A,B|-C
%D 2D
%D 2D  +20        c              C
%D 2D
%D ((      a¨A,b¨B|-c¨C	     #   0
%D    a,b|-c   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:

$_{£a}$ - 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{_{£a}}
\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: