Abstract:
Let $\varphi$ be a standard transformation [5] of Gentzen's $\mathrm L$-derivation $\alpha$ into natural deduction $\varphi(\alpha)$. We prove that $\operatorname{length}(\varphi(\alpha))\leq2^{2\cdot\operatorname{length}(\alpha)}$ where $\alpha$ is $(\&,\supset)$-Gentzen's intuitionistic $\mathrm L$-derivation.
This bound is almost optimal: an increasing sequence of $\mathrm L$-derivations $\alpha_i$ is constructed such that $\operatorname{length}(\varphi(\alpha_i))\leq2^{1/3\operatorname{length}(\alpha_i)}$.