[lifis]

That only provides a proof if the machine halts in a number of steps that you can compute. Otherwise, it is unable to determine whether the machine halts later or doesn't halt at all, which is the current situation.