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

>
>