Commit 2021-10-28 17:00 628f418d
View on Github →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.