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
() . 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
() . 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
() . 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
() . 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
() . 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 () . 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: () . m = [p,(d + m),t]
defpred S1[ Nat] means ( \$1 <= m implies () . \$1 = [p,(d + \$1),t] );
A7: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A8: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: ( k + 1 <= m implies () . (k + 1) = [p,(d + (k + 1)),t] )
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_3 as Tape of tm ;
assume A9: k + 1 <= m ; :: thesis: () . (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 ;
A11: TRAN [p,ik,t] = the Tran of tm . [p,(tt . (Head [p,ik,t]))]
.= the Tran of tm . [p,(t . (Head [p,ik,t]))]
.= [p,1,1] by ;
then A12: offset (TRAN [p,ik,t]) = 1 ;
A13: Tape-Chg (([p,ik,t] `3_3),(Head [p,ik,t]),((TRAN [p,ik,t]) `2_3)) = Tape-Chg (t,(Head [p,ik,t]),((TRAN [p,ik,t]) `2_3))
.= Tape-Chg (t,(d + k),((TRAN [p,ik,t]) `2_3))
.= Tape-Chg (t,(d + k),T) by A11
.= t by ;
thus () . (k + 1) = Following [p,ik,t] by
.= [((TRAN [p,ik,t]) `1_3),((Head [p,ik,t]) + (offset (TRAN [p,ik,t]))),t] by
.= [p,((Head [p,ik,t]) + (offset (TRAN [p,ik,t]))),t] by A11
.= [p,((d + k) + 1),t] by A12
.= [p,(d + (k + 1)),t] ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
A14: S1[ 0 ] by A1, A3, Def7;
for k being Nat holds S1[k] from NAT_1:sch 2(A14, A7);
hence (Computation s) . m = [p,(d + m),t] ; :: thesis: verum