Theorem tmachlem-finscan

Description: Execution on any tape only scanned a finite number of cells. (Contributed by Ender Ting, 27-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	tmachlem-finscan	$$⊢\left(\phi \wedge a\in T\right)\to S\left(a\right)\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	4	ffvelcdmda	$$⊢\left(\phi \wedge a\in T\right)\to S\left(a\right)\in \left(𝒫I\cap \mathrm{Fin}\right)$$
8	7	elin2d	$$⊢\left(\phi \wedge a\in T\right)\to S\left(a\right)\in \mathrm{Fin}$$