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_{1}[ Nat] means ( $1 <= m implies (Computation s) . $1 = [p,(d + $1),t] );

A7: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by A1, A3, Def7;

for k being Nat holds S_{1}[k]
from NAT_1:sch 2(A14, A7);

hence (Computation s) . m = [p,(d + m),t] ; :: thesis: verum

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

A7: for k being Nat st S

S

proof

A14:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A8: S_{1}[k]
; :: thesis: S_{1}[k + 1]

_{1}[k + 1]
; :: thesis: verum

end;assume A8: S

now :: thesis: ( k + 1 <= m implies (Computation s) . (k + 1) = [p,(d + (k + 1)),t] )

hence
Sreconsider 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: (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] ; :: thesis: verum

end;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: (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] ; :: thesis: verum

for k being Nat holds S

hence (Computation s) . m = [p,(d + m),t] ; :: thesis: verum