Functional Abbreviation for Inst Expression in Turing's 1936 Paper 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 &quot;In the complete configuration
$x$ (of $M$) the symbol on the square $y$ is $S_j$.
$I(x,y)$ is to be interpreted as &quot;In the complete configuration $x$
(of $M$) the square $y$ is scanned&quot;.
${K_q}_m(x)$ is to be interpreted as &quot;In the complete configuration
$x$ (of $M$) the m-configuration is $q_m$&quot;.
$F(x,y)$ is to be interpreted as &quot;$y$ is the immediate successor of
$x$&quot;.

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) \,\&amp;\, I(x,y)\,\&amp;\, {K_q}_i(x) \,\&amp;\,  F(x,x') \,\&amp;\, F(y',y)) \to   $ $( I(x',y') \,\&amp;\, {R_S}_k(x',y) \,\&amp;\, {K_q}_l(x') \,\&amp;\, F(y',z)  ∨  [( 
 {R_S}_0(x,z) \to {R_S}_0(x',z))  \,\&amp;\, ({R_S}_1(x,z) \to {R_S}_1(x',z))  \,\&amp;\, ... \,\&amp;\, ({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 &quot;cover&quot; by including it?

$ ... \,\&amp;\, F(y',z) ∨ [({R_S}_0(x,z) \to {R_S}_0(x',z))  \,\&amp;\, ({R_S}_1(x,z) \to {R_S}_1(x',z))  \,\&amp;\, ... \,\&amp;\, ({R_S}_M(x,z) \to {R_S}_M(x',z))] $
The first part of the disjunction is for stating that the next &quot;state/m-configuration&quot; 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.