theorem Th17: :: TURING_1:17

for T being TuringStr
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 ) )