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 & 0 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,0,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds

t . i = 1 ) holds

ex t1 being Tape of tm st

( (Computation s) . m = [p,(d + m),t1] & ( for i being Integer st d <= i & i < d + m holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + m ) holds

t1 . i = t . i ) )

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 & 0 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,0,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds

t . i = 1 ) holds

ex t1 being Tape of tm st

( (Computation s) . m = [p,(d + m),t1] & ( for i being Integer st d <= i & i < d + m holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + m ) holds

t1 . i = t . i ) )

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 & 0 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,0,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds

t . i = 1 ) holds

ex t1 being Tape of tm st

( (Computation s) . m = [p,(d + m),t1] & ( for i being Integer st d <= i & i < d + m holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + m ) holds

t1 . i = t . i ) )

let h be Element of INT ; :: thesis: for t being Tape of tm

for m, d being Element of NAT st d = h & 0 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,0,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds

t . i = 1 ) holds

ex t1 being Tape of tm st

( (Computation s) . m = [p,(d + m),t1] & ( for i being Integer st d <= i & i < d + m holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + m ) holds

t1 . i = t . i ) )

let t be Tape of tm; :: thesis: for m, d being Element of NAT st d = h & 0 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,0,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds

t . i = 1 ) holds

ex t1 being Tape of tm st

( (Computation s) . m = [p,(d + m),t1] & ( for i being Integer st d <= i & i < d + m holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + m ) holds

t1 . i = t . i ) )

let m, d be Element of NAT ; :: thesis: ( d = h & 0 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,0,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds

t . i = 1 ) implies ex t1 being Tape of tm st

( (Computation s) . m = [p,(d + m),t1] & ( for i being Integer st d <= i & i < d + m holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + m ) holds

t1 . i = t . i ) ) )

assume that

A1: d = h and

A2: 0 is Symbol of tm and

A3: s = [p,h,t] and

A4: the Tran of tm . [p,1] = [p,0,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: ex t1 being Tape of tm st

( (Computation s) . m = [p,(d + m),t1] & ( for i being Integer st d <= i & i < d + m holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + m ) holds

t1 . i = t . i ) )

defpred S_{1}[ Nat] means ( $1 <= m implies ex t1 being Tape of tm st

( (Computation s) . $1 = [p,(d + $1),t1] & ( for i being Integer st d <= i & i < d + $1 holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + $1 ) holds

t1 . i = t . i ) ) );

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

S_{1}[k + 1]
_{1}[ 0 ]
_{1}[k]
from NAT_1:sch 2(A27, A7);

hence ex t1 being Tape of tm st

( (Computation s) . m = [p,(d + m),t1] & ( for i being Integer st d <= i & i < d + m holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + m ) holds

t1 . i = t . i ) ) ; :: 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 & 0 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,0,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds

t . i = 1 ) holds

ex t1 being Tape of tm st

( (Computation s) . m = [p,(d + m),t1] & ( for i being Integer st d <= i & i < d + m holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + m ) holds

t1 . i = t . i ) )

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 & 0 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,0,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds

t . i = 1 ) holds

ex t1 being Tape of tm st

( (Computation s) . m = [p,(d + m),t1] & ( for i being Integer st d <= i & i < d + m holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + m ) holds

t1 . i = t . i ) )

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 & 0 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,0,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds

t . i = 1 ) holds

ex t1 being Tape of tm st

( (Computation s) . m = [p,(d + m),t1] & ( for i being Integer st d <= i & i < d + m holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + m ) holds

t1 . i = t . i ) )

let h be Element of INT ; :: thesis: for t being Tape of tm

for m, d being Element of NAT st d = h & 0 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,0,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds

t . i = 1 ) holds

ex t1 being Tape of tm st

( (Computation s) . m = [p,(d + m),t1] & ( for i being Integer st d <= i & i < d + m holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + m ) holds

t1 . i = t . i ) )

let t be Tape of tm; :: thesis: for m, d being Element of NAT st d = h & 0 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,0,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds

t . i = 1 ) holds

ex t1 being Tape of tm st

( (Computation s) . m = [p,(d + m),t1] & ( for i being Integer st d <= i & i < d + m holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + m ) holds

t1 . i = t . i ) )

let m, d be Element of NAT ; :: thesis: ( d = h & 0 is Symbol of tm & s = [p,h,t] & the Tran of tm . [p,1] = [p,0,1] & p <> the AcceptS of tm & ( for i being Integer st d <= i & i < d + m holds

t . i = 1 ) implies ex t1 being Tape of tm st

( (Computation s) . m = [p,(d + m),t1] & ( for i being Integer st d <= i & i < d + m holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + m ) holds

t1 . i = t . i ) ) )

assume that

A1: d = h and

A2: 0 is Symbol of tm and

A3: s = [p,h,t] and

A4: the Tran of tm . [p,1] = [p,0,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: ex t1 being Tape of tm st

( (Computation s) . m = [p,(d + m),t1] & ( for i being Integer st d <= i & i < d + m holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + m ) holds

t1 . i = t . i ) )

defpred S

( (Computation s) . $1 = [p,(d + $1),t1] & ( for i being Integer st d <= i & i < d + $1 holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + $1 ) holds

t1 . i = t . i ) ) );

A7: for k being Nat st S

S

proof

A27:
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 ex t2 being Tape of tm st

( (Computation s) . (k + 1) = [p,(d + (k + 1)),t2] & ( for i being Integer st d <= i & i < d + (k + 1) holds

t2 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + (k + 1) ) holds

t2 . i = t . i ) ) )

hence
S( (Computation s) . (k + 1) = [p,(d + (k + 1)),t2] & ( for i being Integer st d <= i & i < d + (k + 1) holds

t2 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + (k + 1) ) holds

t2 . i = t . i ) ) )

reconsider F = 0 as Symbol of tm by A2;

set dk = d + k;

reconsider ik = d + k as Element of INT by INT_1:def 2;

assume A9: k + 1 <= m ; :: thesis: ex t2 being Tape of tm st

( (Computation s) . (k + 1) = [p,(d + (k + 1)),t2] & ( for i being Integer st d <= i & i < d + (k + 1) holds

t2 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + (k + 1) ) holds

t2 . i = t . i ) )

then consider t1 being Tape of tm such that

A10: (Computation s) . k = [p,(d + k),t1] and

A11: for i being Integer st d <= i & i < d + k holds

t1 . i = 0 and

A12: for i being Integer st ( d > i or i >= d + k ) holds

t1 . i = t . i by A8, NAT_1:13;

k < m by A9, NAT_1:13;

then A13: d + k < d + m by XREAL_1:8;

A14: t1 . ik = t . ik by A12

.= 1 by A6, A13, NAT_1:11 ;

take t2 = Tape-Chg (t1,(d + k),F); :: thesis: ( (Computation s) . (k + 1) = [p,(d + (k + 1)),t2] & ( for i being Integer st d <= i & i < d + (k + 1) holds

t2 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + (k + 1) ) holds

t2 . i = t . i ) )

set sk = [p,ik,t1];

reconsider tt = [p,ik,t1] `3_3 as Tape of tm ;

A15: TRAN [p,ik,t1] = the Tran of tm . [p,(tt . (Head [p,ik,t1]))]

.= the Tran of tm . [p,(t1 . (Head [p,ik,t1]))]

.= [p,0,1] by A4, A14 ;

then A16: offset (TRAN [p,ik,t1]) = 1 ;

A17: Tape-Chg (([p,ik,t1] `3_3),(Head [p,ik,t1]),((TRAN [p,ik,t1]) `2_3)) = Tape-Chg (t1,(Head [p,ik,t1]),((TRAN [p,ik,t1]) `2_3))

.= Tape-Chg (t1,(d + k),((TRAN [p,ik,t1]) `2_3))

.= t2 by A15 ;

thus (Computation s) . (k + 1) = Following [p,ik,t1] by A10, Def7

.= [((TRAN [p,ik,t1]) `1_3),((Head [p,ik,t1]) + (offset (TRAN [p,ik,t1]))),t2] by A5, A17, Th25

.= [p,((Head [p,ik,t1]) + (offset (TRAN [p,ik,t1]))),t2] by A15

.= [p,((d + k) + 1),t2] by A16

.= [p,(d + (k + 1)),t2] ; :: thesis: ( ( for i being Integer st d <= i & i < d + (k + 1) holds

t2 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + (k + 1) ) holds

t2 . i = t . i ) )

end;set dk = d + k;

reconsider ik = d + k as Element of INT by INT_1:def 2;

assume A9: k + 1 <= m ; :: thesis: ex t2 being Tape of tm st

( (Computation s) . (k + 1) = [p,(d + (k + 1)),t2] & ( for i being Integer st d <= i & i < d + (k + 1) holds

t2 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + (k + 1) ) holds

t2 . i = t . i ) )

then consider t1 being Tape of tm such that

A10: (Computation s) . k = [p,(d + k),t1] and

A11: for i being Integer st d <= i & i < d + k holds

t1 . i = 0 and

A12: for i being Integer st ( d > i or i >= d + k ) holds

t1 . i = t . i by A8, NAT_1:13;

k < m by A9, NAT_1:13;

then A13: d + k < d + m by XREAL_1:8;

A14: t1 . ik = t . ik by A12

.= 1 by A6, A13, NAT_1:11 ;

take t2 = Tape-Chg (t1,(d + k),F); :: thesis: ( (Computation s) . (k + 1) = [p,(d + (k + 1)),t2] & ( for i being Integer st d <= i & i < d + (k + 1) holds

t2 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + (k + 1) ) holds

t2 . i = t . i ) )

set sk = [p,ik,t1];

reconsider tt = [p,ik,t1] `3_3 as Tape of tm ;

A15: TRAN [p,ik,t1] = the Tran of tm . [p,(tt . (Head [p,ik,t1]))]

.= the Tran of tm . [p,(t1 . (Head [p,ik,t1]))]

.= [p,0,1] by A4, A14 ;

then A16: offset (TRAN [p,ik,t1]) = 1 ;

A17: Tape-Chg (([p,ik,t1] `3_3),(Head [p,ik,t1]),((TRAN [p,ik,t1]) `2_3)) = Tape-Chg (t1,(Head [p,ik,t1]),((TRAN [p,ik,t1]) `2_3))

.= Tape-Chg (t1,(d + k),((TRAN [p,ik,t1]) `2_3))

.= t2 by A15 ;

thus (Computation s) . (k + 1) = Following [p,ik,t1] by A10, Def7

.= [((TRAN [p,ik,t1]) `1_3),((Head [p,ik,t1]) + (offset (TRAN [p,ik,t1]))),t2] by A5, A17, Th25

.= [p,((Head [p,ik,t1]) + (offset (TRAN [p,ik,t1]))),t2] by A15

.= [p,((d + k) + 1),t2] by A16

.= [p,(d + (k + 1)),t2] ; :: thesis: ( ( for i being Integer st d <= i & i < d + (k + 1) holds

t2 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + (k + 1) ) holds

t2 . i = t . i ) )

hereby :: thesis: for i being Integer st ( d > i or i >= d + (k + 1) ) holds

t2 . i = t . i

t2 . i = t . i

let i be Integer; :: thesis: ( d <= i & i < d + (k + 1) implies t2 . b_{1} = 0 )

assume that

A18: d <= i and

A19: i < d + (k + 1) ; :: thesis: t2 . b_{1} = 0

end;assume that

A18: d <= i and

A19: i < d + (k + 1) ; :: thesis: t2 . b

hereby :: thesis: verum

let i be Integer; :: thesis: ( ( d > i or i >= d + (k + 1) ) implies t2 . b_{1} = t . b_{1} )

assume A22: ( d > i or i >= d + (k + 1) ) ; :: thesis: t2 . b_{1} = t . b_{1}

end;assume A22: ( d > i or i >= d + (k + 1) ) ; :: thesis: t2 . b

proof

for k being Nat holds S
assume
0 <= m
; :: thesis: ex t1 being Tape of tm st

( (Computation s) . 0 = [p,(d + 0),t1] & ( for i being Integer st d <= i & i < d + 0 holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + 0 ) holds

t1 . i = t . i ) )

take t1 = t; :: thesis: ( (Computation s) . 0 = [p,(d + 0),t1] & ( for i being Integer st d <= i & i < d + 0 holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + 0 ) holds

t1 . i = t . i ) )

thus (Computation s) . 0 = [p,(d + 0),t1] by A1, A3, Def7; :: thesis: ( ( for i being Integer st d <= i & i < d + 0 holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + 0 ) holds

t1 . i = t . i ) )

thus for i being Integer st d <= i & i < d + 0 holds

t1 . i = 0 ; :: thesis: for i being Integer st ( d > i or i >= d + 0 ) holds

t1 . i = t . i

thus for i being Integer st ( d > i or i >= d + 0 ) holds

t1 . i = t . i ; :: thesis: verum

end;( (Computation s) . 0 = [p,(d + 0),t1] & ( for i being Integer st d <= i & i < d + 0 holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + 0 ) holds

t1 . i = t . i ) )

take t1 = t; :: thesis: ( (Computation s) . 0 = [p,(d + 0),t1] & ( for i being Integer st d <= i & i < d + 0 holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + 0 ) holds

t1 . i = t . i ) )

thus (Computation s) . 0 = [p,(d + 0),t1] by A1, A3, Def7; :: thesis: ( ( for i being Integer st d <= i & i < d + 0 holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + 0 ) holds

t1 . i = t . i ) )

thus for i being Integer st d <= i & i < d + 0 holds

t1 . i = 0 ; :: thesis: for i being Integer st ( d > i or i >= d + 0 ) holds

t1 . i = t . i

thus for i being Integer st ( d > i or i >= d + 0 ) holds

t1 . i = t . i ; :: thesis: verum

hence ex t1 being Tape of tm st

( (Computation s) . m = [p,(d + m),t1] & ( for i being Integer st d <= i & i < d + m holds

t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + m ) holds

t1 . i = t . i ) ) ; :: thesis: verum