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

% «.ls-deriv»			(to "ls-deriv")
% «.pavlovic-quantifiers»	(to "pavlovic-quantifiers")
% «.seely-plc»			(to "seely-plc")
% «.seely-plc-trees»		(to "seely-plc-trees")
% «.seely-plc-trees-dnc»	(to "seely-plc-trees-dnc")
% «.local-set-theories»		(to "local-set-theories")
% «.local-set-theories-2»	(to "local-set-theories-2")
% «.notes-seelyhyp»		(to "notes-seelyhyp")
% «.luo»			(to "luo")

% Bater: Martin-Löf, Phoa, Reynolds, Wadler, Jacobs

\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 2008notations.dnt

%*
% (eedn4a-bounded)
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")


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")
\tocline {Quantifiers in Pavlovic's thesis} {2}
\tocline {A derivation from Lambek/Scott} {3}
\tocline {Seely's PLC paper} {4}
\tocline {Seely's PLC paper: trees} {5}
\tocline {Seely's PLC paper: trees, in DNC} {6}
\tocline {Local set theories} {7}
\tocline {Local set theories (1)} {8}
\tocline {Notes on reading SeelyHyp} {9}



\setlength{\parindent}{0em}

\newpage
% --------------------
% «pavlovic-quantifiers»  (to ".pavlovic-quantifiers")
% (s "Quantifiers in Pavlovic's thesis" "pavlovic-quantifiers")
\myslide {Quantifiers in Pavlovic's thesis} {pavlovic-quantifiers}

\def#1{{\color{red}#1}}

The rules $Iå, Eå, IÆ, EÆ$, as they appear in Pavlovi\v c:

%:
%:        [X:P:\DD']
%:       ============
%:       {q}:Q:\DD''
%:   --------------------Iå\DD'\DD''
%:   {X.q}:åXP.Q:\DD''
%:
%:   ^pav-IProd
%:
%:
%:   p:P:\DD'   r:åXP.Q(X):\DD''
%:   -------------------------------Eå\DD'\DD''
%:       {rp}:Q{[X:=p]}:\DD''
%:
%:       ^pav-EProd
%:
%:                 [X:P:\DD']
%:                 ==========
%:   {p:P:\DD'}     Q:\DD'     {q:Q(p):\DD''}
%:   ------------------------------------------IÆ\DD'\DD''
%:     {\ang{p,q}}:ÆXP.Q:\DD'
%:
%:     ^pav-ISum
%:
%:                           [X:P:\DD']
%:                         ===============
%:                         [Y:Q(X):\DD'']
%:                     ==========================
%:   r:ÆXP.Q:\DD''   {s(X,Y)}:S(\ang{X,Y}):\DD
%:   --------------------------------------------EÆ\DD'\DD''
%:        {Û(r,(X,Y).s)}:S(r):\DD
%:
%:        ^pav-ESum
%:
$$\ded{pav-IProd}$$

$$\ded{pav-EProd}$$

$$\ded{pav-ISum}$$

$$\ded{pav-ESum}$$

\msk

The same rules, but with a DNC-ish choice of letters:

%:    [b:B:']
%:    ========
%:    c:C:''
%:  -----------------Iå'''
%:  {b.c}:åbB.C:''
%:
%:  ^pav-IProd-abc
%:
%:  b':B:'  f:åbB.C(b):''
%:  -------------------------Eå'''
%:    fb:C[b:=b']:''
%:
%:    ^pav-EProd-abc
%:
%:          [b:B:']
%:          ========
%:  b':B:'   C:'     c:C(b'):''
%:  ------------------------------IÆ'''
%:     \ang{b',c}:ÆbB.C:'
%:
%:     ^pav-ISum-abc
%:
%:                           [b:B:']
%:                         ===============
%:                         [c:C(b):'']
%:                     ==========================
%:   p:ÆbB.C:''   {d(b,c)}:D(\ang{b,c}):'''
%:   --------------------------------------------EÆ'''
%:        {Û(p,(b,c).d)}:D(p):'''
%:
%:        ^pav-ESum-abc
%:
$$\ded{pav-IProd-abc}$$

$$\ded{pav-EProd-abc}$$

$$\ded{pav-ISum-abc}$$

$$\ded{pav-ESum-abc}$$


\newpage
% --------------------
% «ls-deriv»  (to ".ls-deriv")
% (s "A derivation from Lambek/Scott" "ls-deriv")
\myslide {A derivation from Lambek/Scott} {ls-deriv}


Lambek/Scott, p.131:

%:  _{xA}\phi(x)|-_{xA}\phi(x)        _{xA}\phi(x)|-_{xA}\phi(x)
%:  ------------------------------(2.4)   ------------------------------(2.4')
%:    _{xA}\phi(x)|-_x\phi(x)           \phi(x)|-_x_{xA}\phi(x)
%:    -------------------------------------------------------------(1.2)
%:              _{xA}\phi(x)|-_x_{xA}\phi(x)
%:              --------------------------------(1.4)
%:               _{xA}\phi(x)|-_{xA}\phi(x)
%:  
%:               ^LS-p131
%:
$$\ded{LS-p131}$$

%:         a;b.P|-b.P        a;b.P|-b.P
%:         ------------(E)   ------------(ίI)
%:         a,b;b.P|-P         a,b;P|-b.P
%:         -----------------------------
%:  a|-b       a,b;b.P|-b.P
%:  -------------------------(s)
%:       a;b.P|-b.P
%:  
%:       ^LS-p131-dnc
%:
$$\ded{LS-p131-dnc}$$

\newpage
% --------------------
% «seely-plc»  (to ".seely-plc")
% (s "Seely's PLC paper" "seely-plc")
\myslide {Seely's PLC paper} {seely-plc}

(1.1.1. {\sl Orders}) 1 and $$ are orders; if $A$ and $B$ are orders,
then $A×B$ and $^A$ are also orders.

(1.1.2. {\sl Operators}) In the following, ``$A$'' means $$ is an
operator of order $A$; the rest of the arity is left unspecified for
simplicity.

For each order, there is a countable set of variable operators (called
``indeterminates'').

$*1$. $$.

If $,   $, then $∧$ and $⊃$.

If $$ and $\aa$ is an indeterminate of order $A$, then $Æ\aaA$
and $å\aaA$.
 
($×I$) If $A$, $B$, then $\ang{,}A×B$.

($×E$) If $A×B$, then $_1A$, $_2B$.

($PI$) If $\aa$ is an indeterminate of order $A$ and $$, then
$[\aaA:]^A$.

($PE$) If $A$, $^A$, then $()$.

{\textsc{Definition} 1.1.3.} A type is an operator of order $$.

(1.1.4. {\sl Terms}) In the following, ``$a$'' means $a$ is a term
of type $$; the rest of the arity is left unspecified for simplicity.

For each type, there is a countable set of variable terms (called
``variables'').

($I$) $*ݧ$.

($⊃I$) If $a$, $x$ a variable of type $$, then $xa⊃$.

($⊃E$) If $a⊃$, $b$, then $a(b)$.

($∧I$) If $a$, $b$, then $\ang{a,b}∧$.

($∧E$) If $a∧$, then $_1a$ $_2a$.

($ÆI$) If $\aa$is an indeterminate of order $A$, $$, $A$, then
$I_{Æ\aa,}[/\aa]⊃Æ\aaA$. When clear from the context, we
shall denote this term by $I_$, or even by $I$; in particular, if
$b[/\aa]$, then $I(b)Æ\aaA$.

($ÆE$) In $a⊃$, $\aa$ an indeterminate of order $A$ which is not
free in $$ nor in the type of any free variable in $a$, then
$V\aaAa(Æ\aaA)⊃$.

($åI$) If $a$, $\aa$ an indeterminate of order $A$ which is not free
in the type of any free variable in $a$, then
$\Lambda\aaAaå\aaA$.

($åE$) If $aå\aaA\aa$, $A$, then $a\{\}[/\aa]$, where
$[/\aa]$ is $$ with $$ replacing $\aa$.



\newpage
% --------------------
% «seely-plc-trees»  (to ".seely-plc-trees")
% (s "Seely's PLC paper: trees" "seely-plc-trees")
\myslide {Seely's PLC paper: trees} {seely-plc-trees}


%:*<*\langle *
%:*>*\rangle *
%:*&*\&*

%:  ---   
%:  :
%:  
%:  ^Omega
%:  
%:  ---    ---   
%:  1:    *:1   
%:  
%:  ^1     ^*1
%:  
%:  ---    ---
%:  :    *:
%:  
%:  ^T     ^*T
%:  
%:  A:  B:  :A  :B   :A×B   :A×B   
%:  --------  ---------  ------  ------  
%:   A×B:    <,>:A×B  _1:A  _2:B  
%:  
%:   ^x       ^xI        ^xE1    ^xE2
%:  
%:   A:          :         :A  :A->
%:  ------   --------------   -----------
%:  A->:   [\aaA:]:A->     ():
%:  
%:  ^->      ^->I               ^->E
%:  
%:  :  :  a:  b:    a:∧    a:∧ 
%:  --------  ---------   ------   ------
%:    ∧:   <a,b>:∧   _1a:   _2a:
%:  
%:    ^and    ^andI       ^andE1   ^andE2
%:  
%:  :  :     a:       b:  a:⊃
%:  --------  ----------   ----------
%:    ⊃:   xa:⊃     a(b):
%:  
%:    ^imp    ^impI          ^impE
%:  
%:     :          :    :A               a:⊃          
%:  ----------  -------------------   ----------------------
%:  Æ\aaA:  I:[/\aa]⊃Æ\aaA   V\aaAa:(Æ\aaA)⊃
%:  
%:  ^sum        ^sumI                 ^sumE
%:  
%:     :              a:               :A  a:å\aaA\aa
%:  ----------  -----------------------   -----------------
%:  å\aaA:  \Lambda\aaAa:å\aaA    a\{\}:[/\aa] 
%:  
%:  ^prod       ^prodI                     ^prodE
%:  
$$\begin{array}{ccc}
  \ded{Omega}   \\ \\
  \ded{1} & \ded{*1}   \\ \\
  \ded{T} & \ded{*T}   \\ \\
  \ded{x} & \ded{xI} & \ded{xE1} \qquad \ded{xE2}   \\ \\
  \ded{->} & \ded{->I} & \ded{->E}   \\ \\
  \ded{and} & \ded{andI} & \ded{andE1} \qquad \ded{andE2}   \\ \\
  \ded{imp} & \ded{impI} & \ded{impE}   \\ \\
  \end{array}
$$

$$\begin{array}{ccccc}
  \ded{sum}  && \ded{sumI}  && \ded{sumE}   \\ \\
  \ded{prod} && \ded{prodI} && \ded{prodE}   \\ \\
  \end{array}
$$


\newpage
% --------------------
% «seely-plc-trees-dnc»  (to ".seely-plc-trees-dnc")
% (s "Seely's PLC paper: trees, in DNC" "seely-plc-trees-dnc")
\myslide {Seely's PLC paper: trees, in DNC} {seely-plc-trees-dnc}


%:  ---   
%:  :
%:  
%:  ^d.Omega
%:  
%:  ---      ---   
%:  1:      *:1   
%:  
%:  ^d.1     ^d.*1
%:  
%:  ------    -------
%:  Ï[]:    :Ï[T]
%:  
%:  ^d.T      ^d.*T
%:  
%:  A   B  a   b   a,b       a,b   
%:  -----  -----   ---       ---  
%:   A×B    a,b     a         b  
%:  
%:   ^d.x   ^d.xI   ^d.xE1    ^d.xE2
%:  
%:   A         Ï[P]      a  a|->Ï[P]
%:  ------   --------    -----------
%:  A->     a|->Ï[P]       Ï[P]
%:  
%:  ^d.->    ^d.->I         ^d.->E
%:  
%:  Ï[P]  Ï[Q]  P  Q     P&Q        P&Q 
%:  ----------  ----     ---        ---
%:    Ï[P&Q]     P&Q      P          Q
%:  
%:    ^d.and     ^d.andI  ^d.andE1   ^d.andE2
%:  
%:  Ï[P]  Ï[Q]   Q      P  P⊃Q
%:  ----------  ---     ------
%:    Ï[P⊃Q]    P⊃Q       Q
%:  
%:    ^d.imp    ^d.impI   ^d.impE
%:  
%:    Ï[P]   a,b|-Ï[P]   a|-b   a|-Ï[Q]   a,b;|-P⊃Q          
%:  -------  ----------------   --------------------
%:  Ï[b.P]    a|-P⊃(b.P)           a;|-(b.P)⊃Q
%:  
%:  ^d.sum   ^d.sumI                 ^d.sumE
%:  
%:    Ï[P]   a|-Ï[P]  a,b;P|-Q   b  b.P
%:  -------  -----------------   -------
%:  Ï[b.P]     a;P|-b.Q          b 
%:  
%:  ^d.prod     ^d.prodI           ^d.prodE
%:  
$$\begin{array}{ccc}
  \ded{d.Omega}   \\ \\
  \ded{d.1} & \ded{d.*1}   \\ \\
  \ded{d.T} & \ded{d.*T}   \\ \\
  \ded{d.x} & \ded{d.xI} & \ded{d.xE1} \qquad \ded{d.xE2}   \\ \\
  \ded{d.->} & \ded{d.->I} & \ded{d.->E}   \\ \\
  \ded{d.and} & \ded{d.andI} & \ded{d.andE1} \qquad \ded{d.andE2}   \\ \\
  \ded{d.imp} & \ded{d.impI} & \ded{d.impE}   \\ \\
  \end{array}
$$

$$\begin{array}{ccccc}
  \ded{d.sum}  && \ded{d.sumI}  && \ded{d.sumE}   \\ \\
  \ded{d.prod} && \ded{d.prodI} && \ded{d.prodE}   \\ \\
  \end{array}
$$


\newpage
% --------------------
% «local-set-theories»  (to ".local-set-theories")
% (s "Local set theories" "local-set-theories")
\myslide {Local set theories} {local-set-theories}

{\myttchars
\footnotesize
\begin{verbatim}
(T1)  |-*

(T2)  a|-a

      a|-b  b|->c
(T3)  -----------
        a|-c

      a|-b_1 ... a|-b_n
(T4)  -----------------
      a|-(b_1,...,b_n)

      a|-(b_1,...,b_n)
(T5)  -----------------
          a|-b_i

      a,b|-Ï[P]
(T6)  ---------
      a|-{b|P}

      a|-b  a|-b'
(T7)  -----------
      a|-Ï[b=b']

      a|-b  a|-{b|P}
(T8)  --------------
       a|-Ï[b{b|P}]


(L1)  P<=>Q := Ï[P]=Ï[Q]
(L2)       := *=*
(L3)    P∧Q := (Ï[P],Ï[Q])=(Ï[],Ï[])
(L4)    P⊃Q := (P∧Q)<=>P
(L5)   b.P := {b|P}={b|}
(L6)       := Ï[P].P
(L7)     P := P⊃
(L8)    P∨Q := Ï[R].(((P⊃R)∧(Q⊃R))⊃R)
(L9)   b.P := Ï[Q]. ...
\end{verbatim}
}


\newpage
% --------------------
% «local-set-theories-2»  (to ".local-set-theories-2")
% (s "Local set theories (1)" "local-set-theories-2")
\myslide {Local set theories (1)} {local-set-theories-2}


{\myttchars
\footnotesize
\begin{verbatim}
(Tautology)     P|-P
(Unity)         |-*'=*
(Equality)      b'=b''|-c[b:=b']=c[b:=b'']
(Products)      |-<b,c>=b
                |-'<b,c>=c
                |-<(b,c),'(b,c)>=(b,c)
(Comprehension) |-b{b|P}<=>P


                  P|-R
(Thinning)        ------
                  P,Q|-R

                  a;P|-Q   a;P,Q|-R
(Cut)             -----------------
                       a;P|-R

                    a,b;P|-Q   a|-b'
(Subst)           --------------------
                  a;P[b:=b']|-Q[b:=b']

                  a,b;P|-b{b|Q}<=>b{b|R}
(Extensionality)  ------------------------
                    a;P|-{b|Q}<=>{b|R}

                  P,Q|-R   P,R|-Q
(Equivalence)     ---------------
                     P|-Q<=>R
\end{verbatim}
}



\newpage
% --------------------
% «notes-seelyhyp»  (to ".notes-seelyhyp")
% (s "Notes on SeelyHyp" "notes-seelyhyp")
\myslide {Notes on reading SeelyHyp} {notes-seelyhyp}


  %*
% (eedn4a-bounded)
% (find-ragshyppage (+ -504 513))
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")

\def\eqdef{\overset{\text{def}}{=}}

SeelyHyp, \S4:

(5') (i) For $t: X \to Y$, $\phi$ over $X$, we define

$Æ_t \phi \eqdef \xi (t\xi = y ∧ \phi(\xi))$,

$å_t \phi \eqdef \xi (t\xi = y ⊃ \phi(\xi))$,

%:               tx=y∧\cc(x)
%:               -----------(∧E)
%:                  [\cc(x)]       tx=y∧\cc(x)
%:                  :::::::P       -----------(∧E)
%:                  \phi(x)          tx=y
%:                  ---------------------(∧I)
%:                           tx=y∧\phi(x)
%:                           ---------------------(I)
%:  \xi(t\xi=y∧\cc(\xi))    \xi(t\xi=y∧\phi(\xi))
%:  ---------------------------------------------(E)
%:                   \xi(t\xi=y∧\phi(\xi))
%:
%:                   ^xii
%:
$$\ded{xii}$$


\bsk

For $f: A \to B$, define:

$Æ_f \ssst{a}{P(a)} \quad \eqdef \quad \ssst{b}{a.(f(a)=b \;\&\; P(a))}$

$å_f \ssst{a}{P(a)} \quad \eqdef \quad \ssst{b}{a.(f(a)=b \;⊃\; P(a))}$


%:               		 [f(a)=b∧P(a)]^1      
%:                               ---------------(∧E)
%:           [f(a)=b∧P(a)]^1	     P(a)         
%:           ---------------(∧E)     ::::         
%:                  f(a)=b           Q(a)         
%:                  ---------------------(∧I)
%:                  un         f(a)=b∧Q(a)
%:                           ---------------(I)
%:  a.(f(a)=b∧P(a))         a.(f(a)=b∧Q(a))
%:  ---------------------------------------------(E)
%:                   a.(f(a)=b∧Q(a))
%:
%:                   ^xiii
%:
$$\ded{xiii}$$


\newpage
% --------------------
% «luo»  (to ".luo")
% (s "Luo's ECC" "luo")
\myslide {Luo's ECC} {luo}

\def\Type{\mathit{Type}}
\def\Prop{\mathit{Prop}}

% (fooi "\Type_j" "_j")

%:  
%:  ---------------(Ax)                     -------(Ax)
%:  |-\Prop:\Type_0                         |-:_0
%:  
%:  ^luo-Ax                                 ^luo-Ax-dnc
%:  
%:     \GG|-A:\Type_j			      a|-B:_j					
%:  ----------------------(C)		    -----------(C)			
%:  \GG,xA|-\Prop:\Type_0		    a,b|-:_0
%:  					    							
%:  ^luo-C				    ^luo-C-dnc						
%:  					    							
%:    \GG|-\Prop:\Type_0		      a|-:_0				
%:  ------------------------(T)		    ---------------------(T)				
%:  \GG|-\Type_j:\Type_{j+1}		    \GG|-_j:_{j+1}				
%:  					    							
%:  ^luo-T				    ^luo-T-dnc
%:  					    							
%:  \GG,xA,\GG'|-\Prop:\Type_0		    a,b,c|-:_0				
%:  ---------------------------(var)	    ------------(var)			
%:       \GG,xA,\GG'|-xA		      a,b,c|-b				
%:  					    							
%:       ^luo-var			      ^luo-var-dnc					
%:  					    							
%:  \GG,xA|-P:\Prop			    a,b|-Ï[P]:					
%:  -----------------(å1)		    -------------(å1)				
%:  \GG|-åxA.P:\Prop			    a|-Ï[b.P]:					
%:  					    							
%:  ^luo-prod1				    ^luo-prod1-dnc
%:  					    							
%:  \GG|-A:\Type_j  \GG,xA|-B:\Type_j	    a|-B:_j  a,b|-C:_j			
%:  ----------------------------------(å2)  ----------------------(å2)		
%:       \GG|-åxA.B:\Type_j		         a|-åbB.C:_j				
%:                                                                                          
%:       ^luo-prod2			         ^luo-prod2-dnc					
%:                                                                                          
%:  \GG,xA|-M:B			    a,b|-c:C					
%:  ------------------()		    ------------------()				
%:  \GG|-xA.M:åxA.B			    a|-b.c:åbB.C					
%:                                                                                          
%:  ^luo-lambda				    ^luo-lambda-dnc
%:  					    							
%:  \GG|-M:åxA.B  \GG|-N:A		    a|-(b|->c)  a|-b				
%:  -----------------------(app)	    -----------------------(app)			
%:     \GG|-MN:[N/x]B			       a|-c					
%:  					    							
%:     ^luo-app				       ^luo-app-dnc
%:  					    							
%:  \GG|-A:\Type_j  \GG,xA|-B:\Type_j	    a|-B:_j  a,b|-C:_j			
%:  ----------------------------------(Æ)   --------------------(Æ)		
%:     \GG|-ÆxA.B:\Type_j		       a|-ÆbB.C:_j				
%:  					    							
%:     ^luo-sum                                ^luo-sum-dnc
%:
%:  \GG|-M:A  \GG|-N:[M/x]B  \GG,x:A|-B:\Type_j
%:  -------------------------------------------(pair)
%:    \GG|-\mathbf{pair}_{ÆxA.B}(M,N):ÆxA.B
%:
%:    ^luo-pair
%:
%:  \GG|-M:ÆxA.B                            a|-(b,c):ÆbB.C           
%:  -------------(1)                        -------------(1)         
%:  \GG|-_1(M):A                            a|-b:B            
%:                                                                      
%:  ^luo-pi1                                 ^luo-pi1-dnc
%:                                                                      
%:       \GG|-M:ÆxA.B                       a|-(b,c):ÆbB.C           
%:  -----------------------(2)              ---------------(2)
%:  \GG|-_2(M):[_1(M)/x]B                  a|-c:C    
%:
%:  ^luo-pi2                                 ^luo-pi2-dnc
%:
%:  \GG|-M:A   \GG|-A':\Type_j
%:  --------------------------(A{\preceq}A')
%:     \GG|-M:A'
%:
%:     ^luo-preceq
%:
$$\ded{luo-Ax}$$
$$\ded{luo-C}$$
$$\ded{luo-T}$$
$$\ded{luo-var}$$
$$\ded{luo-prod1}$$
$$\ded{luo-prod2}$$
$$\ded{luo-lambda}$$
$$\ded{luo-app}$$
$$\ded{luo-sum}$$
$$\ded{luo-pair}$$
$$\ded{luo-pi1}$$
$$\ded{luo-pi2}$$
$$\ded{luo-preceq}$$

\newpage

$$\ded{luo-Ax-dnc}$$
$$\ded{luo-C-dnc}$$
$$\ded{luo-T-dnc}$$
$$\ded{luo-var-dnc}$$
$$\ded{luo-prod1-dnc}$$
$$\ded{luo-prod2-dnc}$$
$$\ded{luo-lambda-dnc}$$
$$\ded{luo-app-dnc}$$
$$\ded{luo-sum-dnc}$$
% $$\ded{luo-pair-dnc}$$
$$\ded{luo-pi1-dnc}$$
$$\ded{luo-pi2-dnc}$$
% $$\ded{luo-preceq-dnc}$$





%*

\end{document}

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