let T be TuringStr ; :: thesis: for t being Tape of T
for s, n being Element of NAT st t storeData <*s,n*> holds
( t . s = 0 & t . ((s + n) + 2) = 0 & ( for i being Integer st s < i & i < (s + n) + 2 holds
t . i = 1 ) )
let t be Tape of T; :: thesis: for s, n being Element of NAT st t storeData <*s,n*> holds
( t . s = 0 & t . ((s + n) + 2) = 0 & ( for i being Integer st s < i & i < (s + n) + 2 holds
t . i = 1 ) )
let s, n be Element of NAT ; :: thesis: ( t storeData <*s,n*> implies ( t . s = 0 & t . ((s + n) + 2) = 0 & ( for i being Integer st s < i & i < (s + n) + 2 holds
t . i = 1 ) ) )
assume t storeData <*s,n*> ; :: thesis: ( t . s = 0 & t . ((s + n) + 2) = 0 & ( for i being Integer st s < i & i < (s + n) + 2 holds
t . i = 1 ) )
then A1: t is_1_between s,(s + n) + 2 by Th15;
hence ( t . s = 0 & t . ((s + n) + 2) = 0 ) ; :: thesis: for i being Integer st s < i & i < (s + n) + 2 holds
t . i = 1
thus for i being Integer st s < i & i < (s + n) + 2 holds
t . i = 1 by A1; :: thesis: verum