% (find-angg "LATEX/2010-semanact.tex")
% (find-dn4ex "edrx08.sty")
% (find-angg ".emacs.templates" "s2008a")
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2010-semanact.tex && latex    2010-semanact.tex"))
% (defun c () (interactive) (find-zsh "cd ~/LATEX/ && ~/dednat4/dednat41 2010-semanact.tex && pdflatex 2010-semanact.tex"))
% (eev "cd ~/LATEX/ && Scp 2010-semanact.{dvi,pdf} edrx@angg.twu.net:slow_html/LATEX/")
% (defun d () (interactive) (find-dvipage "~/LATEX/2010-semanact.dvi"))
% (find-dvipage "~/LATEX/2010-semanact.dvi")
% (find-pspage  "~/LATEX/2010-semanact.ps")
% (find-pspage  "~/LATEX/2010-semanact.pdf")
% (find-xpdfpage "~/LATEX/2010-semanact.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvipdf         2010-semanact.dvi 2010-semanact.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o 2010-semanact.ps 2010-semanact.dvi")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 600 -P pk -o 2010-semanact.ps 2010-semanact.dvi && ps2pdf 2010-semanact.ps 2010-semanact.pdf")
% (find-zsh0 "cd ~/LATEX/ && dvips -D 300 -o tmp.ps tmp.dvi")
% (find-pspage  "~/LATEX/tmp.ps")
% (ee-cp "~/LATEX/2010-semanact.pdf" (ee-twupfile "LATEX/2010-semanact.pdf") 'over)
% (ee-cp "~/LATEX/2010-semanact.pdf" (ee-twusfile "LATEX/2010-semanact.pdf") 'over)
% (find-twusfile     "LATEX/" "2010-semanact")
% http://angg.twu.net/LATEX/2010-semanact.pdf

\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 2010-semanact.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")


% {\color{red}
% (Eduardo Ochs)
% }
% 
% \bsk
% \bsk
% \bsk
 
{\bf Raciocínio diagramático}

\msk
\par O modo como a gente pensa (em Matemática)
\par não é o modo como a gente escreve...
\msk
\par A gente tem que escrever demonstrações de um modo
\par que convença qualquer um de que os nossos argumentos
\par não têm furos.

\newpage

{\bf Minha trajetória:}
\msk
\par Cálculo
\par $\to$ Análise: argumentos com $$s e $$s
\par $\to$ Topologia
\par $\to$ Análise Não-Standard
\par $\to$ Lógica
\par $\to$ Categorias
\par $\to$ Semântica Categórica
\par $\to$ Teoria de Toposes
\par $\to$ Teoria de Tipos / $ð$-cálculo
\par $\to$ Lógica Intuicionista
\par $\to$ Lógica Modal
\par $\to$ Feixes
\par $\to$ ...

\bsk (Complicando cada vez mais...)

\newpage

\par A ``literatura'' (livros, artigos) sobre estes
\par assuntos é escrita de um modo bem técnico,
\par muito complicado...
\msk
\par Apesar de eu ter estudado estas coisas durante anos
\par tem poucos pedaços desses artigos e livros que 
\par entendo {\sl realmente} bem --- a notação costuma
\par ser tão difícil que eu ainda levo horas em cada
\par parágrafo.
\bsk
\par {\color{red} Como tornar a literatura mais acessível?}
\bsk
\par Solução: formalizar o modo como a gente pensa ---
\par criar uma tradução (precisa o suficiente) entre
\par meus diagramas (2D) e a linguagem usual dos artigos
\par (algébrica, linear).

\newpage

{\bf Projeções e levantamentos}

\def\twoninenyninelemma#1#2{
  \fbox{
  $\begin{array}{rcl}
   2^{#2}-2^{#1} &=& 2^{1+#1}-2^{#1} \\
%                &=& 2^{1}·2^{#1}-2^{#1} \\
                 &=& 2·2^{#1}-1·2^{#1} \\
                 &=& (2-1)·2^{#1} \\
%                &=& 1·2^{#1} \\
                 &=& 2^{#1} \\
   \end{array}
  $}
}

%:&&

%D diagram 2^100-2^99
%D 2Dx     100
%D 2D  100 proof-n
%D 2D
%D 2D  +50 proof-99
%D 2D
%D 2D  +40 statement-99
%D 2D
%D ((
%D    proof-n      .tex= \twoninenyninelemma{n}{n+1}
%D    proof-99     .tex= \twoninenyninelemma{99}{100}
%D    statement-99 .tex= \fbox{$\begin{array}{rcl}2^{100}-2^{99}&=&2^{99}\end{array}$}
%D    @ 0 @ 1 ->
%D    @ 1 @ 2 ->
%D ))
%D enddiagram
%D
$$\diag{2^100-2^99}$$

%:&´


\newpage

{\bf Projeções e levantamentos (2)}

% (find-854     "" "standard-erasings")
% (find-854page 13 "standard-erasings")
% (find-854     "" "generalization")
% (find-854page 14 "generalization")

%L forths["<.>"]  = function () pusharrow("<.>") end
%L forths["<-->"] = function () pusharrow("<-->") end
%L forths["|-->"] = function () pusharrow("|-->") end

% This gives us a way to draw all the "standard
% erasings" of a tree from a single tree definition.
% Low-level words:
%
\def\archfull#1#2#3{#1\equiv #2:#3} \def\ARCHFULL    {\let\arch=\archfull}     
\def\archdnc#1#2#3{#1}              \def\ARCHDNC     {\let\arch=\archdnc}      
\def\archtermtype#1#2#3{#2:#3}      \def\ARCHTERMTYPE{\let\arch=\archtermtype}
\def\archterm#1#2#3{#2}             \def\ARCHTERM    {\let\arch=\archterm}     
\def\archtype#1#2#3{#3}             \def\ARCHTYPE    {\let\arch=\archtype}     
\def\rY#1{#1}                       \def\RY          {\let\r=\rY}              
\def\rN#1{}                         \def\RN          {\let\r=\rN}              
\def\ptypeY#1{#1}                   \def\PTYPEY      {\let\ptype=\ptypeY}      
\def\pytpeN#1{}                     \def\PTYPEN      {\let\ptype=\pytpeN}      
%
% High-level words:
%
\def\FULLRP{\ARCHFULL\RY\PTYPEY}
\def\FULLR {\ARCHFULL\RY\PTYPEN}
\def\FULLP {\ARCHFULL\RN\PTYPEY}
\def\FULL  {\ARCHFULL\RN\PTYPEN}
\def\TERMTYPERP{\ARCHTERMTYPE\RY\PTYPEY}
\def\TERMTYPER {\ARCHTERMTYPE\RY\PTYPEN}
\def\TERMTYPEP {\ARCHTERMTYPE\RN\PTYPEY}
\def\TERMTYPE  {\ARCHTERMTYPE\RN\PTYPEN}
\def\TERMRP{\ARCHTERM\RY\PTYPEY}
\def\TERMR {\ARCHTERM\RY\PTYPEN}
\def\TERMP {\ARCHTERM\RN\PTYPEY}
\def\TERM  {\ARCHTERM\RN\PTYPEN}
\def\TYPER {\ARCHTYPE\RY\PTYPEN}
\def\TYPE  {\ARCHTYPE\RN\PTYPEN}
\def\DNCR  {\ARCHDNC\RY\PTYPEN}
\def\DNC   {\ARCHDNC\RN\PTYPEN}

%:
%:  \arch{a,b}{p}{A×B}
%:  ------------------\r{'}
%:      \arch{b}{'p}{B}         \arch{b|->c}{f}{B->C}
%:      -------------------------------------\r{\app}
%:                  \arch{c}{f('p)}{C}
%:
%:                    ^archetypal-deriv
%:
%:
%:  \arch{a,b}{p}{A×B}   \arch{b|->c}{f}{B->C}
%:  ==========================================
%:            \arch{c}{f('p)}{C}
%:
%:            ^archetypal=deriv
%:
%D diagram archderivs2
%D 2Dx        100        +70       +05       +45       +35
%D 2D  100          \foo{\FULLRP}
%D 2D      
%D 2D  +50 \foo{\DNCR}                \foo{\TERMTYPERP}            
%D 2D                        
%D 2D  +50 \foo{\DNC}           \foo{\TERMR}   \foo{\TYPE}        
%D 2D                    
%D 2D  +45 \fooo{\DNC}          \fooo{\TERMR}  \fooo{\TYPE}       
%D 2D
%D (( \foo{\DNCR}   x+= 15
%D    # \foo{\TERMR}  y+= -10
%D    # \fooo{\TERMR} y+= -10
%D
%D    \foo{\FULLRP} \foo{\TERMTYPERP} ->
%D    \foo{\FULLRP} \foo{\DNCR} ->
%D    \foo{\TERMTYPERP} \foo{\TERMR} ->
%D    \foo{\TERMTYPERP} \foo{\TYPE} ->
%D    \foo{\DNCR} \foo{\DNC} ->
%D    \foo{\TYPE} \foo{\DNC} <--> .slide= 30pt
%D    
%D    \foo{\TERMR} \fooo{\TERMR} ->
%D    \foo{\TYPE}  \fooo{\TYPE}  ->
%D    \foo{\DNC}   \fooo{\DNC}  ->
%D    \fooo{\TYPE} \fooo{\DNC} <--> .slide= 25pt
%D ))
%D enddiagram
%D
$$\def\foo#1{#1\fcded{archetypal-deriv}}
  \def\fooo#1{#1\fcded{archetypal=deriv}}
  \diag{archderivs2}
$$
$$\text{Figure 2}$$


\newpage

{\bf Diagramas e construções}

%D diagram Frob-std
%D 2Dx    100          +45 +35 +10     +30
%D 2D 100 B0 ================> B1
%D 2D	  ^                  ^ ^ 
%D 2D	  |                 /  | 
%D 2D	  -                \   - 
%D 2D +20 B2 ========> B3 <--> B3'
%D 2D	  -                /   - 
%D 2D	  |                 \  |
%D 2D	  v                  v v
%D 2D +20 B4 <================ B5
%D 2D
%D 2D +15 b0 |---------------> b1
%D 2D
%D (( B0 .tex= P                            B1  .tex=  Æ_fP
%D    B2 .tex= P&f^*Q  B3 .tex= Æ_f(P&f^*Q) B3' .tex= (Æ_fP)&Q
%D    B4 .tex= f^*Q                         B5  .tex=     Q
%D    b0 .tex= A                            b1  .tex=     B
%D ))
%D ((
%D    B0 B1 |->   B2 B0 -> B3 B1 -> B3' B1 ->
%D    B4 B5 <-|   B2 B4 -> B3 B5 -> B3' B5 ->
%D    B2 B3 |->   B3 B3' -> sl^ .plabel= a \nat  B3 B3' <- sl_ .plabel= b \Frob
%D    B0 B2 midpoint B1 B3 midpoint  harrownodes nil 20 nil |->
%D    B2 B4 midpoint B3 B5 midpoint  harrownodes nil 20 nil |->
%D ))
%D (( b0 b1 -> .plabel= a f
%D ))
%D enddiagram
%
$$\diag{Frob-std}$$

\def\cob{¯{c.o.b.}}
\def\EqE{{=}E}

%:
%:       f   P  Q                        f    P  Q          
%:  =====================\Frobnat        ---------------------\Frob
%:  Æ_f(P´f^*Q)|-(Æ_fP)´Q                Æ_f(P´f^*Q)|-(Æ_fP)´Q                
%:                                                                                      
%:     ^Frobnat-short-std                 ^Frob-std                   
%:

%:
%:           f  Q                f   Q      
%:           ---\cob             -----\cob
%:       P   f^*Q            P    f^*Q
%:       ---------         ------------'
%:       P´f^*Q|-P   f      P´f^*Q|-f^*Q
%:   -----------------Æ_f   --------------{Æ_f}^\flat
%:   Æ_f(P´f^*Q)|-Æ_fP      Æ_f(P´f^*Q)|-Q
%:   -------------------------------------\ang{,}
%:              Æ_f(P´f^*Q)|-(Æ_fP)´Q
%:
%:              ^Frobnat-std
%:
$$\begin{array}{l}
  \ded{Frobnat-short-std} \quad := \\ \\
  \phantom{OO}
  \ded{Frobnat-std} \\
  \end{array}
$$


\bsk

Mas claro que eu não lembro essa coisa toda aí acima

de memória... eu lembro isso aqui:

$$\includegraphics[scale=0.5]{frob-sketch.eps}$$



\newpage

{\bf Diagramas internos}

\def\Setito{\Set^{\ito}}
\def\Setmto{\Set^{\monicto}}
\def\Pred{¦{Pred}}
\def\Pred{Ð{Pred}}
\def\cob{¯{c.o.b.}}
\def\EqE{{=}E}

\def\TB{§\!_{B}}
\def\TAB{§\!_{A×B}}
\def\SDTB{Æ_\DD\!\TB}
\def\pip     {   \pi'}
\def\opip    {\ov\pi'}
\def\pipstar {   \pi^{\prime*}}
\def\opipstar{\ov\pi^{\prime*}}
\def\pistar  {   \pi^{*}}
\def\opistar {\ov\pi^{*}}
\def\opi     {\ov\pi}
\def\EqEdomain{\opipstarÆ_\DD\TB \land \opistar\dd^*Q}
\def\EqEL      {\opipstarÆ_\DD\TB}
\def\EqER      {\opistar\dd^*Q}
\def\EqEdomthin{\EqEL{´}\EqER}
\def\EqEdomwide{\EqEL\land\EqER}



\def\fdiag#1{\fbox{\!\!\!$\diag{#1}$}}
\def\fdiag#1{\fbox{$\diag{#1}$}}
\def\ffdiag#1#2{\begin{tabular}{l}#2\\\fbox{$\diag{#1}$}\end{tabular}}
\def\fdiag#1{\ffdiag{#1}{foo}}

\def\ctabular#1{\begin{tabular}{c}#1\end{tabular}}
\def\ltabular#1{\begin{tabular}{l}#1\end{tabular}}
% \def\fdiagwithboxest#1#2{\ltabular{#2 \\ \fdiagwithboxes{#1}}}
\def\fdiagest#1#2{\ltabular{#2 \\ \fdiag{#1}}}

\def\fdiag#1{\fbox{$\diag{#1}$}}


%D diagram 5-algebraic-internal
%D 2Dx     100     +35
%D 2D  100 P ====> ÆP
%D 2D      -       -
%D 2D      |  <->  |
%D 2D      v       v
%D 2D  +20 Q* <=== Q
%D 2D      -       -
%D 2D      |  <->  |
%D 2D      v       v
%D 2D  +20 R ====> åR
%D 2D      
%D 2D  +15 A |---> B
%D 2D
%D (( P  .tex= P     ÆP  .tex= Æ_fP
%D    Q* .tex= f^*Q   Q  .tex=  Q  
%D    R  .tex= R     åR  .tex= å_fR
%D    A  .tex= A      B  .tex= B
%D ))
%D ((  P  ÆP |->
%D     P   Q* ->  ÆP   Q  ->  P   Q  harrownodes nil 20 nil <->
%D     Q*  Q <-|
%D     Q*  R  ->  Q   åR  ->  Q*  åR harrownodes nil 20 nil <->
%D     R  åR |->
%D     A   B -> .plabel= a f
%D ))
%D enddiagram
%D
% $$\diag{5-algebraic-internal}$$
%
%D diagram 5-set-binary
%D 2Dx     100     +35
%D 2D  100 P ====> ÆP
%D 2D      -       -
%D 2D      |  <->  |
%D 2D      v       v
%D 2D  +20 Q* <=== Q
%D 2D      -       -
%D 2D      |  <->  |
%D 2D      v       v
%D 2D  +20 R ====> åR
%D 2D      
%D 2D  +15 A |---> B
%D 2D
%D (( P  .tex= \sm{00001\\00011}     ÆP  .tex= \sm{00011}
%D    Q* .tex= \sm{00111\\00111}     Q   .tex= \sm{00111}
%D    R  .tex= \sm{01111\\11111}     åR  .tex= \sm{01111}
%D    A  .tex= X×Y    B  .tex= X
%D ))
%D ((  P  ÆP |->
%D     P   Q* ->  ÆP   Q  ->  P   Q  harrownodes nil 20 nil <->
%D     Q*  Q <-|
%D     Q*  R  ->  Q   åR  ->  Q*  åR harrownodes nil 20 nil <->
%D     R  åR |->
%D     A   B -> .plabel= a \pi
%D ))
%D enddiagram
%D
% $$\diag{5-set-binary}$$
%
%D diagram 5-algebraic-external
%D 2Dx     100     +25     +40
%D 2D  100 \bbE \bbE_A  \bbE_B
%D 2D
%D 2D  +35 \bbB    A       B
%D 2D
%D (( \bbE_A \bbE_B
%D    @ 0 @ 1 -> .slide=  13pt .plabel= a Æ_f
%D    @ 0 @ 1 <-               .plabel= m f^*
%D    @ 0 @ 1 -> .slide= -13pt .plabel= b å_f
%D    @ 0 @ 1 midpoint y+= -5 .TeX= \text{\tiny$®$} place
%D    @ 0 @ 1 midpoint y+=  5 .TeX= \text{\tiny$®$} place
%D ))
%D (( \bbE \bbB -> .plabel= l p
%D    A B -> .plabel= a f
%D ))
%D enddiagram
%D
% $$\diag{5-algebraic-external}$$
%
%D diagram 5-set-external
%D 2Dx     100     +25     +40
%D 2D  100 \bbE \bbE_A  \bbE_B
%D 2D
%D 2D  +35 \bbB    A       B
%D 2D
%D (( \bbE_A .tex= \Setito_{X×Y} \bbE_B .tex= \Setito_X
%D    @ 0 @ 1 -> .slide=  13pt .plabel= a Æ_\pi
%D    @ 0 @ 1 <-               .plabel= m \pi^*
%D    @ 0 @ 1 -> .slide= -13pt .plabel= b å_\pi
%D    @ 0 @ 1 midpoint y+= -5 .TeX= \text{\tiny$®$} place
%D    @ 0 @ 1 midpoint y+=  5 .TeX= \text{\tiny$®$} place
%D ))
%D (( \bbE .tex= \Setito \bbB .tex= \Set -> .plabel= l \Cod
%D    A .tex= X×Y B .tex= X -> .plabel= a \pi
%D ))
%D enddiagram
%D
% $$\diag{5-set-external}$$
%
%D diagram adjoints-to-cob
%D 2Dx     100    +95
%D 2D  100 text
%D 2D
%D 2D  +60 EAEB   PQR
%D 2D
%D 2D  +85 EXYEX  binary
%D 2D
%D ((
%D    text   .tex= \fibrationbox BOX place
%D    EAEB   .tex= \fdiag{5-algebraic-external} BOX place
%D    EXYEX  .tex= \fdiag{5-set-external} BOX place
%D    PQR    .tex= \fdiag{5-algebraic-internal}            BOX place
%D    binary .tex= \fdiag{5-set-binary} BOX place
%D    text EAEB  -> .plabel= l (1)
%D    EAEB PQR   -> .plabel= a (2)
%D    EAEB EXYEX -> .plabel= l (3)
%D    PQR binary -> .plabel= r (4)
%D    EXYEX binary -> .plabel= a (5)
%D ))
%D enddiagram
%D
$$\def\fibrationbox{\fbox{\ltabular{
      A fibration $p:\bbE \to \bbB$ \\
      plus for each $f:A \to B$ in $\bbB$ \\
      adjoints $Æ_f \dashv f^* \dashv å_f$ \\
    }}}
\diag{adjoints-to-cob}
$$


\newpage

{\bf Lógicas com mais de dois valores de verdade}

Em algumas lógicas podemos ter $¬¬P \neq P$.

Uma operação de fecho é uma que obedece:

%:**^{**}
%:*^*

%:
%:                 P|-Q         
%:   ----         ------        -------
%:   |-§*         P*|-Q*        P**|-P*
%:
%:   ^ax*-1       ^ax*-2        ^ax*-3
%:
$$\ded{ax*-1} \qquad \ded{ax*-2} \qquad \ded{ax*-3}$$

Por exemplo, $P \mapsto ¬¬P$ é uma operação de fecho.

\msk

Conseqüências:

%D diagram and-cube
%D 2Dx      100 +20    +25  +20	       +40 +20     +25  +20	 
%D 2D  100  P´Q        P´Q*	       P´Q'        P´Q*'	 
%D 2D  +20     (P´Q)*     (P´Q*)*         (P´Q)*'     (P´Q*)*'
%D 2D      			      			 
%D 2D  +20 P*´Q       P*´Q*	      P*´Q'       P*´Q*'	 
%D 2D  +20    (P*´Q)*    (P*´Q*)*        (P*´Q)*'    (P*´Q*)*'
%D 2D
%D ((  P´Q    P*´Q    P´Q*    P*´Q*
%D    (P´Q)* (P*´Q)* (P´Q*)* (P*´Q*)*
%D    @ 0 @ 1  -> @ 0 @ 2  -> @ 1 @ 3  -> @ 2 @ 3  ->
%D    @ 4 @ 5  =  @ 4 @ 6  =  @ 5 @ 7  =  @ 6 @ 7  = 
%D    @ 0 @ 4  -> @ 1 @ 5  -> @ 2 @ 6  -> @ 3 @ 7  = 
%D ))
%D ((  P´Q'    P*´Q'    P´Q*'    P*´Q*'
%D    (P´Q)*' (P*´Q)*' (P´Q*)*' (P*´Q*)*'
%D    @ 0 .tex= \dagVee001 @ 1 .tex= \dagVee101
%D    @ 2 .tex= \dagVee011 @ 3 .tex= \dagVee111
%D    @ 4 .tex= \dagVee111 @ 5 .tex= \dagVee111
%D    @ 6 .tex= \dagVee111 @ 7 .tex= \dagVee111
%D    @ 0 @ 1  -> @ 0 @ 2  -> @ 1 @ 3  -> @ 2 @ 3  ->
%D    @ 4 @ 5  =  @ 4 @ 6  =  @ 5 @ 7  =  @ 6 @ 7  = 
%D    @ 0 @ 4  -> @ 1 @ 5  -> @ 2 @ 6  -> @ 3 @ 7  = 
%D ))
%D enddiagram
%D
$$\diag{and-cube}$$

%D diagram or-cube
%D 2Dx      100 +20    +25  +20	       +40 +20     +25  +20	 
%D 2D  100  PQ        PQ*	       PQ'        PQ*'	 
%D 2D  +20     (PQ)*     (PQ*)*         (PQ)*'     (PQ*)*'
%D 2D      			      			 
%D 2D  +20 P*Q       P*Q*	      P*Q'       P*Q*'	 
%D 2D  +20    (P*Q)*    (P*Q*)*        (P*Q)*'    (P*Q*)*'
%D 2D
%D ((  PQ    P*Q    PQ*    P*Q*
%D    (PQ)* (P*Q)* (PQ*)* (P*Q*)*
%D    @ 0 @ 1  -> @ 0 @ 2  -> @ 1 @ 3  -> @ 2 @ 3  ->
%D    @ 4 @ 5  =  @ 4 @ 6  =  @ 5 @ 7  =  @ 6 @ 7  = 
%D    @ 0 @ 4  -> @ 1 @ 5  -> @ 2 @ 6  -> @ 3 @ 7  ->
%D ))
%D ((  PQ'    P*Q'    PQ*'    P*Q*'
%D    (PQ)*' (P*Q)*' (PQ*)*' (P*Q*)*'
%D    @ 0 .tex= \dagHouse00011 @ 1 .tex= \dagHouse00111
%D    @ 2 .tex= \dagHouse01011 @ 3 .tex= \dagHouse01111
%D    @ 4 .tex= \dagHouse11111 @ 5 .tex= \dagHouse11111
%D    @ 6 .tex= \dagHouse11111 @ 7 .tex= \dagHouse11111
%D    @ 0 @ 1  -> @ 0 @ 2  -> @ 1 @ 3  -> @ 2 @ 3  ->
%D    @ 4 @ 5  =  @ 4 @ 6  =  @ 5 @ 7  =  @ 6 @ 7  = 
%D    @ 0 @ 4  -> @ 1 @ 5  -> @ 2 @ 6  -> @ 3 @ 7  ->
%D ))
%D enddiagram
%D
$$\diag{or-cube}$$

%D diagram imp-cube-Aor
%D 2Dx      100 +20    +25  +20	       +40 +20     +25  +20	 
%D 2D  100  P¶Q        P¶Q*	       P¶Q'        P¶Q*'	 
%D 2D  +20     (P¶Q)*     (P¶Q*)*         (P¶Q)*'     (P¶Q*)*'
%D 2D      			      			 
%D 2D  +20 P*¶Q       P*¶Q*	      P*¶Q'       P*¶Q*'	 
%D 2D  +20    (P*¶Q)*    (P*¶Q*)*        (P*¶Q)*'    (P*¶Q*)*'
%D 2D
%D ((  P¶Q    P*¶Q    P¶Q*    P*¶Q*
%D    (P¶Q)* (P*¶Q)* (P¶Q*)* (P*¶Q*)*
%D    @ 0 @ 1 <-  @ 0 @ 2  -> @ 1 @ 3  -> @ 2 @ 3  =
%D    @ 4 @ 5 <-  @ 4 @ 6  -> @ 5 @ 7  -> @ 6 @ 7  =
%D    @ 0 @ 4  -> @ 1 @ 5  -> @ 2 @ 6  =  @ 3 @ 7  =
%D ))
%D ((  P¶Q'    P*¶Q'    P¶Q*'    P*¶Q*'
%D    (P¶Q)*' (P*¶Q)*' (P¶Q*)*' (P*¶Q*)*'
%D    @ 0 .tex= \dagSqr0101 @ 1 .tex= \dagSqr0000
%D    @ 2 .tex= \dagSqr1111 @ 3 .tex= \dagSqr1111
%D    @ 4 .tex= \dagSqr0111 @ 5 .tex= \dagSqr0011
%D    @ 6 .tex= \dagSqr1111 @ 7 .tex= \dagSqr1111
%D    @ 0 @ 1 <-  @ 0 @ 2  -> @ 1 @ 3  -> @ 2 @ 3  =
%D    @ 4 @ 5 <-  @ 4 @ 6  -> @ 5 @ 7  -> @ 6 @ 7  =
%D    @ 0 @ 4  -> @ 1 @ 5  -> @ 2 @ 6  =  @ 3 @ 7  =
%D ))
%D enddiagram
%D
$$\diag{imp-cube-Aor}$$






%




\end{document}

% Local Variables:
% coding:           raw-text-unix
% ee-anchor-format: "«%s»"
% End:
