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 A1: ( 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 ) ) ; :: 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[ Element of 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 ) ) );
A2: 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, Def8; :: 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;
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: 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 A6: k < m by NAT_1:13;
consider t1 being Tape of tm such that
A7: ( (Computation s) . k = [p,(d + k),t1] & ( for i being Integer st d <= i & i < d + k holds
t1 . i = 0 ) & ( for i being Integer st ( d > i or i >= d + k ) holds
t1 . i = t . i ) ) by A4, A5, NAT_1:13;
set dk = d + k;
reconsider ik = d + k as Element of INT by INT_1:def 2;
set sk = [p,ik,t1];
reconsider tt = [p,ik,t1] `3 as Tape of tm ;
A8: d + k < d + m by A6, XREAL_1:10;
A9: t1 . ik = t . ik by A7
.= 1 by A1, A8, NAT_1:11 ;
A10: TRAN [p,ik,t1] = the Tran of tm . [p,(tt . (Head [p,ik,t1]))] by MCART_1:68
.= the Tran of tm . [p,(t1 . (Head [p,ik,t1]))] by MCART_1:68
.= [p,0 ,1] by A1, A9, MCART_1:68 ;
reconsider F = 0 as Symbol of tm by A1;
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 ) )
A11: Tape-Chg ([p,ik,t1] `3 ),(Head [p,ik,t1]),((TRAN [p,ik,t1]) `2 ) = Tape-Chg t1,(Head [p,ik,t1]),((TRAN [p,ik,t1]) `2 ) by MCART_1:68
.= Tape-Chg t1,(d + k),((TRAN [p,ik,t1]) `2 ) by MCART_1:68
.= t2 by A10, MCART_1:68 ;
A12: offset (TRAN [p,ik,t1]) = 1 by A10, MCART_1:68;
thus (Computation s) . (k + 1) = Following [p,ik,t1] by A7, Def8
.= [((TRAN [p,ik,t1]) `1 ),((Head [p,ik,t1]) + (offset (TRAN [p,ik,t1]))),t2] by A1, A11, Th29
.= [p,((Head [p,ik,t1]) + (offset (TRAN [p,ik,t1]))),t2] by A10, MCART_1:68
.= [p,((d + k) + 1),t2] by A12, MCART_1:68
.= [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 A13: ( d <= i & 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 Th30; :: thesis: verum
end;
suppose A14: i <> d + k ; :: thesis: t2 . b1 = 0
i < (d + k) + 1 by A13;
then i <= d + k by INT_1:20;
then A15: i < d + k by A14, XXREAL_0:1;
thus t2 . i = t1 . i by A14, Th30
.= 0 by A7, A13, A15 ; :: 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 A16: ( d > i or i >= d + (k + 1) ) ; :: thesis: t2 . b1 = t . b1
per cases ( d > i or i >= d + (k + 1) ) by A16;
suppose A17: d > i ; :: thesis: t2 . b1 = t . b1
d <= d + k by NAT_1:12;
hence t2 . i = t1 . i by A17, Th30
.= t . i by A7, A17 ;
:: thesis: verum
end;
suppose A18: i >= d + (k + 1) ; :: thesis: t2 . b1 = t . b1
k < k + 1 by NAT_1:13;
then A19: d + k < d + (k + 1) by XREAL_1:10;
then A20: i > d + k by A18, XXREAL_0:2;
thus t2 . i = t1 . i by A18, A19, Th30
.= t . i by A7, A20 ; :: thesis: verum
end;
end;
end;
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 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