|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-LATEX "2020bell-lst.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2020bell-lst.tex" :end))
% (defun D () (interactive) (find-pdf-page "~/LATEX/2020bell-lst.pdf"))
% (defun d () (interactive) (find-pdftools-page "~/LATEX/2020bell-lst.pdf"))
% (defun e () (interactive) (find-LATEX "2020bell-lst.tex"))
% (defun u () (interactive) (find-latex-upload-links "2020bell-lst"))
% (defun v () (interactive) (find-2a '(e) '(d)) (g))
% (find-pdf-page "~/LATEX/2020bell-lst.pdf")
% (find-sh0 "cp -v ~/LATEX/2020bell-lst.pdf /tmp/")
% (find-sh0 "cp -v ~/LATEX/2020bell-lst.pdf /tmp/pen/")
% file:///home/edrx/LATEX/2020bell-lst.pdf
% file:///tmp/2020bell-lst.pdf
% file:///tmp/pen/2020bell-lst.pdf
% http://angg.twu.net/LATEX/2020bell-lst.pdf
% (find-LATEX "2019.mk")
% «.3._local_set_theory» (to "3._local_set_theory")
% «.3.8._elim-ex-unique» (to "3.8._elim-ex-unique")
% «.5._from_logic_to_sheaves» (to "5._from_logic_to_sheaves")
% «.5.1.» (to "5.1.")
% «.5.1.(1)_my_proof» (to "5.1.(1)_my_proof")
\documentclass[oneside,12pt]{article}
\usepackage[colorlinks,citecolor=DarkRed,urlcolor=DarkRed]{hyperref} % (find-es "tex" "hyperref")
\usepackage{indentfirst}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage[x11names,svgnames]{xcolor} % (find-es "tex" "xcolor")
%\usepackage{colorweb} % (find-es "tex" "colorweb")
%\usepackage{tikz}
%
% (find-dn6 "preamble6.lua" "preamble0")
\usepackage{proof} % For derivation trees ("%:" lines)
\input diagxy % For 2D diagrams ("%D" lines)
\xyoption{curve} % For the ".curve=" feature in 2D diagrams
%
\usepackage{edrx15} % (find-LATEX "edrx15.sty")
\input edrxaccents.tex % (find-LATEX "edrxaccents.tex")
\input edrxchars.tex % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex % (find-LATEX "edrxheadfoot.tex")
\input edrxgac2.tex % (find-LATEX "edrxgac2.tex")
%
%\usepackage[backend=biber,
% style=alphabetic]{biblatex} % (find-es "tex" "biber")
%\addbibresource{catsem-slides.bib} % (find-LATEX "catsem-slides.bib")
%
% (find-es "tex" "geometry")
\begin{document}
\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"} % (find-LATEX "dednat6load.lua")
\def\True {\textit{true}}
\def\False{\textit{false}}
% (find-belltpage (+ 14 70) "Logic operations, axioms and inference rules")
\def\L{\text{L}}
% (find-belltpage (+ 14 71) "basic axioms")
\def\Taut{\text{Taut}}
\def\Unit{\text{Unit}}
\def\Equa{\text{Equa}}
\def\Produ{\text{Produ}}
\def\Compr{\text{Compr}}
% (find-belltpage (+ 14 71) "rules of inference")
\def\Thin {\text{Thin}}
\def\Cut {\text{Cut}}
\def\Subst{\text{Subst}}
\def\Ext {\text{Ext}}
\def\Equiv{\text{Equiv}}
% (find-belltpage (+ 14 69) "(T6)")
% \setofsc is like \setofst but uses a colon instead of a "such that" bar
\def\setofc#1#2{\{\,#1\;:\;#2\,\}}
\def\setofc#1#2{\{\,#1\,:\,#2\,\}}
\def\setofc#1#2{\{\,#1 : #2\,\}}
{\setlength{\parindent}{0em}
\footnotesize
Notes on Bell's ``Toposes and Local Set Theories'' (Oxford, 1988).
\ssk
These notes are at:
\url{http://angg.twu.net/LATEX/2020bell-lst.pdf}
\ssk
See:
\url{http://angg.twu.net/LATEX/2020favorite-conventions.pdf}
\url{http://angg.twu.net/math-b.html\#favorite-conventions}
I wrote these notes mostly to test if the conventions above
are good enough.
}
% «3._local_set_theory» (to ".3._local_set_theory")
\section*{3. Local Set Theories}
(Page 70):
$$\begin{tabular}{llll}
(L1) & $α⇔β$ & for & $α=β$ \\
(L2) & $\True$ & for & $*=*$ \\
(L3) & $α∧β$ & for & $〈α,β〉 = 〈\True,\True〉$ \\
(L4) & $α⇒β$ & for & $(α∧β)⇔α$ \\
(L5) & $∀xα$ & for & $\setofc{x}{α} = \setofc{x}{\True}$ \\
(L6) & $\False$ & for & $∀ω.ω$ \\
(L7) & $¬α$ & for & $α⇒\False$ \\
(L8) & $α∨β$ & for & $∀ω[(α⇒ω∧β⇒ω)⇒ω]$ \\
(L9) & $∃xα$ & for & $∀ω[∀x(α⇒ω)⇒ω]$ \\
\end{tabular}
$$
(Page 71):
% (find-belltpage (+ 14 71) "basic axioms")
% (find-belltpage (+ 14 71) "rules of inference")
Basic axioms (left) and rules of inference (right):
%
%:
%: ---\Taut
%: α:α
%:
%: ^Taut
%:
%: ----\Unit
%: :x_1=*
%:
%: ^Unit
%:
%: -----------------\Equa
%: x=y,α(z/x):α(z/y)
%:
%: ^Equa
%:
%: -----------------\Produ
%: :(〈x_1,\ldots,x_n〉)_i=x_i
%:
%: ^Produ1
%:
%: -----------------\Produ
%: :x=〈(x)_1,\ldots,(x)_n)〉
%:
%: ^Produ2
%:
%: -----------------\Compr
%: :x∈\setofc{x}{α}⇔α
%:
%: ^Compr
%:
%:
%: Γ:α
%: -----\Thin
%: β,Γ:α
%:
%: ^Thin
%:
%: Γ:α α,Γ:β
%: -----------\Cut
%: Γ:β
%:
%: ^Cut
%:
%: Γ:α
%: ------------\Subst
%: Γ(x/τ):α(x/τ)
%:
%: ^Subst
%:
%: Γ:x∈σ⇔x∈τ
%: ---------\Ext
%: Γ:σ=τ
%:
%: ^Ext
%:
%: α,Γ:β β,Γ:α
%: ---------\Equiv
%: Γ:α⇔β
%:
%: ^Equiv
%:
$$\pu
\begin{array}{c}
\ded{Taut} \\ \\
\ded{Unit} \\ \\
\ded{Equa} \\ \\
\ded{Produ1} \\ \\
\ded{Produ2} \\ \\
\ded{Compr} \\
\end{array}
\qquad
\begin{array}{c}
\ded{Thin} \\ \\
\ded{Cut} \\ \\
\ded{Subst} \\ \\
\ded{Ext} \\ \\
\ded{Equiv} \\ \\
\end{array}
$$
(Page 71):
(3.1.5) (i) and (ii):
%
%:
%: ----\Unit
%: :*=*
%: ------(\L2)
%: :\True
%: ---\Taut -------\Thin
%: α:α α:\True
%: ---------\Thin ---------\Thin
%: \True,α:α α,α:\True
%: --------- -------------------------\Equiv
%: \True,α:α α,α:\True α:α⇔\True
%: --------------------- ---------(\L1)
%: α:α=\True α:α=\True
%:
%: ^p73.1 ^p73.1-my
%:
%:
%:
%:
%:
%:
%:
%:
%:
%:
%:
%:
%:
%:
%:
%:
$$\pu
\ded{p73.1}
\quad \squigto \quad
% \qquad
\ded{p73.1-my}
$$
%:
%:
%: ω=ω',ω':ω
%: --------------- ------
%: α=\True,\True:α :\True
%: ------------------------
%: α=\True:α
%:
%: ^p73.2
%:
%: ---------\Equa
%: ω=ω',ω':ω
%: ---------------\Subst
%: α=\True,\True:α
%: ====== ---------------
%: :\True \True,α=\True:α
%: --------------------------\Cut
%: α=\True:α
%:
%: ^p73.2-my
%:
%:
$$\pu
\ded{p73.2}
\quad \squigto \quad
% \qquad
\ded{p73.2-my}
$$
% (find-belltpage (+ 14 68) "3. Local Set Theories")
% (find-belltpage (+ 14 73) "3.1 Conjunction")
\newpage
% _____ _ _ _____ _
% | ____| (_)_ __ ___ | ____|_ _| |
% | _| | | | '_ ` _ \ | _| \ \/ / |
% | |___| | | | | | | | | |___ > <|_|
% |_____|_|_|_| |_| |_| |_____/_/\_(_)
%
% «3.8._elim-ex-unique» (to ".3.8._elim-ex-unique")
% (lstp 3 "3.8._elim-ex-unique")
% (lst "3.8._elim-ex-unique")
% (find-books "__cats/__cats.el" "bell-lst")
% (find-belltpage (+ 14 81) "Our final task in this section")
%
% (find-books "__cats/__cats.el" "taylor")
% (find-taylorpfmpage (+ 14 61) "8. (...) proof-box rules for Ex!")
%
% (find-books "__logic/__logic.el" "mendelson")
\subsection*{3.8 Eliminability of descriptions}
(Page 81):
Our final task in this section is to show that local set theories
satisfy {\sl eliminability of descriptions for formulae} and {\sl for
terms of power type}. To explain this, define the {\sl unique
existential quantifier} $∃!$ by writing
%
$$∃!xα \quad \text{for} \quad ∃x(α∧∀y(α(x/y)⇒x=y)),$$
%
where $y$ is different from $x$ and not free in $α$. Then, if $α(x)$
is any formula and $x$ is any variable either of type $Ω$ or of power
type, we will exhibit a term $τ$ of the same type as $x$, for which we
have
%
$$∃!xα⊢α(x/τ)$$
%
$τ$ is thus an explicit term satisfying the description: `the unique
$x$ such that $α$'.
\msk
{\bf 3.8. Proposition} (Eliminability of descriptions for formulae)
%
$$∃!ωα ⊢ α(ω/α(ω/\True))$$
% ____ _
% / ___|| |__ ___ __ ___ _____ ___
% \___ \| '_ \ / _ \/ _` \ \ / / _ \/ __|
% ___) | | | | __/ (_| |\ V / __/\__ \
% |____/|_| |_|\___|\__,_| \_/ \___||___/
%
\newpage
% «5._from_logic_to_sheaves» (to ".5._from_logic_to_sheaves")
% (lstp 3 "5._from_logic_to_sheaves")
% (lst "5._from_logic_to_sheaves")
% (find-books "__cats/__cats.el" "bell-lst")
% (find-belltpage (+ 14 162) "5. From Logic to Sheaves")
% (find-belltpage (+ 14 162) "truth-set")
\section*{5. From Logic to Sheaves}
(Page 162):
{\bf Truth-sets, modalities, and universal closure operations}
(...)
More generally, an $S$-set $T$ such that $⊢T⊆Ω$ is called a {\sl
truth-set} in $S$ if it satisfies the same conditions, viz.:
\msk
$\begin{array}{rl}
(tr_0) & ⊢T⊆Ω \\
(tr_1) & ⊢\True∈T \\
(tr_2) & α⊢β \quad \text{implies} \quad α∈T⊢β∈T \\
(tr_3) & (α∈T)∈T⊢α∈T \\
\end{array}
$
Let's write $α^*$ for $α∈T$. We can rewrite the above as:
$\begin{array}{rl}
(tr_1) & ⊢\True^* \\
(tr_2) & α⊢β \quad \text{implies} \quad α^*⊢β^* \\
(tr_3) & α^{**}⊢α^* \\
\end{array}
$
\msk
% ____ _
% | ___| / |
% |___ \ | |
% ___) || |
% |____(_)_|
%
% «5.1.» (to ".5.1.")
% (lstp 3 "5.1.")
% (lst "5.1.")
% (find-belltpage (+ 14 162) "5.1. Proposition")
{\bf 5.1. Proposition.} Let $T$ be a truth-set in $S$. Then:
$\begin{array}{rl}
(i) & α∈T,β∈T ⊢ α∧β∈T, \\
(ii) & α∈T, α⇒β∈T ⊢ β∈T, \\
(iii) & α⇒β ⊢ α∈T⇒β∈T \\
\end{array}
$
i.e.,
$\begin{array}{rl}
(i) & α^*,β^*⊢(α∧β)^* \\
(ii) & α^*, (α⇒β)^* ⊢ β^* \\
(iii) & α⇒β ⊢ α^*⇒β^* \\
\end{array}
$
\msk
Proof. (i) Let us write $α^*$ for $α∈T$. Then from $α⊢β=α∧β$ we deduce
$α⊢β^*=(α∧β)^*$, whence $α⊢β^*⇒(α∧β)^*$, so that
%
$$α,β^*⊢(α∧β)^*. \qquad (1)$$
%
Replacing $α$ by $α^*$ gives
%
$$α^*,β^*⊢(α^*∧β)^*, \qquad (2)$$
%
and interchanging $α$ and $β$ in (1) yields
%
$$α^*,β^*⊢(α^*∧β)^*, \qquad (3)$$
%
% (find-belltpage (+ 14 162) "5.1. Proposition")
(3) gives $...$, so by (tr2) $...$, whence $...$ by (tr3). This,
together with (2), gives $...$.
\newpage
% ____ _ _____
% | ___| / | / (_) \ _ __ ___ _ _
% |___ \ | | | || || | | '_ ` _ \| | | |
% ___) || |_ | || || | | | | | | | |_| |
% |____(_)_(_) | ||_|| | |_| |_| |_|\__, |
% \_\ /_/ |___/
%
% «5.1.(1)_my_proof» (to ".5.1.(1)_my_proof")
% (lstp 4 "5.1.(1)_my_proof")
% (lst "5.1.(1)_my_proof")
{\bf My proof of 5.1.(1).}
%:
%: ----- -----
%: α∧β⊢β \a∧β⊢β
%: ------- ------ ----------- --------
%: α∧β⊢α∧β ⊢α∧β⇒β \a∧β⊢\a∧β ⊢\a∧β⇒β
%: ------- ------- ----------- -----------
%: α⊢β⇒α∧β α⊢α∧β⇒β \a⊢β⇒\a∧β \a⊢\a∧β⇒β
%: ------------------ --------------------------
%: α⊢β=α∧β \a⊢β=\a∧β
%: ------------- ---------------
%: α⊢β^*=(α∧β)^* \a⊢β^*=(\a∧β)^*
%: ------------- ================= ---------------
%: α∧β^*⊢(α∧β)^* α^*∧β^*⊢(α^*∧β)^* \a∧β^*⊢(\a∧β)^*
%:
%: ^5.1.(i)_a ^5.1.(i)_b 5.1.(i)_awithdef
%:
$$\pu
\begin{array}{c}
\ded{5.1.(i)_a} \qquad \ded{5.1.(i)_b} \\
\end{array}
$$
{\bf Old stuff:}
%:
%:
%: α⊢β=α{∧}β α^*⊢β=α^*{∧}β
%: --------------- ---------------
%: α⊢β^*=(α{∧}β)^* α^*⊢β^*=(α^*{∧}β)^*
%: ----------------- -----------------
%: α⊢β^*{⇒}(α{∧}β)^* α^*⊢β^*{⇒}(α^*{∧}β)^*
%: ----------------- -----------------
%: α,β^*⊢(α{∧}β)^* α^*,β^*⊢(α^*{∧}β)^*
%:
%: ^f1 ^f2
%:
$$\pu
\begin{array}{c}
\ded{f1} \qquad \ded{f2} \\
\end{array}
$$
%:
%: ----------- -----------
%: α⊢β=α{∧}β α^*⊢β=α^*{∧}β β⊢α=α{∧}β
%: --------------- ----------------- -----------------
%: α⊢β^*=(α{∧}β)^* α^*⊢β^*=(α^*{∧}β)^* β⊢α^*=(α{∧}β)^*
%: ----------------- --------------------- -----------------
%: α⊢β^*{⇒}(α{∧}β)^* α^*⊢β^*{→}(α^*{∧}β)^* β⊢α^*{→}(α{∧}β)^*
%: ----------------- --------------------- -----------------
%: α,β^*⊢(α{∧}β)^* α^*,β^*⊢(α^*{∧}β)^* α^*,β⊢(α{∧}β)^*
%: ----------------- -------------------- -----------------
%: α{∧}β^*⊢(α{∧}β)^* α^*{∧}β^*⊢(α^*{∧}β)^* α^*{∧}β⊢(α{∧}β)^*
%: ----------------- --------------------- -----------------
%: (α{∧}β^*)^*⊢(α{∧}β)^{**} (α^*{∧}β^*)^*⊢(α^*{∧}β)^{**} (α^*{∧}β)^*⊢(α{∧}β)^{**}
%: ----------------- ----------------- -----------------
%: (α{∧}β^*)^*⊢(α{∧}β)^* (α^*{∧}β^*)^*⊢(α^*{∧}β)^* (α^*{∧}β)^*⊢(α{∧}β)^*
%:
%: ^foo1 ^foo2 ^foo3
%:
$$\pu
\begin{array}{c}
\ded{foo1} \qquad \ded{foo2} \qquad \ded{foo3} \\
\end{array}
$$
(What are these?)
$(tr'_1) \qquad ⊢⊤^*$
$(tr'_2) \qquad α⊢β \qquad α^*⊢β^*$
$(tr'_3) \qquad α^{**}⊢α^*$
$(tr'_4) \qquad α⊢α^*$
\msk
% (find-belltpage (+ 14 163) "modality")
% (find-belltpage (+ 14 164) "universal closure operation")
%:
%: --------- ---------
%: α{∧}β⊢α α{∧}β⊢β
%: ======================== ======================== --------------- ----------
%: α^*{∧}β^*⊢(α^*{∧}β)^* (α^*{∧}β)^*⊢(α{∧}β)^* (α{∧}β)^*⊢α^* (α{∧}β)^*⊢β^*
%: ---------------------------------------------------- --------------------------------
%: α^*{∧}β^*⊢(α{∧}β)^* (α{∧}β)^*⊢α^*{∧}β^*
%: ------------------------------------------------------------------------------------
%: ⊢α^*{∧}β^*=(α{∧}β)^*
%:
%: ^foo4
%:
%: =======================
%: ⊢α^*{∧}β^*=(α{∧}β)^*
%: -----------------------------
%: ⊢(α^*{∧}β^*)^*=(α{∧}β)^{**}
%: -----------------------------
%: ⊢(α^*{∧}β^*)^*=(α{∧}β)^*
%: ======================= -----------------------------
%: ⊢α^*{∧}β^*=(α{∧}β)^* ⊢(α{∧}β)^*=(α^*{∧}β^*)^*
%: -------------------------------------------------------
%: ⊢α^*{∧}β^*=(α{∧}β)^*=(α^*{∧}β^*)^*
%:
%: ^foo5
%:
$$\pu
\begin{array}{c}
\ded{foo4} \\ \\
(i'): \quad \ded{foo5} \\
\end{array}
$$
%:
%: ------------
%: α,α{→}β⊢β
%: ------------
%: α∧(α{→}β)⊢β
%: --------------------
%: (α∧(α{→}β))^*⊢β^*
%: --------------------
%: α^*∧(α{→}β)^*⊢β^*
%: --------------------
%: α^*,(α{→}β)^*⊢β^*
%: ------------------ --------------------
%: α{→}β⊢(α{→}β)^* (α{→}β)^*⊢α^*{→}β^*
%: ----------------------------------------------
%: α{→}β⊢(α{→}β)^*⊢α^*{→}β^*
%:
%: ^bar1
%:
%:
%: ------------------- ----
%: α{→}β⊢(α{→}β)=⊤ ⊤∈T
%: --------------------------
%: α{→}β⊢(α{→}β)∈T α{→}β⊢(α{→}β)^*
%:
%:
%: ------- ----
%: α⊢α=⊤ ⊤∈T
%: -------------
%: α⊢α∈T
%: -------
%: α⊢α^*
%:
%: ^tr4
%:
$$\pu
\begin{array}{c}
(0'): \quad \ded{tr4} \qquad
(ii',iii'): \quad \ded{bar1} \\ \\
\end{array}
$$
\newpage
Notes from 2017...
\msk
\def\dt#1#2{\sm{#1\\#2}}
\def\DT#1#2{\mat{#1\\↓\\#2}}
\def\PDT#1#2{\pmat{#1\\↓\\#2}}
\def\mt#1#2#3#4{\dt#1#2{↦}\dt#3#4}
$Ω=\PDT{\{\dt00,\dt01,\dt11\}}{\{\dt·0,\dt·1\}}$
$\{⊤\}=\PDT{\{\dt11\}}{\{\dt·1\}}$
\msk
$012$:
\quad
$μ=\PDT{\cmat{\mt0011,\, \mt0111,\, \mt1111}}{\cmat{\mt·0·1,\, \mt·1·1}}$
\quad
$T=Ω=\PDT{\{\dt00,\dt01,\dt11\}}{\{\dt·0,\dt·1\}}$
\msk
$0|12$:
\quad
$μ=\PDT{\cmat{\mt0000,\, \mt0111,\, \mt1111}}{\cmat{\mt·0·0,\, \mt·1·1}}$
\quad
$T=\PDT{\{\dt01,\dt11\}}{\{\dt·1\}}$
\msk
$01|2$:
\quad
$μ=\PDT{\cmat{\mt0001,\, \mt0101,\, \mt1111}}{\cmat{\mt·0·1,\, \mt·1·1}}$
\quad
$T=\PDT{\{\dt11\}}{\{\dt·0,\dt·1\}}$
\msk
$0|1|2$:
\quad
$μ=\PDT{\cmat{\mt0000,\, \mt0101,\, \mt1111}}{\cmat{\mt·0·0,\, \mt·1·1}}$
\quad
$T=\{⊤\}=\PDT{\{\dt11\}}{\{\dt·1\}}$
% (find-angg "LATEX/2017bell.tex")
% Gente, posso fazer uma pergunta sobre Local Set Theories? Se voces nao
% souberem eu pergunto no Zulip Chat, mas prefiro perguntar aqui
% primeiro...
%
% Na pagina 71 o Bell define "sequents" e 5 regras de inferencia
% basicas, e a partir dai' ele mostra um monte de arvores de deducao
% nesse sistema dele, e vai definindo um monte de regras derivadas...
%
% Em algum lugar bem mais adiante - num capitulo que eu entendo mal -
% ele define a Local Set Theory associada a um topos dado qualquer, e
% acho que so' a partir dai' esses sequentes vao passar a ter uma
% semantica clara.
%
% Digamos que a gente esta' num topos E que a gente escolheu, e que a
% gente escolheu valores para P e Q - P e Q sao valores de verdade.
%
% (Eu tenho tentado montar sempre exemplos concretos... por exemplo, na
% pagina 12 daqui - http://angg.twu.net/LATEX/2017planar-has-1.pdf - tem
% umas contas com desenhos em que eu fixo uma algebra de Heyting,
% escolho valores pra P e Q nessa HA - P := 10 e Q := 01 - e ai' calculo
% o valor de uma expressao grande envolvendo P e Q...)
%
% Entao, digamos que a gente escolheu o topos E e valores de verdade P e
% Q.
%
% A semantica para o sequente P:Q vai dizer que o "valor" de P:Q e' um
% valor de verdade "classico", i.e., ou "verdadeiro" ou "falso"? Ou vai
% dizer que o valor de P:Q vai ser um valor de verdade do topos, podendo
% ser algum valor intermediario entre "falso" e "verdadeiro"?
%
% Obs: talvez eu devesse ter usado "|-_{S}" ao inves de ":" em alguns
% lugares...
%
% Obs 2: o Bell prova um "soundness theorem" nas paginas 97 ate' 103,
% que nao sei se responde a minha pergunta - ainda nao entendi qual e' a
% semantica de cada sequente P:Q e de cada arvore de derivacao...
%
% José Alvim
% puts, eu não sei não. Vou ter que pensar
%
% Eduardo Ochs
% Tou achando que as duas semanticas funcionam, mas a em que o valor de
% verdade de cada sequente e' so' ou verdadeiro ou falso e' mais
% parecida com a que o Bell usa...
%\printbibliography
\end{document}
% __ __ _
% | \/ | __ _| | _____
% | |\/| |/ _` | |/ / _ \
% | | | | (_| | < __/
% |_| |_|\__,_|_|\_\___|
%
% <make>
* (eepitch-shell)
* (eepitch-kill)
* (eepitch-shell)
# (find-LATEXfile "2019planar-has-1.mk")
make -f 2019.mk STEM=2020bell-lst veryclean
make -f 2019.mk STEM=2020bell-lst pdf
% Local Variables:
% coding: utf-8-unix
% ee-tla: "lst"
% End: