Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
% A test file for the module "underbrace2d.lua" of dednat6.
% This file: http://angg.twu.net/dednat6/demo-underbrace.tex.html
%            http://angg.twu.net/dednat6/demo-underbrace.tex
%                         (find-dednat6 "demo-underbrace.tex")
%    Output: http://angg.twu.net/dednat6/demo-underbrace.pdf
%
% (defun c () (interactive) (find-dednat6sh "lualatex -record demo-underbrace.tex"))
% (defun d () (interactive) (find-pdf-page "~/dednat6/demo-underbrace.pdf"))
% (defun e () (interactive) (find-dednat6 "demo-underbrace.tex"))
% (defun u () (interactive) (find-latex-upload-links "demo-underbrace"))
%   (find-pdf-page "~/dednat6/demo-underbrace.pdf")
% http://angg.twu.net/dednat6/demo-underbrace.pdf
%
% (find-LATEXgrep "grep --color -nH --null -e '%R' 2017planar-has-1.tex")
%
\documentclass[oneside]{article}
%
% Not needed:
%   \usepackage{proof}   % For derivation trees ("%:" lines)
%   \input diagxy        % For 2D diagrams ("%D" lines)
%   \xyoption{curve}     % For the ".curve=" feature in 2D diagrams
%
\usepackage{amsfonts}
\catcode`Â=13 \defÂ{\neg}
\catcode`â=13 \defâ{\land}
\catcode`â=13 \defâ{\lor}
\catcode`â=13 \defâ{\to}
\catcode`â»=13 \defâ»{\Box}
\catcode`â=13 \defâ{\Box}
%
\def\ttchar#1{\setbox0=\hbox{\texttt{a}}\leavevmode\hbox to \wd0{\hss#1\hss}}
\def\basicttchars{
  \defÂ{\ttchar{$\neg$}}
  \defâ{\ttchar{$\to$}}
  \defâ{\ttchar{$\land$}}
  \defâ{\ttchar{$\lor$}}
  \defâ»{\ttchar{$\Box$}}
}
%
\begin{document}
  \catcode`\^^J=10                      % (find-es "luatex" "spurious-omega")
  \directlua{dofile "dednat6load.lua"}  % (find-dednat6 "dednat6load.lua")


\title{Dednat6: a demo for underbrace2d.lua}
\author{Eduardo Ochs}
\maketitle


% From: (find-LATEX "2017planar-has-defs.tex" "defub")
%
\def\defub#1#2{\expandafter\def\csname ub-#1\endcsname{#2}}
\def\ifubundefined#1{\expandafter\ifx\csname ub-#1\endcsname\relax}
\def\ub#1{\ifubundefined{#1}
    \errmessage{UNDEFINED UB: #1}
  \else
    \csname ub-#1\endcsname
  \fi
}
\def\und#1#2{\underbrace{#1}_{#2}}


Output:

% From: (find-LATEX "2017planar-has-1.tex" "prop-calc-ZHA")
%       (find-LATEX "2017planar-has-1.tex" "prop-calc-ZHA" "defub")
%
%UB (Â Â P) â P
%UB     --   --
%UB     10   10
%UB    ---
%UB    02
%UB  -----
%UB   20
%UB ----------- 
%UB       12
%L
%L defub "notnotP"
%
%UB Â(P â Q) â (Â P â Â Q)
%UB   -- --      --    --
%UB   10 01      10    01
%UB   -----     ---   ---
%UB     00      02    20
%UB -------     ---------
%UB    32          22
%UB ----------------------
%UB          22
%L
%L defub "demorgan"
%
$$\pu
  \ub{notnotP}
  \qquad
  \ub{demorgan}
$$

%UB    Â( P â  Q) â (Â  P â Â  Q)
%UB      --   --       --     --
%UB      â»P   â»Q       â»P     â»Q
%UB      -------     ----   ----
%UB      â»P â â»Q     â»Ââ»P   â»Ââ»Q
%UB    ----------   ------------
%UB    â»Â(â»Pââ»Q)     â»Ââ»P â â»Ââ»Q
%UB   ---------------------------
%UB   â»((â»Â(â»Pââ»Q))â(â»Ââ»Pââ»Ââ»Q))
%L
%L defub "T-demorgan"
%
$$\pu
  T(\ub{T-demorgan})
$$

\bigskip

Source (for the upper right diagram):

{
\basicttchars
\begin{verbatim}
   %UB Â(P â Q) â (Â P â Â Q)
   %UB   -- --      --    --
   %UB   10 01      10    01
   %UB   -----     ---   ---
   %UB     00      02    20
   %UB -------     ---------
   %UB    32          22
   %UB ----------------------
   %UB          22
   %L
   %L defub "demorgan"
   %
   $$\pu
     \ub{demorgan}
   $$
\end{verbatim}
}


\end{document}

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