Galoyan, T. M. . Analysis of Bounds for Lengths of Reductions in Typed λ-Calculus. MPCS 2021, 29, 5-15.