theorem Th15: :: TURING_1:15

for T being TuringStr
for t being Tape of T
for s, n being Element of NAT st t storeData <*s,n*> holds
t is_1_between s,(s + n) + 2