```  .
__|___
|    |
a  __|___
|    |
S  __|__
|   |
d  _|__
|  |
S  e
```
First we QR the lower shift operator, replacing it with a variable and abstracting over that variable.
```   .
___|___
|     |
S  ___|___
|     |
\x  __|___
|    |
a  __|___
|    |
S  __|__
|   |
d  _|__
|  |
x  e
```
Next, we QR the upper shift operator
```   .
___|___
|     |
S  ___|____
|      |
\y  ___|___
|     |
S  ___|___
|     |
\x  __|___
|    |
a  __|___
|    |
y  __|__
|   |
d  _|__
|  |
x  e
```
We then evaluate, using the same value for the shift operator proposed before: S = shift = \k.k(k "") It will be easiest to begin evaluating this tree with the lower shift operator (we get the same result if we start with the upper one). The relevant value for k is (\x.a(y(d(x e)))). Then k "" is a(y(d(""(e)))), and k(k "") is a(y(d((a(y(d(""(e)))))(e)))). In tree form:
```   .
___|___
|     |
S  ___|____
|      |
\y  ___|___
|     |
a  ___|___
|     |
y  ___|___
|     |
d  ___|___
|     |
__|___  e
|    |
a  __|___
|    |
y  __|___
|    |
d  __|__
|   |
""  e
```
Repeating the process for the upper shift operator replaces each occurrence of y with a copy of the whole tree.
```      .
|
______|______
|           |
a  _________|__________
|                  |
|               ___|___
___|___            |     |
|     |            d  ___|____
a  ___|____           |      |
|      |        ___|____  e
""  ___|___     |      |
|     |     a  ____|_____
d  ___|___     |        |
|     |     |      __|___
___|___  e  ___|___   |    |
|     |     |     |   d  __|__
a  ___|___  a  ___|____  |   |
|     |     |      |  ""  e
""  __|___  ""  ___|___
|    |      |     |
d  __|__    d  ___|___
|   |       |     |
""  e    ___|___  e
|     |
a  ___|___
|     |
""  __|___
|    |
d  __|__
|   |
""  e
```
```    _______________               _______________            _______________
| [x->2, y->3] |	          | [x->2, y->3] |          | [x->2, y->3] |
------------------- 	         ------------------        ------------------
|              |     ¢        |              |    =     |              |
|    +2        |	          |     y        |          |     5        |
|______________|	          |______________|          |______________|
```
For people who are familiar with Discourse Representation Theory (Kamp 1981, Kamp and Reyle 1993), this separation of boxes into payload and discourse scorekeeping will be familiar (although many details differ). The general pattern is that monadic treatments separate computation into an at-issue (pre-monadic) computation with a layer at which side-effects occur. The tower notation is a precise way of articulating continuation-based computations into a payload and (potentially multiple) layers of side-effects. Visually, we won't keep the outer box, but we will keep the horizontal line dividing main effects from side-effects. Tower convention for types:
```                                              γ | β
(α -> β) -> γ can be equivalently written -----
α
```
Read these types counter-clockwise starting at the bottom. Tower convention for values:
```                                           g[]
\k.g[k(x)] can be equivalently written ---
x
```