# How to build a TM which decides $L_k := \{(\langle M \rangle ,x)\in HP : |(\langle M \rangle ,x)| \le k \}$

For a specific natural $$k$$ we define the language of couples $$(\langle M \rangle, x)$$ such that $$M$$ stops on $$x$$ and the couple's encoding is bounded by $$k$$ i.e $$L_k := \{(\langle M \rangle ,x)\in HP : |(\langle M \rangle ,x)| \le k \}$$ This language is finite thus in $$R$$. I wish to understand how to build (Not formally) a TM, $$\tilde{M}$$ which decide this language. Since the only given information is that the encoding is bounded, I tried to think about "Pigeonhole" claim, i.e define $$\tilde{M}$$ which simulate $$M$$ computation on $$x$$ and remembering the configurations made by $$M$$ or by counting steps made by $$M$$ during the simulation in order to determine that $$M$$ is stuck in a loop. Since $$M$$ is deterministic, if $$\tilde{M}$$ "see" the same configuration twice, it guarantees that $$M$$ entered a loop, but I can't explain why the finite encoding of $$(\langle M \rangle,x)$$ promises that a configuration will repeat itself.

You cannot construct an explicit algorithm/TM which will decide the language $$L_k$$. Regarding your attempt at the proof: you are right that there is no guarantee that the configuration will repeat because these machines are not given to be space bounded.
The TM $$M_k$$ to decide $$L_k$$ will have all the tuples (which are finite in number) which are accepted hard coded in it. The TM will basically perform a search in a look up table: if that tuple is found then accept it, else reject. We don't care how these tuples are actually obtained.
We can perhaps even prove that a general method to construct such TM $$M_k$$ for each $$L_k$$ cannot exists: Suppse there exists, then for a given input $$$$, find the length of input, let it be $$k$$ and construct the TM $$M_k$$. Simulate $$M_k$$ over $$$$. This will act as a decider for Halting Problem: which we know is undecidable. Hence, the assumption that we can have such a method is false.