|
Warning: this is an htmlized version!
The original is here, and the conversion rules are here. |
% (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 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= \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: