% (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,PQ &:& Ø \\
  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=ax=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->>cdb \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->>dd->>c)
%:  ---------------
%:    c->>dd->>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->>dd->>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->>cc->>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:
