Theorem tmachfullfin 47883

Description: Folk theorem. For any algorithm deterministically processing a stream of data (essentially, an infinite tape with cell indices 𝐼 and finite alphabet 𝑈), if it terminates on every possible input, then it never looks beyond a finite portion ∪ ran 𝑆 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.)

Hypotheses

Ref	Expression
tmach.finalph	⊢ (𝜑 → 𝑈 ∈ Fin)
tmach.exindex	⊢ (𝜑 → 𝐼 ∈ V)
tmach.tapelist	⊢ (𝜑 → 𝑇 = (𝑈 ↑m 𝐼))
tmach.scanmap	⊢ (𝜑 → 𝑆:𝑇⟶(𝒫 𝐼 ∩ Fin))
tmach.agreemap	⊢ (𝜑 → 𝐴 = (𝑧 ∈ 𝑇 ↦ {𝑦 ∈ 𝑇 ∣ (𝑦 ↾ (𝑆‘𝑧)) = (𝑧 ↾ (𝑆‘𝑧))}))
tmach.agreement	⊢ (𝜑 → ∀𝑧 ∈ 𝑇 ∀𝑦 ∈ (𝐴‘𝑧)(𝑆‘𝑦) = (𝑆‘𝑧))

Assertion

Ref	Expression
tmachfullfin	⊢ (𝜑 → ∪ ran 𝑆 ∈ Fin)

Distinct variable groups:   𝑦,𝑈,𝑧   𝑦,𝐼,𝑧   𝜑,𝑦,𝑧   𝑦,𝑆,𝑧   𝑦,𝐴,𝑧   𝑦,𝑇,𝑧

Proof of Theorem tmachfullfin

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2145  ∀wral 3076  {crab 3412  Vcvv 3450   ∩ cin 3897   ⊆ wss 3898  𝒫 cpw 4556  ∪ cuni 4866   ↦ cmpt 5185  ran crn 5648   ↾ cres 5649  ⟶wf 6523  ‘cfv 6527  (class class class)co 7408   ↑_m cmap 8825  Fincfn 8951

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7734  ax-ac2 10512

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-int 4907  df-iun 4952  df-iin 4953  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5542  df-eprel 5547  df-po 5555  df-so 5556  df-fr 5600  df-se 5601  df-we 5602  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-pred 6293  df-ord 6354  df-on 6355  df-lim 6356  df-suc 6357  df-iota 6483  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-isom 6536  df-riota 7365  df-ov 7411  df-oprab 7412  df-mpo 7413  df-rpss 7722  df-om 7861  df-1st 7984  df-2nd 7985  df-frecs 8277  df-wrecs 8308  df-recs 8357  df-rdg 8396  df-1o 8454  df-2o 8455  df-oadd 8458  df-omul 8459  df-er 8695  df-map 8827  df-ixp 8904  df-en 8952  df-dom 8953  df-fin 8955  df-fi 9381  df-wdom 9537  df-dju 9953  df-card 9991  df-acn 9994  df-ac 10166  df-topgen 17575  df-pt 17576  df-fbas 21636  df-fg 21637  df-top 23173  df-topon 23190  df-bases 23225  df-cld 23298  df-ntr 23299  df-cls 23300  df-nei 23377  df-cmp 23666  df-fil 24126  df-ufil 24181  df-ufl 24182  df-flim 24219  df-fcls 24221

This theorem is used by: (None)