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 S1[ 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 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 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 ) ) )
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 ) )
hereby :: thesis: for i being Integer st ( d > i or i >= d + (k + 1) ) holds
t2 . i = t . i
let i be Integer; :: thesis: ( d <= i & i < d + (k + 1) implies t2 . b1 = 0 )
assume that
A18: d <= i and
A19: i < d + (k + 1) ; :: thesis: t2 . b1 = 0
per cases ( i = d + k or i <> d + k ) ;
suppose i = d + k ; :: thesis: t2 . b1 = 0
hence t2 . i = 0 by Th26; :: thesis: verum
end;
suppose A20: i <> d + k ; :: thesis: t2 . b1 = 0
i < (d + k) + 1 by A19;
then i <= d + k by INT_1:7;
then A21: i < d + k by A20, XXREAL_0:1;
thus t2 . i = t1 . i by A20, Th26
.= 0 by A11, A18, A21 ; :: thesis: verum
end;
end;
end;
hereby :: thesis: verum
let i be Integer; :: thesis: ( ( d > i or i >= d + (k + 1) ) implies t2 . b1 = t . b1 )
assume A22: ( d > i or i >= d + (k + 1) ) ; :: thesis: t2 . b1 = t . b1
per cases ( d > i or i >= d + (k + 1) ) by A22;
suppose A23: d > i ; :: thesis: t2 . b1 = t . b1
d <= d + k by NAT_1:12;
hence t2 . i = t1 . i by A23, Th26
.= t . i by A12, A23 ;
:: thesis: verum
end;
suppose A24: i >= d + (k + 1) ; :: thesis: t2 . b1 = t . b1
k < k + 1 by NAT_1:13;
then A25: d + k < d + (k + 1) by XREAL_1:8;
then A26: i > d + k by A24, XXREAL_0:2;
thus t2 . i = t1 . i by A24, A25, Th26
.= t . i by A12, A26 ; :: thesis: verum
end;
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
A27: S1[ 0 ]
proof
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;
for k being Nat holds S1[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