Consider the following rules to check whether a lambda terms in
\emph{linear}, \ie if every argument variable occurs exactly once:
\newcommand{\lin}{\mbox{ linear}}
\newcommand{\vdx}{\vd^x}
\bca
\ianc{}{\GG,x\vd x \lin}{\linear\atm}\qquad
\ibnc{\GG\vd e_1 \lin}{\GG\vd e_2\lin}{\GG\vd e_1\ e_2 \lin}{\lin\cdot}
\vsk
\ibnc{\vdx \lx e\lin}{\GG,x\vd e\lin}{\GG\vd \lx e\lin}{\lin\l}
\vsk\vsk
\ianc{}{\vdx \lx x\lin}{\vdx\l}
\qquad
\ianc{\vdx\lx e}{\vdx\lx \ly e\lin}{\vdx\l}
\vsk 
\ianc{\vdx \lx e_1\lin}{\vdx\lx e_1 \ e_2\lin}{\vdx_1\cdot} 
\qquad
\ianc{\vdx \lx e_2\lin}{\vdx\lx e_1 \ e_2\lin}{\vdx_2\cdot} 
\eca


Intutitively, we check for linearity of a function making sure that
the latter is linear in its first argument (judgment $\vdx\lx e\lin$)
and then recurring on the rest of the expression. 