**1. Context**  
While trying to answer my [question] on the existence of a (useful) graphical calculus for star-autonomous categories, I came across the paper [*Natural deduction and coherence for weakly distributive categories*] by Blute, Cockett, Seely and Trimble.
After having defined *circuits* (for given types $\mathscr{T}$ and components $\mathscr{C}$) they look at particular typed circuits, namely *$(\otimes,\oplus)$-circuits with components $\mathscr{C}$ and atomic types $\mathscr{A}$*. Among the components $\mathscr{C}$ are *links* called $\otimes$-introduction and $\otimes$-elimination:

| component links | terminology |
| ------ | -------- |
| [A,B] $\otimes$I [A $\otimes$ B] | $\otimes$-introduction |
| [A $\otimes$ B] $\otimes$E [A,B] | $\otimes$-elimination |

Pictorially they are represented as follows:
[![enter image description here][1]][1]

Blute et al write on page 241:
> Proof theoretically the $\otimes I$ link corresponds to the right-introduction rule for the tensor and $\otimes E$ to the left-introduction rule of the tensor.
\begin{equation}
\dfrac{{\Gamma_1\vdash \Gamma_2,A,\Gamma_3}\qquad{\Delta_1\vdash \Delta_2,B,\Delta_3}}{\Gamma_1, \Delta_1 \vdash \Gamma_2, \Delta_2, A \otimes B, \Gamma_3, \Delta_3}(\otimes R)
\end{equation}
\begin{equation}
\dfrac{{\Gamma_1,A,B,\Gamma_2\vdash \Gamma_3}}{\Gamma_1,A \otimes B, \Gamma_2 \vdash \Gamma_3}(\otimes L)
\end{equation}

**2. Questions**  
I do not see how the above links correspond to the given rules of inference. For instance, the $\otimes$-elimination is an elimination rule while $\otimes L$ is an introduction rule. 
Furthermore, the two links simply seem a reflection of one another (in their pictorial representation a horizontal reflection) while the rules of inference appear to have a greater structural difference. The right-introduction rule derives from two sequents a third while the left-introduction "only uses one sequent".

* How does the correspondence between the above rules of inference and links look like? 
* Does one read the right-hand side of the sequents in the derivation from top to bottom while the left-hand side is read from bottom to top? If so, why?

[question]:https://math.stackexchange.com/questions/4423085/graphical-calculus-for-star-autonomous-categories
[*Natural deduction and coherence for weakly distributive categories*]: https://www.math.mcgill.ca/rags/nets/nets.pdf


 


  [1]: https://i.sstatic.net/SVkF5.jpg