% (find-angg "LATEX/2017bell.tex")
% (defun c () (interactive) (find-LATEXsh "lualatex -record 2017bell.tex"))
% (defun d () (interactive) (find-xpdfpage "~/LATEX/2017bell.pdf"))
% (defun e () (interactive) (find-LATEX "2017bell.tex"))
% (defun u () (interactive) (find-latex-upload-links "2017bell"))
% (find-xpdfpage "~/LATEX/2017bell.pdf")
% (find-sh0 "cp -v  ~/LATEX/2017bell.pdf /tmp/")
% (find-sh0 "cp -v  ~/LATEX/2017bell.pdf /tmp/pen/")
%   file:///home/edrx/LATEX/2017bell.pdf
%               file:///tmp/2017bell.pdf
%           file:///tmp/pen/2017bell.pdf
% http://angg.twu.net/LATEX/2017bell.pdf
\documentclass[oneside]{book}
\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{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
%
\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")
%
\begin{document}

\catcode`\^^J=10
\directlua{dofile "dednat6load.lua"}  % (find-LATEX "dednat6load.lua")

% (find-books "__cats/__cats.el" "bell")
% (find-belltpage (+ 14 162)    "truth-set")
% (find-belltpage (+ 14 163)    "modality")
% (find-belltpage (+ 14 164)    "universal closure operation")

$(tr_0) \qquad ⊢T⊆Ω$

$(tr_1) \qquad ⊢⊤∈T$

$(tr_2) \qquad α⊢β \qquad α∈T⊢β∈T$

$(tr_3) \qquad (α∈T)∈T⊢α∈T$

\msk

$(tr'_1) \qquad ⊢⊤^*$

$(tr'_2) \qquad α⊢β \qquad α^*⊢β^*$

$(tr'_3) \qquad α^{**}⊢α^*$

$(tr'_4) \qquad α⊢α^*$

\msk

%:
%:   -----------                   -----------                       -----------      
%:   α⊢β=α{∧}β                α^*⊢β=α^*{∧}β                      β⊢α=α{∧}β          
%:   -----------------             -----------------                 -----------------
%:   α⊢β^*=(α{∧}β)^*          α^*⊢β^*=(α^*{∧}β)^*                β⊢α^*=(α{∧}β)^*    
%:   -----------------             -----------------                 -----------------
%:   α⊢β^*{→}(α{∧}β)^*       α^*⊢β^*{→}(α^*{∧}β)^*              β⊢α^*{→}(α{∧}β)^*     
%:   -----------------             -----------------                 -----------------
%:   α,β^*⊢(α{∧}β)^*           α^*,β^*⊢(α^*{∧}β)^*               α^*,β⊢(α{∧}β)^*    
%:   -----------------             -----------------                 -----------------
%:   α{∧}β^*⊢(α{∧}β)^*         α^*{∧}β^*⊢(α^*{∧}β)^*            α^*{∧}β⊢(α{∧}β)^*    
%:   -----------------             -----------------                 -----------------
%:   (α{∧}β^*)^*⊢(α{∧}β)^{**}   (α^*{∧}β^*)^*⊢(α^*{∧}β)^{**}    (α^*{∧}β)^*⊢(α{∧}β)^{**}    
%:   -----------------             -----------------                 -----------------
%:   (α{∧}β^*)^*⊢(α{∧}β)^*      (α^*{∧}β^*)^*⊢(α^*{∧}β)^*      (α^*{∧}β)^*⊢(α{∧}β)^*    
%:                                                                          
%:   ^foo1                              ^foo2                         ^foo3            
%:
%:
%:                                                            ---------         ---------
%:                                                            α{∧}β⊢α         α{∧}β⊢β
%:   ========================    ========================     ---------------   ----------
%:   α^*{∧}β^*⊢(α^*{∧}β)^*    (α^*{∧}β)^*⊢(α{∧}β)^*          (α{∧}β)^*⊢α^*   (α{∧}β)^*⊢β^*
%:   ----------------------------------------------------       --------------------------------
%:   α^*{∧}β^*⊢(α{∧}β)^*                                         (α{∧}β)^*⊢α^*{∧}β^*
%:   ------------------------------------------------------------------------------------
%:                     ⊢α^*{∧}β^*=(α{∧}β)^*
%:
%:                      ^foo4  
%:   
%:                               =======================
%:                               ⊢α^*{∧}β^*=(α{∧}β)^*
%:                               -----------------------------
%:                               ⊢(α^*{∧}β^*)^*=(α{∧}β)^{**}
%:                               -----------------------------
%:                               ⊢(α^*{∧}β^*)^*=(α{∧}β)^*
%:   =======================     -----------------------------
%:   ⊢α^*{∧}β^*=(α{∧}β)^*        ⊢(α{∧}β)^*=(α^*{∧}β^*)^*
%:   -------------------------------------------------------
%:          ⊢α^*{∧}β^*=(α{∧}β)^*=(α^*{∧}β^*)^*
%:
%:            ^foo5
%:
%:                           ------------
%:                           α,α{→}β⊢β
%:                           ------------
%:                           α∧(α{→}β)⊢β
%:                           --------------------
%:                           (α∧(α{→}β))^*⊢β^*
%:                           --------------------
%:                           α^*∧(α{→}β)^*⊢β^*
%:                           --------------------
%:                           α^*,(α{→}β)^*⊢β^*
%:   ------------------      --------------------
%:   α{→}β⊢(α{→}β)^*         (α{→}β)^*⊢α^*{→}β^*
%:   ----------------------------------------------
%:       α{→}β⊢(α{→}β)^*⊢α^*{→}β^*
%:
%:         ^bar1
%:
%:
%:   -------------------   ----
%:   α{→}β⊢(α{→}β)=⊤       ⊤∈T
%:   --------------------------
%:      α{→}β⊢(α{→}β)∈T           α{→}β⊢(α{→}β)^*
%:
%:
%:   -------  ----
%:   α⊢α=⊤  ⊤∈T
%:   -------------
%:      α⊢α∈T
%:      -------
%:      α⊢α^*
%:
%:      ^tr4
%:
$$\pu
  \begin{array}{c}
  \ded{foo1} \qquad \ded{foo2} \qquad \ded{foo3} \\ \\
  \ded{foo4} \\ \\
  (i'): \quad \ded{foo5} \\ \\
  (0'): \quad \ded{tr4} \qquad
  (ii',iii'): \quad \ded{bar1} \\ \\
  \end{array}
$$



\newpage

\def\dt#1#2{\sm{#1\\#2}}
\def\DT#1#2{\mat{#1\\↓\\#2}}
\def\PDT#1#2{\pmat{#1\\↓\\#2}}
\def\mt#1#2#3#4{\dt#1#2{↦}\dt#3#4}

$Ω=\PDT{\{\dt00,\dt01,\dt11\}}{\{\dt·0,\dt·1\}}$

$\{⊤\}=\PDT{\{\dt11\}}{\{\dt·1\}}$

\msk

$012$:
\quad
$μ=\PDT{\cmat{\mt0011,\, \mt0111,\, \mt1111}}{\cmat{\mt·0·1,\, \mt·1·1}}$
\quad
$T=Ω=\PDT{\{\dt00,\dt01,\dt11\}}{\{\dt·0,\dt·1\}}$

\msk

$0|12$:
\quad
$μ=\PDT{\cmat{\mt0000,\, \mt0111,\, \mt1111}}{\cmat{\mt·0·0,\, \mt·1·1}}$
\quad
$T=\PDT{\{\dt01,\dt11\}}{\{\dt·1\}}$

\msk

$01|2$:
\quad
$μ=\PDT{\cmat{\mt0001,\, \mt0101,\, \mt1111}}{\cmat{\mt·0·1,\, \mt·1·1}}$
\quad
$T=\PDT{\{\dt11\}}{\{\dt·0,\dt·1\}}$

\msk

$0|1|2$:
\quad
$μ=\PDT{\cmat{\mt0000,\, \mt0101,\, \mt1111}}{\cmat{\mt·0·0,\, \mt·1·1}}$
\quad
$T=\{⊤\}=\PDT{\{\dt11\}}{\{\dt·1\}}$



\end{document}

% Local Variables:
% coding: utf-8-unix
% ee-anchor-format: "«%s»"
% End: