feat(computability/tm_to_partrec): prove finiteness (#6955)
The proof in this file was incomplete, and I finally found the time to
finish it. `tm_to_partrec.lean` constructs a turing machine that can
simulate a given partial recursive function. Previously, the functional
correctness of this machine was proven, but it uses an infinite state
space so it is not a priori obvious that it is in fact a true (finite)
turing machine, which is important for the Church-Turing theorem. This
PR adds a proof that the machine is in fact finite.
