% (find-angg "LATEX/2018-2-MD-sequentes.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2018-2-MD-sequentes.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2018-2-MD-sequentes.pdf"))
% (defun e () (interactive) (find-LATEX "2018-2-MD-sequentes.tex"))
% (defun u () (interactive) (find-latex-upload-links "2018-2-MD-sequentes"))
% (find-xpdfpage "~/LATEX/2018-2-MD-sequentes.pdf")
% (find-sh0 "cp -v  ~/LATEX/2018-2-MD-sequentes.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2018-2-MD-sequentes.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2018-2-MD-sequentes.pdf
%               file:///tmp/2018-2-MD-sequentes.pdf
%           file:///tmp/pen/2018-2-MD-sequentes.pdf
% http://angg.twu.net/LATEX/2018-2-MD-sequentes.pdf

% «.complicadas»	(to "complicadas")
%   «.by-cases»		(to "by-cases")
%   «.forall-easy»	(to "forall-easy")
%   «.forall-hard»	(to "forall-hard")
%   «.exist-easy»	(to "exist-easy")
%   «.exist-hard»	(to "exist-hard")
% «.defs-recursivas»	(to "defs-recursivas")

\documentclass[oneside]{article}
\usepackage[colorlinks]{hyperref} % (find-es "tex" "hyperref")
%\usepackage[latin1]{inputenc}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{pict2e}
\usepackage{color}                % (find-LATEX "edrx15.sty" "colors")
\usepackage{colorweb}             % (find-es "tex" "colorweb")
\usepackage{lplfitch}             % (find-es "tex" "lplfitch")
%\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
\catcode`\^^J=10                      % (find-es "luatex" "spurious-omega")
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")
\def\expr#1{\directlua{output(tostring(#1))}}
\def\eval#1{\directlua{#1}}
%
\usepackage{edrx15}               % (find-angg "LATEX/edrx15.sty")
\input edrxaccents.tex            % (find-angg "LATEX/edrxaccents.tex")
\input edrxchars.tex              % (find-LATEX "edrxchars.tex")
\input edrxheadfoot.tex           % (find-dn4ex "edrxheadfoot.tex")
\input edrxgac2.tex               % (find-LATEX "edrxgac2.tex")
%
% (find-angg ".emacs.papers" "latexgeom")
% (find-latexgeomtext "total={6.5in,8.75in},")
\usepackage[%total={6.5in,4in},
            %textwidth=4in,  paperwidth=4.5in,
            %textheight=5in, paperheight=4.5in,
            a4paper,
            top=1.5in, left=1.5in%, includefoot
           ]{geometry}
%
\begin{document}

\catcode`\^^J=10

\edrxcolors

\def\V{\mathbf{V}}
\def\F{\mathbf{F}}
\def\Par  {\mathsf{par}}
\def\Impar{\mathsf{impar}}

\directlua{dofile "edrxtikz.lua"} % (find-LATEX "edrxtikz.lua")
\directlua{dofile "edrxpict.lua"} % (find-LATEX "edrxpict.lua")
%L V.__tostring = function (v) return format("(%.3f,%.3f)", v[1], v[2]) end

% (code-xpdf     "wikiseq" "~/tmp/Sequent calculus - Wikipedia.pdf")
% (code-pdf-text "wikiseq" "~/tmp/Sequent calculus - Wikipedia.pdf")
% (find-wikiseqpage)
% (find-wikiseqpage 5)
% (find-wikiseqtext)


%:   Δ⊢Γ          Δ⊢Γ       
%:  -----(WL-)   -----(WR-)  
%:  Δ,A⊢Γ        Δ⊢Γ,A      
%:                          
%:  ^WL-         ^WR-        
%:
%:   Δ,Γ⊢Σ          Δ⊢Γ,Σ       
%:  -----(WL)    -----(WR)  
%:  Δ,A,Γ⊢Σ      Δ⊢Γ,A,Σ      
%:                          
%:  ^WL          ^WR        
%:
%:  Δ,A,B,Γ⊢Σ       Δ⊢Γ,A,B,Σ       
%:  ---------(PL)   ---------(PR)  
%:  Δ,B,A,Γ⊢Σ       Δ⊢Γ,B,A,Σ
%:                          
%:     ^PL             ^PR        
%:
%:  Δ,A,A⊢Γ         Δ⊢Γ,A,A       
%:  -------(CL-)     -------(CR-)   
%:   Δ,A⊢Γ           Δ⊢Γ,A        
%:
%:    ^CL-             ^CR-
%:
%:  Δ,A,A,Γ⊢Σ         Δ⊢Γ,A,A,Σ       
%:  -------(CL)     -------(CR)   
%:   Δ,A,Γ⊢Σ           Δ⊢Γ,A,Σ        
%:
%:    ^CL               ^CR
%:
\pu


% (find-wikiseqpage 5)

%:
%:  Γ⊢Δ,A∧B          Γ⊢Δ,A∧B          Γ,A∧B⊢Δ       Γ⊢A,Δ   Σ⊢B,Π
%:  -------(R∧_1)    -------(R∧_2)    -------(L∧)   -------------(R∧)
%:   Γ⊢Δ,A            Γ⊢Δ,B           Γ,A,B⊢Δ        Γ,Σ⊢A∧B,Δ,Π
%:                                  
%:   ^Rand1           ^Rand2           ^Land          ^Rand          
%:
%:
%:  Γ,A∨B⊢Δ          Γ,A∨B⊢Δ          Γ⊢A∨B,Δ       Γ,A⊢Δ   Σ,B⊢Π    
%:  -------(L∨_1)    -------(L∨_2)    -------(R∨)   -------------(L∨)
%:   Γ,A⊢Δ            Γ,B⊢Δ           Γ⊢A,B,Δ        Γ,Σ,A∨B⊢Δ,Π     
%:                                                                   
%:   ^Lor1            ^Lor2            ^Ror           ^Lor
%:
%:
\pu

%:           Γ⊢Δ,A  A,Σ⊢Π
%:  ---(I)   ------------(Cut)
%:  A⊢A        Γ,Σ⊢Δ,Π
%:
%:  ^I          ^Cut
%:
\pu

%:
%:   Γ⊢A,Δ   Σ,B⊢Π         Γ⊢A,Δ   Σ⊢B,Π
%:   --------------(→L)    -------------(→R)    
%:   Γ,Σ,A→B⊢Δ,Π             Γ⊢A→B,Δ       
%:
%:   ^toL                     ^toR
%:
\pu

%:
%:   Γ⊢A,Δ        Γ,A⊢Δ        
%:   -----(¬L)    -----(¬R)    
%:   Γ,¬A⊢Δ       Γ⊢¬A,Δ       
%:
%:   ^notL        ^notR
%:
\pu


% (find-wikiseqpage 8)
%:
%:    Γ,P[y:=t]⊢Δ           Γ⊢P,Δ       
%:    -----------(∀L)     -----------(∀R)^*
%:    Γ,∀y.P⊢Δ            Γ⊢∀y.P,Δ        
%:                                          
%:    ^faL                  ^faR              
%:
%:
%:       Γ,P⊢Δ            Γ⊢P[y:=t],Δ             
%:    -----------(∃L)^*   -----------(∃R)
%:    Γ,∃y.P⊢Δ            Γ⊢∃y.P,Δ          
%:                                            
%:    ^exL                  ^exR              
%:
\pu



\fbox{
\begin{tabular}{l}
Regras estruturais: \\
weakening, permutation, contraction \\
\\
$\begin{array}{ccc}
 \ded{WL-} && \ded{WR-} \\ \\
 \ded{WL}  && \ded{WR} \\ \\
 \ded{PL}  && \ded{PR} \\ \\
 \ded{CL-} && \ded{CR-} \\ \\
 \ded{CL}  && \ded{CR} \\ \\
 \end{array}
$ \\
\end{tabular}
}
%
\fbox{
\begin{tabular}{l}
Identidade e cut:
\\
$\begin{array}{ccc}
 \ded{I} \\ \\
 \ded{Cut} \\
 \end{array}
$ \\
\end{tabular}
}


\ssk

\fbox{
\begin{tabular}{l}
Regras lógicas pro $∧$: \\
\\
$\begin{array}{c}
\ded{Rand1} \\ \\
\ded{Rand2} \\ \\
\ded{Land} \\ \\
\ded{Rand} \\
\end{array}
$
\end{tabular}
}
%
%\quad
%
\fbox{
\begin{tabular}{l}
Regras lógicas pro $∨$: \\
\\
$\begin{array}{c}
\ded{Lor1} \\ \\
\ded{Lor2} \\ \\
\ded{Ror} \\ \\
\ded{Lor} \\
\end{array}
$
\end{tabular}
}

\ssk

\fbox{
\begin{tabular}{l}
Regras lógicas pro $→$: \\
\\
$\begin{array}{c}
\ded{toL} \\ \\
\ded{toR} \\
\end{array}
$
\end{tabular}
}
%
%\quad
%
\fbox{
\begin{tabular}{l}
Regras lógicas pro $¬$: \\
\\
$\begin{array}{c}
\ded{notL} \\ \\
\ded{notR} \\
\end{array}
$
\end{tabular}
}

\ssk

\fbox{
\begin{tabular}{l}
Regras lógicas para o $∀$: \\
\\
$\begin{array}{ccc}
 \ded{faR}  \\ \\
 \ded{faL} \\
 \end{array}
$ \\
\end{tabular}
}
\fbox{
\begin{tabular}{l}
Regras lógicas para o $∃$: \\
\\
$\begin{array}{ccc}
 \ded{exR}  \\ \\
 \ded{exL} \\
 \end{array}
$ \\
\end{tabular}
}

\ssk

Nas regras $(∀R)^*$ e $(∃L)^*$ o `${}^*$' quer dizer que o $y$ não
pode

aparecer como variável livre em $Γ$ ou $Δ$.


\newpage

%:
%:
%:
%:
%:  A∧B⊢C     A∧B⊢C
%:  =====  =  -----(L∧)
%:  A,B⊢C     A,B⊢C
%:
%:  ^ex1a     ^ex1asol
%:
%:                        -------(I)
%:                        A∧B⊢A∧B
%:                        -------(R∧_2)
%:                         A∧B⊢A         A,B⊢C
%:           -------(I)    -------------------(Cut)
%:           A∧B⊢A∧B          A∧B,B⊢C
%:           -------(R∧_2)    -------(PL)
%:            A∧B⊢B        \b B,A∧B⊢C
%:            -----------------------(Cut)
%:  A∧B⊢C             A∧B,A∧B⊢C
%:  =====  =          ---------(CL)
%:  A,B⊢C              A∧B⊢C
%:
%:  ^ex1b              ^ex1bsol
%:
%:
%:
%:
%:
%:  A⊢B∨C     A⊢B∨C
%:  =====  =  -----(R∨)
%:  A⊢B,C     A⊢B,C
%:
%:  ^ex2a     ^ex2asol
%:
%:
%:                       -------(I)
%:                       B∨C⊢B∨C
%:                       -------(L∨_2)
%:             A⊢B,C     C⊢B∨C
%:             -------------------(Cut)   -------(I)
%:              A⊢B,B∨C                  B∨C⊢B∨C
%:              -------(PR)              -------(R∧_2)
%:              A⊢B∨C,B                  B⊢B∨C
%:              ------------------------------(Cut)
%:  A⊢B,C               A⊢B∨C,B∨C
%:  =====  =            ---------(CR)
%:  A⊢B∨C                A⊢B∨C
%:
%:  ^ex2b                ^ex2bsol
%:  
\pu
\def\b{\hskip-6ex}

$\begin{array}{rcl}
 \ded{ex1a} &=& \ded{ex1asol} \\
 \ded{ex1b} &=& \ded{ex1bsol} \\
 \\
 \\
 \ded{ex2a} &=& \ded{ex2asol} \\
 \ded{ex2b} &=& \ded{ex2bsol} \\
 \end{array}
$



% (find-es "tex" "lplfitch")
% (find-lplfitchpage)
% (find-lplfitchtext)


% \fitchprf{}{
%     \subproof{\pline[1.]{\uni{x}{(Cube(x)\lif Small(x))}}}{
%         \subproof{
%                 \pline[2.]{\exi{x}{Cube(x)}}
%             }{
%             \boxedsubproof[3.]{a}{Cube(a)}{
%                 \pline[4.]{Cube(a)\lif Small(a)}[\lalle{1}]\\
%                 \pline[5.]{Small(a)}[\life{4}{3}]\\
%                 \pline[6.]{\exi{x}{Small(x)}}[\lexii{5}]
%             }
%             \pline[7.]{\exi{x}{Small(x)}}[\lexie{2}{3--6}]
%         }
%         \pline[8.]{\exi{x}{Cube(x)}\lif \exi{x}{Small(x)}}[\lifi{2--7}]
%     }
%     \pline[9.]{\brokenform{(\uni{x}{(Cube(x)\lif Small(x))}\lif}{
%         \formula{(\exi{x}{Cube(x)} \lif \exi{x}{Small(x)})}}}[\lifi{1--8}]
% }


\newpage

%   ____                      _ _               _           
%  / ___|___  _ __ ___  _ __ | (_) ___ __ _  __| | __ _ ___ 
% | |   / _ \| '_ ` _ \| '_ \| | |/ __/ _` |/ _` |/ _` / __|
% | |__| (_) | | | | | | |_) | | | (_| (_| | (_| | (_| \__ \
%  \____\___/|_| |_| |_| .__/|_|_|\___\__,_|\__,_|\__,_|___/
%                      |_|                                  
%
% «complicadas» (to ".complicadas")
\section{Cinco regras complicadas}


% (mdq182 58 "20181126" "Regras de dedução que faltam, estruturas algébricas")

% «by-cases» (to ".by-cases")
\subsection{Demonstrações por casos}

A regra básica é esta aqui, que é baseada na $(L∨)$:
%:
%:  Γ,P∨Q,P⊢R   Γ,P∨Q,Q⊢R       
%:  ---------------------(DC)   
%:     Γ,P∨Q⊢R          
%:
%:     ^casos
%:
%:  Γ,P∨Q,P⊢R   Γ,P∨Q,Q⊢R       
%:  ---------------------(L∨)   
%:    Γ,P∨Q,Γ,P∨Q,P∨Q⊢R
%:    =================(PL)
%:    Γ,Γ,P∨Q,P∨Q,P∨Q⊢R
%:    =================(CL)
%:          Γ,P∨Q⊢R
%:
%:          ^casos-2
%:
\pu
$$\ded{casos}
  \quad := \quad
  \ded{casos-2}
$$

Um exemplo de uso:
%:
%:                           ========================  ==========================
%:                           a∈\Z,\Par(a)⊢\Par(a^2+a)  a∈\Z,\Impar(a)⊢\Par(a^2+a)    
%:  ======================   ----------------------------------------------------(DC)
%:  a∈\Z⊢\Par(a)∨\Impar(a)               a∈\Z,\Par(a)∨\Impar(a)⊢\Par(a^2+a)
%:  -----------------------------------------------------------------------(Cut)
%:                       a∈\Z⊢\Par(a^2+a)
%:
%:                          ^casos2
%:
\pu
$$\ded{casos2}$$

% (find-es "tex" "minipage")

\begin{minipage}[t]{15em}
\par 1) Suponha $Γ$
\par 2) (...)
\par 3) Suponha $P∨Q$
\par 4) Caso 1: Suponha $P$
\par 5) (...)
\par 6) Então $R$
\par 7) Caso 2: Suponha $Q$
\par 8) (...)
\par 9) Então $R$ \qquad (Fecha 7,4)
\end{minipage}!
%
\qquad
%
\begin{minipage}[t]{20em}
\par 1) Suponha $a∈\Z$
\par 2) (...)
\par 3) Suponha $\Par(a)∨\Impar(a)$
\par 4) Caso 1: Suponha $\Par(a)$
\par 5) (...)
\par 6) Então $\Par(a^2+a)$
\par 7) Caso 2: Suponha $\Impar(a)$
\par 8) (...)
\par 9) Então $\Par(a^2+a)$ \qquad (Fecha 7,4)
\end{minipage}



% (find-es "math" "provas-MD-naufel")

Ainda não consegui encontrar exemplos ou exercícios de demonstração
por casos no Scheinerman. A P1 do Fernando Naufel de 2012.2
(``md-122-p1-manha-gab.pdf'') para a turma da manhã tem vários
exemplos de provas por casos em Fitch.



% «forall-easy» (to ".forall-easy")

\subsection{A regra fácil para o `$∀$'}

A regra fácil para o `$∀$' {\sl escolhe um caso particular}: por
exemplo, a partir de $∀a∈\Z.\Par(a)∨\Impar(a)$ podemos provar
$\Par(3)∨\Impar(3)$ ou $\Par(2k+1)∨\Impar(2k+1)$. Ela é escrita como:
%:
%:  ------------(∀FI)   ------------------(∀F)    
%:  ∀x.P⊢P[x:=t]        t∈B,∀b∈B.P⊢P[b:=t]        
%:                                                     
%:  ^fa-easy-u          ^fa-easy-b                
%:
$$\pu\ded{fa-easy-u} \qquad\text{ou}\qquad \ded{fa-easy-b}$$
%
Lembre que no curso nós quase só usamos quantificadores ``limitados'',
como ``$∀b∈B$'', porque os ``ilimitados'' como ``$∀x$'' são abstratos
demais, no sentido de que é difícil calcular expressões com eles;
aliás só usamos quantificadores ilimitados na aula de 8/outubro.

Em alguns lugares --- por exemplo, no artigo da Wikipedia --- algumas
letras, como $x$, sempre são usadas para {\sl variáveis}, e outras,
como $t$, sempre são usadas para ``termos''.


% «forall-hard» (to ".forall-hard")

\subsection{A regra difícil para o `$∀$'}

A regra difícil para o `$∀$' diz que se conseguimos provar $Q(x,y)$
num contexto que não impõe nenhuma restrição para o $y$ então podemos
provar $∀y.Q(x,y)$ a partir disto; a versão limitada dela diz que se
conseguimos provar $Q(x,y)$ num contexto em que a única restrição para
o $y$ seja $y∈B$ então podemos provar $∀y∈B.Q(x,y)$. Escrevendo estas
regras no estilo de LK elas viram:
%:
%:  P(x)⊢Q(x,y)              P(x)⊢Q(x,y)
%:  --------------(∀DI)   --------------------(∀D)    
%:  P(x)⊢∀y.Q(x,y)        P(x),y∈B⊢∀y∈B.Q(x,y)
%:                                                     
%:  ^fa-hard-u            ^fa-hard-b                
%:
$$\pu\ded{fa-hard-u} \qquad\text{ou}\qquad \ded{fa-hard-b}$$

Na wikipedia essa regra é exposta de um jeito bem mais abstrato:
%
$$\ded{faR}$$
%
onde ``a variável $y$ não aparece livre em $Γ$ ou $Δ$''.

Um exemplo de uso dela parecido com as coisas que estávamos provando
até a P1 é:
%:
%:  a∈\Z⊢\Par(a)→\Impar(a+1)
%:  --------------------------(∀D)
%:  ⊢∀a∈\Z.\Par(a)→\Impar(a+1)
%:                                                     
%:  ^fa-ex
%:
$$\pu\ded{fa-ex}$$


% «exist-easy» (to ".exist-easy")

\subsection{A regra fácil para o `$∃$'}

A regra fácil para o `$∃$' diz que se conseguimos provar $P(x,t)$ para
algum ``termo'' $t$, por exemplo $t:=3$, ou $t:=x^2$, então a partir
disto conseguimos provar que $∃y.P(x,y)$. Esta é a versão {\sl
  ilimitada} da regra; a versão limitada é $(t∈B∧P(x,t))→∃y∈B.P(x,y)$.
No estilo do LK, temos:
%:
%:  ------------(∃FI)   ------------------(∃F)  
%:  P[y:=t]⊢∃y.P        t∈B,P[y:=t]⊢∃y∈B.P       
%:
%:  ^ex-easy-u          ^ex-easy-b
%:
%:
\pu
$$\ded{ex-easy-u} \qquad\text{ou}\qquad \ded{ex-easy-b}$$

Um exemplo de uso:
%:
%:                =====    ------------------------------------(∃F)
%:                ⊢5∈\Z    5∈\Z,\Impar(x)[x:=5]⊢∃x∈\Z.\Impar(x)
%:                ---------------------------------------------(Cut)
%:  Γ⊢\Impar(5)       \Impar(x)[x:=5]⊢∃x∈\Z.\Impar(x)
%:  -------------------------------------------------
%:             Γ⊢∃x∈\Z.\Impar(x)
%:
%:             ^ex-easy-ex
%:
%:
$$\pu\ded{ex-easy-ex}$$


% «exist-hard» (to ".exist-hard")
\subsection{A regra difícil para o `$∃$'}

A regra difícil para o `$∃$' é uma espécie de ``Cut'' --- mas ela usa
uma conclusão da forma $∃y∈B.P(y)$ para cortar duas hipótese: $y∈B$ e
$P(y)$. No sistema que nós vimos primeiro ela era assim:

\msk

\par 1) Suponha $Γ$
\par 2) (...)
\par 3) Então $∃y∈B.P(y)$
\par 4) Suponha $y∈B, P(y)$
\par 5) (...)
\par 6) Então $Q$ \qquad (Fecha 4)

\msk

% (mdq182 11 "20180827" "Contextos, suponhas abertos, erros comuns, fecha suponha")

Nós discutimos ``suponhas abertos'' e regras que ``fecham suponhas''
na aula de 27/ago/2018.

Em LK essa regra fica assim:
%:
%:  Γ⊢∃y∈B.P(y)   Γ,y∈B,P(y)⊢Q
%:  --------------------------(∃D)
%:             Γ⊢Q
%:
%:             ^ex-D
%:
$$\pu\ded{ex-D}$$

A versão ilimitada dela é:
%:
%:  Γ⊢∃y.P   Γ,P⊢Q
%:  --------------(∃DI)
%:        Γ⊢Q
%:
%:        ^ex-DI
%:
%:
%:             Γ,P⊢Q
%:           --------(∃L)^*
%:  Γ⊢∃y.P   Γ,∃y.P⊢Q
%:  -----------------(Cut)
%:        Γ⊢Q
%:
%:        ^ex-DIe
%:
$$\pu
  \ded{ex-DI}
  \qquad := \qquad
  \ded{ex-DIe}
$$




\newpage

%  ____                          _                
% |  _ \ ___  ___ _   _ _ __ ___(_)_   ____ _ ___ 
% | |_) / _ \/ __| | | | '__/ __| \ \ / / _` / __|
% |  _ <  __/ (__| |_| | |  \__ \ |\ V / (_| \__ \
% |_| \_\___|\___|\__,_|_|  |___/_| \_/ \__,_|___/
%                                                 
% «defs-recursivas» (to ".defs-recursivas")

\section{Definições recursivas}

Os livros de matemática e computação ``pra adultos'' às vezes fazem
umas definições ridiculamente curtas para sequências, funções e
conjuntos e aí supõem que o leitor vai entender essas definições. O
livro da Judith Gersting explica definições recursivas a partir da
p.67; vamos ver alguns exemplos extras mais difíceis e alguns truques
para entender estas definições.

\subsection{Fake binary}

Seja $B:\N→\N$ a função que obedece estas duas condições:

(BP) $∀n∈\N. B(2n)=10·B(n)$

(BI) $∀n∈\N. B(2n+1)=B(2n)+1$

Note que fazendo $n=0$ em (BP) obtemos que $B(0)=0$, e com $n=0$ em
(BI) obtemos $B(1)=1$. Usando $n=1$, $n-2$, etc em (BP) e (BI) obtemos
$B(2)$, $B(3)$, etc. Exercícios: 1) entenda o padrão da função $B$; 2)
descubra o valor de $B(34)$; mostre os passos necessários para
calcular $B(34)$.


\subsection{Módulo}

Seja $\N^+=\setofst{n∈\N}{0<n}$, e seja $M:\Z×\N^+→\N$ a função que
obedece estas duas condições:

(MB) Se $0≤a<b$ então $M(a,b)=a$,

(MM) $M(a+b,b)=M(a,b)$.

Repare que agora não estamos usando `$∀$' e nem dizendo em que
conjuntos os valores de $a$ e $b$ moram --- estamos copiando o que
muitos livros de matemática e computação fazem: estamos deixando tudo
implícito! Tanto em (MB) quanto em (MM) fica implícito que $a∈\Z$ e
$b∈\N^+$.

Exercícios: 1) Use (MB) para calcular $M(0,5), M(1,5), \dots, M(4,5)$;
2) Use (MM) para calcular $M(5,5), M(6,5), \dots$; 3) Use (MM) para
calcular $M(-1,5), M(-2,5), \dots$.

\subsection{Noves}

Seja $D:\N→\N$ a função que obedece estas três condições:

(DZ) $D(0)=0$

(DP) Se $D(n)=n$ então $D(n+1)=10D(n)+9$

(DC) Se $D(n)≠n$ então $D(n+1)=D(n)$

Exercícios: 1) Calcule $D(0), D(1), \dots, D(11)$. 2) Entenda o padrão
e descubra os valores de $D(99), D(100), D(101), \ldots, D(999),
D(1000), D(1001)$.

\subsection{Concatenação de números}

Seja $C:\N×\N→\N$ a função que obedece:

(CD) $C(a,b) = a·(D(b)+1)+b$

Exercícios: 1) Calcule $C(12,345)$; 2) Calcule $C(12,0)$; 3) Calcule
$C(0,12)$.

\subsection{Um conjunto de números}

Seja $S⊆\N$ o conjuntos que obedece:

(S0) $0∈S$,

(S2) Se $n∈S$ então $10n+2∈S$,

(S3) Se $n∈S$ então $10n+3∈S$.

Exercícios: 1) Prove que $23322∈S$; 2) Explique porque não dá pra
provar que $45∈S$.

\subsection{Strings}

\def\str#1{\ensuremath{\text{``{\tt#1}''}}}
\def\Ss#1#2{\mathsf{#1}_\mathsf{#2}}
\def\ED{\Ss ED}
\def\EN{\Ss EN}
\def\EB{\Ss EB}
\def\EM{\Ss EM}
\def\ES{\Ss ES}

O ``Exemplo 23'' na página 70 do livro da Judith define {\sl strings},
que às vezes são chamados de {\sl sequências de caracteres} ou de {\sl
  cadeias de caracteres} --- ou só {\sl cadeias} --- em português.
Alguns exemplos de strings: \str{Hello}, \str{1+2}, \str{}, \str{)+}.
Vamos usar `..' (como em Lua) para a operação de concatenação de
strings. Exemplos:

$\str{Hello}..\str{1+2} = \str{Hello1+2}$

\str{}..\str{)+} $=$ \str{)+}


\subsection{Um conjunto de expressões}

Digamos que os conjuntos de strings $\ED$, $\EN$ e $\ES$
obedecem:

(ED) $\str0, \str1, \ldots, \str9 ∈ \ED$

(EN1) Se $d∈\ED$ então $d∈\EN$

(EN2) Se $n∈\EN$ e $d∈\ED$ então $n..d∈\EN$

(ES1) Se $n∈\EN$ então $n∈\ES$

(ES2) Se $s,t∈\ES$ então $s..\str+..t∈\ES$

(ESP) Se $s∈\ES$ então $\str(..s..\str)∈\EN$

Exercícios: 1) Prove que $\str{123}∈\EN$; 2) Prove que $\str{123}∈\ES$
e $\str{123+4+56}∈\ES$; 3) Prove que $\str{(123+4+56)}∈\EN$; 4) Prove
que $\str{(123+4+56)}∈\ES$; 5) Prove que $\str{(123+4+56)+78}∈\ES$.


\subsection{Outro conjunto de expressões}

Vamos {\sl reusar} os símbolos $\ED$, $\EN$ e $\ES$ do item anterior
--- com outro significado.

Digamos que os conjuntos de strings $\ED$, $\EN$, $\EB$, $\EM$ e $\ES$
obedecem:

(ED) $\str0, \str1, \ldots, \str9 ∈ \ED$

(EN1) $d∈\EN$

(EN2) $n..d∈\EN$

(EB1) $n∈\EB$

(EM1) $b∈\EM$

(EM2) $m..\str*..b∈\EM$

(ES1) $m∈\ES$

(ES2) $s..\str+..m∈\ES$

(EBP) $\str(..s..\str)∈\EB$

Agora estamos usando uma convenção no nome das variáveis para deixar a
especificação mais curta. A convenção é:

$d,d',d''∈\ED$

$n,n',n''∈\EN$

$b,b',b''∈\EB$

$m,m',m''∈\EM$

$s,s',s''∈\ES$

\noindent e os `$∀$'s ficam implícitos. Por exemplo, (EM2) por extenso
é:

$∀m∈\EM.∀b∈\EM.m..\str*..b∈\EM$.

Exercícios: 1) prove que $\str{123+4*56+78}∈\ES$; 2) prove que
$\str{(123+4)*56}∈\EM$.

\newpage

\subsection{Valores de expressões}

É fácil ver que os conjuntos $\ED$, $\EN$, $\EB$, $\EM$ e $\ES$ do
item anterior obedecem $\ED⊂\EN⊂\EB⊂\EM⊂\ES$. Vamos definir uma função
$V:\ES→\N$ da seguinte forma:

(VD) $V(\str0)=0, V(\str1)=1, \ldots, V(\str9)=9$

(VN2) $V(n..d)=10V(n)+V(d)$

(VM2) $V(m..\str*..b)=V(m)·V(b)$

(VS2) $V(s..\str+..m)=V(s)·V(m)$

(VP) $V(\str(..s..\str))=V(s)$





% (find-books "__discrete/__discrete.el" "gersting")
% (find-gerstingpage (+ 20  67)   "Definições recursivas")
% (find-gerstingpage (+ 20  69)   "Conjuntos recursivos")





\end{document}

% Local Variables:
% coding: utf-8-unix
% End:
