|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (find-angg "LATEX/2008induction.tex")
% http://angg.twu.net/LATEX/2008induction.tex.html
% http://angg.twu.net/LATEX/2008induction.pdf
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008induction.tex && latex 2008induction.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2008induction.tex && pdflatex 2008induction.tex"))
% (eev "cd ~/LATEX/ && Scp 2008induction.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (find-dvipage "~/LATEX/2008induction.dvi")
% (find-pspage "~/LATEX/2008induction.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -P pk -o 2008induction.ps 2008induction.dvi")
% (find-pspage "~/LATEX/2008induction.ps")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2008induction.pdf" (ee-twupfile "LATEX/2008induction.pdf") 'over)
% (ee-cp "~/LATEX/2008induction.pdf" (ee-twusfile "LATEX/2008induction.pdf") 'over)
% «.e-mail» (to "e-mail")
% «.incr-and-decr» (to "incr-and-decr")
% «.types» (to "types")
% «.definitions» (to "definitions")
% «.cases-0-1-9» (to "cases-0-1-9")
% «.cases-0-1-9-2» (to "cases-0-1-9-2")
% «.lemmas» (to "lemmas")
% «.proofs-5-to-11» (to "proofs-5-to-11")
% «.proofs-12-to-15ppp» (to "proofs-12-to-15ppp")
% «.proofs-16-to-19» (to "proofs-16-to-19")
% «.proofs-20-to-23» (to "proofs-20-to-23")
% «.interval-lemmas» (to "interval-lemmas")
% «.interval-induction» (to "interval-induction")
% «.interval-induction-2» (to "interval-induction-2")
% «.interval-induction-3» (to "interval-induction-3")
% «.intervals» (to "intervals")
\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 2008induction.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")
\tocline {E-mail} {2}
\tocline {Increasing and decreasing} {3}
\tocline {L1, L2, Types} {4}
\tocline {Definitions} {5}
\tocline {Cases 0, 1 and 9} {6}
\tocline {Cases 0, 1 and 9 (2)} {7}
\tocline {Lemmas} {8}
\tocline {Proofs (5 to 11)} {9}
\tocline {Proofs (12 to 15${}'''$)} {10}
\tocline {Proofs (16 to 19)} {11}
\tocline {Proofs (20 to 23)} {12}
\tocline {Interval lemmas} {13}
\tocline {Induction in intervals} {14}
\tocline {Induction in intervals (2)} {15}
\tocline {Intervals} {16}
% (defun a () (interactive) (insert "$\\begin{array}{lcl}\n \\end{array}\n$\n"))
\def\N{\mathbb{N}}
\def\Zer{\ensuremath{\mathsf{Zer}}}
\def\Inj{\ensuremath{\mathsf{Inj}}}
\def\Ind{\ensuremath{\mathsf{Ind}}}
\def\ang#1{\langle#1\rangle}
\def\Pts{\mathcal{P}}
\def\neto{\nearrow}
\def\neto{{\nearrow}}
\def\seto{\searrow}
\def\seto{{\searrow}}
\def\notS{\begin{picture}(0,0)\put(0,1){$\not{}$}\end{picture}S}
\def\epito{\twoheadrightarrow}
\def\nepito{\not\twoheadrightarrow}
\def\isdisjoint{\text{ is disjoint}}
\def\different{\text{ different}}
\def\covers{\text{ covers }}
\newpage
% --------------------
% «e-mail» (to ".e-mail")
% (s "E-mail" "e-mail")
\myslide {E-mail} {e-mail}
{\myttchars
\footnotesize
\begin{verbatim}
Tenho boas notícias sim... vou dar um resumo.
O Petrúcio tava tentando fazer todas as provas numa linguagem - que eu
chamo de "L1" - que não tem conjuntos, interseções, uniões, etc. Eu
tava usando uma linguagem - "L2" - que permite tudo isso e algumas
coisas mais, e que pra mim era óbvio que tudo que eu fizesse em L2
podia ser traduzido para L1...
Bom, eu formalizei essa L2 - não totalmente ainda, mas acho que
suficiente bem - e a tradução dela para L1, e tenho um monte de lemas
interessantes cujas provas em L2 são curtíssimas e bem intuitivas... e
isto inclui vários pedaços da demonstração de que aquela construção do
Petrúcio prova Ind |- Zer \/ Inj.
Essa outra abordagem daqui me pareceu ainda mais natural. Como sempre,
tudo fica mais fácil com um exemplo ("dever de casa pro leitor:
generalize" - só que como eu não tou dando detalhes suficientes esse
dever de casa não é pra ser levado a sério). Imaginem que o nosso N é
isso aqui:
0->1->2->3->4->5->6->4
eu encontrei um modo de caracterizar os elementos do loop (i.e., {4,
5, 6}) e o primeiro cara de fora do loop que aponta pro loop (o 3),
usando L2 - e portanto, com a tradução, tenho um modo de fazer tudo
isso em L1... daí dá pra provar que o 4 tem dois antecessores. Ainda
não chequei todos os detalhes do que eu vou dizer agora, mas lá vai...
Eu chamo de "L" a construção que me dá esse loop, de "[a,\infty)" a
construção que me dá todos os sucessores de a, e de "\notS A" a
construção que me retorna todos os elementos de A cujo sucessor não
está em A. Então nesse caso
L(0) = {4, 5, 6},
[0,\infty) \ L(0) = {1, 2, 3},
\notS([0,\infty) \ L(0)) = {3},
e o sucessor do 3 é o único cara de [0,\infty) que pode ter mais de um
predecessor em [0,\infty) - um dentro do loop e um fora. No caso em
que eu tenho um w com w->0 (por ~Zer) e vale Inj, então todo mundo
pertence a [0,\infty), inclusive o w; aí eu vou ter L(0) = todo mundo,
[0,\infty) \ L(0) = vazio, e não vou poder ter um cara com dois
predecessores... ou seja, Inj (o "Inj de verdade", sobre o N todo),
vai valer.
Depois vou escrever os detalhes direito.
[[]]s, té quinta,
E.
\end{verbatim}
}
\newpage
% --------------------
% «incr-and-decr» (to ".incr-and-decr")
% (s "Increasing and decreasing" "incr-and-decr")
\myslide {Increasing and decreasing} {incr-and-decr}
We will say that a predicate $P$ on $N$ is ``non-decreasing'' when
$ýx.Px⊃PSx$, and ``non-increasing'' when $ýx.PSx⊃Px$; obviously, the
idea is that the characteristic function of a predicate on $N$ may be
non-decreasing or non-increasing (for each arrow $x \to Sx$), and we
are making these terms apply to predicates too.
Notation:
%
$$\begin{array}{rclll}
\neto P & := & ýx.Px⊃PSx && \text{(non-decreasing)}, \\
\seto P & := & ýx.PSx⊃Px && \text{(non-increasing)}. \\
\end{array}
$$
Note that $\neto P \Bij \seto (¬P)$.
We can define the set of successors of $a$ and the set of predecessors
of $b$ as:
%
$$\begin{array}{rclll}
x Ý [a,‚) & := & ýA. Aa ∧ \neto A ⊃ Ax \\
x Ý (-‚,b] & := & ýB. Bb ∧ \seto A ⊃ Bx \\
\end{array}
$$
It is easy to see that $\neto(Ý[a,‚))$ and that $\seto(Ý(-‚,b])$.
Lemma: $bÝ[a,‚) \Bij aÝ(-‚,b]$.
Proof:
%
$$\begin{array}{rcl}
bÝ[a,‚) & \equiv & ýA. Aa ∧ \neto A ⊃ Ab \\
aÝ(-‚,b] & \equiv & ýB. Bb ∧ \seto A ⊃ Ba \\
& \equiv & ýA. ¬Ab ∧ \neto A ⊃ ¬Aa \\
& \equiv & ýA. Aa ∧ \neto A ⊃ Ab. \\
\end{array}
$$
Now let's define the ``closed interval'' $[a,b]$. This will be like
$[a,‚)$, except that the characteristic function will be allowed to
decrease at the arrow $b \to Sb$; when $b \notin [a,‚)$ we will have
$[a,b]=[a,‚)$.
%
$$\begin{array}{rclll}
x Ý [a,b] & := & ýA. Aa ∧ (ýx \neq b.Px⊃PSx) ⊃ Ax \\
\end{array}
$$
Lemma: if $Sb \in [0,b]$ then $[0,b]=[0,‚)$.
Proof: straightforward (look at the arrow $b \to Sb$).
Lemma: if $xÝ[a,b]$ and $Sx \notin [a,b]$ then $x=b$.
Proof: straightforward.
% \msk
%
% Now suppose that $\ang{N, 0, S}$ is a DP-structure in which $\Ind$
% holds. $\Ind$ means that $N = [0,‚)$ (i.e., all elements of $N$ are
% successors of 0).
%
% Definition: a wabc-structure is a DP-structure with four extra
% constants, $w, a, b, c$, in which $\Ind$ holds, and where $Sw=0$ and
% $Sa=Sb=c$. Note that $\Ind$ implies that $w,a,b,c \in [0,‚)$.
%
% In a wabc-structure we have:
% %
% $$\begin{array}{c}
% {} [0,‚) = [0,w] = (-‚,w] = (-‚,0], \\
% {} [0,a]þ\{c\} = [0,c] = [0,b]þ\{c\} \\
% \end{array}
% $$
%
% {\it (oops, the last line is wrong...)}
%
% (Note that a closed interval $[0,x]$ in a wabc-structure either is the
% whole $N$ or has a ``last element'' whose successor is not in the
% interval... and that element is necessarily $x$.)
\newpage
% --------------------
% «types» (to ".types")
% (s "L1, L2, Types" "types")
\myslide {L1, L2, Types} {types}
\large
Conventions:
$\begin{array}{lcl}
x,y &:& N \\
P,Q &:& Ø \\
A,B &:& \Pts(N) \text{\;\;(i.e., $N \to Ø$)} \\
\calA,\calB &:& \Pts(\Pts(N)) \text{\;\;(i.e., $(N \to Ø) \to Ø$)} \\
\end{array}
$
L1:
$\begin{array}{lcl}
x,0,Sx &:& N \\
§,®,¬P,P∧Q,P⊃Q,P∨Q &:& Ø \\
Ax, x=y &:& Ø \\
ýx.P, Îx.P &:& Ø \\
ýA.P, ÎA.P &:& Ø \\
\end{array}
$
L1'':
$\begin{array}{lcl}
ýx \in N.P, Îx\in N.P &:& Ø \\
ýA \subseteq N.P, ÎA \subseteq N.P &:& Ø \\
\end{array}
$
L2:
$\begin{array}{lcl}
\emp, N, AÌB, AþB, A \bsl B &:& \Pts(N) \\
\{a\}, \{a,b\}, \ldots &:& \Pts(N) \\
\emp, \Pts(A), \calAÌ\calB, \calAþ\calB, \calA\bsl\calB &:& \Pts(\Pts(N)) \\
\sst{aÝN}{P}, \bigcap\calA, \bigcup\calB &:& \Pts(N) \\
ýA \subseteq N.P, ÎA \subseteq N.P &:& Ø \\
\sst{A\subseteq N}{P} &:& \Pts(\Pts(N)) \\
x Ý A &:& Ø \\
A Ý \calA &:& Ø \\
\end{array}
$
Extras:
$\begin{array}{lcl}
[a,‚), \, (-‚,b], \, [a,b] &:& \Pts(N) \\
\neto A, \seto A &:& Ø \\
\notS A &:& \Pts(A) \\
La, a \to b, a \epito b, &:& Ø \\
a \le b, a < b, a \sim b &:& Ø \\
L^9a, L'a, L^¢a &:& \Pts(N) \\
\Ind, \Inj, \Zer &:& Ø \\
\end{array}
$
\newpage
% --------------------
% «definitions» (to ".definitions")
% (s "Definitions" "definitions")
\myslide {Definitions} {definitions}
Definitions:
$\begin{array}{lcl}
aÝA &:=& Aa \\
AÝ\calA &:=& \calA A \\
\sst{x}{P} &:=& ðx¨N.P \\
N &:=& ðx¨N.§ \\
\emp &:=& ðx¨N.® \\
\sof{a,b} &:=& \sst{x}{x=a∨x=b} \\
AÌB &:=& \sst{x}{xÝA ∧ xÝB} \\
AþB &:=& \sst{x}{xÝA ∨ xÝB} \\
A \bsl B &:=& \sst{x}{xÝA ∧ ¬xÝB} \\
\sst{A}{P} &:=& ðA.P \\
\bigcup\calA &:=& \sst{x}{ÎAÝ\calA.xÝA} \\
\bigcap\calA &:=& \sst{x}{ýAÝ\calA.xÝA} \\
\neto A &:=& ýx.xÝA⊃SxÝA \\
\seto A &:=& ýx.SxÝA⊃xÝA \\
{}[a,‚) &:=& \bigcap\sst{A}{aÝA ∧ \neto A} \\
{}[-‚,b) &:=& \bigcap\sst{B}{bÝB ∧ \seto B} \\
% {}[a,b] &:=& \bigcap\sst{A}{aÝA ∧ (ýx \neq b.xÝA⊃SxÝA)} \\
\notS A &:=& \sst{aÝA}{Sa \notin A} \\
La &:=& a Ý [Sa,‚) \\
% L^9a &:=& [a,‚) \\
L^¢a &:=& \sst{bÝ[a,‚)}{Lb} \\
L'a &:=& \sst{bÝ[a,‚)}{¬Lb} \\
a \to b &:=& Sa = b \\
a \epito b &:=& [a,‚) \ni b \\
% a \le b &:=& [a,‚) \supseteq [b,‚) \\
% a < b &:=& [a,‚) \supsetneq [b,‚) \\
% a \sim b &:=& [a,‚) = [b,‚) \\
\calA \isdisjoint &:=& ýA,BÝ\calA.A \neq B \funto AþB=\emp \\
\calA \covers a \to Sa &:=& ÎAÝ\calA.\{a,Sa\} \subseteq A \\
{} [a,b] &:=& \bigcap\sst{A}{aÝA ∧ ýxÝA\bsl\{b\}.SxÝA} \\
{} [a,bc] &:=& \bigcap\sst{A}{aÝA ∧ ýxÝA\bsl\{b,c\}.SxÝA} \\
\end{array}
$
\msk
% Theorem: if $c,dÝ[a,‚)$ then $c \epito d ∨ d \epito c$.
%
% Proof: suppose that $c,dÝ[a,‚)$ and $¬(c \epito d)$ and $¬(d \epito
% c)$, and define:
% %
% $$B := \sst{bÝ[a,‚)}{b \epito c ∧ c \epito d}.$$
%
% Then $aÝB$, $\neto B$, and so $[a,‚) \subseteq B$;
%
% but $c,d \notin B$, which contradicts $c,dÝ[a,‚)$.
%
% \msk
%
% Theorem: the elements in $L^¢a$ are all $\sim$-equivalent.
%
% Theorem: the elements in $L^9a/\sim$ are linearly ordered.
%
% \msk
% Theorem: each element $cÝL'a$, $c \neq a$, has exactly one predecessor in $L'a$.
%
% Proof: the predecessor is $\notS (L^9a \bsl \{c\})$ (...)
%
% \msk
%
% Theorem: each element $cÝL^¢a$ has exactly one predecessor in $cÝL^¢a$.
%
% Proof: the predecessor is $\notS (L^¢a \bsl \{c\})$ (...)
%
% \msk
%
% Theorem: if $L'a \neq \emp$ and $L^¢a \neq \emp$ then $L'a$ has a last element ---
%
% namely, $\notS L'a$.
\newpage
% --------------------
% «cases-0-1-9» (to ".cases-0-1-9")
% (s "Cases 0, 1 and 9" "cases-0-1-9")
\myslide {Cases 0, 1 and 9} {cases-0-1-9}
We say that $b$ {\sl is in a loop} --- and we write this as $Lb$ ---
when $Sb \epito b$, i.e., when $bÝ[Sb,‚)$.
With the predicate $L$ we can split $[a,‚)$ in two disjoint parts:
a ``linear part'', $L'a$, and a ``loop part'', $L^¢a$, that are defined as:
%
$$\begin{array}{rcl}
L'a &:=& \sst{bÝ[a,‚)}{¬Lb} \\
L^¢a &:=& \sst{bÝ[a,‚)}{Lb} \\
\end{array}
$$
Theorem: $[a,‚)$ is either a loop,
an infinite straight line, or a ``nine''.
We will call these cases ``0'', ``1'' and ``9'',
according to the shapes of the numbers.
{\myttchars
%\footnotesize
\normalsize
\begin{verbatim}
. <- ... <- .
<- <-
w .
-> ->
a -> . -> . -> .
Case 0
a -> . -> . -> ...
Case 1
...
<- <-
c .
-> ->
a -> . -> ... -> b -> d -> .
\________ ______/ \____ ____/
\/ \/
L'a L°a
Case 9
\end{verbatim}
}
\newpage
% --------------------
% «cases-0-1-9-2» (to ".cases-0-1-9-2")
% (s "Cases 0, 1 and 9 (2)" "cases-0-1-9-2")
\myslide {Cases 0, 1 and 9 (2)} {cases-0-1-9-2}
If $a=0$ and $\Ind$ holds, then $[a,‚)$ is the whole universe (i.e., $N$).
We want to show that $¬\Zer$ only holds in the case ``0'',
and that $¬\Inj$ only holds in the case ``9''.
\msk
Lemmas:
$L^¢a$ is a single loop: for $b,cÝL^¢a$ we have $b \epito c$ and $c \epito b$.
A loop is a sink: there may be arrows from $L'a$ to $L^¢a$,
but no arrows leave $L^¢a$ back to $L'a$.
$L'a$ is linearly ordered: $b,cÝL'a$ either $b \epito c$ and $c \epito b$ hold,
and if both $b \epito c$ and $c \epito b$ hold then $b=c$.
Each element $\neq a$ of $L'a$ has exactly one predecessor (in $L'a$).
\ssk
$\upto$ {\sl [ I have not proved this yet!]}
\ssk
$L'a$ has a last element if and only if we are in the case ``9'';
and this last element (`$b$' in the figure), when it exists, is unique.
The successor of the last element of $L'a$ is in the loop part
(the arrow $b \to d$ in the figure for the case ``9'').
Every element in a loop has a predecessor in the loop
(arrows $w \to a$ in the figure ``0'', $c \to d$ in the figure ``9'');
this shows that $\Inj$ fails in the case ``9''.
\ssk
{\sl [I have not shown yet that the predecessor-in-the-loop is unique...
I will need that to show that $\Inj$ holds in ``0'']}
\ssk
In the cases ``1'' and ``9'' the element $a$ (i.e., 0) has no
predecessor --- i.e., $\Zer$ holds.
\large
\newpage
% --------------------
% «lemmas» (to ".lemmas")
% (s "Lemmas" "lemmas")
\myslide {Lemmas} {lemmas}
$\begin{array}{rl}
(1) & \neto[a,‚) \\
(2) & \seto(-‚,b] \\
(3) & \neto A \Bij \seto(N \bsl A) \\
(4) & bÝ[a,‚) \Bij aÝ(-‚,b] \\
\\
(5) & [a,‚) = \{a\}þ[Sa,‚) \\
(6) & a \epito b \Bij [a,‚) \supseteq [b,‚) \\
(7) & a \epito b, b \epito a \Bij [a,‚) = [b,‚) \\
(8) & a \epito b \funto Sa \epito Sb \\
(9) & La \Bij [a,‚) = [Sa,‚) \\
(10) & La \funto LSa \\
%(11) & \notS(-‚,b] = \emp \Bij Lb \\
(11) & \neto(-‚,b] \Bij Lb \\
\\
(12) & a \neq b, a \epito b \funto Sa \epito b \\
(13) & \notS(-‚,b] \subseteq \{b\} \\
(14) & La \funto [a,‚) \subseteq (-‚,a] \\
(15) & La, a \epito b \funto b \epito a \\
(15') & La, a \epito b \funto Lb \\
(15'') & La, a \epito b, a \epito c \funto b \epito c ∧ c \epito b \\
(15''') & La, a \epito b \funto [a,‚)=[b,‚) \\
\\
(16) & c \nepito d, d \nepito c \funto \neto\sst{b}{b \epito c ∧ b \epito d} \\
(17) & a \epito c, a \epito d, c \nepito d, d \nepito c \funto ® \\
(18) & a \epito c, a \epito d \funto c \epito d ∨ d \epito c \\
(19) & a \epito c, a \epito d, Lc, Ld \funto c \epito d ∧ d \epito c \\
\\
(20) & L'a \neq \emp, L^¢a \neq \emp \funto \notS L'a \neq \emp \\
(21) & b,cÝ\notS L'a, b \neq c, b \epito c \funto ® \\
(22) & b,cÝ\notS L'a, \funto b=c \\
(23) & Ld, Sd \neq d \funto \notS([d,‚)\bsl\{d\}) \neq \emp \\
\end{array}
$
\newpage
% --------------------
% «proofs-5-to-11» (to ".proofs-5-to-11")
% (s "Proofs (5 to 11)" "proofs-5-to-11")
\myslide {Proofs (5 to 11)} {proofs-5-to-11}
%:*.<=.*\subseteq *
%:*.>=.*\supseteq *
%:*->>*\epito *
%:*!->>*\nepito *
%:*<<-*\epiot *
%:*!=*\neq *
%: *b->>cd*b \epito c ∧ b \epito d*
%:
%: SaÝ[a,‚) \neto[a,‚)
%: ---------------------
%: aÝ(\{a\}þ[Sa,‚)) \neto(\{a\}þ[Sa,‚)) aÝ[a,‚) [Sa,‚).<=.[a,‚)
%: -------------------------------------- ---------------------------
%: [a,‚).<=.\{a\}þ[Sa,‚) \{a\}þ[Sa,‚).<=.[a,‚)
%:
%: ^i-5.1 ^i-5.2
%:
%: a->>b [a,‚).>=.[b,‚)
%: ------- ---------- --------------
%: bÝ[a,‚) \neto[a,‚) [a,‚)\ni"b
%: ------------------- ----------
%: [b,‚).<=.[a,‚) a->>b
%:
%: ^i-6.1 ^i-6.2
%:
%: a->>b b->>a [a,‚)=[b,‚) [a,‚)=[b,‚)
%: -------------- -------------- -------------- --------------
%: [a,‚).>=.[b,‚) [b,‚).>=.[a,‚) [a,‚).>=.[b,‚) [a,‚).<=.[b,‚)
%: ------------------------------- -------------- --------------
%: [a,‚)=[b,‚) a->>b b->>a
%:
%: ^i-7.1 ^i-7.2 ^i-7.3
%:
%: [bÝ\{a\}]^1
%: -----------
%: a->>b b=a
%: ------- ----- -----------
%: bÝ[a,‚) Sb=Sa [bÝ[Sa,‚)]^1 \neto[Sa,‚)
%: -------------- --------- -------------------------
%: bÝ\{a\}þ[Sa,‚) SbÝ[Sa,‚) SbÝ[Sa,‚)
%: --------------------------------------------1 -----------
%: SbÝ[Sa,‚) \neto[Sa,‚)
%: -----------------------------------------------
%: [Sb,‚).<=.[Sa,‚)
%: ----------------
%: Sa->>Sb
%:
%: ^i-8
%:
%: La [a,‚)=[Sa,‚)
%: ------ ------ ------------
%: Sa->>a a->>Sa aÝ[Sa,‚)
%: --------------- --------------- --------
%: [Sa,‚).>=.[a,‚) [a,‚).>=.[Sa,‚) Sa->>a
%: --------------------------------- ------
%: [a,‚)=[Sa,‚) La
%:
%: ^i-9.1 ^i-9.2
%:
%: La
%: ------
%: Sa->>a
%: --------
%: SSa->>Sa
%: --------
%: LSa
%:
%: ^i-10
%:
%: [bÝ(-‚,a]]^1
%: ------------
%: b->>a La
%: ------- ------ --------
%: Sb->>Sa Sa->>a aÝ(-‚,a] \neto(-‚,a]
%: ----------------- ---------------------
%: Sb->>a SaÝ(-‚,a]
%: --------- ---------
%: SbÝ(-‚,a] Sa->>a
%: -----------1 ------
%: \neto(-‚,a] La
%:
%: ^i-11.1 ^i-11.2
%:
$$\ded{i-5.1} \qquad \ded{i-5.2}$$
$$\ded{i-6.1} \qquad \ded{i-6.2}$$
$$\ded{i-7.1} \qquad \ded{i-7.2} \qquad \ded{i-7.3}$$
$$\ded{i-8}$$
$$\ded{i-9.1} \qquad \ded{i-9.2}$$
$$\ded{i-10}$$
$$\ded{i-11.1} \qquad \ded{i-11.2}$$
\newpage
% --------------------
% «proofs-12-to-15ppp» (to ".proofs-12-to-15ppp")
% (s "Proofs (12 to 15${}'''$)" "proofs-12-to-15ppp")
\myslide {Proofs (12 to 15${}'''$)} {proofs-12-to-15ppp}
%: a->>b
%: --------------
%: b!=a bÝ\{a\}þ[Sa,‚)
%: ---------------------
%: bÝ[Sa,‚)
%: --------
%: Sa->>b
%:
%: ^i-12
%:
%: [aÝ(-‚,b]\bsl\{b\}]^1
%: ---------------------
%: [aÝ(-‚,b]\bsl\{b\}]^1 aÝ(-‚,b]
%: --------------------- --------
%: a!=b a->>b
%: -------------------------------
%: Sa->>b
%: ---------
%: SaÝ(-‚,b]
%: --------------------1
%: \notS(-‚,b].<=.\{b\}
%:
%: ^i-13
%:
%: La
%: -------- -----------
%: aÝ(-‚,a] \neto(-‚,a]
%: ----------------------
%: [a,‚).<=.(-‚,a]
%:
%: ^i-14
%:
%: La
%: ---------------
%: [a,‚).<=.(-‚,a]
%: -----------------
%: bÝ[a,‚)=>bÝ(-‚,a]
%: -----------------
%: a->>b=>b->>a
%:
%: ^i-15
%:
%:
%: La a->>b
%: ---------
%: b->>a La
%: ------- ------
%: Sb->>Sa Sa->>a a->>b
%: ------------------------
%: Sb->>b
%: ------
%: Lb
%:
%: ^i-15'
%:
%: La a->>b La a->>c
%: --------- ---------
%: b->>a a->>c c->>a a->>b
%: -------------- --------------
%: b->>c c->>b
%: -----------------------
%: b->>c∧c->>b
%:
%: ^i-15''
%:
%: La a->>b
%: ---------
%: a->>b b->>a
%: --------------
%: [a,‚)=[b,‚)
%:
%: ^i-15'''
%:
%:
$$\ded{i-13}$$
$$\ded{i-14}$$
$$\ded{i-15}$$
$$\ded{i-15'}$$
$$\ded{i-15''}$$
$$\ded{i-15'''}$$
\newpage
% --------------------
% «proofs-16-to-19» (to ".proofs-16-to-19")
% (s "Proofs (16 to 19)" "proofs-16-to-19")
\myslide {Proofs (16 to 19)} {proofs-16-to-19}
%: [b->>d]^1 c!->>d [b->>c]^1 d!->>c
%: ----------------- -----------------
%: b!=c [b->>c]^1 b!=d [b->>d]^1
%: ---------------------- -----------------------
%: Sb->>c Sb->>d
%: ---------------------------------1
%: \neto\sst{b}{b->>c∧b->>d}
%:
%: ^i-16
%:
%: a->>c a->>d c!->>d d!->>c
%: ----------------- --------------------
%: a->>c a->>d aÝ\sst{b}{b->>cd} \neto\sst{b}{b->>cd}
%: ------------ ----------------------------------------
%: c,dÝ[a,‚) [a,‚).<=.\sst{b}{b->>cd} c!->>d d!->>c
%: ------------------------------------------- -----------------------
%: c,dÝ\sst{b}{b->>cd} c,d\notin\sst{b}{b->>cd}
%: ----------------------------------------------------------------
%: ®
%:
%: ^i-17
%: a->>c a->>d
%: ----------------
%: c!->>d∧d!->>c=>®
%: ----------------
%: ¬(c!->>d∧d!->>c)
%: ----------------
%: ¬(¬c->>d∧¬d->>c)
%: ----------------
%: ¬¬(c->>d∨d->>c)
%: ---------------
%: c->>d∨d->>c
%:
%: ^i-18
%:
%: Lc [c->>d]^1 Ld [d->>c]^1
%: ------------- -------------
%: a->>c a->>d [c->>d]^1 d->>c c->>d [d->>c]^1
%: ------------ ------------------ ---------------------
%: c->>d∨d->>c c->>d∧d->>c c->>d∧d->>c
%: ------------------------------------------------------------1
%: c->>d∧d->>c
%:
%: ^i-19
%:
$$\ded{i-16}$$
$$\ded{i-17}$$
$$\ded{i-18}$$
$$\ded{i-19}$$
\newpage
% --------------------
% «proofs-20-to-23» (to ".proofs-20-to-23")
% (s "Proofs (20 to 23)" "proofs-20-to-23")
\myslide {Proofs (20 to 23)} {proofs-20-to-23}
%: L'a!=\emp [\notS"L'a=\emp]^1
%: --------- ------------------
%: aÝL'a \neto"L'a
%: --------------------- ------------
%: [a,‚).<=.L'a L'a.<=.[a,‚)
%: -----------------------------------
%: L'a=[a,‚)
%: ---------
%: L^¢a=\emp L^¢a!=\emp
%: -------------------------------------
%: ®
%: ---------------1
%: \notS"L'a!=\emp
%:
%: ^i-20
%:
%: bÝ\notS"L'a b!=c b->>c cÝ\notS"L'a
%: ---------- ----------- -----------
%: a->>Sb Sb->>c cÝL'a bÝ\notS"L'a
%: --------------------------------- ------------
%: SbÝL'a Sb\notin"L'a
%: --------------------------------------
%: ®
%:
%: ^i-21
%:
%: b,cÝ\notS"L'a
%: -------------
%: b,cÝL'a
%: ---------
%: b,cÝ[a,‚) b,cÝ\notS"L'a [b!=c]^2 [b->>c]^1 b,cÝ\notS"L'a [b!=c]^2 [b->>c]^1
%: ----------- ---------------------------------- ----------------------------------
%: b->>c∨c->>b ® ®
%: -----------------------------------------------------------------1
%: ®
%: ---2
%: b=c
%:
%: ^i-22
%:
%: Sd!=d [\notS([d,‚)\bsl\{d\})=\emp]^1
%: ------------------- ------------------------------
%: Ld SdÝ([d,‚)\bsl\{d\}) \neto([d,‚)\bsl\{d\})
%: ------------ ----------------------------------------------
%: [d,‚)=[Sd,‚) [Sd,‚).<=.[d,‚)\bsl\{d\}
%: --------------------------------------------------
%: [d,‚).<=.[d,‚)\bsl\{d\}
%: -----------------------
%: ®
%: ---------------------------1
%: \notS([d,‚)\bsl\{d\})!=\emp
%:
%: ^i-23
%:
$$\ded{i-20}$$
$$\ded{i-21}$$
$$\ded{i-22}$$
$$\ded{i-23}$$
\newpage
% --------------------
% «interval-lemmas» (to ".interval-lemmas")
% (s "Interval lemmas" "interval-lemmas")
\myslide {Interval lemmas} {interval-lemmas}
Definitions:
$\begin{array}{lcl}
S(A) &:=& \sst{x}{ÎaÝA. Sa=x} \\
A,\_ &:=& \sst{X}{A \subseteq X} \\
\_,B &:=& \sst{X}{S(X \bsl B) \subseteq X} \\
A,B &:=& A,\_ Ì \_,B \\{}
[A,B] &:=& \bigcap \, A,B \\{}
[a,b] &:=& \bigcap \, \{a\},\{b\} \\{}
[ab,cd] &:=& \bigcap \, \{a,b\},\{c,d\} \\
\end{array}
$
\msk
Elementary lemmas:
$\begin{array}{rl}
(1) & A \subseteq [A,B] \\
(2) & \notS([A,B]) \subseteq B \\
(3) & [a,B] \subseteq [a,‚) = [a,\emp] \\
(4) & AþA',\_ = A,\_ Ì A',\_ \\
(5) & AÌA',\_ = A,\_ þ A',\_ \\
(6) & \_,BþB' = \_,B þ \_,B' \\
(7) & \_,BÌB' = \_,B Ì \_,B' \\
(8) & [AþA',B] \\& = \bigcap(A,\_ Ì A',\_ Ì \_,B) \\& = [A,B] þ [A',B] \\
(9) & [A,BÌB'] \\& = \bigcap(A,\_ Ì \_,B Ì \_,B') \\& = [A,B] þ [A,B'] \\
\end{array}
$
\msk
Order lemmas:
$\begin{array}{rl}
(1) & [AþS(B),BþB'] = [AþS(B),B'] \\
(2) & b \notin [A,C] \funto [A,C] = [A,\{b\}þC] \\
(3) & BÌ[A,C] = \emp \funto [A,C] = [A,BþC] \\
(4) & b,b' Ý \notS([a,B]) \funto b=b' \\
(5) & [a,BþC] = [a,B] \text{ or } [a,BþC] = [a,C] \\
(6) & bÝ[a,c] \funto [a,b] \subseteq [a,c] \\
(7) & bÝ[a,c] \funto [b,c] \subseteq [a,c] \\
(8) & b,SbÝ[a,c]\phantom{, \; b \neq Sb} \funto [a,c] = [a,b]þ[Sb,c] \\
(9) & b,SbÝ[a,c] , \; b \neq Sb \funto [a,c] = [a,b]÷[Sb,c] \\
\end{array}
$
\newpage
% --------------------
% «interval-induction» (to ".interval-induction")
% (s "Induction in intervals" "interval-induction")
\myslide {Induction in intervals} {interval-induction}
Induction lemmas:
$\begin{array}{rl}
(1) & A \subseteq X, \; S(X \bsl B) \subseteq X \funto [A,B] \subseteq X \\
(2) & A \subseteq X \subseteq [A,B], \; S(X \bsl B) \subseteq X \funto [A,B] = X \\
\end{array}
$
\msk
Small lemmas: one whose proof I have not finished yet,
$\begin{array}{rl}
(1) & bÝ[a,c] \funto [a,b] = [a,bc] \subseteq [a,c] \\
\end{array}
$
%: -----------------
%: \_,bc.>=.\_,b
%: -------------------------------
%: a,\_Ì\_,bc.>=.a,\_Ì\_,b
%: -------------------------------
%: a,bc.>=.a,b
%: ---------------
%: \bigcapa,bc.<=.\bigcapa,b
%: -----------------------------
%: [a,bc].<=.[a,b]
%:
%: ^indintfoo
%:
$$\ded{indintfoo}$$
%: c\notin[a,b]∨b=c
%: -------------------------------
%: [a,b]\bsl\{b,c\}=[a,b]\bsl\{b\}
%: ------- -------------------------------
%: aÝ[a,b] S([a,b]\bsl\{b,c\}).<=.[a,b]
%: -----------------------------------------
%: [a,b]Ýa,\_Ì\_,bc
%: --------------------
%: [a,b]Ýa,bc
%: --------------------
%: [a,b].>=.\bigcapa,bc
%: --------------------
%: [a,b].>=.[a,bc]
%:
%: ^indint2
%:
%:
%: \_,bc.<=.\_,c
%: -------------------------------
%: a,\_Ì\_,bc.<=.a,\_Ì\_,c
%: -----------------------------------------------
%: \bigcap(a,\_Ì\_,bc).>=.\bigcap(a,\_Ì\_,c)
%: -----------------------------------------------
%: \bigcapa,bc.>=.\bigcapa,c
%: ---------------------------
%: [a,bc].<=.[a,c]
%:
%: ^indint3
%:
$$\ded{indint2}$$
$$\ded{indint3}$$
\newpage
% --------------------
% «interval-induction-2» (to ".interval-induction-2")
% (s "Induction in intervals (2)" "interval-induction-2")
\myslide {Induction in intervals (2)} {interval-induction-2}
...and another small lemma (whose proof is complete):
$\begin{array}{rl}
(2) & bÝ[a,c] \funto [b,c] \subseteq [ab,c] = [a,c] \\
\end{array}
$
%:
%: -----------------
%: b,\_.>=.ab,\_
%: -------------------------------
%: b,\_Ì\_,c.>=.ab,\_Ì\_,c
%: -------------------------------------------------
%: \bigcap(b,\_Ì\_,c).<=.\bigcap(ab,\_Ì\_,c)
%: -------------------------------------------------
%: [b,c]\subseteq[ab,c]
%:
%: ^indint0
%:
%: bÝ[a,c]
%: --------------
%: bÝ\bigcapa,c
%: --------------------
%: b,\_\supseteqa,c
%: --------------------
%: b,\_Ìa,c=a,c
%: --------------------------
%: b,\_Ìa,\_Ì\_,c=a,c
%: --------------------------
%: ab,\_Ì\_,c=a,c
%: --------------------
%: ab,c=a,c
%: ------------
%: [ab,c]=[a,c]
%:
%: ^indint1
%:
$$\ded{indint0} \qquad \ded{indint1}$$
Big lemmas (not proved yet):
$\begin{array}{rl}
(1) & b,cÝ[a,c], b \neq c \funto [a,Sb] = [a,b] ÷ \{Sb\} \\
(2) & b,cÝ[a,c], b \neq c \funto [b,c] = \{b\} ÷ [Sb,c] \\
(3) & b,cÝ[a,c], b \neq c \funto [a,c] = [a,b] ÷ [Sb,c] \\
\end{array}
$
\newpage
% --------------------
% «interval-induction-3» (to ".interval-induction-3")
% (s "Induction in intervals (3)" "interval-induction-3")
\myslide {Induction in intervals (3)} {interval-induction-3}
Definitions:
$\begin{array}{rcl}
{} [a,b;Sb] &:=& ([a,Sb] = [a,b]÷\{Sb\}) \\
{} [b;Sb,c] &:=& ([b,c] = \{b\}÷[Sb,c]) \\
{} [a,b;Sb,c] &:=& ([a,c] = [a,b]÷[Sb,c]) \\
{} [a,b;Sb;SSb,c] &:=& ([a,c] = [a,b]÷\{Sb\}÷[SSb,c]) \\
\end{array}
$
\msk
Induction rules:
%:
%: P(a) ýbÝ[a,‚).P(b)⊃P(Sb)
%: -------------------------
%: ýbÝ[a,‚).P(b)
%:
%: ^iind-1
%:
%: P(a) ýbÝ[a,c],b\neq"c.P(b)⊃P(Sb)
%: ---------------------------------
%: ýbÝ[a,c].P(b)
%:
%: ^iind-2
%:
%: P(a) ýbÝ[a,c],b\neq"c,Sb\neq"c.P(b)⊃P(Sb)
%: ------------------------------------------
%: ýbÝ[a,c],b\neq"c.P(b)
%:
%: ^iind-3
%:
$$\ded{iind-1}$$
$$\ded{iind-2}$$
$$\ded{iind-3}$$
\msk
Lemmas:
%:
%: cÝ[a,c] a\neq"c b,Sb,cÝ[a,c] b,Sb\neq"c [a,b;Sb] b,cÝ[a,c] b\neq"c
%: ================ ================================== ==================
%: [a,a;Sa] [a,Sb;SSb] [a,b;Sb]
%:
%: ^ind-abb0 ^ind-abb+ ^ind-abb
%:
%: cÝ[a,c] a\neq"c b,Sb,cÝ[a,c] b,Sb\neq"c [b;Sb,c] b,cÝ[a,c] b\neq"c
%: ================ ================================== ==================
%: [a;Sa,c] [Sb;SSb,c] [b;Sb,c]
%:
%: ^ind-bbc0 ^ind-bbc+ ^ind-bbc
%:
%: cÝ[a,c] a\neq"c b,Sb,cÝ[a,c] b,Sb\neq"c [a,b;Sb,c] b,cÝ[a,c] b\neq"c
%: ================ ==================================== ==================
%: [a,a;Sa,c] [a,Sb;SSb,c] [a,b;Sb,c]
%:
%: ^ind-abbc0 ^ind-abbc+ ^ind-abbc
%:
$$\ded{ind-abb0} \qquad \ded{ind-abb+} \qquad \ded{ind-abb}$$
$$\ded{ind-bbc0} \qquad \ded{ind-bbc+} \qquad \ded{ind-bbc}$$
$$\ded{ind-abbc0} \qquad \ded{ind-abbc+} \qquad \ded{ind-abbc}$$
Proofs:
%:
%: b,Sb,cÝ[a,c] b,Sb\neq"c [a,b;Sb]
%: ==================================
%: [a,Sb;SSb]
%:
%: ^ind-abb++
%:
%:
%: b,Sb,cÝ[a,c] b,Sb\neq"c [b;Sb,c]
%: ==================================
%: [Sb;SSb,c]
%:
%: ^ind-bbc++
%:
%:
%: Sb,cÝ[a,c] Sb\neq"c
%: --------------------
%: [a,b;Sb,c] [Sb;SSb,c] b,cÝ[a,c] b\neq"c
%: -------------------------- ------------------
%: [a,b;Sb;SSb,c] [a,b;Sb]
%: ----------------------------------------
%: [a,Sb;SSb,c]
%:
%: ^ind-abbc++
%:
$$\ded{ind-abb++}$$
$$\ded{ind-bbc++}$$
$$\ded{ind-abbc++}$$
\newpage
% --------------------
% «intervals» (to ".intervals")
% (s "Intervals" "intervals")
\myslide {Intervals} {intervals}
{\bf [This is old! Cannibalize and delete it.]}
Convention: whenever we write $[a,b]$ it is implicit that $a \epito b$.
We will write $A÷B÷C$ to indicate a disjoint union ---
i.e., $AþBþC$, but it is implicit that $\{A,B,C\}$ is disjoint.
\msk
Lemmas:
$\begin{array}{rl}
(1) & \notS[a,b] \subseteq \{b\} \\
(2) & a \neq b \funto [a,b] = \{a\}÷[Sa,b] \\
(3) & a,b,c \different,\, bÝ[a,c] \funto [a,b]÷[Sb,c] \\
(4) & b,cÝ[a,b] \funto [a,bc]=[a,b]∨[a,bc]=[a,c] \\
(5) & a,b,c,d \different, \, b,cÝ[a,d], \, bÝ[a,bc] \funto \\
& Sb,c \notin [a,bc] \\
(6) & a,b,c,d \different, \, b,cÝ[a,d] \funto \\
& [a,d]=\{a\}÷[Sa,bc]÷[Sb,cd]÷[Sc,bd] \\
(7) & a,b,c,d \different, \, b,cÝ[a,d] \funto \\
& \{\{a\},\,[Sa,bc],\,[Sb,cd],\,[Sc,bd]\} \text{ does not cover } \\
& a \to Sa,\, b \to Sb, \text{ or } c \to Sc \\
(8) & La \funto [Sa,a] = [Sa,‚) = [a,‚) \\
\end{array}
$
\msk
Now suppose that $a$ is in a loop, that $b,cÝ[Sa,a]$,
that $Sa,b,c,a$ are different, and that $Sb=Sc$.
This implies that
%
$$[Sa,a]=\{Sa\}÷[SSa,bc]÷[Sb,ca]÷[Sc,ba],$$
and this should be absurd (check).
\msk
This implies that each element in a loop
has at most one predecessor in the loop.
We already knew that each element in a loop
has a predecessor in the loop, so this shows that
%
$$La \funto Î!pÝ[a,‚).Sp=a.$$
% (fooi "\\nepito" "!->>" "\\epito" "->>" "\\funto" "=>" "\\neq" "!=")
% (fooi "\\nepito" "!->>" "\\epito" "->>" "\\funto" "=>")
%*
\end{document}
% Local Variables:
% coding: raw-text-unix
% ee-anchor-format: "«%s»"
% End: