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	⊢ ( 𝜑 → 𝑈 ∈ Fin )
	tmach.exindex	⊢ ( 𝜑 → 𝐼 ∈ V )
	tmach.tapelist	⊢ ( 𝜑 → 𝑇 = ( 𝑈 ↑m 𝐼 ) )
	tmach.scanmap	⊢ ( 𝜑 → 𝑆 : 𝑇 ⟶ ( 𝒫 𝐼 ∩ Fin ) )
	tmach.agreemap	⊢ ( 𝜑 → 𝐴 = ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
	tmach.agreement	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑇 ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑧 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑧 ) )
Assertion	tmachfullfin	⊢ ( 𝜑 → ∪ ran 𝑆 ∈ Fin )

Proof

Step	Hyp	Ref	Expression
1		tmach.finalph	⊢ ( 𝜑 → 𝑈 ∈ Fin )
2		tmach.exindex	⊢ ( 𝜑 → 𝐼 ∈ V )
3		tmach.tapelist	⊢ ( 𝜑 → 𝑇 = ( 𝑈 ↑m 𝐼 ) )
4		tmach.scanmap	⊢ ( 𝜑 → 𝑆 : 𝑇 ⟶ ( 𝒫 𝐼 ∩ Fin ) )
5		tmach.agreemap	⊢ ( 𝜑 → 𝐴 = ( 𝑧 ∈ 𝑇 ↦ { 𝑦 ∈ 𝑇 ∣ ( 𝑦 ↾ ( 𝑆 ‘ 𝑧 ) ) = ( 𝑧 ↾ ( 𝑆 ‘ 𝑧 ) ) } ) )
6		tmach.agreement	⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑇 ∀ 𝑦 ∈ ( 𝐴 ‘ 𝑧 ) ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑧 ) )
7	1 2 3 4 5 6	tmachlem-franscan	⊢ ( 𝜑 → ran 𝑆 ∈ Fin )
8	1 2 3 4 5 6	tmachlem-fssscan	⊢ ( 𝜑 → ran 𝑆 ⊆ Fin )
9		unifi	⊢ ( ( ran 𝑆 ∈ Fin ∧ ran 𝑆 ⊆ Fin ) → ∪ ran 𝑆 ∈ Fin )
10	7 8 9	syl2anc	⊢ ( 𝜑 → ∪ ran 𝑆 ∈ Fin )