let tm be TuringStr ; :: thesis: for s being All-State of tm
for p being State of tm
for h being Element of INT
for t being Tape of tm
for m, d being Element of NAT st d = h & 1 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,1,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds
t . i = 1 ) holds
(Computation s) . m = [p,(d + m),t]
let s be All-State of tm; :: thesis: for p being State of tm
for h being Element of INT
for t being Tape of tm
for m, d being Element of NAT st d = h & 1 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,1,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds
t . i = 1 ) holds
(Computation s) . m = [p,(d + m),t]
let p be State of tm; :: thesis: for h being Element of INT
for t being Tape of tm
for m, d being Element of NAT st d = h & 1 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,1,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds
t . i = 1 ) holds
(Computation s) . m = [p,(d + m),t]
let h be Element of INT ; :: thesis: for t being Tape of tm
for m, d being Element of NAT st d = h & 1 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,1,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds
t . i = 1 ) holds
(Computation s) . m = [p,(d + m),t]
let t be Tape of tm; :: thesis: for m, d being Element of NAT st d = h & 1 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,1,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds
t . i = 1 ) holds
(Computation s) . m = [p,(d + m),t]
let m, d be Element of NAT ; :: thesis: ( d = h & 1 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,1,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds
t . i = 1 ) implies (Computation s) . m = [p,(d + m),t] )
assume that
A1: d = h and
A2: 1 is Symbol of tm and
A3: s = [p,h,t] and
A4: the Tran of tm . [p,1] = [p,1,1] and
A5: p <> the AcceptS of tm and
A6: for i being Integer st d <= i & i < d + m holds
t . i = 1 ; :: thesis: (Computation s) . m = [p,(d + m),t]
defpred S₁[ Element of NAT ] means ( $1 <= m implies (Computation s) . $1 = [p,(d + $1),t] );
A7: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]

now

reconsider T = 1 as Symbol of tm by A2;
set dk = d + k;
reconsider ik = d + k as Element of INT by INT_1:def 2;
set sk = [p,ik,t];
reconsider tt = [p,ik,t] `3 as Tape of tm ;
assume A9: k + 1 <= m ; :: thesis: (Computation s) . (k + 1) = [p,(d + (k + 1)),t]
then k < m by NAT_1:13;
then d + k < d + m by XREAL_1:8;
then A10: t . ik = 1 by A6, NAT_1:11;
A11: TRAN [p,ik,t] = the Tran of tm . [p,(tt . (Head [p,ik,t]))] by MCART_1:64
.= the Tran of tm . [p,(t . (Head [p,ik,t]))] by MCART_1:64
.= [p,1,1] by A4, A10, MCART_1:64 ;
then A12: offset (TRAN [p,ik,t]) = 1 by MCART_1:64;
A13: Tape-Chg (([p,ik,t] `3),(Head [p,ik,t]),((TRAN [p,ik,t]) `2)) = Tape-Chg (t,(Head [p,ik,t]),((TRAN [p,ik,t]) `2)) by MCART_1:64
.= Tape-Chg (t,(d + k),((TRAN [p,ik,t]) `2)) by MCART_1:64
.= Tape-Chg (t,(d + k),T) by A11, MCART_1:64
.= t by A10, Th28 ;
thus (Computation s) . (k + 1) = Following [p,ik,t] by A8, A9, Def8, NAT_1:13
.= [((TRAN [p,ik,t]) `1),((Head [p,ik,t]) + (offset (TRAN [p,ik,t]))),t] by A5, A13, Th29
.= [p,((Head [p,ik,t]) + (offset (TRAN [p,ik,t]))),t] by A11, MCART_1:64
.= [p,((d + k) + 1),t] by A12, MCART_1:64
.= [p,(d + (k + 1)),t] ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A14: S₁[ 0 ] by A1, A3, Def8;
for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A14, A7);
hence (Computation s) . m = [p,(d + m),t] ; :: thesis: verum