In this current work, we present an upper bound to the proof search procedure of
\(\mathbf {LMT^{\rightarrow }}\)  via translation functions from very known deductive systems for \(\mathbf {M}^{\rightarrow }\) ,
Prawitz's Natural Deduction ([1]}) and Gentzen's sequent calculus
([2]}). These translation functions together with a strategy to
apply the rules of \(\mathbf {LMT^{\rightarrow }}\)   provide termination for the proof search procedure.
Besides that, we show here all counter-model generation cases, including those
missed in [3]}.
