theorem Th18: :: TURING_1:18

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 is_1_between s,(s + n1) + 2 & t is_1_between (s + n1) + 2,((s + n1) + n2) + 4 )