theorem Th22: :: TURING_1:22

for T being TuringStr
for t being Tape of T
for s being Element of NAT
for f being FinSequence of NAT st len f >= 1 & t storeData <*s*> ^ f holds
t is_1_between s,(s + (f /. 1)) + 2