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"
> -- (P <= Q & R) <-> (P <= Q) & (P <= R)
> --       21 12           21         12
> --       \---/       \----/     \----/
> --         ?          \ra        \rb
> -- \---------/      \-----------------/
> --    \rd                   \rc
> --
> ubs_brute_force_and
>> = ubs [[
>>   P   Q 21 u   R 12 u  \& bin ? u   \le bin \rd u ()
>>   P   Q 21 u   \le bin \ra u ()
>>   P   R 21 u   \le bin \rb u ()
>>   \& bin \rc u
>>   \bij bin
>> ]]
._________________________._____.
|                         |     |
.__.___________________.  \bij  \rc
|  |                   |        |
(  \rd                 )        ._________________.___.
   |                            |                 |   |
   .__.____.                    .__.___________.  \&  .__.___________.
   |  |    |                    |  |           |      |  |           |
   P  \le  ?                    (  \ra         )      (  \rb         )
           |                       |                     |
           .___.___.               .__.____.             .__.____.
           |   |   |               |  |    |             |  |    |
           21  \&  12              P  \le  21            P  \le  21
           |       |                       |                     |
           Q       R                       Q                     R

> = ubs_brute_force_and
(\underbrace{
P \le
 \underbrace{
\underbrace{
Q
}_{21} \&
 \underbrace{
R
}_{12}
}_{?}
}_{\rd}) \bij
 \underbrace{
(\underbrace{
P \le
 \underbrace{
Q
}_{21}
}_{\ra}) \&
 (\underbrace{
P \le
 \underbrace{
R
}_{21}
}_{\rb})
}_{\rc}
> 
> ubs_brute_force_imp
>> = ubs [[
>>   P   Q 21 u   R 12 u   \to bin ? u    \le bin \Rc u ()
>>   P   Q 21 u   \land bin \Ra u   R 12 u   \le bin \Rb u ()
>>   \bij bin
>> ]]
.__________________________._____.
|                          |     |
.__.____________________.  \bij  .__.______________________.
|  |                    |        |  |                      |
(  \Rc                  )        (  \Rb                    )
   |                                |
   .__.____.                        ._____________.____.
   |  |    |                        |             |    |
   P  \le  ?                        \Ra           \le  12
           |                        |                  |
           .___.____.               .__.______.        R
           |   |    |               |  |      |
           21  \to  12              P  \land  21
           |        |                         |
           Q        R                         Q

> 
>