theorem Th16: :: TURING_1:16

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