  In a previously published ENTCS paper (Santos et al. (2016)), we introduced a
sequent calculus called $\mathbf{LMT^{\rightarrow}}$ for Minimal Implicational
Propositional Logic ($\mathbf{LMT^{\rightarrow}}$). This calculus provides a
proof search procedure for $\mathbf{LMT^{\rightarrow}}$ that works in a
bottom-up approach. We proved there that $\mathbf{LMT^{\rightarrow}}$ is sound
and complete. We also suggested a strategy to guarantee termination of the
proof search procedure. In this current paper, we refined this strategy and
presented a new strategy for $\mathbf{LMT^{\rightarrow}}$ termination.
Considering this new strategy, we also provide a (new) completeness proof for
the system, which improves the previous version. Besides that, we present
explicit upper bounds on the proof search procedure, derived from this new
strategy. We also provide a full soundness proof of the system.
