In Melliès’ survey Categorical Semantics of Linear Logic, a cut elimination procedure for intuitionistic linear logic is given which includes the following case:
3.9.3 Promotion vs. contraction
The proof $$ \displaystyle\frac{ \displaystyle\frac{\displaystyle\frac{\pi_1\\\vdots}{!\Gamma \vdash A}}{!\Gamma \vdash !A} \text{ Promotion} \qquad \displaystyle\frac{\displaystyle\frac{\pi_2\\\vdots}{\Upsilon_1 , !A , !A , \Upsilon_2 \vdash B}}{\Upsilon_1 , !A , \Upsilon_2 \vdash B} \text{ Contraction} }{ \Upsilon_1 , !\Gamma , \Upsilon_2 \vdash B } \text{ Cut} $$ is transformed into the proof $$ \displaystyle\frac{ \displaystyle\frac{\displaystyle\frac{\pi_1\\\vdots}{!\Gamma \vdash A}}{!\Gamma \vdash !A} \text{ Promotion} \qquad \displaystyle\frac{ \displaystyle\frac{\displaystyle\frac{\pi_1\\\vdots}{!\Gamma \vdash A}}{!\Gamma \vdash !A} \text{ Promotion} \qquad \displaystyle\frac{\pi_2\\\vdots}{\Upsilon_1 , !A , !A , \Upsilon_2 \vdash B} }{ \Upsilon_1 , !A , !\Gamma , \Upsilon_2 \vdash B } \text{ Cut} }{ \displaystyle\frac{\Upsilon_1 , !\Gamma , !\Gamma , \Upsilon_2 \vdash B}{\Upsilon_1 , !\Gamma , \Upsilon_2 \vdash B} \rlap{\;\text{ Series of Contractions and Exchanges}} } \text{ Cut} $$
Why is this a valid inductive step? Neither the size of the cut formula nor the sizes of the derivations are decreasing. It's(In the transformed proof, the right branch of the lower cut is potentially larger after inductively eliminating the upper cut.) So it's not clear why this procedure should terminate.