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 A1:
( 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 ) )
; :: thesis: (Computation s) . m = [p,(d + m),t]
defpred S1[ Element of NAT ] means ( $1 <= m implies (Computation s) . $1 = [p,(d + $1),t] );
A2:
S1[ 0 ]
by A1, Def8;
A3:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A4:
S1[
k]
;
:: thesis: S1[k + 1]
now assume A5:
k + 1
<= m
;
:: thesis: (Computation s) . (k + 1) = [p,(d + (k + 1)),t]then A6:
k < m
by NAT_1:13;
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 ;
d + k < d + m
by A6, XREAL_1:10;
then A7:
t . ik = 1
by A1, NAT_1:11;
A8:
TRAN [p,ik,t] =
the
Tran of
tm . [p,(tt . (Head [p,ik,t]))]
by MCART_1:68
.=
the
Tran of
tm . [p,(t . (Head [p,ik,t]))]
by MCART_1:68
.=
[p,1,1]
by A1, A7, MCART_1:68
;
reconsider T = 1 as
Symbol of
tm by A1;
A9:
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:68
.=
Tape-Chg t,
(d + k),
((TRAN [p,ik,t]) `2 )
by MCART_1:68
.=
Tape-Chg t,
(d + k),
T
by A8, MCART_1:68
.=
t
by A7, Th28
;
A10:
offset (TRAN [p,ik,t]) = 1
by A8, MCART_1:68;
thus (Computation s) . (k + 1) =
Following [p,ik,t]
by A4, A5, Def8, NAT_1:13
.=
[((TRAN [p,ik,t]) `1 ),((Head [p,ik,t]) + (offset (TRAN [p,ik,t]))),t]
by A1, A9, Th29
.=
[p,((Head [p,ik,t]) + (offset (TRAN [p,ik,t]))),t]
by A8, MCART_1:68
.=
[p,((d + k) + 1),t]
by A10, MCART_1:68
.=
[p,(d + (k + 1)),t]
;
:: thesis: verum end;
hence
S1[
k + 1]
;
:: thesis: verum
end;
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A2, A3);
hence
(Computation s) . m = [p,(d + m),t]
; :: thesis: verum