Warning: this is an htmlized version!
The original is across this link,
and the conversion rules are here.
Lua 5.1.5  Copyright (C) 1994-2012 Lua.org, PUC-Rio
> dofile "underbrace.lua"
> --
> -- (find-istfile "1.org" "Some non-tautologies: DeMorgan")
> --
> -- !(P  & Q)->(! P v  ! Q)
> --   10  01      10    01
> --     00      02    20
> -- 32              22
> --          22
> --
> = ubs "P Q \\& bin () 2 + bin"
._______________.__.
|               |  |
.__._________.  +  2
|  |         |
(  .__.___.  )
   |  |   |
   P  \&  Q

(P \&
 Q) +
 2
> = ubs [[
>>   P 10 u   Q 01 u   \& bin 00 u    () \neg pre 32 u
>>   P 10 u   \neg pre 02 u   Q 01 u \neg pre 20 u   \lor bin 22 u ()
>>   \to bin 22 u
>> ]]
22
|
._______________________.____.
|                       |    |
32                      \to  .__._________________________.
|                            |  |                         |
._____.                      (  22                        )
|     |                         |
\neg  .__.___________.          ._________._____.
      |  |           |          |         |     |
      (  00          )          02        \lor  20
         |                      |               |
         .___.___.              ._____.         ._____.
         |   |   |              |     |         |     |
         10  \&  01             \neg  10        \neg  01
         |       |                    |               |
         P       Q                    P               Q

\underbrace{
\underbrace{
\neg (\underbrace{
\underbrace{
P
}_{10} \&
 \underbrace{
Q
}_{01}
}_{00})
}_{32} \to
 (\underbrace{
\underbrace{
\neg \underbrace{
P
}_{10}
}_{02} \lor
 \underbrace{
\neg \underbrace{
Q
}_{01}
}_{20}
}_{22})
}_{22}
> 
> PP(ubs("a () ()"))
.__.________.
|  |        |
(  .__.__.  )
   |  |  |
   (  a  )

 "((a))"
> = synttorect(ubs("a () ()"))
.__.________.
|  |        |
(  .__.__.  )
   |  |  |
   (  a  )

((a))
> = synttorect(ubs([[ P 10 u ]]))
10
|
P

\underbrace{
P
}_{10}
> = synttorect(ubs([[ P 10 u Q 01 u \& bin ]]))
.___.___.
|   |   |
10  \&  01
|       |
P       Q

\underbrace{
P
}_{10} \&
 \underbrace{
Q
}_{01}
> = synttorect(ubs([[ P 10 u Q 01 u \& bin 00 u    () \neg pre 32 u ]]))
32
|
._____.
|     |
\neg  .__.___________.
      |  |           |
      (  00          )
         |
         .___.___.
         |   |   |
         10  \&  01
         |       |
         P       Q

\underbrace{
\neg (\underbrace{
\underbrace{
P
}_{10} \&
 \underbrace{
Q
}_{01}
}_{00})
}_{32}
> = ubs [[ P 10 u Q 01 u \& bin 00 u    () \neg pre 32 u ]]
32
|
._____.
|     |
\neg  .__.___________.
      |  |           |
      (  00          )
         |
         .___.___.
         |   |   |
         10  \&  01
         |       |
         P       Q

\underbrace{
\neg (\underbrace{
\underbrace{
P
}_{10} \&
 \underbrace{
Q
}_{01}
}_{00})
}_{32}
> 
> = ubstree [[ P 0 u Q 1 u \& bin 0 u ]] 
0
|
.__.___.
|  |   |
0  \&  1
|      |
P      Q
> = ubstree  [[ P 0 u   Q 1 u   \& bin 0 u   P 0 u   -> bin 1 u ]] 
1
|
._________.___.
|         |   |
0         ->  0
|             |
.__.___.      P
|  |   |
0  \&  1
|      |
P      Q
> = ubs      [[ P 0 u   Q 1 u   \& bin 0 u   P 0 u   -> bin 1 u ]] 
1
|
._________.___.
|         |   |
0         ->  0
|             |
.__.___.      P
|  |   |
0  \&  1
|      |
P      Q

\underbrace{
\underbrace{
\underbrace{
P
}_{0} \&
 \underbrace{
Q
}_{1}
}_{0} ->
 \underbrace{
P
}_{0}
}_{1}
> 
>