theorem Th19: :: TURING_1:19

for T being TuringStr
for t being Tape of T
for s, n1, n2 being Element of NAT st t storeData <*s,n1,n2*> holds
( t . s = 0 & t . ((s + n1) + 2) = 0 & t . (((s + n1) + n2) + 4) = 0 & ( for i being Integer st s < i & i < (s + n1) + 2 holds
t . i = 1 ) & ( for i being Integer st (s + n1) + 2 < i & i < ((s + n1) + n2) + 4 holds
t . i = 1 ) )