|
Warning: this is an htmlized version!
The original is here, 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}:åX¨P.Q:\DD''
%:
%: ^pav-IProd
%:
%:
%: Ðp:P:\DD' Ðr:åX¨P.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}}:ÆX¨P.Q:\DD'
%:
%: ^pav-ISum
%:
%: [X:P:\DD']
%: ===============
%: [ÐY:Q(X):\DD'']
%: ==========================
%: Ðr:ÆX¨P.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}:åb¨B.C:Þ''
%:
%: ^pav-IProd-abc
%:
%: b':B:Þ' f:åb¨B.C(b):Þ''
%: -------------------------¯EåÞ'Þ''
%: fb:C[b:=b']:Þ''
%:
%: ^pav-EProd-abc
%:
%: [b:B:Þ']
%: ========
%: b':B:Þ' C:Þ' c:C(b'):Þ''
%: ------------------------------¯IÆÞ'Þ''
%: \ang{b',c}:Æb¨B.C:Þ'
%:
%: ^pav-ISum-abc
%:
%: [b:B:Þ']
%: ===============
%: [Ðc:C(b):Þ'']
%: ==========================
%: Ðp:Æb¨B.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:
%: ý_{xÝA}\phi(x)|-ý_{xÝA}\phi(x) Î_{xÝA}\phi(x)|-Î_{xÝA}\phi(x)
%: ------------------------------(2.4) ------------------------------(2.4')
%: ý_{xÝA}\phi(x)|-_x\phi(x) \phi(x)|-_xÎ_{xÝA}\phi(x)
%: -------------------------------------------------------------(1.2)
%: ý_{xÝA}\phi(x)|-_xÎ_{xÝA}\phi(x)
%: --------------------------------(1.4)
%: ý_{xÝA}\phi(x)|-Î_{xÝA}\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 $Æ\aaÝA·$
and $å\aaÝA·ÝØ$.
($×I$) If $ÝA$, $ ÝB$, then $\ang{, }ÝA×B$.
($×E$) If $ÝA×B$, then $_1ÝA$, $_2ÝB$.
($PI$) If $\aa$ is an indeterminate of order $A$ and $ÝØ$, then
$[\aaÝA:]ÝØ^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 $ðxÝ·aÝ⊃ $.
($⊃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]⊃Æ\aaÝA·$. When clear from the context, we
shall denote this term by $I_ $, or even by $I$; in particular, if
$bÝ[ /\aa]$, then $I(b)ÝÆ\aaÝA·$.
($Æ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\aaÝA·aÝ(Æ\aaÝA·)⊃$.
($åI$) If $aÝ$, $\aa$ an indeterminate of order $A$ which is not free
in the type of any free variable in $a$, then
$\Lambda\aaÝA·aÝå\aaÝA·$.
($åE$) If $aÝå\aaÝA·\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->Ø:Þ [\aaÝA:]:A->Ø ( ):Ø
%:
%: ^-> ^->I ^->E
%:
%: :Ø :Ø a: b: a:∧ a:∧
%: -------- --------- ------ ------
%: ∧ :Ø <a,b>:∧ _1a: _2a:
%:
%: ^and ^andI ^andE1 ^andE2
%:
%: :Ø :Ø a: b: a:⊃
%: -------- ---------- ----------
%: ⊃ :Ø ðxÝ·a:⊃ a(b):
%:
%: ^imp ^impI ^impE
%:
%: :Ø :Ø :A a:⊃
%: ---------- ------------------- ----------------------
%: Æ\aaÝA·:Ø I:[ /\aa]⊃Æ\aaÝA· ¦V\aaÝA·a:(Æ\aaÝA·)⊃
%:
%: ^sum ^sumI ^sumE
%:
%: :Ø a: :A a:å\aaÝA·\aa
%: ---------- ----------------------- -----------------
%: å\aaÝA·:Ø \Lambda\aaÝA·a:å\aaÝA· 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,x¨A|-\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,x¨A,\GG'|-\Prop:\Type_0 a,b,c|-Ø:Þ_0
%: ---------------------------(var) ------------(var)
%: \GG,x¨A,\GG'|-x¨A a,b,c|-b
%:
%: ^luo-var ^luo-var-dnc
%:
%: \GG,x¨A|-P:\Prop a,b|-Ï[P]:Ø
%: -----------------(å1) -------------(å1)
%: \GG|-åx¨A.P:\Prop a|-Ï[ýb.P]:Ø
%:
%: ^luo-prod1 ^luo-prod1-dnc
%:
%: \GG|-A:\Type_j \GG,x¨A|-B:\Type_j a|-B:Þ_j a,b|-C:Þ_j
%: ----------------------------------(å2) ----------------------(å2)
%: \GG|-åx¨A.B:\Type_j a|-åb¨B.C:Þ_j
%:
%: ^luo-prod2 ^luo-prod2-dnc
%:
%: \GG,x¨A|-M:B a,b|-c:C
%: ------------------(ð) ------------------(ð)
%: \GG|-ðx¨A.M:åx¨A.B a|-ðb.c:åb¨B.C
%:
%: ^luo-lambda ^luo-lambda-dnc
%:
%: \GG|-M:åx¨A.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,x¨A|-B:\Type_j a|-B:Þ_j a,b|-C:Þ_j
%: ----------------------------------(Æ) --------------------(Æ)
%: \GG|-Æx¨A.B:\Type_j a|-Æb¨B.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}_{Æx¨A.B}(M,N):Æx¨A.B
%:
%: ^luo-pair
%:
%: \GG|-M:Æx¨A.B a|-(b,c):Æb¨B.C
%: -------------(1) -------------(1)
%: \GG|-_1(M):A a|-b:B
%:
%: ^luo-pi1 ^luo-pi1-dnc
%:
%: \GG|-M:Æx¨A.B a|-(b,c):Æb¨B.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: