let tm be TuringStr ; 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; 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; 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 ; 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; 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 ; ( 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
; (Computation s) . m = [p,(d + m),t]
defpred S1[ Nat] means ( $1 <= m implies (Computation s) . $1 = [p,(d + $1),t] );
A7:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A8:
S1[
k]
;
S1[k + 1]
now ( k + 1 <= m implies (Computation s) . (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
;
(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]))]
.=
the
Tran of
tm . [p,(t . (Head [p,ik,t]))]
.=
[p,1,1]
by A4, A10
;
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 A10, Th24
;
thus (Computation s) . (k + 1) =
Following [p,ik,t]
by A8, A9, Def7, NAT_1:13
.=
[((TRAN [p,ik,t]) `1_3),((Head [p,ik,t]) + (offset (TRAN [p,ik,t]))),t]
by A5, A13, Th25
.=
[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]
;
verum end;
hence
S1[
k + 1]
;
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]
; verum