Functional Abbreviation for Inst Expression in Turing's 1936 Paper

Question

In Turing's 1936 paper On Computable Numbers Page 30-31, and its Correction Page 1-2 :

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$.

At any stage of the motion of the machine, the number of the scanned square, the complete sequence of all symbols on the tape, and the m-configuration will be said to describe the complete configuration at that stage. The changes of the machine and tape between successive complete configurations will be called the moves of the machine.

The interpretations of the propositional functions involved are as follows :

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

$I(x,y)$ is to be interpreted as "In the complete configuration $x$ (of $M$) the square $y$ is scanned".

${K_q}_m(x)$ is to be interpreted as "In the complete configuration $x$ (of $M$) the m-configuration is $q_m$".

$F(x,y)$ is to be interpreted as "$y$ is the immediate successor of $x$".

Then, for establishing equivalence between Turing Machine and restricted Hilbert functional calculus, it is written:

$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 formula 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))] $

Answer 1

The first part of the disjunction is for stating that the next "state/m-configuration" of the machine is the one established in $Inst(q_i, S_j, S_k, L, q_l)$ (in case z takes as value the next cell of y', i.e., y), the second part of the disjunct is used to say that the part of the tape not scanned by the machine preserves its value.