Theorem tmachfullfin

Description: Folk theorem. For any algorithm deterministically processing a stream of data (essentially, an infinite tape with cell indices I and finite alphabet U ), if it terminates on every possible input, then it never looks beyond a finite portion U. ran S of the input.

Termination is expressed here with a weaker condition: that an execution may only look at a finite number of cells. Obviously, a program which finishes in a finite number of steps can only scan finite set of cells.

This theorem has many corollaries, such as: any encoding scheme able to represent all integers has at least one non-decodable tape (in other terms, encoding of the infinity).

I no longer have the source for this theorem but I believe I first read about it on LessWrong. My gratitude to Grok for suggesting that this theorem will require Axiom of Choice, and to DeepSeek for suggesting the topology-based proof route. (Contributed by Ender Ting, 28-Jul-2026)

	Ref	Expression
Hypotheses	tmach.finalph	$$⊢\phi \to U\in \mathrm{Fin}$$
	tmach.exindex	$$⊢\phi \to I\in \mathrm{V}$$
	tmach.tapelist	$$⊢\phi \to T=U^I$$
	tmach.scanmap	$$⊢\phi \to S:T⟶𝒫I\cap \mathrm{Fin}$$
	tmach.agreemap	$$⊢\phi \to A=\left(z\in T⟼\left\{y\in T|{y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\right\}\right)$$
	tmach.agreement	$$⊢\phi \to \forall z\in T\forall y\in A\left(z\right)S\left(y\right)=S\left(z\right)$$
Assertion	tmachfullfin	$$⊢\phi \to \bigcup \mathrm{ran}S\in \mathrm{Fin}$$

Proof

Step	Hyp	Ref	Expression
1		tmach.finalph	$$⊢\phi \to U\in \mathrm{Fin}$$
2		tmach.exindex	$$⊢\phi \to I\in \mathrm{V}$$
3		tmach.tapelist	$$⊢\phi \to T=U^I$$
4		tmach.scanmap	$$⊢\phi \to S:T⟶𝒫I\cap \mathrm{Fin}$$
5		tmach.agreemap	$$⊢\phi \to A=\left(z\in T⟼\left\{y\in T|{y\upharpoonright }_{S\left(z\right)}={z\upharpoonright }_{S\left(z\right)}\right\}\right)$$
6		tmach.agreement	$$⊢\phi \to \forall z\in T\forall y\in A\left(z\right)S\left(y\right)=S\left(z\right)$$
7	1 2 3 4 5 6	tmachlem-franscan	$$⊢\phi \to \mathrm{ran}S\in \mathrm{Fin}$$
8	1 2 3 4 5 6	tmachlem-fssscan	$$⊢\phi \to \mathrm{ran}S\subseteq \mathrm{Fin}$$
9		unifi	$$⊢\left(\mathrm{ran}S\in \mathrm{Fin}\wedge \mathrm{ran}S\subseteq \mathrm{Fin}\right)\to \bigcup \mathrm{ran}S\in \mathrm{Fin}$$
10	7 8 9	syl2anc	$$⊢\phi \to \bigcup \mathrm{ran}S\in \mathrm{Fin}$$