# Functional abbreviation for Inst expression in Turing's 1936 paper

In Turing's 1936 paper "On Computable Numbers",

For a Turing Machine $$M$$, $$Inst(q_i S_j S_k L q_l )$$ means that if $$M$$ scans symbol $$S_j$$ under $$m-configuration$$ $$q_i$$, then the symbol on the square under scanner (with symbol $$S_j$$ ) is to be replaced by symbol $$S_k$$, and the scanner/header moves one unit $$Left$$, and its new $$m-configuration$$ becomes $$q_l$$.

If:

$${R_S}_j(x,y)$$ means "In the complete configuration $$x$$ (of $$M$$) the symbol on the square $$y$$ is $$S_j$$.

$$I(x,y)$$ means that "In the complete configuration $$x$$ (of $$M$$) the square $$y$$ is scanned".

$${K_q}_m(x)$$ means that "In the complete configuration $$x$$ (of $$M$$) the m-configuration is $$q_m$$".

$$F(x,y)$$ means that "$$y$$ is the immediate successor of $$x$$".

Then $$Inst(q_i S_j S_k L q_l )$$ is to be an abbreviation for:

$$(x,y,x',y')$$ { ($${R_S}_j(x,y) \,\&\, I(x,y)\,\&\, {K_q}_i(x) \,\&\, F(x,x') \,\&\, F(y',y)) \to$$ $$( I(x',y') \,\&\, {R_S}_k(x',y) \,\&\, {K_q}_l(x') \,\&\, F(y',z) ∨ [( {R_S}_0(x,z) \to {R_S}_0(x',z)) \,\&\, ({R_S}_1(x,z) \to {R_S}_1(x',z)) \,\&\, ... \,\&\, ({R_S}_M(x,z) \to {R_S}_M(x',z))])$$

$$S_0, S_1, ..., S_M$$ being the symbols $$M$$ can print.

I am unable to convince myself of the exact correctness of the above formulae w.r.t. to the meaning of $$Inst(q_i S_j S_k L q_l )$$. More specifically, why do we have the following expression included? What is he trying to "cover" by including it?

$$... \,\&\, F(y',z) ∨ [({R_S}_0(x,z) \to {R_S}_0(x',z)) \,\&\, ({R_S}_1(x,z) \to {R_S}_1(x',z)) \,\&\, ... \,\&\, ({R_S}_M(x,z) \to {R_S}_M(x',z))]$$