Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
% (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{dednat6dir = "dednat6/"}
\directlua{dofile(dednat6dir.."dednat6.lua")}
\directlua{texfile(tex.jobname)}
\directlua{verbose()}
\directlua{output(preamble1)}
\def\expr#1{\directlua{output(tostring(#1))}}
\def\eval#1{\directlua{#1}}
\def\pu{\directlua{pu()}}

\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

% (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: